Merge branch 'feature/basile/standardize-init-clean' into 'master'

[eacsl] Standardize cleanup functions

See merge request frama-c/frama-c!2839

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

@@ -24,7 +24,7 @@ open Cil_types
 open Cil_datatype
 
 let function_init_name = Functions.RTL.mk_api_name "globals_init"
-let function_delete_name = Functions.RTL.mk_api_name "globals_delete"
+let function_clean_name = Functions.RTL.mk_api_name "globals_clean"
 
 (* Hashtable mapping global variables (as Cil_type.varinfo) to their
    initializers (if any).
@@ -186,10 +186,10 @@ let mk_init_function () =
   fundec.sbody.bstmts <- stmts;
   vi, fundec
 
-let mk_delete_function () =
-  (* Create and register [__e_acsl_globals_delete] function with definition
+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_delete_name in
+  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

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

@@ -27,8 +27,8 @@ open Cil_types
 val function_init_name: string
 (** Name of the function in which [mk_init_function] (see below) generates the
     code. *)
-val function_delete_name: string
-(** Name of the function in which [mk_delete_function] (see below) generates the
+val function_clean_name: string
+(** Name of the function in which [mk_clean_function] (see below) generates the
     code. *)
 
 val reset: unit -> unit
@@ -44,7 +44,7 @@ val mk_init_function: unit -> varinfo * fundec
 (** Generate a new C function containing the observers for global variable
     declarations and initializations. *)
 
-val mk_delete_function: unit -> varinfo * fundec
+val mk_clean_function: unit -> varinfo * fundec
 (** Generate a new C function containing the observers for global variable
     de-allocations. *)
 

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

@@ -707,8 +707,8 @@ 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_delete, fundec_delete = Global_observer.mk_delete_function () in
-    let cil_fct_delete = GFun(fundec_delete, Location.unknown) in
+    let vi_clean, fundec_clean = Global_observer.mk_clean_function () in
+    let cil_fct_clean = GFun(fundec_clean, Location.unknown) in
     match main with
     | Some main ->
       let mk_fct_call vi =
@@ -727,14 +727,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_delete =
-        match fundec_delete.sbody.bstmts with
+      let stmt_clean =
+        match fundec_clean.sbody.bstmts with
         | [] -> None
-        | _ -> Some (mk_fct_call vi_delete)
+        | _ -> Some (mk_fct_call vi_clean)
       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_delete;
+      surround_function_with main main_fundec stmt_init stmt_clean;
       (* Retrieve all globals except main *)
       let main_vi = Globals.Functions.get_vi main in
       let new_globals =
@@ -753,11 +753,11 @@ let inject_global_handler file main =
         in
         (* [main] at the end *)
         let globals_to_add = [ GFun(main_fundec, Location.unknown) ] in
-        (* Prepend [__e_acsl_globals_delete] if not empty *)
+        (* Prepend [__e_acsl_globals_clean] if not empty *)
         let globals_to_add =
-          match fundec_delete.sbody.bstmts with
+          match fundec_clean.sbody.bstmts with
           | [] -> globals_to_add
-          | _ -> cil_fct_delete :: globals_to_add
+          | _ -> cil_fct_clean :: globals_to_add
         in
         (* Prepend [__e_acsl_globals_init] *)
         let globals_to_add = cil_fct_init :: globals_to_add in
@@ -777,11 +777,11 @@ let inject_global_handler file main =
                       `__e_acsl_memory_init' and `__e_acsl_memory_clean' \
                       by yourself.@]"
         Global_observer.function_init_name
-        Global_observer.function_delete_name;
+        Global_observer.function_clean_name;
       let globals_func =
-        match fundec_delete.sbody.bstmts with
+        match fundec_clean.sbody.bstmts with
         | [] -> [ cil_fct_init ]
-        | _ -> [ cil_fct_init; cil_fct_delete ]
+        | _ -> [ cil_fct_init; cil_fct_clean ]
       in
       file.globals <- file.globals @ globals_func
 

src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c

@@ -272,7 +272,7 @@ void __e_acsl_globals_init(void)
   return;
 }
 
-void __e_acsl_globals_delete(void)
+void __e_acsl_globals_clean(void)
 {
   __e_acsl_delete_block((void *)(target));
   __e_acsl_delete_block((void *)(source));
@@ -286,7 +286,7 @@ int main(void)
   initialize(source,100);
   duffcopy(source,target,43);
   __retres = 0;
-  __e_acsl_globals_delete();
+  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }

src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c

@@ -53,7 +53,7 @@ void __e_acsl_globals_init(void)
   return;
 }
 
-void __e_acsl_globals_delete(void)
+void __e_acsl_globals_clean(void)
 {
   __e_acsl_delete_block((void *)(& global_i_ptr));
   __e_acsl_delete_block((void *)(& global_i));
@@ -66,7 +66,7 @@ int main(void)
   __e_acsl_globals_init();
   __gen_e_acsl_loop();
   __retres = 0;
-  __e_acsl_globals_delete();
+  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }

src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c

@@ -88,7 +88,7 @@ void __e_acsl_globals_init(void)
   return;
 }
 
-void __e_acsl_globals_delete(void)
+void __e_acsl_globals_clean(void)
 {
   __e_acsl_delete_block((void *)(& S));
 }
@@ -149,7 +149,7 @@ int main(void)
   }
   f();
   __retres = 0;
-  __e_acsl_globals_delete();
+  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }

src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c

@@ -31,7 +31,7 @@ void __e_acsl_globals_init(void)
   return;
 }
 
-void __e_acsl_globals_delete(void)
+void __e_acsl_globals_clean(void)
 {
   __e_acsl_delete_block((void *)(_G));
 }
@@ -60,7 +60,7 @@ int main(int argc, char **argv)
   }
   /*@ assert \valid_read(_G[0].str); */ ;
   __retres = 0;
-  __e_acsl_globals_delete();
+  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }

src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c

@@ -50,7 +50,7 @@ void __e_acsl_globals_init(void)
   return;
 }
 
-void __e_acsl_globals_delete(void)
+void __e_acsl_globals_clean(void)
 {
   __e_acsl_delete_block((void *)(& n));
 }
@@ -63,7 +63,7 @@ int main(int argc, char **argv)
   argc = __gen_e_acsl_atoi((char const *)n);
   a = argc;
   __retres = 0;
-  __e_acsl_globals_delete();
+  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }

src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c

@@ -24,7 +24,7 @@ void __e_acsl_globals_init(void)
   return;
 }
 
-void __e_acsl_globals_delete(void)
+void __e_acsl_globals_clean(void)
 {
   __e_acsl_delete_block((void *)(& t));
 }
@@ -40,7 +40,7 @@ int main(int argc, char **argv)
   t.j = (_Bool)1;
   /*@ assert \initialized(&t.j); */ ;
   tmp = test(& t);
-  __e_acsl_globals_delete();
+  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return tmp;
 }

src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c

@@ -14,7 +14,7 @@ void __e_acsl_globals_init(void)
   return;
 }
 
-void __e_acsl_globals_delete(void)
+void __e_acsl_globals_clean(void)
 {
   __e_acsl_delete_block((void *)(t));
 }
@@ -45,7 +45,7 @@ int main(void)
   /*@ assert \valid(&t[0 .. 9]); */ ;
   __retres = 0;
   __e_acsl_delete_block((void *)(& p));
-  __e_acsl_globals_delete();
+  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }

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

@@ -40,7 +40,7 @@ void __e_acsl_globals_init(void)
   return;
 }
 
-void __e_acsl_globals_delete(void)
+void __e_acsl_globals_clean(void)
 {
   __e_acsl_delete_block((void *)(& b));
   __e_acsl_delete_block((void *)(& a));
@@ -56,7 +56,7 @@ int main(void)
   __e_acsl_full_init((void *)(& __retres));
   __retres = 0;
   __e_acsl_delete_block((void *)(& __retres));
-  __e_acsl_globals_delete();
+  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }

src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c

@@ -16,7 +16,7 @@ void __e_acsl_globals_init(void)
   return;
 }
 
-void __e_acsl_globals_delete(void)
+void __e_acsl_globals_clean(void)
 {
   __e_acsl_delete_block((void *)(& P));
   __e_acsl_delete_block((void *)(& G));
@@ -74,7 +74,7 @@ int main(void)
   }
   __retres = 0;
   __e_acsl_delete_block((void *)(& q));
-  __e_acsl_globals_delete();
+  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }

src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c

@@ -2486,7 +2486,7 @@ void __e_acsl_globals_init(void)
   return;
 }
 
-void __e_acsl_globals_delete(void)
+void __e_acsl_globals_clean(void)
 {
   __e_acsl_delete_block((void *)(& __fc_p_time_tm));
   __e_acsl_delete_block((void *)(& __fc_time_tm));
@@ -6552,7 +6552,7 @@ int main(int argc, char const **argv)
   __retres = 0;
   __e_acsl_delete_block((void *)(& argc));
   __e_acsl_delete_block((void *)(& vptr));
-  __e_acsl_globals_delete();
+  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }

src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c

@@ -39,7 +39,7 @@ void __e_acsl_globals_init(void)
   return;
 }
 
-void __e_acsl_globals_delete(void)
+void __e_acsl_globals_clean(void)
 {
   __e_acsl_delete_block((void *)(& f));
 }
@@ -61,7 +61,7 @@ int main(void)
   __retres = 0;
   __e_acsl_delete_block((void *)(& x));
   __e_acsl_delete_block((void *)(& __retres));
-  __e_acsl_globals_delete();
+  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }

src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c

@@ -17,7 +17,7 @@ void __e_acsl_globals_init(void)
   return;
 }
 
-void __e_acsl_globals_delete(void)
+void __e_acsl_globals_clean(void)
 {
   __e_acsl_delete_block((void *)(& PA));
   __e_acsl_delete_block((void *)(A));
@@ -327,7 +327,7 @@ int main(void)
   __e_acsl_delete_block((void *)(& l));
   __e_acsl_delete_block((void *)(& pa));
   __e_acsl_delete_block((void *)(a));
-  __e_acsl_globals_delete();
+  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }

src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c

@@ -23,7 +23,7 @@ void __e_acsl_globals_init(void)
   return;
 }
 
-void __e_acsl_globals_delete(void)
+void __e_acsl_globals_clean(void)
 {
   __e_acsl_delete_block((void *)(& ZERO));
   __e_acsl_delete_block((void *)(& PA));
@@ -254,7 +254,7 @@ int main(void)
   __e_acsl_delete_block((void *)(& pa));
   __e_acsl_delete_block((void *)(a));
   __e_acsl_delete_block((void *)(& zero));
-  __e_acsl_globals_delete();
+  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }

src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c

@@ -16,7 +16,7 @@ void __e_acsl_globals_init(void)
   return;
 }
 
-void __e_acsl_globals_delete(void)
+void __e_acsl_globals_clean(void)
 {
   __e_acsl_delete_block((void *)(& B));
 }
@@ -161,7 +161,7 @@ int main(int argc, char **argv)
   __e_acsl_delete_block((void *)(& pmin));
   __e_acsl_delete_block((void *)(& b));
   __e_acsl_delete_block((void *)(& p));
-  __e_acsl_globals_delete();
+  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }

src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c

@@ -65,7 +65,7 @@ void __e_acsl_globals_init(void)
   return;
 }
 
-void __e_acsl_globals_delete(void)
+void __e_acsl_globals_clean(void)
 {
   __e_acsl_delete_block((void *)(_G));
   __e_acsl_delete_block((void *)(& _E));
@@ -187,7 +187,7 @@ int main(int argc, char **argv)
                   "tests/memory/compound_initializers.c",43);
   /*@ assert _G[0].num ≡ 99; */ ;
   __retres = 0;
-  __e_acsl_globals_delete();
+  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }

src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c

@@ -14,7 +14,7 @@ void __e_acsl_globals_init(void)
   return;
 }
 
-void __e_acsl_globals_delete(void)
+void __e_acsl_globals_clean(void)
 {
   __e_acsl_delete_block((void *)(& errno));
 }
@@ -45,7 +45,7 @@ int main(int argc, char const **argv)
   /*@ assert \valid(p); */ ;
   __retres = 0;
   __e_acsl_delete_block((void *)(& p));
-  __e_acsl_globals_delete();
+  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }

src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c

@@ -14,7 +14,7 @@ void __e_acsl_globals_init(void)
   return;
 }
 
-void __e_acsl_globals_delete(void)
+void __e_acsl_globals_clean(void)
 {
   __e_acsl_delete_block((void *)(array));
 }
@@ -82,7 +82,7 @@ int main(void)
   /*@ assert ¬\freeable(&array[5]); */ ;
   __retres = 0;
   __e_acsl_delete_block((void *)(& p));
-  __e_acsl_globals_delete();
+  __e_acsl_globals_clean();
   __e_acsl_memory_clean();
   return __retres;
 }