Skip to content

Commit 1431c68

Browse files
committed
Remove some useless custom data keys from witnesses
1 parent 49beeef commit 1431c68

File tree

1 file changed

+9
-9
lines changed

1 file changed

+9
-9
lines changed

src/witness/witness.ml

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -90,14 +90,14 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
9090
GML.write_key g "edge" "threadId" "string" None;
9191
GML.write_key g "edge" "createThread" "string" None;
9292

93-
GML.write_key g "node" "goblintNode" "string" None;
94-
GML.write_key g "node" "sourcecode" "string" None;
93+
(* GML.write_key g "node" "goblintNode" "string" None; *)
94+
(* GML.write_key g "node" "sourcecode" "string" None; *)
9595
GML.write_key g "edge" "goblintEdge" "string" None;
9696
GML.write_key g "edge" "goblintLine" "string" None;
9797
GML.write_key g "edge" "goblintControl" "string" None;
9898
(* TODO: remove *)
99-
GML.write_key g "edge" "enterFunction2" "string" None;
100-
GML.write_key g "edge" "returnFromFunction2" "string" None;
99+
(* GML.write_key g "edge" "enterFunction2" "string" None;
100+
GML.write_key g "edge" "returnFromFunction2" "string" None; *)
101101

102102
GML.start_graph g;
103103

@@ -145,11 +145,11 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
145145
else
146146
[]
147147
end;
148-
begin match cfgnode with
148+
(* begin match cfgnode with
149149
| Statement s ->
150150
[("sourcecode", Pretty.sprint 80 (Basetype.CilStmt.pretty () s))] (* TODO: sourcecode not official? especially on node? *)
151151
| _ -> []
152-
end;
152+
end; *)
153153
(* violation actually only allowed in violation witness *)
154154
(* maybe should appear on from_node of entry edge instead *)
155155
begin if TaskResult.is_violation node then
@@ -167,7 +167,7 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
167167
| Function f -> Printf.sprintf "ret%d%s" f.vid f.vname
168168
| FunctionEntry f -> Printf.sprintf "fun%d%s" f.vid f.vname
169169
)] *)
170-
[("goblintNode", N.to_string node)]
170+
(* [("goblintNode", N.to_string node)] *)
171171
])
172172
in
173173
let write_edge from_node edge to_node =
@@ -214,10 +214,10 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
214214
end
215215
(* enter and return on other side of nodes,
216216
more correct loc (startline) but had some scope problem? *)
217-
| MyARG.CFGEdge (Entry f) ->
217+
(* | MyARG.CFGEdge (Entry f) ->
218218
[("enterFunction2", f.svar.vname)]
219219
| MyARG.CFGEdge (Ret (_, f)) ->
220-
[("returnFromFunction2", f.svar.vname)]
220+
[("returnFromFunction2", f.svar.vname)] *)
221221
| _ -> []
222222
end;
223223
[("goblintEdge", Arg.Edge.to_string edge)]

0 commit comments

Comments
 (0)