Module Calculus.Cfg.R

module R: sig .. end
to store the results of computations : we store a result for each edge, and also a list of proof obligations.

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 : t_mode;
   cfg : Cil2cfg.t;
   tbl : HE.t;
   mutable memo : LabObligs.t;
   mutable obligs : LabObligs.t;
}
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
If needed, clear wp table to compute Pass2. If nothing has been stored in res.memo, there is nothing to do.
val set : WpStrategy.strategy ->
W.t_env -> t -> Cil2cfg.edge -> W.t_prop -> W.t_prop
store the result p for the computation of the edge e.