[typing] fix another typing issue with quantifiers

src/plugins/e-acsl/quantif.ml

@@ -243,6 +243,8 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
       in
       let guard = stmts_block guard_blk in
       (* increment the loop counter [x++] *)
+      (* TODO: should check that it does not overflow in the case of the type
+         of the loop variable is __declared__ too small. *)
       let tlv_one = t_plus_one tlv in
       (* previous typing ensures that [x++] fits type [ty] *)
       Typing.type_term ~use_gmp_opt:false ~ctx:ctx_one tlv_one;

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

@@ -28,6 +28,7 @@ int main(void) {
   { // Gitlab issue #42
     int buf[10];
     /*@ assert \forall integer i; 0 <= i < 10 ==> \valid(buf+i); */
+    /*@ assert \forall char i; 0 <= i < 10 ==> \valid(buf+i); */
   }
 
   return 0;

src/plugins/e-acsl/typing.ml

@@ -567,7 +567,7 @@ let rec type_predicate p =
             | Linteger -> mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:Gmp i)
             | Ctype ty ->
               (match Cil.unrollType ty with
-              | TInt(ik, _) -> C_type ik
+              | TInt(ik, _) -> mk_ctx ~use_gmp_opt:true (C_type ik)
               | ty ->
                 Options.fatal "unexpected type %a for quantified variable %a"
                   Printer.pp_typ ty