From 93cbc74b893cb0d83859c79ad20fb428d3ae197f Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 15 Jun 2021 13:45:40 +0200
Subject: [PATCH] [wp] MemVal compilable with current WP
---
src/plugins/reduc/collect.ml | 5 +++--
src/plugins/reduc/hyp.ml | 4 ++--
src/plugins/reduc/misc.ml | 2 +-
src/plugins/reduc/value2acsl.ml | 6 +++---
src/plugins/wp/MemDebug.ml | 6 ++++++
src/plugins/wp/MemVal.ml | 14 ++++++++++----
src/plugins/wp/MemValue.ml | 10 ++++++++--
7 files changed, 33 insertions(+), 14 deletions(-)
diff --git a/src/plugins/reduc/collect.ml b/src/plugins/reduc/collect.ml
index fab5f06acf1..e428f3ec29c 100644
--- a/src/plugins/reduc/collect.ml
+++ b/src/plugins/reduc/collect.ml
@@ -61,13 +61,14 @@ end
let rec collect_off typ =
match typ with
| TInt _ | TFloat _ -> [ NoOffset ]
- | TComp ({cfields = flds}, _, _) ->
+ | TComp ({cfields = Some flds}, _, _) ->
List.fold_left collect_fields [] flds
| TArray (arrtyp, e_opt, _, _) ->
debug "Array of length %a" (Pretty_utils.pp_opt Printer.pp_exp) e_opt;
begin try collect_array arrtyp [] (Cil.lenOfArray64 e_opt)
with Cil.LenOfArray -> [] end
- | TVoid _ | TFun _ | TPtr _ | TEnum _ | TNamed _ | TBuiltin_va_list _ -> []
+ | TVoid _ | TFun _ | TPtr _ | TEnum _ | TNamed _ | TBuiltin_va_list _
+ | TComp ({cfields = None}, _, _)-> []
and collect_fields acc fld =
let offs = collect_off fld.ftype in
diff --git a/src/plugins/reduc/hyp.ml b/src/plugins/reduc/hyp.ml
index cb17a0d5271..85f9a88dd4f 100644
--- a/src/plugins/reduc/hyp.ml
+++ b/src/plugins/reduc/hyp.ml
@@ -13,14 +13,14 @@ class hypotheses_visitor (env: Collect.env) = object(self)
inherit Visitor.generic_frama_c_visitor (Visitor_behavior.inplace ())
method! vstmt_aux stmt =
- let kf = Extlib.the (self#current_kf) in
+ let kf = Option.get (self#current_kf) in
let state = Db.Value.get_stmt_state stmt in
if Collect.should_annotate_stmt env stmt then begin
let vars = Collect.get_relevant_vars_stmt env kf stmt in
List.iter
(fun e ->
let p_opt = pred_opt_from_expr_state state e in
- Extlib.may (Misc.assert_and_validate ~kf stmt) p_opt)
+ Option.iter (Misc.assert_and_validate ~kf stmt) p_opt)
vars
end;
Cil.DoChildren
diff --git a/src/plugins/reduc/misc.ml b/src/plugins/reduc/misc.ml
index 061e0f5d614..79239e1e09c 100644
--- a/src/plugins/reduc/misc.ml
+++ b/src/plugins/reduc/misc.ml
@@ -23,7 +23,7 @@ let validate_ip ip =
Property_status.emit emitter ~hyps:[] ip Property_status.True
let assert_and_validate ~kf stmt p =
- let p = { tp_only_check = false; tp_statement = p } in
+ let p = { tp_kind = Assert ; tp_statement = p } in
let annot = Logic_const.new_code_annotation (AAssert([], p)) in
Annotations.add_code_annot emitter ~kf stmt annot ;
List.iter
diff --git a/src/plugins/reduc/value2acsl.ml b/src/plugins/reduc/value2acsl.ml
index 637948a5c14..21aff431c32 100644
--- a/src/plugins/reduc/value2acsl.ml
+++ b/src/plugins/reduc/value2acsl.ml
@@ -31,8 +31,8 @@ let interval_to_predicate_opt ~loc te min max =
Extlib.merge_opt
(fun _ pmin pmax -> Logic_const.pand ~loc (pmin, pmax))
()
- (Extlib.opt_map min_predicate min)
- (Extlib.opt_map max_predicate max)
+ (Option.map min_predicate min)
+ (Option.map max_predicate max)
(* [congruence_to_predicate_opt ~loc te rem modulo] may create a congruence
predicate where [te] mod [modulo] equals [rem] *)
@@ -126,7 +126,7 @@ let base_offset_to_predicate ~loc t b o =
let _base_offsets_to_predicate ~loc t (m: Cvalue.V.M.t) =
let aux b o (acc: predicate list) =
let p_opt = base_offset_to_predicate ~loc t b o in
- (Extlib.list_of_opt p_opt) @ acc
+ (Option.to_list p_opt) @ acc
in
match Cvalue.V.M.fold aux m [] with
| [] -> None
diff --git a/src/plugins/wp/MemDebug.ml b/src/plugins/wp/MemDebug.ml
index 66ba6046881..2ac81532b37 100644
--- a/src/plugins/wp/MemDebug.ml
+++ b/src/plugins/wp/MemDebug.ml
@@ -193,6 +193,8 @@ struct
Sigma.pretty s Ctypes.pretty obj pretty l (pp_value pretty) v;
v
+ let load_init _s _obj _l = e_false
+
let stored seq obj l t =
let preds = M.stored seq obj l t in
debug_access "@[stored %a@, %a@, %a@, %a ->@, %a@]@."
@@ -200,6 +202,8 @@ struct
(Pretty_utils.pp_list pp_equation) preds;
preds
+ let stored_init _seq _obj _l _v = []
+
let copied seq obj ll rl =
let preds = M.copied seq obj ll rl in
debug_access "@[copied %a@, %a@, %a@, %a ->@, %a@]@."
@@ -207,6 +211,8 @@ struct
(Pretty_utils.pp_list pp_equation) preds;
preds
+ let copied_init _seq _obj _ll _rl = []
+
let assigned seq obj sloc =
let preds = M.assigned seq obj sloc in
debug_access "@[assigned %a@, %a@, %a ->@, %a@]@."
diff --git a/src/plugins/wp/MemVal.ml b/src/plugins/wp/MemVal.ml
index 54e318eb17e..950f0518a5d 100644
--- a/src/plugins/wp/MemVal.ml
+++ b/src/plugins/wp/MemVal.ml
@@ -209,7 +209,7 @@ struct
let datatype = "MemVal." ^ V.datatype
let configure () =
let rollback = V.configure () in
- let orig_pointer = Context.push Lang.pointer (fun _typ -> t_addr) in
+ let orig_pointer = Context.push Lang.pointer t_addr in
let rollback () =
rollback ();
Context.pop Lang.pointer orig_pointer;
@@ -384,7 +384,7 @@ struct
* F.set_builtin_2 f_rd (phi_read ~obj ~read:f_rd ~write:f_wr)
* end; *)
Definitions.define_lemma {
- l_kind = `Axiom;
+ l_kind = Cil_types.Admit;
l_name = name; l_types = 0;
l_triggers = [];
l_forall = [xw; xo; xv];
@@ -413,7 +413,7 @@ struct
in
let cluster = cluster () in
Definitions.define_lemma {
- l_kind = `Axiom;
+ l_kind = Cil_types.Admit;
l_name = name; l_types = 0;
l_triggers = [];
l_forall = [xw; xwo; xro; xv];
@@ -564,6 +564,8 @@ struct
| _ -> load_loc ~assume:false sigma obj l
end
+ let load_init _sigma _obj _loc = e_false
+
(* -------------------------------------------------------------------------- *)
(* --- Memory Store --- *)
(* -------------------------------------------------------------------------- *)
@@ -587,6 +589,8 @@ struct
in
store [ ] (V.domain l.loc_v)
+ let stored_init _seq _obj _loc _t = []
+
let copied seq obj ll lr =
let v = match load seq.pre obj lr with
| Sigs.Val v -> v
@@ -594,6 +598,8 @@ struct
in
stored seq obj ll v
+ let copied_init _seq _obj _ll _lr = []
+
let assigned _s _obj _sloc = [ Assert F.p_true ]
@@ -634,7 +640,7 @@ struct
LOC (la, n)
| Rrange (l, obj, a_opt, b_opt) ->
let f = F.e_fact (Ctypes.sizeof_object obj) in
- RANGE (l, Vset.range (Extlib.opt_map f a_opt) (Extlib.opt_map f b_opt))
+ RANGE (l, Vset.range (Option.map f a_opt) (Option.map f b_opt))
(* -------------------------------------------------------------------------- *)
(* --- Validity --- *)
diff --git a/src/plugins/wp/MemValue.ml b/src/plugins/wp/MemValue.ml
index fb301c91c31..5ef0165be8e 100644
--- a/src/plugins/wp/MemValue.ml
+++ b/src/plugins/wp/MemValue.ml
@@ -218,7 +218,7 @@ let configure () =
if not (Db.Value.is_computed ()) then
Warning.error ~source:"Value Model"
"A previous Value analysis is needed by this memory model.";
- let orig_pointer = Context.push Lang.pointer (fun _ -> t_addr) in
+ let orig_pointer = Context.push Lang.pointer t_addr in
let rollback () =
Context.pop Lang.pointer orig_pointer;
in
@@ -309,7 +309,7 @@ module TermV = WpContext.Generator(Value)
| [] -> ()
| bs ->
Definitions.define_lemma {
- l_kind = `Axiom;
+ l_kind = Cil_types.Admit;
l_name = name; l_types = 0; l_triggers = []; l_forall = [];
l_lemma = lemma bs;
l_cluster = cluster_dummy ();
@@ -573,6 +573,8 @@ let load sigma obj l = match load sigma obj l with
Ctypes.pp_object obj pretty l pretty l';
v
+let load_init _sgima _obj _l = e_false
+
(* -------------------------------------------------------------------------- *)
(* --- Memory Store --- *)
(* -------------------------------------------------------------------------- *)
@@ -605,10 +607,14 @@ let stored : sigma sequence -> c_object -> loc -> term -> equation list = fun se
| C_pointer _ -> stored seq obj l e
| _ -> not_yet_obj obj
+let stored_init _seq _obj _l _v = []
+
let copied : sigma sequence -> c_object -> loc -> loc -> equation list = fun seq obj ll lr ->
debug_flow "copied";
stored seq obj ll (loadvalue seq.pre obj lr)
+let copied_init _seq _obj _ll _rl = []
+
let assigned : sigma sequence -> c_object -> loc sloc -> equation list = fun _ _ _ ->
debug_flow "assigned";
[ Assert F.p_true ]
--
GitLab