From 570027f23dd1eb7a8b1868a20b1c7593e434dbba Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 6 Mar 2020 10:13:08 +0100
Subject: [PATCH] [eacsl:codegen] Update all e-acsl tests
---
.../e-acsl/tests/arith/oracle_ci/gen_arith.c | 1 -
.../e-acsl/tests/arith/oracle_ci/gen_array.c | 1 -
.../e-acsl/tests/arith/oracle_ci/gen_cast.c | 1 -
.../tests/arith/oracle_ci/gen_comparison.c | 1 -
.../tests/arith/oracle_ci/gen_functions.c | 1 -
.../tests/arith/oracle_ci/gen_functions_rec.c | 1 -
.../arith/oracle_ci/gen_integer_constant.c | 1 -
.../tests/arith/oracle_ci/gen_longlong.c | 1 -
.../e-acsl/tests/arith/oracle_ci/gen_not.c | 1 -
.../tests/arith/oracle_ci/gen_rationals.c | 1 -
.../e-acsl/tests/bts/oracle_ci/gen_bts1395.c | 1 -
.../e-acsl/tests/bts/oracle_ci/gen_bts1478.c | 9 +++++--
.../e-acsl/tests/bts/oracle_ci/gen_bts1837.c | 7 +++++-
.../e-acsl/tests/bts/oracle_ci/gen_bts2191.c | 7 +++++-
.../e-acsl/tests/bts/oracle_ci/gen_bts2192.c | 7 +++++-
.../e-acsl/tests/bts/oracle_ci/gen_bts2231.c | 1 -
.../e-acsl/tests/bts/oracle_ci/gen_bts2305.c | 7 +++++-
.../e-acsl/tests/bts/oracle_ci/gen_bts2406.c | 7 +++++-
.../e-acsl/tests/bts/oracle_ci/gen_issue69.c | 1 -
.../tests/constructs/oracle_ci/gen_false.c | 1 -
.../oracle_ci/gen_function_contract.c | 1 -
.../tests/constructs/oracle_ci/gen_ghost.c | 9 +++++--
.../constructs/oracle_ci/gen_invariant.c | 1 -
.../constructs/oracle_ci/gen_labeled_stmt.c | 1 -
.../tests/constructs/oracle_ci/gen_lazy.c | 1 -
.../tests/constructs/oracle_ci/gen_loop.c | 1 -
.../oracle_ci/gen_nested_code_annot.c | 1 -
.../tests/constructs/oracle_ci/gen_result.c | 1 -
.../constructs/oracle_ci/gen_stmt_contract.c | 1 -
.../tests/constructs/oracle_ci/gen_true.c | 1 -
.../tests/constructs/oracle_ci/gen_typedef.c | 1 -
.../examples/oracle_ci/gen_linear_search.c | 1 -
.../tests/full-mmodel/oracle_ci/gen_addrOf.c | 25 +++++++++++--------
.../tests/gmp-only/oracle_ci/gen_arith.c | 1 -
.../tests/gmp-only/oracle_ci/gen_functions.c | 1 -
.../tests/memory/oracle_ci/gen_base_addr.c | 9 +++++--
.../tests/memory/oracle_ci/gen_block_length.c | 11 +++++---
.../tests/memory/oracle_ci/gen_block_valid.c | 7 +++++-
.../oracle_ci/gen_compound_initializers.c | 19 ++++++++------
.../e-acsl/tests/memory/oracle_ci/gen_errno.c | 7 +++++-
.../tests/memory/oracle_ci/gen_freeable.c | 7 +++++-
.../memory/oracle_ci/gen_ghost_parameters.c | 1 -
.../e-acsl/tests/memory/oracle_ci/gen_goto.c | 7 +++++-
.../e-acsl/tests/memory/oracle_ci/gen_init.c | 9 +++++--
.../tests/memory/oracle_ci/gen_initialized.c | 9 +++++--
.../memory/oracle_ci/gen_literal_string.c | 15 +++++++----
.../tests/memory/oracle_ci/gen_local_init.c | 9 +++++--
.../e-acsl/tests/memory/oracle_ci/gen_null.c | 1 -
.../tests/memory/oracle_ci/gen_offset.c | 9 +++++--
.../memory/oracle_ci/gen_other_constants.c | 1 -
.../tests/memory/oracle_ci/gen_ptr_init.c | 9 +++++--
.../tests/memory/oracle_ci/gen_sizeof.c | 1 -
.../tests/memory/oracle_ci/gen_stdout.c | 11 +++++---
.../e-acsl/tests/memory/oracle_ci/gen_valid.c | 9 +++++--
.../tests/special/oracle_ci/gen_builtin.c | 1 -
.../tests/temporal/oracle_ci/gen_t_darray.c | 9 +++++--
.../tests/temporal/oracle_ci/gen_t_fptr.c | 7 +++++-
.../temporal/oracle_ci/gen_t_global_init.c | 17 ++++++++-----
.../temporal/oracle_ci/gen_t_local_init.c | 9 +++++--
59 files changed, 201 insertions(+), 98 deletions(-)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
index 9ae1f7c21dd..6677db53488 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
@@ -4,7 +4,6 @@
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int x = -3;
int y = 2;
long z = 2L;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
index b5a38e3d9d5..334e1f1891a 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
@@ -6,7 +6,6 @@ int T2[4];
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
{
int i = 0;
while (i < 3) {
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c
index 1d262fa573a..c5a5d0cce53 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c
@@ -4,7 +4,6 @@
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
long x = (long)0;
int y = 0;
__e_acsl_assert((int)x == y,"Assertion","main","(int)x == y",
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c
index 80676d549eb..08496d44c23 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c
@@ -4,7 +4,6 @@
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int x = 0;
int y = 1;
__e_acsl_assert(x < y,"Assertion","main","x < y",
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
index c5a633e0350..f8431536df1 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
@@ -85,7 +85,6 @@ int main(void)
{
int __retres;
mystruct m;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int x = 1;
int y = 2;
{
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
index b6a6fd8abf5..6b5f403f5a2 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
@@ -38,7 +38,6 @@ unsigned long __gen_e_acsl_f4_2(long n);
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
{
__e_acsl_mpz_t __gen_e_acsl_f1_6;
__e_acsl_mpz_t __gen_e_acsl__3;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c
index f9c0176310c..15a95e16559 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c
@@ -5,7 +5,6 @@ int main(void)
{
int __retres;
int x;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_assert(1,"Assertion","main","0 == 0",
"tests/arith/integer_constant.i",6);
/*@ assert 0 ≡ 0; */ ;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
index 9278b61ce9f..7ee8de54085 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
@@ -26,7 +26,6 @@ unsigned long long my_pow(unsigned int x, unsigned int n)
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
unsigned long long x = my_pow((unsigned int)2,(unsigned int)63);
{
__e_acsl_mpz_t __gen_e_acsl_;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c
index 9426f228f9a..4ba24ca0879 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c
@@ -4,7 +4,6 @@
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int x = 0;
__e_acsl_assert(x == 0,"Assertion","main","x == 0","tests/arith/not.i",6);
/*@ assert x ≡ 0; */ ;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
index 8d7127bbb63..bd22a341b9b 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
@@ -19,7 +19,6 @@ double avg(double a, double b)
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
{
__e_acsl_mpq_t __gen_e_acsl_;
__e_acsl_mpq_t __gen_e_acsl__2;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
index f9def933ef7..66f0d9080e4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
@@ -25,7 +25,6 @@ int fact(int n)
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int x = __gen_e_acsl_fact(5);
__e_acsl_assert(x == 120,"Assertion","main","x == 120",
"tests/bts/bts1395.i",14);
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 869af38e287..6dddd2a4045 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,6 +53,12 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& global_i_ptr));
+ __e_acsl_delete_block((void *)(& global_i));
+}
+
int main(void)
{
int __retres;
@@ -60,8 +66,7 @@ int main(void)
__e_acsl_globals_init();
__gen_e_acsl_loop();
__retres = 0;
- __e_acsl_delete_block((void *)(& global_i_ptr));
- __e_acsl_delete_block((void *)(& global_i));
+ __e_acsl_globals_delete();
__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 20ab35b8cb0..0c35a1254be 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,6 +88,11 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& S));
+}
+
int main(void)
{
int __retres;
@@ -144,7 +149,7 @@ int main(void)
}
f();
__retres = 0;
- __e_acsl_delete_block((void *)(& S));
+ __e_acsl_globals_delete();
__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 809a47170c6..41b668706f8 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,6 +31,11 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(_G));
+}
+
int main(int argc, char **argv)
{
int __retres;
@@ -55,7 +60,7 @@ int main(int argc, char **argv)
}
/*@ assert \valid_read(_G[0].str); */ ;
__retres = 0;
- __e_acsl_delete_block((void *)(_G));
+ __e_acsl_globals_delete();
__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 5cd32431657..02dcc623302 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
@@ -21,6 +21,11 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& n));
+}
+
int main(int argc, char **argv)
{
int __retres;
@@ -29,7 +34,7 @@ int main(int argc, char **argv)
argc = __gen_e_acsl_atoi((char const *)n);
a = argc;
__retres = 0;
- __e_acsl_delete_block((void *)(& n));
+ __e_acsl_globals_delete();
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c
index 64ef82e9bf9..e3887d10a70 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c
@@ -5,7 +5,6 @@ long A = (long)0;
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
{
__e_acsl_mpz_t __gen_e_acsl_A;
__e_acsl_mpz_t __gen_e_acsl_;
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 29d1004ec5b..55454d5d36b 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,6 +24,11 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& t));
+}
+
int main(int argc, char **argv)
{
int tmp;
@@ -35,7 +40,7 @@ int main(int argc, char **argv)
t.j = (_Bool)1;
/*@ assert \initialized(&t.j); */ ;
tmp = test(& t);
- __e_acsl_delete_block((void *)(& t));
+ __e_acsl_globals_delete();
__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 8e24a58e622..3dbfd57c93a 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,6 +14,11 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(t));
+}
+
int main(void)
{
int __retres;
@@ -39,8 +44,8 @@ int main(void)
}
/*@ assert \valid(&t[0 .. 9]); */ ;
__retres = 0;
- __e_acsl_delete_block((void *)(t));
__e_acsl_delete_block((void *)(& p));
+ __e_acsl_globals_delete();
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c
index cbc6c2e0d19..44cfac328f8 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c
@@ -4,7 +4,6 @@
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
{
int __gen_e_acsl_forall;
int __gen_e_acsl_c;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c
index ffb55240c93..7c2dc5ed469 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c
@@ -4,7 +4,6 @@
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int x = 0;
if (x) {
__e_acsl_assert(0,"Assertion","main","\\false",
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c
index dcfe6a61c3f..9e7f63becc8 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c
@@ -129,7 +129,6 @@ void n(void)
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__gen_e_acsl_f();
__gen_e_acsl_g();
__gen_e_acsl_h();
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 e942d64b232..ab2bc7b7038 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,6 +16,12 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& P));
+ __e_acsl_delete_block((void *)(& G));
+}
+
int main(void)
{
int __retres;
@@ -67,9 +73,8 @@ int main(void)
G ++;
}
__retres = 0;
- __e_acsl_delete_block((void *)(& P));
- __e_acsl_delete_block((void *)(& G));
__e_acsl_delete_block((void *)(& q));
+ __e_acsl_globals_delete();
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c
index 226d6482951..803e14a2914 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c
@@ -4,7 +4,6 @@
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int x = 0;
{
int i = 0;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c
index c364fb15de4..06a5de92573 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c
@@ -40,7 +40,6 @@ int __gen_e_acsl_main(void)
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__retres = __gen_e_acsl_main();
__e_acsl_assert(X == 3,"Postcondition","main","X == 3",
"tests/constructs/labeled_stmt.i",7);
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c
index 72434006bf4..b9ba06467be 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c
@@ -4,7 +4,6 @@
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int x = 0;
int y = 1;
{
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c
index 2626d70b85c..879d1ee52a8 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c
@@ -183,7 +183,6 @@ void unnatural_loop(void)
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
simple_loop();
nested_loops();
unnatural_loop();
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c
index 9411fb1ecd8..252046ac3c8 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c
@@ -4,7 +4,6 @@
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int x = 0;
int y = 1;
__e_acsl_assert(x < y,"Assertion","main","x < y",
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c
index 88919141b53..6b0f6fcf6b2 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c
@@ -35,7 +35,6 @@ int h(void)
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__gen_e_acsl_f(1);
__gen_e_acsl_g(Y);
__gen_e_acsl_h();
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c
index 0fc68d324f2..b9942c443b7 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c
@@ -4,7 +4,6 @@
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int x = 0;
int y = 2;
/*@ ensures x ≡ 1; */
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c
index f8a614b4c48..243f60598a1 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c
@@ -4,7 +4,6 @@
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int x = 0;
x ++;
__e_acsl_assert(1,"Assertion","main","\\true","tests/constructs/true.i",8);
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c
index 7b74563fa1e..92e02166357 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c
@@ -5,7 +5,6 @@ typedef unsigned char uint8;
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
uint8 x = (unsigned char)0;
__e_acsl_assert((int)x == 0,"Assertion","main","x == 0",
"tests/constructs/typedef.i",9);
diff --git a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c
index 09509e5c90a..6657c1ae8ee 100644
--- a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c
@@ -102,7 +102,6 @@ int main(void)
{
int __retres;
int found;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
{
int i = 0;
while (i < 10) {
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
index a96c903d115..ca3a611c9bd 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
@@ -57,6 +57,20 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& f));
+ __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
+ __e_acsl_delete_block((void *)(__fc_tmpnam));
+ __e_acsl_delete_block((void *)(& __fc_p_fopen));
+ __e_acsl_delete_block((void *)(__fc_fopen));
+ __e_acsl_delete_block((void *)(& stdin));
+ __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
+ __e_acsl_delete_block((void *)(random48_counter));
+ __e_acsl_delete_block((void *)(& __fc_random48_init));
+ __e_acsl_delete_block((void *)(& __fc_rand_max));
+}
+
int main(void)
{
int __retres;
@@ -72,18 +86,9 @@ int main(void)
/*@ assert &x ≡ &x; */ ;
__e_acsl_full_init((void *)(& __retres));
__retres = 0;
- __e_acsl_delete_block((void *)(& f));
- __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
- __e_acsl_delete_block((void *)(__fc_tmpnam));
- __e_acsl_delete_block((void *)(& __fc_p_fopen));
- __e_acsl_delete_block((void *)(__fc_fopen));
- __e_acsl_delete_block((void *)(& stdin));
- __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
- __e_acsl_delete_block((void *)(random48_counter));
- __e_acsl_delete_block((void *)(& __fc_random48_init));
- __e_acsl_delete_block((void *)(& __fc_rand_max));
__e_acsl_delete_block((void *)(& x));
__e_acsl_delete_block((void *)(& __retres));
+ __e_acsl_globals_delete();
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
index 721e1250221..dc901aa064e 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
@@ -4,7 +4,6 @@
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int x = -3;
int y = 2;
long z = 2L;
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
index f47d15dc1de..25a8fe98421 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
@@ -83,7 +83,6 @@ int main(void)
{
int __retres;
mystruct m;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int x = 1;
int y = 2;
{
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 6f888df6d06..9f45f3d678f 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
@@ -16,6 +16,12 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& PA));
+ __e_acsl_delete_block((void *)(A));
+}
+
int main(void)
{
int __retres;
@@ -311,8 +317,6 @@ int main(void)
}
/*@ assert \base_addr(q) ≡ \base_addr(qd); */ ;
__retres = 0;
- __e_acsl_delete_block((void *)(& PA));
- __e_acsl_delete_block((void *)(A));
__e_acsl_delete_block((void *)(& qd));
__e_acsl_delete_block((void *)(& q));
__e_acsl_delete_block((void *)(& pd));
@@ -322,6 +326,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_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 4f0f4366d63..4cbe891d458 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
@@ -22,6 +22,13 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& ZERO));
+ __e_acsl_delete_block((void *)(& PA));
+ __e_acsl_delete_block((void *)(A));
+}
+
int main(void)
{
int __retres;
@@ -238,9 +245,6 @@ int main(void)
}
/*@ assert \block_length(q) ≡ size; */ ;
__retres = 0;
- __e_acsl_delete_block((void *)(& ZERO));
- __e_acsl_delete_block((void *)(& PA));
- __e_acsl_delete_block((void *)(A));
__e_acsl_delete_block((void *)(& q));
__e_acsl_delete_block((void *)(& p));
__e_acsl_delete_block((void *)(& pi));
@@ -249,6 +253,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_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 a839a6888e5..3871a01e451 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
@@ -15,6 +15,11 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& B));
+}
+
int main(int argc, char **argv)
{
int __retres;
@@ -151,11 +156,11 @@ int main(int argc, char **argv)
}
/*@ assert ¬\valid(pmax - diff); */ ;
__retres = 0;
- __e_acsl_delete_block((void *)(& B));
__e_acsl_delete_block((void *)(& pmax));
__e_acsl_delete_block((void *)(& pmin));
__e_acsl_delete_block((void *)(& b));
__e_acsl_delete_block((void *)(& p));
+ __e_acsl_globals_delete();
__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 e10793f4101..a5c53537815 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,6 +65,17 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(_G));
+ __e_acsl_delete_block((void *)(& _E));
+ __e_acsl_delete_block((void *)(_D));
+ __e_acsl_delete_block((void *)(& _C));
+ __e_acsl_delete_block((void *)(& _B));
+ __e_acsl_delete_block((void *)(_A));
+ __e_acsl_delete_block((void *)(& _F));
+}
+
int main(int argc, char **argv)
{
int __retres;
@@ -176,13 +187,7 @@ int main(int argc, char **argv)
"tests/memory/compound_initializers.c",43);
/*@ assert _G[0].num ≡ 99; */ ;
__retres = 0;
- __e_acsl_delete_block((void *)(_G));
- __e_acsl_delete_block((void *)(& _E));
- __e_acsl_delete_block((void *)(_D));
- __e_acsl_delete_block((void *)(& _C));
- __e_acsl_delete_block((void *)(& _B));
- __e_acsl_delete_block((void *)(_A));
- __e_acsl_delete_block((void *)(& _F));
+ __e_acsl_globals_delete();
__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 f8a0d9b78f7..cc458e4e367 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
@@ -13,6 +13,11 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& errno));
+}
+
int main(int argc, char const **argv)
{
int __retres;
@@ -38,8 +43,8 @@ int main(int argc, char const **argv)
}
/*@ assert \valid(p); */ ;
__retres = 0;
- __e_acsl_delete_block((void *)(& errno));
__e_acsl_delete_block((void *)(& p));
+ __e_acsl_globals_delete();
__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 57d0968b677..6504639acc7 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
@@ -13,6 +13,11 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(array));
+}
+
int main(void)
{
int __retres;
@@ -75,8 +80,8 @@ int main(void)
}
/*@ assert ¬\freeable(&array[5]); */ ;
__retres = 0;
- __e_acsl_delete_block((void *)(array));
__e_acsl_delete_block((void *)(& p));
+ __e_acsl_globals_delete();
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
index 21e0d8d49e9..dcd56fb12c7 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
@@ -9,7 +9,6 @@ void function(int a, int b, int c, int d)
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int w = 0;
int x = 1;
int y = 2;
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 ac4c3251956..d5c1542ac4f 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,6 +13,11 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& a));
+}
+
int main(void)
{
int __retres;
@@ -34,8 +39,8 @@ int main(void)
}
/*@ assert \initialized(b); */ ;
__retres = 0;
- __e_acsl_delete_block((void *)(& a));
__e_acsl_delete_block((void *)(& b));
+ __e_acsl_globals_delete();
__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 97f4520a88a..e3a9201614e 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,6 +16,12 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& b));
+ __e_acsl_delete_block((void *)(& a));
+}
+
int main(void)
{
int __retres;
@@ -45,10 +51,9 @@ int main(void)
}
/*@ assert \initialized(p); */ ;
__retres = 0;
- __e_acsl_delete_block((void *)(& b));
- __e_acsl_delete_block((void *)(& a));
__e_acsl_delete_block((void *)(& q));
__e_acsl_delete_block((void *)(& p));
+ __e_acsl_globals_delete();
__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 c426b1e9265..026e4bbef14 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
@@ -16,6 +16,12 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& B));
+ __e_acsl_delete_block((void *)(& A));
+}
+
int main(void)
{
int __retres;
@@ -352,8 +358,6 @@ int main(void)
dup[0] = 1;
dup[0] = 1;
__retres = 0;
- __e_acsl_delete_block((void *)(& B));
- __e_acsl_delete_block((void *)(& A));
__e_acsl_delete_block((void *)(d));
__e_acsl_delete_block((void *)(c));
__e_acsl_delete_block((void *)(& r));
@@ -361,6 +365,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_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 3dbfb76f1f0..74ba7f26de6 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,6 +82,15 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& l_str));
+ __e_acsl_delete_block((void *)(& s_str));
+ __e_acsl_delete_block((void *)(& S2));
+ __e_acsl_delete_block((void *)(& S));
+ __e_acsl_delete_block((void *)(& T));
+}
+
int main(void)
{
int __retres;
@@ -138,12 +147,8 @@ int main(void)
s_str ++;
l_str ++;
__retres = 0;
- __e_acsl_delete_block((void *)(& l_str));
- __e_acsl_delete_block((void *)(& s_str));
- __e_acsl_delete_block((void *)(& S2));
- __e_acsl_delete_block((void *)(& S));
- __e_acsl_delete_block((void *)(& T));
__e_acsl_delete_block((void *)(& SS));
+ __e_acsl_globals_delete();
__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 2556be7d024..1f7424a1ec1 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,6 +22,12 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_delete_block((void *)(& X));
+}
+
int main(void)
{
int __retres;
@@ -29,8 +35,7 @@ int main(void)
__e_acsl_globals_init();
f();
__retres = 0;
- __e_acsl_delete_block((void *)(& p));
- __e_acsl_delete_block((void *)(& X));
+ __e_acsl_globals_delete();
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c
index ba7b47ef1ef..02d31514dd5 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c
@@ -4,7 +4,6 @@
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_assert((void *)0 == (void *)0,"Assertion","main",
"\\null == (void *)0","tests/memory/null.i",6);
/*@ assert \null ≡ (void *)0; */ ;
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 5c92ba33022..4ce316ea42c 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
@@ -16,6 +16,12 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& PA));
+ __e_acsl_delete_block((void *)(A));
+}
+
int main(void)
{
int __retres;
@@ -208,14 +214,13 @@ int main(void)
}
/*@ assert \offset(q) ≡ sizeof(long) * 7; */ ;
__retres = 0;
- __e_acsl_delete_block((void *)(& PA));
- __e_acsl_delete_block((void *)(A));
__e_acsl_delete_block((void *)(& q));
__e_acsl_delete_block((void *)(& p));
__e_acsl_delete_block((void *)(& pi));
__e_acsl_delete_block((void *)(& pl));
__e_acsl_delete_block((void *)(& l));
__e_acsl_delete_block((void *)(a));
+ __e_acsl_globals_delete();
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c
index 1af62be5336..e6f639fa935 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c
@@ -8,7 +8,6 @@ enum bool {
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_assert(1,"Assertion","main","\'c\' == \'c\'",
"tests/memory/other_constants.i",10);
/*@ assert 'c' ≡ 'c'; */ ;
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 91f376c3479..e021ea6783c 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
@@ -32,6 +32,12 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& B));
+ __e_acsl_delete_block((void *)(& A));
+}
+
int main(void)
{
int __retres;
@@ -60,10 +66,9 @@ int main(void)
/*@ assert \initialized(&x); */ ;
g(x,y);
__retres = 0;
- __e_acsl_delete_block((void *)(& B));
- __e_acsl_delete_block((void *)(& A));
__e_acsl_delete_block((void *)(& y));
__e_acsl_delete_block((void *)(& x));
+ __e_acsl_globals_delete();
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c
index 0439ae760d2..7920e6b98d1 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c
@@ -4,7 +4,6 @@
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int x = 0;
x ++;
__e_acsl_assert(1,"Assertion","main","sizeof(int) == sizeof(x)",
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 f9b0f156e87..49ec6cf163e 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,6 +16,13 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& stdout));
+ __e_acsl_delete_block((void *)(& stdin));
+ __e_acsl_delete_block((void *)(& stderr));
+}
+
int main(void)
{
int __retres;
@@ -46,9 +53,7 @@ int main(void)
}
/*@ assert \valid(__fc_stdout); */ ;
__retres = 0;
- __e_acsl_delete_block((void *)(& stdout));
- __e_acsl_delete_block((void *)(& stdin));
- __e_acsl_delete_block((void *)(& stderr));
+ __e_acsl_globals_delete();
__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 70735ca3898..38b803a26a3 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
@@ -137,6 +137,12 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& Z));
+ __e_acsl_delete_block((void *)(& X));
+}
+
int main(void)
{
int __retres;
@@ -521,13 +527,12 @@ int main(void)
/*@ assert \valid(&Z); */ ;
g();
__retres = 0;
- __e_acsl_delete_block((void *)(& Z));
- __e_acsl_delete_block((void *)(& X));
__e_acsl_delete_block((void *)(& n));
__e_acsl_delete_block((void *)(& d));
__e_acsl_delete_block((void *)(& c));
__e_acsl_delete_block((void *)(& b));
__e_acsl_delete_block((void *)(& a));
+ __e_acsl_globals_delete();
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
index 0678e6d6236..dcc566b58e8 100644
--- a/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
@@ -24,7 +24,6 @@ int incr(int x)
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
int i = __gen_e_acsl_f(2);
__retres = 0;
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 ca59330238b..f2c564d40b4 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,6 +58,12 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(Vertices2));
+ __e_acsl_delete_block((void *)(Vertices));
+}
+
int main(int argc, char const **argv)
{
int __retres;
@@ -105,13 +111,12 @@ int main(int argc, char const **argv)
__e_acsl_temporal_save_nblock_parameter((void *)(triple_vertices2[0]),0U);
abe_matrix(triple_vertices2[0]);
__retres = 0;
- __e_acsl_delete_block((void *)(Vertices2));
- __e_acsl_delete_block((void *)(Vertices));
__e_acsl_delete_block((void *)(triple_vertices2));
__e_acsl_delete_block((void *)(triple_vertices));
__e_acsl_delete_block((void *)(vertices3));
__e_acsl_delete_block((void *)(vertices2));
__e_acsl_delete_block((void *)(vertices));
+ __e_acsl_globals_delete();
__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 4a0750a1833..6ce50be381f 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,6 +18,11 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(& foo));
+}
+
int main(int argc, char const **argv)
{
int __retres;
@@ -61,10 +66,10 @@ int main(int argc, char const **argv)
/*@ assert \valid(q); */ ;
__retres = 0;
__e_acsl_delete_block((void *)(& argc));
- __e_acsl_delete_block((void *)(& foo));
__e_acsl_delete_block((void *)(& fp));
__e_acsl_delete_block((void *)(& q));
__e_acsl_delete_block((void *)(& p));
+ __e_acsl_globals_delete();
__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 d1c0cc7c58f..1a223bf90f4 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,6 +110,16 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(descs2));
+ __e_acsl_delete_block((void *)(& l_desc2));
+ __e_acsl_delete_block((void *)(descs));
+ __e_acsl_delete_block((void *)(& l_desc));
+ __e_acsl_delete_block((void *)(extra_lbits));
+ __e_acsl_delete_block((void *)(strings));
+}
+
int main(int argc, char const **argv)
{
int __retres;
@@ -193,13 +203,8 @@ int main(int argc, char const **argv)
}
/*@ assert \valid_read(*p); */ ;
__retres = 0;
- __e_acsl_delete_block((void *)(descs2));
- __e_acsl_delete_block((void *)(& l_desc2));
- __e_acsl_delete_block((void *)(descs));
- __e_acsl_delete_block((void *)(& l_desc));
- __e_acsl_delete_block((void *)(extra_lbits));
- __e_acsl_delete_block((void *)(strings));
__e_acsl_delete_block((void *)(& p));
+ __e_acsl_globals_delete();
__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 b6341802859..9ccb27aa258 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,6 +106,12 @@ void __e_acsl_globals_init(void)
return;
}
+void __e_acsl_globals_delete(void)
+{
+ __e_acsl_delete_block((void *)(Str));
+ __e_acsl_delete_block((void *)(Strings));
+}
+
int main(int argc, char const **argv)
{
int __retres;
@@ -411,8 +417,6 @@ int main(int argc, char const **argv)
__e_acsl_temporal_save_nblock_parameter((void *)(& descs2[1].desc),0U);
build_tree(& descs2[1].desc);
__retres = 0;
- __e_acsl_delete_block((void *)(Str));
- __e_acsl_delete_block((void *)(Strings));
__e_acsl_delete_block((void *)(descs2));
__e_acsl_delete_block((void *)(& l_desc2));
__e_acsl_delete_block((void *)(descs));
@@ -422,6 +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_memory_clean();
return __retres;
}
--
GitLab