diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 719ddd88bf4ad108260ad2ea520087f5add265ce..d5ff495ee8e3ce6d4540d2a11f600e893d713473 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 0c42f7aab3cbccaa2fde6d5345715203b1cc5fef..9b29f4bc05d661b117f77eb31f912f0103cfe30c 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 953aab3bce73223ada331ddb1d509f05e5b44e3b..73b9047ed0bd81ff8eb72811aefc2058a4159294 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 e7438f3f838b84e937d4ea0733665af8b075d31b..f979bf5871825db84a8cc5a2d576c3e4e201fafe 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 70d3c69e5e6273dec1fef967f73dccd716797409..51f3303b8662e204b597f65564e6abf65cee4548 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 6fe363eac68b79186b971164e152cbd566e9b31e..8870dde3d615c67ac13a2ce8fce8af477847cefb 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 5f8991d6c83955d5174d2c1bfbbc27c308baab10..356e129f4e4bea0b9a054c5e4c650c2f0601d7cb 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