From 4ce59bc9dd6f42a75debbccb68a40c15897beb47 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 27 Mar 2023 09:20:05 +0200
Subject: [PATCH] [wp] fix internal doc of smoke-tests
---
src/plugins/wp/cfgAnnot.ml | 18 ++++++++++--------
src/plugins/wp/cfgCalculus.ml | 3 +--
src/plugins/wp/cfgInfos.ml | 7 ++++---
src/plugins/wp/wpReached.ml | 4 ++--
4 files changed, 17 insertions(+), 15 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index b06baf97c1c..1e6485daec5 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -464,7 +464,7 @@ module CodeAssertions = WpContext.StaticGenerator(CodeKey)
let get_code_assertions ?(smoking=false) kf stmt =
let ca = CodeAssertions.get (kf,stmt) in
- (* Make sur that smoke tests are in the end so that it can see surely false
+ (* Make sure that smoke tests are in the end so that it can see surely false
assertions associated to this statement, in particular RTE assertions. *)
List.rev @@
if smoking then
@@ -607,20 +607,22 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
end)
let get_loop_contract ?(smoking=false) ?terminates kf stmt =
+ (* Loop Contract *)
let lc = LoopContract.get (kf,stmt) in
- let lc_smoke = if smoking && not (WpReached.is_dead_code stmt) then
+ (* Loop Smoking *)
+ let lc =
+ if smoking && not (WpReached.is_dead_code stmt) then
let g = smoke kf ~id:"dead_loop" ~unreachable:stmt () in
{ lc with loop_smoke = g :: lc.loop_smoke }
else lc
in
- match lc_smoke.loop_terminates, terminates with
- | None, _ ->
- lc_smoke
- | Some _, None ->
- { lc_smoke with loop_terminates = None }
+ (* Loop Termination *)
+ match lc.loop_terminates, terminates with
+ | None, _ -> lc
+ | Some _, None -> { lc with loop_terminates = None }
| Some loop_terminates, Some terminates ->
let prop = Logic_const.pimplies(terminates, loop_terminates) in
- { lc_smoke with loop_terminates = Some prop }
+ { lc with loop_terminates = Some prop }
(* -------------------------------------------------------------------------- *)
(* --- Clear Tablesnts --- *)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index a57a8c1c069..d5c81fc3a8f 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -219,8 +219,7 @@ struct
let kl = Cil.CurrentLoc.get () in
try
Cil.CurrentLoc.set (Stmt.loc s) ;
- let smoking =
- is_default_bhv env.mode && env.dead s in
+ let smoking = is_default_bhv env.mode && env.dead s in
let cas = CfgAnnot.get_code_assertions ~smoking env.mode.kf s in
let opt_fold f = Option.fold ~none:Fun.id ~some:f in
let do_assert env CfgAnnot.{ code_admitted ; code_verified } w =
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index a24e5e48c2e..b2da833c128 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -52,10 +52,11 @@ let calls infos = infos.calls
let annots infos = infos.annots
let doomed infos = infos.doomed
-let wpreached s = function
+let wp_reached_smoking s = function
| None -> false
| Some reachability -> WpReached.smoking reachability s
-let smoking infos s = wpreached s infos.reachability
+
+let smoking infos s = wp_reached_smoking s infos.reachability
let unreachable infos v =
match infos.body, infos.checkpath with
@@ -457,7 +458,7 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
let loop_pids = loop_contract_pids kf stmt in
if dead then
begin
- if wpreached stmt reachability then
+ if wp_reached_smoking stmt reachability then
(let p = CfgAnnot.get_unreachable kf stmt in
infos.doomed <- Bag.append infos.doomed p) ;
infos.doomed <- Bag.concat infos.doomed (Bag.list ca_pids) ;
diff --git a/src/plugins/wp/wpReached.ml b/src/plugins/wp/wpReached.ml
index d797a9f0479..0193f2e4630 100644
--- a/src/plugins/wp/wpReached.ml
+++ b/src/plugins/wp/wpReached.ml
@@ -211,9 +211,9 @@ let rec protected node =
and protected_by prev =
match prev.flow with
- | F_dead | F_entry | F_effect -> true
+ | F_return | F_dead | F_entry | F_effect -> true
| F_goto -> protected prev
- | F_call | F_branch | F_return -> unreachable prev
+ | F_call | F_branch -> unreachable prev
let smoking_node n =
match n.flow with
--
GitLab