diff --git a/conf/bench-yaml-validate.json b/conf/bench-yaml-validate.json
index 46f76fb2ce..ca830be08a 100644
--- a/conf/bench-yaml-validate.json
+++ b/conf/bench-yaml-validate.json
@@ -1,24 +1,31 @@
{
"ana": {
+ "sv-comp": {
+ "functions": true
+ },
"int": {
"def_exc": true,
"enums": false,
"interval": true
},
"activated": [
- "expRelation",
"base",
"threadid",
"threadflag",
"threadreturn",
- "escape",
+ "mallocWrapper",
"mutexEvents",
"mutex",
"access",
"race",
- "mallocWrapper",
+ "escape",
+ "expRelation",
"mhp",
"assert",
+ "var_eq",
+ "symb_locks",
+ "thread",
+ "threadJoins",
"unassume"
],
"malloc": {
@@ -65,6 +72,9 @@
},
"int": {
"signed_overflow": "assume_none"
+ },
+ "null-pointer": {
+ "dereference": "assume_none"
}
},
"pre": {
diff --git a/conf/bench-yaml.json b/conf/bench-yaml.json
index 734ac235be..a24035fc9b 100644
--- a/conf/bench-yaml.json
+++ b/conf/bench-yaml.json
@@ -1,24 +1,31 @@
{
"ana": {
+ "sv-comp": {
+ "functions": true
+ },
"int": {
"def_exc": true,
"enums": false,
"interval": true
},
"activated": [
- "expRelation",
"base",
"threadid",
"threadflag",
"threadreturn",
- "escape",
+ "mallocWrapper",
"mutexEvents",
"mutex",
"access",
"race",
- "mallocWrapper",
+ "escape",
+ "expRelation",
"mhp",
- "assert"
+ "assert",
+ "var_eq",
+ "symb_locks",
+ "thread",
+ "threadJoins"
],
"malloc": {
"wrappers": [
@@ -67,6 +74,9 @@
},
"int": {
"signed_overflow": "assume_none"
+ },
+ "null-pointer": {
+ "dereference": "assume_none"
}
},
"pre": {
diff --git a/conf/svcomp-yaml-validate.json b/conf/svcomp-yaml-validate.json
index ad635c787e..05bb1ebcc2 100644
--- a/conf/svcomp-yaml-validate.json
+++ b/conf/svcomp-yaml-validate.json
@@ -68,6 +68,9 @@
"tokens": true
}
},
+ "pre": {
+ "transform-paths": false
+ },
"exp": {
"region-offsets": true
},
diff --git a/conf/svcomp-yaml.json b/conf/svcomp-yaml.json
index 28483e8059..6e3d0e4767 100644
--- a/conf/svcomp-yaml.json
+++ b/conf/svcomp-yaml.json
@@ -64,6 +64,9 @@
"enabled": false
}
},
+ "pre": {
+ "transform-paths": false
+ },
"exp": {
"region-offsets": true
},
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index a328e8fac8..a932ef015a 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -45,7 +45,7 @@ struct
module V =
struct
- include Printable.Either (Priv.V) (ThreadIdDomain.Thread)
+ include Printable.Either (struct include Priv.V let name () = "priv" end) (struct include ThreadIdDomain.Thread let name () = "threadreturn" end)
let priv x = `Left x
let thread x = `Right x
include StdV
@@ -1606,6 +1606,8 @@ struct
let id_meet_down ~old ~c = ID.meet old c
let fd_meet_down ~old ~c = FD.meet old c
+
+ let contra _ = raise Deadcode
end
module Invariant = BaseInvariant.Make (InvariantEval)
@@ -2453,6 +2455,8 @@ struct
(* don't meet with current octx values when propagating inverse operands down *)
let id_meet_down ~old ~c = c
let fd_meet_down ~old ~c = c
+
+ let contra st = st
end
in
let module Unassume = BaseInvariant.Make (UnassumeEval) in
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index f31a578aec..705a05bc03 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -29,6 +29,12 @@ sig
val id_meet_down: old:ID.t -> c:ID.t -> ID.t
val fd_meet_down: old:FD.t -> c:FD.t -> FD.t
+
+ (** Handle contradiction.
+
+ Normal branch refinement just raises {!Analyses.Deadcode}.
+ Unassume leaves unchanged. *)
+ val contra: D.t -> D.t
end
module Make (Eval: Eval) =
@@ -81,7 +87,7 @@ struct
(* make that address meet the invariant, i.e exclusion sets will be joined *)
if is_some_bot new_val then (
if M.tracing then M.tracel "branch" "C The branch %B is dead!\n" tv;
- raise Analyses.Deadcode
+ contra st
)
else if VD.is_bot new_val
then set a gs st addr t_lval value ~ctx (* no *_raw because this is not a real assignment *)
@@ -97,7 +103,7 @@ struct
let offs = convert_offset a gs st o in
let newv = VD.update_offset a oldv offs c' (Some exp) x (var.vtype) in
let v = VD.meet oldv newv in
- if is_some_bot v then raise Analyses.Deadcode
+ if is_some_bot v then contra st
else (
if M.tracing then M.tracel "inv" "improve variable %a from %a to %a (c = %a, c' = %a)\n" d_varinfo var VD.pretty oldv VD.pretty v pretty c VD.pretty c';
let r = set' (Var var,NoOffset) v st in
@@ -110,7 +116,7 @@ struct
let oldv = eval_rv_lval_refine a gs st exp x in
let oldv = map_oldval oldv (Cilfacade.typeOfLval x) in
let v = VD.meet oldv c' in
- if is_some_bot v then raise Analyses.Deadcode
+ if is_some_bot v then contra st
else (
if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)\n" d_lval x VD.pretty oldv VD.pretty v pretty c VD.pretty c';
set' x v st
@@ -339,11 +345,10 @@ struct
in
a, b
| Eq | Ne as op ->
- let both x = x, x in
- let m = ID.meet a b in
begin match op, ID.to_bool c with
| Eq, Some true
- | Ne, Some false -> both m (* def. equal: if they compare equal, both values must be from the meet *)
+ | Ne, Some false -> (* def. equal: if they compare equal, both values must be from the meet *)
+ (id_meet_down ~old:a ~c:b, id_meet_down ~old:b ~c:a)
| Eq, Some false
| Ne, Some true -> (* def. unequal *)
(* Both values can not be in the meet together, but it's not sound to exclude the meet from both.
@@ -544,7 +549,7 @@ struct
let eval_bool e st = match eval e st with `Int i -> ID.to_bool i | _ -> None in
let rec inv_exp c_typed exp (st:D.t): D.t =
(* trying to improve variables in an expression so it is bottom means dead code *)
- if VD.is_bot_value c_typed then raise Analyses.Deadcode;
+ if VD.is_bot_value c_typed then contra st else
match exp, c_typed with
| UnOp (LNot, e, _), `Int c ->
let ikind = Cilfacade.get_ikind_exp e in
@@ -633,7 +638,17 @@ struct
in
begin match eqs_st with
| Some st -> st
- | None -> st (* TODO: not bothering to fall back, no other case can refine LOr anyway *)
+ | None when ID.to_bool c = Some true ->
+ begin match inv_exp (`Int c) arg1 st with
+ | st1 ->
+ begin match inv_exp (`Int c) arg2 st with
+ | st2 -> D.join st1 st2
+ | exception Analyses.Deadcode -> st1
+ end
+ | exception Analyses.Deadcode -> inv_exp (`Int c) arg2 st (* Deadcode falls through *)
+ end
+ | None ->
+ st (* TODO: not bothering to fall back, no other case can refine LOr anyway *)
end
| (BinOp (op, e1, e2, _) as e, `Float _)
| (BinOp (op, e1, e2, _) as e, `Int _) ->
@@ -720,7 +735,7 @@ struct
| v -> fallback ("CastE: e did not evaluate to `Int, but " ^ sprint VD.pretty v) st)
| e, _ -> fallback (sprint d_plainexp e ^ " not implemented") st
in
- if eval_bool exp st = Some (not tv) then raise Analyses.Deadcode (* we already know that the branch is dead *)
+ if eval_bool exp st = Some (not tv) then contra st (* we already know that the branch is dead *)
else
(* C11 6.5.13, 6.5.14, 6.5.3.3: LAnd, LOr and LNot also return 0 or 1 *)
let is_cmp = function
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 670e89f16a..982c9565cf 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -85,6 +85,7 @@ struct
struct
(* TODO: Either3? *)
include Printable.Either (Printable.Either (VMutex) (VMutexInits)) (VGlobal)
+ let name () = "MutexGlobals"
let mutex x: t = `Left (`Left x)
let mutex_inits: t = `Left (`Right ())
let global x: t = `Right x
diff --git a/src/analyses/mCPRegistry.ml b/src/analyses/mCPRegistry.ml
index 620fbc8c79..30bd1eed69 100644
--- a/src/analyses/mCPRegistry.ml
+++ b/src/analyses/mCPRegistry.ml
@@ -197,7 +197,8 @@ struct
f n (assoc_dom n) d
let pretty () = unop_map (fun n (module S: Printable.S) x ->
- Pretty.dprintf "%s:%a" (S.name ()) S.pretty (obj x)
+ let analysis_name = find_spec_name n in
+ Pretty.dprintf "%s:%a" analysis_name S.pretty (obj x)
)
let show = unop_map (fun n (module S: Printable.S) x ->
@@ -257,6 +258,7 @@ struct
open Obj
include DomVariantPrintable (PrintableOfSysVarSpec (DLSpec))
+ let name () = "MCP.V"
let unop_map f ((n, d):t) =
f n (assoc_dom n) d
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 83590ac16a..08d3363a4b 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -25,7 +25,7 @@ struct
module V =
struct
- include Printable.Either (CilType.Varinfo) (ValueDomain.Addr)
+ include Printable.Either (struct include CilType.Varinfo let name () = "protecting" end) (struct include ValueDomain.Addr let name () = "protected" end)
let name () = "mutex"
let protecting x = `Left x
let protected x = `Right x
diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
index 7df56023ab..4729258295 100644
--- a/src/analyses/unassumeAnalysis.ml
+++ b/src/analyses/unassumeAnalysis.ml
@@ -55,7 +55,8 @@ struct
let rec iter_node node =
if not (NH.mem reachable node) then begin
NH.replace reachable node ();
- (* TODO: filter synthetic like in Validator *)
+ (* TODO: filter synthetic?
+ See YamlWitness. *)
if WitnessInvariant.is_invariant_node node then
Locator.add locator (Node.location node) node;
if WitnessUtil.NH.mem WitnessInvariant.loop_heads node then
@@ -229,7 +230,7 @@ struct
match es with
| x :: xs ->
let e = List.fold_left (fun a {exp = b; _} -> Cil.(BinOp (LAnd, a, b, intType))) x.exp xs in
- (* M.info ~category:Witness "unassume invariant: %a" CilType.Exp.pretty e; *)
+ M.info ~category:Witness "unassume invariant: %a" CilType.Exp.pretty e;
if not !Goblintutil.postsolving then (
if not (GobConfig.get_bool "ana.unassume.precheck" && Queries.ID.to_bool (ctx.ask (EvalInt e)) = Some false) then (
let uuids = x.uuid :: List.map (fun {uuid; _} -> uuid) xs in
diff --git a/src/domains/printable.ml b/src/domains/printable.ml
index c67c3c94a6..f708d58c51 100644
--- a/src/domains/printable.ml
+++ b/src/domains/printable.ml
@@ -255,13 +255,13 @@ struct
let pretty () (state:t) =
match state with
- | `Left n -> Base1.pretty () n
- | `Right n -> Base2.pretty () n
+ | `Left n -> Pretty.dprintf "%s:%a" (Base1.name ()) Base1.pretty n
+ | `Right n -> Pretty.dprintf "%s:%a" (Base2.name ()) Base2.pretty n
let show state =
match state with
- | `Left n -> Base1.show n
- | `Right n -> Base2.show n
+ | `Left n -> (Base1.name ()) ^ ":" ^ Base1.show n
+ | `Right n -> (Base2.name ()) ^ ":" ^ Base2.show n
let name () = "either " ^ Base1.name () ^ " or " ^ Base2.name ()
let printXml f = function
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index abe4f72804..31398f71fd 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -450,8 +450,8 @@ struct
| `G x -> `G (GV.relift x)
let pretty_trace () = function
- | `L a -> LV.pretty_trace () a
- | `G a -> GV.pretty_trace () a
+ | `L a -> Pretty.dprintf "L:%a" LV.pretty_trace a
+ | `G a -> Pretty.dprintf "G:%a" GV.pretty_trace a
let printXml f = function
| `L a -> LV.printXml f a
@@ -1211,6 +1211,7 @@ struct
module V =
struct
include Printable.Either (S.V) (Node)
+ let name () = "DeadBranch"
let s x = `Left x
let node x = `Right x
let is_write_only = function
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 89b80bc52d..fca8438c21 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -385,9 +385,14 @@ let parse_preprocessed preprocessed =
(path_str, system_header) (* ignore special "paths" *)
| _ ->
let path = Fpath.v path_str in
- let dir = (Option.get task_opt).ProcessPool.cwd |? goblint_cwd in (* relative to compilation database directory or goblint's cwd *)
- let path' = Fpath.normalize @@ Fpath.append dir path in
- let path' = Fpath.rem_prefix goblint_cwd path' |? path' in (* remove goblint cwd prefix (if has one) for readability *)
+ let path' = if get_bool "pre.transform-paths" then (
+ let dir = (Option.get task_opt).ProcessPool.cwd |? goblint_cwd in (* relative to compilation database directory or goblint's cwd *)
+ let path' = Fpath.normalize @@ Fpath.append dir path in
+ Fpath.rem_prefix goblint_cwd path' |? path' (* remove goblint cwd prefix (if has one) for readability *)
+ )
+ else
+ path
+ in
Preprocessor.FpathH.modify_def Fpath.Map.empty preprocessed_file (Fpath.Map.add path' system_header) Preprocessor.dependencies; (* record dependency *)
(Fpath.to_string path', system_header)
in
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index f32115c926..730b1f3f12 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -311,7 +311,7 @@ module Base =
if not wp then tmp
else
if term then
- match phase with Widen -> S.Dom.widen old (S.Dom.join old tmp) | Narrow -> S.Dom.narrow old tmp
+ match phase with Widen -> S.Dom.widen old (S.Dom.join old tmp) | Narrow when GobConfig.get_bool "exp.no-narrow" -> old (* no narrow *) | Narrow -> S.Dom.narrow old tmp
else
box old tmp
in
@@ -415,6 +415,7 @@ module Base =
if tracing then trace "sol2" "stable add %a\n" S.Var.pretty_trace y;
HM.replace stable y ();
if not (S.Dom.leq tmp old) then (
+ if tracing && not (S.Dom.is_bot old) then trace "solside" "side to %a (wpx: %b) from %a\n" S.Var.pretty_trace y (HM.mem wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x;
let sided = match x with
| Some x ->
let sided = VS.mem x old_sides in
diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml
index c3553431ac..c3a6387328 100644
--- a/src/util/gobConfig.ml
+++ b/src/util/gobConfig.ml
@@ -387,7 +387,7 @@ struct
(** Merge configurations form a file with current. *)
let merge_file fn =
let cwd = Fpath.v (Sys.getcwd ()) in
- let config_dirs = cwd :: Goblint_sites.conf in
+ let config_dirs = cwd :: Fpath.(parent (v Sys.executable_name)) :: Goblint_sites.conf in
let file = List.find_map_opt (fun custom_include_dir ->
let path = Fpath.append custom_include_dir fn in
if Sys.file_exists (Fpath.to_string path) then
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index c3346677d6..667a757b2f 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -242,6 +242,12 @@
}
},
"additionalProperties": false
+ },
+ "transform-paths": {
+ "title": "pre.transform-paths",
+ "description": "Normalize and relativize paths in parsed CIL locations. Can cause issues locating YAML witness invariants due to differing paths.",
+ "type": "boolean",
+ "default": true
}
},
"additionalProperties": false
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 3f5354d488..ddea3d652b 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -16,7 +16,7 @@ struct
let producer: Producer.t = {
name = "Goblint";
version = Version.goblint;
- command_line = Goblintutil.command_line;
+ command_line = Some Goblintutil.command_line;
}
let metadata ?task (): Metadata.t =
@@ -447,7 +447,12 @@ struct
let loop_locator = Locator.create () in
LHT.iter (fun ((n, _) as lvar) _ ->
let loc = Node.location n in
- if not loc.synthetic then
+ (* TODO: filter synthetic?
+
+ Almost all loops are transformed by CIL, so the loop constructs all get synthetic locations. Filtering them from the locator could give some odd behavior: if the location is right before the loop and all the synthetic loop head stuff is filtered, then the first non-synthetic node is already inside the loop, not outside where the location actually was.
+ Similarly, if synthetic locations are then filtered, witness.invariant.loop-head becomes essentially useless.
+ I guess at some point during testing and benchmarking I achieved better results with the filtering removed. *)
+ if WitnessInvariant.is_invariant_node n then
Locator.add locator loc lvar;
if WitnessUtil.NH.mem WitnessInvariant.loop_heads n then
Locator.add loop_locator loc lvar
diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml
index aad206d0fc..ae30828a55 100644
--- a/src/witness/yamlWitnessType.ml
+++ b/src/witness/yamlWitnessType.ml
@@ -4,22 +4,27 @@ struct
name: string;
version: string;
(* TODO: configuration *)
- command_line: string;
+ command_line: string option;
(* TODO: description *)
}
let to_yaml {name; version; command_line} =
- `O [
- ("name", `String name);
- ("version", `String version);
- ("command_line", `String command_line);
- ]
+ `O ([
+ ("name", `String name);
+ ("version", `String version);
+ ] @ match command_line with
+ | Some command_line -> [
+ ("command_line", `String command_line);
+ ]
+ | None ->
+ []
+ )
let of_yaml y =
let open GobYaml in
let+ name = y |> find "name" >>= to_string
and+ version = y |> find "version" >>= to_string
- and+ command_line = y |> find "command_line" >>= to_string in
+ and+ command_line = y |> Yaml.Util.find "command_line" >>= option_map to_string in
{name; version; command_line}
end
diff --git a/sv-comp/my-bench-sv-comp/yaml/goblint-bench-validate.xml b/sv-comp/my-bench-sv-comp/yaml/goblint-bench-validate.xml
deleted file mode 100644
index dfb24a2ae3..0000000000
--- a/sv-comp/my-bench-sv-comp/yaml/goblint-bench-validate.xml
+++ /dev/null
@@ -1,31 +0,0 @@
-
-
-
-
-
-
-
-
-
-
- evals = (\d+)
-
-
-
-
-
-
-
-
-
-
-
-
- RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.yml
-
-
-
- /mnt/goblint-svcomp/goblint-bench/bench/Pthread.set
-
-
-
diff --git a/sv-comp/my-bench-sv-comp/yaml/goblint-bench.sh b/sv-comp/my-bench-sv-comp/yaml/goblint-bench.sh
deleted file mode 100755
index ca37845ced..0000000000
--- a/sv-comp/my-bench-sv-comp/yaml/goblint-bench.sh
+++ /dev/null
@@ -1,42 +0,0 @@
-#!/bin/bash
-
-shopt -s extglob
-
-MYBENCHDIR=/mnt/goblint-svcomp/benchexec/my-bench-sv-comp/yaml
-RESULTSDIR=/mnt/goblint-svcomp/benchexec/results/yaml-xy-bench
-GOBLINTPARALLEL=14
-VALIDATEPARALLEL=14
-
-mkdir $RESULTSDIR
-
-# Run verification
-cd /mnt/goblint-svcomp/sv-comp/goblint
-# read-only and overlay dirs for Value too large for defined data type workaround
-benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $GOBLINTPARALLEL $MYBENCHDIR/goblint-bench.xml
-
-# Extract witness directory
-cd $RESULTSDIR
-LOGDIR=`echo goblint-bench.*.files`
-echo $LOGDIR
-
-# Construct validation XMLs
-cd $MYBENCHDIR
-sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" goblint-bench-validate.xml > goblint-bench-validate-tmp.xml
-
-# Run validation
-cd /mnt/goblint-svcomp/sv-comp/goblint
-benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/goblint-bench-validate-tmp.xml
-
-# Merge witness validation results
-cd $RESULTSDIR
-# python3 /mnt/goblint-svcomp/benchexec/benchexec/contrib/mergeBenchmarkSets.py -o . goblint.*.results.*.xml.bz2 goblint-validate-tmp.*.results.*.xml.bz2
-python3 /mnt/goblint-svcomp/benchexec/benchexec/contrib/mergeBenchmarkSets.py -o . goblint-bench.*.results.all.Pthread.xml.bz2 goblint-bench-validate-tmp.*.results.all.Pthread.xml.bz2
-python3 /mnt/goblint-svcomp/benchexec/benchexec/contrib/mergeBenchmarkSets.py -o . goblint-bench.*.results.loop-head.Pthread.xml.bz2 goblint-bench-validate-tmp.*.results.loop-head.Pthread.xml.bz2
-
-# Generate table with merged results and witness validation results
-sed -e "s/LOGDIR/$LOGDIR/" $MYBENCHDIR/table-generator-bench.xml > table-generator.xml
-table-generator -x table-generator.xml
-
-# Decompress all tool outputs for table HTML links
-unzip -o goblint-bench.*.logfiles.zip
-unzip -o goblint-bench-validate-tmp.*.logfiles.zip
diff --git a/sv-comp/my-bench-sv-comp/yaml/goblint-bench.xml b/sv-comp/my-bench-sv-comp/yaml/goblint-bench.xml
deleted file mode 100644
index 547d67b8cd..0000000000
--- a/sv-comp/my-bench-sv-comp/yaml/goblint-bench.xml
+++ /dev/null
@@ -1,28 +0,0 @@
-
-
-
-
- **.yml
-
-
-
-
-
- evals = (\d+)
-
-
-
-
-
-
-
-
-
-
-
-
-
- /mnt/goblint-svcomp/goblint-bench/bench/Pthread.set
-
-
-
diff --git a/sv-comp/my-bench-sv-comp/yaml/goblint-validate.xml b/sv-comp/my-bench-sv-comp/yaml/goblint-validate.xml
deleted file mode 100644
index 5a3cac3065..0000000000
--- a/sv-comp/my-bench-sv-comp/yaml/goblint-validate.xml
+++ /dev/null
@@ -1,42 +0,0 @@
-
-
-
-
-
-
-
-
-
-
- evals = (\d+)
-
-
-
-
-
-
-
-
-
-
-
-
- RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.yml
-
-
-
- /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ReachSafety-Loops-Simple.set
- /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp
-
-
-
-
-
diff --git a/sv-comp/my-bench-sv-comp/yaml/goblint.sh b/sv-comp/my-bench-sv-comp/yaml/goblint.sh
deleted file mode 100755
index ffbfa9f1a2..0000000000
--- a/sv-comp/my-bench-sv-comp/yaml/goblint.sh
+++ /dev/null
@@ -1,42 +0,0 @@
-#!/bin/bash
-
-shopt -s extglob
-
-MYBENCHDIR=/mnt/goblint-svcomp/benchexec/my-bench-sv-comp/yaml
-RESULTSDIR=/mnt/goblint-svcomp/benchexec/results/yaml-xy
-GOBLINTPARALLEL=14
-VALIDATEPARALLEL=14
-
-mkdir $RESULTSDIR
-
-# Run verification
-cd /mnt/goblint-svcomp/sv-comp/goblint
-# read-only and overlay dirs for Value too large for defined data type workaround
-benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $GOBLINTPARALLEL $MYBENCHDIR/goblint.xml
-
-# Extract witness directory
-cd $RESULTSDIR
-LOGDIR=`echo goblint.*.files`
-echo $LOGDIR
-
-# Construct validation XMLs
-cd $MYBENCHDIR
-sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" goblint-validate.xml > goblint-validate-tmp.xml
-
-# Run validation
-cd /mnt/goblint-svcomp/sv-comp/goblint
-benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/goblint-validate-tmp.xml
-
-# Merge witness validation results
-cd $RESULTSDIR
-# python3 /mnt/goblint-svcomp/benchexec/benchexec/contrib/mergeBenchmarkSets.py -o . goblint.*.results.*.xml.bz2 goblint-validate-tmp.*.results.*.xml.bz2
-python3 /mnt/goblint-svcomp/benchexec/benchexec/contrib/mergeBenchmarkSets.py -o . goblint.*.results.all.ReachSafety-Loops-Simple.xml.bz2 goblint-validate-tmp.*.results.all.ReachSafety-Loops-Simple.xml.bz2
-python3 /mnt/goblint-svcomp/benchexec/benchexec/contrib/mergeBenchmarkSets.py -o . goblint.*.results.loop-head.ReachSafety-Loops-Simple.xml.bz2 goblint-validate-tmp.*.results.loop-head.ReachSafety-Loops-Simple.xml.bz2
-
-# Generate table with merged results and witness validation results
-sed -e "s/LOGDIR/$LOGDIR/" $MYBENCHDIR/table-generator.xml > table-generator.xml
-table-generator -x table-generator.xml
-
-# Decompress all tool outputs for table HTML links
-unzip -o goblint.*.logfiles.zip
-unzip -o goblint-validate-tmp.*.logfiles.zip
diff --git a/sv-comp/my-bench-sv-comp/yaml/goblint.xml b/sv-comp/my-bench-sv-comp/yaml/goblint.xml
deleted file mode 100644
index 5ca9a58d06..0000000000
--- a/sv-comp/my-bench-sv-comp/yaml/goblint.xml
+++ /dev/null
@@ -1,39 +0,0 @@
-
-
-
-
- **.yml
-
-
-
-
-
- evals = (\d+)
-
-
-
-
-
-
-
-
-
-
-
-
-
- /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ReachSafety-Loops-Simple.set
- /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp
-
-
-
-
-
diff --git a/sv-comp/my-bench-sv-comp/yaml/table-generator-bench.xml b/sv-comp/my-bench-sv-comp/yaml/table-generator-bench.xml
deleted file mode 100644
index 4bf2676eef..0000000000
--- a/sv-comp/my-bench-sv-comp/yaml/table-generator-bench.xml
+++ /dev/null
@@ -1,55 +0,0 @@
-
-
-