[eacsl:codegen] Update inject_in_block to support the new clean and delete globals placements

Since `memory_clean` and `delete_globals` are added after the calls to
`inject_in_block`, this function must be updated to add the free locals
statements as last statements of the innermost block instead of before
the `memory_clean` statement in the innermost block. Additionnaly, this
fix harmonize the treatment between a classic function and the function
`main()`, and fix the issue frama-c/e-acsl#105.

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

@@ -502,7 +502,21 @@ and inject_in_block (env: Env.t) kf blk =
   | [], _ :: _ | _ :: _, [] | _ :: _, _ :: _ ->
     (* [TODO] this piece of code could be improved *)
     (* de-allocate the memory blocks observing locals *)
-    let add_locals stmts =
+    let last_stmts ?return_stmt () =
+      let stmts =
+        match return_stmt with
+        | Some return_stmt ->
+          (* now that [free] stmts for [kf] have been inserted,
+             there is no more need to keep the corresponding entries in the
+             table managing them. *)
+          At_with_lscope.Free.remove_all kf;
+          (* The free statements are passed in the same order than the malloc
+             ones. In order to free the variable in the reverse order, the list
+             is reversed before appending the return statement. Moreover,
+             `rev_append` is tail recursive contrary to `append` *)
+          List.rev_append free_stmts [ return_stmt ]
+        | None -> []
+      in
       if Functions.instrument kf then
         List.fold_left
           (fun acc vi ->
@@ -515,28 +529,8 @@ and inject_in_block (env: Env.t) kf blk =
         stmts
     in
     (* select the precise location to inject these pieces of code *)
-    let rec insert_in_innermost_last_block blk = function
-      | { skind = Return _ } as ret :: ((potential_clean :: tl) as l) ->
-        (* keep the return (enclosed in a generated block) at the end;
-           preceded by clean if any *)
-        let init, tl =
-          if Kernel_function.is_main kf && Mmodel_analysis.use_model () then
-            free_stmts @ [ potential_clean; ret ], tl
-          else
-            free_stmts @ [ ret ], l
-        in
-        (* now that [free] stmts for [kf] have been inserted,
-           there is no more need to keep the corresponding entries in the
-           table managing them. *)
-        At_with_lscope.Free.remove_all kf;
-        blk.bstmts <-
-          List.fold_left (fun acc v -> v :: acc) (add_locals init) tl
-      | { skind = Block b } :: _ ->
-        insert_in_innermost_last_block b (List.rev b.bstmts)
-      | l ->
-        blk.bstmts <- List.fold_left (fun acc v -> v :: acc) (add_locals []) l
-    in
-    insert_in_innermost_last_block blk (List.rev blk.bstmts);
+    insert_as_last_stmts_in_innermost_block ~last_stmts kf blk ;
+    (* allocate the memory blocks observing locals *)
     if Functions.instrument kf then
       blk.bstmts <-
         List.fold_left

src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c

@@ -570,13 +570,13 @@ int main(void)
   __retres = 0;
   __e_acsl_delete_block((void *)(t));
   __e_acsl_delete_block((void *)(& n));
-  free((void *)__gen_e_acsl_at_7);
-  free((void *)__gen_e_acsl_at_6);
-  free((void *)__gen_e_acsl_at_5);
-  free((void *)__gen_e_acsl_at_4);
-  free((void *)__gen_e_acsl_at_3);
-  free((void *)__gen_e_acsl_at_2);
   free((void *)__gen_e_acsl_at);
+  free((void *)__gen_e_acsl_at_2);
+  free((void *)__gen_e_acsl_at_3);
+  free((void *)__gen_e_acsl_at_4);
+  free((void *)__gen_e_acsl_at_5);
+  free((void *)__gen_e_acsl_at_6);
+  free((void *)__gen_e_acsl_at_7);
   __e_acsl_memory_clean();
   return __retres;
 }
@@ -706,10 +706,10 @@ void __gen_e_acsl_f(int *t)
                     "\\let m = 4; \\old(*(t + m) == -4) && \\old(*(t + (m - 4))) == 9",
                     "tests/arith/at_on-purely-logic-variables.c",8);
     __e_acsl_delete_block((void *)(& t));
-    free((void *)__gen_e_acsl_at_4);
-    free((void *)__gen_e_acsl_at_3);
-    free((void *)__gen_e_acsl_at_2);
     free((void *)__gen_e_acsl_at);
+    free((void *)__gen_e_acsl_at_2);
+    free((void *)__gen_e_acsl_at_3);
+    free((void *)__gen_e_acsl_at_4);
     return;
   }
 }

src/plugins/e-acsl/tests/bts/issue-eacsl-105.c

+/* run.config
+   COMMENT: frama-c/e-acsl#105, test for delete block before exiting the 
+    function in the presence of early return.
+*/
+
+int f() {
+  int a = 10;
+  goto lbl_1;
+
+ lbl_2:
+  /*@ assert \valid(&a); */
+  return 0;
+
+ lbl_1:
+  goto lbl_2;
+}
+
+int main(void) {
+  f();
+  return 0;
+}

src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-105.c

+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+int f(void)
+{
+  int __retres;
+  int a = 10;
+  __e_acsl_store_block((void *)(& a),(size_t)4);
+  __e_acsl_full_init((void *)(& a));
+  goto lbl_1;
+  lbl_2:
+  /*@ assert \valid(&a); */
+  {
+    int __gen_e_acsl_valid;
+    __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int),
+                                        (void *)(& a),(void *)0);
+    __e_acsl_assert(__gen_e_acsl_valid,"Assertion","f","\\valid(&a)",
+                    "tests/bts/issue-eacsl-105.c",11);
+  }
+  __retres = 0;
+  goto return_label;
+  lbl_1: goto lbl_2;
+  return_label: {
+                  __e_acsl_delete_block((void *)(& a));
+                  return __retres;
+                }
+}
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  f();
+  __retres = 0;
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+

src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-105.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".

src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-105.res.oracle

+[kernel] Parsing tests/bts/issue-eacsl-105.c (with preprocessing)