diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 1f83c8625e..1f106c936e 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -246,9 +246,7 @@ struct if entry_type_enabled YamlWitnessType.LocationInvariant.entry_type then ( LH.fold (fun loc ns acc -> if List.exists is_invariant_node ns then ( - let fundec = ref None in let inv = List.fold_left (fun acc n -> - fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in let lvals = local_lvals n local in Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) @@ -256,10 +254,11 @@ struct in match inv with | `Lifted inv -> + let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *) + let location_function = fundec.svar.vname in + let location = Entry.location ~location:loc ~location_function in let invs = WitnessUtil.InvariantExp.process_exp inv in List.fold_left (fun acc inv -> - let location_function = (Option.get !fundec).svar.vname in - let location = Entry.location ~location:loc ~location_function in let invariant = Entry.invariant (CilType.Exp.show inv) in let entry = Entry.location_invariant ~task ~location ~invariant in entry :: acc @@ -280,19 +279,18 @@ struct 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 ( - let fundec = ref None in let inv = List.fold_left (fun acc n -> - fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) 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 (||) *) ) (Invariant.bot ()) ns in match inv with | `Lifted inv -> + let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *) + let location_function = fundec.svar.vname in + let location = Entry.location ~location:loc ~location_function in let invs = WitnessUtil.InvariantExp.process_exp inv in List.fold_left (fun acc inv -> - let location_function = (Option.get !fundec).svar.vname in - let location = Entry.location ~location:loc ~location_function in let invariant = Entry.invariant (CilType.Exp.show inv) in let entry = Entry.loop_invariant ~task ~location ~invariant in entry :: acc @@ -443,9 +441,7 @@ struct if invariant_type_enabled YamlWitnessType.InvariantSet.LocationInvariant.invariant_type then ( LH.fold (fun loc ns acc -> if List.exists is_invariant_node ns then ( - let fundec = ref None in let inv = List.fold_left (fun acc n -> - fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in let lvals = local_lvals n local in Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) @@ -453,10 +449,11 @@ struct in match inv with | `Lifted inv -> + let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *) + let location_function = fundec.svar.vname in + let location = Entry.location ~location:loc ~location_function in let invs = WitnessUtil.InvariantExp.process_exp inv in List.fold_left (fun acc inv -> - let location_function = (Option.get !fundec).svar.vname in - let location = Entry.location ~location:loc ~location_function in let invariant = CilType.Exp.show inv in let invariant = Entry.location_invariant' ~location ~invariant in invariant :: acc @@ -477,19 +474,18 @@ struct 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 ( - let fundec = ref None in let inv = List.fold_left (fun acc n -> - fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) 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 (||) *) ) (Invariant.bot ()) ns in match inv with | `Lifted inv -> + let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *) + let location_function = fundec.svar.vname in + let location = Entry.location ~location:loc ~location_function in let invs = WitnessUtil.InvariantExp.process_exp inv in List.fold_left (fun acc inv -> - let location_function = (Option.get !fundec).svar.vname in - let location = Entry.location ~location:loc ~location_function in let invariant = CilType.Exp.show inv in let invariant = Entry.loop_invariant' ~location ~invariant in invariant :: acc