[wp] fix internal doc of smoke-tests

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                                                    --- *)

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 =

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) ;

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