diff --git a/src/plugins/wp/tests/wp_plugin/doomed_unreach.i b/src/plugins/wp/tests/wp_plugin/doomed_unreach.i
new file mode 100644
index 0000000000000000000000000000000000000000..6327fad4ec08aa62ba356fd50696547c3400b4c9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/doomed_unreach.i
@@ -0,0 +1,24 @@
+/* run.config
+ DONTRUN:
+ */
+
+/* run.config_qualif
+ OPT: -wp-smoke-tests -wp-steps 100
+*/
+
+//@ assigns \result;
+int job(int x) {
+ switch(x) {
+ return 42;
+ case 0:
+ return 0;
+ case 1:
+ return 1;
+ x = 42;
+ return 42;
+ default:
+ return 3;
+ }
+ x = 42;
+ return 42;
+}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7140362d3548372aa5cbc7e8ff1bc89cf34acbf4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle
@@ -0,0 +1,21 @@
+# frama-c -wp -wp-steps 100 [...]
+[kernel] Parsing tests/wp_plugin/doomed_unreach.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] tests/wp_plugin/doomed_unreach.i:12: Warning: Failed smoke-test
+[wp] tests/wp_plugin/doomed_unreach.i:17: Warning: Failed smoke-test
+[wp] tests/wp_plugin/doomed_unreach.i:22: Warning: Failed smoke-test
+[wp] Warning: Missing RTE guards
+[wp] 6 goals scheduled
+[wp] [Passed] Smoke-test typed_job_wp_smoke_dead_code_s4
+[wp] [Passed] Smoke-test typed_job_wp_smoke_dead_code_s5
+[wp] [Passed] Smoke-test typed_job_wp_smoke_dead_code_s8
+[wp] [Qed] Goal typed_job_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job_assigns_part2 : Valid
+[wp] [Qed] Goal typed_job_assigns_part3 : Valid
+[wp] Proved goals: 6 / 9
+ Qed: 3
+ Alt-Ergo: 3
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ job 3 3 6 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index ad7739a514330aa32acee7cb455161c4541bd0a5..4a8f6ea3aeadb06a0fde85baa9c1bc075daec05b 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -1294,7 +1294,7 @@ class vexit kf acc =
Cil.DoChildren
end
-let process_unreached_annots cfg =
+let process_unreached_annots cfg reachability =
debug "collecting unreachable annotations@.";
let unreached = Cil2cfg.unreachable_nodes cfg in
let kf = Cil2cfg.cfg_kf cfg in
@@ -1311,7 +1311,15 @@ let process_unreached_annots cfg =
List.fold_left add_id acc (WpPropId.mk_code_annot_ids kf s a)
in
let do_stmt s acc =
- Annotations.fold_code_annot (do_annot s) s acc in
+ let acc =
+ match reachability with
+ | None -> acc
+ | Some r ->
+ if WpReached.smoking r s then
+ WpPropId.mk_smoke kf ~id:"unreachable" ~unreachable:s () :: acc
+ else acc
+ in Annotations.fold_code_annot (do_annot s) s acc
+ in
let do_node acc n =
debug
"process annotations of unreachable node %a@."
@@ -1364,7 +1372,7 @@ let build_configs assigns kf model behaviors ki property =
&& Wp_parameters.SmokeDeadcode.get ()
then Some (WpReached.reachability kf)
else None in
- process_unreached_annots cfg ;
+ process_unreached_annots cfg reachability ;
let def_annot_bhv, bhvs = find_behaviors kf cfg ki behaviors in
if bhvs <> [] then debug "[get_strategies] %d behaviors" (List.length bhvs);
let mk_bhv_config bhv = {
diff --git a/src/plugins/wp/wpReached.ml b/src/plugins/wp/wpReached.ml
index faa8f4fa17349e6af2a4f7fa3392ea0763f4018a..60fe40d175ef9651652217627cc829397fddd8c9 100644
--- a/src/plugins/wp/wpReached.ml
+++ b/src/plugins/wp/wpReached.ml
@@ -40,15 +40,20 @@ type node = {
id : int ;
mutable flow : flow ;
mutable prev : node list ;
- mutable reached : bool option ;
- mutable alive : bool option ;
+ mutable protected : bool option ;
+ (* whether the node is dominated by unreachable node or by a smoke test *)
+ mutable unreachable : bool option ;
+ (* whether the node is unreachable from the entry point *)
}
let kid = ref 0
let node () =
incr kid ;
- { id = !kid ; prev = [] ; alive = None ; reached = None ; flow = F_goto }
+ { id = !kid ; prev = [] ;
+ protected = None ;
+ unreachable = None ;
+ flow = F_goto }
(* -------------------------------------------------------------------------- *)
(* --- Unrolled Loop --- *)
@@ -175,46 +180,46 @@ and sequence env seq b = match seq with
(* --- Compute Reachability --- *)
(* -------------------------------------------------------------------------- *)
-let rec reached node =
- match node.reached with
+let rec unreachable node =
+ match node.unreachable with
| Some r -> r
| None ->
- node.reached <- Some true ; (* cut loops *)
+ node.unreachable <- Some true ; (* cut loops *)
let r =
match node.flow with
- | F_dead | F_entry -> true
+ | F_dead -> true
+ | F_entry -> false
| F_goto | F_effect | F_return | F_branch | F_call ->
- List.for_all reached_after node.prev
- in
- node.reached <- Some r ; r
-
-and reached_after node =
- match node.flow with
- | F_goto -> reached node
- | F_effect | F_entry | F_dead -> true
- | F_return | F_branch | F_call -> false
+ List.for_all unreachable node.prev
+ in node.unreachable <- Some r ; r
-let rec alive node =
- match node.alive with
- | Some a -> a
+let rec protected node =
+ match node.protected with
+ | Some r -> r
| None ->
- match node.flow with
- | F_dead -> false
- | F_entry -> true
- | _ ->
- node.alive <- Some false ;
- let a = List.exists alive node.prev in
- node.alive <- Some a ; a
+ node.protected <- Some false ; (* cut loops *)
+ let r =
+ match node.flow with
+ | F_dead | F_entry -> true
+ | F_goto | F_effect | F_return | F_branch | F_call ->
+ node.prev <> [] && List.for_all protected_by node.prev
+ in node.protected <- Some r ; r
+
+and protected_by prev =
+ match prev.flow with
+ | F_dead | F_entry | F_effect -> true
+ | F_goto -> protected prev
+ | F_call | F_branch | F_return -> unreachable prev
let smoking_node n =
match n.flow with
- | F_effect | F_call | F_return -> alive n && not (reached n)
+ | F_effect | F_call | F_return -> not (protected n)
| F_goto | F_branch | F_entry | F_dead -> false
(* returns true if the stmt requires a reachability smoke test *)
let smoking reachability stmt =
try Stmt.Map.find stmt reachability |> smoking_node
- with Not_found -> false
+ with Not_found -> true
let compute kf =
try
@@ -245,14 +250,10 @@ let dump ~dir kf reached =
N.define dot
(fun a na ->
let attr =
- if smoking_node a
- then [`Filled;`Fillcolor "orange"]
- else
- match a.flow with
- | F_entry | F_effect | F_return | F_call ->
- [`Filled;`Fillcolor "green"]
- | F_dead -> [`Filled;`Fillcolor "red"]
- | F_branch | F_goto -> []
+ if smoking_node a then [`Filled;`Fillcolor "orange"]
+ else if protected a then [`Filled;`Fillcolor "green"]
+ else if unreachable a then [`Filled;`Fillcolor "red"]
+ else []
in G.node dot na attr ;
List.iter
(fun b ->