From 7ad12249c111c7dbdb906be7f57311c49a3a15be Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 30 Oct 2023 16:52:50 +0200 Subject: [PATCH 1/5] Move GraphML witness options into witness.graphml (issue #1217) --- conf/ldv-races.json | 6 +- conf/svcomp-yaml.json | 4 +- conf/svcomp.json | 6 +- conf/svcomp21.json | 4 +- ...vcomp22-intervals-novareq-affeq-apron.json | 6 +- ...comp22-intervals-novareq-affeq-native.json | 6 +- ...omp22-intervals-novareq-octagon-apron.json | 6 +- ...p22-intervals-novareq-polyhedra-apron.json | 6 +- conf/svcomp22.json | 6 +- conf/svcomp23.json | 6 +- src/common/util/options.schema.json | 93 ++++++++++--------- src/framework/control.ml | 2 +- src/witness/myARG.ml | 4 +- src/witness/witness.ml | 14 +-- sv-comp/sv-comp-run-no-overflow.py | 2 +- sv-comp/sv-comp-run.py | 2 +- .../observer/path_nofun_true-unreach-call.c | 2 +- 17 files changed, 101 insertions(+), 74 deletions(-) diff --git a/conf/ldv-races.json b/conf/ldv-races.json index 01c60efc8d..2840bb368c 100644 --- a/conf/ldv-races.json +++ b/conf/ldv-races.json @@ -53,8 +53,10 @@ } }, "witness": { - "id": "enumerate", - "unknown": false + "graphml": { + "id": "enumerate", + "unknown": false + } }, "solver": "td3", "sem": { diff --git a/conf/svcomp-yaml.json b/conf/svcomp-yaml.json index e09d1c80d7..10a977ff47 100644 --- a/conf/svcomp-yaml.json +++ b/conf/svcomp-yaml.json @@ -76,7 +76,9 @@ "region-offsets": true }, "witness": { - "enabled": false, + "graphml": { + "enabled": false + }, "yaml": { "enabled": true }, diff --git a/conf/svcomp.json b/conf/svcomp.json index 913d43784b..87fef277c3 100644 --- a/conf/svcomp.json +++ b/conf/svcomp.json @@ -90,8 +90,10 @@ } }, "witness": { - "id": "enumerate", - "unknown": false + "graphml": { + "id": "enumerate", + "unknown": false + } }, "pre": { "enabled": false diff --git a/conf/svcomp21.json b/conf/svcomp21.json index a19bfdb9d0..eda5cdfb88 100644 --- a/conf/svcomp21.json +++ b/conf/svcomp21.json @@ -64,6 +64,8 @@ } }, "witness": { - "id": "enumerate" + "graphml": { + "id": "enumerate" + } } } diff --git a/conf/svcomp22-intervals-novareq-affeq-apron.json b/conf/svcomp22-intervals-novareq-affeq-apron.json index 7f72f5d0d8..1dafe0a76d 100644 --- a/conf/svcomp22-intervals-novareq-affeq-apron.json +++ b/conf/svcomp22-intervals-novareq-affeq-apron.json @@ -68,7 +68,9 @@ } }, "witness": { - "id": "enumerate", - "unknown": false + "graphml": { + "id": "enumerate", + "unknown": false + } } } \ No newline at end of file diff --git a/conf/svcomp22-intervals-novareq-affeq-native.json b/conf/svcomp22-intervals-novareq-affeq-native.json index 3ae1b19788..47b5cbbd8f 100644 --- a/conf/svcomp22-intervals-novareq-affeq-native.json +++ b/conf/svcomp22-intervals-novareq-affeq-native.json @@ -65,7 +65,9 @@ } }, "witness": { - "id": "enumerate", - "unknown": false + "graphml": { + "id": "enumerate", + "unknown": false + } } } diff --git a/conf/svcomp22-intervals-novareq-octagon-apron.json b/conf/svcomp22-intervals-novareq-octagon-apron.json index 3bf149800e..c6c7144cf6 100644 --- a/conf/svcomp22-intervals-novareq-octagon-apron.json +++ b/conf/svcomp22-intervals-novareq-octagon-apron.json @@ -68,7 +68,9 @@ } }, "witness": { - "id": "enumerate", - "unknown": false + "graphml": { + "id": "enumerate", + "unknown": false + } } } diff --git a/conf/svcomp22-intervals-novareq-polyhedra-apron.json b/conf/svcomp22-intervals-novareq-polyhedra-apron.json index e4e513415a..e636b6fcdf 100644 --- a/conf/svcomp22-intervals-novareq-polyhedra-apron.json +++ b/conf/svcomp22-intervals-novareq-polyhedra-apron.json @@ -68,7 +68,9 @@ } }, "witness": { - "id": "enumerate", - "unknown": false + "graphml": { + "id": "enumerate", + "unknown": false + } } } diff --git a/conf/svcomp22.json b/conf/svcomp22.json index 85ea693375..09113a38c9 100644 --- a/conf/svcomp22.json +++ b/conf/svcomp22.json @@ -67,7 +67,9 @@ } }, "witness": { - "id": "enumerate", - "unknown": false + "graphml": { + "id": "enumerate", + "unknown": false + } } } diff --git a/conf/svcomp23.json b/conf/svcomp23.json index 56474fbe2b..6f404060ba 100644 --- a/conf/svcomp23.json +++ b/conf/svcomp23.json @@ -90,7 +90,9 @@ } }, "witness": { - "id": "enumerate", - "unknown": false + "graphml": { + "id": "enumerate", + "unknown": false + } } } diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index 400dde06dc..5f2081e8d6 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -2279,24 +2279,56 @@ "title": "witness", "type": "object", "properties": { - "enabled": { - "title": "witness.enabled", - "description": "Output witness", - "type": "boolean", - "default": true - }, - "path": { - "title": "witness.path", - "description": "Witness output path", - "type": "string", - "default": "witness.graphml" - }, - "id": { - "title": "witness.id", - "description": "Which witness node IDs to use? node/enumerate", - "type": "string", - "enum": ["node", "enumerate"], - "default": "node" + "graphml": { + "title": "witness.graphml", + "type": "object", + "properties": { + "enabled": { + "title": "witness.graphml.enabled", + "description": "Output GraphML witness", + "type": "boolean", + "default": true + }, + "path": { + "title": "witness.graphml.path", + "description": "GraphML witness output path", + "type": "string", + "default": "witness.graphml" + }, + "id": { + "title": "witness.graphml.id", + "description": "Which witness node IDs to use? node/enumerate", + "type": "string", + "enum": ["node", "enumerate"], + "default": "node" + }, + "minimize": { + "title": "witness.graphml.minimize", + "description": "Try to minimize the witness", + "type": "boolean", + "default": false + }, + "uncil": { + "title": "witness.graphml.uncil", + "description": + "Try to undo CIL control flow transformations in witness", + "type": "boolean", + "default": false + }, + "stack": { + "title": "witness.graphml.stack", + "description": "Construct stacktrace-based witness nodes", + "type": "boolean", + "default": true + }, + "unknown": { + "title": "witness.graphml.unknown", + "description": "Output witness for unknown result", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false }, "invariant": { "title": "witness.invariant", @@ -2376,31 +2408,6 @@ }, "additionalProperties": false }, - "minimize": { - "title": "witness.minimize", - "description": "Try to minimize the witness", - "type": "boolean", - "default": false - }, - "uncil": { - "title": "witness.uncil", - "description": - "Try to undo CIL control flow transformations in witness", - "type": "boolean", - "default": false - }, - "stack": { - "title": "witness.stack", - "description": "Construct stacktrace-based witness nodes", - "type": "boolean", - "default": true - }, - "unknown": { - "title": "witness.unknown", - "description": "Output witness for unknown result", - "type": "boolean", - "default": true - }, "yaml": { "title": "witness.yaml", "type": "object", diff --git a/src/framework/control.ml b/src/framework/control.ml index 9baa2dd1ca..fe43deb45f 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -14,7 +14,7 @@ module type S2S = functor (X : Spec) -> Spec (* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *) let spec_module: (module Spec) Lazy.t = lazy ( GobConfig.building_spec := true; - let arg_enabled = (get_bool "ana.sv-comp.enabled" && get_bool "witness.enabled") || get_bool "exp.arg" in + let arg_enabled = (get_bool "ana.sv-comp.enabled" && get_bool "witness.graphml.enabled") || get_bool "exp.arg" in let open Batteries in (* apply functor F on module X if opt is true *) let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in diff --git a/src/witness/myARG.ml b/src/witness/myARG.ml index 62c705f5b1..068aed7a22 100644 --- a/src/witness/myARG.ml +++ b/src/witness/myARG.ml @@ -320,7 +320,7 @@ struct let rec next_opt' n = match n with - | Statement {sid; skind=If (_, _, _, loc, eloc); _} when GobConfig.get_bool "witness.uncil" -> (* TODO: use elocs instead? *) + | Statement {sid; skind=If (_, _, _, loc, eloc); _} when GobConfig.get_bool "witness.graphml.uncil" -> (* TODO: use elocs instead? *) let (e, if_true_next_n, if_false_next_n) = partition_if_next (Arg.next n) in (* avoid infinite recursion with sid <> sid2 in if_nondet_var *) (* TODO: why physical comparison if_false_next_n != n doesn't work? *) @@ -373,7 +373,7 @@ struct Question(e_cond, e_true, e_false, Cilfacade.typeOf e_false) let next_opt' n = match n with - | Statement {skind=If (_, _, _, loc, eloc); _} when GobConfig.get_bool "witness.uncil" -> (* TODO: use eloc instead? *) + | Statement {skind=If (_, _, _, loc, eloc); _} when GobConfig.get_bool "witness.graphml.uncil" -> (* TODO: use eloc instead? *) let (e_cond, if_true_next_n, if_false_next_n) = partition_if_next (Arg.next n) in if Node.location if_true_next_n = loc && Node.location if_false_next_n = loc then match Arg.next if_true_next_n, Arg.next if_false_next_n with diff --git a/src/witness/witness.ml b/src/witness/witness.ml index 9f5a3c1801..2d94f4a18d 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -13,7 +13,7 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult) let module Invariant = WitnessUtil.Invariant (Task) in let module TaskResult = - (val if get_bool "witness.stack" then + (val if get_bool "witness.graphml.stack" then (module StackTaskResult (Task.Cfg) (TaskResult) : WitnessTaskResult) else (module TaskResult) @@ -24,7 +24,7 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult) struct (* type node = N.t type edge = TaskResult.Arg.Edge.t *) - let minwitness = get_bool "witness.minimize" + let minwitness = get_bool "witness.graphml.minimize" let is_interesting_real from_node edge to_node = (* TODO: don't duplicate this logic with write_node, write_edge *) (* startlines aren't currently interesting because broken, see below *) @@ -58,12 +58,12 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult) let module N = Arg.Node in let module GML = XmlGraphMlWriter in let module GML = - (val match get_string "witness.id" with + (val match get_string "witness.graphml.id" with | "node" -> (module ArgNodeGraphMlWriter (N) (GML) : GraphMlWriter with type node = N.t) | "enumerate" -> (module EnumerateNodeGraphMlWriter (N) (GML)) - | _ -> failwith "witness.id: illegal value" + | _ -> failwith "witness.graphml.id: illegal value" ) in let module GML = DeDupGraphMlWriter (N) (GML) in @@ -305,7 +305,7 @@ struct let determine_result entrystates (module Task:Task): (module WitnessTaskResult) = let module Arg: BiArgInvariant = - (val if GobConfig.get_bool "witness.enabled" then ( + (val if GobConfig.get_bool "witness.graphml.enabled" then ( let module Arg = (val ArgTool.create entrystates) in let module Arg = struct @@ -576,8 +576,8 @@ struct print_task_result (module TaskResult); - if get_bool "witness.enabled" && (TaskResult.result <> Result.Unknown || get_bool "witness.unknown") then ( - let witness_path = get_string "witness.path" in + if get_bool "witness.graphml.enabled" && (TaskResult.result <> Result.Unknown || get_bool "witness.graphml.unknown") then ( + let witness_path = get_string "witness.graphml.path" in Timing.wrap "write" (write_file witness_path (module Task)) (module TaskResult) ) diff --git a/sv-comp/sv-comp-run-no-overflow.py b/sv-comp/sv-comp-run-no-overflow.py index a3461b1a64..88ee2c0e53 100755 --- a/sv-comp/sv-comp-run-no-overflow.py +++ b/sv-comp/sv-comp-run-no-overflow.py @@ -13,7 +13,7 @@ OVERVIEW = False # with True Goblint isn't executed # TODO: don't hard-code specification -GOBLINT_COMMAND = "./goblint --conf conf/svcomp21.json --set ana.specification ./tests/sv-comp/no-overflow.prp --set witness.path {witness_filename} {code_filename} -v" +GOBLINT_COMMAND = "./goblint --conf conf/svcomp21.json --set ana.specification ./tests/sv-comp/no-overflow.prp --set witness.graphml.path {witness_filename} {code_filename} -v" TIMEOUT = 10 # with some int that's Goblint timeout for single execution START = 1 EXIT_ON_ERROR = True diff --git a/sv-comp/sv-comp-run.py b/sv-comp/sv-comp-run.py index af7cada051..977aa69ab6 100755 --- a/sv-comp/sv-comp-run.py +++ b/sv-comp/sv-comp-run.py @@ -13,7 +13,7 @@ OVERVIEW = False # with True Goblint isn't executed # TODO: don't hard-code specification -GOBLINT_COMMAND = "./goblint --conf conf/svcomp21.json --set ana.specification ./tests/sv-comp/unreach-call-__VERIFIER_error.prp --set witness.path {witness_filename} {code_filename}" +GOBLINT_COMMAND = "./goblint --conf conf/svcomp21.json --set ana.specification ./tests/sv-comp/unreach-call-__VERIFIER_error.prp --set witness.graphml.path {witness_filename} {code_filename}" TIMEOUT = 30 # with some int that's Goblint timeout for single execution START = 1 EXIT_ON_ERROR = True diff --git a/tests/sv-comp/observer/path_nofun_true-unreach-call.c b/tests/sv-comp/observer/path_nofun_true-unreach-call.c index 0cb70d23e9..cf1191e9fd 100644 --- a/tests/sv-comp/observer/path_nofun_true-unreach-call.c +++ b/tests/sv-comp/observer/path_nofun_true-unreach-call.c @@ -21,4 +21,4 @@ int main() return 0; } -// ./goblint --enable ana.sv-comp --enable ana.wp --enable witness.uncil --disable ana.int.def_exc --enable ana.int.interval --set ana.activated '["base"]' --html tests/sv-comp/observer/path_nofun_true-unreach-call.c +// ./goblint --enable ana.sv-comp --enable ana.wp --enable witness.graphml.uncil --disable ana.int.def_exc --enable ana.int.interval --set ana.activated '["base"]' --html tests/sv-comp/observer/path_nofun_true-unreach-call.c From 8399258dc31e0f12bbeea04be749f730bac080e0 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 30 Oct 2023 17:01:12 +0200 Subject: [PATCH 2/5] Disable witness.graphml.enabled by default --- conf/ldv-races.json | 1 + conf/svcomp.json | 1 + conf/svcomp21.json | 1 + conf/svcomp22-intervals-novareq-affeq-apron.json | 1 + conf/svcomp22-intervals-novareq-affeq-native.json | 1 + conf/svcomp22-intervals-novareq-octagon-apron.json | 1 + conf/svcomp22-intervals-novareq-polyhedra-apron.json | 1 + conf/svcomp22.json | 1 + conf/svcomp23.json | 1 + src/common/util/options.schema.json | 2 +- 10 files changed, 10 insertions(+), 1 deletion(-) diff --git a/conf/ldv-races.json b/conf/ldv-races.json index 2840bb368c..8db800d74c 100644 --- a/conf/ldv-races.json +++ b/conf/ldv-races.json @@ -54,6 +54,7 @@ }, "witness": { "graphml": { + "enabled": true, "id": "enumerate", "unknown": false } diff --git a/conf/svcomp.json b/conf/svcomp.json index 87fef277c3..2c310c076d 100644 --- a/conf/svcomp.json +++ b/conf/svcomp.json @@ -91,6 +91,7 @@ }, "witness": { "graphml": { + "enabled": true, "id": "enumerate", "unknown": false } diff --git a/conf/svcomp21.json b/conf/svcomp21.json index eda5cdfb88..2e36e61d0c 100644 --- a/conf/svcomp21.json +++ b/conf/svcomp21.json @@ -65,6 +65,7 @@ }, "witness": { "graphml": { + "enabled": true, "id": "enumerate" } } diff --git a/conf/svcomp22-intervals-novareq-affeq-apron.json b/conf/svcomp22-intervals-novareq-affeq-apron.json index 1dafe0a76d..f7f7662b6a 100644 --- a/conf/svcomp22-intervals-novareq-affeq-apron.json +++ b/conf/svcomp22-intervals-novareq-affeq-apron.json @@ -69,6 +69,7 @@ }, "witness": { "graphml": { + "enabled": true, "id": "enumerate", "unknown": false } diff --git a/conf/svcomp22-intervals-novareq-affeq-native.json b/conf/svcomp22-intervals-novareq-affeq-native.json index 47b5cbbd8f..00db00f30f 100644 --- a/conf/svcomp22-intervals-novareq-affeq-native.json +++ b/conf/svcomp22-intervals-novareq-affeq-native.json @@ -66,6 +66,7 @@ }, "witness": { "graphml": { + "enabled": true, "id": "enumerate", "unknown": false } diff --git a/conf/svcomp22-intervals-novareq-octagon-apron.json b/conf/svcomp22-intervals-novareq-octagon-apron.json index c6c7144cf6..a0c09e8937 100644 --- a/conf/svcomp22-intervals-novareq-octagon-apron.json +++ b/conf/svcomp22-intervals-novareq-octagon-apron.json @@ -69,6 +69,7 @@ }, "witness": { "graphml": { + "enabled": true, "id": "enumerate", "unknown": false } diff --git a/conf/svcomp22-intervals-novareq-polyhedra-apron.json b/conf/svcomp22-intervals-novareq-polyhedra-apron.json index e636b6fcdf..3a478bf687 100644 --- a/conf/svcomp22-intervals-novareq-polyhedra-apron.json +++ b/conf/svcomp22-intervals-novareq-polyhedra-apron.json @@ -69,6 +69,7 @@ }, "witness": { "graphml": { + "enabled": true, "id": "enumerate", "unknown": false } diff --git a/conf/svcomp22.json b/conf/svcomp22.json index 09113a38c9..316c3c5534 100644 --- a/conf/svcomp22.json +++ b/conf/svcomp22.json @@ -68,6 +68,7 @@ }, "witness": { "graphml": { + "enabled": true, "id": "enumerate", "unknown": false } diff --git a/conf/svcomp23.json b/conf/svcomp23.json index 6f404060ba..af584f1593 100644 --- a/conf/svcomp23.json +++ b/conf/svcomp23.json @@ -91,6 +91,7 @@ }, "witness": { "graphml": { + "enabled": true, "id": "enumerate", "unknown": false } diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index 5f2081e8d6..8255be2b48 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -2287,7 +2287,7 @@ "title": "witness.graphml.enabled", "description": "Output GraphML witness", "type": "boolean", - "default": true + "default": false }, "path": { "title": "witness.graphml.path", From 783442572bdc03837dd1378c71994e4f53bae360 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 30 Oct 2023 17:27:09 +0200 Subject: [PATCH 3/5] Forbid witness.graphml.enabled outside of SV-COMP mode --- src/framework/control.ml | 2 +- src/maingoblint.ml | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/framework/control.ml b/src/framework/control.ml index fe43deb45f..948dce6075 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -14,7 +14,7 @@ module type S2S = functor (X : Spec) -> Spec (* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *) let spec_module: (module Spec) Lazy.t = lazy ( GobConfig.building_spec := true; - let arg_enabled = (get_bool "ana.sv-comp.enabled" && get_bool "witness.graphml.enabled") || get_bool "exp.arg" in + let arg_enabled = get_bool "witness.graphml.enabled" || get_bool "exp.arg" in let open Batteries in (* apply functor F on module X if opt is true *) let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in diff --git a/src/maingoblint.ml b/src/maingoblint.ml index b5998df2d1..6c55f43ba1 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -160,7 +160,8 @@ let check_arguments () = ^ String.concat " and " @@ List.map (fun s -> "'" ^ s ^ "'") imprecise_options) ); if get_bool "solvers.td3.space" && get_bool "solvers.td3.remove-wpoint" then fail "solvers.td3.space is incompatible with solvers.td3.remove-wpoint"; - if get_bool "solvers.td3.space" && get_string "solvers.td3.side_widen" = "sides-local" then fail "solvers.td3.space is incompatible with solvers.td3.side_widen = 'sides-local'" + if get_bool "solvers.td3.space" && get_string "solvers.td3.side_widen" = "sides-local" then fail "solvers.td3.space is incompatible with solvers.td3.side_widen = 'sides-local'"; + if not (get_bool "ana.sv-comp.enabled") && get_bool "witness.graphml.enabled" then fail "witness.graphml.enabled: cannot generate GraphML witness without SV-COMP mode (ana.sv-comp.enabled)" (** Initialize some globals in other modules. *) let handle_flags () = From e01caccff051316ecb3ff26ba176656f06a9fb76 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 30 Oct 2023 17:31:30 +0200 Subject: [PATCH 4/5] Disable witness.invariant.accessed by default Makes access analysis more expensive --- src/common/util/options.schema.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index 8255be2b48..188e5a77e8 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -2365,7 +2365,7 @@ "title": "witness.invariant.accessed", "description": "Only emit invariants for locally accessed variables", "type": "boolean", - "default": true + "default": false }, "full": { "title": "witness.invariant.full", From 6cd62e5163aaaa5deb6ac046d6ab7995e358d1a1 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 30 Oct 2023 17:39:48 +0200 Subject: [PATCH 5/5] Update witness timings --- src/witness/witness.ml | 7 ++----- src/witness/yamlWitness.ml | 3 +++ 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/witness/witness.ml b/src/witness/witness.ml index 2d94f4a18d..af2e1c03ec 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -572,13 +572,13 @@ struct let write entrystates = let module Task = (val (BatOption.get !task)) in - let module TaskResult = (val (Timing.wrap "determine" (determine_result entrystates) (module Task))) in + let module TaskResult = (val (Timing.wrap "sv-comp result" (determine_result entrystates) (module Task))) in print_task_result (module TaskResult); if get_bool "witness.graphml.enabled" && (TaskResult.result <> Result.Unknown || get_bool "witness.graphml.unknown") then ( let witness_path = get_string "witness.graphml.path" in - Timing.wrap "write" (write_file witness_path (module Task)) (module TaskResult) + Timing.wrap "graphml witness" (write_file witness_path (module Task)) (module TaskResult) ) let write entrystates = @@ -595,7 +595,4 @@ struct ) else write entrystates - - let write entrystates = - Timing.wrap "witness" write entrystates end diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 72ff21f6bd..9e8ebeff51 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -392,6 +392,9 @@ struct ]; yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path")) + + let write () = + Timing.wrap "yaml witness" write () end