From 226fb4360a0b2404a40ea831feb7a05ca1b1552b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 8 Feb 2021 10:32:08 +0100
Subject: [PATCH] [wp] smoke deadcode
---
src/plugins/wp/cfgAnnot.ml | 10 +++++++++-
src/plugins/wp/cfgAnnot.mli | 4 +++-
src/plugins/wp/cfgCalculus.ml | 13 +++++++++++--
3 files changed, 23 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 4e1f02f1c98..c3e3836b467 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -305,7 +305,15 @@ module CodeAssertions = WpContext.StaticGenerator(CodeKey)
}
end)
-let get_code_assertions kf stmt = CodeAssertions.get (kf,stmt)
+let get_code_assertions ?smoking kf stmt =
+ let ca = CodeAssertions.get (kf,stmt) in
+ match smoking with
+ | None -> ca
+ | Some r ->
+ if WpReached.smoking r stmt then
+ let s = smoke kf ~id:"deadcode" ~unreachable:stmt () in
+ { ca with code_verified = s :: ca.code_verified }
+ else ca
(* -------------------------------------------------------------------------- *)
(* --- Loop Invariants --- *)
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index 8ca20ccbf96..5a06e3cb6dc 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -62,7 +62,9 @@ type code_assertions = {
code_verified: pred_info list ;
}
-val get_code_assertions : kernel_function -> stmt -> code_assertions
+val get_code_assertions :
+ ?smoking:WpReached.reachability ->
+ kernel_function -> stmt -> code_assertions
(* -------------------------------------------------------------------------- *)
(* --- Property Accessors : Loop Contracts --- *)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index fcee261c074..b9b2658183e 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -131,6 +131,7 @@ struct
props: props;
body: Cfg.automaton option;
succ: Cfg.vertex -> Cfg.G.edge list;
+ dead: WpReached.reachability option;
we: W.t_env;
wp: W.t_prop option Vhash.t; (* None is used for non-dag detection *)
mutable wk: W.t_prop; (* end point *)
@@ -197,7 +198,9 @@ struct
let kl = Cil.CurrentLoc.get () in
try
Cil.CurrentLoc.set (Stmt.loc s) ;
- let ca = CfgAnnot.get_code_assertions env.mode.kf s in
+ let smoking =
+ if is_default_bhv env.mode then env.dead else None in
+ let ca = CfgAnnot.get_code_assertions ?smoking env.mode.kf s in
let pi =
W.label env.we (Some s) (Clabels.stmt s) @@
List.fold_right (prove_property env) ca.code_verified @@
@@ -370,8 +373,14 @@ struct
let succ = match body with
| None -> (fun _ -> [])
| Some cfg -> Cfg.G.succ_e cfg.graph in
+ let dead =
+ if body <> None &&
+ is_default_bhv mode &&
+ WpLog.SmokeTests.get () &&
+ WpLog.SmokeDeadcall.get ()
+ then Some (WpReached.reachability kf) else None in
let env = {
- mode ; props ; body ; succ ;
+ mode ; props ; body ; succ ; dead ;
we = W.new_env kf ;
wp = Vhash.create 32 ;
wk = W.empty ;
--
GitLab