From 91cd6b419d28a69d05b8a04ab5d84801bff9e676 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 7 Jun 2021 10:44:28 +0200
Subject: [PATCH] [wp] Trivial termination handled before WP
---
src/plugins/wp/cfgCalculus.ml | 7 ---
src/plugins/wp/cfgInfos.ml | 32 +++++++++++++
.../terminates_call_options.0.res.oracle | 14 +-----
.../oracle/terminates_formulae.res.oracle | 47 +++----------------
.../terminates_variant_option.0.res.oracle | 15 ------
.../terminates_variant_option.1.res.oracle | 15 ------
.../terminates_call_options.0.res.oracle | 16 +++----
.../terminates_formulae.res.oracle | 39 +++++++--------
.../terminates_variant_option.0.res.oracle | 15 +++---
.../terminates_variant_option.1.res.oracle | 15 +++---
src/plugins/wp/wpAnnot.ml | 14 ++++++
src/plugins/wp/wpAnnot.mli | 1 +
12 files changed, 90 insertions(+), 140 deletions(-)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 73b9047ed0b..ffc222e95de 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -400,12 +400,6 @@ struct
env.wk <- if exits then do_exit env ~formals b w else w ;
wp env cfg.entry_point
- let do_terminates env w =
- match env.terminates with
- | Some p when is_default_bhv env.mode && is_selected ~goal:true env p ->
- prove_property env (fst p, Logic_const.ptrue) w
- | _ -> w
-
(* Putting everything together *)
let compute ~mode ~props =
let kf = mode.kf in
@@ -438,7 +432,6 @@ struct
do_preconditions env ~formals bhv @@
do_complete_disjoint env @@
do_funbehavior env ~formals ~exits bhv @@
- do_terminates env @@
W.empty
end
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 0bb9bfc65f1..203ded1f820 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -22,6 +22,7 @@
module Cfg = Interpreted_automata
module Fset = Kernel_function.Set
+module Sset = Cil_datatype.Stmt.Set
module Shash = Cil_datatype.Stmt.Hashtbl
(* -------------------------------------------------------------------------- *)
@@ -37,6 +38,7 @@ type t = {
mutable annots : bool; (* has goals to prove *)
mutable doomed : WpPropId.prop_id Bag.t;
mutable calls : Kernel_function.Set.t;
+ mutable no_variant_loops : Sset.t;
}
(* -------------------------------------------------------------------------- *)
@@ -165,6 +167,22 @@ let collect_calls ~bhv kf stmt =
x vf args kind loc
| _ -> Fset.empty
+(* -------------------------------------------------------------------------- *)
+(* --- No variant loops --- *)
+(* -------------------------------------------------------------------------- *)
+
+let collect_loops_no_variant stmt =
+ let open Cil_types in
+ let fold_no_variant _ = function
+ | { annot_content = AVariant _ } -> (&&) false
+ | _ -> (&&) true
+ in
+ match stmt.skind with
+ | Loop _ when Annotations.fold_code_annot fold_no_variant stmt true ->
+ Sset.singleton stmt
+ | _ ->
+ Sset.empty
+
(* -------------------------------------------------------------------------- *)
(* --- Memoization Key --- *)
(* -------------------------------------------------------------------------- *)
@@ -247,6 +265,7 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
annots = false ;
doomed = Bag.empty ;
calls = Fset.empty ;
+ no_variant_loops = Sset.empty
} in
let behaviors = Annotations.behaviors kf in
(* Inits *)
@@ -264,6 +283,7 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
Shash.iter
(fun stmt (src,_) ->
let fs = collect_calls ~bhv kf stmt in
+ let nv_loops = collect_loops_no_variant stmt in
let dead = unreachable infos src in
let ca = CfgAnnot.get_code_assertions kf stmt in
let ca_pids = List.map fst ca.code_verified in
@@ -284,6 +304,8 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
Fset.exists (selected_call ~bhv ~prop) fs )
then infos.annots <- true ;
infos.calls <- Fset.union fs infos.calls ;
+ infos.no_variant_loops <-
+ Sset.union nv_loops infos.no_variant_loops ;
end
) cfg.stmt_table ;
(* Dead Post Conditions *)
@@ -305,6 +327,16 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
Bag.iter
(fun p -> if WpPropId.filter_status p then WpAnnot.set_unreachable p)
infos.doomed ;
+ (* Trivial terminates *)
+ begin match Annotations.terminates kf with
+ | Some t
+ when selected_terminates ~prop kf
+ && infos.calls = Fset.empty
+ && infos.no_variant_loops = Sset.empty ->
+ WpAnnot.set_trivially_terminates @@
+ WpPropId.mk_terminates_id kf Kglobal t
+ | _ -> ()
+ end ;
(* Collected Infos *)
infos
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle
index f979bf58718..4a627a68199 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle
@@ -10,12 +10,7 @@
Function call_declaration
------------------------------------------------------------
-Goal Termination-condition (file tests/wp_acsl/terminates_call_options.i, line 19) in 'call_declaration' (1/2):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Termination-condition (file tests/wp_acsl/terminates_call_options.i, line 19) in 'call_declaration' (2/2):
+Goal Termination-condition (file tests/wp_acsl/terminates_call_options.i, line 19) in 'call_declaration':
Call Effect at line 21
Prove: false.
@@ -24,12 +19,7 @@ Prove: false.
Function call_definition
------------------------------------------------------------
-Goal Termination-condition (file tests/wp_acsl/terminates_call_options.i, line 24) in 'call_definition' (1/2):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Termination-condition (file tests/wp_acsl/terminates_call_options.i, line 24) in 'call_definition' (2/2):
+Goal Termination-condition (file tests/wp_acsl/terminates_call_options.i, line 24) in 'call_definition':
Call Effect at line 26
Prove: false.
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
index 032fbb6e338..81be3fb1362 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
@@ -6,12 +6,7 @@
Function base_call
------------------------------------------------------------
-Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 22) in 'base_call' (1/2):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 22) in 'base_call' (2/2):
+Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 22) in 'base_call':
Call Effect at line 24
Assume { (* Heap *) Type: is_sint32(a). (* Goal *) When: P_Q. }
Prove: P_P(a).
@@ -21,12 +16,7 @@ Prove: P_P(a).
Function call_change
------------------------------------------------------------
-Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 32) in 'call_change' (1/2):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 32) in 'call_change' (2/2):
+Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 32) in 'call_change':
Call Effect at line 35
Assume { (* Heap *) Type: is_sint32(a). (* Goal *) When: P_P(a). }
Prove: P_P(0).
@@ -36,12 +26,7 @@ Prove: P_P(0).
Function call_param_change
------------------------------------------------------------
-Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 48) in 'call_param_change' (1/2):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 48) in 'call_param_change' (2/2):
+Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 48) in 'call_param_change':
Call Effect at line 51
Let x = Mint_0[p].
Assume {
@@ -58,12 +43,7 @@ Prove: false.
Function call_param_same
------------------------------------------------------------
-Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 43) in 'call_param_same' (1/2):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 43) in 'call_param_same' (2/2):
+Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 43) in 'call_param_same':
Call Effect at line 45
Prove: true.
@@ -72,12 +52,7 @@ Prove: true.
Function call_same
------------------------------------------------------------
-Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 27) in 'call_same' (1/2):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 27) in 'call_same' (2/2):
+Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 27) in 'call_same':
Call Effect at line 29
Prove: true.
@@ -86,12 +61,7 @@ Prove: true.
Function no_variant
------------------------------------------------------------
-Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 62) in 'no_variant' (1/2):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 62) in 'no_variant' (2/2):
+Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 62) in 'no_variant':
Effect at line 65
Prove: !P_Q.
@@ -105,11 +75,6 @@ Prove: true.
Function variant
------------------------------------------------------------
-Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 54) in 'variant':
-Prove: true.
-
-------------------------------------------------------------
-
Goal Loop assigns (file tests/wp_acsl/terminates_formulae.i, line 56):
Prove: true.
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 4c0590685f6..6d44b1ce657 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
@@ -6,11 +6,6 @@
Function f1
------------------------------------------------------------
-Goal Termination-condition (file tests/wp_acsl/terminates_variant_option.i, line 34) in 'f1':
-Prove: true.
-
-------------------------------------------------------------
-
Goal Preservation of Invariant (file tests/wp_acsl/terminates_variant_option.i, line 37):
Assume {
Type: is_sint32(c1_0) /\ is_sint32(cpt_0) /\ is_sint32(cpt_0 - 1).
@@ -64,11 +59,6 @@ Prove: 0 <= cpt_0.
Function fails_decreases
------------------------------------------------------------
-Goal Termination-condition (file tests/wp_acsl/terminates_variant_option.i, line 23) in 'fails_decreases':
-Prove: true.
-
-------------------------------------------------------------
-
Goal Loop assigns (file tests/wp_acsl/terminates_variant_option.i, line 26):
Prove: true.
@@ -95,11 +85,6 @@ Prove: true.
Function fails_positive
------------------------------------------------------------
-Goal Termination-condition (file tests/wp_acsl/terminates_variant_option.i, line 13) in 'fails_positive':
-Prove: true.
-
-------------------------------------------------------------
-
Goal Preservation of Invariant (file tests/wp_acsl/terminates_variant_option.i, line 15):
Let x = Mint_0[p].
Assume {
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 9b9f856e6c3..edc34bb3c90 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
@@ -6,11 +6,6 @@
Function f1
------------------------------------------------------------
-Goal Termination-condition (file tests/wp_acsl/terminates_variant_option.i, line 34) in 'f1':
-Prove: true.
-
-------------------------------------------------------------
-
Goal Preservation of Invariant (file tests/wp_acsl/terminates_variant_option.i, line 37):
Assume {
Type: is_sint32(c1_0) /\ is_sint32(cpt_0) /\ is_sint32(cpt_0 - 1).
@@ -59,11 +54,6 @@ Prove: 0 <= cpt_0.
Function fails_decreases
------------------------------------------------------------
-Goal Termination-condition (file tests/wp_acsl/terminates_variant_option.i, line 23) in 'fails_decreases':
-Prove: true.
-
-------------------------------------------------------------
-
Goal Loop assigns (file tests/wp_acsl/terminates_variant_option.i, line 26):
Prove: true.
@@ -83,11 +73,6 @@ Prove: true.
Function fails_positive
------------------------------------------------------------
-Goal Termination-condition (file tests/wp_acsl/terminates_variant_option.i, line 13) in 'fails_positive':
-Prove: true.
-
-------------------------------------------------------------
-
Goal Preservation of Invariant (file tests/wp_acsl/terminates_variant_option.i, line 15):
Let x = Mint_0[p].
Assume {
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle
index 8870dde3d61..7b93fe01e15 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle
@@ -6,18 +6,16 @@
Missing terminates clause on call to declaration, defaults to \false
[wp] tests/wp_acsl/terminates_call_options.i:26: Warning:
Missing terminates clause on call to definition, defaults to \false
-[wp] 5 goals scheduled
+[wp] 3 goals scheduled
[wp] [Qed] Goal typed_definition_assigns : Valid
-[wp] [Qed] Goal typed_call_declaration_terminates_part1 : Valid
-[wp] [Alt-Ergo] Goal typed_call_declaration_terminates_part2 : Unsuccess
-[wp] [Qed] Goal typed_call_definition_terminates_part1 : Valid
-[wp] [Alt-Ergo] Goal typed_call_definition_terminates_part2 : Unsuccess
-[wp] Proved goals: 3 / 5
- Qed: 3
+[wp] [Alt-Ergo] Goal typed_call_declaration_terminates : Unsuccess
+[wp] [Alt-Ergo] Goal typed_call_definition_terminates : Unsuccess
+[wp] Proved goals: 1 / 3
+ Qed: 1
Alt-Ergo: 0 (unsuccess: 2)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
definition 1 - 1 100%
- call_declaration 1 - 2 50.0%
- call_definition 1 - 2 50.0%
+ call_declaration - - 1 0.0%
+ call_definition - - 1 0.0%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
index 1b83f3171c6..095b267c6ec 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
@@ -2,34 +2,27 @@
[kernel] Parsing tests/wp_acsl/terminates_formulae.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 17 goals scheduled
-[wp] [Qed] Goal typed_base_call_terminates_part1 : Valid
-[wp] [Alt-Ergo] Goal typed_base_call_terminates_part2 : Unsuccess
-[wp] [Qed] Goal typed_call_same_terminates_part1 : Valid
-[wp] [Qed] Goal typed_call_same_terminates_part2 : Valid
-[wp] [Qed] Goal typed_call_change_terminates_part1 : Valid
-[wp] [Alt-Ergo] Goal typed_call_change_terminates_part2 : Unsuccess
-[wp] [Qed] Goal typed_call_param_same_terminates_part1 : Valid
-[wp] [Qed] Goal typed_call_param_same_terminates_part2 : Valid
-[wp] [Qed] Goal typed_call_param_change_terminates_part1 : Valid
-[wp] [Alt-Ergo] Goal typed_call_param_change_terminates_part2 : Unsuccess
-[wp] [Qed] Goal typed_variant_terminates : Valid
+[wp] 10 goals scheduled
+[wp] [Alt-Ergo] Goal typed_base_call_terminates : Unsuccess
+[wp] [Qed] Goal typed_call_same_terminates : Valid
+[wp] [Alt-Ergo] Goal typed_call_change_terminates : Unsuccess
+[wp] [Qed] Goal typed_call_param_same_terminates : Valid
+[wp] [Alt-Ergo] Goal typed_call_param_change_terminates : Unsuccess
[wp] [Qed] Goal typed_variant_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_variant_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_variant_loop_variant_positive : Valid
-[wp] [Qed] Goal typed_no_variant_terminates_part1 : Valid
-[wp] [Alt-Ergo] Goal typed_no_variant_terminates_part2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_no_variant_terminates : Unsuccess
[wp] [Qed] Goal typed_no_variant_loop_assigns : Valid
-[wp] Proved goals: 13 / 17
- Qed: 12
+[wp] Proved goals: 6 / 10
+ Qed: 5
Alt-Ergo: 1 (unsuccess: 4)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- base_call 1 - 2 50.0%
- call_same 2 - 2 100%
- call_change 1 - 2 50.0%
- call_param_same 2 - 2 100%
- call_param_change 1 - 2 50.0%
- variant 3 1 4 100%
- no_variant 2 - 3 66.7%
+ base_call - - 1 0.0%
+ call_same 1 - 1 100%
+ call_change - - 1 0.0%
+ call_param_same 1 - 1 100%
+ call_param_change - - 1 0.0%
+ variant 2 1 3 100%
+ no_variant 1 - 2 50.0%
------------------------------------------------------------
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 ed6365ffa37..fea85c63ab7 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,30 +2,27 @@
[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] [Qed] Goal typed_fails_positive_terminates : Valid
+[wp] 14 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
[wp] [Qed] Goal typed_fails_positive_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_fails_positive_loop_variant_decrease : Valid
[wp] [Alt-Ergo] Goal typed_fails_positive_loop_variant_positive : Unsuccess
-[wp] [Qed] Goal typed_fails_decreases_terminates : Valid
[wp] [Qed] Goal typed_fails_decreases_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_fails_decreases_loop_variant_decrease : Unsuccess
[wp] [Qed] Goal typed_fails_decreases_loop_variant_positive : Valid
-[wp] [Qed] Goal typed_f1_terminates : Valid
[wp] [Alt-Ergo] Goal typed_f1_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_f1_loop_invariant_established : Valid
[wp] [Qed] Goal typed_f1_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_f1_loop_variant_decrease : Unsuccess
[wp] [Alt-Ergo] Goal typed_f1_loop_variant_positive : Valid
-[wp] Proved goals: 14 / 17
- Qed: 11
+[wp] Proved goals: 11 / 14
+ Qed: 8
Alt-Ergo: 3 (unsuccess: 3)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- fails_positive 5 1 7 85.7%
- fails_decreases 3 - 4 75.0%
- f1 3 2 6 83.3%
+ fails_positive 4 1 6 83.3%
+ fails_decreases 2 - 3 66.7%
+ f1 2 2 5 80.0%
------------------------------------------------------------
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 c7928a6b12e..5f25f74bab3 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
@@ -2,30 +2,27 @@
[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] [Qed] Goal typed_fails_positive_terminates : Valid
+[wp] 14 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
[wp] [Qed] Goal typed_fails_positive_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_fails_positive_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_fails_positive_loop_variant_positive : Valid
-[wp] [Qed] Goal typed_fails_decreases_terminates : Valid
[wp] [Qed] Goal typed_fails_decreases_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_fails_decreases_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_fails_decreases_loop_variant_positive : Valid
-[wp] [Qed] Goal typed_f1_terminates : Valid
[wp] [Alt-Ergo] Goal typed_f1_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_f1_loop_invariant_established : Valid
[wp] [Qed] Goal typed_f1_loop_assigns : Valid
[wp] [Qed] Goal typed_f1_loop_variant_decrease : Valid
[wp] [Alt-Ergo] Goal typed_f1_loop_variant_positive : Valid
-[wp] Proved goals: 17 / 17
- Qed: 13
+[wp] Proved goals: 14 / 14
+ Qed: 10
Alt-Ergo: 4
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- fails_positive 6 1 7 100%
- fails_decreases 3 1 4 100%
- f1 4 2 6 100%
+ fails_positive 5 1 6 100%
+ fails_decreases 2 1 3 100%
+ f1 3 2 5 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index fef919f1502..7b2126233d0 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -76,6 +76,20 @@ let set_unreachable pid =
in
List.iter emit pids
+(* -------------------------------------------------------------------------- *)
+(* --- Status of Terminates Annotations --- *)
+(* -------------------------------------------------------------------------- *)
+let wp_trivially_terminates =
+ Emitter.create
+ "Trivial Termination"
+ [Emitter.Property_status]
+ ~correctness:[] (* TBC *)
+ ~tuning:[] (* TBC *)
+
+let set_trivially_terminates p =
+ let pid = WpPropId.property_of_id p in
+ Property_status.emit wp_trivially_terminates ~hyps:[] pid Property_status.True
+
(* -------------------------------------------------------------------------- *)
(* --- Preconditions at Callsites --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpAnnot.mli b/src/plugins/wp/wpAnnot.mli
index a0a268cbc61..e08e70cdcbc 100644
--- a/src/plugins/wp/wpAnnot.mli
+++ b/src/plugins/wp/wpAnnot.mli
@@ -35,6 +35,7 @@ open Cil_types
val unreachable_proved : int ref
val unreachable_failed : int ref
val set_unreachable : WpPropId.prop_id -> unit
+val set_trivially_terminates : WpPropId.prop_id -> unit
type asked_assigns = NoAssigns | OnlyAssigns | WithAssigns
--
GitLab