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 077c0847b439ca7600c915855d19bbb51961a4d7..56bc91ebe1d98aedec7c0081c125f3f5763625f1 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
@@ -1,6 +1,4 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/bts/bts1390.c:13:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:13:[value] warning: function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:18:[value] warning: out of bounds read. assert \valid_read(s);
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:150:[value] warning: function __gmpz_add: precondition got status invalid.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
index d8e364312905cdab01f8e1cb5bc71d33239d5aa7..370a935bc4793ba14b6cf1f7dbef6dc0727e4a1f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -78,29 +78,13 @@ int __gen_e_acsl_sorted(int *t, int n)
while (1) {
if (__gen_e_acsl_i < n) ; else break;
{
-<<<<<<< HEAD
int __gen_e_acsl_valid_read;
int __gen_e_acsl_valid_read_2;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(t + (unsigned long)((unsigned int)__gen_e_acsl_i)),
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(t + (unsigned long)__gen_e_acsl_i),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",
(char *)"sorted",
(char *)"mem_access: \\valid_read(t+(unsigned long)__gen_e_acsl_i)",
-||||||| merged common ancestors
- int __e_acsl_valid_read;
- int __e_acsl_valid_read_2;
- __e_acsl_valid_read = __valid_read((void *)(t + (unsigned long)((unsigned int)__e_acsl_i)),
- sizeof(int));
- __e_acsl_assert(__e_acsl_valid_read,(char *)"RTE",(char *)"sorted",
- (char *)"mem_access: \\valid_read(t+(unsigned long)__e_acsl_i)",
-=======
- int __e_acsl_valid_read;
- int __e_acsl_valid_read_2;
- __e_acsl_valid_read = __valid_read((void *)(t + (unsigned long)__e_acsl_i),
- sizeof(int));
- __e_acsl_assert(__e_acsl_valid_read,(char *)"RTE",(char *)"sorted",
- (char *)"mem_access: \\valid_read(t+(unsigned long)__e_acsl_i)",
->>>>>>> [tests] fix additional oracles
6);
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(t + (unsigned long)(
__gen_e_acsl_i - 1)),
@@ -116,13 +100,7 @@ int __gen_e_acsl_sorted(int *t, int n)
goto e_acsl_end_loop1;
}
}
-<<<<<<< HEAD
- __gen_e_acsl_i ++;
-||||||| merged common ancestors
- __e_acsl_i ++;
-=======
- __e_acsl_i = (int)(__e_acsl_i + 1L);
->>>>>>> [tests] fix additional oracles
+ __gen_e_acsl_i = (int)(__gen_e_acsl_i + 1L);
}
e_acsl_end_loop1: ;
__gen_e_acsl_at = __gen_e_acsl_forall;
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 c0b7cc3487b1b3db4c20791b77745f4f326826d4..f2790b2a2d6e506dae914675af757c8ca61d1049 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -37,7 +37,6 @@ void *memchr(void const *buf, int c, size_t n)
s = (char *)buf;
i = 0;
while ((size_t)i < n) {
- /*@ assert Value: mem_access: \valid_read(s); */
if ((int)*s == c) {
__e_acsl_full_init((void *)(& __retres));
__retres = (void *)s;
@@ -80,7 +79,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
int __gen_e_acsl_forall_2;
unsigned long __gen_e_acsl_k;
__gen_e_acsl_forall_2 = 1;
- __gen_e_acsl_k = (unsigned long)0;
+ __gen_e_acsl_k = 0;
while (1) {
if (__gen_e_acsl_k < n) ; else break;
{
@@ -97,7 +96,19 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
goto e_acsl_end_loop3;
}
}
- __gen_e_acsl_k ++;
+ {
+ mpz_t __gen_e_acsl__5;
+ mpz_t __gen_e_acsl_add_3;
+ unsigned long __gen_e_acsl__6;
+ __gmpz_init_set_ui(__gen_e_acsl__5,1UL);
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,(__mpz_struct const *)__gen_e_acsl_k,
+ (__mpz_struct const *)(__gen_e_acsl__5));
+ __gen_e_acsl__6 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_add_3));
+ __gen_e_acsl_k = __gen_e_acsl__6;
+ __gmpz_clear(__gen_e_acsl__5);
+ __gmpz_clear(__gen_e_acsl_add_3);
+ }
}
e_acsl_end_loop3: ;
__gen_e_acsl_at_4 = __gen_e_acsl_forall_2;
@@ -109,7 +120,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
int __gen_e_acsl_exists;
unsigned long __gen_e_acsl_i;
__gen_e_acsl_exists = 0;
- __gen_e_acsl_i = (unsigned long)0;
+ __gen_e_acsl_i = 0;
while (1) {
if (__gen_e_acsl_i < n) ; else break;
{
@@ -126,7 +137,19 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
goto e_acsl_end_loop1;
}
}
- __gen_e_acsl_i ++;
+ {
+ mpz_t __gen_e_acsl_;
+ mpz_t __gen_e_acsl_add;
+ unsigned long __gen_e_acsl__2;
+ __gmpz_init_set_ui(__gen_e_acsl_,1UL);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,(__mpz_struct const *)__gen_e_acsl_i,
+ (__mpz_struct const *)(__gen_e_acsl_));
+ __gen_e_acsl__2 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_i = __gen_e_acsl__2;
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_add);
+ }
}
e_acsl_end_loop1: ;
__gen_e_acsl_at = __gen_e_acsl_exists;
@@ -140,13 +163,12 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
int __gen_e_acsl_forall;
unsigned long __gen_e_acsl_j;
__gen_e_acsl_forall = 1;
- __gen_e_acsl_j = (unsigned long)0;
+ __gen_e_acsl_j = 0;
while (1) {
{
int __gen_e_acsl_offset;
__gen_e_acsl_offset = __e_acsl_offset(__retres);
- if (__gen_e_acsl_j < (unsigned long)__gen_e_acsl_offset) ;
- else break;
+ if (__gen_e_acsl_j < __gen_e_acsl_offset) ; else break;
}
{
int __gen_e_acsl_valid_read_2;
@@ -163,7 +185,19 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
goto e_acsl_end_loop2;
}
}
- __gen_e_acsl_j ++;
+ {
+ mpz_t __gen_e_acsl__3;
+ mpz_t __gen_e_acsl_add_2;
+ unsigned long __gen_e_acsl__4;
+ __gmpz_init_set_ui(__gen_e_acsl__3,1UL);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,(__mpz_struct const *)__gen_e_acsl_j,
+ (__mpz_struct const *)(__gen_e_acsl__3));
+ __gen_e_acsl__4 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_add_2));
+ __gen_e_acsl_j = __gen_e_acsl__4;
+ __gmpz_clear(__gen_e_acsl__3);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ }
}
e_acsl_end_loop2: ;
__gen_e_acsl_implies = __gen_e_acsl_forall;