[wp] stmt assertions

src/plugins/wp/cfgCalculus.ml

@@ -103,19 +103,21 @@ struct
     try
       env.ki <- Kstmt s ;
       Cil.CurrentLoc.set (Stmt.loc s) ;
-      let pi = M.label env.we (Some s) (Clabels.stmt s) (asserts env a s) in
+      let ca = WpAnnot.get_code_assertions env.kf s in
+      let pi =
+        M.label env.we (Some s) (Clabels.stmt s) @@
+        List.fold_right (M.add_goal env.we) ca.code_verified @@
+        List.fold_right (M.add_hyp env.we) ca.code_admitted @@
+        control env a s
+      in
       Cil.CurrentLoc.set kl ;
       env.ki <- ki ; pi
     with err ->
       Cil.CurrentLoc.set kl ;
       env.ki <- ki ; raise err
 
-  (* Consider assertions *)
-  and asserts env a (s: stmt) : M.t_prop =
-    (*TODO: apply code annots *) control env a s
-
   (* Branching wrt control-flow *)
-  and control env a (s: stmt) : M.t_prop =
+  and control env a s : M.t_prop =
     match s.skind with
     | Loop(_,_,_,_,_) ->
         loop env a s (WpAnnot.get_loop_contract env.kf s)

src/plugins/wp/wpAnnot.ml

@@ -188,6 +188,43 @@ let preconditions_at_call s = function
 let get_called_preconditions_at kf stmt =
   List.map snd (call_preconditions 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 ;
+}
+
+let get_code_assertions kf stmt : code_assertions =
+  let labels = NormAtLabels.labels_assert_before ~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
+      | AAssert(_,a) ->
+          let p =
+            WpPropId.mk_assert_id kf stmt ca ,
+            normalize_pred a.tp_statement
+          in if a.tp_only_check then {
+            l with code_admitted = p :: l.code_admitted ;
+          } else {
+            code_admitted = p :: l.code_admitted ;
+            code_verified = p :: l.code_verified ;
+          }
+      | _ -> l
+    end stmt {
+    code_admitted = [];
+    code_verified = [];
+  }
+
 (* -------------------------------------------------------------------------- *)
 (* --- Loop Invariants                                                    --- *)
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/wpAnnot.mli

@@ -63,6 +63,17 @@ val get_called_post_conditions : kernel_function -> Property.t list
 val get_called_exit_conditions : kernel_function -> Property.t list
 val get_called_assigns : kernel_function -> Property.t list
 
+(* -------------------------------------------------------------------------- *)
+(* --- Property Accessors : Assertions                                    --- *)
+(* -------------------------------------------------------------------------- *)
+
+type code_assertions = {
+  code_admitted: WpPropId.pred_info list ;
+  code_verified: WpPropId.pred_info list ;
+}
+
+val get_code_assertions : kernel_function -> stmt -> code_assertions
+
 (* -------------------------------------------------------------------------- *)
 (* --- Property Accessors : Loop Contracts                                --- *)
 (* -------------------------------------------------------------------------- *)