diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 846b909f021aef97bbcb0761d6dceeb906f77089..fa4dbd4f4abde2c118f0def338e392cc02cc23f8 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2017/02/17] Fix bug with goto which points to a labeled
+ statement which must be instrumented.
-* E-ACSL [2017/01/23] Fix bug #2252 about pointer arithmetic with
negative offsets.
-* E-ACSL [2017/01/23] Fix bug with typing of unary and binary
diff --git a/src/plugins/e-acsl/label.ml b/src/plugins/e-acsl/label.ml
index 2e1cedd931c1aca6958fc52663de4e3a082d6bfe..bef275d6776f7537ecf22a1686c3af14fb687787 100644
--- a/src/plugins/e-acsl/label.ml
+++ b/src/plugins/e-acsl/label.ml
@@ -46,11 +46,26 @@ let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
new_stmt.labels <- labels @ new_stmt.labels;
Labeled_stmts.add old new_stmt;
(* update the gotos of the function jumping to one of the labels *)
- let o = object
+ let o orig_stmt = object
inherit Visitor.frama_c_inplace
- method !vstmt_aux s = match s.skind with
- | Goto(s_ref, _) ->
- if Cil_datatype.Stmt.equal !s_ref old then s_ref := new_stmt;
+ (* invariant of this method: [s = Cil.memo_stmt vis#behavior orig_stmt] *)
+ method !vstmt_aux s = match s.skind, orig_stmt.skind with
+ | Goto(s_ref, loc), Goto(orig_ref, _) ->
+ if Cil_datatype.Stmt.equal !s_ref old then
+ if s_ref == orig_ref then
+ (* The memo_stmt and its origin [orig_stmt] contain a shared
+ reference because [orig_stmt] has not yet been visited by [vis]
+ (forward goto). Consequently, do not modify the ref directly but
+ replace the corresponding stmt in the memoisation table. When
+ [orig_stmt] will be visited, the visitor will automatically
+ substitute it with the updated stmt. *)
+ Cil.set_stmt vis#behavior
+ orig_stmt
+ { s with skind = Goto(ref new_stmt, loc) }
+ else
+ (* Backward goto: it has already been visited and there is no more
+ sharing. Directly update the reference. *)
+ s_ref := new_stmt;
Cil.SkipChildren
| _ -> Cil.DoChildren
(* improve efficiency: skip childrens which cannot contain any label *)
@@ -60,7 +75,7 @@ let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
end in
let f = Extlib.the vis#current_func in
let mv_labels s =
- ignore (Visitor.visitFramacStmt o (Cil.memo_stmt vis#behavior s))
+ ignore (Visitor.visitFramacStmt (o s) (Cil.memo_stmt vis#behavior s))
in
List.iter mv_labels f.sallstmts
diff --git a/src/plugins/e-acsl/tests/runtime/goto.c b/src/plugins/e-acsl/tests/runtime/goto.c
new file mode 100644
index 0000000000000000000000000000000000000000..9369b871b5a9e886f1c485ff19ff4020009bc910
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/goto.c
@@ -0,0 +1,17 @@
+/* run.config
+ COMMENT: check a fix of a bug which occured when a [full_init] stmt is
+ COMMENT: generated for a labeled statement which a goto points to.
+ COMMENT: test both backward and forward gotos.
+*/
+
+char a;
+
+int main(void) {
+ char *b;
+ goto _LOR;
+ _LOR: b = &a;
+ if (a) goto _LOR; // dead code in order to prevent infinite loop
+ // but still meaningfull in term of code generated by E-ACSL
+ /*@ assert \initialized(b); */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_goto.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_goto.c
new file mode 100644
index 0000000000000000000000000000000000000000..7f90eb4d89b496cf3196712cc0c45062eb456ba4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_goto.c
@@ -0,0 +1,38 @@
+/* Generated by Frama-C */
+#include "stdlib.h"
+char a;
+void __e_acsl_globals_init(void)
+{
+ __e_acsl_store_block((void *)(& a),(size_t)1);
+ __e_acsl_full_init((void *)(& a));
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ char *b;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_globals_init();
+ __e_acsl_store_block((void *)(& b),(size_t)8);
+ goto _LOR;
+ _LOR: __e_acsl_full_init((void *)(& b));
+ b = & a;
+ if (a) goto _LOR;
+ /*@ assert \initialized(b); */
+ {
+ {
+ int __gen_e_acsl_initialized;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)b,sizeof(char));
+ __e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",
+ (char *)"main",(char *)"\\initialized(b)",15);
+ }
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& a));
+ __e_acsl_delete_block((void *)(& b));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/goto.err.oracle b/src/plugins/e-acsl/tests/runtime/oracle/goto.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/goto.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/goto.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a0a8836bb7a329fc53da2da239850fee8b952dde
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/oracle/goto.res.oracle
@@ -0,0 +1,4 @@
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+[e-acsl] translation done in project "e-acsl".
+FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 2a76fd3872c10d5bf640501100b1143ed2d99cf3..dc9997ed37d194ff5427f6819e16a43de98bdcec 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -632,13 +632,18 @@ you must call function `__e_acsl_memory_init` by yourself.@]";
Printer.pp_lval checked_lv
(not (may_safely_ignore assigned_lv))
(Pre_analysis.must_model_lval ~kf ~stmt checked_lv);*)
- if not (may_safely_ignore assigned_lv) &&
+ if not (may_safely_ignore assigned_lv) &&
Mmodel_analysis.must_model_lval ~kf ~stmt checked_lv
then
let new_stmt =
- Misc.mk_debug_mmodel_stmt (Misc.mk_initialize loc assigned_lv)
+ (* must be in the new project to build a new stmt *)
+ Project.on
+ prj
+ Misc.mk_debug_mmodel_stmt
+ (Misc.mk_initialize loc assigned_lv)
in
let before = Cil.memo_stmt self#behavior stmt in
+ let new_stmt = Cil.memo_stmt self#behavior new_stmt in
function_env := Env.add_stmt ~before !function_env new_stmt
method !vinst = function