Skip to content
Snippets Groups Projects
Commit 54670357 authored by Fonenantsoa Maurica's avatar Fonenantsoa Maurica Committed by Fonenantsoa Maurica
Browse files

Empty quantif

parent 839128f2
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 494 additions and 487 deletions
src/plugins/e-acsl/doc/Changelog
+ 5
− 2
View file @ 54670357
...@@ -19,13 +19,16 @@ ...@@ -19,13 +19,16 @@
# configure configure # configure configure
############################################################################### ###############################################################################
- E-ACSL [2018/11/15] Predicates with empty quantifications
directly generate \true or \false instead of nested loops.
########################## ##########################
Plugin E-ACSL 18.0 (Argon) Plugin E-ACSL 18.0 (Argon)
########################## ##########################
-* E-ACSL [2018/11/13] Fix typing bug in quantifications when the -* E-ACSL [2018/11/13] Fix typing bug in quantifications when the
guards of the quantifier variable cannot be represented into guards of the quantifier variable cannot be represented into
its type. its type.
-* runtime [2018/11/13] Fix bug #!2405 about memory initialization -* runtime [2018/11/13] Fix bug #!2405 about memory initialization
in presence of GCC constructors. in presence of GCC constructors.
-* E-ACSL [2018/10/23] Fix bug #2406 about monitoring of variables -* E-ACSL [2018/10/23] Fix bug #2406 about monitoring of variables
......
src/plugins/e-acsl/quantif.ml
+ 41
− 0
View file @ 54670357
...@@ -101,6 +101,36 @@ let compute_quantif_guards quantif bounded_vars hyps = ...@@ -101,6 +101,36 @@ let compute_quantif_guards quantif bounded_vars hyps =
Error.untypable msg); Error.untypable msg);
List.rev acc List.rev acc
(* It could happen that the bounds provided for a quantified [lv] are empty
in the sense that [min <= lv <= max] but [min > max]. In such cases, \true
(or \false depending on the quantification) should be generated instead of
nested loops.
[has_empty_quantif_with_false_negative] partially detects such cases:
Case 1: an empty qunatification was detected for sure, return true.
Case 2: we don't know, return false. *)
let rec has_empty_quantif_with_false_negative = function
| [] ->
(* case 2 *)
false
| (t1, rel1, _, rel2, t2) :: guards ->
let i1 = Interval.infer t1 in
let i2 = Interval.infer t2 in
if Ival.is_singleton_int i1 && Ival.is_singleton_int i2 then
(* we know the precise values of the bounds *)
let lower_bound, _ = Misc.finite_min_and_max i1 in
let upper_bound, _ = Misc.finite_min_and_max i2 in
let res = match rel1, rel2 with
| Rle, Rle -> lower_bound > upper_bound
| Rle, Rlt -> lower_bound >= upper_bound
| Rlt, Rle -> lower_bound >= upper_bound
| Rlt, Rlt -> lower_bound >= Z.sub upper_bound Z.one
| _ -> assert false
in
if res then (* case 1 *) res
else has_empty_quantif_with_false_negative guards
else
has_empty_quantif_with_false_negative guards
let () = Typing.compute_quantif_guards_ref := compute_quantif_guards let () = Typing.compute_quantif_guards_ref := compute_quantif_guards
module Label_ids = module Label_ids =
...@@ -117,6 +147,16 @@ let convert kf env loc is_forall p bounded_vars hyps goal = ...@@ -117,6 +147,16 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
in in
(* universal quantification over integers (or a subtype of integer) *) (* universal quantification over integers (or a subtype of integer) *)
let guards = compute_quantif_guards p bounded_vars hyps in let guards = compute_quantif_guards p bounded_vars hyps in
let has_empty_quantif_with_false_negative =
has_empty_quantif_with_false_negative guards
in
match has_empty_quantif_with_false_negative, is_forall with
| true, true ->
Cil.one ~loc, env
| true, false ->
Cil.zero ~loc, env
| false, _ ->
begin
(* transform [guards] into [lscope_var list], (* transform [guards] into [lscope_var list],
and update logic scope in the process *) and update logic scope in the process *)
let lvs_guards, env = List.fold_right let lvs_guards, env = List.fold_right
...@@ -179,6 +219,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal = ...@@ -179,6 +219,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
end_loop_ref := end_loop; end_loop_ref := end_loop;
let env = Env.add_stmt env end_loop in let env = Env.add_stmt env end_loop in
res, env res, env
end
let quantif_to_exp kf env p = let quantif_to_exp kf env p =
let loc = p.pred_loc in let loc = p.pred_loc in
......
src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
+ 84
− 87
View file @ 54670357
...@@ -49,15 +49,15 @@ int main(void) ...@@ -49,15 +49,15 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_forall_2,(char *)"Assertion",(char *)"main", __e_acsl_assert(__gen_e_acsl_forall_2,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x; 0 < x <= 1 ==> x == 1",10); (char *)"\\forall integer x; 0 < x <= 1 ==> x == 1",10);
} }
/*@ assert ∀ ℤ x; 0 < x < 1 ⇒ \false; */ /*@ assert ∀ ℤ x; 0 ≤ x < 1 ⇒ x ≡ 0; */
{ {
int __gen_e_acsl_forall_3; int __gen_e_acsl_forall_3;
int __gen_e_acsl_x_3; int __gen_e_acsl_x_3;
__gen_e_acsl_forall_3 = 1; __gen_e_acsl_forall_3 = 1;
__gen_e_acsl_x_3 = 0 + 1; __gen_e_acsl_x_3 = 0;
while (1) { while (1) {
if (__gen_e_acsl_x_3 < 1) ; else break; if (__gen_e_acsl_x_3 < 1) ; else break;
if (0) ; if (__gen_e_acsl_x_3 == 0) ;
else { else {
__gen_e_acsl_forall_3 = 0; __gen_e_acsl_forall_3 = 0;
goto e_acsl_end_loop3; goto e_acsl_end_loop3;
...@@ -66,81 +66,62 @@ int main(void) ...@@ -66,81 +66,62 @@ int main(void)
} }
e_acsl_end_loop3: ; e_acsl_end_loop3: ;
__e_acsl_assert(__gen_e_acsl_forall_3,(char *)"Assertion",(char *)"main", __e_acsl_assert(__gen_e_acsl_forall_3,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x; 0 < x < 1 ==> \\false",11); (char *)"\\forall integer x; 0 <= x < 1 ==> x == 0",11);
}
/*@ assert ∀ ℤ x; 0 ≤ x < 1 ⇒ x ≡ 0; */
{
int __gen_e_acsl_forall_4;
int __gen_e_acsl_x_4;
__gen_e_acsl_forall_4 = 1;
__gen_e_acsl_x_4 = 0;
while (1) {
if (__gen_e_acsl_x_4 < 1) ; else break;
if (__gen_e_acsl_x_4 == 0) ;
else {
__gen_e_acsl_forall_4 = 0;
goto e_acsl_end_loop4;
}
__gen_e_acsl_x_4 ++;
}
e_acsl_end_loop4: ;
__e_acsl_assert(__gen_e_acsl_forall_4,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x; 0 <= x < 1 ==> x == 0",12);
} }
/*@ assert /*@ assert
∀ ℤ x, ℤ y, ℤ z; ∀ ℤ x, ℤ y, ℤ z;
0 ≤ x < 2 ∧ 0 ≤ y < 5 ∧ 0 ≤ z ≤ y ⇒ x + z ≤ y + 1; 0 ≤ x < 2 ∧ 0 ≤ y < 5 ∧ 0 ≤ z ≤ y ⇒ x + z ≤ y + 1;
*/ */
{ {
int __gen_e_acsl_forall_5; int __gen_e_acsl_forall_4;
int __gen_e_acsl_x_5; int __gen_e_acsl_x_4;
int __gen_e_acsl_y; int __gen_e_acsl_y;
int __gen_e_acsl_z; int __gen_e_acsl_z;
__gen_e_acsl_forall_5 = 1; __gen_e_acsl_forall_4 = 1;
__gen_e_acsl_x_5 = 0; __gen_e_acsl_x_4 = 0;
while (1) { while (1) {
if (__gen_e_acsl_x_5 < 2) ; else break; if (__gen_e_acsl_x_4 < 2) ; else break;
__gen_e_acsl_y = 0; __gen_e_acsl_y = 0;
while (1) { while (1) {
if (__gen_e_acsl_y < 5) ; else break; if (__gen_e_acsl_y < 5) ; else break;
__gen_e_acsl_z = 0; __gen_e_acsl_z = 0;
while (1) { while (1) {
if (__gen_e_acsl_z <= __gen_e_acsl_y) ; else break; if (__gen_e_acsl_z <= __gen_e_acsl_y) ; else break;
if (__gen_e_acsl_x_5 + __gen_e_acsl_z <= __gen_e_acsl_y + 1) if (__gen_e_acsl_x_4 + __gen_e_acsl_z <= __gen_e_acsl_y + 1)
; ;
else { else {
__gen_e_acsl_forall_5 = 0; __gen_e_acsl_forall_4 = 0;
goto e_acsl_end_loop5; goto e_acsl_end_loop4;
} }
__gen_e_acsl_z ++; __gen_e_acsl_z ++;
} }
__gen_e_acsl_y ++; __gen_e_acsl_y ++;
} }
__gen_e_acsl_x_5 ++; __gen_e_acsl_x_4 ++;
} }
e_acsl_end_loop5: ; e_acsl_end_loop4: ;
__e_acsl_assert(__gen_e_acsl_forall_5,(char *)"Assertion",(char *)"main", __e_acsl_assert(__gen_e_acsl_forall_4,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x, integer y, integer z;\n 0 <= x < 2 && 0 <= y < 5 && 0 <= z <= y ==> x + z <= y + 1", (char *)"\\forall integer x, integer y, integer z;\n 0 <= x < 2 && 0 <= y < 5 && 0 <= z <= y ==> x + z <= y + 1",
16); 15);
} }
/*@ assert ∃ int x; 0 ≤ x < 10 ∧ x ≡ 5; */ /*@ assert ∃ int x; 0 ≤ x < 10 ∧ x ≡ 5; */
{ {
int __gen_e_acsl_exists; int __gen_e_acsl_exists;
int __gen_e_acsl_x_6; int __gen_e_acsl_x_5;
__gen_e_acsl_exists = 0; __gen_e_acsl_exists = 0;
__gen_e_acsl_x_6 = 0; __gen_e_acsl_x_5 = 0;
while (1) { while (1) {
if (__gen_e_acsl_x_6 < 10) ; else break; if (__gen_e_acsl_x_5 < 10) ; else break;
if (! (__gen_e_acsl_x_6 == 5)) ; if (! (__gen_e_acsl_x_5 == 5)) ;
else { else {
__gen_e_acsl_exists = 1; __gen_e_acsl_exists = 1;
goto e_acsl_end_loop6; goto e_acsl_end_loop5;
} }
__gen_e_acsl_x_6 ++; __gen_e_acsl_x_5 ++;
} }
e_acsl_end_loop6: ; e_acsl_end_loop5: ;
__e_acsl_assert(__gen_e_acsl_exists,(char *)"Assertion",(char *)"main", __e_acsl_assert(__gen_e_acsl_exists,(char *)"Assertion",(char *)"main",
(char *)"\\exists int x; 0 <= x < 10 && x == 5",21); (char *)"\\exists int x; 0 <= x < 10 && x == 5",20);
} }
/*@ assert /*@ assert
∀ int x; ∀ int x;
...@@ -148,44 +129,44 @@ int main(void) ...@@ -148,44 +129,44 @@ int main(void)
x % 2 ≡ 0 ⇒ (∃ ℤ y; 0 ≤ y ≤ x / 2 ∧ x ≡ 2 * y); x % 2 ≡ 0 ⇒ (∃ ℤ y; 0 ≤ y ≤ x / 2 ∧ x ≡ 2 * y);
*/ */
{ {
int __gen_e_acsl_forall_6; int __gen_e_acsl_forall_5;
int __gen_e_acsl_x_7; int __gen_e_acsl_x_6;
__gen_e_acsl_forall_6 = 1; __gen_e_acsl_forall_5 = 1;
__gen_e_acsl_x_7 = 0; __gen_e_acsl_x_6 = 0;
while (1) { while (1) {
if (__gen_e_acsl_x_7 < 10) ; else break; if (__gen_e_acsl_x_6 < 10) ; else break;
{ {
int __gen_e_acsl_implies; int __gen_e_acsl_implies;
if (! (__gen_e_acsl_x_7 % 2 == 0)) __gen_e_acsl_implies = 1; if (! (__gen_e_acsl_x_6 % 2 == 0)) __gen_e_acsl_implies = 1;
else { else {
int __gen_e_acsl_exists_2; int __gen_e_acsl_exists_2;
int __gen_e_acsl_y_2; int __gen_e_acsl_y_2;
__gen_e_acsl_exists_2 = 0; __gen_e_acsl_exists_2 = 0;
__gen_e_acsl_y_2 = 0; __gen_e_acsl_y_2 = 0;
while (1) { while (1) {
if (__gen_e_acsl_y_2 <= __gen_e_acsl_x_7 / 2) ; else break; if (__gen_e_acsl_y_2 <= __gen_e_acsl_x_6 / 2) ; else break;
if (! (__gen_e_acsl_x_7 == 2 * __gen_e_acsl_y_2)) ; if (! (__gen_e_acsl_x_6 == 2 * __gen_e_acsl_y_2)) ;
else { else {
__gen_e_acsl_exists_2 = 1; __gen_e_acsl_exists_2 = 1;
goto e_acsl_end_loop7; goto e_acsl_end_loop6;
} }
__gen_e_acsl_y_2 ++; __gen_e_acsl_y_2 ++;
} }
e_acsl_end_loop7: ; e_acsl_end_loop6: ;
__gen_e_acsl_implies = __gen_e_acsl_exists_2; __gen_e_acsl_implies = __gen_e_acsl_exists_2;
} }
if (__gen_e_acsl_implies) ; if (__gen_e_acsl_implies) ;
else { else {
__gen_e_acsl_forall_6 = 0; __gen_e_acsl_forall_5 = 0;
goto e_acsl_end_loop8; goto e_acsl_end_loop7;
} }
} }
__gen_e_acsl_x_7 ++; __gen_e_acsl_x_6 ++;
} }
e_acsl_end_loop8: ; e_acsl_end_loop7: ;
__e_acsl_assert(__gen_e_acsl_forall_6,(char *)"Assertion",(char *)"main", __e_acsl_assert(__gen_e_acsl_forall_5,(char *)"Assertion",(char *)"main",
(char *)"\\forall int x;\n 0 <= x < 10 ==>\n x % 2 == 0 ==> (\\exists integer y; 0 <= y <= x / 2 && x == 2 * y)", (char *)"\\forall int x;\n 0 <= x < 10 ==>\n x % 2 == 0 ==> (\\exists integer y; 0 <= y <= x / 2 && x == 2 * y)",
25); 24);
} }
{ {
int buf[10]; int buf[10];
...@@ -193,9 +174,9 @@ int main(void) ...@@ -193,9 +174,9 @@ int main(void)
unsigned long len = (unsigned long)9; unsigned long len = (unsigned long)9;
/*@ assert ∀ ℤ i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */ /*@ assert ∀ ℤ i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */
{ {
int __gen_e_acsl_forall_7; int __gen_e_acsl_forall_6;
int __gen_e_acsl_i; int __gen_e_acsl_i;
__gen_e_acsl_forall_7 = 1; __gen_e_acsl_forall_6 = 1;
__gen_e_acsl_i = 0; __gen_e_acsl_i = 0;
while (1) { while (1) {
if (__gen_e_acsl_i < 10) ; else break; if (__gen_e_acsl_i < 10) ; else break;
...@@ -207,23 +188,23 @@ int main(void) ...@@ -207,23 +188,23 @@ int main(void)
(void *)0); (void *)0);
if (__gen_e_acsl_valid) ; if (__gen_e_acsl_valid) ;
else { else {
__gen_e_acsl_forall_7 = 0; __gen_e_acsl_forall_6 = 0;
goto e_acsl_end_loop9; goto e_acsl_end_loop8;
} }
} }
__gen_e_acsl_i ++; __gen_e_acsl_i ++;
} }
e_acsl_end_loop9: ; e_acsl_end_loop8: ;
__e_acsl_assert(__gen_e_acsl_forall_7,(char *)"Assertion", __e_acsl_assert(__gen_e_acsl_forall_6,(char *)"Assertion",
(char *)"main", (char *)"main",
(char *)"\\forall integer i; 0 <= i < 10 ==> \\valid(&buf[i])", (char *)"\\forall integer i; 0 <= i < 10 ==> \\valid(&buf[i])",
31); 30);
} }
/*@ assert ∀ char i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */ /*@ assert ∀ char i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */
{ {
int __gen_e_acsl_forall_8; int __gen_e_acsl_forall_7;
int __gen_e_acsl_i_2; int __gen_e_acsl_i_2;
__gen_e_acsl_forall_8 = 1; __gen_e_acsl_forall_7 = 1;
__gen_e_acsl_i_2 = (char)0; __gen_e_acsl_i_2 = (char)0;
while (1) { while (1) {
if (__gen_e_acsl_i_2 < 10) ; else break; if (__gen_e_acsl_i_2 < 10) ; else break;
...@@ -235,23 +216,23 @@ int main(void) ...@@ -235,23 +216,23 @@ int main(void)
(void *)0); (void *)0);
if (__gen_e_acsl_valid_2) ; if (__gen_e_acsl_valid_2) ;
else { else {
__gen_e_acsl_forall_8 = 0; __gen_e_acsl_forall_7 = 0;
goto e_acsl_end_loop10; goto e_acsl_end_loop9;
} }
} }
__gen_e_acsl_i_2 ++; __gen_e_acsl_i_2 ++;
} }
e_acsl_end_loop10: ; e_acsl_end_loop9: ;
__e_acsl_assert(__gen_e_acsl_forall_8,(char *)"Assertion", __e_acsl_assert(__gen_e_acsl_forall_7,(char *)"Assertion",
(char *)"main", (char *)"main",
(char *)"\\forall char i; 0 <= i < 10 ==> \\valid(&buf[i])", (char *)"\\forall char i; 0 <= i < 10 ==> \\valid(&buf[i])",
32); 31);
} }
/*@ assert ∀ ℤ i; 0 ≤ i < len ⇒ \valid(&buf[i]); */ /*@ assert ∀ ℤ i; 0 ≤ i < len ⇒ \valid(&buf[i]); */
{ {
int __gen_e_acsl_forall_9; int __gen_e_acsl_forall_8;
unsigned long __gen_e_acsl_i_3; unsigned long __gen_e_acsl_i_3;
__gen_e_acsl_forall_9 = 1; __gen_e_acsl_forall_8 = 1;
__gen_e_acsl_i_3 = 0UL; __gen_e_acsl_i_3 = 0UL;
while (1) { while (1) {
if (__gen_e_acsl_i_3 < len) ; else break; if (__gen_e_acsl_i_3 < len) ; else break;
...@@ -263,23 +244,23 @@ int main(void) ...@@ -263,23 +244,23 @@ int main(void)
(void *)0); (void *)0);
if (__gen_e_acsl_valid_3) ; if (__gen_e_acsl_valid_3) ;
else { else {
__gen_e_acsl_forall_9 = 0; __gen_e_acsl_forall_8 = 0;
goto e_acsl_end_loop11; goto e_acsl_end_loop10;
} }
} }
__gen_e_acsl_i_3 ++; __gen_e_acsl_i_3 ++;
} }
e_acsl_end_loop11: ; e_acsl_end_loop10: ;
__e_acsl_assert(__gen_e_acsl_forall_9,(char *)"Assertion", __e_acsl_assert(__gen_e_acsl_forall_8,(char *)"Assertion",
(char *)"main", (char *)"main",
(char *)"\\forall integer i; 0 <= i < len ==> \\valid(&buf[i])", (char *)"\\forall integer i; 0 <= i < len ==> \\valid(&buf[i])",
33); 32);
} }
/*@ assert ∀ ℤ i; 0 ≤ i ≤ len ⇒ \valid(&buf[i]); */ /*@ assert ∀ ℤ i; 0 ≤ i ≤ len ⇒ \valid(&buf[i]); */
{ {
int __gen_e_acsl_forall_10; int __gen_e_acsl_forall_9;
__e_acsl_mpz_t __gen_e_acsl_i_4; __e_acsl_mpz_t __gen_e_acsl_i_4;
__gen_e_acsl_forall_10 = 1; __gen_e_acsl_forall_9 = 1;
__gmpz_init(__gen_e_acsl_i_4); __gmpz_init(__gen_e_acsl_i_4);
{ {
__e_acsl_mpz_t __gen_e_acsl_; __e_acsl_mpz_t __gen_e_acsl_;
...@@ -308,8 +289,8 @@ int main(void) ...@@ -308,8 +289,8 @@ int main(void)
(void *)0); (void *)0);
if (__gen_e_acsl_valid_4) ; if (__gen_e_acsl_valid_4) ;
else { else {
__gen_e_acsl_forall_10 = 0; __gen_e_acsl_forall_9 = 0;
goto e_acsl_end_loop12; goto e_acsl_end_loop11;
} }
} }
{ {
...@@ -326,15 +307,31 @@ int main(void) ...@@ -326,15 +307,31 @@ int main(void)
__gmpz_clear(__gen_e_acsl_add); __gmpz_clear(__gen_e_acsl_add);
} }
} }
e_acsl_end_loop12: ; e_acsl_end_loop11: ;
__e_acsl_assert(__gen_e_acsl_forall_10,(char *)"Assertion", __e_acsl_assert(__gen_e_acsl_forall_9,(char *)"Assertion",
(char *)"main", (char *)"main",
(char *)"\\forall integer i; 0 <= i <= len ==> \\valid(&buf[i])", (char *)"\\forall integer i; 0 <= i <= len ==> \\valid(&buf[i])",
34); 33);
__gmpz_clear(__gen_e_acsl_i_4); __gmpz_clear(__gen_e_acsl_i_4);
__e_acsl_delete_block((void *)(buf)); __e_acsl_delete_block((void *)(buf));
} }
} }
/*@ assert ∀ ℤ x; 0 < x < 1 ⇒ \false; */
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"\\forall integer x; 0 < x < 1 ==> \\false",37);
/*@ assert ¬(∃ char c; 10 ≤ c < 10 ∧ c ≡ 10); */
__e_acsl_assert(! 0,(char *)"Assertion",(char *)"main",
(char *)"!(\\exists char c; 10 <= c < 10 && c == 10)",38);
/*@ assert \let u = 5;
∀ ℤ x, ℤ y; 0 ≤ x < 2 ∧ 4 < y < u ⇒ \false;
*/
{
int __gen_e_acsl_u;
__gen_e_acsl_u = 5;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"\\let u = 5;\n\\forall integer x, integer y; 0 <= x < 2 && 4 < y < u ==> \\false",
40);
}
__retres = 0; __retres = 0;
__e_acsl_memory_clean(); __e_acsl_memory_clean();
return __retres; return __retres;
......
src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
+ 325
− 365
View file @ 54670357
This diff is collapsed.
src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
+ 17
− 16
View file @ 54670357
...@@ -16,33 +16,32 @@ ...@@ -16,33 +16,32 @@
[eva:alarm] tests/gmp/quantif.i:10: Warning: assertion got status unknown. [eva:alarm] tests/gmp/quantif.i:10: Warning: assertion got status unknown.
[eva] tests/gmp/quantif.i:10: starting to merge loop iterations [eva] tests/gmp/quantif.i:10: starting to merge loop iterations
[eva:alarm] tests/gmp/quantif.i:11: Warning: assertion got status unknown. [eva:alarm] tests/gmp/quantif.i:11: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/quantif.i:12: Warning: assertion got status unknown. [eva] tests/gmp/quantif.i:11: starting to merge loop iterations
[eva] tests/gmp/quantif.i:12: starting to merge loop iterations [eva:alarm] tests/gmp/quantif.i:15: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/quantif.i:16: Warning: assertion got status unknown. [eva] tests/gmp/quantif.i:15: starting to merge loop iterations
[eva] tests/gmp/quantif.i:16: starting to merge loop iterations [eva:alarm] tests/gmp/quantif.i:15: Warning:
[eva:alarm] tests/gmp/quantif.i:16: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/quantif.i:21: Warning: assertion got status unknown. [eva:alarm] tests/gmp/quantif.i:20: Warning: assertion got status unknown.
[eva] tests/gmp/quantif.i:21: starting to merge loop iterations [eva] tests/gmp/quantif.i:20: starting to merge loop iterations
[eva:alarm] tests/gmp/quantif.i:25: Warning: assertion got status unknown. [eva:alarm] tests/gmp/quantif.i:24: Warning: assertion got status unknown.
[eva] tests/gmp/quantif.i:24: starting to merge loop iterations
[eva] tests/gmp/quantif.i:25: starting to merge loop iterations [eva] tests/gmp/quantif.i:25: starting to merge loop iterations
[eva] tests/gmp/quantif.i:26: starting to merge loop iterations [eva:alarm] tests/gmp/quantif.i:24: Warning:
[eva:alarm] tests/gmp/quantif.i:25: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __e_acsl_store_block [eva] using specification for function __e_acsl_store_block
[eva:alarm] tests/gmp/quantif.i:31: Warning: assertion got status unknown. [eva:alarm] tests/gmp/quantif.i:30: Warning: assertion got status unknown.
[eva] using specification for function __e_acsl_valid [eva] using specification for function __e_acsl_valid
[eva] tests/gmp/quantif.i:30: starting to merge loop iterations
[eva:alarm] tests/gmp/quantif.i:30: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] tests/gmp/quantif.i:31: starting to merge loop iterations [eva] tests/gmp/quantif.i:31: starting to merge loop iterations
[eva:alarm] tests/gmp/quantif.i:31: Warning: [eva:alarm] tests/gmp/quantif.i:31: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/quantif.i:32: Warning: assertion got status unknown.
[eva] tests/gmp/quantif.i:32: starting to merge loop iterations [eva] tests/gmp/quantif.i:32: starting to merge loop iterations
[eva:alarm] tests/gmp/quantif.i:32: Warning: [eva:alarm] tests/gmp/quantif.i:32: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/quantif.i:33: Warning: assertion got status unknown. [eva:alarm] tests/gmp/quantif.i:33: Warning: assertion got status unknown.
[eva] tests/gmp/quantif.i:33: starting to merge loop iterations
[eva:alarm] tests/gmp/quantif.i:33: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/quantif.i:34: Warning: assertion got status unknown.
[eva] using specification for function __gmpz_init [eva] using specification for function __gmpz_init
[eva] using specification for function __gmpz_init_set_si [eva] using specification for function __gmpz_init_set_si
[eva] using specification for function __gmpz_set [eva] using specification for function __gmpz_set
...@@ -51,8 +50,10 @@ ...@@ -51,8 +50,10 @@
[eva] using specification for function __gmpz_cmp [eva] using specification for function __gmpz_cmp
[eva] using specification for function __gmpz_get_si [eva] using specification for function __gmpz_get_si
[eva] using specification for function __gmpz_add [eva] using specification for function __gmpz_add
[eva:alarm] tests/gmp/quantif.i:34: Warning: [eva:alarm] tests/gmp/quantif.i:33: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __e_acsl_delete_block [eva] using specification for function __e_acsl_delete_block
[eva:alarm] tests/gmp/quantif.i:37: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/quantif.i:40: Warning: assertion got status unknown.
[eva] using specification for function __e_acsl_memory_clean [eva] using specification for function __e_acsl_memory_clean
[eva] done for function main [eva] done for function main
src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
+ 15
− 16
View file @ 54670357
...@@ -27,40 +27,39 @@ ...@@ -27,40 +27,39 @@
[eva:alarm] tests/gmp/quantif.i:11: Warning: assertion got status unknown. [eva:alarm] tests/gmp/quantif.i:11: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/quantif.i:11: Warning: [eva:alarm] tests/gmp/quantif.i:11: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/quantif.i:12: Warning: assertion got status unknown. [eva:alarm] tests/gmp/quantif.i:15: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/quantif.i:12: Warning: [eva:alarm] tests/gmp/quantif.i:15: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/quantif.i:16: Warning: assertion got status unknown. [eva:alarm] tests/gmp/quantif.i:20: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/quantif.i:16: Warning: [eva:alarm] tests/gmp/quantif.i:20: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/quantif.i:21: Warning: assertion got status unknown. [eva:alarm] tests/gmp/quantif.i:24: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/quantif.i:21: Warning: [eva:alarm] tests/gmp/quantif.i:25: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/quantif.i:25: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/quantif.i:26: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpz_tdiv_r [eva] using specification for function __gmpz_tdiv_r
[eva:alarm] tests/gmp/quantif.i:26: Warning: [eva:alarm] tests/gmp/quantif.i:25: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpz_tdiv_q [eva] using specification for function __gmpz_tdiv_q
[eva] using specification for function __gmpz_mul [eva] using specification for function __gmpz_mul
[eva:alarm] tests/gmp/quantif.i:25: Warning: [eva:alarm] tests/gmp/quantif.i:24: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __e_acsl_store_block [eva] using specification for function __e_acsl_store_block
[eva:alarm] tests/gmp/quantif.i:31: Warning: assertion got status unknown. [eva:alarm] tests/gmp/quantif.i:30: Warning: assertion got status unknown.
[eva] using specification for function __gmpz_get_si [eva] using specification for function __gmpz_get_si
[eva] using specification for function __e_acsl_valid [eva] using specification for function __e_acsl_valid
[eva:alarm] tests/gmp/quantif.i:30: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/quantif.i:31: Warning: [eva:alarm] tests/gmp/quantif.i:31: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/quantif.i:32: Warning: assertion got status unknown.
[eva] using specification for function __gmpz_init_set_ui
[eva:alarm] tests/gmp/quantif.i:32: Warning: [eva:alarm] tests/gmp/quantif.i:32: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/quantif.i:33: Warning: assertion got status unknown. [eva:alarm] tests/gmp/quantif.i:33: Warning: assertion got status unknown.
[eva] using specification for function __gmpz_init_set_ui
[eva:alarm] tests/gmp/quantif.i:33: Warning: [eva:alarm] tests/gmp/quantif.i:33: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/quantif.i:34: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/quantif.i:34: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __e_acsl_delete_block [eva] using specification for function __e_acsl_delete_block
[eva:alarm] tests/gmp/quantif.i:37: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/quantif.i:40: Warning: assertion got status unknown.
[eva] using specification for function __e_acsl_memory_clean [eva] using specification for function __e_acsl_memory_clean
[eva] done for function main [eva] done for function main
src/plugins/e-acsl/tests/gmp/quantif.i
+ 7
− 1
View file @ 54670357
...@@ -8,7 +8,6 @@ int main(void) { ...@@ -8,7 +8,6 @@ int main(void) {
/*@ assert \forall integer x; 0 <= x <= 1 ==> x == 0 || x == 1; */ /*@ assert \forall integer x; 0 <= x <= 1 ==> x == 0 || x == 1; */
/*@ assert \forall integer x; 0 < x <= 1 ==> x == 1; */ /*@ assert \forall integer x; 0 < x <= 1 ==> x == 1; */
/*@ assert \forall integer x; 0 < x < 1 ==> \false; */
/*@ assert \forall integer x; 0 <= x < 1 ==> x == 0; */ /*@ assert \forall integer x; 0 <= x < 1 ==> x == 0; */
/* // multiple universal quantifications */ /* // multiple universal quantifications */
...@@ -34,5 +33,12 @@ int main(void) { ...@@ -34,5 +33,12 @@ int main(void) {
/*@ assert \forall integer i; 0 <= i <= len ==> \valid(buf+i); */ /*@ assert \forall integer i; 0 <= i <= len ==> \valid(buf+i); */
} }
// Empty quantifications
/*@ assert \forall integer x; 0 < x < 1 ==> \false; */
/*@ assert ! \exists char c; 10 <= c < 10 && c == 10; */ ;
/*@ assert
\let u = 5;
\forall integer x,y; 0 <= x < 2 && 4 < y < u ==> \false; */ ;
return 0; return 0;
} }
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment