Skip to content
Snippets Groups Projects
Commit 80bc9790 authored by Julien Signoles's avatar Julien Signoles
Browse files

Merge branch 'feature/fonenantsoa/empty-quantification' into 'master' 

Empty quantification

See merge request frama-c/e-acsl!267
parents 839128f2 d69deaaa
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 551 additions and 549 deletions
src/plugins/e-acsl/doc/Changelog
+ 5
− 2
View file @ 80bc9790
...@@ -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
+ 98
− 62
View file @ 80bc9790
...@@ -101,6 +101,34 @@ let compute_quantif_guards quantif bounded_vars hyps = ...@@ -101,6 +101,34 @@ 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 quantification 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
let lower_bound, _ = Ival.min_and_max i1 in
let _, upper_bound = Ival.min_and_max i2 in
match lower_bound, upper_bound with
| Some lower_bound, Some upper_bound ->
let res = match rel1, rel2 with
| Rle, Rle -> lower_bound > upper_bound
| Rle, Rlt | Rlt, Rle -> lower_bound >= upper_bound
| Rlt, Rlt -> lower_bound >= Z.sub upper_bound Z.one
| _ -> assert false
in
res (* case 1 *) || has_empty_quantif_with_false_negative guards
| None, _ | _, None ->
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,68 +145,76 @@ let convert kf env loc is_forall p bounded_vars hyps goal = ...@@ -117,68 +145,76 @@ 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
(* transform [guards] into [lscope_var list], match has_empty_quantif_with_false_negative guards, is_forall with
and update logic scope in the process *) | true, true ->
let lvs_guards, env = List.fold_right Cil.one ~loc, env
(fun (t1, rel1, lv, rel2, t2) (lvs_guards, env) -> | true, false ->
let lvs = Lscope.Lvs_quantif(t1, rel1, lv, rel2, t2) in Cil.zero ~loc, env
let env = Env.Logic_scope.extend env lvs in | false, _ ->
lvs :: lvs_guards, env) begin
guards (* transform [guards] into [lscope_var list],
([], env) and update logic scope in the process *)
in let lvs_guards, env = List.fold_right
let var_res, res, env = (fun (t1, rel1, lv, rel2, t2) (lvs_guards, env) ->
(* variable storing the result of the quantifier *) let lvs = Lscope.Lvs_quantif(t1, rel1, lv, rel2, t2) in
let name = if is_forall then "forall" else "exists" in let env = Env.Logic_scope.extend env lvs in
Env.new_var lvs :: lvs_guards, env)
~loc guards
~name ([], env)
env in
None let var_res, res, env =
intType (* variable storing the result of the quantifier *)
(fun v _ -> let name = if is_forall then "forall" else "exists" in
let lv = var v in Env.new_var
[ mkStmtOneInstr ~valid_sid:true (Set(lv, init_val, loc)) ]) ~loc
in ~name
let end_loop_ref = ref dummyStmt in env
(* innermost block *) None
let mk_innermost_block env = intType
(* innermost loop body: store the result in [res] and go out according (fun v _ ->
to evaluation of the goal *) let lv = var v in
let named_predicate_to_exp = !predicate_to_exp_ref in [ mkStmtOneInstr ~valid_sid:true (Set(lv, init_val, loc)) ])
let test, env = named_predicate_to_exp kf (Env.push env) goal in in
let then_block = mkBlock [ mkEmptyStmt ~loc () ] in let end_loop_ref = ref dummyStmt in
let else_block = (* innermost block *)
(* use a 'goto', not a simple 'break' in order to handle 'forall' with let mk_innermost_block env =
multiple binders (leading to imbricated loops) *) (* innermost loop body: store the result in [res] and go out according
mkBlock to evaluation of the goal *)
[ mkStmtOneInstr ~valid_sid:true (Set(var var_res, found_val, loc)); let named_predicate_to_exp = !predicate_to_exp_ref in
mkStmt ~valid_sid:true (Goto(end_loop_ref, loc)) ] let test, env = named_predicate_to_exp kf (Env.push env) goal in
in let then_block = mkBlock [ mkEmptyStmt ~loc () ] in
let blk, env = Env.pop_and_get let else_block =
env (* use a 'goto', not a simple 'break' in order to handle 'forall' with
(mkStmt ~valid_sid:true multiple binders (leading to imbricated loops) *)
(If(mk_guard test, then_block, else_block, loc))) mkBlock
~global_clear:false [ mkStmtOneInstr ~valid_sid:true (Set(var var_res, found_val, loc));
Env.After mkStmt ~valid_sid:true (Goto(end_loop_ref, loc)) ]
in in
let blk = Cil.flatten_transient_sub_blocks blk in let blk, env = Env.pop_and_get
[ mkStmt ~valid_sid:true (Block blk) ], env env
in (mkStmt ~valid_sid:true
let stmts, env = (If(mk_guard test, then_block, else_block, loc)))
Loops.mk_nested_loops ~loc mk_innermost_block kf env lvs_guards ~global_clear:false
in Env.After
let env = in
Env.add_stmt env (mkStmt ~valid_sid:true (Block (mkBlock stmts))) let blk = Cil.flatten_transient_sub_blocks blk in
in [ mkStmt ~valid_sid:true (Block blk) ], env
(* where to jump to go out of the loop *) in
let end_loop = mkEmptyStmt ~loc () in let stmts, env =
let label_name = "e_acsl_end_loop" ^ string_of_int (Label_ids.next ()) in Loops.mk_nested_loops ~loc mk_innermost_block kf env lvs_guards
let label = Label(label_name, loc, false) in in
end_loop.labels <- label :: end_loop.labels; let env =
end_loop_ref := end_loop; Env.add_stmt env (mkStmt ~valid_sid:true (Block (mkBlock stmts)))
let env = Env.add_stmt env end_loop in in
res, env (* where to jump to go out of the loop *)
let end_loop = mkEmptyStmt ~loc () in
let label_name = "e_acsl_end_loop" ^ string_of_int (Label_ids.next ()) in
let label = Label(label_name, loc, false) in
end_loop.labels <- label :: end_loop.labels;
end_loop_ref := end_loop;
let env = Env.add_stmt env end_loop in
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 @ 80bc9790
...@@ -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 @ 80bc9790
This diff is collapsed.
src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
+ 17
− 16
View file @ 80bc9790
...@@ -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 @ 80bc9790
...@@ -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 @ 80bc9790
...@@ -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