diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 2629c793465eccb13baf84119b38d7b63a874099..a921d7ac21a0e8021a796aaa960b970eebf4a4a0 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -116,11 +116,20 @@ let get_behavior_goals kf ?(smoking=false) ?(exits=false) bhv =
let post_cond = normalize_post ~goal:true kf bhv in
let p_asgn, e_asgn = normalize_fct_assigns kf ~exits bhv bhv.b_assigns in
let smokes =
- if smoking && bhv.b_requires <> [] then
+ let do_assumes =
+ Wp_parameters.SmokeDeadassumes.get() && bhv.b_assumes <> [] in
+ if smoking && (bhv.b_requires <> [] || do_assumes) then
let bname =
if Cil.is_default_behavior bhv then "default" else bhv.b_name in
- let id = bname ^ "_requires" in
- let doomed = Property.ip_requires_of_behavior kf Kglobal bhv in
+ let id, doomed =
+ if bhv.b_requires <> []
+ then
+ bname ^ "_requires",
+ Property.ip_requires_of_behavior kf Kglobal bhv
+ else
+ bname ^ "_assumes",
+ Property.ip_assumes_of_behavior kf Kglobal bhv
+ in
[smoke kf ~id ~doomed ()]
else []
in
diff --git a/src/plugins/wp/tests/wp_plugin/doomed_pre.i b/src/plugins/wp/tests/wp_plugin/doomed_pre.i
new file mode 100644
index 0000000000000000000000000000000000000000..d7be0aa8c9a95835f78b720590d4f5a971a397a0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/doomed_pre.i
@@ -0,0 +1,56 @@
+/* run.config
+ OPT: -wp-smoke-tests
+*/
+
+/* run.config_qualif
+ OPT: -wp-smoke-tests
+*/
+
+//@ requires a < 0 && a > 0 ;
+void requires(int a){}
+
+/*@ requires a < 0 ;
+ behavior B:
+ assumes a > 0 ;
+*/
+void reqs_assumes(int a){}
+
+/*@ requires a < 0 ;
+ behavior B:
+ assumes a > 0 ;
+ assumes a > 1 ;
+*/
+void reqs_2_2_assumes(int a){}
+
+/*@ requires a < 0 ;
+ behavior B:
+ assumes a > 0 ;
+ assumes a < -42 ;
+*/
+void reqs_1_2_assumes(int a){}
+
+/*@ requires a >= 0 ;
+ behavior B:
+ assumes a > 10 ;
+ assumes a < 10 ;
+*/
+void reqs_combined_assumes(int a){}
+
+/*@ behavior B:
+ assumes a < 0 && a > 0 ; // not detected
+*/
+void only_assumes(int a){}
+
+/*@ behavior B:
+ assumes a > 0 ;
+ requires a < 0 ;
+*/
+void bhv_requires_assumes(int a){}
+
+/*@ requires a < 0 ;
+ behavior B1:
+ assumes a > 0 ;
+ behavior B2:
+ assumes a > 1 ;
+*/
+void reqs_massumes(int a){}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/doomed_pre.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/doomed_pre.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..fe70e5a3f43446af7c7f6dd0390d6eeccff8d88d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/doomed_pre.res.oracle
@@ -0,0 +1,113 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/doomed_pre.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function bhv_requires_assumes with behavior B
+------------------------------------------------------------
+
+Goal Wp_smoke_B_requires in 'bhv_requires_assumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_1_2_assumes
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'reqs_1_2_assumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: a < 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_1_2_assumes with behavior B
+------------------------------------------------------------
+
+Goal Wp_smoke_B_assumes in 'reqs_1_2_assumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_2_2_assumes
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'reqs_2_2_assumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: a < 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_2_2_assumes with behavior B
+------------------------------------------------------------
+
+Goal Wp_smoke_B_assumes in 'reqs_2_2_assumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_assumes
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'reqs_assumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: a < 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_assumes with behavior B
+------------------------------------------------------------
+
+Goal Wp_smoke_B_assumes in 'reqs_assumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_combined_assumes
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'reqs_combined_assumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: 0 <= a. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_combined_assumes with behavior B
+------------------------------------------------------------
+
+Goal Wp_smoke_B_assumes in 'reqs_combined_assumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_massumes
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'reqs_massumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: a < 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_massumes with behavior B1
+------------------------------------------------------------
+
+Goal Wp_smoke_B1_assumes in 'reqs_massumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_massumes with behavior B2
+------------------------------------------------------------
+
+Goal Wp_smoke_B2_assumes in 'reqs_massumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function requires
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'requires':
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..34eb51d822f54facf0cfd3de01835067da2b6867
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle
@@ -0,0 +1,47 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/doomed_pre.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 13 goals scheduled
+[wp] [Failed] Smoke-test typed_requires_wp_smoke_default_requires
+ Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:10: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_assumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_assumes_wp_smoke_B_assumes
+ Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:16: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_2_2_assumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_2_2_assumes_wp_smoke_B_assumes
+ Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:23: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_1_2_assumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_1_2_assumes_wp_smoke_B_assumes
+ Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:30: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_combined_assumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_combined_assumes_wp_smoke_B_assumes
+ Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:37: Warning: Failed smoke-test
+[wp] [Failed] Smoke-test typed_bhv_requires_assumes_wp_smoke_B_requires
+ Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:48: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_massumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_massumes_wp_smoke_B1_assumes
+ Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:56: Warning: Failed smoke-test
+[wp] [Failed] Smoke-test typed_reqs_massumes_wp_smoke_B2_assumes
+ Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:56: Warning: Failed smoke-test
+[wp] Proved goals: 5 / 13
+ Qed: 0 (failed: 8)
+ Alt-Ergo: 5
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ requires - - 1 0.0%
+ reqs_assumes - 1 2 50.0%
+ reqs_2_2_assumes - 1 2 50.0%
+ reqs_1_2_assumes - 1 2 50.0%
+ reqs_combined_assumes - 1 2 50.0%
+ bhv_requires_assumes - - 1 0.0%
+ reqs_massumes - 1 3 33.3%
+------------------------------------------------------------
diff --git a/src/plugins/wp/wpReached.ml b/src/plugins/wp/wpReached.ml
index a52a93aec86ddd0264d29bc6b2a270a4165bd2ae..fa15b385d0ef17ea8666aa2e1fc8b969b6d1867b 100644
--- a/src/plugins/wp/wpReached.ml
+++ b/src/plugins/wp/wpReached.ml
@@ -318,8 +318,45 @@ let reachability = FRmap.memo
(* --- Doome Status --- *)
(* -------------------------------------------------------------------------- *)
+module Invalid_behaviors = struct
+ module String_set = Datatype.String.Set
+
+ include State_builder.Hashtbl(Kernel_function.Hashtbl)(String_set)
+ (struct
+ let name = "Wp.WpReached.Invalid_behavior"
+ let dependencies = [Ast.self]
+ let size = 32
+ end)
+
+ let add kf bhv =
+ let set =
+ try find kf
+ with Not_found -> String_set.empty
+ in
+ add kf (String_set.add bhv.b_name set)
+
+ let mem kf bhv =
+ try String_set.mem bhv.b_name (find kf)
+ with Not_found -> false
+end
+
let set_invalid emitter tgt =
- Property_status.emit emitter ~hyps:[] tgt Property_status.False_if_reachable
+ let open Property_status in
+ match tgt with
+ (* For invalid assumes, introduce "ensures false" in behavior on need *)
+ | Property.IPPredicate { ip_kind = PKAssumes(bhv) ; ip_kf ; ip_pred } ->
+ if not (Invalid_behaviors.mem ip_kf bhv) then begin
+ Invalid_behaviors.add ip_kf bhv ;
+ let pred_name = [ "Wp" ; "SmokeTest" ] in
+ let pred_loc = ip_pred.ip_content.tp_statement.pred_loc in
+ let p = { Logic_const.pfalse with pred_loc ; pred_name } in
+ let p = Logic_const.(new_predicate p) in
+ let pid = Property.ip_of_ensures ip_kf Kglobal bhv (Normal, p) in
+ Annotations.add_ensures emitter ip_kf ~behavior:bhv.b_name [Normal, p];
+ emit emitter ~hyps:[] pid False_if_reachable
+ end
+ | p ->
+ emit emitter ~hyps:[] p False_if_reachable
let set_doomed emitter pid =
List.iter (set_invalid emitter) (WpPropId.doomed_if_valid pid) ;
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 00b5815d2cd892a51bd9ea4d3a27588998b47e0c..955cb0988ace3a74cf08f6add2c16d7b22aa778b 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -400,6 +400,13 @@ module SmokeTests =
let help = "Smoke-tests : look for inconsistent contracts (best effort)"
end)
+let () = Parameter_customize.set_group wp_strategy
+module SmokeDeadassumes =
+ True(struct
+ let option_name = "-wp-smoke-dead-assumes"
+ let help = "When generating smoke tests, look for dead assumes"
+ end)
+
let () = Parameter_customize.set_group wp_strategy
module SmokeDeadcode =
True(struct
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 2bb0a1fea14799a4fc2f5ed9cb40d536343baa8c..62fd4168df38dc8371a94a3dab6f3762e841ff69 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -153,6 +153,7 @@ module ReportName: Parameter_sig.String
module MemoryContext: Parameter_sig.Bool
module CheckMemoryContext: Parameter_sig.Bool
module SmokeTests: Parameter_sig.Bool
+module SmokeDeadassumes: Parameter_sig.Bool
module SmokeDeadloop: Parameter_sig.Bool
module SmokeDeadcode: Parameter_sig.Bool
module SmokeDeadcall: Parameter_sig.Bool