diff --git a/src/plugins/e-acsl/new_typing.ml b/src/plugins/e-acsl/new_typing.ml
index 15b09a0af35b9d37a3993d9e4686a82d222e0f02..a7ae7dbb5ba061576d8f2b2504c8c24380a34517 100644
--- a/src/plugins/e-acsl/new_typing.ml
+++ b/src/plugins/e-acsl/new_typing.ml
@@ -61,6 +61,10 @@ let typ_of_integer_ty = function
let c_int = C_type IInt
+let size_t () = match Cil.theMachine.Cil.typeOfSizeOf with
+ | TInt(kind, _) -> C_type kind
+ | _ -> assert false
+
include Datatype.Make
(struct
type t = integer_ty
@@ -302,15 +306,10 @@ let rec type_term env ~ctx t =
Other
| TBinOp ((PlusPI | IndexPI | MinusPI), t1, t2) ->
-(* Options.feedback "BIN PI %a ; %a" Printer.pp_term t1 Printer.pp_term t2; (* HERE *)*)
(* it is a pointer, as well as [t1], while [t2] is a size_t.
Both [t1] and [t2] must be typed. *)
ignore (type_term env ~ctx:Other t1);
- let size_t_kind = match Cil.theMachine.Cil.typeOfSizeOf with
- | TInt(kind, _) -> kind
- | _ -> assert false
- in
- ignore (type_term env ~ctx:(C_type size_t_kind) t2);
+ ignore (type_term env ~ctx:(size_t ()) t2);
Other
| Tapp (_,_,_) -> Error.not_yet "logic function application"
@@ -345,9 +344,8 @@ and type_term_offset env = function
| TField(_, toff)
| TModel(_, toff) -> type_term_offset env toff
| TIndex(t, toff) ->
- (* HERE: Other est faux ? *)
- Options.feedback "INDEX";
- ignore (type_term env ~ctx:Other t);
+ (* [t] is an array index which must fits into size_t *)
+ ignore (type_term env ~ctx:(size_t ()) t);
type_term_offset env toff
let rec type_predicate_named env p =
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
index 156fd24a1dd5319903f4652e0972c4cb1a0e33f4..fbc5d522f1b971c974b711342f2879c2cb0aa0bc 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
@@ -5,13 +5,15 @@ tests/bts/bts1399.c:22:[e-acsl] warning: E-ACSL construct `complete behaviors' i
Ignoring annotation.
tests/bts/bts1399.c:22:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:179:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
index 233878777882dc8f0c131b34d5bb0ed4db0cd2ab..eec556a814892f9a85a5d4dfa3ea30e86cd4504b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
@@ -25,7 +25,7 @@ int main(void)
(char *)"mem_access: \\valid_read(&state->bitsInQueue)",
22);
__gen_e_acsl_initialized = __e_acsl_initialized((void *)(& state->dataQueue[
- state->bitsInQueue / (unsigned int)8]),
+ state->bitsInQueue / 8]),
sizeof(unsigned char __attribute__((
__aligned__(32)))));
__e_acsl_assert(! __gen_e_acsl_initialized,(char *)"Assertion",
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_base_addr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_base_addr.c
index 8363cb460ba289cab38856923fa012437eb58d0d..14aba6b8cd0dce558d00480d07d29297a9b68ef3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_base_addr.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_base_addr.c
@@ -48,7 +48,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_3;
void *__gen_e_acsl_base_addr_4;
- __gen_e_acsl_base_addr_3 = __e_acsl_base_addr((void *)(& A[3]));
+ __gen_e_acsl_base_addr_3 = __e_acsl_base_addr((void *)(& A[(unsigned long)3]));
__gen_e_acsl_base_addr_4 = __e_acsl_base_addr((void *)PA);
__e_acsl_assert(__gen_e_acsl_base_addr_3 == __gen_e_acsl_base_addr_4,
(char *)"Assertion",(char *)"main",
@@ -69,8 +69,8 @@ int main(void)
{
void *__gen_e_acsl_base_addr_7;
void *__gen_e_acsl_base_addr_8;
- __gen_e_acsl_base_addr_7 = __e_acsl_base_addr((void *)(PA + 2));
- __gen_e_acsl_base_addr_8 = __e_acsl_base_addr((void *)(& A[3]));
+ __gen_e_acsl_base_addr_7 = __e_acsl_base_addr((void *)(PA + (unsigned long)2));
+ __gen_e_acsl_base_addr_8 = __e_acsl_base_addr((void *)(& A[(unsigned long)3]));
__e_acsl_assert(__gen_e_acsl_base_addr_7 == __gen_e_acsl_base_addr_8,
(char *)"Assertion",(char *)"main",
(char *)"\\base_addr(PA+2) == \\base_addr(&A[3])",17);
@@ -99,7 +99,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_11;
void *__gen_e_acsl_base_addr_12;
- __gen_e_acsl_base_addr_11 = __e_acsl_base_addr((void *)(& a[3]));
+ __gen_e_acsl_base_addr_11 = __e_acsl_base_addr((void *)(& a[(unsigned long)3]));
__gen_e_acsl_base_addr_12 = __e_acsl_base_addr((void *)pa);
__e_acsl_assert(__gen_e_acsl_base_addr_11 == __gen_e_acsl_base_addr_12,
(char *)"Assertion",(char *)"main",
@@ -121,7 +121,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_15;
void *__gen_e_acsl_base_addr_16;
- __gen_e_acsl_base_addr_15 = __e_acsl_base_addr((void *)(pa + 2));
+ __gen_e_acsl_base_addr_15 = __e_acsl_base_addr((void *)(pa + (unsigned long)2));
__gen_e_acsl_base_addr_16 = __e_acsl_base_addr((void *)(a));
__e_acsl_assert(__gen_e_acsl_base_addr_15 == __gen_e_acsl_base_addr_16,
(char *)"Assertion",(char *)"main",
@@ -145,7 +145,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_19;
void *__gen_e_acsl_base_addr_20;
- __gen_e_acsl_base_addr_19 = __e_acsl_base_addr((void *)(pl + 2));
+ __gen_e_acsl_base_addr_19 = __e_acsl_base_addr((void *)(pl + (unsigned long)2));
__gen_e_acsl_base_addr_20 = __e_acsl_base_addr((void *)(& l));
__e_acsl_assert(__gen_e_acsl_base_addr_19 == __gen_e_acsl_base_addr_20,
(char *)"Assertion",(char *)"main",
@@ -195,8 +195,8 @@ int main(void)
{
void *__gen_e_acsl_base_addr_27;
void *__gen_e_acsl_base_addr_28;
- __gen_e_acsl_base_addr_27 = __e_acsl_base_addr((void *)(p + 1));
- __gen_e_acsl_base_addr_28 = __e_acsl_base_addr((void *)(pd + 5));
+ __gen_e_acsl_base_addr_27 = __e_acsl_base_addr((void *)(p + (unsigned long)1));
+ __gen_e_acsl_base_addr_28 = __e_acsl_base_addr((void *)(pd + (unsigned long)5));
__e_acsl_assert(__gen_e_acsl_base_addr_27 == __gen_e_acsl_base_addr_28,
(char *)"Assertion",(char *)"main",
(char *)"\\base_addr(p+1) == \\base_addr(pd+5)",45);
@@ -205,8 +205,8 @@ int main(void)
{
void *__gen_e_acsl_base_addr_29;
void *__gen_e_acsl_base_addr_30;
- __gen_e_acsl_base_addr_29 = __e_acsl_base_addr((void *)(p + 11));
- __gen_e_acsl_base_addr_30 = __e_acsl_base_addr((void *)(pd + 1));
+ __gen_e_acsl_base_addr_29 = __e_acsl_base_addr((void *)(p + (unsigned long)11));
+ __gen_e_acsl_base_addr_30 = __e_acsl_base_addr((void *)(pd + (unsigned long)1));
__e_acsl_assert(__gen_e_acsl_base_addr_29 == __gen_e_acsl_base_addr_30,
(char *)"Assertion",(char *)"main",
(char *)"\\base_addr(p+11) == \\base_addr(pd+1)",46);
@@ -217,7 +217,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_31;
void *__gen_e_acsl_base_addr_32;
- __gen_e_acsl_base_addr_31 = __e_acsl_base_addr((void *)(p + 5));
+ __gen_e_acsl_base_addr_31 = __e_acsl_base_addr((void *)(p + (unsigned long)5));
__gen_e_acsl_base_addr_32 = __e_acsl_base_addr((void *)pd);
__e_acsl_assert(__gen_e_acsl_base_addr_31 == __gen_e_acsl_base_addr_32,
(char *)"Assertion",(char *)"main",
@@ -227,7 +227,7 @@ int main(void)
{
void *__gen_e_acsl_base_addr_33;
void *__gen_e_acsl_base_addr_34;
- __gen_e_acsl_base_addr_33 = __e_acsl_base_addr((void *)(p - 5));
+ __gen_e_acsl_base_addr_33 = __e_acsl_base_addr((void *)(p - (unsigned long)5));
__gen_e_acsl_base_addr_34 = __e_acsl_base_addr((void *)pd);
__e_acsl_assert(__gen_e_acsl_base_addr_33 == __gen_e_acsl_base_addr_34,
(char *)"Assertion",(char *)"main",