Commit 6a3af3b2 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] added post-effects to global assigns

parent de09f05c
......@@ -90,7 +90,7 @@ struct
(* Authorized written region from an assigns specification *)
type effect = {
e_pid : P.t ; (* Assign Property *)
e_kind : a_kind ; (* Requires post effects (in case of loop-assigns) *)
e_post : bool ; (* Requires post effects (loop-assigns or post-assigns) *)
e_label : c_label ; (* scope for collection *)
e_valid : L.sigma ; (* sigma where locations are filtered for validity *)
e_region : L.region ; (* expected from spec *)
......@@ -444,21 +444,23 @@ struct
ainfo.a_assigns
in match authorized_region with
| None -> None
| Some region -> Some {
e_pid = pid ;
e_kind = ainfo.a_kind ;
e_label = from ;
e_valid = sigma ;
e_region = region ;
e_warn = Warning.Set.empty ;
}
| Some region ->
let post = match ainfo.a_kind with
| LoopAssigns -> true
| StmtAssigns -> NormAtLabels.has_postassigns ainfo.a_assigns
in Some {
e_pid = pid ;
e_post = post ;
e_label = from ;
e_valid = sigma ;
e_region = region ;
e_warn = Warning.Set.empty ;
}
let cc_posteffect e vcs =
match e.e_kind with
| StmtAssigns -> vcs
| LoopAssigns ->
let vc = { empty_vc with vars = L.vars e.e_region } in
Gmap.add (Gposteffect e.e_pid) (Splitter.singleton vc) vcs
if not e.e_post then vcs else
let vc = { empty_vc with vars = L.vars e.e_region } in
Gmap.add (Gposteffect e.e_pid) (Splitter.singleton vc) vcs
(* -------------------------------------------------------------------------- *)
(* --- WP RULES : adding axioms, hypotheses and goals --- *)
......@@ -549,14 +551,13 @@ struct
vars = xs }
in
let group =
match e.e_kind with
| StmtAssigns ->
Splitter.singleton (setup empty_vc)
| LoopAssigns ->
try Splitter.map setup (Gmap.find (Gposteffect e.e_pid) vcs)
with Not_found ->
Wp_parameters.fatal "Missing post-effect for %a"
WpPropId.pretty e.e_pid
if not e.e_post then
Splitter.singleton (setup empty_vc)
else
try Splitter.map setup (Gmap.find (Gposteffect e.e_pid) vcs)
with Not_found ->
Wp_parameters.fatal "Missing post-effect for %a"
WpPropId.pretty e.e_pid
in
let target = match sloc with
| None -> Gprop e.e_pid
......
......@@ -74,6 +74,11 @@ let of_logic = function
| BuiltinLabel LoopEntry -> loopentry
| StmtLabel s -> stmt !s
let is_post = function
| BuiltinLabel Post -> true
| FormalLabel a -> a = post
| _ -> false
let name = function FormalLabel a -> a | _ -> ""
let lookup labels a =
......
......@@ -65,6 +65,9 @@ val of_logic : Cil_types.logic_label -> c_label
labels. Ambiguous labels are: Old, LoopEntry and LoopCurrent, since
they points to different program points dependending on the context. *)
val is_post : Cil_types.logic_label -> bool
(** Checks whether the logic-label is [Post] or [to_logic post] *)
val pretty : Format.formatter -> c_label -> unit
open Cil_types
......
......@@ -210,9 +210,27 @@ let preproc_assigns labels asgns =
let visitor = new norm_at labels in
List.map (Visitor.visitFramacFrom visitor) asgns
let has_postassigns = function
| WritesAny -> false
| Writes froms ->
let exception HAS_POST in
let visitor = new norm_at (fun l ->
if Clabels.is_post l then raise HAS_POST
else Clabels.of_logic l
) in
try
List.iter
(fun fr -> ignore @@ Visitor.visitFramacFrom visitor fr)
froms ;
false
with HAS_POST ->
true
let catch_label_error ex txt1 txt2 = match ex with
| LabelError lab ->
Wp_parameters.warning
"Unexpected label %a in %s : ignored %s"
Wp_error.pp_logic_label lab txt1 txt2
| _ -> raise ex
(* -------------------------------------------------------------------------- *)
......@@ -42,5 +42,5 @@ val labels_predicate : (logic_label * logic_label) list -> label_mapping
val labels_axiom : label_mapping
val preproc_annot : label_mapping -> predicate -> predicate
val preproc_assigns : label_mapping -> from list -> from list
val has_postassigns : assigns -> bool
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment