From 20c500fbec6504204a30e824916768105f3d9a18 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 24 Jan 2024 13:24:55 +0200 Subject: [PATCH 1/2] Exclude Goblint stubs from YAML witnesses --- src/witness/yamlWitness.ml | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 253ee5eecd..b7ec584dfb 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -193,15 +193,25 @@ struct in let task = Entry.task ~input_files ~data_model ~specification in + let is_stub_node n = + let fundec = Node.find_fundec n in + Cil.hasAttribute "goblint_stub" fundec.svar.vattr + in + let is_invariant_node (n : Node.t) = let loc = Node.location n in match n with - | Statement _ when not loc.synthetic && WitnessInvariant.is_invariant_node n -> true + | Statement _ when not loc.synthetic && WitnessInvariant.is_invariant_node n -> + not (is_stub_node n) | _ -> (* avoid FunctionEntry/Function, because their locations are not inside the function where asserts could be inserted *) false in + let is_loop_head_node n = + WitnessUtil.NH.mem WitnessInvariant.loop_heads n && not (is_stub_node n) + in + let local_lvals n local = if GobConfig.get_bool "witness.invariant.accessed" then ( match R.ask_local_node n ~local MayAccessed with @@ -277,7 +287,7 @@ struct let entries = if entry_type_enabled YamlWitnessType.LoopInvariant.entry_type then ( LH.fold (fun loc ns acc -> - if WitnessInvariant.emit_loop_head && List.exists (WitnessUtil.NH.mem WitnessInvariant.loop_heads) ns then ( + if WitnessInvariant.emit_loop_head && List.exists is_loop_head_node ns then ( let inv = List.fold_left (fun acc n -> let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) @@ -472,7 +482,7 @@ struct let invariants = if invariant_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then ( LH.fold (fun loc ns acc -> - if WitnessInvariant.emit_loop_head && List.exists (WitnessUtil.NH.mem WitnessInvariant.loop_heads) ns then ( + if WitnessInvariant.emit_loop_head && List.exists is_loop_head_node ns then ( let inv = List.fold_left (fun acc n -> let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) From 7e51d9a0630532bf4930c00f7863fff2fab35cd4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 7 Feb 2024 12:12:57 +0200 Subject: [PATCH 2/2] Refactor is_invariant_node in YamlWitness --- src/witness/yamlWitness.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index b7ec584dfb..d9d39ccee1 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -201,9 +201,9 @@ struct let is_invariant_node (n : Node.t) = let loc = Node.location n in match n with - | Statement _ when not loc.synthetic && WitnessInvariant.is_invariant_node n -> - not (is_stub_node n) - | _ -> + | Statement _ -> + not loc.synthetic && WitnessInvariant.is_invariant_node n && not (is_stub_node n) + | FunctionEntry _ | Function _ -> (* avoid FunctionEntry/Function, because their locations are not inside the function where asserts could be inserted *) false in