From 7b6417f4c3a6bd5e6f9894510f3674235a4a1f5f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 8 Feb 2021 15:08:56 +0100
Subject: [PATCH] [wp] dead-call smoke tests
---
src/plugins/wp/cfgAnnot.ml | 11 ++++++++++-
src/plugins/wp/cfgAnnot.mli | 2 +-
src/plugins/wp/cfgCalculus.ml | 7 ++++++-
src/plugins/wp/wpAnnot.ml | 2 +-
4 files changed, 18 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index c3e3836b467..3ed9641b471 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -259,7 +259,16 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
}
end)
-let get_call_contract = CallContract.get
+let get_call_contract ?smoking kf =
+ let cc = CallContract.get kf in
+ match smoking with
+ | None -> cc
+ | Some s ->
+ let g = smoke kf ~id:"dead_call" ~unreachable:s () in
+ { cc with
+ call_post = g :: cc.call_post ;
+ call_exit = g :: cc.call_exit ;
+ }
(* -------------------------------------------------------------------------- *)
(* --- Code Assertions --- *)
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index 5a06e3cb6dc..9ba615b4305 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -95,7 +95,7 @@ type call_contract = {
}
val get_precond_at : kernel_function -> stmt -> pred_info -> pred_info
-val get_call_contract : kernel_function -> call_contract
+val get_call_contract : ?smoking:stmt -> kernel_function -> call_contract
(* -------------------------------------------------------------------------- *)
(* --- Clear Tablesnts --- *)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index b9b2658183e..431b3df41f3 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -294,7 +294,12 @@ struct
W.use_assigns env.we None (WpPropId.mk_asm_assigns_desc s) w
and call env s r kf es wr : W.t_prop =
- let c = CfgAnnot.get_call_contract kf in
+ let smoking =
+ if is_default_bhv env.mode &&
+ WpLog.SmokeTests.get () &&
+ WpLog.SmokeDeadcall.get ()
+ then Some s else None in
+ let c = CfgAnnot.get_call_contract ?smoking kf in
let w_call = W.call env.we s r kf es
~pre:c.call_pre
~post:c.call_post
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index db7a24fa9c2..b25934771ab 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -657,7 +657,7 @@ let add_called_post called_kf termination_kind acc =
let add_call_checks config s kf posts exits =
if cur_fct_default_bhv config
&& Wp_parameters.SmokeTests.get ()
- && Wp_parameters.SmokeDeadcode.get ()
+ && Wp_parameters.SmokeDeadcall.get ()
then
WpStrategy.add_prop_dead_call kf s posts exits
else
--
GitLab