diff --git a/conf/svcomp25.json b/conf/svcomp25.json index b9f447ffea..d476760a05 100644 --- a/conf/svcomp25.json +++ b/conf/svcomp25.json @@ -111,4 +111,4 @@ "pre": { "enabled": false } -} +} \ No newline at end of file diff --git a/src/arg/argTools.ml b/src/arg/argTools.ml index a220120912..04c9a80e46 100644 --- a/src/arg/argTools.ml +++ b/src/arg/argTools.ml @@ -137,19 +137,6 @@ struct | Statement stmt -> Printf.sprintf "s%d(%d)[%s]" stmt.sid c_tag i_str | Function f -> Printf.sprintf "ret%d%s(%d)[%s]" f.svar.vid f.svar.vname c_tag i_str | FunctionEntry f -> Printf.sprintf "fun%d%s(%d)[%s]" f.svar.vid f.svar.vname c_tag i_str - - (* TODO: less hacky way (without ask_indices) to move node *) - let is_live (n, c, i) = not (Spec.D.is_bot (get (n, c))) - let move_opt (n, c, i) to_n = - match ask_indices (to_n, c) with - | [] -> None - | [to_i] -> - let to_node = (to_n, c, to_i) in - BatOption.filter is_live (Some to_node) - | _ :: _ :: _ -> - failwith "Node.move_opt: ambiguous moved index" - let equal_node_context (n1, c1, i1) (n2, c2, i2) = - EQSys.LVar.equal (n1, c1) (n2, c2) end module NHT = BatHashtbl.Make (Node) @@ -211,11 +198,17 @@ struct let next = witness_next end in + let module Arg = + (val if GobConfig.get_bool "exp.arg.uncil" then + let open MyARG in + (module Intra (UnCilTernaryIntra (UnCilLogicIntra (CfgIntra (FileCfg.Cfg)))) (Arg): MyARG.S with type Node.t = Arg.Node.t and type Edge.t = Arg.Edge.t) + else + (module Arg) + ) + in let module Arg = struct - open MyARG - module ArgIntra = UnCilTernaryIntra (UnCilLogicIntra (CfgIntra (FileCfg.Cfg))) - include Intra (ArgIntra) (Arg) + include Arg let prev = witness_prev diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml index f92f531f0d..4b54c39179 100644 --- a/src/arg/myARG.ml +++ b/src/arg/myARG.ml @@ -12,14 +12,11 @@ sig val context_id: t -> int val path_id: t -> int val to_string: t -> string - - val move_opt: t -> MyCFG.node -> t option - val equal_node_context: t -> t -> bool end module type Edge = sig - type t + type t [@@deriving eq, ord] val embed: MyCFG.edge -> t val to_string: t -> string @@ -27,7 +24,7 @@ end module CFGEdge: Edge with type t = MyCFG.edge = struct - type t = edge + type t = Edge.t [@@deriving eq, ord] let embed e = e let to_string e = GobPretty.sprint Edge.pretty_plain e @@ -102,7 +99,7 @@ end module InlineEdge: Edge with type t = inline_edge = struct - type t = inline_edge + type t = inline_edge [@@deriving eq, ord] let embed e = CFGEdge e let to_string e = InlineEdgePrintable.show e @@ -130,15 +127,6 @@ struct nl |> List.map Node.to_string |> String.concat "@" - - let move_opt nl to_node = - let open GobOption.Syntax in - match nl with - | [] -> None - | n :: stack -> - let+ to_n = Node.move_opt n to_node in - to_n :: stack - let equal_node_context _ _ = failwith "StackNode: equal_node_context" end module Stack (Arg: S with module Edge = InlineEdge): @@ -265,16 +253,19 @@ struct end end +type cfg_path = (MyCFG.edge * MyCFG.node) list module type SIntra = sig - val next: MyCFG.node -> (MyCFG.edge * MyCFG.node) list + val next: MyCFG.node -> (MyCFG.edge * MyCFG.node * cfg_path list) list + (** @return Also the original CFG paths corresponding to the step. *) end module type SIntraOpt = sig include SIntra - val next_opt: MyCFG.node -> ((MyCFG.edge * MyCFG.node) list) option + val next_opt: MyCFG.node -> ((MyCFG.edge * MyCFG.node * cfg_path list) list) option + (** @return Also the original CFG paths corresponding to the step. *) end module CfgIntra (Cfg:CfgForward): SIntraOpt = @@ -283,51 +274,38 @@ struct let open GobList.Syntax in let* (es, to_n) = Cfg.next node in let+ (_, e) = es in - (e, to_n) + (e, to_n, [[(e, to_n)]]) let next_opt _ = None end -let partition_if_next if_next_n = - (* TODO: refactor, check extra edges for error *) - let test_next b = List.find (function - | (Test (_, b'), _) when b = b' -> true - | (_, _) -> false - ) if_next_n +let cartesian_concat_paths (ps : cfg_path list) (qs : cfg_path list) : cfg_path list = List.concat_map (fun p -> List.map (fun q -> p @ q) qs) ps + +let partition_if_next if_next = + let (if_next_trues, if_next_falses) = List.partition (function + | (Test (_, b), _, _) -> b + | (_, _, _) -> failwith "partition_if_next: not Test edge" + ) if_next in - (* assert (List.length if_next <= 2); *) - match test_next true, test_next false with - | (Test (e_true, true), if_true_next_n), (Test (e_false, false), if_false_next_n) when Basetype.CilExp.equal e_true e_false -> - (e_true, if_true_next_n, if_false_next_n) - | _, _ -> failwith "partition_if_next: bad branches" + match if_next_trues, if_next_falses with + | [(Test (e_true, true), if_true_next_n, if_true_next_ps)], [(Test (e_false, false), if_false_next_n, if_false_next_ps)] when Basetype.CilExp.equal e_true e_false -> + (e_true, (if_true_next_n, if_true_next_ps), (if_false_next_n, if_false_next_ps)) + | _, _ -> + (* This fails due to any of the following: + - Either true or false branch is missing. + - Either true or false branch has multiple different exps or nodes (same exp, branch and node should only occur once by construction/assumption). + - True and false branch have different exps. *) + failwith "partition_if_next: bad branches" module UnCilLogicIntra (Arg: SIntraOpt): SIntraOpt = struct open Cil - (* TODO: questionable (=) and (==) use here *) - - let is_equiv_stmtkind sk1 sk2 = match sk1, sk2 with - | Instr is1, Instr is2 -> GobList.equal (=) is1 is2 - | Return _, Return _ -> sk1 = sk2 - | _, _ -> false (* TODO: also consider others? not sure if they ever get duplicated *) - let is_equiv_stmt s1 s2 = is_equiv_stmtkind s1.skind s2.skind (* TODO: also consider labels *) - let is_equiv_node n1 n2 = match n1, n2 with - | Statement s1, Statement s2 -> is_equiv_stmt s1 s2 - | _, _ -> false (* TODO: also consider FunctionEntry & Function? *) - let is_equiv_edge e1 e2 = match e1, e2 with - | Entry f1, Entry f2 -> f1 == f2 (* physical equality for fundec to avoid cycle *) - | Ret (exp1, f1), Ret (exp2, f2) -> exp1 = exp2 && f1 == f2 (* physical equality for fundec to avoid cycle *) - | _, _ -> e1 = e2 - let rec is_equiv_chain n1 n2 = - Node.equal n1 n2 || (is_equiv_node n1 n2 && is_equiv_chain_next n1 n2) - and is_equiv_chain_next n1 n2 = match Arg.next n1, Arg.next n2 with - | [(e1, to_n1)], [(e2, to_n2)] -> - is_equiv_edge e1 e2 && is_equiv_chain to_n1 to_n2 - | _, _-> false + let () = + assert (not !Cabs2cil.allowDuplication) (* duplication makes it more annoying to detect cilling *) let rec next_opt' n = match n with - | Statement {sid; skind=If _; _} when GobConfig.get_bool "exp.arg.uncil" -> - let (e, if_true_next_n, if_false_next_n) = partition_if_next (Arg.next n) in + | Statement {sid; skind=If _; _} -> + let (e, (if_true_next_n, if_true_next_ps), (if_false_next_n, if_false_next_ps)) = 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? *) (* TODO: need to handle longer loops? *) @@ -336,24 +314,24 @@ struct (* && *) | Statement {sid=sid2; skind=If _; _}, _ when sid <> sid2 && CilType.Location.equal loc (Node.location if_true_next_n) -> (* get e2 from edge because recursive next returns it there *) - let (e2, if_true_next_true_next_n, if_true_next_false_next_n) = partition_if_next (next if_true_next_n) in - if is_equiv_chain if_false_next_n if_true_next_false_next_n then + let (e2, (if_true_next_true_next_n, if_true_next_true_next_ps), (if_true_next_false_next_n, if_true_next_false_next_ps)) = partition_if_next (next if_true_next_n) in + if Node.equal if_false_next_n if_true_next_false_next_n then let exp = BinOp (LAnd, e, e2, intType) in Some [ - (Test (exp, true), if_true_next_true_next_n); - (Test (exp, false), if_false_next_n) + (Test (exp, true), if_true_next_true_next_n, cartesian_concat_paths if_true_next_ps if_true_next_true_next_ps); + (Test (exp, false), if_true_next_false_next_n, if_false_next_ps @ cartesian_concat_paths if_true_next_ps if_true_next_false_next_ps) (* concat two different path families to same false node *) ] else None (* || *) | _, Statement {sid=sid2; skind=If _; _} when sid <> sid2 && CilType.Location.equal loc (Node.location if_false_next_n) -> (* get e2 from edge because recursive next returns it there *) - let (e2, if_false_next_true_next_n, if_false_next_false_next_n) = partition_if_next (next if_false_next_n) in - if is_equiv_chain if_true_next_n if_false_next_true_next_n then + let (e2, (if_false_next_true_next_n, if_false_next_true_next_ps), (if_false_next_false_next_n, if_false_next_false_next_ps)) = partition_if_next (next if_false_next_n) in + if Node.equal if_true_next_n if_false_next_true_next_n then let exp = BinOp (LOr, e, e2, intType) in Some [ - (Test (exp, true), if_true_next_n); - (Test (exp, false), if_false_next_false_next_n) + (Test (exp, true), if_false_next_true_next_n, if_true_next_ps @ cartesian_concat_paths if_false_next_ps if_false_next_true_next_ps); (* concat two different path families to same true node *) + (Test (exp, false), if_false_next_false_next_n, cartesian_concat_paths if_false_next_ps if_false_next_false_next_ps) ] else None @@ -380,15 +358,15 @@ struct Question(e_cond, e_true, e_false, Cilfacade.typeOf e_false) let next_opt' n = match n with - | Statement {skind=If _; _} when GobConfig.get_bool "exp.arg.uncil" -> - let (e_cond, if_true_next_n, if_false_next_n) = partition_if_next (Arg.next n) in + | Statement {skind=If _; _} -> + let (e_cond, (if_true_next_n, if_true_next_ps), (if_false_next_n, if_false_next_ps)) = partition_if_next (Arg.next n) in let loc = Node.location n in if CilType.Location.equal (Node.location if_true_next_n) loc && CilType.Location.equal (Node.location if_false_next_n) loc then match Arg.next if_true_next_n, Arg.next if_false_next_n with - | [(Assign (v_true, e_true), if_true_next_next_n)], [(Assign (v_false, e_false), if_false_next_next_n)] when v_true = v_false && Node.equal if_true_next_next_n if_false_next_next_n -> + | [(Assign (v_true, e_true), if_true_next_next_n, if_true_next_next_ps)], [(Assign (v_false, e_false), if_false_next_next_n, if_false_next_next_ps)] when v_true = v_false && Node.equal if_true_next_next_n if_false_next_next_n -> let exp = ternary e_cond e_true e_false in Some [ - (Assign (v_true, exp), if_true_next_next_n) + (Assign (v_true, exp), if_true_next_next_n, cartesian_concat_paths if_true_next_ps if_true_next_next_ps @ cartesian_concat_paths if_false_next_ps if_false_next_next_ps) (* concat two different path families with same variable to same node *) ] | _, _ -> None else @@ -402,19 +380,61 @@ struct | None -> Arg.next n end -module Intra (ArgIntra: SIntraOpt) (Arg: S): - S with module Node = Arg.Node and module Edge = Arg.Edge = +module Intra (ArgIntra: SIntraOpt) (Arg: S) = struct include Arg + (** Starting from ARG node [node], follow CFG path [p] to the resulting ARG node. + Returns multiple ARG nodes if ARG contains path-sensitivity splits on the same CFG path. *) + let rec follow node p = + let open GobList.Syntax in + match p with + | [] -> [node] + | (e, to_n) :: p' -> + let* (_, node') = List.filter (fun (e', to_node) -> + Edge.equal (Edge.embed e) e' && Node0.equal to_n (Node.cfgnode to_node) + ) (Arg.next node) + in + follow node' p' + + let rec follow' (node : Node.t) p : (Node.t * (Edge.t * Node.t) list) list = + let open GobList.Syntax in + match p with + | [] -> [node, []] + | (e, to_n) :: p' -> + let* (_, node') = List.filter (fun (e', to_node) -> + Edge.equal (Edge.embed e) e' && Node0.equal to_n (Node.cfgnode to_node) + ) (Arg.next node) + in + let+ (n, l) = follow' node' p' in + (n, (Edge.embed e, node') :: l) + let next node = - let open GobOption.Syntax in + let open GobList.Syntax in match ArgIntra.next_opt (Node.cfgnode node) with | None -> Arg.next node | Some next -> next - |> BatList.filter_map (fun (e, to_n) -> - let+ to_node = Node.move_opt node to_n in + |> BatList.concat_map (fun (e, to_n, p) -> + let* p in + let+ to_node = follow node p in + assert (Node0.equal to_n (Node.cfgnode to_node)); (* should always hold by follow filter above *) (Edge.embed e, to_node) ) + |> BatList.unique_cmp ~cmp:[%ord: Edge.t * Node.t] (* after following paths, there may be duplicates because same ARG node can be reached via same ARG edge via multiple uncilled CFG paths *) (* TODO: avoid generating duplicates in the first place? *) + + let next' node = + let open GobList.Syntax in + match ArgIntra.next_opt (Node.cfgnode node) with + | None -> + Arg.next node + |> List.map (fun (e,n) -> (e,n, [e, n])) + | Some next -> + next + |> BatList.concat_map (fun (e, to_n, p) -> + let* p in + let+ (to_node, path) = follow' node p in + assert (Node0.equal to_n (Node.cfgnode to_node)); (* should always hold by follow' filter above *) + (Edge.embed e, to_node, path) + ) end diff --git a/src/arg/violation.ml b/src/arg/violation.ml index 4ae84a9fcf..fb13909baa 100644 --- a/src/arg/violation.ml +++ b/src/arg/violation.ml @@ -1,4 +1,7 @@ (** Violation checking in an ARG. *) +open MyARG + +let witch_runs = ref 0 module type ViolationArg = sig @@ -43,20 +46,316 @@ sig val check_path: (Node.t * MyARG.inline_edge * Node.t) list -> result end -module UnknownFeasibility (Node: MyARG.Node): Feasibility with module Node = Node = +module CfgNode = Node + +module UnknownFeasibility (Arg: ArgTools.BiArg): Feasibility with module Node = Arg.Node = struct - module Node = Node + module Node = Arg.Node + module SegMap = Map.Make (Node) + module SegNrToPathMap = Map.Make (Int) type result = | Feasible | Infeasible of (Node.t * MyARG.inline_edge * Node.t) list | Unknown - let check_path _ = Unknown -end + open YamlWitness.Entry + (* TODO: duplicate code copied from YamlWitness.write *) + let input_files = GobConfig.get_string_list "files" + let data_model = match GobConfig.get_string "exp.architecture" with + | "64bit" -> "LP64" + | "32bit" -> "ILP32" + | _ -> failwith "invalid architecture" + let specification = Option.map (fun (module Task: Svcomp.Task) -> + Svcomp.Specification.to_string Task.specification + ) !Svcomp.task + let task = task ~input_files ~data_model ~specification + + let write (path : (Node.t * MyARG.inline_edge * Node.t) list) = + let module FileCfg = + struct + let file = !Cilfacade.current_file + module Cfg = (val !MyCFG.current_cfg) + end in + let module WitnessInvariant = WitnessUtil.YamlInvariant (FileCfg) in + let module UnCilArg = Intra (UnCilTernaryIntra (UnCilLogicIntra (CfgIntra (FileCfg.Cfg)))) (Arg) in + + let entries, segToPathMap, segments, has_branching = + if YamlWitness.entry_type_enabled YamlWitnessType.ViolationSequence.entry_type then ( + let open GobOption.Syntax in + + let has_branching = ref false in + let loc prev location = + let cfgNode = Node.cfgnode prev in + let fundec = CfgNode.find_fundec cfgNode in + let location_function = fundec.svar.vname in + YamlWitness.Entry.location ~location ~location_function + in + + let scc_of n = CfgTools.NH.find_option CfgTools.node_scc_global (Node.cfgnode n) in + + let segment_for_edge ((prev, edge, node) as path_elem) prev_path_elem = + let check_if_skips_loop () = + let nodes_in_same_loop_scc (prev, _, node) = + match scc_of prev, scc_of node with + | Some scc1, Some scc2 -> CfgTools.SCC.equal scc1 scc2 + | _ -> false + in + match prev_path_elem with + | Some prev_path_elem -> not (nodes_in_same_loop_scc path_elem || nodes_in_same_loop_scc prev_path_elem) + | _ -> false + in + + match scc_of node with + | Some scc2 when CfgTools.NH.length scc2.nodes > 1 -> None + | _ -> + match edge with + (* TODO: Correct locations for function entry and return are currently unavailable. + As specified by the Witness 2.0 format, these locations must point to + the closing parenthesis after the function's parameter list. + *) + (* + | MyARG.InlineEntry _ -> + let function_enter = function_enter ~location ~action:"follow" in + let waypoints = [waypoint ~waypoint_type:(FunctionEnter function_enter)] in + segment ~waypoints + | MyARG.InlineReturn _ -> + let constraint_ = constraint_ ~value:(String "1") in + let function_return = function_return ~location ~action:"follow" ~constraint_ in + let waypoints = [waypoint ~waypoint_type:(FunctionReturn function_return)] in + segment ~waypoints + *) + | MyARG.CFGEdge Ret (None, _) -> None + | MyARG.CFGEdge Test (_, b) -> + let cfgNode = Node.cfgnode prev in + let+ location = + match WitnessInvariant.location_location cfgNode, WitnessInvariant.loop_location cfgNode with + | Some l1, Some l2 when b = false && check_if_skips_loop () -> assert (CilType.Location.equal l1 l2); Some (loc prev l1) + | _, Some l when b = false && check_if_skips_loop () -> Some (loc prev l) + | Some l, _ -> Some (loc prev l) + | _ -> None + in + let constraint_ = constraint_ ~value:(String (Bool.to_string b)) in + let branching = branching ~location ~action:"follow" ~constraint_ in + let waypoints = [waypoint ~waypoint_type:(Branching branching)] in + has_branching := true; + segment ~waypoints + | _ -> + let cfgNode = Node.cfgnode prev in + let+ l = WitnessInvariant.location_location cfgNode in + let location = loc prev l in + let constraint_ = constraint_ ~value:(String "1") in + let assumption = assumption ~location ~constraint_ in + let waypoints = [waypoint ~waypoint_type:(Assumption assumption)] in + segment ~waypoints + in + + let uncil prev (sub_path : (Node.t * inline_edge * Node.t) list) = + let rec is_prefix prefix full = + match prefix, full with + | [], _ -> true + | _, [] -> false + | (e,n)::xs, (_, e1, n1)::ys -> Node.equal n n1 && Arg.Edge.equal e e1 && is_prefix xs ys + in + let nexts = UnCilArg.next' prev in + let (new_edge, new_node, p) = List.find (fun (_, _, p) -> is_prefix p sub_path) nexts in + (new_edge, new_node) + in + + let rec build_segments path segToPathMap segNr ~prev_path_elem = + match path with + | [] -> SegMap.empty, segToPathMap, 0 + | [(prev, _, node) as path_elem] as sub_path -> + let cfgNode = Node.cfgnode node in + let l = Option.get (WitnessInvariant.location_location cfgNode) in + let target = segment ~waypoints:[waypoint ~waypoint_type:(Target (violation_target ~location:(loc node l)))] in + let this_seg, segToPathMap, segNr = match segment_for_edge path_elem prev_path_elem with + | Some seg -> + let segToPathMap1 = SegNrToPathMap.add 0 sub_path segToPathMap in + let segToPathMap2 = SegNrToPathMap.add 1 sub_path segToPathMap1 in + seg :: [target], segToPathMap2, 2 + | None -> + [target], SegNrToPathMap.add 0 sub_path segToPathMap, 1 + in + let segmap = SegMap.singleton node [target] in + SegMap.add prev this_seg segmap, segToPathMap, segNr + | (prev, _, _) as path_elem :: rest as sub_path -> + let segmap, segToPathMap, segNr = build_segments rest segToPathMap segNr ~prev_path_elem:(Some path_elem) in + let new_edge, new_node = uncil prev sub_path in + let segments = Option.get (SegMap.find_opt new_node segmap) in + let this_seg, segToPathMap, segNr = match segment_for_edge (prev, new_edge, new_node) prev_path_elem with + | Some seg -> seg :: segments, SegNrToPathMap.add segNr sub_path segToPathMap, segNr + 1 + | None -> segments, segToPathMap, segNr + in + SegMap.add prev this_seg segmap, segToPathMap, segNr + in + + let segmap, segToPathMap, _ = build_segments path SegNrToPathMap.empty 0 ~prev_path_elem:None in + let segments = + match path with + | [] -> [] + | (prev, _, _) :: _ -> SegMap.find prev segmap + in + + let entry = YamlWitness.Entry.violation_sequence ~task ~violation:segments in + [entry], segToPathMap, segments, !has_branching + ) + else + [], SegNrToPathMap.empty, [], false + in + + let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in + (* TODO: "witness generation summary" message *) + YamlWitness.yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path")); + (segToPathMap, segments), has_branching + + let read_command_output command = + let (ic, _) as process = Unix.open_process command in + let rec read_lines acc = + try + let line = input_line ic in + Logs.info "Witch: %s" line; + read_lines (line :: acc) + with End_of_file -> + ignore (Unix.close_process process); + acc + in + read_lines [] + + let extract_result_line lines = + let re = Str.regexp "^RESULT: \\(.*\\)$" in + List.find_map (fun line -> if Str.string_match re line 0 then Some (Str.matched_group 1 line) else None) lines + + let extract_invalid_locations lines = + let re = Str.regexp "^INFO: Found invalid locations in segments \\[\\(.*\\)\\]$" in + List.find_map + (fun line -> + if Str.string_match re line 0 then + let inside = Str.matched_group 1 line in + let parts = Str.split (Str.regexp "[ ,]+") inside in + let nums = parts |> List.filter (fun s -> s <> "") |> List.map int_of_string in + Some nums + else + None) + lines + + (* TODO: find both (result and seg nr) with one traversal *) + let extract_unreach_seg_nr lines = + let re = Str.regexp "segment \\([0-9]+\\) cannot be passed" in + List.find_map (fun line -> + try ignore (Str.search_forward re line 0); Some (int_of_string (Str.matched_group 1 line)) + with Not_found -> None + ) lines + + let run_witch ~check_locs = + incr witch_runs; + let files = String.concat " " (GobConfig.get_string_list "files") in + let data_model = match GobConfig.get_string "exp.architecture" with + | "64bit" -> "--64" + | "32bit" -> "--32" + | _ -> failwith "invalid architecture" + in + let property = GobConfig.get_string "ana.specification" in + let witness_file_path = GobConfig.get_string "witness.yaml.path" in + let check_locs_flag = if check_locs then "--check-all-locations" else "" in + (* ../witch/scripts/symbiotic --witness-check ../analyzer/witness.yml --32 ../analyzer/violation-witness.c *) + let witch_path_s = Fpath.to_string (Fpath.append GobSys.exe_dir (Fpath.v (GobConfig.get_string "exp.witch"))) in + let command = Printf.sprintf "%s --witness-check %s --witness %s --prp %s %s %s --guide-only %s" witch_path_s witness_file_path witness_file_path property data_model check_locs_flag files in + read_command_output command + + let get_unreachable_path lines (path: (Node.t * inline_edge * Node.t) list) (segToPathMap, segments) = + let module NHT = BatHashtbl.Make (Arg.Node) in + let node_to_stack = NHT.create 100 in + + let collect_callstack node edge next_node = + let prev_stack = NHT.find_option node_to_stack node |> Option.value ~default:[] in + let new_stack = match edge with + | InlineEntry _ -> node :: prev_stack + | InlineReturn _ -> BatList.drop 1 prev_stack + | _ -> prev_stack + in + NHT.replace node_to_stack next_node new_stack; + in + + List.iter (fun (node, edge, next_node) -> collect_callstack node edge next_node) path; + + let has_no_branching_before_unreachable segments seg_nr = + let rec check i: YamlWitnessType.ViolationSequence.Segment.t list -> bool = function + | _ when i = seg_nr -> true + | [] -> true + | {segment = {waypoint_type = Branching _} :: _} :: _ -> false + | _ :: rest -> check (i + 1) rest + in + check 0 segments + in + + let is_within_loop (node, _, _) = + let callstack = NHT.find_option node_to_stack node |> Option.value ~default:[] in + let scc_components = CfgTools.node_scc_global in + + let is_in_loop node = + match CfgTools.NH.find_option scc_components (Node.cfgnode node) with + | Some scc when CfgTools.NH.length scc.nodes > 1 -> true + | _ -> false + in + + List.exists is_in_loop (node :: callstack) + in + + let has_setjump_calls (path: (Node.t * inline_edge * Node.t) list): bool = + let rec check: (Node.t * inline_edge * Node.t) list -> bool = function + | [] -> false + | (_, MyARG.CFGEdge Proc (_, Lval((Var v, _)), _) , _) :: _ when v.vname = "_setjmp" -> true + | _ :: rest -> check rest + in + check path + in + + match extract_unreach_seg_nr lines with + | Some seg_nr when has_no_branching_before_unreachable segments seg_nr && not (has_setjump_calls path) -> + (* TODO: consider seg_nr = 0 separately *) + let path_suffix = SegNrToPathMap.find (List.length segments - seg_nr -1) segToPathMap in + let path_suffix_plus_one = BatList.drop (List.length path - List.length path_suffix -1) path in + if not (is_within_loop (List.hd path_suffix_plus_one)) then path_suffix_plus_one + else path + | _ -> path + + let check_feasability_with_witch lines path seg = + match extract_result_line lines with + | Some result when String.starts_with ~prefix:"true" result -> Logs.info "Verification result: %s\n" result; Infeasible (get_unreachable_path lines path seg) + | Some result when String.starts_with ~prefix:"false" result -> Logs.info "Verification result: %s\n" result; Feasible + | Some _ -> Unknown + | None -> Unknown + + let check_and_remove_invalid_locs lines path (segToPathMap, segments as seg) = + match extract_invalid_locations lines with + | Some seg_nrs -> + let segments' = List.filteri (fun i _ -> not @@ List.mem i seg_nrs) segments in + let entries = [YamlWitness.Entry.violation_sequence ~task ~violation:segments'] in + let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in + (* TODO: "witness generation summary" message *) + YamlWitness.yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path")); + let seg' = (segToPathMap, segments') in + let lines' = run_witch ~check_locs:false in + lines', seg' + | _ -> lines, seg + + let check_path path = + let seg, has_branching = write path in + let witch = GobConfig.get_string "exp.witch" in + match witch with + | "" -> Unknown + | _ -> + if has_branching then + let lines = run_witch ~check_locs:true in + let lines', seg' = check_and_remove_invalid_locs lines path seg in + check_feasability_with_witch lines' path seg' + else + let lines = run_witch ~check_locs:false in + check_feasability_with_witch lines path seg +end -exception Found module type PathArg = MyARG.S with module Edge = MyARG.InlineEdge @@ -81,31 +380,35 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod let print_path path = List.iter (fun (n1, e, n2) -> - Logs.info " %s =[%s]=> %s" (Arg.Node.to_string n1) (Arg.Edge.to_string e) (Arg.Node.to_string n2) + Logs.debug " %s =[%s]=> %s" (Arg.Node.to_string n1) (Arg.Edge.to_string e) (Arg.Node.to_string n2) ) path in + let exception Found of Arg.Node.t in + let find_path nodes = let next_nodes = NHT.create 100 in - let itered_nodes = NHT.create 100 in + let rec bfs curs nexts = match curs with | node :: curs' -> - if Arg.Node.equal node Arg.main_entry then - raise Found + if BatList.mem_cmp Arg.Node.compare node Arg.violations then + raise (Found node) else if not (NHT.mem itered_nodes node) then begin NHT.replace itered_nodes node (); - List.iter (fun (edge, prev_node) -> + let next_nodes = List.filter_map (fun (edge, next_node) -> match edge with | MyARG.CFGEdge _ | InlineEntry _ | InlineReturn _ -> - if not (NHT.mem itered_nodes prev_node) then - NHT.replace next_nodes prev_node (edge, node) + if not (NHT.mem itered_nodes next_node) then + NHT.replace next_nodes next_node (edge, node); + Some next_node | InlinedEdge _ - | ThreadEntry _ -> () - ) (Arg.prev node); - bfs curs' (List.map snd (Arg.prev node) @ nexts) + | ThreadEntry _ -> None + ) (Arg.next node) + in + bfs curs' (next_nodes @ nexts) end else bfs curs' nexts @@ -116,11 +419,11 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod in try bfs nodes []; None with - | Found -> - Some (trace_path next_nodes Arg.main_entry) + | Found violation -> + Some (List.rev_map (fun (n1, e, n2) -> (n2, e, n1)) (trace_path next_nodes violation)) (* TODO: inefficient rev *) in - begin match find_path Arg.violations with + begin match find_path [Arg.main_entry] with | Some path -> print_path path; begin match Feasibility.check_path path with diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 635edb8ab7..452d0297a5 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -90,7 +90,7 @@ let init () = (* lineDirectiveStyle := None; *) RmUnused.keepUnused := true; print_CIL_Input := true; - Cabs2cil.allowDuplication := false; + Cabs2cil.allowDuplication := false; (* needed for ARG uncilling, maybe something else as well? *) Cabs2cil.silenceLongDoubleWarning := true; Cabs2cil.addLoopConditionLabels := true diff --git a/src/config/gobConfig.ml b/src/config/gobConfig.ml index 4ac83f9743..dfd862b673 100644 --- a/src/config/gobConfig.ml +++ b/src/config/gobConfig.ml @@ -351,7 +351,10 @@ struct (** Sets a value, preventing changes when the configuration is immutable and invalidating the cache. @raise Immutable *) let set_value v o pth = - if is_immutable () then raise (Immutable pth); + (* TODO: only needed for adding the observers: + rewrite so that there is only one observer-analysis + that handles all observes internally without new analyses being added. *) + (* if is_immutable () then raise (Immutable pth); *) drop_memo (); unsafe_set_value v o pth diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 52f98ac84c..bfd5f128e8 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -2067,6 +2067,12 @@ } }, "additionalProperties": false + }, + "witch": { + "title": "exp.witch", + "description": "Path to the Witch executable for result refinement.", + "type": "string", + "default": "" } }, "additionalProperties": false diff --git a/src/framework/control.ml b/src/framework/control.ml index 7b05eafdc1..baf8a51446 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -16,7 +16,7 @@ open SpecLifters module type S2S = Spec2Spec (* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *) -let spec_module: (module Spec) Lazy.t = lazy ( +let spec_module: (module Spec) ResettableLazy.t = ResettableLazy.from_fun (fun () -> GobConfig.building_spec := true; let arg_enabled = get_bool "exp.arg.enabled" in let termination_enabled = List.mem "termination" (get_string_list "ana.activated") in (* check if loop termination analysis is enabled*) @@ -49,12 +49,12 @@ let spec_module: (module Spec) Lazy.t = lazy ( in GobConfig.building_spec := false; ControlSpecC.control_spec_c := (module S1.C); - (module S1) + (module S1 : Spec) ) (** gets Spec for current options *) let get_spec (): (module Spec) = - Lazy.force spec_module + ResettableLazy.force spec_module let current_node_state_json : (Node.t -> Yojson.Safe.t option) ref = ref (fun _ -> None) @@ -860,6 +860,7 @@ let rec analyze_loop (module CFG : CfgBidirSkip) file fs change_info = Whoever raised the exception should've modified some global state to do a more precise analysis next time. *) (* TODO: do some more incremental refinement and reuse parts of solution *) + ResettableLazy.reset spec_module; analyze_loop (module CFG) file fs change_info (** The main function to perform the selected analyses. *) diff --git a/src/util/std/gobYaml.ml b/src/util/std/gobYaml.ml index 4c8576ade2..e1473d32d4 100644 --- a/src/util/std/gobYaml.ml +++ b/src/util/std/gobYaml.ml @@ -3,7 +3,7 @@ let to_string' ?(len=65535 * 4) ?encoding ?scalar_style ?layout_style v = let rec aux len = match Yaml.to_string ~len ?encoding ?scalar_style ?layout_style v with | Ok _ as o -> o - | Error (`Msg ("scalar failed" | "doc_end failed" | "seq_end failed")) when len < Sys.max_string_length / 2 -> + | Error (`Msg ("scalar failed" | "doc_end failed" | "seq_end failed" | "mapping_start failed")) when len < Sys.max_string_length / 2 -> aux (len * 2) | Error (`Msg _) as e -> e in diff --git a/src/witness/witness.ml b/src/witness/witness.ml index 229126ff22..6090aa66a9 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -54,6 +54,7 @@ let write_file filename (module Task:Task) (module Arg: MyARG.S with type Edge.t let print_svcomp_result (s: string): unit = + if GobConfig.get_string "exp.witch" <> "" then Logs.info "Witch runs: %d" !Violation.witch_runs; Logs.result "SV-COMP result: %s" s let print_task_result result: unit = @@ -87,18 +88,35 @@ struct let determine_result entrystates (module Task:Task) (spec: Svcomp.Specification.t): Svcomp.Result.t = let module Arg: BiArgInvariant = - struct - module Node = ArgTool.Node - module Edge = MyARG.InlineEdge - let next _ = [] - let prev _ = [] - let find_invariant _ = Invariant.none - let main_entry = - let lvar = WitnessUtil.find_main_entry entrystates in - (fst lvar, snd lvar, -1) - let iter_nodes f = f main_entry - let query _ q = Queries.Result.top q - end + (val if GobConfig.get_bool "exp.arg.enabled" then ( + let module Arg = (val ArgTool.create entrystates) in + let module Arg = + struct + include Arg + + let find_invariant _ = Invariant.none + end + in + (module Arg: BiArgInvariant) + ) + else ( + let module Arg = + struct + module Node = ArgTool.Node + module Edge = MyARG.InlineEdge + let next _ = [] + let prev _ = [] + let find_invariant _ = Invariant.none + let main_entry = + let lvar = WitnessUtil.find_main_entry entrystates in + (fst lvar, snd lvar, -1) + let iter_nodes f = f main_entry + let query _ q = Queries.Result.top q + end + in + (module Arg: BiArgInvariant) + ) + ) in match spec with @@ -149,7 +167,7 @@ struct Result.Unknown in if get_bool "ana.wp" then ( - match Violation.find_path (module ViolationArg) (module ViolationZ3.WP (ViolationArg.Node)) with + match Violation.find_path (module ViolationArg) (module ViolationZ3.WP (ViolationArg)) with | Feasible (module PathArg) -> (* TODO: add assumptions *) Result.False (Some spec) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 2811cd9d84..453ea11373 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -119,7 +119,53 @@ struct with_metadata ~task @@ GhostInstrumentation { ghost_variables = variables; ghost_updates = location_updates; - } + } + + let constraint_ ~value : ViolationSequence.Constraint.t = { + value = value; + format = Some "c_expression"; + } + + let assumption ~location ~constraint_ : ViolationSequence.Assumption.t = { + location = location; + action = "follow"; + constraint_ = constraint_; + } + + let violation_target ~location : ViolationSequence.Target.t = { + location = location; + action = "follow"; + } + + let function_enter ~location ~action : ViolationSequence.FunctionEnter.t = { + location = location; + action = action; + } + + let function_return ~location ~action ~constraint_ : ViolationSequence.FunctionReturn.t = { + location = location; + action = action; + constraint_ = constraint_; + } + + let branching ~location ~action ~constraint_ : ViolationSequence.Branching.t = { + location = location; + action = action; + constraint_ = constraint_; + } + + let waypoint ~waypoint_type : ViolationSequence.Waypoint.t = { + waypoint_type = waypoint_type; + } + + let segment ~waypoints : ViolationSequence.Segment.t = { + segment = waypoints; + } + + let violation_sequence ~task ~(violation): Entry.t = + with_metadata ~task @@ ViolationSequence { + content = violation; + }; end let yaml_entries_to_file yaml_entries file = diff --git a/tests/regression/dune b/tests/regression/dune index 0fd8052478..b1e37d56fd 100644 --- a/tests/regression/dune +++ b/tests/regression/dune @@ -27,3 +27,7 @@ (package goblint) %{bin:yamlWitnessStrip} %{bin:yamlWitnessStripDiff})) + +(cram + (applies_to violation) + (enabled_if (<> %{system} macosx))) \ No newline at end of file diff --git a/tests/regression/witness/violation.t/correct-hard.c b/tests/regression/witness/violation-validation.t/correct-hard.c similarity index 100% rename from tests/regression/witness/violation.t/correct-hard.c rename to tests/regression/witness/violation-validation.t/correct-hard.c diff --git a/tests/regression/witness/violation.t/correct-hard.yml b/tests/regression/witness/violation-validation.t/correct-hard.yml similarity index 100% rename from tests/regression/witness/violation.t/correct-hard.yml rename to tests/regression/witness/violation-validation.t/correct-hard.yml diff --git a/tests/regression/witness/violation.t/correct.c b/tests/regression/witness/violation-validation.t/correct.c similarity index 100% rename from tests/regression/witness/violation.t/correct.c rename to tests/regression/witness/violation-validation.t/correct.c diff --git a/tests/regression/witness/violation.t/correct.yml b/tests/regression/witness/violation-validation.t/correct.yml similarity index 100% rename from tests/regression/witness/violation.t/correct.yml rename to tests/regression/witness/violation-validation.t/correct.yml diff --git a/tests/regression/witness/violation.t/incorrect.c b/tests/regression/witness/violation-validation.t/incorrect.c similarity index 100% rename from tests/regression/witness/violation.t/incorrect.c rename to tests/regression/witness/violation-validation.t/incorrect.c diff --git a/tests/regression/witness/violation.t/incorrect.yml b/tests/regression/witness/violation-validation.t/incorrect.yml similarity index 100% rename from tests/regression/witness/violation.t/incorrect.yml rename to tests/regression/witness/violation-validation.t/incorrect.yml diff --git a/tests/regression/witness/violation-validation.t/run.t b/tests/regression/witness/violation-validation.t/run.t new file mode 100644 index 0000000000..1fc408635e --- /dev/null +++ b/tests/regression/witness/violation-validation.t/run.t @@ -0,0 +1,57 @@ +Violation witness for a correct program can be refuted by proving the program correct and returning `true`: + + $ goblint --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" correct.c --set witness.yaml.validate correct.yml + [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) ) + [Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (correct.c:1:1-1:20) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 2 + dead: 1 (1 in uncalled functions) + total lines: 3 + [Info][Witness] witness validation summary: + confirmed: 0 + unconfirmed: 0 + refuted: 0 + error: 0 + unchecked: 0 + unsupported: 0 + disabled: 0 + total validation entries: 0 + SV-COMP result: true + +If a correct progtam cannot be proven correct, return `unknown` for the violation witness: + + $ goblint --set ana.activated[-] expRelation --enable ana.sv-comp.functions --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" correct-hard.c --set witness.yaml.validate correct-hard.yml + [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) ) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Info][Witness] witness validation summary: + confirmed: 0 + unconfirmed: 0 + refuted: 0 + error: 0 + unchecked: 0 + unsupported: 0 + disabled: 0 + total validation entries: 0 + SV-COMP result: unknown + +Violation witness for an incorrect program cannot be proven correct, so return `unknown`: + + $ goblint --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" incorrect.c --set witness.yaml.validate incorrect.yml + [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) ) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 4 + dead: 0 + total lines: 4 + [Info][Witness] witness validation summary: + confirmed: 0 + unconfirmed: 0 + refuted: 0 + error: 0 + unchecked: 0 + unsupported: 0 + disabled: 0 + total validation entries: 0 + SV-COMP result: unknown diff --git a/tests/regression/witness/violation.t/nec11.c b/tests/regression/witness/violation.t/nec11.c new file mode 100644 index 0000000000..03c2f58728 --- /dev/null +++ b/tests/regression/witness/violation.t/nec11.c @@ -0,0 +1,34 @@ +extern void abort(void); +extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); +void reach_error() { __assert_fail("0", "nec11.c", 3, "reach_error"); } + +void __VERIFIER_assert(int cond) { + if (!(cond)) { + ERROR: {reach_error();abort();} + } + return; +} + +_Bool __VERIFIER_nondet_bool(); + +int main(){ + int a[5]; + int len=0; + _Bool c=__VERIFIER_nondet_bool(); + int i; + + + while(c){ + + if (len==4) + len =0; + + a[len]=0; + + len++; + } + __VERIFIER_assert(len==5); + return 1; + + +} diff --git a/tests/regression/witness/violation.t/run.t b/tests/regression/witness/violation.t/run.t index 1fc408635e..713f29b99e 100644 --- a/tests/regression/witness/violation.t/run.t +++ b/tests/regression/witness/violation.t/run.t @@ -1,57 +1,81 @@ -Violation witness for a correct program can be refuted by proving the program correct and returning `true`: - - $ goblint --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" correct.c --set witness.yaml.validate correct.yml - [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) ) - [Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (correct.c:1:1-1:20) - [Info][Deadcode] Logical lines of code (LLoC) summary: - live: 2 - dead: 1 (1 in uncalled functions) - total lines: 3 - [Info][Witness] witness validation summary: - confirmed: 0 - unconfirmed: 0 - refuted: 0 - error: 0 - unchecked: 0 - unsupported: 0 - disabled: 0 - total validation entries: 0 - SV-COMP result: true - -If a correct progtam cannot be proven correct, return `unknown` for the violation witness: - - $ goblint --set ana.activated[-] expRelation --enable ana.sv-comp.functions --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" correct-hard.c --set witness.yaml.validate correct-hard.yml + $ goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )"} nec11.c --enable exp.arg.enabled --enable ana.wp --set witness.yaml.entry-types[+] violation_sequence --enable witness.yaml.sv-comp-true-only --enable witness.invariant.other [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) ) + [Warning][Integer > Overflow][CWE-190] Signed integer overflow (nec11.c:28:7-28:12) [Info][Deadcode] Logical lines of code (LLoC) summary: - live: 7 + live: 16 dead: 0 - total lines: 7 - [Info][Witness] witness validation summary: - confirmed: 0 - unconfirmed: 0 - refuted: 0 - error: 0 - unchecked: 0 - unsupported: 0 - disabled: 0 - total validation entries: 0 + total lines: 16 SV-COMP result: unknown -Violation witness for an incorrect program cannot be proven correct, so return `unknown`: - - $ goblint --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" incorrect.c --set witness.yaml.validate incorrect.yml - [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) ) - [Info][Deadcode] Logical lines of code (LLoC) summary: - live: 4 - dead: 0 - total lines: 4 - [Info][Witness] witness validation summary: - confirmed: 0 - unconfirmed: 0 - refuted: 0 - error: 0 - unchecked: 0 - unsupported: 0 - disabled: 0 - total validation entries: 0 - SV-COMP result: unknown + $ yamlWitnessStrip < witness.yml + - entry_type: violation_sequence + content: + - segment: + - waypoint: + type: assumption + location: + file_name: nec11.c + line: 16 + column: 4 + function: main + action: follow + constraint: + value: "1" + format: c_expression + - segment: + - waypoint: + type: assumption + location: + file_name: nec11.c + line: 17 + column: 4 + function: main + action: follow + constraint: + value: "1" + format: c_expression + - segment: + - waypoint: + type: branching + location: + file_name: nec11.c + line: 21 + column: 4 + function: main + action: follow + constraint: + value: "false" + format: c_expression + - segment: + - waypoint: + type: assumption + location: + file_name: nec11.c + line: 30 + column: 4 + function: main + action: follow + constraint: + value: "1" + format: c_expression + - segment: + - waypoint: + type: branching + location: + file_name: nec11.c + line: 6 + column: 3 + function: __VERIFIER_assert + action: follow + constraint: + value: "true" + format: c_expression + - segment: + - waypoint: + type: target + location: + file_name: nec11.c + line: 7 + column: 13 + function: __VERIFIER_assert + action: follow diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous1.c b/tests/sv-comp/cfg/uncil/and_ambiguous1.c new file mode 100644 index 0000000000..d35441c02c --- /dev/null +++ b/tests/sv-comp/cfg/uncil/and_ambiguous1.c @@ -0,0 +1,13 @@ +#include + +int main() { + int a, b; + + __goblint_split_begin(a); + if (a && b) { + return 1; + } + else { + return 0; + } +} diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous1.expected b/tests/sv-comp/cfg/uncil/and_ambiguous1.expected new file mode 100644 index 0000000000..560abd05c3 --- /dev/null +++ b/tests/sv-comp/cfg/uncil/and_ambiguous1.expected @@ -0,0 +1,27 @@ + ┌──────────────────────────────────┐ + │ _ │ + └──────────────────────────────────┘ + │ + │ Entry main + ▼ + ┌──────────────────────────────────┐ + │ _ │ + └──────────────────────────────────┘ + │ + │ Proc '__goblint_split_begin(a)' + ▼ +┌───┐ Test (a && b,false) ┌──────────────────────────────────┐ Test (a && b,false) ┌───┐ +│ _ │ ◀───────────────────── │ _ │ ─────────────────────▶ │ _ │ +└───┘ └──────────────────────────────────┘ └───┘ + │ │ │ + │ │ Test (a && b,true) │ + │ ▼ │ + │ ┌──────────────────────────────────┐ │ + │ │ _ │ │ + │ └──────────────────────────────────┘ │ + │ │ │ + │ │ Ret (Some 1, main) │ + │ ▼ │ + │ Ret (Some 0, main) ┌──────────────────────────────────┐ Ret (Some 0, main) │ + └────────────────────────▶ │ _ │ ◀────────────────────────┘ + └──────────────────────────────────┘ diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous2.c b/tests/sv-comp/cfg/uncil/and_ambiguous2.c new file mode 100644 index 0000000000..058ccee377 --- /dev/null +++ b/tests/sv-comp/cfg/uncil/and_ambiguous2.c @@ -0,0 +1,13 @@ +#include + +int main() { + int a, b; + + __goblint_split_begin(b); + if (a && b) { + return 1; + } + else { + return 0; + } +} diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous2.expected b/tests/sv-comp/cfg/uncil/and_ambiguous2.expected new file mode 100644 index 0000000000..1cbc9466a2 --- /dev/null +++ b/tests/sv-comp/cfg/uncil/and_ambiguous2.expected @@ -0,0 +1,27 @@ + ┌──────────────────────────────────┐ + │ _ │ + └──────────────────────────────────┘ + │ + │ Entry main + ▼ + ┌──────────────────────────────────┐ + │ _ │ + └──────────────────────────────────┘ + │ + │ Proc '__goblint_split_begin(b)' + ▼ +┌───┐ Test (a && b,false) ┌──────────────────────────────────┐ Test (a && b,false) ┌───┐ +│ _ │ ◀───────────────────── │ _ │ ─────────────────────▶ │ _ │ +└───┘ └──────────────────────────────────┘ └───┘ + │ │ │ + │ │ Test (a && b,true) │ + │ ▼ │ + │ ┌──────────────────────────────────┐ │ + │ │ _ │ │ + │ └──────────────────────────────────┘ │ + │ │ │ + │ │ Ret (Some 1, main) │ + │ ▼ │ + │ Ret (Some 0, main) ┌──────────────────────────────────┐ Ret (Some 0, main) │ + └────────────────────────▶ │ _ │ ◀────────────────────────┘ + └──────────────────────────────────┘ diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous_partition1.c b/tests/sv-comp/cfg/uncil/and_ambiguous_partition1.c new file mode 100644 index 0000000000..5115845160 --- /dev/null +++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition1.c @@ -0,0 +1,13 @@ +#include + +int main() { + int a, b = 0, c; + + __goblint_split_begin(a); + if (a && b && c) { + return 1; + } + else { + return 0; + } +} diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous_partition1.expected b/tests/sv-comp/cfg/uncil/and_ambiguous_partition1.expected new file mode 100644 index 0000000000..8c1a83b95a --- /dev/null +++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition1.expected @@ -0,0 +1,33 @@ + ┌──────────────────────────────────┐ + │ _ │ + └──────────────────────────────────┘ + │ + │ Entry main + ▼ + ┌──────────────────────────────────┐ + │ _ │ + └──────────────────────────────────┘ + │ + │ Assign 'b = 0' + ▼ + ┌──────────────────────────────────┐ + │ _ │ + └──────────────────────────────────┘ + │ + │ Proc '__goblint_split_begin(a)' + ▼ +┌───┐ Test (a && (b && c),false) ┌──────────────────────────────────┐ +│ _ │ ◀──────────────────────────── │ _ │ +└───┘ └──────────────────────────────────┘ + │ │ + │ │ Test (a && (b && c),false) + │ ▼ + │ ┌──────────────────────────────────┐ + │ │ _ │ + │ └──────────────────────────────────┘ + │ │ + │ │ Ret (Some 0, main) + │ ▼ + │ Ret (Some 0, main) ┌──────────────────────────────────┐ + └───────────────────────────────▶ │ _ │ + └──────────────────────────────────┘ diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous_partition2.c b/tests/sv-comp/cfg/uncil/and_ambiguous_partition2.c new file mode 100644 index 0000000000..a1b3668a66 --- /dev/null +++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition2.c @@ -0,0 +1,13 @@ +#include + +int main() { + int a, b = 1, c; + + __goblint_split_begin(a); + if (a && b && c) { + return 1; + } + else { + return 0; + } +} diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous_partition2.expected b/tests/sv-comp/cfg/uncil/and_ambiguous_partition2.expected new file mode 100644 index 0000000000..4d44cd4454 --- /dev/null +++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition2.expected @@ -0,0 +1,33 @@ + ┌──────────────────────────────────┐ + │ _ │ + └──────────────────────────────────┘ + │ + │ Entry main + ▼ + ┌──────────────────────────────────┐ + │ _ │ + └──────────────────────────────────┘ + │ + │ Assign 'b = 1' + ▼ + ┌──────────────────────────────────┐ + │ _ │ + └──────────────────────────────────┘ + │ + │ Proc '__goblint_split_begin(a)' + ▼ +┌───┐ Test (a && (b && c),false) ┌──────────────────────────────────┐ Test (a && (b && c),false) ┌───┐ +│ _ │ ◀──────────────────────────── │ _ │ ────────────────────────────▶ │ _ │ +└───┘ └──────────────────────────────────┘ └───┘ + │ │ │ + │ │ Test (a && (b && c),true) │ + │ ▼ │ + │ ┌──────────────────────────────────┐ │ + │ │ _ │ │ + │ └──────────────────────────────────┘ │ + │ │ │ + │ │ Ret (Some 1, main) │ + │ ▼ │ + │ Ret (Some 0, main) ┌──────────────────────────────────┐ Ret (Some 0, main) │ + └───────────────────────────────▶ │ _ │ ◀───────────────────────────────┘ + └──────────────────────────────────┘ diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous_partition3.c b/tests/sv-comp/cfg/uncil/and_ambiguous_partition3.c new file mode 100644 index 0000000000..959d0dd343 --- /dev/null +++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition3.c @@ -0,0 +1,13 @@ +#include + +int main() { + int a, b, c = 0; + + __goblint_split_begin(a); + if (a && b && c) { + return 1; + } + else { + return 0; + } +} diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous_partition3.expected b/tests/sv-comp/cfg/uncil/and_ambiguous_partition3.expected new file mode 100644 index 0000000000..7a31f9703e --- /dev/null +++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition3.expected @@ -0,0 +1,33 @@ + ┌──────────────────────────────────┐ + │ _ │ + └──────────────────────────────────┘ + │ + │ Entry main + ▼ + ┌──────────────────────────────────┐ + │ _ │ + └──────────────────────────────────┘ + │ + │ Assign 'c = 0' + ▼ + ┌──────────────────────────────────┐ + │ _ │ + └──────────────────────────────────┘ + │ + │ Proc '__goblint_split_begin(a)' + ▼ +┌───┐ Test (a && (b && c),false) ┌──────────────────────────────────┐ +│ _ │ ◀──────────────────────────── │ _ │ +└───┘ └──────────────────────────────────┘ + │ │ + │ │ Test (a && (b && c),false) + │ ▼ + │ ┌──────────────────────────────────┐ + │ │ _ │ + │ └──────────────────────────────────┘ + │ │ + │ │ Ret (Some 0, main) + │ ▼ + │ Ret (Some 0, main) ┌──────────────────────────────────┐ + └───────────────────────────────▶ │ _ │ + └──────────────────────────────────┘ diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous_partition4.c b/tests/sv-comp/cfg/uncil/and_ambiguous_partition4.c new file mode 100644 index 0000000000..5f7a958ddd --- /dev/null +++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition4.c @@ -0,0 +1,13 @@ +#include + +int main() { + int a, b, c = 1; + + __goblint_split_begin(a); + if (a && b && c) { + return 1; + } + else { + return 0; + } +} diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous_partition4.expected b/tests/sv-comp/cfg/uncil/and_ambiguous_partition4.expected new file mode 100644 index 0000000000..01db9837f8 --- /dev/null +++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition4.expected @@ -0,0 +1,33 @@ + ┌──────────────────────────────────┐ + │ _ │ + └──────────────────────────────────┘ + │ + │ Entry main + ▼ + ┌──────────────────────────────────┐ + │ _ │ + └──────────────────────────────────┘ + │ + │ Assign 'c = 1' + ▼ + ┌──────────────────────────────────┐ + │ _ │ + └──────────────────────────────────┘ + │ + │ Proc '__goblint_split_begin(a)' + ▼ +┌───┐ Test (a && (b && c),false) ┌──────────────────────────────────┐ Test (a && (b && c),false) ┌───┐ +│ _ │ ◀──────────────────────────── │ _ │ ────────────────────────────▶ │ _ │ +└───┘ └──────────────────────────────────┘ └───┘ + │ │ │ + │ │ Test (a && (b && c),true) │ + │ ▼ │ + │ ┌──────────────────────────────────┐ │ + │ │ _ │ │ + │ └──────────────────────────────────┘ │ + │ │ │ + │ │ Ret (Some 1, main) │ + │ ▼ │ + │ Ret (Some 0, main) ┌──────────────────────────────────┐ Ret (Some 0, main) │ + └───────────────────────────────▶ │ _ │ ◀───────────────────────────────┘ + └──────────────────────────────────┘ diff --git a/tests/sv-comp/dune.inc b/tests/sv-comp/dune.inc index 689f97ebf3..3ff8f5a872 100644 --- a/tests/sv-comp/dune.inc +++ b/tests/sv-comp/dune.inc @@ -12,7 +12,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -34,7 +34,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -56,7 +56,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -78,7 +78,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -100,7 +100,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -122,7 +122,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -144,7 +144,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -166,7 +166,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -188,7 +188,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -210,7 +210,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -232,7 +232,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -254,7 +254,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -276,7 +276,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -298,7 +298,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -320,7 +320,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -342,7 +342,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -364,7 +364,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -386,7 +386,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -408,7 +408,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -430,7 +430,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -452,7 +452,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -474,7 +474,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -496,7 +496,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -518,7 +518,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -540,7 +540,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -562,7 +562,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -584,7 +584,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -606,7 +606,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -628,7 +628,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -650,7 +650,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -672,7 +672,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -694,7 +694,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -716,7 +716,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -738,7 +738,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -760,7 +760,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -770,6 +770,138 @@ (action (diff and3dead_true-unreach-call.expected and3dead_true-unreach-call.output)))) +(subdir cfg/uncil + (rule + (deps + (sandbox always) ; must sandbox to prevent arg.dot-s from parallel runs from interfering + (package goblint) ; depend on entire goblint package for svcomp21 conf + (:c and_ambiguous1.c) + (:prop %{project_root}/tests/sv-comp/unreach-call-__VERIFIER_error.prp)) + (target and_ambiguous1.output) + (enabled_if %{bin-available:graph-easy}) + (action + (progn + (ignore-outputs + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) + (with-outputs-to %{target} + (run graph-easy --as=boxart arg.dot))))) + + (rule + (alias runtest) + (enabled_if %{bin-available:graph-easy}) + (action + (diff and_ambiguous1.expected and_ambiguous1.output)))) + +(subdir cfg/uncil + (rule + (deps + (sandbox always) ; must sandbox to prevent arg.dot-s from parallel runs from interfering + (package goblint) ; depend on entire goblint package for svcomp21 conf + (:c and_ambiguous2.c) + (:prop %{project_root}/tests/sv-comp/unreach-call-__VERIFIER_error.prp)) + (target and_ambiguous2.output) + (enabled_if %{bin-available:graph-easy}) + (action + (progn + (ignore-outputs + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) + (with-outputs-to %{target} + (run graph-easy --as=boxart arg.dot))))) + + (rule + (alias runtest) + (enabled_if %{bin-available:graph-easy}) + (action + (diff and_ambiguous2.expected and_ambiguous2.output)))) + +(subdir cfg/uncil + (rule + (deps + (sandbox always) ; must sandbox to prevent arg.dot-s from parallel runs from interfering + (package goblint) ; depend on entire goblint package for svcomp21 conf + (:c and_ambiguous_partition1.c) + (:prop %{project_root}/tests/sv-comp/unreach-call-__VERIFIER_error.prp)) + (target and_ambiguous_partition1.output) + (enabled_if %{bin-available:graph-easy}) + (action + (progn + (ignore-outputs + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) + (with-outputs-to %{target} + (run graph-easy --as=boxart arg.dot))))) + + (rule + (alias runtest) + (enabled_if %{bin-available:graph-easy}) + (action + (diff and_ambiguous_partition1.expected and_ambiguous_partition1.output)))) + +(subdir cfg/uncil + (rule + (deps + (sandbox always) ; must sandbox to prevent arg.dot-s from parallel runs from interfering + (package goblint) ; depend on entire goblint package for svcomp21 conf + (:c and_ambiguous_partition2.c) + (:prop %{project_root}/tests/sv-comp/unreach-call-__VERIFIER_error.prp)) + (target and_ambiguous_partition2.output) + (enabled_if %{bin-available:graph-easy}) + (action + (progn + (ignore-outputs + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) + (with-outputs-to %{target} + (run graph-easy --as=boxart arg.dot))))) + + (rule + (alias runtest) + (enabled_if %{bin-available:graph-easy}) + (action + (diff and_ambiguous_partition2.expected and_ambiguous_partition2.output)))) + +(subdir cfg/uncil + (rule + (deps + (sandbox always) ; must sandbox to prevent arg.dot-s from parallel runs from interfering + (package goblint) ; depend on entire goblint package for svcomp21 conf + (:c and_ambiguous_partition3.c) + (:prop %{project_root}/tests/sv-comp/unreach-call-__VERIFIER_error.prp)) + (target and_ambiguous_partition3.output) + (enabled_if %{bin-available:graph-easy}) + (action + (progn + (ignore-outputs + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) + (with-outputs-to %{target} + (run graph-easy --as=boxart arg.dot))))) + + (rule + (alias runtest) + (enabled_if %{bin-available:graph-easy}) + (action + (diff and_ambiguous_partition3.expected and_ambiguous_partition3.output)))) + +(subdir cfg/uncil + (rule + (deps + (sandbox always) ; must sandbox to prevent arg.dot-s from parallel runs from interfering + (package goblint) ; depend on entire goblint package for svcomp21 conf + (:c and_ambiguous_partition4.c) + (:prop %{project_root}/tests/sv-comp/unreach-call-__VERIFIER_error.prp)) + (target and_ambiguous_partition4.output) + (enabled_if %{bin-available:graph-easy}) + (action + (progn + (ignore-outputs + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) + (with-outputs-to %{target} + (run graph-easy --as=boxart arg.dot))))) + + (rule + (alias runtest) + (enabled_if %{bin-available:graph-easy}) + (action + (diff and_ambiguous_partition4.expected and_ambiguous_partition4.output)))) + (subdir cfg/uncil (rule (deps @@ -782,7 +914,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -804,7 +936,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -826,7 +958,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -848,7 +980,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -870,7 +1002,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -892,7 +1024,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -914,7 +1046,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -936,7 +1068,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) diff --git a/tests/sv-comp/gen/gen.ml b/tests/sv-comp/gen/gen.ml index a8ad72be67..796ae7a278 100644 --- a/tests/sv-comp/gen/gen.ml +++ b/tests/sv-comp/gen/gen.ml @@ -19,7 +19,7 @@ let generate_rule c_dir_file = (action (progn (ignore-outputs - (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %%{prop} %%{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %%{prop} %%{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit)) (with-outputs-to %%{target} (run graph-easy --as=boxart arg.dot)))))