From 17172acc504c46b9febd4b69f48b38a5f868ad13 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 11 Jun 2020 15:04:53 +0200
Subject: [PATCH] [tests] adds some traceability into the new test
---
tests/spec/loop_assigns_generated.ml | 8 +++++---
tests/spec/oracle/loop_assigns_generated.res.oracle | 2 +-
2 files changed, 6 insertions(+), 4 deletions(-)
diff --git a/tests/spec/loop_assigns_generated.ml b/tests/spec/loop_assigns_generated.ml
index 603589b0445..9dcca735d36 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 c3505d045ec..1f7516a5f50 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;
}
--
GitLab