[wp] Weaken code assertions + move smoke tests

- A1 A2 ... : prove A1 -> hyp A1 -> prove A2 -> hyp A2 ...
- Move smoke tests to the end of code assertions

src/plugins/wp/cfgAnnot.ml

@@ -410,25 +410,20 @@ let get_stmt_assigns kf stmt =
 (* --- Code Assertions                                                    --- *)
 (* -------------------------------------------------------------------------- *)
 
-type code_assertions = {
-  code_admitted: WpPropId.pred_info list ;
-  code_verified: WpPropId.pred_info list ;
-}
-
-let reverse_code_assertions a = {
-  code_admitted = List.rev a.code_admitted ;
-  code_verified = List.rev a.code_verified ;
+type code_assertion = {
+  code_admitted: WpPropId.pred_info option ;
+  code_verified: WpPropId.pred_info option ;
 }
 
+(* Note: generated in REVERSE order *)
 module CodeAssertions = WpContext.StaticGenerator(CodeKey)
     (struct
       type key = CodeKey.t
-      type data = code_assertions
+      type data = code_assertion list
       let name = "Wp.CfgAnnot.CodeAssertions"
       let compile (kf,stmt) =
         let labels = NormAtLabels.labels_assert ~kf stmt in
         let normalize_pred p = NormAtLabels.preproc_annot labels p in
-        reverse_code_assertions @@
         Annotations.fold_code_annot
           begin fun _emitter ca l ->
             match ca.annot_content with
@@ -446,23 +441,23 @@ module CodeAssertions = WpContext.StaticGenerator(CodeKey)
                   normalize_pred a.tp_statement in
                 let admit = Logic_utils.use_predicate a.tp_kind in
                 let verif = Logic_utils.verify_predicate a.tp_kind in
-                let use flag p ps = if flag then p::ps else ps in
+                let use flag p = if flag then Some p else None in
                 {
-                  code_admitted = use admit p l.code_admitted ;
-                  code_verified = use verif p l.code_verified ;
-                }
+                  code_admitted = use admit p ;
+                  code_verified = use verif p ;
+                } :: l
             | _ -> l
-          end stmt {
-          code_admitted = [];
-          code_verified = [];
-        }
+          end stmt []
     end)
 
 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
+     assertions associated to this statement, in particular RTE assertions.   *)
+  List.rev @@
   if smoking then
     let s = smoke kf ~id:"dead_code" ~unreachable:stmt () in
-    { ca with code_verified = s :: ca.code_verified }
+    { code_admitted = None ; code_verified = Some s } :: ca
   else ca
 
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/cfgAnnot.mli

@@ -63,13 +63,13 @@ val get_decreases_goal : kernel_function -> variant_info option
 (* --- Property Accessors : Assertions                                    --- *)
 (* -------------------------------------------------------------------------- *)
 
-type code_assertions = {
-  code_admitted: pred_info list ;
-  code_verified: pred_info list ;
+type code_assertion = {
+  code_admitted: pred_info option ;
+  code_verified: pred_info option ;
 }
 
 val get_code_assertions :
-  ?smoking:bool -> kernel_function -> stmt -> code_assertions
+  ?smoking:bool -> kernel_function -> stmt -> code_assertion list
 
 val get_unreachable : kernel_function -> stmt -> prop_id
 val get_stmt_assigns : kernel_function -> stmt -> assigns_full_info list

src/plugins/wp/cfgCalculus.ml

@@ -221,11 +221,15 @@ struct
       Cil.CurrentLoc.set (Stmt.loc s) ;
       let smoking =
         is_default_bhv env.mode && env.dead s in
-      let ca = CfgAnnot.get_code_assertions ~smoking env.mode.kf s in
+      let cas = CfgAnnot.get_code_assertions ~smoking env.mode.kf s in
+      let opt_fold f = Option.fold ~none:Extlib.id ~some:f in
+      let do_assert env CfgAnnot.{ code_admitted ; code_verified } w =
+        opt_fold (prove_property env) code_verified @@
+        opt_fold (use_property env) code_admitted w
+      in
       let pi =
         W.label env.we (Some s) (Clabels.stmt s) @@
-        List.fold_right (prove_property env) ca.code_verified @@
-        List.fold_right (use_property env) ca.code_admitted @@
+        List.fold_right (do_assert env) cas @@
         control env a s
       in
       Cil.CurrentLoc.set kl ; pi

src/plugins/wp/cfgInfos.ml

@@ -449,8 +449,10 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
            let fs = collect_calls ~bhv kf stmt in
            let nv_loops, term_deps = collect_loops_no_variant kf stmt in
            let dead = unreachable infos src in
-           let ca = CfgAnnot.get_code_assertions kf stmt in
-           let ca_pids = List.map fst ca.code_verified in
+           let cas = CfgAnnot.get_code_assertions kf stmt in
+           let ca_pids =
+             Extlib.filter_map_opt
+               (fun CfgAnnot.{ code_verified=ca } -> Option.map fst ca) cas in
            let loop_pids = loop_contract_pids kf stmt in
            if dead then
              begin

src/plugins/wp/tests/wp/oracle/bug_rte.res.oracle

@@ -7,7 +7,11 @@
 ------------------------------------------------------------
 
 Goal Assertion 'rte,signed_overflow' (file bug_rte.i, line 7):
-Assume { Type: is_sint32(i) /\ is_sint32(j). }
+Assume {
+  Type: is_sint32(i) /\ is_sint32(j).
+  (* Assertion 'rte,signed_overflow' *)
+  Have: i <= (2147483647 + (if (j = 1) then 1 else 0)).
+}
 Prove: if (j = 1) then ((-2147483647) <= i) else ((-2147483648) <= i).
 
 ------------------------------------------------------------