diff --git a/tests/spec/loop_assigns_generated.ml b/tests/spec/loop_assigns_generated.ml index 603589b0445b135d0e1bebf29907649e9428a47b..9dcca735d36fbdc712753375bde33c1f8f2c9c26 100644 --- a/tests/spec/loop_assigns_generated.ml +++ b/tests/spec/loop_assigns_generated.ml @@ -1,11 +1,13 @@ open Cil_types -let e1 = Emitter.(create "test1" [ Code_annot ] [] []) -let e2 = Emitter.(create "test2" [ Code_annot ] [] []) +let e1 = Emitter.(create "emitter1" [ Code_annot ] [] []) +let e2 = Emitter.(create "emitter2" [ Code_annot ] [] []) let add_assigns e kf stmt v = let lv = Cil.cvar_to_lvar v in - let id_v = Logic_const.new_identified_term (Logic_const.tvar lv) in + let term_v = Logic_const.tvar lv in + let named_term_v = { term_v with term_name = ("added_by_"^(Emitter.get_name e))::term_v.term_name } in + let id_v = Logic_const.new_identified_term named_term_v in Annotations.add_code_annot e ~kf stmt (Logic_const.new_code_annotation (AAssigns ([], Writes [id_v, FromAny]))); diff --git a/tests/spec/oracle/loop_assigns_generated.res.oracle b/tests/spec/oracle/loop_assigns_generated.res.oracle index c3505d045ec9334bcd113e19a518b10fe060f5fb..1f7516a5f50c6e92898b966496db28efa8c6c473 100644 --- a/tests/spec/oracle/loop_assigns_generated.res.oracle +++ b/tests/spec/oracle/loop_assigns_generated.res.oracle @@ -5,7 +5,7 @@ void f(void) int k; int j; int i = 0; - /*@ loop assigns k, j, i; */ + /*@ loop assigns (added_by_emitter2: k), (added_by_emitter1: j), i; */ while (i < 10) i ++; return; }