From b25866a735412442ed4dff0dd47b2dcc397ff22a Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 27 Feb 2017 13:56:11 +0100
Subject: [PATCH] [typing] fix issue with -e-acsl-gmp-only and quantifier
---
.../e-acsl/tests/gmp/oracle/gen_quantif.c | 35 ++++++++++
.../e-acsl/tests/gmp/oracle/gen_quantif2.c | 65 +++++++++++++++++++
.../tests/gmp/oracle/quantif.0.res.oracle | 7 ++
.../tests/gmp/oracle/quantif.1.res.oracle | 8 +++
src/plugins/e-acsl/tests/gmp/quantif.i | 5 ++
src/plugins/e-acsl/typing.ml | 17 +++--
src/plugins/e-acsl/typing.mli | 2 +
7 files changed, 135 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
index cd49f58f7fe..05fec071e8b 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
index 558fad0101c..6cd4639620c 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
index ee86d9b6561..4995ae47205 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
index 5621b649209..8fa4c96f4f3 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/gmp/quantif.i b/src/plugins/e-acsl/tests/gmp/quantif.i
index 81531e338c2..c6e7b2d842e 100644
--- a/src/plugins/e-acsl/tests/gmp/quantif.i
+++ b/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;
}
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 4c7a0424dc2..3ad11c0c70e 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/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"
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index 2cfeff48d33..1c79574742f 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/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
--
GitLab