[eacsl] Fix generated `__e_acsl_globals_clean()`

The `__eacsl_globals_clean()` global function is only created if there
are globals variables. A `return;` statement is added at the end of the
function to satisfy Frama-C invariants.

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

@@ -187,20 +187,24 @@ let mk_init_function () =
   vi, fundec
 
 let mk_clean_function () =
-  (* Create and register [__e_acsl_globals_clean] function with definition
-     for de-allocation of global variables *)
-  let vi, fundec, _kf = mk_function function_clean_name in
-  (* Generate delete statements and add them to the function body *)
-  let stmts =
-    Varinfo.Hashtbl.fold_sorted
-      (fun vi _l acc ->
-         if Misc.is_fc_or_compiler_builtin vi then acc
-         else Smart_stmt.delete_stmt vi :: acc)
-      tbl
-      []
-  in
-  fundec.sbody.bstmts <- stmts;
-  vi, fundec
+  if Varinfo.Hashtbl.length tbl = 0 then
+    None
+  else
+    (* Create and register [__e_acsl_globals_clean] function with definition
+       for de-allocation of global variables *)
+    let vi, fundec, _kf = mk_function function_clean_name in
+    (* Generate delete statements and add them to the function body *)
+    let return = Cil.mkStmt ~valid_sid:true (Return (None, Location.unknown)) in
+    let stmts =
+      Varinfo.Hashtbl.fold_sorted
+        (fun vi _l acc ->
+           if Misc.is_fc_or_compiler_builtin vi then acc
+           else Smart_stmt.delete_stmt vi :: acc)
+        tbl
+        [return]
+    in
+    fundec.sbody.bstmts <- stmts;
+    Some (vi, fundec)
 
 (*
 Local Variables:

src/plugins/e-acsl/src/code_generator/global_observer.mli

@@ -44,9 +44,9 @@ val mk_init_function: unit -> varinfo * fundec
 (** Generate a new C function containing the observers for global variable
     declarations and initializations. *)
 
-val mk_clean_function: unit -> varinfo * fundec
+val mk_clean_function: unit -> (varinfo * fundec) option
 (** Generate a new C function containing the observers for global variable
-    de-allocations. *)
+    de-allocations if there are global variables. *)
 
 (*
 Local Variables:

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

@@ -710,8 +710,12 @@ let inject_global_handler file main =
     let vi_init, fundec_init = Global_observer.mk_init_function () in
     let cil_fct_init = GFun(fundec_init, Location.unknown) in
     (* Create [__e_acsl_globals_delete] function *)
-    let vi_clean, fundec_clean = Global_observer.mk_clean_function () in
-    let cil_fct_clean = GFun(fundec_clean, Location.unknown) in
+    let vi_and_fundec_clean_opt = Global_observer.mk_clean_function () in
+    let cil_fct_clean_opt =
+      Option.map
+        (fun (_, fundec_clean) -> GFun(fundec_clean, Location.unknown))
+        vi_and_fundec_clean_opt
+    in
     match main with
     | Some main ->
       let mk_fct_call vi =
@@ -730,14 +734,14 @@ let inject_global_handler file main =
       (* Create [__e_acsl_globals_init();] call *)
       let stmt_init = mk_fct_call vi_init in
       (* Create [__e_acsl_globals_delete();] call *)
-      let stmt_clean =
-        match fundec_clean.sbody.bstmts with
-        | [] -> None
-        | _ -> Some (mk_fct_call vi_clean)
+      let stmt_clean_opt =
+        Option.map
+          (fun (vi_clean, _) -> mk_fct_call vi_clean)
+          vi_and_fundec_clean_opt
       in
       (* Surround the content of main with the calls to
          [__e_acsl_globals_init();] and [__e_acsl_globals_delete();] *)
-      surround_function_with main main_fundec stmt_init stmt_clean;
+      surround_function_with main main_fundec stmt_init stmt_clean_opt;
       (* Retrieve all globals except main *)
       let main_vi = Globals.Functions.get_vi main in
       let new_globals =
@@ -758,9 +762,10 @@ let inject_global_handler file main =
         let globals_to_add = [ GFun(main_fundec, Location.unknown) ] in
         (* Prepend [__e_acsl_globals_clean] if not empty *)
         let globals_to_add =
-          match fundec_clean.sbody.bstmts with
-          | [] -> globals_to_add
-          | _ -> cil_fct_clean :: globals_to_add
+          Option.fold
+            ~none:globals_to_add
+            ~some:(fun cil_fct_clean -> cil_fct_clean :: globals_to_add)
+            cil_fct_clean_opt
         in
         (* Prepend [__e_acsl_globals_init] *)
         let globals_to_add = cil_fct_init :: globals_to_add in
@@ -782,9 +787,10 @@ let inject_global_handler file main =
         Global_observer.function_init_name
         Global_observer.function_clean_name;
       let globals_func =
-        match fundec_clean.sbody.bstmts with
-        | [] -> [ cil_fct_init ]
-        | _ -> [ cil_fct_init; cil_fct_clean ]
+        Option.fold
+          ~none:[ cil_fct_init ]
+          ~some:(fun cil_fct_clean -> [ cil_fct_init; cil_fct_clean ])
+          cil_fct_clean_opt
       in
       file.globals <- file.globals @ globals_func
 

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

+/* run.config_ci
+  COMMENT: frama-c/e-acsl#145, test for validity of globals_init and
+  globals_clean.
+  STDOPT: +"-verbose 1 -eva-print"
+*/
+int G = 0;
+
+int main(void) {
+  /*@ assert \valid(&G); */
+  int a = G;
+  return 0;
+}

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

+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+int G = 0;
+void __e_acsl_globals_init(void)
+{
+  static char __e_acsl_already_run = 0;
+  if (! __e_acsl_already_run) {
+    __e_acsl_already_run = 1;
+    __e_acsl_store_block((void *)(& G),(size_t)4);
+    __e_acsl_full_init((void *)(& G));
+  }
+  return;
+}
+
+void __e_acsl_globals_clean(void)
+{
+  __e_acsl_delete_block((void *)(& G));
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  __e_acsl_globals_init();
+  {
+    int __gen_e_acsl_valid;
+    __gen_e_acsl_valid = __e_acsl_valid((void *)(& G),sizeof(int),
+                                        (void *)(& G),(void *)0);
+    __e_acsl_assert(__gen_e_acsl_valid,"Assertion","main","\\valid(&G)",
+                    "tests/bts/issue-eacsl-145.c",9);
+  }
+  /*@ assert \valid(&G); */ ;
+  int a = G;
+  __retres = 0;
+  __e_acsl_globals_clean();
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+

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

+[kernel] Parsing tests/bts/issue-eacsl-145.c (with preprocessing)
+[e-acsl] beginning translation.
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
+[e-acsl] translation done in project "e-acsl".
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  G ∈ {0}
+  __e_acsl_heap_allocation_size ∈ [--..--]
+  __e_acsl_heap_allocated_blocks ∈ [--..--]
+  __fc_heap_status ∈ [--..--]
+  __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+  __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+  __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+  __e_acsl_init ∈ [--..--]
+[eva] using specification for function __e_acsl_memory_init
+[eva] using specification for function __e_acsl_store_block
+[eva] using specification for function __e_acsl_full_init
+[eva] using specification for function __e_acsl_valid
+[eva] using specification for function __e_acsl_assert
+[eva] using specification for function __e_acsl_delete_block
+[eva] using specification for function __e_acsl_memory_clean
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  5 functions analyzed (out of 5): 100% coverage.
+  In these functions, 27 statements reached (out of 27): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        1 valid     0 unknown     0 invalid      1 total
+    Preconditions     1 valid     0 unknown     0 invalid      1 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------