From 628c21d7e61f274f0f474c8c7265e234446f874d Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 30 Aug 2019 13:34:40 +0200
Subject: [PATCH] [tests] remove useless STDOPT
---
src/plugins/e-acsl/tests/arith/cast.i | 1 -
.../e-acsl/tests/arith/functions_rec.c | 6 +-
.../e-acsl/tests/arith/oracle/cast.res.oracle | 2 +-
.../arith/oracle/functions_rec.res.oracle | 18 ++
.../e-acsl/tests/arith/oracle/gen_cast.c | 12 +-
.../tests/arith/oracle/gen_functions_rec.c | 173 ++++++++++++++----
src/plugins/e-acsl/tests/bts/bts1390.c | 1 -
src/plugins/e-acsl/tests/bts/bts1399.c | 3 -
src/plugins/e-acsl/tests/bts/bts2386.c | 11 +-
.../tests/bts/oracle/bts1390.res.oracle | 10 +-
.../tests/bts/oracle/bts2386.1.res.oracle | 2 -
.../tests/bts/oracle/bts2386.2.res.oracle | 6 -
...ts2386.0.res.oracle => bts2386.res.oracle} | 2 +-
.../e-acsl/tests/bts/oracle/gen_bts1390.c | 10 +-
.../e-acsl/tests/bts/oracle/gen_bts1399.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts2386.c | 4 +-
.../e-acsl/tests/bts/oracle/gen_bts2386_2.c | 52 ------
.../e-acsl/tests/bts/oracle/gen_bts2386_3.c | 81 --------
.../e-acsl/tests/language_constructs/ghost.i | 1 -
.../language_constructs/oracle/gen_ghost.c | 8 +-
src/plugins/e-acsl/tests/memory/call.c | 3 -
src/plugins/e-acsl/tests/memory/freeable.c | 1 -
src/plugins/e-acsl/tests/memory/initialized.c | 1 -
src/plugins/e-acsl/tests/memory/local_init.c | 2 +-
src/plugins/e-acsl/tests/memory/local_var.c | 3 -
.../tests/memory/oracle/freeable.res.oracle | 4 +-
.../e-acsl/tests/memory/oracle/gen_call.c | 2 +-
.../e-acsl/tests/memory/oracle/gen_freeable.c | 14 +-
.../tests/memory/oracle/gen_initialized.c | 70 +++----
.../tests/memory/oracle/gen_local_init.c | 17 ++
.../tests/memory/oracle/gen_local_var.c | 2 +-
.../e-acsl/tests/memory/oracle/gen_valid.c | 40 ++--
.../tests/memory/oracle/gen_valid_alias.c | 10 +-
.../memory/oracle/gen_valid_in_contract.c | 6 +-
.../e-acsl/tests/memory/oracle/gen_vector.c | 56 +++++-
.../memory/oracle/initialized.res.oracle | 4 +-
.../tests/memory/oracle/local_init.res.oracle | 2 -
.../tests/memory/oracle/valid.res.oracle | 2 +-
.../memory/oracle/valid_alias.res.oracle | 2 +-
.../tests/memory/oracle/vector.res.oracle | 6 +-
src/plugins/e-acsl/tests/memory/valid.c | 4 -
src/plugins/e-acsl/tests/memory/valid_alias.c | 1 -
.../e-acsl/tests/memory/valid_in_contract.c | 1 -
src/plugins/e-acsl/tests/memory/vector.c | 5 +-
.../tests/temporal/oracle/gen_t_getenv.c | 4 +-
.../tests/temporal/oracle/t_getenv.res.oracle | 12 +-
src/plugins/e-acsl/tests/temporal/t_getenv.c | 1 -
47 files changed, 354 insertions(+), 328 deletions(-)
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts2386.1.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/bts2386.2.res.oracle
rename src/plugins/e-acsl/tests/bts/oracle/{bts2386.0.res.oracle => bts2386.res.oracle} (75%)
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/gen_bts2386_2.c
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/gen_bts2386_3.c
diff --git a/src/plugins/e-acsl/tests/arith/cast.i b/src/plugins/e-acsl/tests/arith/cast.i
index 700d338841e..910ca8b40d1 100644
--- a/src/plugins/e-acsl/tests/arith/cast.i
+++ b/src/plugins/e-acsl/tests/arith/cast.i
@@ -1,6 +1,5 @@
/* run.config
COMMENT: cast
- STDOPT: #"-no-warn-signed-downcast" #"-no-warn-unsigned-downcast"
*/
int main(void) {
diff --git a/src/plugins/e-acsl/tests/arith/functions_rec.c b/src/plugins/e-acsl/tests/arith/functions_rec.c
index 76c60912194..f875751830f 100644
--- a/src/plugins/e-acsl/tests/arith/functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/functions_rec.c
@@ -19,9 +19,9 @@
6; */
int main (void) {
- // /*@ assert f1(0) == 0; */ ;
- // /*@ assert f1(1) == 1; */ ;
- // /*@ assert f1(100) == 5050; */ ;
+ /*@ assert f1(0) == 0; */ ;
+ /*@ assert f1(1) == 1; */ ;
+ /*@ assert f1(100) == 5050; */ ;
/*@ assert f2(7) == 1; */ ;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/cast.res.oracle
index e4c1a84ed16..91932086457 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/cast.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/cast.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-[e-acsl] tests/arith/cast.i:23: Warning:
+[e-acsl] tests/arith/cast.i:22: Warning:
E-ACSL construct `R to Int' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
index 139e052e16d..83535c9eff5 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
@@ -1,5 +1,23 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/arith/functions_rec.c:22: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/arith/functions_rec.c:22: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/functions_rec.c:23: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/arith/functions_rec.c:23: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/functions_rec.c:24: Warning:
+ assertion got status unknown.
+[eva] tests/arith/functions_rec.c:7: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_f1_2 (__gen_e_acsl_f1_2 <- __gen_e_acsl_f1_2 :: tests/arith/functions_rec.c:7 <-
+ __gen_e_acsl_f1 :: tests/arith/functions_rec.c:24 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/arith/functions_rec.c:24: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:26: Warning:
assertion got status unknown.
[eva] tests/arith/functions_rec.c:10: Warning:
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_cast.c b/src/plugins/e-acsl/tests/arith/oracle/gen_cast.c
index 134e920276e..b11e400d362 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_cast.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_cast.c
@@ -9,24 +9,24 @@ int main(void)
int y = 0;
/*@ assert (int)x ≡ y; */
__e_acsl_assert((int)x == y,(char *)"Assertion",(char *)"main",
- (char *)"(int)x == y",10);
+ (char *)"(int)x == y",9);
/*@ assert x ≡ (long)y; */
__e_acsl_assert(x == (long)y,(char *)"Assertion",(char *)"main",
- (char *)"x == (long)y",11);
+ (char *)"x == (long)y",10);
/*@ assert y ≡ (int)0; */
__e_acsl_assert(y == 0,(char *)"Assertion",(char *)"main",
- (char *)"y == (int)0",13);
+ (char *)"y == (int)0",12);
/*@ assert (unsigned int)y ≡ (unsigned int)0; */
__e_acsl_assert((unsigned int)y == 0U,(char *)"Assertion",(char *)"main",
- (char *)"(unsigned int)y == (unsigned int)0",14);
+ (char *)"(unsigned int)y == (unsigned int)0",13);
/*@ assert y ≢ (int)0xfffffffffffffff; */
__e_acsl_assert(y != -1,(char *)"Assertion",(char *)"main",
- (char *)"y != (int)0xfffffffffffffff",17);
+ (char *)"y != (int)0xfffffffffffffff",16);
/*@ assert (unsigned int)y ≢ (unsigned int)0xfffffffffffffff; */
__e_acsl_assert((unsigned int)y != 4294967295U,(char *)"Assertion",
(char *)"main",
(char *)"(unsigned int)y != (unsigned int)0xfffffffffffffff",
- 18);
+ 17);
int t[2] = {0, 1};
/*@ assert (float)x ≡ t[(int)0.1]; */ ;
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
index bc071fb5cb4..cbed6cde4bb 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
@@ -2,7 +2,12 @@
#include "stdio.h"
#include "stdlib.h"
/*@ logic ℤ f1(ℤ n) = n ≤ 0? 0: f1(n - 1) + n;
- */
+
+*/
+void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n);
+
+void __gen_e_acsl_f1_2(__e_acsl_mpz_t *__retres_arg, long n);
+
/*@ logic ℤ f2(ℤ n) = n < 0? 1: (f2(n - 1) * f2(n - 2)) / f2(n - 3);
*/
int __gen_e_acsl_f2(int n);
@@ -34,6 +39,48 @@ int main(void)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ /*@ assert f1(0) ≡ 0; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f1_6;
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ int __gen_e_acsl_eq;
+ __gen_e_acsl_f1(& __gen_e_acsl_f1_6,0);
+ __gmpz_init_set_si(__gen_e_acsl__3,0L);
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+ __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
+ (char *)"f1(0) == 0",22);
+ __gmpz_clear(__gen_e_acsl_f1_6);
+ __gmpz_clear(__gen_e_acsl__3);
+ }
+ /*@ assert f1(1) ≡ 1; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f1_8;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_eq_2;
+ __gen_e_acsl_f1(& __gen_e_acsl_f1_8,1);
+ __gmpz_init_set_si(__gen_e_acsl__4,1L);
+ __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
+ (char *)"main",(char *)"f1(1) == 1",23);
+ __gmpz_clear(__gen_e_acsl_f1_8);
+ __gmpz_clear(__gen_e_acsl__4);
+ }
+ /*@ assert f1(100) ≡ 5050; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f1_10;
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ int __gen_e_acsl_eq_3;
+ __gen_e_acsl_f1(& __gen_e_acsl_f1_10,100);
+ __gmpz_init_set_si(__gen_e_acsl__5,5050L);
+ __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_10),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
+ (char *)"main",(char *)"f1(100) == 5050",24);
+ __gmpz_clear(__gen_e_acsl_f1_10);
+ __gmpz_clear(__gen_e_acsl__5);
+ }
/*@ assert f2(7) ≡ 1; */
{
int __gen_e_acsl_f2_14;
@@ -59,10 +106,74 @@ int main(void)
return __retres;
}
+void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n)
+{
+ __e_acsl_mpz_t __gen_e_acsl_if_2;
+ if (n <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gmpz_init_set(__gen_e_acsl_if_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_clear(__gen_e_acsl_);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_f1_5;
+ __e_acsl_mpz_t __gen_e_acsl_n_2;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __gen_e_acsl_f1_2(& __gen_e_acsl_f1_5,n - 1L);
+ __gmpz_init_set_si(__gen_e_acsl_n_2,(long)n);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2));
+ __gmpz_init_set(__gen_e_acsl_if_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __gmpz_clear(__gen_e_acsl_f1_5);
+ __gmpz_clear(__gen_e_acsl_n_2);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ }
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
+ __gmpz_clear(__gen_e_acsl_if_2);
+ return;
+}
+
+void __gen_e_acsl_f1_2(__e_acsl_mpz_t *__retres_arg, long n)
+{
+ __e_acsl_mpz_t __gen_e_acsl_if;
+ if (n <= 0L) {
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_clear(__gen_e_acsl__2);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_f1_4;
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __gen_e_acsl_f1_2(& __gen_e_acsl_f1_4,n - 1L);
+ __gmpz_init_set_si(__gen_e_acsl_n,n);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
+ __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gmpz_clear(__gen_e_acsl_f1_4);
+ __gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl_add);
+ }
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __gmpz_clear(__gen_e_acsl_if);
+ return;
+}
+
int __gen_e_acsl_f2(int n)
{
- int __gen_e_acsl_if_2;
- if (n < 0) __gen_e_acsl_if_2 = 1;
+ int __gen_e_acsl_if_4;
+ if (n < 0) __gen_e_acsl_if_4 = 1;
else {
int __gen_e_acsl_f2_9;
int __gen_e_acsl_f2_11;
@@ -86,15 +197,15 @@ int __gen_e_acsl_f2(int n)
(int)(__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13
≤ 2147483647;
*/
- __gen_e_acsl_if_2 = (__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13;
+ __gen_e_acsl_if_4 = (__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13;
}
- return __gen_e_acsl_if_2;
+ return __gen_e_acsl_if_4;
}
int __gen_e_acsl_f2_2(long n)
{
- int __gen_e_acsl_if;
- if (n < 0L) __gen_e_acsl_if = 1;
+ int __gen_e_acsl_if_3;
+ if (n < 0L) __gen_e_acsl_if_3 = 1;
else {
int __gen_e_acsl_f2_4;
int __gen_e_acsl_f2_6;
@@ -118,9 +229,9 @@ int __gen_e_acsl_f2_2(long n)
(int)(__gen_e_acsl_f2_4 * __gen_e_acsl_f2_6) / __gen_e_acsl_f2_8
≤ 2147483647;
*/
- __gen_e_acsl_if = (__gen_e_acsl_f2_4 * __gen_e_acsl_f2_6) / __gen_e_acsl_f2_8;
+ __gen_e_acsl_if_3 = (__gen_e_acsl_f2_4 * __gen_e_acsl_f2_6) / __gen_e_acsl_f2_8;
}
- return __gen_e_acsl_if;
+ return __gen_e_acsl_if_3;
}
int __gen_e_acsl_g(int n)
@@ -137,72 +248,72 @@ int __gen_e_acsl_g_5(long n)
int __gen_e_acsl_f3(int n)
{
- int __gen_e_acsl_if_4;
+ int __gen_e_acsl_if_6;
if (n > 0) {
int __gen_e_acsl_g_2;
int __gen_e_acsl_f3_5;
__gen_e_acsl_g_2 = __gen_e_acsl_g(n);
__gen_e_acsl_f3_5 = __gen_e_acsl_f3_2(n - 1L);
- __gen_e_acsl_if_4 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_5 - 5;
+ __gen_e_acsl_if_6 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_5 - 5;
}
else {
int __gen_e_acsl_g_8;
__gen_e_acsl_g_8 = __gen_e_acsl_g_5(n + 1L);
- __gen_e_acsl_if_4 = __gen_e_acsl_g_8;
+ __gen_e_acsl_if_6 = __gen_e_acsl_g_8;
}
- return __gen_e_acsl_if_4;
+ return __gen_e_acsl_if_6;
}
int __gen_e_acsl_f3_2(long n)
{
- int __gen_e_acsl_if_3;
+ int __gen_e_acsl_if_5;
if (n > 0L) {
int __gen_e_acsl_g_4;
int __gen_e_acsl_f3_4;
__gen_e_acsl_g_4 = __gen_e_acsl_g((int)n);
__gen_e_acsl_f3_4 = __gen_e_acsl_f3_2(n - 1L);
- __gen_e_acsl_if_3 = __gen_e_acsl_g_4 * __gen_e_acsl_f3_4 - 5;
+ __gen_e_acsl_if_5 = __gen_e_acsl_g_4 * __gen_e_acsl_f3_4 - 5;
}
else {
int __gen_e_acsl_g_6;
__gen_e_acsl_g_6 = __gen_e_acsl_g_5(n + 1L);
- __gen_e_acsl_if_3 = __gen_e_acsl_g_6;
+ __gen_e_acsl_if_5 = __gen_e_acsl_g_6;
}
- return __gen_e_acsl_if_3;
+ return __gen_e_acsl_if_5;
}
unsigned long __gen_e_acsl_f4(int n)
{
- unsigned long __gen_e_acsl_if_8;
+ unsigned long __gen_e_acsl_if_10;
if (n < 100) {
unsigned long __gen_e_acsl_f4_5;
__gen_e_acsl_f4_5 = __gen_e_acsl_f4_2(n + 1L);
- __gen_e_acsl_if_8 = __gen_e_acsl_f4_5;
+ __gen_e_acsl_if_10 = __gen_e_acsl_f4_5;
}
else {
- unsigned long __gen_e_acsl_if_7;
- if ((long)n < 9223372036854775807L) __gen_e_acsl_if_7 = 9223372036854775807UL;
- else __gen_e_acsl_if_7 = 6UL;
- __gen_e_acsl_if_8 = __gen_e_acsl_if_7;
+ unsigned long __gen_e_acsl_if_9;
+ if ((long)n < 9223372036854775807L) __gen_e_acsl_if_9 = 9223372036854775807UL;
+ else __gen_e_acsl_if_9 = 6UL;
+ __gen_e_acsl_if_10 = __gen_e_acsl_if_9;
}
- return __gen_e_acsl_if_8;
+ return __gen_e_acsl_if_10;
}
unsigned long __gen_e_acsl_f4_2(long n)
{
- unsigned long __gen_e_acsl_if_6;
+ unsigned long __gen_e_acsl_if_8;
if (n < 100L) {
unsigned long __gen_e_acsl_f4_4;
__gen_e_acsl_f4_4 = __gen_e_acsl_f4_2(n + 1L);
- __gen_e_acsl_if_6 = __gen_e_acsl_f4_4;
+ __gen_e_acsl_if_8 = __gen_e_acsl_f4_4;
}
else {
- unsigned long __gen_e_acsl_if_5;
- if (n < 9223372036854775807L) __gen_e_acsl_if_5 = 9223372036854775807UL;
- else __gen_e_acsl_if_5 = 6UL;
- __gen_e_acsl_if_6 = __gen_e_acsl_if_5;
+ unsigned long __gen_e_acsl_if_7;
+ if (n < 9223372036854775807L) __gen_e_acsl_if_7 = 9223372036854775807UL;
+ else __gen_e_acsl_if_7 = 6UL;
+ __gen_e_acsl_if_8 = __gen_e_acsl_if_7;
}
- return __gen_e_acsl_if_6;
+ return __gen_e_acsl_if_8;
}
diff --git a/src/plugins/e-acsl/tests/bts/bts1390.c b/src/plugins/e-acsl/tests/bts/bts1390.c
index eddb97a0285..74cba86cdbe 100644
--- a/src/plugins/e-acsl/tests/bts/bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/bts1390.c
@@ -1,5 +1,4 @@
/* run.config
- STDOPT: +"-no-val-builtins-auto"
COMMENT: bts #1390, issue with typing of quantified variables
*/
diff --git a/src/plugins/e-acsl/tests/bts/bts1399.c b/src/plugins/e-acsl/tests/bts/bts1399.c
index 66032b3c177..4e2266935d9 100644
--- a/src/plugins/e-acsl/tests/bts/bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/bts1399.c
@@ -1,12 +1,9 @@
/* run.config
COMMENT: complex fields and indexes + potential RTE in \initialized
- STDOPT: +"-no-val-alloc-returns-null"
*/
#include "stdlib.h"
-extern void *malloc(size_t p);
-
struct spongeStateStruct {
unsigned char __attribute__((__aligned__(32))) state[1600 / 8] ;
unsigned char __attribute__((__aligned__(32))) dataQueue[1536 / 8] ;
diff --git a/src/plugins/e-acsl/tests/bts/bts2386.c b/src/plugins/e-acsl/tests/bts/bts2386.c
index a401b20823c..007b5c1523d 100644
--- a/src/plugins/e-acsl/tests/bts/bts2386.c
+++ b/src/plugins/e-acsl/tests/bts/bts2386.c
@@ -1,14 +1,5 @@
/* run.config, run.config_2
COMMENT: pointer substraction
- COMMENT: on gcc_x86_64
- LOG: gen_@PTEST_NAME@.c
- OPT: -machdep gcc_x86_64 -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/bts/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -value-verbose 0
- COMMENT: on x86_32 (default case when no machdep is given)
- LOG: gen_@PTEST_NAME@_2.c
- OPT: -machdep x86_32 -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/bts/result/gen_@PTEST_NAME@_2.c -kernel-verbose 0 -val -value-verbose 0
- COMMENT: with "-e-acsl-gmp-only"
- LOG: gen_@PTEST_NAME@_3.c
- OPT: -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/bts/result/gen_@PTEST_NAME@_3.c -kernel-verbose 0 -val -value-verbose 0
*/
void f(const void *s, int c, unsigned long n) {
@@ -21,4 +12,4 @@ int main() {
const char *s = "1234567890";
f(s, '0', 11);
return 0;
-}
\ No newline at end of file
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
index a0dedf7f3e9..929213a9cd2 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
@@ -1,10 +1,12 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/bts/bts1390.c:12: Warning:
+[eva:builtins:missing-spec] tests/bts/bts1390.c:13: Warning:
+ The builtin for function memchr will not be used, as its frama-c libc specification is not available.
+[eva:alarm] tests/bts/bts1390.c:11: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/bts/bts1390.c:9: Warning:
+[eva:alarm] tests/bts/bts1390.c:8: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/bts/bts1390.c:13: Warning:
+[eva:alarm] tests/bts/bts1390.c:12: Warning:
function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-[eva:alarm] tests/bts/bts1390.c:18: Warning:
+[eva:alarm] tests/bts/bts1390.c:17: Warning:
out of bounds read. assert \valid_read(s);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2386.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2386.1.res.oracle
deleted file mode 100644
index efd02631129..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2386.1.res.oracle
+++ /dev/null
@@ -1,2 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2386.2.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2386.2.res.oracle
deleted file mode 100644
index 164b435ffa8..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2386.2.res.oracle
+++ /dev/null
@@ -1,6 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/bts/bts2386.c:16: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/bts/bts2386.c:17: Warning:
- function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2386.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2386.res.oracle
similarity index 75%
rename from src/plugins/e-acsl/tests/bts/oracle/bts2386.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts2386.res.oracle
index 3ca31dcb9c9..46b9b8d4ff2 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2386.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2386.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/bts/bts2386.c:16: Warning:
+[eva:alarm] tests/bts/bts2386.c:7: Warning:
function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
index f199c2a1637..b45368fa2b4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -86,7 +86,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
(char *)"memchr",
(char *)"mem_access: \\valid_read((char *)buf + __gen_e_acsl_k)",
- 12);
+ 11);
if ((int)*((char *)buf + __gen_e_acsl_k) != c) ;
else {
__gen_e_acsl_forall_2 = 0;
@@ -117,7 +117,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",
(char *)"memchr",
(char *)"mem_access: \\valid_read((char *)buf + __gen_e_acsl_i)",
- 9);
+ 8);
if (! ((int)*((char *)buf + __gen_e_acsl_i) == c)) ;
else {
__gen_e_acsl_exists = 1;
@@ -157,7 +157,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"memchr",
(char *)"mem_access: \\valid_read((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j)",
- 10);
+ 9);
if ((int)*((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j) != __gen_e_acsl_at_3)
;
else {
@@ -173,13 +173,13 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_assert(__gen_e_acsl_implies,(char *)"Postcondition",
(char *)"memchr",
(char *)"\\old(\\exists integer i; 0 <= i < (int)n && (int)*((char *)buf + i) == c) ==>\n(\\forall int j;\n 0 <= j < (int)\\offset((char *)\\result) ==>\n (int)*((char *)\\old(buf) + j) != \\old(c))",
- 10);
+ 9);
if (! __gen_e_acsl_at_4) __gen_e_acsl_implies_2 = 1;
else __gen_e_acsl_implies_2 = __retres == (void *)0;
__e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Postcondition",
(char *)"memchr",
(char *)"\\old(\\forall integer k; 0 <= k < (int)n ==> (int)*((char *)buf + k) != c) ==>\n\\result == (void *)0",
- 13);
+ 12);
__e_acsl_delete_block((void *)(& buf));
__e_acsl_delete_block((void *)(& __retres));
return __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
index 071c1a1276c..5b3967bd61d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
@@ -26,7 +26,7 @@ int main(void)
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(&state->bitsInQueue)",
- 22);
+ 19);
__gen_e_acsl_initialized = __e_acsl_initialized((void *)(& state->dataQueue[
state->bitsInQueue / 8U]),
sizeof(unsigned char __attribute__((
@@ -34,7 +34,7 @@ int main(void)
__e_acsl_assert(! __gen_e_acsl_initialized,(char *)"Assertion",
(char *)"main",
(char *)"!\\initialized(&state->dataQueue[state->bitsInQueue / 8])",
- 22);
+ 19);
}
free((void *)state);
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c
index 874346e021e..d2bead7b834 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c
@@ -23,14 +23,14 @@ void f(void const *s, int c, unsigned long n)
__gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sub));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"f",
- (char *)"p - (unsigned char const *)s == n - n",16);
+ (char *)"p - (unsigned char const *)s == n - n",7);
__gmpz_clear(__gen_e_acsl_);
__gmpz_clear(__gen_e_acsl_n);
__gmpz_clear(__gen_e_acsl_sub);
}
/*@ assert p - (unsigned char const *)s ≡ 0; */
__e_acsl_assert(p - (unsigned char const *)s == 0UL,(char *)"Assertion",
- (char *)"f",(char *)"p - (unsigned char const *)s == 0",17);
+ (char *)"f",(char *)"p - (unsigned char const *)s == 0",8);
__e_acsl_delete_block((void *)(& s));
__e_acsl_delete_block((void *)(& p));
return;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386_2.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386_2.c
deleted file mode 100644
index 99d090f4adb..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386_2.c
+++ /dev/null
@@ -1,52 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-char *__gen_e_acsl_literal_string;
-void f(void const *s, int c, unsigned long n)
-{
- __e_acsl_store_block((void *)(& s),(size_t)4);
- unsigned char const *p = (unsigned char const *)s;
- __e_acsl_store_block((void *)(& p),(size_t)4);
- __e_acsl_full_init((void *)(& p));
- /*@ assert p - (unsigned char const *)s ≡ n - n; */
- __e_acsl_assert(p - (unsigned char const *)s == n - (long long)n,
- (char *)"Assertion",(char *)"f",
- (char *)"p - (unsigned char const *)s == n - n",16);
- /*@ assert p - (unsigned char const *)s ≡ 0; */
- __e_acsl_assert(p - (unsigned char const *)s == 0U,(char *)"Assertion",
- (char *)"f",(char *)"p - (unsigned char const *)s == 0",17);
- __e_acsl_delete_block((void *)(& s));
- __e_acsl_delete_block((void *)(& p));
- return;
-}
-
-void __e_acsl_globals_init(void)
-{
- static char __e_acsl_already_run = 0;
- if (! __e_acsl_already_run) {
- __e_acsl_already_run = 1;
- __gen_e_acsl_literal_string = "1234567890";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
- sizeof("1234567890"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
- }
- return;
-}
-
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)4);
- __e_acsl_globals_init();
- char const *s = __gen_e_acsl_literal_string;
- __e_acsl_store_block((void *)(& s),(size_t)4);
- __e_acsl_full_init((void *)(& s));
- f((void const *)s,'0',(unsigned long)11);
- __retres = 0;
- __e_acsl_delete_block((void *)(& s));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386_3.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386_3.c
deleted file mode 100644
index 2977b9cbbe0..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386_3.c
+++ /dev/null
@@ -1,81 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-char *__gen_e_acsl_literal_string;
-void f(void const *s, int c, unsigned long n)
-{
- __e_acsl_store_block((void *)(& s),(size_t)4);
- unsigned char const *p = (unsigned char const *)s;
- __e_acsl_store_block((void *)(& p),(size_t)4);
- __e_acsl_full_init((void *)(& p));
- /*@ assert p - (unsigned char const *)s ≡ n - n; */
- {
- __e_acsl_mpz_t __gen_e_acsl_;
- __e_acsl_mpz_t __gen_e_acsl_n;
- __e_acsl_mpz_t __gen_e_acsl_sub;
- int __gen_e_acsl_eq;
- __gmpz_init_set_ui(__gen_e_acsl_,
- (unsigned long)(p - (unsigned char const *)s));
- __gmpz_init_set_ui(__gen_e_acsl_n,n);
- __gmpz_init(__gen_e_acsl_sub);
- __gmpz_sub(__gen_e_acsl_sub,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"f",
- (char *)"p - (unsigned char const *)s == n - n",16);
- __gmpz_clear(__gen_e_acsl_);
- __gmpz_clear(__gen_e_acsl_n);
- __gmpz_clear(__gen_e_acsl_sub);
- }
- /*@ assert p - (unsigned char const *)s ≡ 0; */
- {
- __e_acsl_mpz_t __gen_e_acsl__2;
- __e_acsl_mpz_t __gen_e_acsl__3;
- int __gen_e_acsl_eq_2;
- __gmpz_init_set_ui(__gen_e_acsl__2,
- (unsigned long)(p - (unsigned char const *)s));
- __gmpz_init_set_si(__gen_e_acsl__3,0L);
- __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",(char *)"f",
- (char *)"p - (unsigned char const *)s == 0",17);
- __gmpz_clear(__gen_e_acsl__2);
- __gmpz_clear(__gen_e_acsl__3);
- }
- __e_acsl_delete_block((void *)(& s));
- __e_acsl_delete_block((void *)(& p));
- return;
-}
-
-void __e_acsl_globals_init(void)
-{
- static char __e_acsl_already_run = 0;
- if (! __e_acsl_already_run) {
- __e_acsl_already_run = 1;
- __gen_e_acsl_literal_string = "1234567890";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
- sizeof("1234567890"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
- }
- return;
-}
-
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)4);
- __e_acsl_globals_init();
- char const *s = __gen_e_acsl_literal_string;
- __e_acsl_store_block((void *)(& s),(size_t)4);
- __e_acsl_full_init((void *)(& s));
- f((void const *)s,'0',(unsigned long)11);
- __retres = 0;
- __e_acsl_delete_block((void *)(& s));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/language_constructs/ghost.i b/src/plugins/e-acsl/tests/language_constructs/ghost.i
index 449c958445b..e7c4414b6b1 100644
--- a/src/plugins/e-acsl/tests/language_constructs/ghost.i
+++ b/src/plugins/e-acsl/tests/language_constructs/ghost.i
@@ -1,6 +1,5 @@
/* run.config
COMMENT: ghost code
- STDOPT:
*/
/*@ ghost int G = 0; */
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_ghost.c b/src/plugins/e-acsl/tests/language_constructs/oracle/gen_ghost.c
index cf47b08a6d2..739fa7d6e26 100644
--- a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_ghost.c
+++ b/src/plugins/e-acsl/tests/language_constructs/oracle/gen_ghost.c
@@ -32,11 +32,11 @@ int main(void)
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)P,sizeof(int),
(void *)P,(void *)(& P));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(P)",14);
+ (char *)"mem_access: \\valid_read(P)",13);
__gen_e_acsl_valid = __e_acsl_valid((void *)P,sizeof(int),(void *)P,
(void *)(& P));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid(P)",14);
+ (char *)"mem_access: \\valid(P)",13);
}
(*P) ++;
/*@ assert *q ≡ G; */
@@ -54,9 +54,9 @@ int main(void)
}
else __gen_e_acsl_and = 0;
__e_acsl_assert(__gen_e_acsl_and,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(q)",15);
+ (char *)"mem_access: \\valid_read(q)",14);
__e_acsl_assert(*q == G,(char *)"Assertion",(char *)"main",
- (char *)"*q == G",15);
+ (char *)"*q == G",14);
}
__retres = 0;
__e_acsl_delete_block((void *)(& P));
diff --git a/src/plugins/e-acsl/tests/memory/call.c b/src/plugins/e-acsl/tests/memory/call.c
index bbb9e9300d4..6d6cdccc6bd 100644
--- a/src/plugins/e-acsl/tests/memory/call.c
+++ b/src/plugins/e-acsl/tests/memory/call.c
@@ -1,12 +1,9 @@
/* run.config
COMMENT: function call
- STDOPT: +"-no-val-alloc-returns-null"
*/
#include <stdlib.h>
-//extern void *malloc(unsigned int size);
-
/*@ ensures \valid(\result); */
int *f(int *x, int *y) {
*y = 1;
diff --git a/src/plugins/e-acsl/tests/memory/freeable.c b/src/plugins/e-acsl/tests/memory/freeable.c
index 4ec6fcf57c1..86422bb512c 100644
--- a/src/plugins/e-acsl/tests/memory/freeable.c
+++ b/src/plugins/e-acsl/tests/memory/freeable.c
@@ -1,6 +1,5 @@
/* run.config
COMMENT: \freeable
- STDOPT:
*/
#include <stdlib.h>
diff --git a/src/plugins/e-acsl/tests/memory/initialized.c b/src/plugins/e-acsl/tests/memory/initialized.c
index 752facb20f2..4af4918caa2 100644
--- a/src/plugins/e-acsl/tests/memory/initialized.c
+++ b/src/plugins/e-acsl/tests/memory/initialized.c
@@ -1,5 +1,4 @@
/* run.config
- STDOPT:
COMMENT: Behaviours of the \initialized E-ACSL predicate
*/
diff --git a/src/plugins/e-acsl/tests/memory/local_init.c b/src/plugins/e-acsl/tests/memory/local_init.c
index 417add7d562..2c7440cdb2f 100644
--- a/src/plugins/e-acsl/tests/memory/local_init.c
+++ b/src/plugins/e-acsl/tests/memory/local_init.c
@@ -1,7 +1,7 @@
/* run.config
COMMENT: test of a local initializer which contains an annotation
LOG: gen_@PTEST_NAME@.c
- STDOPT: #"-eva -e-acsl-prepare -e-acsl-share ./share/e-acsl -lib-entry -then"
+ STDOPT: #"-lib-entry -eva -e-acsl-prepare -e-acsl-share ./share/e-acsl -then -no-lib-entry"
*/
int X = 0;
diff --git a/src/plugins/e-acsl/tests/memory/local_var.c b/src/plugins/e-acsl/tests/memory/local_var.c
index 21ad932233f..e7239f6e861 100644
--- a/src/plugins/e-acsl/tests/memory/local_var.c
+++ b/src/plugins/e-acsl/tests/memory/local_var.c
@@ -1,12 +1,9 @@
/* run.config
COMMENT: allocation and de-allocation of local variables
- STDOPT: +"-no-val-alloc-returns-null"
*/
#include <stdlib.h>
-extern void *malloc(size_t size);
-
struct list {
int element;
struct list * next;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/freeable.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/freeable.res.oracle
index 960337255a2..bed0b61add3 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/freeable.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/freeable.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/memory/freeable.c:15: Warning: assertion got status unknown.
-[eva:alarm] tests/memory/freeable.c:15: Warning:
+[eva:alarm] tests/memory/freeable.c:14: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/freeable.c:14: Warning:
accessing uninitialized left-value. assert \initialized(&p);
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_call.c b/src/plugins/e-acsl/tests/memory/oracle/gen_call.c
index 546cd79477d..ac3c12211ae 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_call.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_call.c
@@ -56,7 +56,7 @@ int *__gen_e_acsl_f(int *x, int *y)
(void *)__retres,
(void *)(& __retres));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Postcondition",(char *)"f",
- (char *)"\\valid(\\result)",10);
+ (char *)"\\valid(\\result)",7);
__e_acsl_delete_block((void *)(& y));
__e_acsl_delete_block((void *)(& x));
__e_acsl_delete_block((void *)(& __retres));
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_freeable.c b/src/plugins/e-acsl/tests/memory/oracle/gen_freeable.c
index 41fce61b3d2..2dd9560ae9b 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_freeable.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_freeable.c
@@ -26,14 +26,14 @@ int main(void)
/*@ assert Eva: initialization: \initialized(&p); */
__gen_e_acsl_freeable = __e_acsl_freeable((void *)p);
__e_acsl_assert(! __gen_e_acsl_freeable,(char *)"Assertion",
- (char *)"main",(char *)"!\\freeable(p)",15);
+ (char *)"main",(char *)"!\\freeable(p)",14);
}
/*@ assert ¬\freeable((void *)0); */
{
int __gen_e_acsl_freeable_2;
__gen_e_acsl_freeable_2 = __e_acsl_freeable((void *)0);
__e_acsl_assert(! __gen_e_acsl_freeable_2,(char *)"Assertion",
- (char *)"main",(char *)"!\\freeable((void *)0)",16);
+ (char *)"main",(char *)"!\\freeable((void *)0)",15);
}
__e_acsl_full_init((void *)(& p));
p = (int *)malloc((unsigned long)4 * sizeof(int));
@@ -42,14 +42,14 @@ int main(void)
int __gen_e_acsl_freeable_3;
__gen_e_acsl_freeable_3 = __e_acsl_freeable((void *)(p + 1));
__e_acsl_assert(! __gen_e_acsl_freeable_3,(char *)"Assertion",
- (char *)"main",(char *)"!\\freeable(p + 1)",18);
+ (char *)"main",(char *)"!\\freeable(p + 1)",17);
}
/*@ assert \freeable(p); */
{
int __gen_e_acsl_freeable_4;
__gen_e_acsl_freeable_4 = __e_acsl_freeable((void *)p);
__e_acsl_assert(__gen_e_acsl_freeable_4,(char *)"Assertion",
- (char *)"main",(char *)"\\freeable(p)",19);
+ (char *)"main",(char *)"\\freeable(p)",18);
}
free((void *)p);
/*@ assert ¬\freeable(p); */
@@ -57,21 +57,21 @@ int main(void)
int __gen_e_acsl_freeable_5;
__gen_e_acsl_freeable_5 = __e_acsl_freeable((void *)p);
__e_acsl_assert(! __gen_e_acsl_freeable_5,(char *)"Assertion",
- (char *)"main",(char *)"!\\freeable(p)",21);
+ (char *)"main",(char *)"!\\freeable(p)",20);
}
/*@ assert ¬\freeable((char *)array); */
{
int __gen_e_acsl_freeable_6;
__gen_e_acsl_freeable_6 = __e_acsl_freeable((void *)(array));
__e_acsl_assert(! __gen_e_acsl_freeable_6,(char *)"Assertion",
- (char *)"main",(char *)"!\\freeable((char *)array)",24);
+ (char *)"main",(char *)"!\\freeable((char *)array)",23);
}
/*@ assert ¬\freeable(&array[5]); */
{
int __gen_e_acsl_freeable_7;
__gen_e_acsl_freeable_7 = __e_acsl_freeable((void *)(& array[5]));
__e_acsl_assert(! __gen_e_acsl_freeable_7,(char *)"Assertion",
- (char *)"main",(char *)"!\\freeable(&array[5])",25);
+ (char *)"main",(char *)"!\\freeable(&array[5])",24);
}
__retres = 0;
__e_acsl_delete_block((void *)(array));
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_initialized.c b/src/plugins/e-acsl/tests/memory/oracle/gen_initialized.c
index 10ada7d1065..421fbafa443 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_initialized.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_initialized.c
@@ -36,23 +36,23 @@ int main(void)
__e_acsl_full_init((void *)(& q));
/*@ assert \initialized(&A); */
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
- (char *)"\\initialized(&A)",17);
+ (char *)"\\initialized(&A)",16);
/*@ assert \initialized(&B); */
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
- (char *)"\\initialized(&B)",18);
+ (char *)"\\initialized(&B)",17);
/*@ assert \initialized(p); */
{
int __gen_e_acsl_initialized;
__gen_e_acsl_initialized = __e_acsl_initialized((void *)p,sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(p)",19);
+ (char *)"main",(char *)"\\initialized(p)",18);
}
/*@ assert \initialized(q); */
{
int __gen_e_acsl_initialized_2;
__gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)q,sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_2,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(q)",20);
+ (char *)"main",(char *)"\\initialized(q)",19);
}
int a = 0;
__e_acsl_store_block((void *)(& a),(size_t)4);
@@ -70,7 +70,7 @@ int main(void)
__gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& a),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_3,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(&a)",31);
+ (char *)"main",(char *)"\\initialized(&a)",30);
}
/*@ assert ¬\initialized(&b); */
{
@@ -78,21 +78,21 @@ int main(void)
__gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& b),
sizeof(int));
__e_acsl_assert(! __gen_e_acsl_initialized_4,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(&b)",32);
+ (char *)"main",(char *)"!\\initialized(&b)",31);
}
/*@ assert \initialized(p); */
{
int __gen_e_acsl_initialized_5;
__gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)p,sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_5,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(p)",33);
+ (char *)"main",(char *)"\\initialized(p)",32);
}
/*@ assert ¬\initialized(q); */
{
int __gen_e_acsl_initialized_6;
__gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)q,sizeof(int));
__e_acsl_assert(! __gen_e_acsl_initialized_6,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(q)",34);
+ (char *)"main",(char *)"!\\initialized(q)",33);
}
/*@ assert \initialized(&c); */
{
@@ -100,7 +100,7 @@ int main(void)
__gen_e_acsl_initialized_7 = __e_acsl_initialized((void *)(& c),
sizeof(long [2]));
__e_acsl_assert(__gen_e_acsl_initialized_7,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(&c)",35);
+ (char *)"main",(char *)"\\initialized(&c)",34);
}
/*@ assert ¬\initialized(&d); */
{
@@ -108,7 +108,7 @@ int main(void)
__gen_e_acsl_initialized_8 = __e_acsl_initialized((void *)(& d),
sizeof(long [2]));
__e_acsl_assert(! __gen_e_acsl_initialized_8,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(&d)",36);
+ (char *)"main",(char *)"!\\initialized(&d)",35);
}
__e_acsl_full_init((void *)(& b));
b = 0;
@@ -117,7 +117,7 @@ int main(void)
int __gen_e_acsl_initialized_9;
__gen_e_acsl_initialized_9 = __e_acsl_initialized((void *)q,sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_9,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(q)",40);
+ (char *)"main",(char *)"\\initialized(q)",39);
}
/*@ assert \initialized(&b); */
{
@@ -125,7 +125,7 @@ int main(void)
__gen_e_acsl_initialized_10 = __e_acsl_initialized((void *)(& b),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_10,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(&b)",41);
+ (char *)"main",(char *)"\\initialized(&b)",40);
}
__e_acsl_full_init((void *)(& r));
r = d;
@@ -135,7 +135,7 @@ int main(void)
__gen_e_acsl_initialized_11 = __e_acsl_initialized((void *)(d),
sizeof(long));
__e_acsl_assert(! __gen_e_acsl_initialized_11,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized((long *)d)",44);
+ (char *)"main",(char *)"!\\initialized((long *)d)",43);
}
/*@ assert ¬\initialized(&d[1]); */
{
@@ -143,7 +143,7 @@ int main(void)
__gen_e_acsl_initialized_12 = __e_acsl_initialized((void *)(& d[1]),
sizeof(long));
__e_acsl_assert(! __gen_e_acsl_initialized_12,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(&d[1])",45);
+ (char *)"main",(char *)"!\\initialized(&d[1])",44);
}
/*@ assert ¬\initialized(&d); */
{
@@ -151,7 +151,7 @@ int main(void)
__gen_e_acsl_initialized_13 = __e_acsl_initialized((void *)(& d),
sizeof(long [2]));
__e_acsl_assert(! __gen_e_acsl_initialized_13,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(&d)",46);
+ (char *)"main",(char *)"!\\initialized(&d)",45);
}
/*@ assert ¬\initialized(r); */
{
@@ -159,7 +159,7 @@ int main(void)
__gen_e_acsl_initialized_14 = __e_acsl_initialized((void *)r,
sizeof(long));
__e_acsl_assert(! __gen_e_acsl_initialized_14,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(r)",47);
+ (char *)"main",(char *)"!\\initialized(r)",46);
}
/*@ assert ¬\initialized(r + 1); */
{
@@ -167,7 +167,7 @@ int main(void)
__gen_e_acsl_initialized_15 = __e_acsl_initialized((void *)(r + 1),
sizeof(long));
__e_acsl_assert(! __gen_e_acsl_initialized_15,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(r + 1)",48);
+ (char *)"main",(char *)"!\\initialized(r + 1)",47);
}
__e_acsl_initialize((void *)(d),sizeof(long));
d[0] = (long)1;
@@ -177,7 +177,7 @@ int main(void)
__gen_e_acsl_initialized_16 = __e_acsl_initialized((void *)(d),
sizeof(long));
__e_acsl_assert(__gen_e_acsl_initialized_16,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized((long *)d)",51);
+ (char *)"main",(char *)"\\initialized((long *)d)",50);
}
/*@ assert ¬\initialized(&d[1]); */
{
@@ -185,7 +185,7 @@ int main(void)
__gen_e_acsl_initialized_17 = __e_acsl_initialized((void *)(& d[1]),
sizeof(long));
__e_acsl_assert(! __gen_e_acsl_initialized_17,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(&d[1])",52);
+ (char *)"main",(char *)"!\\initialized(&d[1])",51);
}
/*@ assert ¬\initialized(&d); */
{
@@ -193,7 +193,7 @@ int main(void)
__gen_e_acsl_initialized_18 = __e_acsl_initialized((void *)(& d),
sizeof(long [2]));
__e_acsl_assert(! __gen_e_acsl_initialized_18,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(&d)",53);
+ (char *)"main",(char *)"!\\initialized(&d)",52);
}
/*@ assert \initialized(r); */
{
@@ -201,7 +201,7 @@ int main(void)
__gen_e_acsl_initialized_19 = __e_acsl_initialized((void *)r,
sizeof(long));
__e_acsl_assert(__gen_e_acsl_initialized_19,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(r)",54);
+ (char *)"main",(char *)"\\initialized(r)",53);
}
/*@ assert ¬\initialized(r + 1); */
{
@@ -209,7 +209,7 @@ int main(void)
__gen_e_acsl_initialized_20 = __e_acsl_initialized((void *)(r + 1),
sizeof(long));
__e_acsl_assert(! __gen_e_acsl_initialized_20,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(r + 1)",55);
+ (char *)"main",(char *)"!\\initialized(r + 1)",54);
}
__e_acsl_initialize((void *)(& d[1]),sizeof(long));
d[1] = (long)1;
@@ -219,7 +219,7 @@ int main(void)
__gen_e_acsl_initialized_21 = __e_acsl_initialized((void *)(d),
sizeof(long));
__e_acsl_assert(__gen_e_acsl_initialized_21,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized((long *)d)",58);
+ (char *)"main",(char *)"\\initialized((long *)d)",57);
}
/*@ assert \initialized(&d[1]); */
{
@@ -227,7 +227,7 @@ int main(void)
__gen_e_acsl_initialized_22 = __e_acsl_initialized((void *)(& d[1]),
sizeof(long));
__e_acsl_assert(__gen_e_acsl_initialized_22,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(&d[1])",59);
+ (char *)"main",(char *)"\\initialized(&d[1])",58);
}
/*@ assert \initialized(&d); */
{
@@ -235,7 +235,7 @@ int main(void)
__gen_e_acsl_initialized_23 = __e_acsl_initialized((void *)(& d),
sizeof(long [2]));
__e_acsl_assert(__gen_e_acsl_initialized_23,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(&d)",60);
+ (char *)"main",(char *)"\\initialized(&d)",59);
}
/*@ assert \initialized(r); */
{
@@ -243,7 +243,7 @@ int main(void)
__gen_e_acsl_initialized_24 = __e_acsl_initialized((void *)r,
sizeof(long));
__e_acsl_assert(__gen_e_acsl_initialized_24,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(r)",61);
+ (char *)"main",(char *)"\\initialized(r)",60);
}
/*@ assert \initialized(r + 1); */
{
@@ -251,7 +251,7 @@ int main(void)
__gen_e_acsl_initialized_25 = __e_acsl_initialized((void *)(r + 1),
sizeof(long));
__e_acsl_assert(__gen_e_acsl_initialized_25,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(r + 1)",62);
+ (char *)"main",(char *)"\\initialized(r + 1)",61);
}
__e_acsl_full_init((void *)(& p));
p = (int *)malloc(sizeof(int *));
@@ -260,7 +260,7 @@ int main(void)
int __gen_e_acsl_initialized_26;
__gen_e_acsl_initialized_26 = __e_acsl_initialized((void *)p,sizeof(int));
__e_acsl_assert(! __gen_e_acsl_initialized_26,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(p)",66);
+ (char *)"main",(char *)"!\\initialized(p)",65);
}
__e_acsl_full_init((void *)(& q));
q = (int *)calloc((unsigned long)1,sizeof(int));
@@ -269,7 +269,7 @@ int main(void)
int __gen_e_acsl_initialized_27;
__gen_e_acsl_initialized_27 = __e_acsl_initialized((void *)q,sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_27,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(q)",70);
+ (char *)"main",(char *)"\\initialized(q)",69);
}
__e_acsl_full_init((void *)(& q));
q = (int *)realloc((void *)q,(unsigned long)2 * sizeof(int));
@@ -278,7 +278,7 @@ int main(void)
int __gen_e_acsl_initialized_28;
__gen_e_acsl_initialized_28 = __e_acsl_initialized((void *)q,sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_28,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(q)",75);
+ (char *)"main",(char *)"\\initialized(q)",74);
}
__e_acsl_full_init((void *)(& q));
q ++;
@@ -287,7 +287,7 @@ int main(void)
int __gen_e_acsl_initialized_29;
__gen_e_acsl_initialized_29 = __e_acsl_initialized((void *)q,sizeof(int));
__e_acsl_assert(! __gen_e_acsl_initialized_29,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(q)",77);
+ (char *)"main",(char *)"!\\initialized(q)",76);
}
__e_acsl_full_init((void *)(& q));
q --;
@@ -299,14 +299,14 @@ int main(void)
/*@ assert Eva: dangling_pointer: ¬\dangling(&p); */
__gen_e_acsl_initialized_30 = __e_acsl_initialized((void *)p,sizeof(int));
__e_acsl_assert(! __gen_e_acsl_initialized_30,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(p)",85);
+ (char *)"main",(char *)"!\\initialized(p)",84);
}
/*@ assert ¬\initialized(q); */
{
int __gen_e_acsl_initialized_31;
__gen_e_acsl_initialized_31 = __e_acsl_initialized((void *)q,sizeof(int));
__e_acsl_assert(! __gen_e_acsl_initialized_31,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(q)",86);
+ (char *)"main",(char *)"!\\initialized(q)",85);
}
__e_acsl_full_init((void *)(& q));
q = (int *)(& q - 1024 * 5);
@@ -317,7 +317,7 @@ int main(void)
int __gen_e_acsl_initialized_32;
__gen_e_acsl_initialized_32 = __e_acsl_initialized((void *)q,sizeof(int));
__e_acsl_assert(! __gen_e_acsl_initialized_32,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(q)",94);
+ (char *)"main",(char *)"!\\initialized(q)",93);
}
__e_acsl_full_init((void *)(& p));
p = (int *)0;
@@ -326,7 +326,7 @@ int main(void)
int __gen_e_acsl_initialized_33;
__gen_e_acsl_initialized_33 = __e_acsl_initialized((void *)p,sizeof(int));
__e_acsl_assert(! __gen_e_acsl_initialized_33,(char *)"Assertion",
- (char *)"main",(char *)"!\\initialized(p)",97);
+ (char *)"main",(char *)"!\\initialized(p)",96);
}
int size = 100;
char *partsc = malloc((unsigned long)size * sizeof(char));
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c b/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c
index daf584a9f58..2556be7d024 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c
@@ -9,12 +9,29 @@ int f(void)
return x;
}
+void __e_acsl_globals_init(void)
+{
+ static char __e_acsl_already_run = 0;
+ if (! __e_acsl_already_run) {
+ __e_acsl_already_run = 1;
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_full_init((void *)(& p));
+ __e_acsl_store_block((void *)(& X),(size_t)4);
+ __e_acsl_full_init((void *)(& X));
+ }
+ return;
+}
+
int main(void)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_globals_init();
f();
__retres = 0;
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_delete_block((void *)(& X));
+ __e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_local_var.c b/src/plugins/e-acsl/tests/memory/oracle/gen_local_var.c
index 787629e8400..567bf6af140 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_local_var.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_local_var.c
@@ -26,7 +26,7 @@ struct list *add(struct list *l, int i)
}
else __gen_e_acsl_and = 0;
__e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"add",
- (char *)"\\valid(new)",18);
+ (char *)"\\valid(new)",15);
}
__e_acsl_initialize((void *)(& new->element),sizeof(int));
new->element = i;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_valid.c b/src/plugins/e-acsl/tests/memory/oracle/gen_valid.c
index e2149de7ee4..26b8a81c4b8 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_valid.c
@@ -28,7 +28,7 @@ int *f(int *x)
}
else __gen_e_acsl_and = 0;
__e_acsl_assert(! __gen_e_acsl_and,(char *)"Assertion",(char *)"f",
- (char *)"!\\valid(y)",17);
+ (char *)"!\\valid(y)",13);
}
__e_acsl_full_init((void *)(& y));
y = x;
@@ -38,7 +38,7 @@ int *f(int *x)
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)x,sizeof(int),(void *)x,
(void *)(& x));
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",(char *)"f",
- (char *)"\\valid(x)",19);
+ (char *)"\\valid(x)",15);
}
__e_acsl_delete_block((void *)(& x));
__e_acsl_delete_block((void *)(& y));
@@ -80,14 +80,14 @@ void g(void)
}
else __gen_e_acsl_and = 0;
__e_acsl_assert(__gen_e_acsl_and,(char *)"RTE",(char *)"g",
- (char *)"mem_access: \\valid_read(p)",28);
+ (char *)"mem_access: \\valid_read(p)",24);
__gen_e_acsl_valid = __e_acsl_valid((void *)*p,sizeof(int),(void *)*p,
(void *)p);
__gen_e_acsl_and_2 = __gen_e_acsl_valid;
}
else __gen_e_acsl_and_2 = 0;
__e_acsl_assert(__gen_e_acsl_and_2,(char *)"Assertion",(char *)"g",
- (char *)"\\valid(*p)",28);
+ (char *)"\\valid(*p)",24);
}
__e_acsl_delete_block((void *)(& p));
__e_acsl_delete_block((void *)(& u));
@@ -107,7 +107,7 @@ int *__gen_e_acsl_f(int *x)
__gen_e_acsl_valid = __e_acsl_valid((void *)x,sizeof(int),(void *)x,
(void *)(& x));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"f",
- (char *)"\\valid(x)",13);
+ (char *)"\\valid(x)",9);
}
__retres = f(x);
{
@@ -116,7 +116,7 @@ int *__gen_e_acsl_f(int *x)
(void *)__retres,
(void *)(& __retres));
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Postcondition",(char *)"f",
- (char *)"\\valid(\\result)",14);
+ (char *)"\\valid(\\result)",10);
__e_acsl_delete_block((void *)(& x));
__e_acsl_delete_block((void *)(& __retres));
return __retres;
@@ -190,7 +190,7 @@ int main(void)
}
else __gen_e_acsl_and_4 = 0;
__e_acsl_assert(__gen_e_acsl_and_4,(char *)"Assertion",(char *)"main",
- (char *)"!\\valid(a) && !\\valid(b) && !\\valid(X)",33);
+ (char *)"!\\valid(a) && !\\valid(b) && !\\valid(X)",29);
}
__e_acsl_full_init((void *)(& a));
a = (int *)malloc(sizeof(int));
@@ -232,7 +232,7 @@ int main(void)
}
else __gen_e_acsl_and_8 = 0;
__e_acsl_assert(__gen_e_acsl_and_8,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(a) && !\\valid(b) && !\\valid(X)",35);
+ (char *)"\\valid(a) && !\\valid(b) && !\\valid(X)",31);
}
X = a;
/*@ assert \valid(a) ∧ ¬\valid(b) ∧ \valid(X); */
@@ -273,7 +273,7 @@ int main(void)
}
else __gen_e_acsl_and_12 = 0;
__e_acsl_assert(__gen_e_acsl_and_12,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(a) && !\\valid(b) && \\valid(X)",37);
+ (char *)"\\valid(a) && !\\valid(b) && \\valid(X)",33);
}
__e_acsl_full_init((void *)(& b));
b = __gen_e_acsl_f(& n);
@@ -315,7 +315,7 @@ int main(void)
}
else __gen_e_acsl_and_16 = 0;
__e_acsl_assert(__gen_e_acsl_and_16,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(a) && \\valid(b) && \\valid(X)",39);
+ (char *)"\\valid(a) && \\valid(b) && \\valid(X)",35);
}
X = b;
/*@ assert \valid(a) ∧ \valid(b) ∧ \valid(X); */
@@ -356,7 +356,7 @@ int main(void)
}
else __gen_e_acsl_and_20 = 0;
__e_acsl_assert(__gen_e_acsl_and_20,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(a) && \\valid(b) && \\valid(X)",41);
+ (char *)"\\valid(a) && \\valid(b) && \\valid(X)",37);
}
__e_acsl_full_init((void *)(& c));
c = & a;
@@ -384,14 +384,14 @@ int main(void)
}
else __gen_e_acsl_and_21 = 0;
__e_acsl_assert(__gen_e_acsl_and_21,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(c)",44);
+ (char *)"mem_access: \\valid_read(c)",40);
__gen_e_acsl_valid_16 = __e_acsl_valid((void *)*c,sizeof(int),
(void *)*c,(void *)c);
__gen_e_acsl_and_22 = __gen_e_acsl_valid_16;
}
else __gen_e_acsl_and_22 = 0;
__e_acsl_assert(__gen_e_acsl_and_22,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(*c)",44);
+ (char *)"\\valid(*c)",40);
}
/*@ assert \valid(*(*d)); */
{
@@ -401,7 +401,7 @@ int main(void)
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)d,sizeof(int **),
(void *)d,(void *)(& d));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(d)",45);
+ (char *)"mem_access: \\valid_read(d)",41);
__gen_e_acsl_initialized_13 = __e_acsl_initialized((void *)*d,
sizeof(int *));
if (__gen_e_acsl_initialized_13) {
@@ -428,7 +428,7 @@ int main(void)
}
else __gen_e_acsl_and_23 = 0;
__e_acsl_assert(__gen_e_acsl_and_23,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(d)",45);
+ (char *)"mem_access: \\valid_read(d)",41);
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)*d,
sizeof(int *),
(void *)*d,(void *)d);
@@ -436,7 +436,7 @@ int main(void)
}
else __gen_e_acsl_and_24 = 0;
__e_acsl_assert(__gen_e_acsl_and_24,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(*d)",45);
+ (char *)"mem_access: \\valid_read(*d)",41);
__gen_e_acsl_initialized_16 = __e_acsl_initialized((void *)(& d),
sizeof(int ***));
if (__gen_e_acsl_initialized_16) {
@@ -449,14 +449,14 @@ int main(void)
}
else __gen_e_acsl_and_25 = 0;
__e_acsl_assert(__gen_e_acsl_and_25,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(d)",45);
+ (char *)"mem_access: \\valid_read(d)",41);
__gen_e_acsl_valid_17 = __e_acsl_valid((void *)*(*d),sizeof(int),
(void *)*(*d),(void *)*d);
__gen_e_acsl_and_26 = __gen_e_acsl_valid_17;
}
else __gen_e_acsl_and_26 = 0;
__e_acsl_assert(__gen_e_acsl_and_26,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(*(*d))",45);
+ (char *)"\\valid(*(*d))",41);
}
free((void *)a);
/*@ assert ¬\valid(a) ∧ \valid(b) ∧ \valid(X); */
@@ -498,7 +498,7 @@ int main(void)
}
else __gen_e_acsl_and_30 = 0;
__e_acsl_assert(__gen_e_acsl_and_30,(char *)"Assertion",(char *)"main",
- (char *)"!\\valid(a) && \\valid(b) && \\valid(X)",47);
+ (char *)"!\\valid(a) && \\valid(b) && \\valid(X)",43);
}
/*@ assert \valid(&Z); */
{
@@ -506,7 +506,7 @@ int main(void)
__gen_e_acsl_valid_21 = __e_acsl_valid((void *)(& Z),sizeof(int),
(void *)(& Z),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_21,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(&Z)",48);
+ (char *)"\\valid(&Z)",44);
}
g();
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_alias.c
index 240cfaf9d6f..e3bdcf3e194 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_alias.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_alias.c
@@ -40,7 +40,7 @@ int main(void)
}
else __gen_e_acsl_and_3 = 0;
__e_acsl_assert(__gen_e_acsl_and_3,(char *)"Assertion",(char *)"main",
- (char *)"!\\valid(a) && !\\valid(b)",10);
+ (char *)"!\\valid(a) && !\\valid(b)",9);
}
__e_acsl_full_init((void *)(& a));
a = (int *)malloc(sizeof(int));
@@ -78,7 +78,7 @@ int main(void)
}
else __gen_e_acsl_and_6 = 0;
__e_acsl_assert(__gen_e_acsl_and_6,(char *)"Assertion",(char *)"main",
- (char *)"\\valid(a) && \\valid(b)",14);
+ (char *)"\\valid(a) && \\valid(b)",13);
}
/*@ assert *b ≡ n; */
{
@@ -94,9 +94,9 @@ int main(void)
}
else __gen_e_acsl_and_7 = 0;
__e_acsl_assert(__gen_e_acsl_and_7,(char *)"RTE",(char *)"main",
- (char *)"mem_access: \\valid_read(b)",15);
+ (char *)"mem_access: \\valid_read(b)",14);
__e_acsl_assert(*b == n,(char *)"Assertion",(char *)"main",
- (char *)"*b == n",15);
+ (char *)"*b == n",14);
}
free((void *)b);
/*@ assert ¬\valid(a) ∧ ¬\valid(b); */
@@ -130,7 +130,7 @@ int main(void)
}
else __gen_e_acsl_and_10 = 0;
__e_acsl_assert(__gen_e_acsl_and_10,(char *)"Assertion",(char *)"main",
- (char *)"!\\valid(a) && !\\valid(b)",17);
+ (char *)"!\\valid(a) && !\\valid(b)",16);
}
__retres = 0;
__e_acsl_delete_block((void *)(& b));
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
index a003b9a603b..6395c435c6c 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
@@ -88,7 +88,7 @@ struct list *__gen_e_acsl_f(struct list *l)
(void *)(& l->next),
(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"f",
- (char *)"mem_access: \\valid_read(&l->next)",18);
+ (char *)"mem_access: \\valid_read(&l->next)",17);
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)l->next,
sizeof(struct list),
(void *)l->next,
@@ -110,13 +110,13 @@ struct list *__gen_e_acsl_f(struct list *l)
if (! __gen_e_acsl_at) __gen_e_acsl_implies = 1;
else __gen_e_acsl_implies = __retres == __gen_e_acsl_at_2;
__e_acsl_assert(__gen_e_acsl_implies,(char *)"Postcondition",(char *)"f",
- (char *)"\\old(l == \\null) ==> \\result == \\old(l)",16);
+ (char *)"\\old(l == \\null) ==> \\result == \\old(l)",15);
if (! __gen_e_acsl_at_3) __gen_e_acsl_implies_2 = 1;
else __gen_e_acsl_implies_2 = __retres == __gen_e_acsl_at_4;
__e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Postcondition",
(char *)"f",
(char *)"\\old(!\\valid{Here}(l) || !\\valid{Here}(l->next)) ==> \\result == \\old(l)",
- 19);
+ 18);
__e_acsl_delete_block((void *)(& l));
__e_acsl_delete_block((void *)(& __retres));
return __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_vector.c b/src/plugins/e-acsl/tests/memory/oracle/gen_vector.c
index ed998b8cb0f..eff00e76dd7 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_vector.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_vector.c
@@ -7,6 +7,47 @@ int *new_inversed(int len, int *v)
int i;
int *p;
__e_acsl_store_block((void *)(& p),(size_t)8);
+ /*@ assert
+ \valid(v) ∧ \offset(v) + len * sizeof(int) ≤ \block_length(v);
+ */
+ {
+ int __gen_e_acsl_valid;
+ int __gen_e_acsl_and;
+ __e_acsl_store_block((void *)(& v),(size_t)8);
+ __gen_e_acsl_valid = __e_acsl_valid((void *)v,sizeof(int),(void *)v,
+ (void *)(& v));
+ if (__gen_e_acsl_valid) {
+ unsigned long __gen_e_acsl_offset;
+ __e_acsl_mpz_t __gen_e_acsl_offset_2;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ unsigned long __gen_e_acsl_block_length;
+ __e_acsl_mpz_t __gen_e_acsl_block_length_2;
+ int __gen_e_acsl_le;
+ __gen_e_acsl_offset = __e_acsl_offset((void *)v);
+ __gmpz_init_set_ui(__gen_e_acsl_offset_2,__gen_e_acsl_offset);
+ __gmpz_init_set_si(__gen_e_acsl_,len * 4L);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_offset_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gen_e_acsl_block_length = __e_acsl_block_length((void *)v);
+ __gmpz_init_set_ui(__gen_e_acsl_block_length_2,
+ __gen_e_acsl_block_length);
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_block_length_2));
+ __gen_e_acsl_and = __gen_e_acsl_le <= 0;
+ __gmpz_clear(__gen_e_acsl_offset_2);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl_block_length_2);
+ }
+ else __gen_e_acsl_and = 0;
+ __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",
+ (char *)"new_inversed",
+ (char *)"\\valid(v) && \\offset(v) + len * sizeof(int) <= \\block_length(v)",
+ 11);
+ }
__e_acsl_full_init((void *)(& p));
p = (int *)malloc(sizeof(int) * (unsigned long)len);
i = 0;
@@ -15,6 +56,7 @@ int *new_inversed(int len, int *v)
*(p + i) = *(v + ((len - i) - 1));
i ++;
}
+ __e_acsl_delete_block((void *)(& v));
__e_acsl_delete_block((void *)(& p));
return p;
}
@@ -29,6 +71,14 @@ int main(void)
int v1[3] = {1, 2, x};
__e_acsl_store_block((void *)(v1),(size_t)12);
__e_acsl_full_init((void *)(& v1));
+ /*@ assert \valid(&v1[2]); */
+ {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(& v1[2]),sizeof(int),
+ (void *)(& v1[2]),(void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&v1[2])",21);
+ }
LAST = v1[2];
/*@ assert \initialized(&v1[2]); */
{
@@ -36,7 +86,7 @@ int main(void)
__gen_e_acsl_initialized = __e_acsl_initialized((void *)(& v1[2]),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(&v1[2])",24);
+ (char *)"main",(char *)"\\initialized(&v1[2])",23);
}
__e_acsl_full_init((void *)(& v2));
v2 = new_inversed(3,v1);
@@ -48,11 +98,11 @@ int main(void)
__gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(v2 + 2),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_2,(char *)"Assertion",
- (char *)"main",(char *)"\\initialized(v2 + 2)",27);
+ (char *)"main",(char *)"\\initialized(v2 + 2)",26);
}
/*@ assert LAST ≡ 1; */
__e_acsl_assert(LAST == 1,(char *)"Assertion",(char *)"main",
- (char *)"LAST == 1",28);
+ (char *)"LAST == 1",27);
free((void *)v2);
__retres = 0;
__e_acsl_delete_block((void *)(& v2));
diff --git a/src/plugins/e-acsl/tests/memory/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/initialized.res.oracle
index f7e7728886d..2a7b78f4dd4 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/initialized.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/initialized.res.oracle
@@ -1,7 +1,7 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/memory/initialized.c:85: Warning:
+[eva:alarm] tests/memory/initialized.c:84: Warning:
assertion got status unknown.
-[eva:alarm] tests/memory/initialized.c:85: Warning:
+[eva:alarm] tests/memory/initialized.c:84: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&p);
diff --git a/src/plugins/e-acsl/tests/memory/oracle/local_init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/local_init.res.oracle
index 97c5a744275..e5104fb7e86 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/local_init.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/local_init.res.oracle
@@ -2,5 +2,3 @@
out of bounds read. assert \valid_read(p);
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/memory/local_init.c:11: Warning:
- out of bounds read. assert \valid_read(p);
diff --git a/src/plugins/e-acsl/tests/memory/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/valid.res.oracle
index cd7f1aa8784..10d60024c84 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/valid.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/memory/valid.c:47: Warning:
+[eva:alarm] tests/memory/valid.c:43: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&a);
diff --git a/src/plugins/e-acsl/tests/memory/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/valid_alias.res.oracle
index 194beb0f957..6fdc0e52c0e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/valid_alias.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/memory/valid_alias.c:17: Warning:
+[eva:alarm] tests/memory/valid_alias.c:16: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&a);
diff --git a/src/plugins/e-acsl/tests/memory/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/vector.res.oracle
index 32603d785fa..f511ea7c117 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/vector.res.oracle
@@ -1,5 +1,7 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/memory/vector.c:26: Warning:
+[eva:alarm] tests/memory/vector.c:11: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/vector.c:25: Warning:
accessing uninitialized left-value. assert \initialized(v2 + 2);
-[eva:alarm] tests/memory/vector.c:28: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/vector.c:27: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/memory/valid.c b/src/plugins/e-acsl/tests/memory/valid.c
index aa2f4de1d73..9d48defa048 100644
--- a/src/plugins/e-acsl/tests/memory/valid.c
+++ b/src/plugins/e-acsl/tests/memory/valid.c
@@ -1,13 +1,9 @@
/* run.config
COMMENT: \valid
- STDOPT: +"-no-val-alloc-returns-null"
*/
#include "stdlib.h"
-extern void *malloc(size_t p);
-extern void free(void* p);
-
int *X, Z;
/*@ requires \valid(x);
diff --git a/src/plugins/e-acsl/tests/memory/valid_alias.c b/src/plugins/e-acsl/tests/memory/valid_alias.c
index 78808ce2816..8ec383b38de 100644
--- a/src/plugins/e-acsl/tests/memory/valid_alias.c
+++ b/src/plugins/e-acsl/tests/memory/valid_alias.c
@@ -1,6 +1,5 @@
/* run.config
COMMENT: \valid in presence of aliasing
- STDOPT: +"-no-val-alloc-returns-null"
*/
#include "stdlib.h"
diff --git a/src/plugins/e-acsl/tests/memory/valid_in_contract.c b/src/plugins/e-acsl/tests/memory/valid_in_contract.c
index c5746dae3bb..ed7db447fc4 100644
--- a/src/plugins/e-acsl/tests/memory/valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/memory/valid_in_contract.c
@@ -1,6 +1,5 @@
/* run.config
COMMENT: function contract involving \valid
- STDOPT:
*/
#include <stdlib.h>
diff --git a/src/plugins/e-acsl/tests/memory/vector.c b/src/plugins/e-acsl/tests/memory/vector.c
index 0f144381f62..bda4a716fef 100644
--- a/src/plugins/e-acsl/tests/memory/vector.c
+++ b/src/plugins/e-acsl/tests/memory/vector.c
@@ -1,6 +1,5 @@
/* run.config
COMMENT: function call + initialized
- STDOPT: +"-no-val-alloc-returns-null"
*/
#include<stdlib.h>
@@ -9,7 +8,7 @@ int LAST;
int* new_inversed(int len, int *v) {
int i, *p;
- // @ assert \valid(v) && \offset(v)+len*sizeof(int) <= \block_length(v);
+ //@ assert \valid(v) && \offset(v)+len*sizeof(int) <= \block_length(v);
p = malloc(sizeof(int)*len);
for(i=0; i<len; i++)
p[i] = v[len-i-1];
@@ -19,7 +18,7 @@ int* new_inversed(int len, int *v) {
int main(void) {
int x = 3;
int v1[3]= { 1, 2, x }, *v2;
- // @ assert \valid(&v1[2]);
+ //@ assert \valid(&v1[2]);
LAST = v1[2];
//@ assert \initialized(v1+2);
v2 = new_inversed(3, v1);
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c
index 6409e05e1b4..33d62b000f2 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c
@@ -65,7 +65,7 @@ int main(int argc, char const **argv)
__gen_e_acsl_or = __gen_e_acsl_and;
}
__e_acsl_assert(__gen_e_acsl_or,(char *)"Assertion",(char *)"main",
- (char *)"g1 == \\null || \\valid(g1)",14);
+ (char *)"g1 == \\null || \\valid(g1)",13);
}
/*@ assert g2 ≡ \null ∨ \valid(g2); */
{
@@ -89,7 +89,7 @@ int main(int argc, char const **argv)
__gen_e_acsl_or_2 = __gen_e_acsl_and_2;
}
__e_acsl_assert(__gen_e_acsl_or_2,(char *)"Assertion",(char *)"main",
- (char *)"g2 == \\null || \\valid(g2)",15);
+ (char *)"g2 == \\null || \\valid(g2)",14);
}
__retres = 0;
__e_acsl_delete_block((void *)(& g2));
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
index f5fa7a17110..9e376cf88d3 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
@@ -15,13 +15,13 @@
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:484: Warning:
function __gen_e_acsl_getenv: postcondition 'null_or_valid_result' got status unknown.
-[eva:alarm] tests/temporal/t_getenv.c:14: Warning: assertion got status unknown.
-[eva:alarm] tests/temporal/t_getenv.c:14: Warning:
+[eva:alarm] tests/temporal/t_getenv.c:13: Warning: assertion got status unknown.
+[eva:alarm] tests/temporal/t_getenv.c:13: Warning:
pointer comparison. assert \pointer_comparable((void *)g1, (void *)0);
-[eva:alarm] tests/temporal/t_getenv.c:14: Warning:
+[eva:alarm] tests/temporal/t_getenv.c:13: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/temporal/t_getenv.c:15: Warning: assertion got status unknown.
-[eva:alarm] tests/temporal/t_getenv.c:15: Warning:
+[eva:alarm] tests/temporal/t_getenv.c:14: Warning: assertion got status unknown.
+[eva:alarm] tests/temporal/t_getenv.c:14: Warning:
pointer comparison. assert \pointer_comparable((void *)g2, (void *)0);
-[eva:alarm] tests/temporal/t_getenv.c:15: Warning:
+[eva:alarm] tests/temporal/t_getenv.c:14: Warning:
function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/temporal/t_getenv.c b/src/plugins/e-acsl/tests/temporal/t_getenv.c
index 41dfd454996..1f5066ee368 100644
--- a/src/plugins/e-acsl/tests/temporal/t_getenv.c
+++ b/src/plugins/e-acsl/tests/temporal/t_getenv.c
@@ -1,6 +1,5 @@
/* run.config
COMMENT: Check temporal validity of environment string (via getenv function)
- STDOPT: #"-eva-warn-key=libc:unsupported-spec=inactive"
*/
#include <stdlib.h>
#include <errno.h>
--
GitLab