From 7d0e9489b3e16c1999296940df13be84b5434d28 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Virgile=20Pr=C3=A9vosto?= <virgile.prevosto@cea.fr>
Date: Wed, 25 May 2011 16:02:21 +0000
Subject: [PATCH] [e-acsl] Fixing bug in handling of statement contracts
(duplication of blocks)
---
.../e-acsl-runtime/oracle/gen_stmt_contract.c | 59 +++++---
.../oracle/stmt_contract.res.oracle | 133 ++++++++++++++----
.../tests/e-acsl-runtime/stmt_contract.i | 10 +-
src/plugins/e-acsl/visit.ml | 74 +++++-----
4 files changed, 186 insertions(+), 90 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
index a25ef89b8e5..9141713a57c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
@@ -827,27 +827,50 @@ int main(void)
}
x += y;
- /*@ requires x ≡ 5;
- ensures x ≡ 5; */
+ /*@ requires x ≡ 5; */
+ /*@ requires y ≡ 2; */
+ { mpz_t e_acsl_86; mpz_t e_acsl_87; int e_acsl_88;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_86),(long)y);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_87),(long)2);
+ e_acsl_88 = __gmpz_cmp((__mpz_struct const *)(e_acsl_86),
+ (__mpz_struct const *)(e_acsl_87));
+ if (! (e_acsl_88 == 0)) { e_acsl_fail((char *)"(y == 2)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_86));
+ __gmpz_clear((__mpz_struct *)(e_acsl_87));
+ }
+
+ { mpz_t e_acsl_89; mpz_t e_acsl_90; int e_acsl_91;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_89),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_90),(long)5);
+ e_acsl_91 = __gmpz_cmp((__mpz_struct const *)(e_acsl_89),
+ (__mpz_struct const *)(e_acsl_90));
+ if (! (e_acsl_91 == 0)) { e_acsl_fail((char *)"(x == 5)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_89));
+ __gmpz_clear((__mpz_struct *)(e_acsl_90));
+ }
+
+ x += y;
+ /*@ requires x ≡ 7;
+ ensures x ≡ 7; */
{
- { mpz_t e_acsl_86; mpz_t e_acsl_87; int e_acsl_88;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_86),(long)x);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_87),(long)5);
- e_acsl_88 = __gmpz_cmp((__mpz_struct const *)(e_acsl_86),
- (__mpz_struct const *)(e_acsl_87));
- if (! (e_acsl_88 == 0)) { e_acsl_fail((char *)"(x == 5)"); }
- __gmpz_clear((__mpz_struct *)(e_acsl_86));
- __gmpz_clear((__mpz_struct *)(e_acsl_87));
+ { mpz_t e_acsl_92; mpz_t e_acsl_93; int e_acsl_94;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_92),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_93),(long)7);
+ e_acsl_94 = __gmpz_cmp((__mpz_struct const *)(e_acsl_92),
+ (__mpz_struct const *)(e_acsl_93));
+ if (! (e_acsl_94 == 0)) { e_acsl_fail((char *)"(x == 7)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_92));
+ __gmpz_clear((__mpz_struct *)(e_acsl_93));
}
__retres = 0;
- { mpz_t e_acsl_89; mpz_t e_acsl_90; int e_acsl_91;
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_89),(long)x);
- __gmpz_init_set_si((__mpz_struct *)(e_acsl_90),(long)5);
- e_acsl_91 = __gmpz_cmp((__mpz_struct const *)(e_acsl_89),
- (__mpz_struct const *)(e_acsl_90));
- if (! (e_acsl_91 == 0)) { e_acsl_fail((char *)"(x == 5)"); }
- __gmpz_clear((__mpz_struct *)(e_acsl_89));
- __gmpz_clear((__mpz_struct *)(e_acsl_90));
+ { mpz_t e_acsl_95; mpz_t e_acsl_96; int e_acsl_97;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_95),(long)x);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_96),(long)7);
+ e_acsl_97 = __gmpz_cmp((__mpz_struct const *)(e_acsl_95),
+ (__mpz_struct const *)(e_acsl_96));
+ if (! (e_acsl_97 == 0)) { e_acsl_fail((char *)"(x == 7)"); }
+ __gmpz_clear((__mpz_struct *)(e_acsl_95));
+ __gmpz_clear((__mpz_struct *)(e_acsl_96));
}
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
index 3f86f8c193f..489d27a1e0a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
@@ -483,16 +483,16 @@ PROJECT_FILE.i:246:[value] assigning non deterministic value for the first time
Called from PROJECT_FILE.i:306.
[value] Done for function mpz_clear
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:314.
+ Called from PROJECT_FILE.i:313.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:314.
+ Called from PROJECT_FILE.i:313.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:315.
+ Called from PROJECT_FILE.i:314.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:316.
+ Called from PROJECT_FILE.i:315.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -502,22 +502,72 @@ PROJECT_FILE.i:246:[value] assigning non deterministic value for the first time
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:317.
+ Called from PROJECT_FILE.i:316.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:317.
+ Called from PROJECT_FILE.i:316.
[value] Done for function mpz_clear
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:321.
+ Called from PROJECT_FILE.i:320.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:321.
+ Called from PROJECT_FILE.i:320.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:322.
+ Called from PROJECT_FILE.i:321.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:322.
+[value] computing for function printf <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:115.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:115.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:323.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:323.
+[value] Done for function mpz_clear
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:331.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:331.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- main.
+ Called from PROJECT_FILE.i:332.
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:333.
+[value] computing for function printf <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:115.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:115.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:334.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:334.
+[value] Done for function mpz_clear
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:338.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:338.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- main.
+ Called from PROJECT_FILE.i:339.
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:340.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -527,10 +577,10 @@ PROJECT_FILE.i:246:[value] assigning non deterministic value for the first time
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:324.
+ Called from PROJECT_FILE.i:341.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:324.
+ Called from PROJECT_FILE.i:341.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
@@ -539,7 +589,7 @@ PROJECT_FILE.i:246:[value] assigning non deterministic value for the first time
NON TERMINATING FUNCTION
[value] Values for function main:
__retres ∈ {0}
- x ∈ {5}
+ x ∈ {7}
y ∈ {2}
/* Generated by Frama-C */
struct __anonstruct___mpz_struct_1 {
@@ -835,27 +885,50 @@ int main(void)
}
x += y;
- /*@ requires x ≡ 5;
- ensures x ≡ 5; */
+ /*@ requires x ≡ 5; */
+ /*@ requires y ≡ 2; */
+ { mpz_t e_acsl_86; mpz_t e_acsl_87; int e_acsl_88;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_86),(long)y);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_87),(long)2);
+ e_acsl_88 = mpz_cmp((__mpz_struct const *)(e_acsl_86),
+ (__mpz_struct const *)(e_acsl_87));
+ if (! (e_acsl_88 == 0)) { e_acsl_fail((char *)"(y == 2)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_86));
+ mpz_clear((__mpz_struct *)(e_acsl_87));
+ }
+
+ { mpz_t e_acsl_89; mpz_t e_acsl_90; int e_acsl_91;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_89),(long)x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_90),(long)5);
+ e_acsl_91 = mpz_cmp((__mpz_struct const *)(e_acsl_89),
+ (__mpz_struct const *)(e_acsl_90));
+ if (! (e_acsl_91 == 0)) { e_acsl_fail((char *)"(x == 5)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_89));
+ mpz_clear((__mpz_struct *)(e_acsl_90));
+ }
+
+ x += y;
+ /*@ requires x ≡ 7;
+ ensures x ≡ 7; */
{
- { mpz_t e_acsl_86; mpz_t e_acsl_87; int e_acsl_88;
- mpz_init_set_si((__mpz_struct *)(e_acsl_86),(long)x);
- mpz_init_set_si((__mpz_struct *)(e_acsl_87),(long)5);
- e_acsl_88 = mpz_cmp((__mpz_struct const *)(e_acsl_86),
- (__mpz_struct const *)(e_acsl_87));
- if (! (e_acsl_88 == 0)) { e_acsl_fail((char *)"(x == 5)"); }
- mpz_clear((__mpz_struct *)(e_acsl_86));
- mpz_clear((__mpz_struct *)(e_acsl_87));
+ { mpz_t e_acsl_92; mpz_t e_acsl_93; int e_acsl_94;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_92),(long)x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_93),(long)7);
+ e_acsl_94 = mpz_cmp((__mpz_struct const *)(e_acsl_92),
+ (__mpz_struct const *)(e_acsl_93));
+ if (! (e_acsl_94 == 0)) { e_acsl_fail((char *)"(x == 7)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_92));
+ mpz_clear((__mpz_struct *)(e_acsl_93));
}
__retres = 0;
- { mpz_t e_acsl_89; mpz_t e_acsl_90; int e_acsl_91;
- mpz_init_set_si((__mpz_struct *)(e_acsl_89),(long)x);
- mpz_init_set_si((__mpz_struct *)(e_acsl_90),(long)5);
- e_acsl_91 = mpz_cmp((__mpz_struct const *)(e_acsl_89),
- (__mpz_struct const *)(e_acsl_90));
- if (! (e_acsl_91 == 0)) { e_acsl_fail((char *)"(x == 5)"); }
- mpz_clear((__mpz_struct *)(e_acsl_89));
- mpz_clear((__mpz_struct *)(e_acsl_90));
+ { mpz_t e_acsl_95; mpz_t e_acsl_96; int e_acsl_97;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_95),(long)x);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_96),(long)7);
+ e_acsl_97 = mpz_cmp((__mpz_struct const *)(e_acsl_95),
+ (__mpz_struct const *)(e_acsl_96));
+ if (! (e_acsl_97 == 0)) { e_acsl_fail((char *)"(x == 7)"); }
+ mpz_clear((__mpz_struct *)(e_acsl_95));
+ mpz_clear((__mpz_struct *)(e_acsl_96));
}
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/stmt_contract.i b/src/plugins/e-acsl/tests/e-acsl-runtime/stmt_contract.i
index 60314cece3d..eb443f78b14 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/stmt_contract.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/stmt_contract.i
@@ -39,11 +39,11 @@ int main(void) {
x = x + y;
// TODO: break the CFG and I don't know why :(
- /* /\*@ requires x == 3; *\/ */
- /* /\*@ requires y == 2; *\/ */
- /* x = x + y; */
+ /*@ requires x == 5; */
+ /*@ requires y == 2; */
+ x = x + y;
- /*@ requires x == 5;
- @ ensures x == 5; */
+ /*@ requires x == 7;
+ @ ensures x == 7; */
return 0;
}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index a3c201b31fb..0e72131f5b7 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -269,36 +269,32 @@ let rec named_predicate_to_exp env p =
statement (if any) for runtime assertion checking *)
(* ************************************************************************** *)
-let convert_preconditions only_behaviors env behaviors =
+let convert_preconditions env behaviors =
let do_behavior env b =
- if only_behaviors = [] || List.mem b.b_name only_behaviors then begin
- let assumes_pred =
- List.fold_left
- (fun acc p -> Logic_const.pand (acc, Logic_const.unamed p.ip_content))
- Logic_const.ptrue
- b.b_assumes
- in
+ let assumes_pred =
List.fold_left
- (fun env p ->
- let p =
- Logic_const.pimplies (assumes_pred, Logic_const.unamed p.ip_content)
- in
- let e, env = named_predicate_to_exp env p in
- Env.add_stmt env (Misc.mk_e_acsl_guard ~reverse:true e p))
- env
- b.b_requires
- end else
+ (fun acc p -> Logic_const.pand (acc, Logic_const.unamed p.ip_content))
+ Logic_const.ptrue
+ b.b_assumes
+ in
+ List.fold_left
+ (fun env p ->
+ let p =
+ Logic_const.pimplies (assumes_pred, Logic_const.unamed p.ip_content)
+ in
+ let e, env = named_predicate_to_exp env p in
+ Env.add_stmt env (Misc.mk_e_acsl_guard ~reverse:true e p))
env
+ b.b_requires
in
List.fold_left do_behavior env behaviors
-let convert_postconditions only_behaviors env behaviors =
+let convert_postconditions env behaviors =
(* generate one guard by postcondition of each behavior *)
let do_behavior env b =
- if only_behaviors = [] || List.mem b.b_name only_behaviors then begin
- List.fold_left
- (fun env (t, p) ->
- match t with
+ List.fold_left
+ (fun env (t, p) ->
+ match t with
| Normal ->
let p = p.ip_content in
if p <> Ptrue && b.b_assumes <> [] then
@@ -308,35 +304,36 @@ let convert_postconditions only_behaviors env behaviors =
Env.add_stmt env (Misc.mk_e_acsl_guard ~reverse:true e p)
| Exits | Breaks | Continues | Returns ->
Misc.not_yet "abnormal termination case in behavior")
- env
- b.b_post_cond
- end else
env
+ b.b_post_cond
in
List.fold_left do_behavior env behaviors
-let convert_behaviors only_behaviors env behaviors =
+let convert_behaviors env behaviors =
List.iter
(fun b ->
if b.b_assigns <> WritesAny then
Misc.not_yet "assigns clause in behavior";
if b.b_extended <> [] then Misc.not_yet "grammar extensions in behavior")
behaviors;
- let pre_env = convert_preconditions only_behaviors env behaviors in
+ let pre_env =
+ convert_preconditions (Env.no_overlap ~from:env Env.empty) behaviors
+ in
let post_env =
- convert_postconditions
- only_behaviors (Env.no_overlap ~from:pre_env env) behaviors
+ convert_postconditions (Env.no_overlap ~from:pre_env Env.empty) behaviors
in
+ let env = Env.merge_function_vars ~from:pre_env env in
+ let env = Env.merge_function_vars ~from:post_env env in
Env.close_block_option pre_env,
Env.close_block_option post_env,
- Env.merge_function_vars ~from:post_env pre_env
+ env
-let convert_spec only_behaviors env spec =
+let convert_spec env spec =
if spec.spec_variant <> None then Misc.not_yet "variant clause";
if spec.spec_terminates <> None then Misc.not_yet "terminates clause";
if spec.spec_complete_behaviors <> [] then Misc.not_yet "complete behaviors";
if spec.spec_disjoint_behaviors <> [] then Misc.not_yet "disjoint behaviors";
- convert_behaviors only_behaviors env spec.spec_behavior
+ convert_behaviors env spec.spec_behavior
let convert_named_predicate env p =
let e, env = named_predicate_to_exp env p in
@@ -349,9 +346,11 @@ let convert_annotation env annot =
| AAssert(l, p) ->
if l <> [] then Misc.not_yet "assertions applied only on some behaviors";
convert_named_predicate env p, None
- | AStmtSpec(only_behaviors, spec) ->
- let pre_block, post_block, new_env =
- convert_spec only_behaviors env spec
+ | AStmtSpec(l, spec) ->
+ if l <> [] then
+ Misc.not_yet "statement contract applied only on some behaviors";
+ let pre_block, post_block, new_env =
+ convert_spec env spec
in
let env = Env.merge_function_vars ~from:new_env env in
let env = match pre_block with
@@ -405,7 +404,7 @@ class e_acsl_visitor prj generate = object (self)
try
let kf = Globals.Functions.get vi in
let pre_b, post_b, env =
- convert_spec [] Env.empty (Kernel_function.get_spec kf)
+ convert_spec Env.empty (Kernel_function.get_spec kf)
in
pre_block <- pre_b;
post_block <- post_b;
@@ -432,7 +431,8 @@ class e_acsl_visitor prj generate = object (self)
let env, post_block = convert_rooted env ba in
let post_stmts = match post_block with
| None -> post_stmts
- | Some b -> mkStmt ~valid_sid:true (Block b) :: post_stmts
+ | Some b ->
+ mkStmt ~valid_sid:true (Block b) :: post_stmts
in
env, post_stmts)
stmt
--
GitLab