From 620443c2ac1944172d98bad02c3ae8980193daa9 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 18 Sep 2020 17:32:04 +0200
Subject: [PATCH] [eacsl] Standardize cleanup functions
---
.../src/code_generator/global_observer.ml | 8 +++----
.../src/code_generator/global_observer.mli | 6 ++---
.../e-acsl/src/code_generator/injector.ml | 24 +++++++++----------
.../oracle_ci/gen_bts1386_complex_flowgraph.c | 4 ++--
.../e-acsl/tests/bts/oracle_ci/gen_bts1478.c | 4 ++--
.../e-acsl/tests/bts/oracle_ci/gen_bts1837.c | 4 ++--
.../e-acsl/tests/bts/oracle_ci/gen_bts2191.c | 4 ++--
.../e-acsl/tests/bts/oracle_ci/gen_bts2192.c | 4 ++--
.../e-acsl/tests/bts/oracle_ci/gen_bts2305.c | 4 ++--
.../e-acsl/tests/bts/oracle_ci/gen_bts2406.c | 4 ++--
.../tests/bts/oracle_ci/gen_issue-eacsl-91.c | 4 ++--
.../tests/constructs/oracle_ci/gen_ghost.c | 4 ++--
.../tests/format/oracle_ci/gen_printf.c | 4 ++--
.../full-mtracking/oracle_ci/gen_addrOf.c | 4 ++--
.../tests/memory/oracle_ci/gen_base_addr.c | 4 ++--
.../tests/memory/oracle_ci/gen_block_length.c | 4 ++--
.../tests/memory/oracle_ci/gen_block_valid.c | 4 ++--
.../oracle_ci/gen_compound_initializers.c | 4 ++--
.../e-acsl/tests/memory/oracle_ci/gen_errno.c | 4 ++--
.../tests/memory/oracle_ci/gen_freeable.c | 4 ++--
.../e-acsl/tests/memory/oracle_ci/gen_goto.c | 4 ++--
.../e-acsl/tests/memory/oracle_ci/gen_init.c | 4 ++--
.../tests/memory/oracle_ci/gen_initialized.c | 4 ++--
.../memory/oracle_ci/gen_literal_string.c | 4 ++--
.../tests/memory/oracle_ci/gen_local_init.c | 4 ++--
.../tests/memory/oracle_ci/gen_offset.c | 4 ++--
.../tests/memory/oracle_ci/gen_ptr_init.c | 4 ++--
.../tests/memory/oracle_ci/gen_stdout.c | 4 ++--
.../e-acsl/tests/memory/oracle_ci/gen_valid.c | 4 ++--
.../tests/temporal/oracle_ci/gen_t_darray.c | 4 ++--
.../tests/temporal/oracle_ci/gen_t_fptr.c | 4 ++--
.../temporal/oracle_ci/gen_t_global_init.c | 4 ++--
.../temporal/oracle_ci/gen_t_local_init.c | 4 ++--
33 files changed, 79 insertions(+), 79 deletions(-)
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 023dd1cfc9d..c53604fc55f 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 fa18ebead12..e37f39301d3 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 c7ea8438a11..36c62ebc2dd 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 8131e10a3bd..be6316c86be 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 93c920650cd..8597f7d23ee 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 bc80c8d28dc..fc9046840ed 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 ee4442c59fd..0786c95e01e 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 b8f3d271918..5ade9142b8f 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 634afea64ae..2ce056ec2ae 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 0c331aeb3b6..3c48bb9e561 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 33c28617704..c3248c722e3 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 89cee38a6d7..d1e84e229ba 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 e5b082351a5..74db87f2f2c 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 3d27c36ba8d..8b38c74f47a 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 9927263df1e..b831f777ef0 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 70135545c5c..cec16f53eaf 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 44cb0bfe503..33dd06e7f2d 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 96bcfdbdcdf..ab6e1941648 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 f38474ba466..66d885e493a 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 06eabe4d9f0..ab2185597f8 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 4e033175d14..aa5bc854da2 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 c063f126339..c4eb1d146e1 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 50566fb3407..2fc7f4ff024 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 8710dc8c595..3fc0d11efa0 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 508da20bd2b..bae0a768655 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 a294b87c024..90041c6e180 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 7437d4c8785..9f802d1b7fc 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 225763b343e..63d1db28971 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 133ae6895b7..872f31b112b 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 39664bb15a9..8b6f8a3517a 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 a1ab4f085fb..a0774cc3429 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 bfb6fd16794..c91eca2c101 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 e77ce2220c0..1b6b3cd7af3 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;
}
--
GitLab