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 023dd1cfc9de35ef187803485bfe157e36dfd759..c53604fc55ff57a738d6725e1c0731cef0104453 100644 --- a/src/plugins/e-acsl/src/code_generator/global_observer.ml +++ b/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 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 fa18ebead123e6af2c21ddad05e397417daa1c56..e37f39301d3515e52be12305f3505d6797eae8c6 100644 --- a/src/plugins/e-acsl/src/code_generator/global_observer.mli +++ b/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. *) diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml index c7ea8438a11895d3bfe22dcb14b0b5f4d4b4764d..36c62ebc2dde11aca0c178a12e4728b517068c22 100644 --- a/src/plugins/e-acsl/src/code_generator/injector.ml +++ b/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 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 8131e10a3bd632923d333eae81fc18b92ed19afe..be6316c86be622b7091172ee88711dbc77e3c620 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 @@ -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; } 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 93c920650cd3172b3813c8c37b94f6c06de89f98..8597f7d23ee7d071eda0d71e93d5f6a31b63d6ae 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 @@ -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; } 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 bc80c8d28dca93ea1fbc338769c80432ac8be614..fc9046840ed4ca86df28bb7a865d2e7edc1ae2b7 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 @@ -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; } 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 ee4442c59fd67c3ed332ea822f1eb11d1825545f..0786c95e01ee021b0812c0200cf26953106efdbb 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 @@ -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; } 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 b8f3d27191812e698cc095efcd9f8ac24f29033a..5ade9142b8f3038322176beddc25f6e675b371f6 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 @@ -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; } 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 634afea64aeca153816808a03ca37aa56f2d6fea..2ce056ec2aefa8069a191eef62e02a29706b39cf 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 @@ -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; } 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 0c331aeb3b66bc2c15a76c77b9373c2b0935d525..3c48bb9e56162ba5522dfccc4ab3b1564e640cad 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 @@ -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; } 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 33c2861770404d56bcb16081bf8189028ee28a47..c3248c722e31367998e848cf0df89ea8db9c7fd4 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 @@ -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; } 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 89cee38a6d7bd88fdee0c4b405888bf0d7f15956..d1e84e229ba0f4ce85097cf6267cb5637fd10bda 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 @@ -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; } 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 e5b082351a5170c1e916b87a198f257a9341d039..74db87f2f2cf38f6ea5fde6db54d0c38cdf73c16 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 @@ -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; } 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 3d27c36ba8de272b81fa91f56270861049922dad..8b38c74f47adf8a8dee1af80e6cf8e50eee56625 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 @@ -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; } 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 9927263df1e1fec8e896f400960815d7d4e1a612..b831f777ef00fa9aca954755f319d46fe0dc2666 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 @@ -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; } 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 70135545c5ca8b7ff92943720cac1f45dfa7c96a..cec16f53eafcf4bdda73c28cfd23e9f84a52f914 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 @@ -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; } 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 44cb0bfe5031c10ce9a505834988481998a85b6f..33dd06e7f2d63264ef03f86307f95d511ccaa216 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 @@ -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; } 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 96bcfdbdcdf34552bad0243ce6717143c9ecc0d9..ab6e1941648571820ef95453bb48dd5f1411e4a0 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 @@ -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; } 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 f38474ba466e667532e9d52c1e92653513013858..66d885e493a78e17c9156d5739888910c1afa127 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 @@ -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; } 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 06eabe4d9f0fe10af383b73f7f4a3f1019f0b296..ab2185597f8b3aed26adfc4e8b2bd9cf0e3dc130 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 @@ -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; } 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 4e033175d14ddbd54c706f56c571b3f131cde53e..aa5bc854da21cdcd0906771fb6acfb7d15550196 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 @@ -13,7 +13,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 *)(& a)); } @@ -40,7 +40,7 @@ int main(void) /*@ assert \initialized(b); */ ; __retres = 0; __e_acsl_delete_block((void *)(& b)); - __e_acsl_globals_delete(); + __e_acsl_globals_clean(); __e_acsl_memory_clean(); return __retres; } 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 c063f126339e5b511cd94963ae48f84f98c2a6e8..c4eb1d146e11ff56d96023a62831c6a24bb837d1 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 @@ -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)); __e_acsl_delete_block((void *)(& a)); @@ -53,7 +53,7 @@ int main(void) __retres = 0; __e_acsl_delete_block((void *)(& q)); __e_acsl_delete_block((void *)(& p)); - __e_acsl_globals_delete(); + __e_acsl_globals_clean(); __e_acsl_memory_clean(); return __retres; } 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 50566fb3407c6f21b57ddcd6cb35f96da4b686aa..2fc7f4ff02452f9cf5ec262dc1a11a7dff556df0 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 @@ -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 *)(& B)); __e_acsl_delete_block((void *)(& A)); @@ -366,7 +366,7 @@ int main(void) __e_acsl_delete_block((void *)(& a)); __e_acsl_delete_block((void *)(& q)); __e_acsl_delete_block((void *)(& p)); - __e_acsl_globals_delete(); + __e_acsl_globals_clean(); __e_acsl_memory_clean(); return __retres; } 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 8710dc8c59571250e10b104fbcb998b2d919b716..3fc0d11efa059b157cbf14f9651a0a2f1e537244 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 @@ -82,7 +82,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 *)(& l_str)); __e_acsl_delete_block((void *)(& s_str)); @@ -148,7 +148,7 @@ int main(void) l_str ++; __retres = 0; __e_acsl_delete_block((void *)(& SS)); - __e_acsl_globals_delete(); + __e_acsl_globals_clean(); __e_acsl_memory_clean(); return __retres; } 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 508da20bd2bdfc7fe35da252a666b3f3a5dd159f..bae0a76865527daf719714166599c90ca4e9e9ee 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 @@ -22,7 +22,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 *)(& X)); @@ -35,7 +35,7 @@ int main(void) __e_acsl_globals_init(); f(); __retres = 0; - __e_acsl_globals_delete(); + __e_acsl_globals_clean(); __e_acsl_memory_clean(); return __retres; } 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 a294b87c0249b45f73ddee723818982f93756dab..90041c6e180ce1b6859a7d80e14f3777f8ec0bb7 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 @@ -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)); @@ -221,7 +221,7 @@ int main(void) __e_acsl_delete_block((void *)(& pl)); __e_acsl_delete_block((void *)(& l)); __e_acsl_delete_block((void *)(a)); - __e_acsl_globals_delete(); + __e_acsl_globals_clean(); __e_acsl_memory_clean(); return __retres; } 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 7437d4c8785aee9fcf9a93441856365517afacf0..9f802d1b7fc773bb191e1f1d442744a2754b3540 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 @@ -33,7 +33,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)); @@ -69,7 +69,7 @@ int main(void) __retres = 0; __e_acsl_delete_block((void *)(& y)); __e_acsl_delete_block((void *)(& x)); - __e_acsl_globals_delete(); + __e_acsl_globals_clean(); __e_acsl_memory_clean(); return __retres; } 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 225763b343eb67778691e0351f5045a2cd513d96..63d1db28971baba9550159fcbfd0c46ef6b54c54 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 @@ -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 *)(& stdout)); __e_acsl_delete_block((void *)(& stdin)); @@ -53,7 +53,7 @@ int main(void) } /*@ assert \valid(__fc_stdout); */ ; __retres = 0; - __e_acsl_globals_delete(); + __e_acsl_globals_clean(); __e_acsl_memory_clean(); return __retres; } 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 133ae6895b7de3536fda0f7074a18a5b1f8e8bcf..872f31b112b4b253e3ac9a0ba3499fd144e6d262 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 @@ -138,7 +138,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 *)(& Z)); __e_acsl_delete_block((void *)(& X)); @@ -533,7 +533,7 @@ int main(void) __e_acsl_delete_block((void *)(& c)); __e_acsl_delete_block((void *)(& b)); __e_acsl_delete_block((void *)(& a)); - __e_acsl_globals_delete(); + __e_acsl_globals_clean(); __e_acsl_memory_clean(); return __retres; } 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 39664bb15a905d77a0a77b801a6851fd367fb13b..8b6f8a3517a3a9c0557baaca1779ba4708b3b1d6 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 @@ -58,7 +58,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 *)(Vertices2)); __e_acsl_delete_block((void *)(Vertices)); @@ -116,7 +116,7 @@ int main(int argc, char const **argv) __e_acsl_delete_block((void *)(vertices3)); __e_acsl_delete_block((void *)(vertices2)); __e_acsl_delete_block((void *)(vertices)); - __e_acsl_globals_delete(); + __e_acsl_globals_clean(); __e_acsl_memory_clean(); return __retres; } 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 a1ab4f085fb127dcfb3a6af1403e05a688163bf6..a0774cc34295c87a5a34d639ba0140cec590ddc5 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 @@ -18,7 +18,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 *)(& foo)); } @@ -69,7 +69,7 @@ int main(int argc, char const **argv) __e_acsl_delete_block((void *)(& fp)); __e_acsl_delete_block((void *)(& q)); __e_acsl_delete_block((void *)(& p)); - __e_acsl_globals_delete(); + __e_acsl_globals_clean(); __e_acsl_memory_clean(); return __retres; } 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 bfb6fd16794df282bb6507aee3803eeeece3460d..c91eca2c10152d43084174f55903cdc2d34618b6 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 @@ -110,7 +110,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 *)(descs2)); __e_acsl_delete_block((void *)(& l_desc2)); @@ -204,7 +204,7 @@ int main(int argc, char const **argv) /*@ assert \valid_read(*p); */ ; __retres = 0; __e_acsl_delete_block((void *)(& p)); - __e_acsl_globals_delete(); + __e_acsl_globals_clean(); __e_acsl_memory_clean(); return __retres; } 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 e77ce2220c0e3669518cd8279a60ab09e441a171..1b6b3cd7af3b988453828e9ba7090dda85407203 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 @@ -106,7 +106,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 *)(Str)); __e_acsl_delete_block((void *)(Strings)); @@ -426,7 +426,7 @@ int main(int argc, char const **argv) __e_acsl_delete_block((void *)(str)); __e_acsl_delete_block((void *)(& p)); __e_acsl_delete_block((void *)(strings)); - __e_acsl_globals_delete(); + __e_acsl_globals_clean(); __e_acsl_memory_clean(); return __retres; }