From c37ab5e9ba5984fd9c8b088116feb90241a2372c Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 16 Jun 2021 11:21:12 +0200
Subject: [PATCH] [eacsl] Update line numbers in test oracles
---
.../tests/arith/oracle/bitwise.res.oracle | 16 ++--
.../e-acsl/tests/arith/oracle/gen_bitwise.c | 92 +++++++++----------
.../tests/memory/oracle/local_init.res.oracle | 2 +-
.../tests/special/oracle/builtin.res.oracle | 2 +-
.../oracle/e-acsl-functions.res.oracle | 2 +-
.../special/oracle/e-acsl-valid.res.oracle | 6 +-
.../e-acsl/tests/special/oracle/gen_builtin.c | 3 +-
.../special/oracle/gen_e-acsl-functions.c | 14 +--
.../special/oracle/gen_e-acsl-instrument.c | 8 +-
.../tests/special/oracle/gen_e-acsl-valid.c | 20 ++--
.../e-acsl-instrument.e-acsl.err.log | 8 +-
11 files changed, 87 insertions(+), 86 deletions(-)
diff --git a/src/plugins/e-acsl/tests/arith/oracle/bitwise.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/bitwise.res.oracle
index e4a35555d5f..1d829537034 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/bitwise.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/bitwise.res.oracle
@@ -1,16 +1,12 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/arith/bitwise.c:40: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/bitwise.c:40: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/bitwise.c:42: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/bitwise.c:42: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/bitwise.c:44: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/bitwise.c:45: Warning:
+[eva:alarm] tests/arith/bitwise.c:44: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/bitwise.c:46: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
@@ -18,9 +14,9 @@
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/bitwise.c:48: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/bitwise.c:55: Warning:
+[eva:alarm] tests/arith/bitwise.c:49: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/bitwise.c:55: Warning:
+[eva:alarm] tests/arith/bitwise.c:50: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/bitwise.c:57: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
@@ -28,7 +24,7 @@
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/bitwise.c:59: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/bitwise.c:60: Warning:
+[eva:alarm] tests/arith/bitwise.c:59: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/bitwise.c:61: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
@@ -36,3 +32,7 @@
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/bitwise.c:63: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:64: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:65: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c b/src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c
index 45747581a41..54340192b07 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c
@@ -5,27 +5,27 @@ void f_signed(int a, int b)
{
int c = a << 2;
__e_acsl_assert(0 <= a,1,"RTE","f_signed","shift: 0 <= a",
- "tests/arith/bitwise.c",12);
+ "tests/arith/bitwise.c",14);
__e_acsl_assert((long)c == a << 2L,1,"Assertion","f_signed","c == a << 2",
- "tests/arith/bitwise.c",12);
+ "tests/arith/bitwise.c",14);
/*@ assert c ≡ a << 2; */ ;
int d = b >> 2;
__e_acsl_assert(0 <= b,1,"RTE","f_signed","shift: 0 <= b",
- "tests/arith/bitwise.c",14);
+ "tests/arith/bitwise.c",16);
__e_acsl_assert(d == b >> 2,1,"Assertion","f_signed","d == b >> 2",
- "tests/arith/bitwise.c",14);
+ "tests/arith/bitwise.c",16);
/*@ assert d ≡ b >> 2; */ ;
int e = a | b;
__e_acsl_assert((long)e == (a | (long)b),1,"Assertion","f_signed",
- "e == (a | b)","tests/arith/bitwise.c",16);
+ "e == (a | b)","tests/arith/bitwise.c",18);
/*@ assert e ≡ (a | b); */ ;
int f = a & b;
__e_acsl_assert((long)f == (a & (long)b),1,"Assertion","f_signed",
- "f == (a & b)","tests/arith/bitwise.c",18);
+ "f == (a & b)","tests/arith/bitwise.c",20);
/*@ assert f ≡ (a & b); */ ;
int g = a ^ b;
__e_acsl_assert((long)g == (a ^ (long)b),1,"Assertion","f_signed",
- "g == (a ^ b)","tests/arith/bitwise.c",20);
+ "g == (a ^ b)","tests/arith/bitwise.c",22);
/*@ assert g ≡ (a ^ b); */ ;
return;
}
@@ -34,23 +34,23 @@ void f_unsigned(unsigned int a, unsigned int b)
{
unsigned int c = a << 2u;
__e_acsl_assert((unsigned long)c == a << 2UL,1,"Assertion","f_unsigned",
- "c == a << 2","tests/arith/bitwise.c",26);
+ "c == a << 2","tests/arith/bitwise.c",28);
/*@ assert c ≡ a << 2; */ ;
unsigned int d = b >> 2u;
__e_acsl_assert(d == b >> 2U,1,"Assertion","f_unsigned","d == b >> 2",
- "tests/arith/bitwise.c",28);
+ "tests/arith/bitwise.c",30);
/*@ assert d ≡ b >> 2; */ ;
unsigned int e = a | b;
__e_acsl_assert(e == (a | b),1,"Assertion","f_unsigned","e == (a | b)",
- "tests/arith/bitwise.c",30);
+ "tests/arith/bitwise.c",32);
/*@ assert e ≡ (a | b); */ ;
unsigned int f = a & b;
__e_acsl_assert(f == (a & b),1,"Assertion","f_unsigned","f == (a & b)",
- "tests/arith/bitwise.c",32);
+ "tests/arith/bitwise.c",34);
/*@ assert f ≡ (a & b); */ ;
unsigned int g = a ^ b;
__e_acsl_assert(g == (a ^ b),1,"Assertion","f_unsigned","g == (a ^ b)",
- "tests/arith/bitwise.c",34);
+ "tests/arith/bitwise.c",36);
/*@ assert g ≡ (a ^ b); */ ;
return;
}
@@ -78,7 +78,7 @@ void g_signed(int a, int b)
*/
__e_acsl_assert(__gen_e_acsl_b_shiftl_guard,1,"RTE","g_signed",
"shiftl_rhs_fits_in_mp_bitcnt_t: 0 <= b <= 18446744073709551615",
- "tests/arith/bitwise.c",40);
+ "tests/arith/bitwise.c",42);
__gen_e_acsl_b_shiftl_coerced = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_b));
__gmpz_init_set_si(__gen_e_acsl_,0L);
__gen_e_acsl_a_shiftl_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_a),
@@ -86,14 +86,14 @@ void g_signed(int a, int b)
__gmpz_init(__gen_e_acsl_shiftl);
/*@ assert E_ACSL: a ≥ 0; */
__e_acsl_assert(__gen_e_acsl_a_shiftl_guard >= 0,1,"RTE","g_signed",
- "a >= 0","tests/arith/bitwise.c",40);
+ "a >= 0","tests/arith/bitwise.c",42);
__gmpz_mul_2exp(__gen_e_acsl_shiftl,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_a),
__gen_e_acsl_b_shiftl_coerced);
__gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_c),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_shiftl));
__e_acsl_assert(__gen_e_acsl_eq == 0,1,"Assertion","g_signed",
- "c == a << b","tests/arith/bitwise.c",40);
+ "c == a << b","tests/arith/bitwise.c",42);
__gmpz_clear(__gen_e_acsl_c);
__gmpz_clear(__gen_e_acsl_a);
__gmpz_clear(__gen_e_acsl_b);
@@ -122,7 +122,7 @@ void g_signed(int a, int b)
*/
__e_acsl_assert(__gen_e_acsl_b_shiftr_guard,1,"RTE","g_signed",
"shiftr_rhs_fits_in_mp_bitcnt_t: 0 <= b <= 18446744073709551615",
- "tests/arith/bitwise.c",42);
+ "tests/arith/bitwise.c",44);
__gen_e_acsl_b_shiftr_coerced = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_b_2));
__gmpz_init_set_si(__gen_e_acsl__2,0L);
__gen_e_acsl_a_shiftr_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_a_2),
@@ -130,14 +130,14 @@ void g_signed(int a, int b)
__gmpz_init(__gen_e_acsl_shiftr);
/*@ assert E_ACSL: a ≥ 0; */
__e_acsl_assert(__gen_e_acsl_a_shiftr_guard >= 0,1,"RTE","g_signed",
- "a >= 0","tests/arith/bitwise.c",42);
+ "a >= 0","tests/arith/bitwise.c",44);
__gmpz_tdiv_q_2exp(__gen_e_acsl_shiftr,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_a_2),
__gen_e_acsl_b_shiftr_coerced);
__gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_d),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_shiftr));
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,1,"Assertion","g_signed",
- "d == a >> b","tests/arith/bitwise.c",42);
+ "d == a >> b","tests/arith/bitwise.c",44);
__gmpz_clear(__gen_e_acsl_d);
__gmpz_clear(__gen_e_acsl_a_2);
__gmpz_clear(__gen_e_acsl_b_2);
@@ -168,7 +168,7 @@ void g_signed(int a, int b)
*/
__e_acsl_assert(__gen_e_acsl_cst_shiftl_guard,1,"RTE","g_signed",
"shiftl_rhs_fits_in_mp_bitcnt_t: 0 <= 1 <= 18446744073709551615",
- "tests/arith/bitwise.c",44);
+ "tests/arith/bitwise.c",46);
__gen_e_acsl_cst_shiftl_coerced = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
__gmpz_init_set_si(__gen_e_acsl__5,0L);
__gen_e_acsl_shiftl_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
@@ -177,7 +177,7 @@ void g_signed(int a, int b)
/*@ assert E_ACSL: 18446744073709551615ULL + 1 ≥ 0; */
__e_acsl_assert(__gen_e_acsl_shiftl_guard >= 0,1,"RTE","g_signed",
"18446744073709551615ULL + 1 >= 0",
- "tests/arith/bitwise.c",44);
+ "tests/arith/bitwise.c",46);
__gmpz_mul_2exp(__gen_e_acsl_shiftl_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
__gen_e_acsl_cst_shiftl_coerced);
@@ -185,7 +185,7 @@ void g_signed(int a, int b)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
__e_acsl_assert(__gen_e_acsl_ne != 0,1,"Assertion","g_signed",
"(18446744073709551615ULL + 1) << 1 != 0",
- "tests/arith/bitwise.c",44);
+ "tests/arith/bitwise.c",46);
__gmpz_clear(__gen_e_acsl__3);
__gmpz_clear(__gen_e_acsl__4);
__gmpz_clear(__gen_e_acsl_add);
@@ -216,7 +216,7 @@ void g_signed(int a, int b)
*/
__e_acsl_assert(__gen_e_acsl_cst_shiftr_guard,1,"RTE","g_signed",
"shiftr_rhs_fits_in_mp_bitcnt_t: 0 <= 1 <= 18446744073709551615",
- "tests/arith/bitwise.c",45);
+ "tests/arith/bitwise.c",47);
__gen_e_acsl_cst_shiftr_coerced = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
__gmpz_init_set_si(__gen_e_acsl__8,0L);
__gen_e_acsl_shiftr_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
@@ -225,14 +225,14 @@ void g_signed(int a, int b)
/*@ assert E_ACSL: 18446744073709551615ULL + 1 ≥ 0; */
__e_acsl_assert(__gen_e_acsl_shiftr_guard >= 0,1,"RTE","g_signed",
"18446744073709551615ULL + 1 >= 0",
- "tests/arith/bitwise.c",45);
+ "tests/arith/bitwise.c",47);
__gmpz_tdiv_q_2exp(__gen_e_acsl_shiftr_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
__gen_e_acsl_cst_shiftr_coerced);
__gen_e_acsl__9 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_shiftr_2));
__e_acsl_assert(__gen_e_acsl__9 != 0UL,1,"Assertion","g_signed",
"(18446744073709551615ULL + 1) >> 1 != 0",
- "tests/arith/bitwise.c",45);
+ "tests/arith/bitwise.c",47);
__gmpz_clear(__gen_e_acsl__6);
__gmpz_clear(__gen_e_acsl__7);
__gmpz_clear(__gen_e_acsl_add_2);
@@ -258,7 +258,7 @@ void g_signed(int a, int b)
*/
__e_acsl_assert(__gen_e_acsl_cst_shiftl_guard_2,1,"RTE","g_signed",
"shiftl_rhs_fits_in_mp_bitcnt_t: 0 <= 65 <= 18446744073709551615",
- "tests/arith/bitwise.c",46);
+ "tests/arith/bitwise.c",48);
__gen_e_acsl_cst_shiftl_coerced_2 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
__gmpz_init_set_si(__gen_e_acsl__12,0L);
__gen_e_acsl_cst_shiftl_guard_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
@@ -266,14 +266,14 @@ void g_signed(int a, int b)
__gmpz_init(__gen_e_acsl_shiftl_3);
/*@ assert E_ACSL: 1 ≥ 0; */
__e_acsl_assert(__gen_e_acsl_cst_shiftl_guard_3 >= 0,1,"RTE","g_signed",
- "1 >= 0","tests/arith/bitwise.c",46);
+ "1 >= 0","tests/arith/bitwise.c",48);
__gmpz_mul_2exp(__gen_e_acsl_shiftl_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
__gen_e_acsl_cst_shiftl_coerced_2);
__gen_e_acsl_ne_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_shiftl_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
__e_acsl_assert(__gen_e_acsl_ne_2 != 0,1,"Assertion","g_signed",
- "1 << 65 != 0","tests/arith/bitwise.c",46);
+ "1 << 65 != 0","tests/arith/bitwise.c",48);
__gmpz_clear(__gen_e_acsl__10);
__gmpz_clear(__gen_e_acsl__11);
__gmpz_clear(__gen_e_acsl__12);
@@ -309,7 +309,7 @@ void g_signed(int a, int b)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
__e_acsl_assert(__gen_e_acsl_ne_3 != 0,1,"Assertion","g_signed",
"((18446744073709551615ULL + 1) | ((-9223372036854775807LL - 1LL) - 1)) != 0",
- "tests/arith/bitwise.c",47);
+ "tests/arith/bitwise.c",49);
__gmpz_clear(__gen_e_acsl__13);
__gmpz_clear(__gen_e_acsl__14);
__gmpz_clear(__gen_e_acsl_add_3);
@@ -355,7 +355,7 @@ void g_signed(int a, int b)
(__e_acsl_mpz_struct const *)(__gen_e_acsl_bxor));
__e_acsl_assert(__gen_e_acsl_ne_4 != 0,1,"Assertion","g_signed",
"((18446744073709551615ULL + 1) & ((-9223372036854775807LL - 1LL) - 1)) !=\n((18446744073709551615ULL + 1) ^ ((-9223372036854775807LL - 1LL) - 1))",
- "tests/arith/bitwise.c",48);
+ "tests/arith/bitwise.c",50);
__gmpz_clear(__gen_e_acsl__17);
__gmpz_clear(__gen_e_acsl__18);
__gmpz_clear(__gen_e_acsl_add_4);
@@ -395,7 +395,7 @@ void g_unsigned(unsigned int a, unsigned int b)
*/
__e_acsl_assert(__gen_e_acsl_b_shiftl_guard,1,"RTE","g_unsigned",
"shiftl_rhs_fits_in_mp_bitcnt_t: 0 <= b <= 18446744073709551615",
- "tests/arith/bitwise.c",55);
+ "tests/arith/bitwise.c",57);
__gen_e_acsl_b_shiftl_coerced = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_b));
__gmpz_init_set_si(__gen_e_acsl_,0L);
__gen_e_acsl_a_shiftl_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_a),
@@ -403,14 +403,14 @@ void g_unsigned(unsigned int a, unsigned int b)
__gmpz_init(__gen_e_acsl_shiftl);
/*@ assert E_ACSL: a ≥ 0; */
__e_acsl_assert(__gen_e_acsl_a_shiftl_guard >= 0,1,"RTE","g_unsigned",
- "a >= 0","tests/arith/bitwise.c",55);
+ "a >= 0","tests/arith/bitwise.c",57);
__gmpz_mul_2exp(__gen_e_acsl_shiftl,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_a),
__gen_e_acsl_b_shiftl_coerced);
__gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_c),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_shiftl));
__e_acsl_assert(__gen_e_acsl_eq == 0,1,"Assertion","g_unsigned",
- "c == a << b","tests/arith/bitwise.c",55);
+ "c == a << b","tests/arith/bitwise.c",57);
__gmpz_clear(__gen_e_acsl_c);
__gmpz_clear(__gen_e_acsl_a);
__gmpz_clear(__gen_e_acsl_b);
@@ -439,7 +439,7 @@ void g_unsigned(unsigned int a, unsigned int b)
*/
__e_acsl_assert(__gen_e_acsl_b_shiftr_guard,1,"RTE","g_unsigned",
"shiftr_rhs_fits_in_mp_bitcnt_t: 0 <= b <= 18446744073709551615",
- "tests/arith/bitwise.c",57);
+ "tests/arith/bitwise.c",59);
__gen_e_acsl_b_shiftr_coerced = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_b_2));
__gmpz_init_set_si(__gen_e_acsl__2,0L);
__gen_e_acsl_a_shiftr_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_a_2),
@@ -447,14 +447,14 @@ void g_unsigned(unsigned int a, unsigned int b)
__gmpz_init(__gen_e_acsl_shiftr);
/*@ assert E_ACSL: a ≥ 0; */
__e_acsl_assert(__gen_e_acsl_a_shiftr_guard >= 0,1,"RTE","g_unsigned",
- "a >= 0","tests/arith/bitwise.c",57);
+ "a >= 0","tests/arith/bitwise.c",59);
__gmpz_tdiv_q_2exp(__gen_e_acsl_shiftr,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_a_2),
__gen_e_acsl_b_shiftr_coerced);
__gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_d),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_shiftr));
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,1,"Assertion","g_unsigned",
- "d == a >> b","tests/arith/bitwise.c",57);
+ "d == a >> b","tests/arith/bitwise.c",59);
__gmpz_clear(__gen_e_acsl_d);
__gmpz_clear(__gen_e_acsl_a_2);
__gmpz_clear(__gen_e_acsl_b_2);
@@ -485,7 +485,7 @@ void g_unsigned(unsigned int a, unsigned int b)
*/
__e_acsl_assert(__gen_e_acsl_cst_shiftl_guard,1,"RTE","g_unsigned",
"shiftl_rhs_fits_in_mp_bitcnt_t: 0 <= 1u <= 18446744073709551615",
- "tests/arith/bitwise.c",59);
+ "tests/arith/bitwise.c",61);
__gen_e_acsl_cst_shiftl_coerced = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
__gmpz_init_set_si(__gen_e_acsl__5,0L);
__gen_e_acsl_shiftl_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
@@ -494,7 +494,7 @@ void g_unsigned(unsigned int a, unsigned int b)
/*@ assert E_ACSL: 18446744073709551615ULL + 1u ≥ 0; */
__e_acsl_assert(__gen_e_acsl_shiftl_guard >= 0,1,"RTE","g_unsigned",
"18446744073709551615ULL + 1u >= 0",
- "tests/arith/bitwise.c",59);
+ "tests/arith/bitwise.c",61);
__gmpz_mul_2exp(__gen_e_acsl_shiftl_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
__gen_e_acsl_cst_shiftl_coerced);
@@ -502,7 +502,7 @@ void g_unsigned(unsigned int a, unsigned int b)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
__e_acsl_assert(__gen_e_acsl_ne != 0,1,"Assertion","g_unsigned",
"(18446744073709551615ULL + 1u) << 1u != 0",
- "tests/arith/bitwise.c",59);
+ "tests/arith/bitwise.c",61);
__gmpz_clear(__gen_e_acsl__3);
__gmpz_clear(__gen_e_acsl__4);
__gmpz_clear(__gen_e_acsl_add);
@@ -533,7 +533,7 @@ void g_unsigned(unsigned int a, unsigned int b)
*/
__e_acsl_assert(__gen_e_acsl_cst_shiftr_guard,1,"RTE","g_unsigned",
"shiftr_rhs_fits_in_mp_bitcnt_t: 0 <= 1u <= 18446744073709551615",
- "tests/arith/bitwise.c",60);
+ "tests/arith/bitwise.c",62);
__gen_e_acsl_cst_shiftr_coerced = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
__gmpz_init_set_si(__gen_e_acsl__8,0L);
__gen_e_acsl_shiftr_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
@@ -542,14 +542,14 @@ void g_unsigned(unsigned int a, unsigned int b)
/*@ assert E_ACSL: 18446744073709551615ULL + 1u ≥ 0; */
__e_acsl_assert(__gen_e_acsl_shiftr_guard >= 0,1,"RTE","g_unsigned",
"18446744073709551615ULL + 1u >= 0",
- "tests/arith/bitwise.c",60);
+ "tests/arith/bitwise.c",62);
__gmpz_tdiv_q_2exp(__gen_e_acsl_shiftr_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
__gen_e_acsl_cst_shiftr_coerced);
__gen_e_acsl__9 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_shiftr_2));
__e_acsl_assert(__gen_e_acsl__9 != 0UL,1,"Assertion","g_unsigned",
"(18446744073709551615ULL + 1u) >> 1u != 0",
- "tests/arith/bitwise.c",60);
+ "tests/arith/bitwise.c",62);
__gmpz_clear(__gen_e_acsl__6);
__gmpz_clear(__gen_e_acsl__7);
__gmpz_clear(__gen_e_acsl_add_2);
@@ -575,7 +575,7 @@ void g_unsigned(unsigned int a, unsigned int b)
*/
__e_acsl_assert(__gen_e_acsl_cst_shiftl_guard_2,1,"RTE","g_unsigned",
"shiftl_rhs_fits_in_mp_bitcnt_t: 0 <= 65u <= 18446744073709551615",
- "tests/arith/bitwise.c",61);
+ "tests/arith/bitwise.c",63);
__gen_e_acsl_cst_shiftl_coerced_2 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
__gmpz_init_set_si(__gen_e_acsl__12,0L);
__gen_e_acsl_cst_shiftl_guard_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
@@ -583,14 +583,14 @@ void g_unsigned(unsigned int a, unsigned int b)
__gmpz_init(__gen_e_acsl_shiftl_3);
/*@ assert E_ACSL: 1u ≥ 0; */
__e_acsl_assert(__gen_e_acsl_cst_shiftl_guard_3 >= 0,1,"RTE",
- "g_unsigned","1u >= 0","tests/arith/bitwise.c",61);
+ "g_unsigned","1u >= 0","tests/arith/bitwise.c",63);
__gmpz_mul_2exp(__gen_e_acsl_shiftl_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
__gen_e_acsl_cst_shiftl_coerced_2);
__gen_e_acsl_ne_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_shiftl_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
__e_acsl_assert(__gen_e_acsl_ne_2 != 0,1,"Assertion","g_unsigned",
- "1u << 65u != 0","tests/arith/bitwise.c",61);
+ "1u << 65u != 0","tests/arith/bitwise.c",63);
__gmpz_clear(__gen_e_acsl__10);
__gmpz_clear(__gen_e_acsl__11);
__gmpz_clear(__gen_e_acsl__12);
@@ -619,7 +619,7 @@ void g_unsigned(unsigned int a, unsigned int b)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
__e_acsl_assert(__gen_e_acsl_ne_3 != 0,1,"Assertion","g_unsigned",
"((18446744073709551615ULL + 1u) | 1u) != 0",
- "tests/arith/bitwise.c",62);
+ "tests/arith/bitwise.c",64);
__gmpz_clear(__gen_e_acsl__13);
__gmpz_clear(__gen_e_acsl__14);
__gmpz_clear(__gen_e_acsl_add_3);
@@ -652,7 +652,7 @@ void g_unsigned(unsigned int a, unsigned int b)
(__e_acsl_mpz_struct const *)(__gen_e_acsl_bxor));
__e_acsl_assert(__gen_e_acsl_ne_4 != 0,1,"Assertion","g_unsigned",
"((18446744073709551615ULL + 1u) & 1u) !=\n((18446744073709551615ULL + 1u) ^ 1u)",
- "tests/arith/bitwise.c",63);
+ "tests/arith/bitwise.c",65);
__gmpz_clear(__gen_e_acsl__16);
__gmpz_clear(__gen_e_acsl__17);
__gmpz_clear(__gen_e_acsl_add_4);
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 e5104fb7e86..05cabd8f302 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
@@ -1,4 +1,4 @@
-[eva:alarm] tests/memory/local_init.c:11: Warning:
+[eva:alarm] tests/memory/local_init.c:10: Warning:
out of bounds read. assert \valid_read(p);
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/special/oracle/builtin.res.oracle b/src/plugins/e-acsl/tests/special/oracle/builtin.res.oracle
index f829e96e464..ea338178977 100644
--- a/src/plugins/e-acsl/tests/special/oracle/builtin.res.oracle
+++ b/src/plugins/e-acsl/tests/special/oracle/builtin.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/special/builtin.i:9: Warning:
+[eva:alarm] tests/special/builtin.i:11: Warning:
function __gen_e_acsl_f: postcondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle
index 4661ead8e70..2c2f479abd8 100644
--- a/src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle
+++ b/src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/special/e-acsl-functions.c:29: Warning:
+[eva:alarm] tests/special/e-acsl-functions.c:31: Warning:
function g: precondition *p ≡ 1 got status invalid.
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.res.oracle
index c14797a555b..3962383599f 100644
--- a/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.res.oracle
+++ b/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.res.oracle
@@ -1,10 +1,10 @@
-[eva:alarm] tests/special/e-acsl-valid.c:37: Warning:
+[eva:alarm] tests/special/e-acsl-valid.c:39: Warning:
function f: precondition \valid(y) got status unknown.
[e-acsl] beginning translation.
-[e-acsl] tests/special/e-acsl-valid.c:28: Warning:
+[e-acsl] tests/special/e-acsl-valid.c:30: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:24: Warning:
+[e-acsl] tests/special/e-acsl-valid.c:26: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c b/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c
index 6f5f431cd75..dad8120db26 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c
@@ -40,7 +40,8 @@ int __gen_e_acsl_f(int i)
int __gen_e_acsl_incr_app;
__gen_e_acsl_incr_app = incr(__gen_e_acsl_at);
__e_acsl_assert(__retres == __gen_e_acsl_incr_app,1,"Postcondition","f",
- "\\result == incr(\\old(i))","tests/special/builtin.i",9);
+ "\\result == incr(\\old(i))","tests/special/builtin.i",
+ 11);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c
index d238464570c..f94e292fc42 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c
@@ -19,7 +19,7 @@ int f(int *p)
int __gen_e_acsl_and;
if (0 <= i) __gen_e_acsl_and = i <= 1; else __gen_e_acsl_and = 0;
__e_acsl_assert(__gen_e_acsl_and,1,"Invariant","f","0 <= i <= 1",
- "tests/special/e-acsl-functions.c",11);
+ "tests/special/e-acsl-functions.c",13);
}
/*@ loop invariant 0 ≤ i ≤ 1; */
while (i < 1) {
@@ -27,7 +27,7 @@ int f(int *p)
i ++;
if (0 <= i) __gen_e_acsl_and_2 = i <= 1; else __gen_e_acsl_and_2 = 0;
__e_acsl_assert(__gen_e_acsl_and_2,1,"Invariant","f","0 <= i <= 1",
- "tests/special/e-acsl-functions.c",11);
+ "tests/special/e-acsl-functions.c",13);
}
}
__retres = 0;
@@ -81,14 +81,14 @@ int __gen_e_acsl_f(int *p)
__e_acsl_store_block((void *)(& p),(size_t)8);
__gen_e_acsl_initialized = __e_acsl_initialized((void *)p,sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized,1,"Precondition","f",
- "\\initialized(p)","tests/special/e-acsl-functions.c",7);
+ "\\initialized(p)","tests/special/e-acsl-functions.c",9);
__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,1,"RTE","f",
"mem_access: \\valid_read(p)",
- "tests/special/e-acsl-functions.c",8);
+ "tests/special/e-acsl-functions.c",10);
__e_acsl_assert(*p == 0,1,"Precondition","f","*p == 0",
- "tests/special/e-acsl-functions.c",8);
+ "tests/special/e-acsl-functions.c",10);
}
{
int __gen_e_acsl_valid_read_2;
@@ -96,13 +96,13 @@ int __gen_e_acsl_f(int *p)
(void *)p,(void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid_read_2,1,"RTE","f",
"mem_access: \\valid_read(p)",
- "tests/special/e-acsl-functions.c",9);
+ "tests/special/e-acsl-functions.c",11);
__gen_e_acsl_at = *p;
}
__retres = f(p);
__e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","f",
"\\result == \\old(*p)","tests/special/e-acsl-functions.c",
- 9);
+ 11);
__e_acsl_delete_block((void *)(& p));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c
index c56ee16b78b..61a4e7c62bd 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c
@@ -100,7 +100,7 @@ int main(void)
sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized,1,"Assertion","main",
"\\initialized(&x)","tests/special/e-acsl-instrument.c",
- 56);
+ 58);
}
/*@ assert \initialized(&x); */ ;
{
@@ -109,7 +109,7 @@ int main(void)
sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized_2,1,"Assertion","main",
"\\initialized(&y)","tests/special/e-acsl-instrument.c",
- 57);
+ 59);
}
/*@ assert \initialized(&y); */ ;
{
@@ -139,7 +139,7 @@ int __gen_e_acsl_instrument2(int *p)
__gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
(void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid,1,"Precondition","instrument2",
- "\\valid(p)","tests/special/e-acsl-instrument.c",29);
+ "\\valid(p)","tests/special/e-acsl-instrument.c",31);
}
__retres = instrument2(p);
__e_acsl_delete_block((void *)(& p));
@@ -155,7 +155,7 @@ int __gen_e_acsl_uninstrument2(int *p)
__gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
(void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid,1,"Precondition","uninstrument2",
- "\\valid(p)","tests/special/e-acsl-instrument.c",14);
+ "\\valid(p)","tests/special/e-acsl-instrument.c",16);
}
__e_acsl_sound_verdict = 0;
__retres = uninstrument2(p);
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c
index d16e2cf103f..91bf7941f61 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c
@@ -35,9 +35,9 @@ void f(int *x, int *y)
(void *)x,(void *)(& x));
__e_acsl_assert(__gen_e_acsl_valid_read,1,"RTE","f",
"mem_access: \\valid_read(x)",
- "tests/special/e-acsl-valid.c",25);
+ "tests/special/e-acsl-valid.c",27);
__e_acsl_assert(*x >= 0,1,"Precondition","f","*x >= 0",
- "tests/special/e-acsl-valid.c",25);
+ "tests/special/e-acsl-valid.c",27);
}
/*@ requires *x ≥ 0;
ensures 2 ≥ 1;
@@ -47,7 +47,7 @@ void f(int *x, int *y)
(*x) ++;
}
__e_acsl_assert(1,1,"Postcondition","f","2 >= 1",
- "tests/special/e-acsl-valid.c",26);
+ "tests/special/e-acsl-valid.c",28);
{
int i = 0;
/*@ loop invariant 0 ≤ i ≤ 1;
@@ -60,10 +60,10 @@ void f(int *x, int *y)
i ++;
__e_acsl_assert(__gen_e_acsl_old_variant >= 0L,1,"Variant","f",
"(old 2 - i) \342\211\245 0",
- "tests/special/e-acsl-valid.c",31);
+ "tests/special/e-acsl-valid.c",33);
__e_acsl_assert(__gen_e_acsl_old_variant > 2L - i,1,"Variant","f",
"(old 2 - i) > 2 - i","tests/special/e-acsl-valid.c",
- 31);
+ 33);
}
}
__e_acsl_delete_block((void *)(& y));
@@ -122,30 +122,30 @@ void __gen_e_acsl_f(int *x, int *y)
(void *)x,(void *)(& x));
__e_acsl_assert(__gen_e_acsl_valid_read,1,"RTE","f",
"mem_access: \\valid_read(x)",
- "tests/special/e-acsl-valid.c",15);
+ "tests/special/e-acsl-valid.c",17);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
*x == 1);
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)x,sizeof(int),
(void *)x,(void *)(& x));
__e_acsl_assert(__gen_e_acsl_valid_read_2,1,"RTE","f",
"mem_access: \\valid_read(x)",
- "tests/special/e-acsl-valid.c",19);
+ "tests/special/e-acsl-valid.c",21);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1,
*x == 0);
__gen_e_acsl_valid = __e_acsl_valid((void *)y,sizeof(int),(void *)y,
(void *)(& y));
__e_acsl_assert(__gen_e_acsl_valid,1,"Precondition","f","\\valid(y)",
- "tests/special/e-acsl-valid.c",10);
+ "tests/special/e-acsl-valid.c",12);
__gen_e_acsl_active_bhvrs = __e_acsl_contract_partial_count_all_behaviors
((__e_acsl_contract_t const *)__gen_e_acsl_contract);
__e_acsl_assert(__gen_e_acsl_active_bhvrs >= 1,1,"Precondition","f",
"all behaviors complete","tests/special/e-acsl-valid.c",
- 24);
+ 26);
__gen_e_acsl_active_bhvrs = __e_acsl_contract_partial_count_all_behaviors
((__e_acsl_contract_t const *)__gen_e_acsl_contract);
__e_acsl_assert(__gen_e_acsl_active_bhvrs <= 1,1,"Precondition","f",
"all behaviors disjoint","tests/special/e-acsl-valid.c",
- 24);
+ 26);
}
f(x,y);
__e_acsl_contract_clean(__gen_e_acsl_contract);
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-instrument.e-acsl.err.log b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-instrument.e-acsl.err.log
index be2b0df1fe6..fe20ca61ec1 100644
--- a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-instrument.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-instrument.e-acsl.err.log
@@ -1,16 +1,16 @@
tests/special/e-acsl-instrument.c: In function 'instrument2'
-tests/special/e-acsl-instrument.c:29: Warning: no sound verdict for Precondition (guess: ok).
+tests/special/e-acsl-instrument.c:31: Warning: no sound verdict for Precondition (guess: ok).
the considered predicate is:
\valid(p)
tests/special/e-acsl-instrument.c: In function 'uninstrument2'
-tests/special/e-acsl-instrument.c:14: Warning: no sound verdict for Precondition (guess: ok).
+tests/special/e-acsl-instrument.c:16: Warning: no sound verdict for Precondition (guess: ok).
the considered predicate is:
\valid(p)
tests/special/e-acsl-instrument.c: In function 'main'
-tests/special/e-acsl-instrument.c:56: Warning: no sound verdict for Assertion (guess: ok).
+tests/special/e-acsl-instrument.c:58: Warning: no sound verdict for Assertion (guess: ok).
the considered predicate is:
\initialized(&x)
tests/special/e-acsl-instrument.c: In function 'main'
-tests/special/e-acsl-instrument.c:57: Warning: no sound verdict for Assertion (guess: ok).
+tests/special/e-acsl-instrument.c:59: Warning: no sound verdict for Assertion (guess: ok).
the considered predicate is:
\initialized(&y)
--
GitLab