[typing] fix issue with -e-acsl-gmp-only and quantifier

src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c

@@ -3,6 +3,7 @@
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   /*@ assert ∀ ℤ x; 0 ≤ x ≤ 1 ⇒ x ≡ 0 ∨ x ≡ 1; */
   {
     {
@@ -204,7 +205,41 @@ int main(void)
                       25);
     }
   }
+  {
+    int buf[10];
+    __e_acsl_store_block((void *)(buf),(size_t)40);
+    /*@ assert ∀ ℤ i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */
+    {
+      {
+        int __gen_e_acsl_forall_7;
+        int __gen_e_acsl_i;
+        __gen_e_acsl_forall_7 = 1;
+        __gen_e_acsl_i = 0;
+        while (1) {
+          if (__gen_e_acsl_i < 10) ; else break;
+          {
+            int __gen_e_acsl_valid;
+            __gen_e_acsl_valid = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i]),
+                                                sizeof(int));
+            if (__gen_e_acsl_valid) ;
+            else {
+              __gen_e_acsl_forall_7 = 0;
+              goto e_acsl_end_loop9;
+            }
+          }
+          __gen_e_acsl_i ++;
+        }
+        e_acsl_end_loop9: ;
+        __e_acsl_assert(__gen_e_acsl_forall_7,(char *)"Assertion",
+                        (char *)"main",
+                        (char *)"\\forall integer i; 0 <= i < 10 ==> \\valid(&buf[i])",
+                        30);
+        __e_acsl_delete_block((void *)(buf));
+      }
+    }
+  }
   __retres = 0;
+  __e_acsl_memory_clean();
   return __retres;
 }
 

src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c

@@ -3,6 +3,7 @@
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   /*@ assert ∀ ℤ x; 0 ≤ x ≤ 1 ⇒ x ≡ 0 ∨ x ≡ 1; */
   {
     {
@@ -596,7 +597,71 @@ int main(void)
       __gmpz_clear(__gen_e_acsl_x_7);
     }
   }
+  {
+    int buf[10];
+    __e_acsl_store_block((void *)(buf),(size_t)40);
+    /*@ assert ∀ ℤ i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */
+    {
+      {
+        int __gen_e_acsl_forall_7;
+        __e_acsl_mpz_t __gen_e_acsl_i;
+        __gen_e_acsl_forall_7 = 1;
+        __gmpz_init(__gen_e_acsl_i);
+        {
+          __e_acsl_mpz_t __gen_e_acsl__40;
+          __gmpz_init_set_si(__gen_e_acsl__40,0L);
+          __gmpz_set(__gen_e_acsl_i,
+                     (__e_acsl_mpz_struct const *)(__gen_e_acsl__40));
+          __gmpz_clear(__gen_e_acsl__40);
+        }
+        while (1) {
+          {
+            __e_acsl_mpz_t __gen_e_acsl__41;
+            int __gen_e_acsl_lt_7;
+            __gmpz_init_set_si(__gen_e_acsl__41,10L);
+            __gen_e_acsl_lt_7 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i),
+                                           (__e_acsl_mpz_struct const *)(__gen_e_acsl__41));
+            if (__gen_e_acsl_lt_7 < 0) ; else break;
+            __gmpz_clear(__gen_e_acsl__41);
+          }
+          {
+            long __gen_e_acsl_i_2;
+            int __gen_e_acsl_valid;
+            __gen_e_acsl_i_2 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i));
+            __gen_e_acsl_valid = __e_acsl_valid((void *)(& buf[__gen_e_acsl_i_2]),
+                                                sizeof(int));
+            if (__gen_e_acsl_valid) ;
+            else {
+              __gen_e_acsl_forall_7 = 0;
+              goto e_acsl_end_loop9;
+            }
+          }
+          {
+            __e_acsl_mpz_t __gen_e_acsl__42;
+            __e_acsl_mpz_t __gen_e_acsl_add_15;
+            __gmpz_init_set_si(__gen_e_acsl__42,1L);
+            __gmpz_init(__gen_e_acsl_add_15);
+            __gmpz_add(__gen_e_acsl_add_15,
+                       (__e_acsl_mpz_struct const *)(__gen_e_acsl_i),
+                       (__e_acsl_mpz_struct const *)(__gen_e_acsl__42));
+            __gmpz_set(__gen_e_acsl_i,
+                       (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_15));
+            __gmpz_clear(__gen_e_acsl__42);
+            __gmpz_clear(__gen_e_acsl_add_15);
+          }
+        }
+        e_acsl_end_loop9: ;
+        __e_acsl_assert(__gen_e_acsl_forall_7,(char *)"Assertion",
+                        (char *)"main",
+                        (char *)"\\forall integer i; 0 <= i < 10 ==> \\valid(&buf[i])",
+                        30);
+        __gmpz_clear(__gen_e_acsl_i);
+        __e_acsl_delete_block((void *)(buf));
+      }
+    }
+  }
   __retres = 0;
+  __e_acsl_memory_clean();
   return __retres;
 }
 

src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle

@@ -14,6 +14,7 @@ FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns cl
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
 tests/gmp/quantif.i:9:[value] warning: assertion got status unknown.
 tests/gmp/quantif.i:9:[value] entering loop for the first time
 [value] using specification for function __e_acsl_assert
@@ -31,4 +32,10 @@ tests/gmp/quantif.i:21:[value] entering loop for the first time
 tests/gmp/quantif.i:25:[value] warning: assertion got status unknown.
 tests/gmp/quantif.i:25:[value] entering loop for the first time
 tests/gmp/quantif.i:26:[value] entering loop for the first time
+[value] using specification for function __e_acsl_store_block
+tests/gmp/quantif.i:30:[value] warning: assertion got status unknown.
+tests/gmp/quantif.i:30:[value] entering loop for the first time
+[value] using specification for function __e_acsl_valid
+[value] using specification for function __e_acsl_delete_block
+[value] using specification for function __e_acsl_memory_clean
 [value] done for function main

src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle

@@ -14,6 +14,7 @@ FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns cl
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
 tests/gmp/quantif.i:9:[value] warning: assertion got status unknown.
 [value] using specification for function __gmpz_init
 [value] using specification for function __gmpz_init_set_si
@@ -41,4 +42,11 @@ tests/gmp/quantif.i:25:[value] entering loop for the first time
 tests/gmp/quantif.i:26:[value] entering loop for the first time
 [value] using specification for function __gmpz_tdiv_q
 [value] using specification for function __gmpz_mul
+[value] using specification for function __e_acsl_store_block
+tests/gmp/quantif.i:30:[value] warning: assertion got status unknown.
+tests/gmp/quantif.i:30:[value] entering loop for the first time
+[value] using specification for function __gmpz_get_si
+[value] using specification for function __e_acsl_valid
+[value] using specification for function __e_acsl_delete_block
+[value] using specification for function __e_acsl_memory_clean
 [value] done for function main

src/plugins/e-acsl/tests/gmp/quantif.i

@@ -25,5 +25,10 @@ int main(void) {
   /*@ assert \forall int x; 0 <= x < 10
     ==> x % 2 == 0 ==> \exists integer y; 0 <= y <= x/2 && x == 2 * y; */
 
+  { // Gitlab issue #42
+    int buf[10];
+    /*@ assert \forall integer i; 0 <= i < 10 ==> \valid(buf+i); */
+  }
+
   return 0;
 }

src/plugins/e-acsl/typing.ml

@@ -178,7 +178,9 @@ let ty_of_interv ?ctx i =
           let ukind = Cil.intKindForValue u is_pos in
           (* kind corresponding to the interval *)
           if Cil.intTypeIncluded lkind ukind then ukind else lkind
-        | _, _ -> Kernel.fatal ~current:true "ival: %a" Ival.pretty i
+        | None, None -> raise Cil.Not_representable (* GMP *)
+        | None, Some _ | Some _, None ->
+          Kernel.fatal ~current:true "ival: %a" Ival.pretty i
     in
     (* convert the kind to [IInt] whenever smaller. *)
     let kind = if Cil.intTypeIncluded itv_kind IInt then IInt else itv_kind in
@@ -553,8 +555,8 @@ let rec type_predicate p =
             | _ -> assert false
           in
           let i2 = Interval.infer t2 in
-            (* add one to [i2], since we increment the loop counter one more
-               time before going outside the loop. *)
+          (* add one to [i2], since we increment the loop counter one more
+             time before going outside the loop. *)
           let i2 = match r2 with
             | Rlt -> i2
             | Rle -> Ival.add_singleton_int Integer.one i2
@@ -579,6 +581,13 @@ let rec type_predicate p =
              GMP variable when --e-acsl-gmp-only *)
           ignore (type_term ~use_gmp_opt:false ~ctx t1);
           ignore (type_term ~use_gmp_opt:false ~ctx t2);
+          (* if we must generate GMP code, degrade the interval in order to
+             guarantee that [x] will be a GMP when typing the goal *)
+          let i = match ctx with
+            | C_type _ -> i
+            | Gmp -> Ival.inject_range None None (* [ -\infty; +\infty ] *)
+            | Other -> assert false
+          in
           Interval.Env.add x i)
         guards;
       (type_predicate goal).ty
@@ -589,7 +598,7 @@ let rec type_predicate p =
     | Pvalid(_, t)
     | Pvalid_read(_, t)
     | Pvalid_function t ->
-      ignore (type_term ~use_gmp_opt:true ~ctx:Other t);
+      ignore (type_term ~use_gmp_opt:false ~ctx:Other t);
       c_int
 
     | Pforall _ -> Error.not_yet "unguarded \\forall quantification"

src/plugins/e-acsl/typing.mli

@@ -56,6 +56,8 @@ type integer_ty = private
   | C_type of ikind
   | Other (** Any non-integral type *)
 
+val pretty: Format.formatter -> integer_ty -> unit
+
 (** {3 Smart constructors} *)
 
 val gmp: integer_ty