diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.ml b/src/plugins/e-acsl/src/code_generator/global_observer.ml
index 352152f2c2a83846935cd323e03bf0838cf5fb99..6ee21213ec0f84eefeec8ec96431d438e48f836f 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.ml
+++ b/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:
diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.mli b/src/plugins/e-acsl/src/code_generator/global_observer.mli
index e37f39301d3515e52be12305f3505d6797eae8c6..de355a0efc90b637caa0253f59ea6e93fee502f2 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.mli
+++ b/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:
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index acae30bc013eeaf62599ee7ba2617d39e26fcba4..f095fa81d2cf4144cf04e60d98175a71b82b5bda 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/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
diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-145.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-145.c
new file mode 100644
index 0000000000000000000000000000000000000000..dde2d2aed6d86286c36c65a36223e36f2132880d
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-145.c
@@ -0,0 +1,12 @@
+/* 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;
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c
index be6316c86be622b7091172ee88711dbc77e3c620..02552add425756b02c26807c25d7ffb1cac95659 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c
@@ -276,6 +276,7 @@ void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(target));
__e_acsl_delete_block((void *)(source));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c
index 8597f7d23ee7d071eda0d71e93d5f6a31b63d6ae..6c2d67be53715e7a5d784fd50bc381f5d4907df3 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c
@@ -57,6 +57,7 @@ void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& global_i_ptr));
__e_acsl_delete_block((void *)(& global_i));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c
index fc9046840ed4ca86df28bb7a865d2e7edc1ae2b7..3cf6adc6f02ac52fe708175c49057a05fa940204 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c
@@ -91,6 +91,7 @@ void __e_acsl_globals_init(void)
void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& S));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c
index 0786c95e01ee021b0812c0200cf26953106efdbb..67003d8a70d3b79b29cedb5364bb28061ea60fb9 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c
@@ -34,6 +34,7 @@ void __e_acsl_globals_init(void)
void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(_G));
+ return;
}
int main(int argc, char **argv)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
index 5ade9142b8f3038322176beddc25f6e675b371f6..5c8f2b5dde78060dfa54b8f79ab6df8a7c8cc91f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
@@ -53,6 +53,7 @@ void __e_acsl_globals_init(void)
void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& n));
+ return;
}
int main(int argc, char **argv)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c
index 2ce056ec2aefa8069a191eef62e02a29706b39cf..327af999d255e34319a0073d8f6157c59a7cc582 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c
@@ -27,6 +27,7 @@ void __e_acsl_globals_init(void)
void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& t));
+ return;
}
int main(int argc, char **argv)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
index 08f3b321a24ee68353bd2d629d1f6859c1458c26..827fce50a41bf6c3b06f32547deb8bfe1754ca2e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
@@ -17,6 +17,7 @@ void __e_acsl_globals_init(void)
void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(t));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-145.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-145.c
new file mode 100644
index 0000000000000000000000000000000000000000..7382aae832390fa4f238bd22d1c5753777fdbe85
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-145.c
@@ -0,0 +1,42 @@
+/* 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;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c
index c3248c722e31367998e848cf0df89ea8db9c7fd4..b83e193f02ff582da79def45864e71198e617a07 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c
@@ -44,6 +44,7 @@ void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& b));
__e_acsl_delete_block((void *)(& a));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-145.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-145.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..73cc9ba6ba110276500aff04912bcc3028097845
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-145.res.oracle
@@ -0,0 +1,39 @@
+[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.
+ ----------------------------------------------------------------------------
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-145.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-145.e-acsl.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c
index d1e84e229ba0f4ce85097cf6267cb5637fd10bda..b6332376af73055adfbe8867b1711754b22783c1 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c
@@ -20,6 +20,7 @@ void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& P));
__e_acsl_delete_block((void *)(& G));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c
index 09554f35c6239bf11140f87b8473afb363a08eaf..084b8d80b0b70f0e187479c626ebfae990014a28 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c
@@ -2558,6 +2558,7 @@ void __e_acsl_globals_clean(void)
__e_acsl_delete_block((void *)(& valid_specifiers));
__e_acsl_delete_block((void *)(& __fc_p_time_tm));
__e_acsl_delete_block((void *)(& __fc_time_tm));
+ return;
}
int main(int argc, char const **argv)
diff --git a/src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c
index 8b38c74f47adf8a8dee1af80e6cf8e50eee56625..a8dbdfefe43c11e564c98d33b80eaab44e20a8bb 100644
--- a/src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c
@@ -42,6 +42,7 @@ void __e_acsl_globals_init(void)
void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& f));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c
index b831f777ef00fa9aca954755f319d46fe0dc2666..378a05448ddcad596a447595e78776e7f72d7b93 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c
@@ -21,6 +21,7 @@ void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& PA));
__e_acsl_delete_block((void *)(A));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c
index cec16f53eafcf4bdda73c28cfd23e9f84a52f914..167233407cad6d69ab1621e17806184c46a1a937 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c
@@ -28,6 +28,7 @@ void __e_acsl_globals_clean(void)
__e_acsl_delete_block((void *)(& ZERO));
__e_acsl_delete_block((void *)(& PA));
__e_acsl_delete_block((void *)(A));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c
index 33dd06e7f2d63264ef03f86307f95d511ccaa216..4f427bb14ad5288673fba5701c07dcffb87b5937 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c
@@ -19,6 +19,7 @@ void __e_acsl_globals_init(void)
void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& B));
+ return;
}
int main(int argc, char **argv)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
index ab6e1941648571820ef95453bb48dd5f1411e4a0..f8af717e7fc9df4d1b7eb04fc1bd52cc5b60962e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
@@ -74,6 +74,7 @@ void __e_acsl_globals_clean(void)
__e_acsl_delete_block((void *)(& _B));
__e_acsl_delete_block((void *)(_A));
__e_acsl_delete_block((void *)(& _F));
+ return;
}
int main(int argc, char **argv)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
index 66d885e493a78e17c9156d5739888910c1afa127..95604146d2919167711fa1e940d76c19284c76c8 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
@@ -17,6 +17,7 @@ void __e_acsl_globals_init(void)
void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& errno));
+ return;
}
int main(int argc, char const **argv)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c
index ab2185597f8b3aed26adfc4e8b2bd9cf0e3dc130..5ec1eaf5bca0f14146c818fd8260405b02da7234 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c
@@ -17,6 +17,7 @@ void __e_acsl_globals_init(void)
void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(array));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c
index aa5bc854da21cdcd0906771fb6acfb7d15550196..3c3305ed098b3183adb1a506f537556d888581b2 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c
@@ -16,6 +16,7 @@ void __e_acsl_globals_init(void)
void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& a));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c
index c4eb1d146e11ff56d96023a62831c6a24bb837d1..30203990a805d527ac9cf3fb2587a1895b82d9d1 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c
@@ -20,6 +20,7 @@ void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& b));
__e_acsl_delete_block((void *)(& a));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
index dec94db6533f1ddb8db1ab53e6913dab01393817..7359bae6a17a8d5d64d528e7bfde1ee9204c8933 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
@@ -21,6 +21,7 @@ void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& B));
__e_acsl_delete_block((void *)(& A));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c
index 3fc0d11efa059b157cbf14f9651a0a2f1e537244..133b539e51077488090cd319cc47ad04983e1a31 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c
@@ -89,6 +89,7 @@ void __e_acsl_globals_clean(void)
__e_acsl_delete_block((void *)(& S2));
__e_acsl_delete_block((void *)(& S));
__e_acsl_delete_block((void *)(& T));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c
index bae0a76865527daf719714166599c90ca4e9e9ee..946ce35b05636f8bdb682530c16f0ce766d03438 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c
@@ -26,6 +26,7 @@ void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& p));
__e_acsl_delete_block((void *)(& X));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c
index 90041c6e180ce1b6859a7d80e14f3777f8ec0bb7..efd908b7a93b22ffcdd486e0659408667d8beb26 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c
@@ -21,6 +21,7 @@ void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& PA));
__e_acsl_delete_block((void *)(A));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c
index 9f802d1b7fc773bb191e1f1d442744a2754b3540..94cdae153a181cff156ba55e8223e7091c513b33 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c
@@ -37,6 +37,7 @@ void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& B));
__e_acsl_delete_block((void *)(& A));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
index 63d1db28971baba9550159fcbfd0c46ef6b54c54..b127d652e3c261085c526cce4d62b012f04afb29 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
@@ -21,6 +21,7 @@ void __e_acsl_globals_clean(void)
__e_acsl_delete_block((void *)(& stdout));
__e_acsl_delete_block((void *)(& stdin));
__e_acsl_delete_block((void *)(& stderr));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c
index 872f31b112b4b253e3ac9a0ba3499fd144e6d262..5a651806a48c3bce2482ba35ec1fbe0fa68b50fd 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c
@@ -142,6 +142,7 @@ void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& Z));
__e_acsl_delete_block((void *)(& X));
+ return;
}
int main(void)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
index 8b6f8a3517a3a9c0557baaca1779ba4708b3b1d6..2d5749303a26b15e1ab2b9436ba2ec3a98e23413 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
@@ -62,6 +62,7 @@ void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(Vertices2));
__e_acsl_delete_block((void *)(Vertices));
+ return;
}
int main(int argc, char const **argv)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c
index a0774cc34295c87a5a34d639ba0140cec590ddc5..e3bf8c116eb8f54b52216bf9adfeb4768712746b 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c
@@ -21,6 +21,7 @@ void __e_acsl_globals_init(void)
void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(& foo));
+ return;
}
int main(int argc, char const **argv)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c
index c91eca2c10152d43084174f55903cdc2d34618b6..4b7cbfa0412ae5e8e90dab852b2c2ac16699135c 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c
@@ -118,6 +118,7 @@ void __e_acsl_globals_clean(void)
__e_acsl_delete_block((void *)(& l_desc));
__e_acsl_delete_block((void *)(extra_lbits));
__e_acsl_delete_block((void *)(strings));
+ return;
}
int main(int argc, char const **argv)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
index 1b6b3cd7af3b988453828e9ba7090dda85407203..6086892d5bdee7c9945bfd2b78882ecdef0c16a0 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
@@ -110,6 +110,7 @@ void __e_acsl_globals_clean(void)
{
__e_acsl_delete_block((void *)(Str));
__e_acsl_delete_block((void *)(Strings));
+ return;
}
int main(int argc, char const **argv)