Functor CfgWP.VC

module VC: 
functor (M : Memory.Model) -> sig .. end
Parameters:
M : Memory.Model

module V: Lang.F.Vars
module P: WpPropId.PropId
module C: CodeSemantics.Make(M)
module L: LogicSemantics.Make(M)
module A: LogicAssigns.Make(M)(C)(L)
type target = 
| Gprop of P.t
| Geffect of P.t * Cil_datatype.Stmt.t * WpPropId.effect_source
| Gposteffect of P.t
module TARGET: sig .. end
type effect = {
   e_pid : P.t;
   e_kind : WpPropId.a_kind;
   e_label : Clabels.c_label;
   e_valid : L.sigma;
   e_region : A.region;
   e_warn : Warning.Set.t;
}
module EFFECT: sig .. end
module G: Qed.Collection.Make(TARGET)
module W: Warning.Set
module D: Property.Set
module S: Cil_datatype.Stmt.Set
module Eset: FCSet.Make(EFFECT)
module Gset: G.Set
module Gmap: G.Map
type vc = {
   hyps : Conditions.bundle;
   goal : Lang.F.pred;
   vars : Lang.F.Vars.t;
   warn : W.t;
   deps : D.t;
   path : S.t;
}
type t_env = {
   frame : L.frame;
   main : L.env;
}
type t_prop = {
   sigma : L.sigma option;
   effects : Eset.t;
   vcs : vc Splitter.t Gmap.t;
}
val pp_vc : Format.formatter -> vc -> unit
val pp_vcs : Format.formatter -> vc Splitter.t -> unit
val pp_gvcs : Format.formatter -> vc Splitter.t Gmap.t -> unit
val pretty : Format.formatter -> t_prop -> unit
val empty_vc : vc
val sigma_opt : M.Sigma.t option -> M.Sigma.t
val sigma_at : t_prop -> L.sigma
val sigma_any : call:bool -> t_prop -> M.Sigma.t
val sigma_union : M.Sigma.t option -> M.Sigma.t option -> M.Sigma.t * Passive.t * Passive.t
val merge_sigma : M.Sigma.t option ->
M.Sigma.t option -> M.Sigma.t option * Passive.t * Passive.t
val join_with : M.Sigma.t -> M.Sigma.t option -> Passive.t
val occurs_vc : vc -> Lang.F.Vars.elt -> bool
val intersect_vc : vc -> Lang.F.pred -> bool
val assume_vc : descr:string ->
?hpid:WpPropId.prop_id ->
?stmt:S.elt ->
?warn:Warning.Set.t -> Lang.F.pred list -> vc -> vc
val passify_vc : Passive.t -> vc -> vc
val branch_vc : stmt:Cil_types.stmt ->
Lang.F.pred -> vc -> vc -> vc
val merge_vc : vc -> vc -> vc
val merge_vcs : vc list -> vc
val gmerge : vc Splitter.t Gmap.t ->
vc Splitter.t Gmap.t ->
vc Splitter.t Gmap.t
val gmap : ('a -> 'b) -> 'a Splitter.t Gmap.t -> 'b Splitter.t Gmap.t
val gbranch : left:('a -> 'b) ->
both:('a -> 'c -> 'b) ->
right:('c -> 'b) ->
'a Splitter.t Gmap.t ->
'c Splitter.t Gmap.t -> 'b Splitter.t Gmap.t
val merge_all_vcs : vc Splitter.t Gmap.t list ->
vc Splitter.t Gmap.t
val empty : t_prop
val merge : t_env -> t_prop -> t_prop -> t_prop
val new_env : ?lvars:Cil_types.logic_var list ->
Cil_types.kernel_function -> t_env
val in_wenv : t_env ->
t_prop -> (L.env -> t_prop -> 'a) -> 'a
val intros : Lang.F.pred list -> Lang.F.pred -> Lang.F.pred list * Lang.F.pred
val introduction : Lang.F.pred -> Lang.F.Vars.t * Lang.F.pred list * Lang.F.pred
val add_vc : Gmap.key ->
?warn:W.t ->
Lang.F.pred ->
vc Splitter.t Gmap.t ->
vc Splitter.t Gmap.t
val cc_effect : L.env ->
P.t -> WpPropId.assigns_desc -> effect option
val cc_posteffect : effect ->
vc Splitter.t Gmap.t ->
vc Splitter.t Gmap.t
val add_axiom : 'a -> 'b -> unit
val add_hyp : t_env ->
WpPropId.prop_id * Cil_types.predicate Cil_types.named ->
t_prop -> t_prop
val add_goal : t_env ->
P.t * Cil_types.predicate Cil_types.named ->
t_prop -> t_prop
val add_assigns : t_env ->
P.t * WpPropId.assigns_desc -> t_prop -> t_prop
val add_warnings : W.t ->
vc Splitter.t Gmap.t ->
vc Splitter.t Gmap.t
val assigns_condition : A.region -> effect -> Lang.F.pred
exception COLLECTED
val is_collected : 'a Splitter.t Gmap.t -> P.t -> bool
val check_nothing : Eset.t ->
vc Splitter.t Gmap.t ->
vc Splitter.t Gmap.t
val check_assigns : Cil_datatype.Stmt.t option ->
WpPropId.effect_source ->
?warn:Warning.Set.t ->
A.region ->
Eset.t ->
vc Splitter.t Gmap.t ->
vc Splitter.t Gmap.t
val do_assigns : descr:string ->
?stmt:Cil_datatype.Stmt.t ->
source:WpPropId.effect_source ->
?hpid:WpPropId.prop_id ->
?warn:Warning.Set.t ->
M.sigma Memory.sequence ->
A.region ->
Eset.t ->
vc Splitter.t Gmap.t ->
vc Splitter.t Gmap.t
val do_assigns_everything : ?stmt:Cil_datatype.Stmt.t ->
?warn:W.t ->
Eset.t ->
vc Splitter.t Gmap.t ->
vc Splitter.t Gmap.t
val cc_assigned : L.env ->
WpPropId.a_kind ->
Cil_types.identified_term Cil_types.from list ->
L.sigma Memory.sequence * (Ctypes.c_object * L.region) list
val use_assigns : t_env ->
Cil_datatype.Stmt.t option ->
WpPropId.prop_id option ->
WpPropId.assigns_desc -> t_prop -> t_prop
val is_stopeffect : Clabels.c_label -> effect -> bool
val not_posteffect : Eset.t -> target -> 'a -> bool
val label : t_env -> Clabels.c_label -> t_prop -> t_prop
val cc_lval : L.env ->
Cil_types.lval ->
Ctypes.c_object * M.Heap.set * L.sigma Memory.sequence *
C.loc
val cc_stored : M.sigma Memory.sequence ->
M.loc -> Ctypes.c_object -> Cil_types.exp -> Lang.F.pred list
val assign : t_env ->
Cil_datatype.Stmt.t ->
Cil_types.lval -> Cil_types.exp -> t_prop -> t_prop
val return : t_env ->
S.elt -> Cil_types.exp option -> t_prop -> t_prop
val condition : descr:string ->
?stmt:S.elt ->
?warn:Warning.Set.t ->
Passive.t -> Lang.F.pred list -> vc -> vc
val mark : Splitter.tag -> vc Splitter.t option -> vc Splitter.t
val random : unit -> Lang.F.pred
val pp_opt : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a option -> unit
val test : t_env ->
S.elt ->
Cil_types.exp -> t_prop -> t_prop -> t_prop
val cc_case_values : int64 list ->
Lang.F.term list ->
C.sigma -> Cil_types.exp list -> int64 list * Lang.F.term list
val cc_group_case : S.elt ->
Warning.Set.t ->
string ->
Splitter.tag ->
Passive.t ->
Lang.F.pred list ->
vc Splitter.t Gmap.t ->
vc Splitter.t Gmap.t
val cc_case : S.elt ->
Warning.Set.t ->
C.sigma ->
Lang.F.term ->
Cil_types.exp list * t_prop ->
Lang.F.term list * vc Splitter.t Gmap.t
val cc_default : S.elt ->
M.Sigma.t ->
Lang.F.pred list -> t_prop -> vc Splitter.t Gmap.t
val switch : t_env ->
S.elt ->
Cil_types.exp ->
(Cil_types.exp list * t_prop) list ->
t_prop -> t_prop
val init_value : t_env ->
Cil_types.lval ->
Cil_types.typ -> Cil_types.exp option -> t_prop -> t_prop
val init_range : t_env ->
Cil_types.lval ->
Cil_types.typ -> int64 -> int64 -> t_prop -> t_prop
val loop_step : 'a -> 'a
val loop_entry : 'a -> 'a
val call_instances : C.sigma ->
P.t ->
Cil_types.exp ->
Cil_types.kernel_function list ->
vc Splitter.t Gmap.t ->
vc Splitter.t Gmap.t
val call_contract : S.elt ->
M.Sigma.t ->
(Warning.Set.t * C.loc) option ->
Kernel_function.t * t_prop -> vc Splitter.t Gmap.t
val call_dynamic : t_env ->
S.elt ->
P.t ->
Cil_types.exp ->
(Kernel_function.t * t_prop) list -> t_prop
val call_goal_precond : t_env ->
'a ->
Cil_types.kernel_function ->
Cil_types.exp list ->
pre:(P.t * Cil_types.predicate Cil_types.named) list ->
t_prop -> t_prop
type callenv = {
   sigma_pre : M.sigma;
   seq_post : M.sigma Memory.sequence;
   seq_exit : M.sigma Memory.sequence;
   seq_result : M.sigma Memory.sequence;
   loc_result : (Cil_types.typ * Ctypes.c_object * M.loc) option;
   frame_pre : L.frame;
   frame_post : L.frame;
   frame_exit : L.frame;
}
val cc_result_domain : Cil_types.lval option -> M.Heap.Set.t option
val cc_call_domain : L.env ->
Cil_types.kernel_function ->
Cil_types.exp list ->
Cil_types.identified_term Cil_types.assigns -> M.Heap.set option
val cc_havoc : M.Sigma.domain option -> M.Sigma.t -> M.Sigma.t Memory.sequence
val cc_callenv : L.env ->
Cil_types.lval option ->
Cil_types.kernel_function ->
Cil_types.exp list ->
Cil_types.identified_term Cil_types.assigns ->
t_prop -> t_prop -> callenv
type call_vcs = {
   vcs_post : vc Splitter.t Gmap.t;
   vcs_exit : vc Splitter.t Gmap.t;
}
val cc_call_effects : Cil_datatype.Stmt.t ->
callenv ->
L.env ->
Cil_types.identified_term Cil_types.assigns ->
t_prop -> t_prop -> call_vcs
val cc_contract_hyp : L.frame ->
L.env ->
('a * Cil_types.predicate Cil_types.named) list -> Lang.F.pred list
val cc_result : callenv -> Lang.F.pred list
val cc_status : L.frame -> L.frame -> Lang.F.pred
val call_proper : t_env ->
Cil_datatype.Stmt.t ->
Cil_types.lval option ->
Kernel_function.t ->
Cil_types.exp list ->
pre:('a * Cil_types.predicate Cil_types.named) list ->
post:('b * Cil_types.predicate Cil_types.named) list ->
pexit:('c * Cil_types.predicate Cil_types.named) list ->
assigns:Cil_types.identified_term Cil_types.assigns ->
p_post:t_prop -> p_exit:t_prop -> unit -> t_prop
val call : t_env ->
Cil_datatype.Stmt.t ->
Cil_types.lval option ->
Kernel_function.t ->
Cil_types.exp list ->
pre:('a * Cil_types.predicate Cil_types.named) list ->
post:('b * Cil_types.predicate Cil_types.named) list ->
pexit:('c * Cil_types.predicate Cil_types.named) list ->
assigns:Cil_types.identified_term Cil_types.assigns ->
p_post:t_prop -> p_exit:t_prop -> t_prop
val scope : t_env ->
Cil_types.varinfo list -> Mcfg.scope -> t_prop -> t_prop
val close : t_env -> t_prop -> t_prop
val cc_from : D.t -> Lang.F.pred list -> vc -> vc
val build_prop_of_from : t_env ->
(WpPropId.prop_id * Cil_types.predicate Cil_types.named) list ->
t_prop -> t_prop
val is_trivial : vc -> bool
val is_empty : vc -> bool
val make_vcqs : target -> Splitter.tag list -> vc -> Wpo.VC_Annot.t Bag.t
val make_trivial : vc -> Wpo.VC_Annot.t
val make_oblig : Wpo.index -> WpPropId.prop_id -> Emitter.t -> Wpo.VC_Annot.t -> Wpo.t
module PMAP: FCMap.Make(P)
type group = {
   mutable verifs : Wpo.VC_Annot.t Bag.t;
   mutable trivial : vc;
}
val group_vc : group PMAP.t Pervasives.ref ->
target -> Splitter.tag list -> vc -> unit
val compile : Wpo.t Bag.t Pervasives.ref -> Wpo.index -> t_prop -> unit
val compile_lemma : LogicUsage.logic_lemma -> unit
val prove_lemma : Wpo.t Bag.t Pervasives.ref -> LogicUsage.logic_lemma -> unit