diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index f6a1b64190328a6944010dc80de45572c2d3a10d..eedb1df786526354d81e7b1144b458a258094a62 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -109,12 +109,6 @@ let infer_sizeof ty =
let infer_alignof ty = singleton_of_int (Cil.bytesAlignOf ty)
-(* used to infer type for offsets *)
-type offset_interv =
- | I_no_offset (* no offset for this lvalue: will use the host *)
- | I_field of interv (* a field with its infered interval *)
- | I_index (* an index *)
-
let rec infer env t =
let get_cty t = match t.term_type with Ctype ty -> ty | _ -> assert false in
match t.term_node with
@@ -251,12 +245,12 @@ let rec infer env t =
| Ttype _
| Tempty_set -> raise Not_an_integer
-and infer_term_lval env (host, offset) =
- let io = infer_term_offset env offset in
- match io with
- | I_no_offset -> infer_term_host env host
- | I_field i -> i
- | I_index -> raise Not_an_integer
+and infer_term_lval env (host, offset as tlv) =
+ match offset with
+ | TNoOffset -> infer_term_host env host
+ | _ ->
+ let ty = Logic_utils.logicCType (Cil.typeOfTermLval tlv) in
+ interv_of_typ ty
and infer_term_host env = function
| TVar v ->
@@ -272,21 +266,6 @@ and infer_term_host env = function
Printer.pp_typ ty
Printer.pp_term t
-and infer_term_offset env = function
- | TNoOffset -> I_no_offset
- | TField (f, o) ->
- let io = infer_term_offset env o in
- (match io with
- | I_no_offset -> I_field (interv_of_typ f.ftype)
- | I_field _ as i -> i
- | I_index ->
- (match Cil.unrollType f.ftype with
- | TArray(ty, _, _, _) -> I_field (interv_of_typ ty)
- | TPtr _ -> raise Not_an_integer
- | _ -> assert false))
- | TIndex _ -> I_index
- | TModel _ -> Error.not_yet "model"
-
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
index 4443f95e060d3b3ba6a6eaa54f6d9c0ac0cb6261..95fee64be9ecc16f1cd16bd8662532044f9701f8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
@@ -35,16 +35,16 @@ int search(int elt)
__gen_e_acsl_i = 0;
while (1) {
if (__gen_e_acsl_i < k) ; else break;
- __e_acsl_assert(__gen_e_acsl_i < 10,(char *)"RTE",(char *)"search",
- (char *)"index_bound: __gen_e_acsl_i < 10",18);
- __e_acsl_assert(0 <= __gen_e_acsl_i,(char *)"RTE",(char *)"search",
- (char *)"index_bound: 0 <= __gen_e_acsl_i",18);
- if (A[__gen_e_acsl_i] < elt) ;
+ __e_acsl_assert((unsigned int)((unsigned long)__gen_e_acsl_i) < 10,
+ (char *)"RTE",(char *)"search",
+ (char *)"index_bound: (unsigned long)__gen_e_acsl_i < 10",
+ 18);
+ if (A[(unsigned long)__gen_e_acsl_i] < elt) ;
else {
__gen_e_acsl_forall = 0;
goto e_acsl_end_loop1;
}
- __gen_e_acsl_i ++;
+ __gen_e_acsl_i = (int)(__gen_e_acsl_i + 1L);
}
e_acsl_end_loop1: ;
__e_acsl_assert(__gen_e_acsl_forall,(char *)"Invariant",(char *)"search",
@@ -79,18 +79,16 @@ int search(int elt)
__gen_e_acsl_i_2 = 0;
while (1) {
if (__gen_e_acsl_i_2 < k) ; else break;
- __e_acsl_assert(__gen_e_acsl_i_2 < 10,(char *)"RTE",
- (char *)"search",
- (char *)"index_bound: __gen_e_acsl_i_2 < 10",18);
- __e_acsl_assert(0 <= __gen_e_acsl_i_2,(char *)"RTE",
- (char *)"search",
- (char *)"index_bound: 0 <= __gen_e_acsl_i_2",18);
- if (A[__gen_e_acsl_i_2] < elt) ;
+ __e_acsl_assert((unsigned int)((unsigned long)__gen_e_acsl_i_2) < 10,
+ (char *)"RTE",(char *)"search",
+ (char *)"index_bound: (unsigned long)__gen_e_acsl_i_2 < 10",
+ 18);
+ if (A[(unsigned long)__gen_e_acsl_i_2] < elt) ;
else {
__gen_e_acsl_forall_2 = 0;
goto e_acsl_end_loop2;
}
- __gen_e_acsl_i_2 ++;
+ __gen_e_acsl_i_2 = (int)(__gen_e_acsl_i_2 + 1L);
}
e_acsl_end_loop2: ;
__e_acsl_assert(__gen_e_acsl_forall_2,(char *)"Invariant",
@@ -150,10 +148,10 @@ 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(__gen_e_acsl_i + 1 < 10,(char *)"RTE",(char *)"search",
- (char *)"index_bound: (int)(__gen_e_acsl_i+1) < 10",7);
- __e_acsl_assert(0 <= __gen_e_acsl_i + 1,(char *)"RTE",(char *)"search",
- (char *)"index_bound: 0 <= (int)(__gen_e_acsl_i+1)",7);
+ __e_acsl_assert((unsigned int)((unsigned long)(__gen_e_acsl_i + 1)) < 10,
+ (char *)"RTE",(char *)"search",
+ (char *)"index_bound: (unsigned long)(__gen_e_acsl_i+1) < 10",
+ 7);
__e_acsl_assert(__gen_e_acsl_i < 10,(char *)"RTE",(char *)"search",
(char *)"index_bound: __gen_e_acsl_i < 10",7);
__e_acsl_assert(0 <= __gen_e_acsl_i,(char *)"RTE",(char *)"search",
@@ -163,7 +161,7 @@ int __gen_e_acsl_search(int elt)
__gen_e_acsl_forall = 0;
goto e_acsl_end_loop3;
}
- __gen_e_acsl_i ++;
+ __gen_e_acsl_i = (int)(__gen_e_acsl_i + 1L);
}
e_acsl_end_loop3: ;
__e_acsl_assert(__gen_e_acsl_forall,(char *)"Precondition",
@@ -186,7 +184,7 @@ int __gen_e_acsl_search(int elt)
__gen_e_acsl_forall_2 = 0;
goto e_acsl_end_loop5;
}
- __gen_e_acsl_j_2 ++;
+ __gen_e_acsl_j_2 = (int)(__gen_e_acsl_j_2 + 1L);
}
e_acsl_end_loop5: ;
__gen_e_acsl_at_2 = __gen_e_acsl_forall_2;
@@ -207,7 +205,7 @@ int __gen_e_acsl_search(int elt)
__gen_e_acsl_exists = 1;
goto e_acsl_end_loop4;
}
- __gen_e_acsl_j ++;
+ __gen_e_acsl_j = (int)(__gen_e_acsl_j + 1L);
}
e_acsl_end_loop4: ;
__gen_e_acsl_at = __gen_e_acsl_exists;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
index e559b441ee9b011beb77f9506a719808247d6276..138fec283e4f154d6d5288d47e998384b6840d45 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
@@ -37,12 +37,16 @@ int main(void)
(char *)"*p == 1",11);
}
/*@ assert t[0] ≡ 2; */
- __e_acsl_assert(t[0] == 2,(char *)"Assertion",(char *)"main",
+ __e_acsl_assert(t[0UL] == 2,(char *)"Assertion",(char *)"main",
(char *)"t[0] == 2",12);
/*@ assert t[2] ≡ 4; */
__e_acsl_assert(t[2] == 4,(char *)"Assertion",(char *)"main",
(char *)"t[2] == 4",13);
/*@ assert t[(2*sizeof(int))/sizeof((int)0x0)] ≡ 4; */
+ __e_acsl_assert((unsigned long)((unsigned long)(2 * 4) / 4) < 3,
+ (char *)"RTE",(char *)"main",
+ (char *)"index_bound: (unsigned long)((unsigned long)(2*4)/4) < 3",
+ 14);
__e_acsl_assert(t[(2 * 4) / 4] == 4,(char *)"Assertion",(char *)"main",
(char *)"t[(2*sizeof(int))/sizeof((int)0x0)] == 4",14);
{
@@ -50,30 +54,28 @@ int main(void)
i = 0;
while (i < 2) {
/*@ assert t[i] ≡ i+2; */
- __e_acsl_assert(i < 3,(char *)"RTE",(char *)"main",
- (char *)"index_bound: i < 3",17);
- __e_acsl_assert(0 <= i,(char *)"RTE",(char *)"main",
- (char *)"index_bound: 0 <= i",17);
- __e_acsl_assert((long)t[i] == (long)i + (long)2,(char *)"Assertion",
+ __e_acsl_assert((unsigned int)((unsigned long)i) < 3,(char *)"RTE",
+ (char *)"main",
+ (char *)"index_bound: (unsigned long)i < 3",17);
+ __e_acsl_assert(t[(unsigned long)i] == i + 2,(char *)"Assertion",
(char *)"main",(char *)"t[i] == i+2",17);
/*@ assert t[2-i] ≡ 4-i; */
- __e_acsl_assert((long)2 - (long)i < (long)3,(char *)"RTE",
- (char *)"main",
- (char *)"index_bound: (long)(2-(long)i) < 3",18);
- __e_acsl_assert(0L <= (long)2 - (long)i,(char *)"RTE",(char *)"main",
- (char *)"index_bound: 0 <= (long)(2-(long)i)",18);
- __e_acsl_assert((long)t[(long)2 - (long)i] == (long)4 - (long)i,
- (char *)"Assertion",(char *)"main",
- (char *)"t[2-i] == 4-i",18);
+ __e_acsl_assert((unsigned int)((unsigned long)(2 - i)) < 3,
+ (char *)"RTE",(char *)"main",
+ (char *)"index_bound: (unsigned long)((long)(2-i)) < 3",
+ 18);
+ __e_acsl_assert(t[(unsigned long)(2 - i)] == 4 - i,(char *)"Assertion",
+ (char *)"main",(char *)"t[2-i] == 4-i",18);
/*@ assert *(&t[2]-i) ≡ 4-i; */
{
int __gen_e_acsl_valid_read_2;
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& t[2] - i),
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& t[2] - (unsigned long)i),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"main",
- (char *)"mem_access: \\valid_read(&t[2]-i)",19);
- __e_acsl_assert((long)*(& t[2] - i) == (long)4 - (long)i,
+ (char *)"mem_access: \\valid_read(&t[2]-(unsigned long)i)",
+ 19);
+ __e_acsl_assert(*(& t[2] - (unsigned long)i) == 4 - i,
(char *)"Assertion",(char *)"main",
(char *)"*(&t[2]-i) == 4-i",19);
}