[typing] fix inference of intervals for complex term_lval

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"

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;

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);
       }