From 8f9aad0053bec54dc2a425c0d0acf4103a8e50d9 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 27 Feb 2017 14:09:31 +0100
Subject: [PATCH] [typing] fix another typing issue with quantifiers
---
src/plugins/e-acsl/quantif.ml | 2 ++
src/plugins/e-acsl/tests/gmp/quantif.i | 1 +
src/plugins/e-acsl/typing.ml | 2 +-
3 files changed, 4 insertions(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index 3b9f31eb7b5..6ec351f314d 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/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;
diff --git a/src/plugins/e-acsl/tests/gmp/quantif.i b/src/plugins/e-acsl/tests/gmp/quantif.i
index c6e7b2d842e..e7870dc4f32 100644
--- a/src/plugins/e-acsl/tests/gmp/quantif.i
+++ b/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;
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 3ad11c0c70e..ca61314a6ae 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/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
--
GitLab