From 5e1fe19c71fd5cbe2d136b6fe68dc6a83be93cd5 Mon Sep 17 00:00:00 2001
From: "Fonenantsoa Maurica (fmaurica)" <maurica.fonenantsoa@gmail.com>
Date: Tue, 27 Mar 2018 20:02:51 +0200
Subject: [PATCH] Test for name capturing.
---
src/plugins/e-acsl/tests/gmp/let.c | 3 +
src/plugins/e-acsl/tests/gmp/oracle/gen_let.c | 75 ++++-----
.../e-acsl/tests/gmp/oracle/gen_let2.c | 148 ++++++++++--------
.../e-acsl/tests/gmp/oracle/let.0.res.oracle | 26 ++-
.../e-acsl/tests/gmp/oracle/let.1.res.oracle | 29 ++--
5 files changed, 154 insertions(+), 127 deletions(-)
diff --git a/src/plugins/e-acsl/tests/gmp/let.c b/src/plugins/e-acsl/tests/gmp/let.c
index 388a2646cf0..b42c297fbcc 100644
--- a/src/plugins/e-acsl/tests/gmp/let.c
+++ b/src/plugins/e-acsl/tests/gmp/let.c
@@ -13,6 +13,9 @@ int main(void) {
/*@ assert
\let u = 1;
(\let v = u + 1; v) == 2; */ ;
+ /*@ assert
+ \let u = 1;
+ (\let u = u + 1; u) == 2; */ ;
long m = 0x7fffffffffffffffL;
/*@ assert (\let u = m; u*u) > m; */ ;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_let.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_let.c
index 9bf65bd1632..33945c99959 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_let.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_let.c
@@ -14,7 +14,6 @@ int main(void)
int __retres;
union __anonunion_s_2 s;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- __e_acsl_store_block((void *)(& s),(size_t)8);
int n = -2;
/*@ assert \let u = n * n; u ≥ 0; */
{
@@ -48,89 +47,93 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_v_2 == 2,(char *)"Assertion",(char *)"main",
(char *)"\\let u = 1; (\\let v = u + 1; v) == 2",14);
}
+ /*@ assert \let u = 1; (\let u = u + 1; u) ≡ 2; */
+ {
+ int __gen_e_acsl_u_5;
+ int __gen_e_acsl_u_6;
+ __gen_e_acsl_u_5 = 1;
+ __gen_e_acsl_u_6 = __gen_e_acsl_u_5 + 1;
+ __e_acsl_assert(__gen_e_acsl_u_6 == 2,(char *)"Assertion",(char *)"main",
+ (char *)"\\let u = 1; (\\let u = u + 1; u) == 2",17);
+ }
long m = 0x7fffffffffffffffL;
- __e_acsl_store_block((void *)(& m),(size_t)8);
- __e_acsl_full_init((void *)(& m));
/*@ assert (\let u = m; u * u) > m; */
{
- long __gen_e_acsl_u_5;
- __e_acsl_mpz_t __gen_e_acsl_u_6;
+ long __gen_e_acsl_u_7;
+ __e_acsl_mpz_t __gen_e_acsl_u_8;
__e_acsl_mpz_t __gen_e_acsl_mul;
__e_acsl_mpz_t __gen_e_acsl_m;
int __gen_e_acsl_gt;
- __gen_e_acsl_u_5 = m;
- __gmpz_init_set_si(__gen_e_acsl_u_6,__gen_e_acsl_u_5);
+ __gen_e_acsl_u_7 = m;
+ __gmpz_init_set_si(__gen_e_acsl_u_8,__gen_e_acsl_u_7);
__gmpz_init(__gen_e_acsl_mul);
__gmpz_mul(__gen_e_acsl_mul,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_6));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_8));
__gmpz_init_set_si(__gen_e_acsl_m,m);
__gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_m));
__e_acsl_assert(__gen_e_acsl_gt > 0,(char *)"Assertion",(char *)"main",
- (char *)"(\\let u = m; u * u) > m",18);
- __gmpz_clear(__gen_e_acsl_u_6);
+ (char *)"(\\let u = m; u * u) > m",21);
+ __gmpz_clear(__gen_e_acsl_u_8);
__gmpz_clear(__gen_e_acsl_mul);
__gmpz_clear(__gen_e_acsl_m);
}
char c = (char)'a';
/*@ assert \let u = 'b'; c < u; */
{
- int __gen_e_acsl_u_7;
- __gen_e_acsl_u_7 = 'b';
- __e_acsl_assert((int)c < __gen_e_acsl_u_7,(char *)"Assertion",
- (char *)"main",(char *)"\\let u = \'b\'; c < u",21);
+ int __gen_e_acsl_u_9;
+ __gen_e_acsl_u_9 = 'b';
+ __e_acsl_assert((int)c < __gen_e_acsl_u_9,(char *)"Assertion",
+ (char *)"main",(char *)"\\let u = \'b\'; c < u",24);
}
float f = 1.0f;
__e_acsl_store_block((void *)(& f),(size_t)4);
__e_acsl_full_init((void *)(& f));
/*@ assert \let u = f; u ≡ f; */
{
- float __gen_e_acsl_u_8;
- __gen_e_acsl_u_8 = f;
- __e_acsl_assert(__gen_e_acsl_u_8 == f,(char *)"Assertion",(char *)"main",
- (char *)"\\let u = f; u == f",24);
+ float __gen_e_acsl_u_10;
+ __gen_e_acsl_u_10 = f;
+ __e_acsl_assert(__gen_e_acsl_u_10 == f,(char *)"Assertion",
+ (char *)"main",(char *)"\\let u = f; u == f",27);
}
int t[4] = {1, 2, 3, 4};
/*@ assert \let u = &t[1]; 1 ≡ 1; */
{
- int * /*[4]*/ __gen_e_acsl_u_9;
- __gen_e_acsl_u_9 = & t[1];
+ int * /*[4]*/ __gen_e_acsl_u_11;
+ __gen_e_acsl_u_11 = & t[1];
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
- (char *)"\\let u = &t[1]; 1 == 1",27);
+ (char *)"\\let u = &t[1]; 1 == 1",30);
}
/*@ assert (\let u = &t[1]; 1) ≡ 1; */
{
- int * /*[4]*/ __gen_e_acsl_u_10;
- __gen_e_acsl_u_10 = & t[1];
+ int * /*[4]*/ __gen_e_acsl_u_12;
+ __gen_e_acsl_u_12 = & t[1];
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
- (char *)"(\\let u = &t[1]; 1) == 1",29);
+ (char *)"(\\let u = &t[1]; 1) == 1",32);
}
struct __anonstruct_r_1 r = {.x = 1, .y = 2};
__e_acsl_store_block((void *)(& r),(size_t)8);
__e_acsl_full_init((void *)(& r));
/*@ assert \let u = r; u.x + u.y ≡ 3; */
{
- struct __anonstruct_r_1 __gen_e_acsl_u_11;
- __gen_e_acsl_u_11 = r;
- __e_acsl_assert(__gen_e_acsl_u_11.x + (long)__gen_e_acsl_u_11.y == 3L,
+ struct __anonstruct_r_1 __gen_e_acsl_u_13;
+ __gen_e_acsl_u_13 = r;
+ __e_acsl_assert(__gen_e_acsl_u_13.x + (long)__gen_e_acsl_u_13.y == 3L,
(char *)"Assertion",(char *)"main",
- (char *)"\\let u = r; u.x + u.y == 3",32);
+ (char *)"\\let u = r; u.x + u.y == 3",35);
}
- __e_acsl_initialize((void *)(& s.x),sizeof(int));
s.x = 5;
/*@ assert (\let u = s; u.x) > 0; */
{
- union __anonunion_s_2 __gen_e_acsl_u_12;
- __gen_e_acsl_u_12 = s;
- __e_acsl_assert(__gen_e_acsl_u_12.x > 0,(char *)"Assertion",
- (char *)"main",(char *)"(\\let u = s; u.x) > 0",36);
+ union __anonunion_s_2 __gen_e_acsl_u_14;
+ __gen_e_acsl_u_14 = s;
+ __e_acsl_assert(__gen_e_acsl_u_14.x > 0,(char *)"Assertion",
+ (char *)"main",(char *)"(\\let u = s; u.x) > 0",39);
}
__retres = 0;
- __e_acsl_delete_block((void *)(& s));
__e_acsl_delete_block((void *)(& r));
__e_acsl_delete_block((void *)(& f));
- __e_acsl_delete_block((void *)(& m));
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c
index ffcf544f6ad..96b37ea579d 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c
@@ -14,7 +14,6 @@ int main(void)
int __retres;
union __anonunion_s_2 s;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- __e_acsl_store_block((void *)(& s),(size_t)8);
int n = -2;
/*@ assert \let u = n * n; u ≥ 0; */
{
@@ -132,121 +131,146 @@ int main(void)
__gmpz_clear(__gen_e_acsl_add_3);
__gmpz_clear(__gen_e_acsl__8);
}
+ /*@ assert \let u = 1; (\let u = u + 1; u) ≡ 2; */
+ {
+ int __gen_e_acsl_u_6;
+ __e_acsl_mpz_t __gen_e_acsl_u_7;
+ __e_acsl_mpz_t __gen_e_acsl_u_8;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ int __gen_e_acsl_eq_3;
+ __gen_e_acsl_u_6 = 1;
+ __gmpz_init_set_si(__gen_e_acsl_u_8,(long)__gen_e_acsl_u_6);
+ __gmpz_init_set_si(__gen_e_acsl__9,1L);
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ __gmpz_init_set(__gen_e_acsl_u_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
+ __gmpz_init_set_si(__gen_e_acsl__10,2L);
+ __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_u_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
+ __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
+ (char *)"main",
+ (char *)"\\let u = 1; (\\let u = u + 1; u) == 2",17);
+ __gmpz_clear(__gen_e_acsl_u_7);
+ __gmpz_clear(__gen_e_acsl_u_8);
+ __gmpz_clear(__gen_e_acsl__9);
+ __gmpz_clear(__gen_e_acsl_add_4);
+ __gmpz_clear(__gen_e_acsl__10);
+ }
long m = 0x7fffffffffffffffL;
- __e_acsl_store_block((void *)(& m),(size_t)8);
- __e_acsl_full_init((void *)(& m));
/*@ assert (\let u = m; u * u) > m; */
{
- long __gen_e_acsl_u_6;
- __e_acsl_mpz_t __gen_e_acsl_u_7;
+ long __gen_e_acsl_u_9;
+ __e_acsl_mpz_t __gen_e_acsl_u_10;
__e_acsl_mpz_t __gen_e_acsl_mul_3;
__e_acsl_mpz_t __gen_e_acsl_m;
int __gen_e_acsl_gt_2;
- __gen_e_acsl_u_6 = m;
- __gmpz_init_set_si(__gen_e_acsl_u_7,__gen_e_acsl_u_6);
+ __gen_e_acsl_u_9 = m;
+ __gmpz_init_set_si(__gen_e_acsl_u_10,__gen_e_acsl_u_9);
__gmpz_init(__gen_e_acsl_mul_3);
__gmpz_mul(__gen_e_acsl_mul_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_7));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_10),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_10));
__gmpz_init_set_si(__gen_e_acsl_m,m);
__gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_m));
__e_acsl_assert(__gen_e_acsl_gt_2 > 0,(char *)"Assertion",(char *)"main",
- (char *)"(\\let u = m; u * u) > m",18);
- __gmpz_clear(__gen_e_acsl_u_7);
+ (char *)"(\\let u = m; u * u) > m",21);
+ __gmpz_clear(__gen_e_acsl_u_10);
__gmpz_clear(__gen_e_acsl_mul_3);
__gmpz_clear(__gen_e_acsl_m);
}
char c = (char)'a';
/*@ assert \let u = 'b'; c < u; */
{
- int __gen_e_acsl_u_8;
+ int __gen_e_acsl_u_11;
__e_acsl_mpz_t __gen_e_acsl_c;
- __e_acsl_mpz_t __gen_e_acsl_u_9;
+ __e_acsl_mpz_t __gen_e_acsl_u_12;
int __gen_e_acsl_lt;
- __gen_e_acsl_u_8 = 'b';
+ __gen_e_acsl_u_11 = 'b';
__gmpz_init_set_si(__gen_e_acsl_c,(long)c);
- __gmpz_init_set_si(__gen_e_acsl_u_9,(long)__gen_e_acsl_u_8);
+ __gmpz_init_set_si(__gen_e_acsl_u_12,(long)__gen_e_acsl_u_11);
__gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_c),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_9));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_u_12));
__e_acsl_assert(__gen_e_acsl_lt < 0,(char *)"Assertion",(char *)"main",
- (char *)"\\let u = \'b\'; c < u",21);
+ (char *)"\\let u = \'b\'; c < u",24);
__gmpz_clear(__gen_e_acsl_c);
- __gmpz_clear(__gen_e_acsl_u_9);
+ __gmpz_clear(__gen_e_acsl_u_12);
}
float f = 1.0f;
__e_acsl_store_block((void *)(& f),(size_t)4);
__e_acsl_full_init((void *)(& f));
/*@ assert \let u = f; u ≡ f; */
{
- float __gen_e_acsl_u_10;
- __gen_e_acsl_u_10 = f;
- __e_acsl_assert(__gen_e_acsl_u_10 == f,(char *)"Assertion",
- (char *)"main",(char *)"\\let u = f; u == f",24);
+ float __gen_e_acsl_u_13;
+ __gen_e_acsl_u_13 = f;
+ __e_acsl_assert(__gen_e_acsl_u_13 == f,(char *)"Assertion",
+ (char *)"main",(char *)"\\let u = f; u == f",27);
}
int t[4] = {1, 2, 3, 4};
/*@ assert \let u = &t[1]; 1 ≡ 1; */
{
- int * /*[4]*/ __gen_e_acsl_u_11;
- __e_acsl_mpz_t __gen_e_acsl__9;
- int __gen_e_acsl_eq_3;
- __gen_e_acsl_u_11 = & t[1];
- __gmpz_init_set_si(__gen_e_acsl__9,1L);
- __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__9),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
- __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
- (char *)"main",(char *)"\\let u = &t[1]; 1 == 1",27);
- __gmpz_clear(__gen_e_acsl__9);
+ int * /*[4]*/ __gen_e_acsl_u_14;
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ int __gen_e_acsl_eq_4;
+ __gen_e_acsl_u_14 = & t[1];
+ __gmpz_init_set_si(__gen_e_acsl__11,1L);
+ __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__11),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
+ (char *)"main",(char *)"\\let u = &t[1]; 1 == 1",30);
+ __gmpz_clear(__gen_e_acsl__11);
}
/*@ assert (\let u = &t[1]; 1) ≡ 1; */
{
- int * /*[4]*/ __gen_e_acsl_u_12;
- __gen_e_acsl_u_12 = & t[1];
+ int * /*[4]*/ __gen_e_acsl_u_15;
+ __gen_e_acsl_u_15 = & t[1];
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
- (char *)"(\\let u = &t[1]; 1) == 1",29);
+ (char *)"(\\let u = &t[1]; 1) == 1",32);
}
struct __anonstruct_r_1 r = {.x = 1, .y = 2};
__e_acsl_store_block((void *)(& r),(size_t)8);
__e_acsl_full_init((void *)(& r));
/*@ assert \let u = r; u.x + u.y ≡ 3; */
{
- struct __anonstruct_r_1 __gen_e_acsl_u_13;
- __e_acsl_mpz_t __gen_e_acsl__10;
- __e_acsl_mpz_t __gen_e_acsl__11;
- __e_acsl_mpz_t __gen_e_acsl_add_4;
+ struct __anonstruct_r_1 __gen_e_acsl_u_16;
__e_acsl_mpz_t __gen_e_acsl__12;
- int __gen_e_acsl_eq_4;
- __gen_e_acsl_u_13 = r;
- __gmpz_init_set_si(__gen_e_acsl__10,(long)__gen_e_acsl_u_13.x);
- __gmpz_init_set_si(__gen_e_acsl__11,(long)__gen_e_acsl_u_13.y);
- __gmpz_init(__gen_e_acsl_add_4);
- __gmpz_add(__gen_e_acsl_add_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
- __gmpz_init_set_si(__gen_e_acsl__12,3L);
- __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
- __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
- (char *)"main",(char *)"\\let u = r; u.x + u.y == 3",32);
- __gmpz_clear(__gen_e_acsl__10);
- __gmpz_clear(__gen_e_acsl__11);
- __gmpz_clear(__gen_e_acsl_add_4);
+ __e_acsl_mpz_t __gen_e_acsl__13;
+ __e_acsl_mpz_t __gen_e_acsl_add_5;
+ __e_acsl_mpz_t __gen_e_acsl__14;
+ int __gen_e_acsl_eq_5;
+ __gen_e_acsl_u_16 = r;
+ __gmpz_init_set_si(__gen_e_acsl__12,(long)__gen_e_acsl_u_16.x);
+ __gmpz_init_set_si(__gen_e_acsl__13,(long)__gen_e_acsl_u_16.y);
+ __gmpz_init(__gen_e_acsl_add_5);
+ __gmpz_add(__gen_e_acsl_add_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__12),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
+ __gmpz_init_set_si(__gen_e_acsl__14,3L);
+ __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
+ __e_acsl_assert(__gen_e_acsl_eq_5 == 0,(char *)"Assertion",
+ (char *)"main",(char *)"\\let u = r; u.x + u.y == 3",35);
__gmpz_clear(__gen_e_acsl__12);
+ __gmpz_clear(__gen_e_acsl__13);
+ __gmpz_clear(__gen_e_acsl_add_5);
+ __gmpz_clear(__gen_e_acsl__14);
}
- __e_acsl_initialize((void *)(& s.x),sizeof(int));
s.x = 5;
/*@ assert (\let u = s; u.x) > 0; */
{
- union __anonunion_s_2 __gen_e_acsl_u_14;
- __gen_e_acsl_u_14 = s;
- __e_acsl_assert(__gen_e_acsl_u_14.x > 0,(char *)"Assertion",
- (char *)"main",(char *)"(\\let u = s; u.x) > 0",36);
+ union __anonunion_s_2 __gen_e_acsl_u_17;
+ __gen_e_acsl_u_17 = s;
+ __e_acsl_assert(__gen_e_acsl_u_17.x > 0,(char *)"Assertion",
+ (char *)"main",(char *)"(\\let u = s; u.x) > 0",39);
}
__retres = 0;
- __e_acsl_delete_block((void *)(& s));
__e_acsl_delete_block((void *)(& r));
__e_acsl_delete_block((void *)(& f));
- __e_acsl_delete_block((void *)(& m));
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/let.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/let.0.res.oracle
index 3900d2e7c64..47658609fcf 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/let.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/let.0.res.oracle
@@ -1,7 +1,5 @@
[e-acsl] beginning translation.
-tests/gmp/let.c:29:[e-acsl] warning: E-ACSL construct `let-binding on array or pointer' is not yet supported.
- Ignoring annotation.
-tests/gmp/let.c:27:[e-acsl] warning: E-ACSL construct `let-binding on array or pointer' is not yet supported.
+tests/gmp/let.c:30:[e-acsl] warning: E-ACSL construct `let-binding on array or pointer' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -18,31 +16,31 @@ tests/gmp/let.c:27:[e-acsl] warning: E-ACSL construct `let-binding on array or p
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
[value] using specification for function __e_acsl_memory_init
-[value] using specification for function __e_acsl_store_block
tests/gmp/let.c:7:[value:alarm] warning: assertion got status unknown.
[value] using specification for function __e_acsl_assert
tests/gmp/let.c:9:[value:alarm] warning: assertion got status unknown.
tests/gmp/let.c:12:[value] cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
tests/gmp/let.c:12:[value:alarm] warning: assertion got status unknown.
tests/gmp/let.c:14:[value:alarm] warning: assertion got status unknown.
-[value] using specification for function __e_acsl_full_init
-tests/gmp/let.c:18:[value] cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
-tests/gmp/let.c:18:[value:alarm] warning: assertion got status unknown.
+tests/gmp/let.c:17:[value:alarm] warning: assertion got status unknown.
+tests/gmp/let.c:21:[value] cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
+tests/gmp/let.c:21:[value:alarm] warning: assertion got status unknown.
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_mul
[value] using specification for function __gmpz_cmp
-tests/gmp/let.c:18:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/let.c:21:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-tests/gmp/let.c:21:[value:alarm] warning: assertion got status unknown.
tests/gmp/let.c:24:[value:alarm] warning: assertion got status unknown.
+[value] using specification for function __e_acsl_store_block
+[value] using specification for function __e_acsl_full_init
tests/gmp/let.c:27:[value:alarm] warning: assertion got status unknown.
-tests/gmp/let.c:29:[value] cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
-tests/gmp/let.c:29:[value:alarm] warning: assertion got status unknown.
+tests/gmp/let.c:30:[value:alarm] warning: assertion got status unknown.
+tests/gmp/let.c:32:[value] cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
tests/gmp/let.c:32:[value:alarm] warning: assertion got status unknown.
-[value] using specification for function __e_acsl_initialize
-tests/gmp/let.c:36:[value] cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
-tests/gmp/let.c:36:[value:alarm] warning: assertion got status unknown.
+tests/gmp/let.c:35:[value:alarm] warning: assertion got status unknown.
+tests/gmp/let.c:39:[value] cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
+tests/gmp/let.c:39:[value:alarm] warning: assertion got status unknown.
[value] using specification for function __e_acsl_delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/let.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/let.1.res.oracle
index 8d0c74303e4..e32fc4b2987 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/let.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/let.1.res.oracle
@@ -1,7 +1,5 @@
[e-acsl] beginning translation.
-tests/gmp/let.c:29:[e-acsl] warning: E-ACSL construct `let-binding on array or pointer' is not yet supported.
- Ignoring annotation.
-tests/gmp/let.c:27:[e-acsl] warning: E-ACSL construct `let-binding on array or pointer' is not yet supported.
+tests/gmp/let.c:30:[e-acsl] warning: E-ACSL construct `let-binding on array or pointer' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -18,7 +16,6 @@ tests/gmp/let.c:27:[e-acsl] warning: E-ACSL construct `let-binding on array or p
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
[value] using specification for function __e_acsl_memory_init
-[value] using specification for function __e_acsl_store_block
tests/gmp/let.c:7:[value:alarm] warning: assertion got status unknown.
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_init
@@ -36,22 +33,24 @@ tests/gmp/let.c:12:[value:alarm] warning: assertion got status unknown.
tests/gmp/let.c:12:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
tests/gmp/let.c:14:[value:alarm] warning: assertion got status unknown.
tests/gmp/let.c:14:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
-[value] using specification for function __e_acsl_full_init
-tests/gmp/let.c:18:[value] cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
-tests/gmp/let.c:18:[value:alarm] warning: assertion got status unknown.
-tests/gmp/let.c:18:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/let.c:17:[value:alarm] warning: assertion got status unknown.
+tests/gmp/let.c:17:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/let.c:21:[value] cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
tests/gmp/let.c:21:[value:alarm] warning: assertion got status unknown.
tests/gmp/let.c:21:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
tests/gmp/let.c:24:[value:alarm] warning: assertion got status unknown.
+tests/gmp/let.c:24:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+[value] using specification for function __e_acsl_store_block
+[value] using specification for function __e_acsl_full_init
tests/gmp/let.c:27:[value:alarm] warning: assertion got status unknown.
-tests/gmp/let.c:27:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/let.c:29:[value] cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
-tests/gmp/let.c:29:[value:alarm] warning: assertion got status unknown.
+tests/gmp/let.c:30:[value:alarm] warning: assertion got status unknown.
+tests/gmp/let.c:30:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/let.c:32:[value] cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
tests/gmp/let.c:32:[value:alarm] warning: assertion got status unknown.
-tests/gmp/let.c:32:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
-[value] using specification for function __e_acsl_initialize
-tests/gmp/let.c:36:[value] cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
-tests/gmp/let.c:36:[value:alarm] warning: assertion got status unknown.
+tests/gmp/let.c:35:[value:alarm] warning: assertion got status unknown.
+tests/gmp/let.c:35:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/let.c:39:[value] cannot evaluate ACSL term, unsupported ACSL construct: \let bindings
+tests/gmp/let.c:39:[value:alarm] warning: assertion got status unknown.
[value] using specification for function __e_acsl_delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
--
GitLab