[e-acsl:archi] fix bug with switch

src/plugins/e-acsl/src/code_generator/injector.ml

@@ -365,15 +365,8 @@ let rec inject_in_substmt env kf stmt = match stmt.skind with
     If(e, blk1, blk2, loc), env
 
   | Switch(e, blk, stmts, loc) ->
+    (* [blk] and [stmts] are visited at the same time *)
     let env = inject_in_block env kf blk in
-    let stmts, env =
-      List.fold_left
-        (fun (stmts, env) stmt ->
-           let stmt, env = inject_in_stmt env kf stmt in
-           stmt :: stmts, env)
-        ([], env)
-        stmts
-    in
     let e, env = replace_literal_string_in_exp env (Some kf) e in
     Switch(e, blk, stmts, loc), env
 

src/plugins/e-acsl/src/project_initializer/keep_status.ml

@@ -141,18 +141,22 @@ let must_translate kf kind =
     let kind', keep =
       try Datatype.Int.Map.find info.cpt info.statuses
       with Not_found ->
-        Options.fatal "[keep_status] unbound annotation (id %d)" info.cpt
+        Options.fatal "[keep_status] unbound annotation (id %d)@ in function %a"
+          info.cpt
+          Kernel_function.pretty kf
     in
     (* check kind consistency in order to detect more abnormal behaviors *)
     if kind <> kind' then
-      Options.fatal "[keep_status] incorrect kind '%a' (expected: '%a')"
+      Options.fatal
+        "[keep_status] incorrect kind '%a' (expected: '%a')@ in function %a"
         pretty_kind kind
-        pretty_kind kind';
+        pretty_kind kind'
+        Kernel_function.pretty kf;
     keep
     with Not_found -> true
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)

src/plugins/e-acsl/tests/memory/early_exit.c

@@ -19,8 +19,8 @@ L:
   return 0;
 }
 
-/* Make sure that when `goto` jumps over several scopes all locals
- * from those scopes are removed. */
+/* Make sure that, when 'goto' jumps over several scopes,
+   all locals from those scopes are removed. */
 int goto_valid() {
   int a = 9;
   int *p, *q, *r;
@@ -41,14 +41,14 @@ int goto_valid() {
       }
     }
 FIRST:
-    /* At this point `a1` is still in scope, while `a2` and `a3` are not, thus
-     * `q` and `r` become invalid, whereas `p` is still valid. */
+    /* at this point 'a1' is still in scope, while 'a2' and 'a3 are not,
+       thus 'q' and 'r' become invalid, whereas 'p' is still valid. */
     /*@ assert   \valid(p); */
     /*@ assert ! \valid(q); */
     /*@ assert ! \valid(r); */
-    /* The following `goto` invalidates `p`. */
+    /* the following 'goto' invalidates 'p' */
     goto SECOND;
-    /* Dead code */
+    /* dead code */
     p = r = q = &a;
   }
 
@@ -60,7 +60,7 @@ SECOND:
 }
 
 /* Make sure that when a break statement is executed within a switch statement
- * then all local variables declared within that switch are removed. */
+   then all local variables declared within that switch are removed. */
 int switch_valid() {
   int i = 1;
   int *p, *q, *s;
@@ -78,12 +78,12 @@ int switch_valid() {
           /*@ assert \valid(s); */
           break;
         }
-        /* Dead code */
+        /* dead code */
         p = q = &i;
         s = (void*)0;
       }
     }
-    /* Break invalidates `p` and `q` but `s` is still in scope. */
+    /* [break] invalidates 'p' and 'q' but 's' is still in scope. */
     /*@ assert ! \valid(q); */
     /*@ assert ! \valid(p); */
     /*@ assert \valid(s); */
@@ -120,8 +120,8 @@ int while_valid() {
   return 0;
 }
 
-/* Make sure that when `continue` is executed then local variables in scope
- * are not recorded twice. */
+/* Make sure that when [continue] is executed, then local variables in scope
+   are not recorded twice. */
 void continue_valid() {
   int i = 0;
   int *p, *q;