Skip to content
Snippets Groups Projects
Commit 17172acc authored by Patrick Baudin's avatar Patrick Baudin Committed by Virgile Prevosto
Browse files

[tests] adds some traceability into the new test

parent 051da72d
No related branches found
No related tags found
No related merge requests found
open Cil_types open Cil_types
let e1 = Emitter.(create "test1" [ Code_annot ] [] []) let e1 = Emitter.(create "emitter1" [ Code_annot ] [] [])
let e2 = Emitter.(create "test2" [ Code_annot ] [] []) let e2 = Emitter.(create "emitter2" [ Code_annot ] [] [])
let add_assigns e kf stmt v = let add_assigns e kf stmt v =
let lv = Cil.cvar_to_lvar v in 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 Annotations.add_code_annot e ~kf stmt
(Logic_const.new_code_annotation (Logic_const.new_code_annotation
(AAssigns ([], Writes [id_v, FromAny]))); (AAssigns ([], Writes [id_v, FromAny])));
......
...@@ -5,7 +5,7 @@ void f(void) ...@@ -5,7 +5,7 @@ void f(void)
int k; int k;
int j; int j;
int i = 0; int i = 0;
/*@ loop assigns k, j, i; */ /*@ loop assigns (added_by_emitter2: k), (added_by_emitter1: j), i; */
while (i < 10) i ++; while (i < 10) i ++;
return; return;
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment