diff --git a/src/plugins/e-acsl/tests/bts/bts2231.i b/src/plugins/e-acsl/tests/bts/bts2231.i
new file mode 100644
index 0000000000000000000000000000000000000000..8040723e115afb78b9ed45da517570e2231b4c18
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/bts2231.i
@@ -0,0 +1,10 @@
+/* run.config
+ COMMENT: bts #2231, issue with typing of casts
+*/
+
+long A = 0;
+
+int main(void) {
+ /*@ assert A + (long)((long)(3 * A) - 1) == -1; */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2231.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2231.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..73a14510c9fb7ae6565e7c60d7c7f96a30c87910
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle
@@ -0,0 +1,4 @@
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+[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.
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 c2302f70811614faa51481211425ec7a4d140363..677c5c9103eaad8fc4163eb80821eda0016ac97a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -78,11 +78,11 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_store_block((void *)(& buf),8UL);
{
int __gen_e_acsl_forall_2;
- unsigned long __gen_e_acsl_k;
+ unsigned int __gen_e_acsl_k;
__gen_e_acsl_forall_2 = 1;
__gen_e_acsl_k = 0U;
while (1) {
- if (__gen_e_acsl_k < (unsigned int)((int)n)) ; else break;
+ if (__gen_e_acsl_k < (int)((unsigned int)n)) ; else break;
{
int __gen_e_acsl_valid_read_3;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)((char *)buf + __gen_e_acsl_k),
@@ -106,11 +106,11 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
__gen_e_acsl_at_2 = buf;
{
int __gen_e_acsl_exists;
- unsigned long __gen_e_acsl_i;
+ unsigned int __gen_e_acsl_i;
__gen_e_acsl_exists = 0;
__gen_e_acsl_i = 0U;
while (1) {
- if (__gen_e_acsl_i < (unsigned int)((int)n)) ; else break;
+ if (__gen_e_acsl_i < (int)((unsigned int)n)) ; else break;
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)((char *)buf + __gen_e_acsl_i),
@@ -137,14 +137,15 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
if (! __gen_e_acsl_at) __gen_e_acsl_implies = 1;
else {
int __gen_e_acsl_forall;
- unsigned long __gen_e_acsl_j;
+ unsigned int __gen_e_acsl_j;
__gen_e_acsl_forall = 1;
__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 int)__gen_e_acsl_offset) ;
+ if (__gen_e_acsl_j < (int)((unsigned int)__gen_e_acsl_offset))
+ ;
else break;
}
{
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
new file mode 100644
index 0000000000000000000000000000000000000000..3857056fbcde3e6ad7b5b7a7ec4e40906a477e39
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
@@ -0,0 +1,57 @@
+/* Generated by Frama-C */
+long A = (long)0;
+int main(void)
+{
+ int __retres;
+ /*@ assert A+(long)((long)(3*A)-1) ≡ -1; */
+ {
+ __e_acsl_mpz_t __gen_e_acsl_A;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_mul;
+ long __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ long __gen_e_acsl__5;
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ int __gen_e_acsl_eq;
+ __gmpz_init_set_si(__gen_e_acsl_A,A);
+ __gmpz_init_set_si(__gen_e_acsl_,3L);
+ __gmpz_init(__gen_e_acsl_mul);
+ __gmpz_mul(__gen_e_acsl_mul,(__e_acsl_mpz_struct const *)(__gen_e_acsl_),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_A));
+ __gen_e_acsl__2 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
+ __gmpz_init_set_si(__gen_e_acsl__3,__gen_e_acsl__2);
+ __gmpz_init_set_si(__gen_e_acsl__4,1L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __gen_e_acsl__5 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_sub));
+ __gmpz_init_set_si(__gen_e_acsl__6,__gen_e_acsl__5);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_A),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ __gmpz_init_set_si(__gen_e_acsl__7,(long)(-1));
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
+ (char *)"A+(long)((long)(3*A)-1) == -1",8);
+ __gmpz_clear(__gen_e_acsl_A);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_mul);
+ __gmpz_clear(__gen_e_acsl__3);
+ __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl__7);
+ }
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
index 3c37f649684a8abc508edbe934a65b43e927f17c..7802e16a2d7c6f227b7a16cd6b4dba06e0337094 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
@@ -18,8 +18,9 @@ FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns cl
[value] using specification for function __gmpz_init
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_q
-[value] using specification for function __gmpz_get_ui
+[value] using specification for function __gmpz_get_si
[value] using specification for function __gmpz_clear
[value] using specification for function __gmpz_add
+tests/gmp/arith.i:34:[value] warning: signed overflow. assert -2147483648 ≤ 1+__gen_e_acsl__7;
tests/gmp/arith.i:34:[value] warning: signed overflow. assert 1+__gen_e_acsl__7 ≤ 2147483647;
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
index 69d5e43631b18deaf53cf4bcbb7f43dc9ee0c7a7..e8f90152326c8e936e77ea5043d850dc467cd6b6 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
@@ -12,10 +12,11 @@ FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns cl
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_size ∈ [--..--]
[value] using specification for function __gmpz_init_set_si
-[value] using specification for function __gmpz_get_ui
-[value] using specification for function __gmpz_init_set_ui
+[value] using specification for function __gmpz_get_si
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
+[value] using specification for function __gmpz_get_ui
+[value] using specification for function __gmpz_init_set_ui
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
index ef0f72e74c99407c5f04b7c5a3ba74d5565b5d56..00636435b9f21e07c7f319ad15e80824a33ba135 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
@@ -35,7 +35,7 @@ int main(void)
__e_acsl_mpz_t __gen_e_acsl__2;
int __gen_e_acsl_div_guard;
__e_acsl_mpz_t __gen_e_acsl_div;
- unsigned long __gen_e_acsl__3;
+ long __gen_e_acsl__3;
__gmpz_init_set_str(__gen_e_acsl_,"309485009821345068724781055",10);
__gmpz_init_set_si(__gen_e_acsl__2,0L);
__gen_e_acsl_div_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_),
@@ -48,7 +48,7 @@ int main(void)
__gmpz_tdiv_q(__gen_e_acsl_div,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gen_e_acsl__3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_div));
+ __gen_e_acsl__3 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_div));
__e_acsl_assert(__gen_e_acsl__3 == 1,(char *)"Assertion",(char *)"main",
(char *)"0xffffffffffffffffffffff/0xffffffffffffffffffffff == 1",
18);
@@ -98,7 +98,7 @@ int main(void)
__e_acsl_mpz_t __gen_e_acsl__6;
int __gen_e_acsl_div_guard_2;
__e_acsl_mpz_t __gen_e_acsl_div_2;
- unsigned long __gen_e_acsl__7;
+ long __gen_e_acsl__7;
__gmpz_init_set_si(__gen_e_acsl_z,z);
__gmpz_init_set_si(__gen_e_acsl__4,1L);
__gmpz_init(__gen_e_acsl_add);
@@ -116,7 +116,8 @@ int main(void)
__gmpz_tdiv_q(__gen_e_acsl_div_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
- __gen_e_acsl__7 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_div_2));
+ __gen_e_acsl__7 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_div_2));
+ /*@ assert Value: signed_overflow: -2147483648 ≤ 1+__gen_e_acsl__7; */
/*@ assert Value: signed_overflow: 1+__gen_e_acsl__7 ≤ 2147483647; */
__e_acsl_assert(1 + __gen_e_acsl__7 == 1,(char *)"Assertion",
(char *)"main",
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
index 844c8bac7eb8b4afab7630c10cce4e434fd92b16..f1bc478568aa681b700eea95e7d2f65a0243f59f 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
@@ -29,7 +29,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:99:[value] warning: function __gmpz_import: pre
[value] using specification for function __e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_r
-[value] using specification for function __gmpz_get_ui
+[value] using specification for function __gmpz_get_si
tests/gmp/longlong.i:17:[value] warning: pointer comparison.
assert \pointer_comparable((void *)__gen_e_acsl__4, (void *)1);
[value] using specification for function __gmpz_clear
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
index 706a1e4335d58a3912aa374551f8794ac9f583d3..a9c0cf751272acaee55b8aa6acaa4d351da8375a 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
@@ -35,7 +35,7 @@ int search(int elt)
__gen_e_acsl_i = 0;
while (1) {
if (__gen_e_acsl_i < k) ; else break;
- __e_acsl_assert((unsigned int)((unsigned long)__gen_e_acsl_i) < 10U,
+ __e_acsl_assert((unsigned long)((unsigned int)__gen_e_acsl_i) < 10U,
(char *)"RTE",(char *)"search",
(char *)"index_bound: (unsigned long)__gen_e_acsl_i < 10",
18);
@@ -79,7 +79,7 @@ int search(int elt)
__gen_e_acsl_i_2 = 0;
while (1) {
if (__gen_e_acsl_i_2 < k) ; else break;
- __e_acsl_assert((unsigned int)((unsigned long)__gen_e_acsl_i_2) < 10U,
+ __e_acsl_assert((unsigned long)((unsigned int)__gen_e_acsl_i_2) < 10U,
(char *)"RTE",(char *)"search",
(char *)"index_bound: (unsigned long)__gen_e_acsl_i_2 < 10",
18);
@@ -148,7 +148,7 @@ int __gen_e_acsl_search(int elt)
__gen_e_acsl_i = 0;
while (1) {
if (__gen_e_acsl_i < 9) ; else break;
- __e_acsl_assert((unsigned int)((unsigned long)(__gen_e_acsl_i + 1L)) < 10U,
+ __e_acsl_assert((unsigned long)((unsigned int)(__gen_e_acsl_i + 1L)) < 10U,
(char *)"RTE",(char *)"search",
(char *)"index_bound: (unsigned long)(__gen_e_acsl_i+1) < 10",
7);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
index 05ebfe2e433308df264cb866d57785b3d0e222d1..9f4b1ba21d8064a39d6fd32d22a89069bded0b69 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
@@ -54,13 +54,13 @@ int main(void)
i = 0;
while (i < 2) {
/*@ assert t[i] ≡ i+2; */
- __e_acsl_assert((unsigned int)((unsigned long)i) < 3U,(char *)"RTE",
+ __e_acsl_assert((unsigned long)((unsigned int)i) < 3U,(char *)"RTE",
(char *)"main",
(char *)"index_bound: (unsigned long)i < 3",17);
__e_acsl_assert(t[(unsigned long)i] == i + 2L,(char *)"Assertion",
(char *)"main",(char *)"t[i] == i+2",17);
/*@ assert t[2-i] ≡ 4-i; */
- __e_acsl_assert((unsigned int)((unsigned long)(2L - i)) < 3U,
+ __e_acsl_assert((unsigned long)((unsigned int)(2L - i)) < 3U,
(char *)"RTE",(char *)"main",
(char *)"index_bound: (unsigned long)((long)(2-i)) < 3",
18);
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index dfa9d344029730670ef19de89442b5bddc89069c..bcb73b373ca6c5f3394fd6ff59971d44b0fcadf7 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -119,7 +119,7 @@ let add_cast ~loc ?name env ctx is_mpz_string t_opt e =
if (Gmpz.is_t ty || is_mpz_string) then
(* we get an mpz, but it fits into a C integer: convert it *)
let fname, new_ty =
- if Cil.isSignedInteger ty then
+ if Cil.isSignedInteger ctx then
"__gmpz_get_si", Cil.longType
else
"__gmpz_get_ui", Cil.ulongType
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index f349a4f66f4c50444db2141bc189dd02bf02db8d..7b7832024fc6384ec236fb7cffee767eb7e1227b 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -338,7 +338,8 @@ let rec type_term ~force ?ctx t =
| TCoerce(t', _) ->
let ctx =
try
- let i = Interval.infer t' in
+ (* compute the smallest interval from the whole term [t] *)
+ let i = Interval.infer t in
(* nothing more to do: [i] is already more precise than what we
could infer from the arguments of the cast. *)
ty_of_interv ?ctx i