From ef9e3cb6436b4b1d572dca6ab880918f8edc4ac5 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 7 Jun 2021 09:59:00 +0200
Subject: [PATCH] [wp] Warns on missing terminates clause
---
src/plugins/wp/cfgAnnot.ml | 6 ++++--
src/plugins/wp/cfgAnnot.mli | 2 +-
src/plugins/wp/cfgCalculus.ml | 7 ++++++-
.../wp_acsl/oracle/terminates_call_options.0.res.oracle | 4 ++++
.../wp_acsl/oracle/terminates_call_options.1.res.oracle | 4 ++++
.../oracle_qualif/terminates_call_options.0.res.oracle | 4 ++++
.../oracle_qualif/terminates_call_options.1.res.oracle | 4 ++++
7 files changed, 27 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 719ddd88bf4..d5ff495ee8e 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -191,12 +191,14 @@ let get_terminates kf =
let get_terminates_call kf =
match (Annotations.funspec kf).spec_terminates with
| Some p ->
- normalize_terminates p
+ false, normalize_terminates p
| None when Kernel_function.is_definition kf ->
+ true,
if Wp_parameters.TerminatesDefinitions.get ()
then Logic_const.ptrue
else Logic_const.pfalse
| None ->
+ true,
if Wp_parameters.TerminatesDeclarations.get ()
then Logic_const.ptrue
else Logic_const.pfalse
@@ -213,7 +215,7 @@ type contract = {
contract_exit : WpPropId.pred_info list ;
contract_smoke : WpPropId.pred_info list ;
contract_assigns : Cil_types.assigns ;
- contract_terminates : Cil_types.predicate ;
+ contract_terminates : bool * Cil_types.predicate ;
}
let assigns_upper_bound behaviors =
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index 0c42f7aab3c..9b29f4bc05d 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -105,7 +105,7 @@ type contract = {
contract_exit : pred_info list ;
contract_smoke : pred_info list ;
contract_assigns : assigns ;
- contract_terminates : predicate ;
+ contract_terminates : bool * predicate ; (* boolean: default generated *)
}
val get_call_contract : ?smoking:stmt -> kernel_function -> stmt -> contract
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 953aab3bce7..73b9047ed0b 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -338,7 +338,12 @@ struct
in
match env.terminates with
| Some p when is_default_bhv env.mode && is_selected ~goal:true env p ->
- W.call_terminates env.we p s kf es ~callee_t:c.contract_terminates w_pre
+ let generated, callee_t = c.contract_terminates in
+ if generated then
+ Wp_parameters.warning ~once:true
+ "Missing terminates clause on call to %a, defaults to %a"
+ Kernel_function.pretty kf Cil_printer.pp_predicate callee_t ;
+ W.call_terminates env.we p s kf es ~callee_t w_pre
| _ -> w_pre
let do_complete_disjoint env w =
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 e7438f3f838..f979bf58718 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
@@ -2,6 +2,10 @@
[kernel] Parsing tests/wp_acsl/terminates_call_options.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/terminates_call_options.i:21: Warning:
+ 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
------------------------------------------------------------
Function call_declaration
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
index 70d3c69e5e6..51f3303b866 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
@@ -2,6 +2,10 @@
[kernel] Parsing tests/wp_acsl/terminates_call_options.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/terminates_call_options.i:21: Warning:
+ Missing terminates clause on call to declaration, defaults to \true
+[wp] tests/wp_acsl/terminates_call_options.i:26: Warning:
+ Missing terminates clause on call to definition, defaults to \true
------------------------------------------------------------
Function call_declaration
------------------------------------------------------------
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 6fe363eac68..8870dde3d61 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
@@ -2,6 +2,10 @@
[kernel] Parsing tests/wp_acsl/terminates_call_options.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/terminates_call_options.i:21: Warning:
+ 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] [Qed] Goal typed_definition_assigns : Valid
[wp] [Qed] Goal typed_call_declaration_terminates_part1 : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
index 5f8991d6c83..356e129f4e4 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
@@ -2,6 +2,10 @@
[kernel] Parsing tests/wp_acsl/terminates_call_options.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/terminates_call_options.i:21: Warning:
+ Missing terminates clause on call to declaration, defaults to \true
+[wp] tests/wp_acsl/terminates_call_options.i:26: Warning:
+ Missing terminates clause on call to definition, defaults to \true
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_definition_assigns : Valid
[wp] [Qed] Goal typed_call_declaration_terminates : Valid
--
GitLab