module R:sig
..end
Be careful that there are two modes of computation :
the first one (Pass1
) is used to prove the establishment of properties
while the second (after change_mode_if_needed
) prove the preservation.
See Calculus.Cfg.R.set
for more details.
type
t = {
|
mutable mode : |
|
cfg : |
|
tbl : |
|
mutable memo : |
|
mutable obligs : |
val empty : Cil2cfg.t -> t
val is_pass1 : t -> bool
val add_oblig : t -> Clabels.c_label -> W.t_prop -> unit
val add_memo : t -> Cil2cfg.edge -> W.t_prop -> unit
val find : t -> Cil2cfg.edge -> W.t_prop
val change_mode_if_needed : t -> unit
val set : WpStrategy.strategy ->
W.t_env -> t -> Cil2cfg.edge -> W.t_prop -> W.t_prop
H => [ BG /\ (BH => (G /\ P)) ]