From 38df934084f1644ce7a2feabe0b0a8c74615feb6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Sat, 16 Jan 2021 13:24:04 +0100
Subject: [PATCH] [wp] stmt assertions
---
src/plugins/wp/cfgCalculus.ml | 14 +++++++------
src/plugins/wp/wpAnnot.ml | 37 +++++++++++++++++++++++++++++++++++
src/plugins/wp/wpAnnot.mli | 11 +++++++++++
3 files changed, 56 insertions(+), 6 deletions(-)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 650d4addff0..35ee2023a40 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 61871bf069d..88708e985e5 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 9f89597ed15..daaf415162e 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 --- *)
(* -------------------------------------------------------------------------- *)
--
GitLab