From 3e139296f61ffefbe5c0883a17fcc18efa71161b Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 8 Jun 2021 15:29:18 +0200
Subject: [PATCH] [wp] extended variant verification when terminates
---
src/plugins/wp/cfgAnnot.ml | 22 +++++++++----------
.../terminates_variant_option.0.res.oracle | 18 +++++++++++++++
.../terminates_variant_option.1.res.oracle | 20 +++++++++++++++++
.../terminates_variant_option.0.res.oracle | 12 ++++++----
.../terminates_variant_option.1.res.oracle | 12 +++++++---
.../tests/wp_acsl/terminates_variant_option.i | 7 ++++++
6 files changed, 73 insertions(+), 18 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 0b715a6aee4..93e8cd53242 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -207,7 +207,7 @@ let get_terminates kf =
| Some p ->
Some (WpPropId.mk_terminates_id kf Kglobal p, normalize_terminates p)
-let get_terminates_call kf =
+let get_terminates_hyp kf =
let to_default option =
if option then Logic_const.ptrue else Logic_const.pfalse in
match Annotations.terminates kf with
@@ -307,7 +307,7 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
| WritesAny -> WritesAny
| Writes froms -> Writes (normalize_froms Normal froms)
in
- let terminates = get_terminates_call kf in
+ let terminates = get_terminates_hyp kf in
{
contract_cond = List.rev !wcond ;
contract_hpre = List.rev !whpre ;
@@ -488,15 +488,15 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
WpStrategy.mk_variant_properties kf stmt ca term in
let intro_terminates (pid, v) =
pid,
- match get_terminates kf with
- | Some (_,t) when Wp_parameters.TerminatesVariantHyp.get () ->
- if Logic_utils.is_same_predicate t Logic_const.pfalse then
- Wp_parameters.warning
- ~source:(fst term.term_loc) ~once:true
- "Loop variant is always trivially verified \
- (terminates \\false)" ;
- Logic_const.pimplies (t, v)
- | _ -> v
+ let t = snd @@ get_terminates_hyp kf in
+ if Wp_parameters.TerminatesVariantHyp.get () then begin
+ if Logic_utils.is_same_predicate t Logic_const.pfalse then
+ Wp_parameters.warning
+ ~source:(fst term.term_loc) ~once:true
+ "Loop variant is always trivially verified \
+ (terminates \\false)" ;
+ Logic_const.pimplies (t, v)
+ end else v
in
{ l with loop_terminates = None ;
loop_preserved =
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.0.res.oracle
index 7a22f208d35..758094faa1e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.0.res.oracle
@@ -155,3 +155,21 @@ Goal Positivity of Loop variant at loop (file tests/wp_acsl/terminates_variant_o
Prove: false.
------------------------------------------------------------
+------------------------------------------------------------
+ Function trivial_variant_default
+------------------------------------------------------------
+
+Goal Loop assigns nothing:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 61):
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 61):
+Prove: false.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.1.res.oracle
index a000f9536e6..2324adf7478 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.1.res.oracle
@@ -4,6 +4,8 @@
[wp] Warning: Missing RTE guards
[wp] tests/wp_acsl/terminates_variant_option.i:52: Warning:
Loop variant is always trivially verified (terminates \false)
+[wp] tests/wp_acsl/terminates_variant_option.i:59: Warning:
+ Loop variant is always trivially verified (terminates \false)
------------------------------------------------------------
Function f1
------------------------------------------------------------
@@ -135,3 +137,21 @@ Goal Positivity of Loop variant at loop (file tests/wp_acsl/terminates_variant_o
Prove: true.
------------------------------------------------------------
+------------------------------------------------------------
+ Function trivial_variant_default
+------------------------------------------------------------
+
+Goal Loop assigns nothing:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 61):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_acsl/terminates_variant_option.i, line 61):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.0.res.oracle
index d620d07696e..927ca972024 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.0.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing tests/wp_acsl/terminates_variant_option.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 17 goals scheduled
+[wp] 20 goals scheduled
[wp] [Alt-Ergo] Goal typed_fails_positive_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_fails_positive_loop_invariant_established : Valid
[wp] [Qed] Goal typed_fails_positive_loop_assigns_part1 : Valid
@@ -20,13 +20,17 @@
[wp] [Qed] Goal typed_trivial_variant_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_trivial_variant_loop_variant_decrease : Unsuccess
[wp] [Alt-Ergo] Goal typed_trivial_variant_loop_variant_positive : Unsuccess
-[wp] Proved goals: 12 / 17
- Qed: 9
- Alt-Ergo: 3 (unsuccess: 5)
+[wp] [Qed] Goal typed_trivial_variant_default_loop_assigns : Valid
+[wp] [Alt-Ergo] Goal typed_trivial_variant_default_loop_variant_decrease : Unsuccess
+[wp] [Alt-Ergo] Goal typed_trivial_variant_default_loop_variant_positive : Unsuccess
+[wp] Proved goals: 13 / 20
+ Qed: 10
+ Alt-Ergo: 3 (unsuccess: 7)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
fails_positive 4 1 6 83.3%
fails_decreases 2 - 3 66.7%
f1 2 2 5 80.0%
trivial_variant 1 - 3 33.3%
+ trivial_variant_default 1 - 3 33.3%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.1.res.oracle
index 4dcd738b627..f7c77c67df3 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.1.res.oracle
@@ -4,7 +4,9 @@
[wp] Warning: Missing RTE guards
[wp] tests/wp_acsl/terminates_variant_option.i:52: Warning:
Loop variant is always trivially verified (terminates \false)
-[wp] 17 goals scheduled
+[wp] tests/wp_acsl/terminates_variant_option.i:59: Warning:
+ Loop variant is always trivially verified (terminates \false)
+[wp] 20 goals scheduled
[wp] [Alt-Ergo] Goal typed_fails_positive_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_fails_positive_loop_invariant_established : Valid
[wp] [Qed] Goal typed_fails_positive_loop_assigns_part1 : Valid
@@ -22,8 +24,11 @@
[wp] [Qed] Goal typed_trivial_variant_loop_assigns : Valid
[wp] [Qed] Goal typed_trivial_variant_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_trivial_variant_loop_variant_positive : Valid
-[wp] Proved goals: 17 / 17
- Qed: 13
+[wp] [Qed] Goal typed_trivial_variant_default_loop_assigns : Valid
+[wp] [Qed] Goal typed_trivial_variant_default_loop_variant_decrease : Valid
+[wp] [Qed] Goal typed_trivial_variant_default_loop_variant_positive : Valid
+[wp] Proved goals: 20 / 20
+ Qed: 16
Alt-Ergo: 4
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
@@ -31,4 +36,5 @@
fails_decreases 2 1 3 100%
f1 3 2 5 100%
trivial_variant 3 - 3 100%
+ trivial_variant_default 3 - 3 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/terminates_variant_option.i b/src/plugins/wp/tests/wp_acsl/terminates_variant_option.i
index 919cb6fc6ff..6720dff292d 100644
--- a/src/plugins/wp/tests/wp_acsl/terminates_variant_option.i
+++ b/src/plugins/wp/tests/wp_acsl/terminates_variant_option.i
@@ -53,3 +53,10 @@ void trivial_variant(void){
*/
while(1);
}
+
+void trivial_variant_default(void){
+ /*@ loop assigns \nothing ;
+ loop variant -1 ;
+ */
+ while(1);
+}
--
GitLab