diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 650d4addff09bacba730d53ae3c99004d902be82..35ee2023a40f73d16f87affb2afd73fee50882b8 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/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)
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 61871bf069d504a52cac645d49a33b6dc8f7f6bf..88708e985e55d6cf6ab33d725109134b4894939b 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/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                                                    --- *)
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpAnnot.mli b/src/plugins/wp/wpAnnot.mli
index 9f89597ed15c39ac48ebc0878a959f01cffd061d..daaf415162ecef6133a28f23d20eaada8bf8f41c 100644
--- a/src/plugins/wp/wpAnnot.mli
+++ b/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                                --- *)
 (* -------------------------------------------------------------------------- *)