diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.0.res.oracle
index c0ae2df3d3eb9bd2ab2f5dc92f7397d7b3a997cd..5170b1fe4ba40ee38526fcf4da7a7232988f4b14 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.0.res.oracle
@@ -35,15 +35,10 @@
allocating variable __malloc_main_l28
[eva] using specification for function __e_acsl_store_block
[eva] using specification for function __e_acsl_full_init
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:37: Warning:
- out of bounds write. assert \valid(__gen_e_acsl_at_4 + 0);
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
- out of bounds write.
- assert \valid(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j_2 - 2));
[eva] tests/gmp/at_on-purely-logic-variables.c:29:
starting to merge loop iterations
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:28: Warning:
- out of bounds write. assert \valid(__gen_e_acsl_at + 0);
+[eva] tests/gmp/at_on-purely-logic-variables.c:57:
+ starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:57: Warning:
out of bounds write.
assert
@@ -51,22 +46,8 @@
(int)((int)((int)(__gen_e_acsl_u_6 - 10) * 300) +
(int)((int)((int)((int)(__gen_e_acsl_v_6 - -10) - 1) * 100) +
(int)((int)(__gen_e_acsl_w_2 - 100) - 1))));
-[eva] tests/gmp/at_on-purely-logic-variables.c:57:
- starting to merge loop iterations
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
- out of bounds write.
- assert
- \valid(__gen_e_acsl_at_6 +
- (int)((int)((int)(__gen_e_acsl_u_4 - 9) * 32) +
- (int)((int)(__gen_e_acsl_v_4 - -5) - 1)));
[eva] tests/gmp/at_on-purely-logic-variables.c:45:
starting to merge loop iterations
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:34: Warning:
- out of bounds write.
- assert
- \valid(__gen_e_acsl_at_3 +
- (int)((int)((int)(__gen_e_acsl_u_2 - 9) * 11) +
- (int)((int)(__gen_e_acsl_v_2 - -5) - 1)));
[eva] tests/gmp/at_on-purely-logic-variables.c:34:
starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:28: Warning:
@@ -75,74 +56,52 @@
[eva] using specification for function __e_acsl_assert
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
assertion got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
- function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2));
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
- out of bounds read.
- assert \valid_read(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j - 2));
[eva] tests/gmp/at_on-purely-logic-variables.c:29:
starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:31: Warning:
assertion got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:34: Warning:
- function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:33: Warning:
accessing uninitialized left-value.
assert
\initialized(__gen_e_acsl_at_3 +
((__gen_e_acsl_u - 9) * 11 + ((__gen_e_acsl_v - -5) - 1)));
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:33: Warning:
- out of bounds read.
- assert
- \valid_read(__gen_e_acsl_at_3 +
- (int)((int)((int)(__gen_e_acsl_u - 9) * 11) +
- (int)((int)(__gen_e_acsl_v - -5) - 1)));
[eva] tests/gmp/at_on-purely-logic-variables.c:33:
starting to merge loop iterations
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:34: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:37: Warning:
assertion got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
- out of bounds write.
- assert \valid(__gen_e_acsl_at_5 + (int)((int)(__gen_e_acsl_k_4 - -9) - 1));
[eva] tests/gmp/at_on-purely-logic-variables.c:41:
starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
assertion got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
- function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1));
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
- out of bounds read.
- assert
- \valid_read(__gen_e_acsl_at_5 + (int)((int)(__gen_e_acsl_k_3 - -9) - 1));
[eva] tests/gmp/at_on-purely-logic-variables.c:41:
starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:43: Warning:
assertion got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
- function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:44: Warning:
accessing uninitialized left-value.
assert
\initialized(__gen_e_acsl_at_6 +
((__gen_e_acsl_u_3 - 9) * 32 + ((__gen_e_acsl_v_3 - -5) - 1)));
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:44: Warning:
- out of bounds read.
- assert
- \valid_read(__gen_e_acsl_at_6 +
- (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +
- (int)((int)(__gen_e_acsl_v_3 - -5) - 1)));
[eva] tests/gmp/at_on-purely-logic-variables.c:44:
starting to merge loop iterations
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva] tests/gmp/at_on-purely-logic-variables.c:8:
allocating variable __malloc___gen_e_acsl_f_l8
[eva] tests/gmp/at_on-purely-logic-variables.c:8:
@@ -151,68 +110,44 @@
allocating variable __malloc___gen_e_acsl_f_l7
[eva] tests/gmp/at_on-purely-logic-variables.c:7:
allocating variable __malloc___gen_e_acsl_f_l7_0
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:8: Warning:
- out of bounds write. assert \valid(__gen_e_acsl_at_4 + 0);
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:8: Warning:
- out of bounds write. assert \valid(__gen_e_acsl_at_3 + 0);
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
- out of bounds write.
- assert \valid(__gen_e_acsl_at_2 + (int)((int)(__gen_e_acsl_n_3 - 1) - 1));
[eva] tests/gmp/at_on-purely-logic-variables.c:7:
starting to merge loop iterations
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
- out of bounds write.
- assert \valid(__gen_e_acsl_at + (int)((int)(__gen_e_acsl_n_2 - 1) - 1));
[eva] tests/gmp/at_on-purely-logic-variables.c:7:
starting to merge loop iterations
[eva] using specification for function __e_acsl_delete_block
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
- function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1));
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
- out of bounds read.
- assert \valid_read(__gen_e_acsl_at + (int)((int)(__gen_e_acsl_n - 1) - 1));
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
- function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
- out of bounds read.
- assert \valid_read(__gen_e_acsl_at_2 + (int)((int)(__gen_e_acsl_n - 1) - 1));
[eva] tests/gmp/at_on-purely-logic-variables.c:6:
starting to merge loop iterations
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:6: Warning:
function __gen_e_acsl_f: postcondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:8: Warning:
function __gen_e_acsl_f: postcondition got status unknown.
[eva] tests/gmp/at_on-purely-logic-variables.c:16:
allocating variable __malloc_g_l16
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
- out of bounds write.
- assert \valid(__gen_e_acsl_at + (int)(__gen_e_acsl_w_2 - 3));
[eva] tests/gmp/at_on-purely-logic-variables.c:16:
starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
assertion got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
- function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at + (__gen_e_acsl_w - 3));
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
- out of bounds read.
- assert \valid_read(__gen_e_acsl_at + (int)(__gen_e_acsl_w - 3));
[eva] tests/gmp/at_on-purely-logic-variables.c:16:
starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:54: Warning:
assertion got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:57: Warning:
- function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:56: Warning:
accessing uninitialized left-value.
assert
@@ -220,13 +155,6 @@
((__gen_e_acsl_u_5 - 10) * 300 +
(((__gen_e_acsl_v_5 - -10) - 1) * 100 +
((__gen_e_acsl_w - 100) - 1))));
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:56: Warning:
- out of bounds read.
- assert
- \valid_read(__gen_e_acsl_at_7 +
- (int)((int)((int)(__gen_e_acsl_u_5 - 10) * 300) +
- (int)((int)((int)((int)(__gen_e_acsl_v_5 - -10) - 1) * 100)
- + (int)((int)(__gen_e_acsl_w - 100) - 1))));
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:63: Warning:
assertion got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:65: Warning:
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c
index fa086a5115bb81b6c88406da29dac173c5fa2e98..e60a352da3bcb1f38ff9c2f0f9c3203a6c819bae 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c
@@ -28,10 +28,6 @@ void g(void)
__gen_e_acsl_w_2 = 3;
while (1) {
if (__gen_e_acsl_w_2 < 6) ; else break;
- /*@ assert
- Value: mem_access:
- \valid(__gen_e_acsl_at + (int)(__gen_e_acsl_w_2 - 3));
- */
*(__gen_e_acsl_at + (__gen_e_acsl_w_2 - 3)) = m + (long)__gen_e_acsl_w_2 == 12L;
__gen_e_acsl_w_2 ++;
}
@@ -61,10 +57,6 @@ void g(void)
Value: initialization:
\initialized(__gen_e_acsl_at + (__gen_e_acsl_w - 3));
*/
- /*@ assert
- Value: mem_access:
- \valid_read(__gen_e_acsl_at + (int)(__gen_e_acsl_w - 3));
- */
if (! *(__gen_e_acsl_at + (__gen_e_acsl_w - 3))) ;
else {
__gen_e_acsl_exists = 1;
@@ -109,7 +101,6 @@ int main(void)
{
int __gen_e_acsl_i_4;
__gen_e_acsl_i_4 = 3;
- /*@ assert Value: mem_access: \valid(__gen_e_acsl_at_4 + 0); */
*(__gen_e_acsl_at_4 + 0) = n + (long)__gen_e_acsl_i_4;
}
{
@@ -117,10 +108,6 @@ int main(void)
__gen_e_acsl_j_2 = 2;
while (1) {
if (__gen_e_acsl_j_2 < 5) ; else break;
- /*@ assert
- Value: mem_access:
- \valid(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j_2 - 2));
- */
*(__gen_e_acsl_at_2 + (__gen_e_acsl_j_2 - 2)) = n + (long)__gen_e_acsl_j_2 == 11L;
__gen_e_acsl_j_2 ++;
}
@@ -128,7 +115,6 @@ int main(void)
{
int __gen_e_acsl_i_2;
__gen_e_acsl_i_2 = 3;
- /*@ assert Value: mem_access: \valid(__gen_e_acsl_at + 0); */
*(__gen_e_acsl_at + 0) = n + (long)__gen_e_acsl_i_2 == 10L;
}
;
@@ -195,12 +181,6 @@ int main(void)
else __gen_e_acsl_if_2 = 3;
if (__gen_e_acsl_v_4 <= __gen_e_acsl_if_2) ; else break;
}
- /*@ assert
- Value: mem_access:
- \valid(__gen_e_acsl_at_6 +
- (int)((int)((int)(__gen_e_acsl_u_4 - 9) * 32) +
- (int)((int)(__gen_e_acsl_v_4 - -5) - 1)));
- */
*(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_4 - 9) * 32 + ((__gen_e_acsl_v_4 - -5) - 1))) =
(n + (long)__gen_e_acsl_u_4) + n > 0L;
__gen_e_acsl_v_4 ++;
@@ -223,12 +203,6 @@ int main(void)
long __gen_e_acsl_if;
if (__gen_e_acsl_u_2 > 0) __gen_e_acsl_if = n + (long)__gen_e_acsl_k_2;
else __gen_e_acsl_if = __gen_e_acsl_u_2 + __gen_e_acsl_v_2;
- /*@ assert
- Value: mem_access:
- \valid(__gen_e_acsl_at_3 +
- (int)((int)((int)(__gen_e_acsl_u_2 - 9) * 11) +
- (int)((int)(__gen_e_acsl_v_2 - -5) - 1)));
- */
*(__gen_e_acsl_at_3 + ((__gen_e_acsl_u_2 - 9) * 11 + ((__gen_e_acsl_v_2 - -5) - 1))) =
__gen_e_acsl_if > 0L;
}
@@ -280,10 +254,6 @@ int main(void)
Value: initialization:
\initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2));
*/
- /*@ assert
- Value: mem_access:
- \valid_read(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j - 2));
- */
if (! *(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2))) ;
else {
__gen_e_acsl_exists = 1;
@@ -339,12 +309,6 @@ int main(void)
((__gen_e_acsl_u - 9) * 11 +
((__gen_e_acsl_v - -5) - 1)));
*/
- /*@ assert
- Value: mem_access:
- \valid_read(__gen_e_acsl_at_3 +
- (int)((int)((int)(__gen_e_acsl_u - 9) * 11) +
- (int)((int)(__gen_e_acsl_v - -5) - 1)));
- */
if (*(__gen_e_acsl_at_3 + ((__gen_e_acsl_u - 9) * 11 + ((
__gen_e_acsl_v - -5) - 1))))
;
@@ -393,11 +357,6 @@ int main(void)
__gen_e_acsl_k_4 = -9 + 1;
while (1) {
if (__gen_e_acsl_k_4 < 0) ; else break;
- /*@ assert
- Value: mem_access:
- \valid(__gen_e_acsl_at_5 +
- (int)((int)(__gen_e_acsl_k_4 - -9) - 1));
- */
*(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_4 - -9) - 1)) = m + (long)__gen_e_acsl_k_4;
__gen_e_acsl_k_4 ++;
}
@@ -429,11 +388,6 @@ int main(void)
Value: initialization:
\initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1));
*/
- /*@ assert
- Value: mem_access:
- \valid_read(__gen_e_acsl_at_5 +
- (int)((int)(__gen_e_acsl_k_3 - -9) - 1));
- */
if (! (*(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1)) == 0L))
;
else {
@@ -493,12 +447,6 @@ int main(void)
((__gen_e_acsl_u_3 - 9) * 32 +
((__gen_e_acsl_v_3 - -5) - 1)));
*/
- /*@ assert
- Value: mem_access:
- \valid_read(__gen_e_acsl_at_6 +
- (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +
- (int)((int)(__gen_e_acsl_v_3 - -5) - 1)));
- */
if (*(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_3 - 9) * 32 + (
(__gen_e_acsl_v_3 - -5) - 1))))
;
@@ -589,21 +537,6 @@ int main(void)
(((__gen_e_acsl_v_5 - -10) - 1) * 100 +
((__gen_e_acsl_w - 100) - 1))));
*/
- /*@ assert
- Value: mem_access:
- \valid_read(__gen_e_acsl_at_7 +
- (int)((int)((int)(__gen_e_acsl_u_5 - 10) *
- 300)
- +
- (int)((int)((int)((int)(__gen_e_acsl_v_5
- - -10)
- - 1)
- * 100)
- +
- (int)((int)(__gen_e_acsl_w -
- 100)
- - 1))));
- */
if (! *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_5 - 10) * 300 + (
((__gen_e_acsl_v_5 - -10) - 1) * 100 + (
(__gen_e_acsl_w - 100) - 1)))))
@@ -674,13 +607,11 @@ void __gen_e_acsl_f(int *t)
{
int __gen_e_acsl_m_3;
__gen_e_acsl_m_3 = 4;
- /*@ assert Value: mem_access: \valid(__gen_e_acsl_at_4 + 0); */
*(__gen_e_acsl_at_4 + 0) = *(t + (__gen_e_acsl_m_3 - 4));
}
{
int __gen_e_acsl_m_2;
__gen_e_acsl_m_2 = 4;
- /*@ assert Value: mem_access: \valid(__gen_e_acsl_at_3 + 0); */
*(__gen_e_acsl_at_3 + 0) = *(t + __gen_e_acsl_m_2) == -4;
}
{
@@ -688,10 +619,6 @@ void __gen_e_acsl_f(int *t)
__gen_e_acsl_n_3 = 1 + 1;
while (1) {
if (__gen_e_acsl_n_3 <= 3) ; else break;
- /*@ assert
- Value: mem_access:
- \valid(__gen_e_acsl_at_2 + (int)((int)(__gen_e_acsl_n_3 - 1) - 1));
- */
*(__gen_e_acsl_at_2 + ((__gen_e_acsl_n_3 - 1) - 1)) = *(t + (__gen_e_acsl_n_3 - 1)) > 5;
__gen_e_acsl_n_3 ++;
}
@@ -701,10 +628,6 @@ void __gen_e_acsl_f(int *t)
__gen_e_acsl_n_2 = 1 + 1;
while (1) {
if (__gen_e_acsl_n_2 <= 3) ; else break;
- /*@ assert
- Value: mem_access:
- \valid(__gen_e_acsl_at + (int)((int)(__gen_e_acsl_n_2 - 1) - 1));
- */
*(__gen_e_acsl_at + ((__gen_e_acsl_n_2 - 1) - 1)) = *(t + __gen_e_acsl_n_2) == 12;
__gen_e_acsl_n_2 ++;
}
@@ -737,11 +660,6 @@ void __gen_e_acsl_f(int *t)
Value: initialization:
\initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1));
*/
- /*@ assert
- Value: mem_access:
- \valid_read(__gen_e_acsl_at +
- (int)((int)(__gen_e_acsl_n - 1) - 1));
- */
if (*(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1))) {
int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_2 + (int)(
@@ -758,11 +676,6 @@ void __gen_e_acsl_f(int *t)
Value: initialization:
\initialized(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
*/
- /*@ assert
- Value: mem_access:
- \valid_read(__gen_e_acsl_at_2 +
- (int)((int)(__gen_e_acsl_n - 1) - 1));
- */
__gen_e_acsl_and = *(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
}
else __gen_e_acsl_and = 0;
diff --git a/src/plugins/e-acsl/tests/gmp/test_config b/src/plugins/e-acsl/tests/gmp/test_config
index b51a18dcf2f95a90239b1a25a517a65a5e866834..645d2c1fa60b62e4c9c9223a7c2f6adf06608878 100644
--- a/src/plugins/e-acsl/tests/gmp/test_config
+++ b/src/plugins/e-acsl/tests/gmp/test_config
@@ -1,5 +1,5 @@
LOG: gen_@PTEST_NAME@.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
+OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results -eva-no-alloc-returns-null
EXEC: ./scripts/testrun.sh @PTEST_NAME@ gmp "1" "--frama-c=@frama-c@"
LOG: gen_@PTEST_NAME@2.c
-OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
+OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results -eva-no-alloc-returns-null