functor (M : Memory.Model) ->
sig
module V :
sig
type elt = Lang.F.var
type t = Lang.F.Vars.t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val find : elt -> t -> elt
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val map : (elt -> elt) -> t -> t
val mapf : (elt -> elt option) -> t -> t
val intersect : t -> t -> bool
end
module P :
sig
type t = WpPropId.prop_id
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
module C :
sig
type loc = M.loc
type value = loc Memory.value
type sigma = M.Sigma.t
val cval : value -> Lang.F.term
val cloc : value -> loc
val cast : Cil_types.typ -> Cil_types.typ -> value -> value
val equal_typ : Cil_types.typ -> value -> value -> Lang.F.pred
val equal_obj : Ctypes.c_object -> value -> value -> Lang.F.pred
val exp : sigma -> Cil_types.exp -> value
val cond : sigma -> Cil_types.exp -> Lang.F.pred
val lval : sigma -> Cil_types.lval -> loc
val call : sigma -> Cil_types.exp -> loc
val loc_of_exp : sigma -> Cil_types.exp -> loc
val val_of_exp : sigma -> Cil_types.exp -> Lang.F.term
val return : sigma -> Cil_types.typ -> Cil_types.exp -> Lang.F.term
val is_zero : sigma -> Ctypes.c_object -> loc -> Lang.F.pred
val is_zero_range :
sigma ->
loc -> Ctypes.c_object -> Lang.F.term -> Lang.F.term -> Lang.F.pred
val instance_of : loc -> Cil_types.kernel_function -> Lang.F.pred
end
module L :
sig
type loc = M.loc
type sigma = M.Sigma.t
type value = M.loc Memory.value
type logic = M.loc Memory.logic
type region = M.loc Memory.sloc list
val pp_logic : Format.formatter -> logic -> unit
val pp_sloc : Format.formatter -> loc Memory.sloc -> unit
val pp_region : Format.formatter -> region -> unit
type frame = LogicSemantics.Make(M).frame
val pp_frame : Format.formatter -> frame -> unit
val get_frame : unit -> frame
val in_frame : frame -> ('a -> 'b) -> 'a -> 'b
val mem_frame : Clabels.c_label -> sigma
val mem_at_frame : frame -> Clabels.c_label -> sigma
val frame : Cil_types.kernel_function -> frame
val frame_copy : frame -> frame
val call_pre :
Cil_types.kernel_function -> value list -> sigma -> frame
val call_post :
Cil_types.kernel_function ->
value list -> sigma Memory.sequence -> frame
val return : unit -> Cil_types.typ
val result : unit -> Lang.F.var
val status : unit -> Lang.F.var
val guards : frame -> Lang.F.pred list
type env = LogicSemantics.Make(M).env
val new_env : Cil_types.logic_var list -> env
val move : env -> sigma -> env
val sigma : env -> sigma
val mem_at : env -> Clabels.c_label -> sigma
val call : sigma -> env
val term : env -> Cil_types.term -> Lang.F.term
val pred :
positive:bool ->
env -> Cil_types.predicate Cil_types.named -> Lang.F.pred
val region : env -> Cil_types.term -> region
val assigns :
env ->
Cil_types.identified_term Cil_types.assigns ->
(Ctypes.c_object * region) list option
val assigns_from :
env ->
Cil_types.identified_term Cil_types.from list ->
(Ctypes.c_object * region) list
val val_of_term : env -> Cil_types.term -> Lang.F.term
val loc_of_term : env -> Cil_types.term -> loc
val lemma : LogicUsage.logic_lemma -> Definitions.dlemma
val vars : region -> Lang.F.Vars.t
val occurs : Lang.F.var -> region -> bool
val valid :
sigma -> Memory.acs -> Ctypes.c_object -> region -> Lang.F.pred
val included :
Ctypes.c_object ->
region -> Ctypes.c_object -> region -> Lang.F.pred
val separated : (Ctypes.c_object * region) list -> Lang.F.pred
end
module A :
sig
type region = (Ctypes.c_object * M.loc Memory.sloc list) list
val vars : region -> Lang.F.Vars.t
val domain : region -> M.Heap.set
val assigned : M.sigma Memory.sequence -> region -> Lang.F.pred list
end
type target =
Gprop of CfgWP.VC.P.t
| Geffect of CfgWP.VC.P.t * Cil_datatype.Stmt.t *
WpPropId.effect_source
| Gposteffect of CfgWP.VC.P.t
module TARGET :
sig
type t = CfgWP.VC.target
val hsrc : WpPropId.effect_source -> int
val hash : CfgWP.VC.target -> int
val compare : CfgWP.VC.target -> CfgWP.VC.target -> int
val equal : CfgWP.VC.target -> CfgWP.VC.target -> bool
val prop_id : CfgWP.VC.target -> CfgWP.VC.P.t
val source :
CfgWP.VC.target ->
(Cil_datatype.Stmt.t * WpPropId.effect_source) option
val pretty : Format.formatter -> CfgWP.VC.target -> unit
end
type effect = {
e_pid : CfgWP.VC.P.t;
e_kind : WpPropId.a_kind;
e_label : Clabels.c_label;
e_valid : CfgWP.VC.L.sigma;
e_region : CfgWP.VC.A.region;
e_warn : Warning.Set.t;
}
module EFFECT :
sig
type t = CfgWP.VC.effect
val compare : CfgWP.VC.effect -> CfgWP.VC.effect -> int
end
module G :
sig
type t = TARGET.t
type set = Qed.Collection.Make(TARGET).set
type 'a map = 'a Qed.Collection.Make(TARGET).map
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
module Map :
sig
type key = t
type 'a t = 'a map
val empty : 'a t
val add : key -> 'a -> 'a t -> 'a t
val mem : key -> 'a t -> bool
val find : key -> 'a t -> 'a
val findk : key -> 'a t -> key * 'a
val size : 'a t -> int
val insert : (key -> 'a -> 'a -> 'a) -> key -> 'a -> 'a t -> 'a t
val change :
(key -> 'b -> 'a option -> 'a option) ->
key -> 'b -> 'a t -> 'a t
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
val mapf : (key -> 'a -> 'b option) -> 'a t -> 'b t
val mapq : (key -> 'a -> 'a option) -> 'a t -> 'a t
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val iter_sorted : (key -> 'a -> unit) -> 'a t -> unit
val fold_sorted : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val union : (key -> 'a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
val inter : (key -> 'a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
val interf :
(key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
val interq :
(key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val diffq :
(key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val subset : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iterk : (key -> 'a -> 'b -> unit) -> 'a t -> 'b t -> unit
val iter2 :
(key -> 'a option -> 'b option -> unit) -> 'a t -> 'b t -> unit
val merge :
(key -> 'a option -> 'b option -> 'c option) ->
'a t -> 'b t -> 'c t
type domain = set
val domain : 'a t -> domain
end
module Set :
sig
type elt = t
type t = set
val empty : t
val add : elt -> t -> t
val singleton : elt -> t
val elements : t -> elt list
val mem : elt -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val iter_sorted : (elt -> unit) -> t -> unit
val fold_sorted : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val union : t -> t -> t
val inter : t -> t -> t
val subset : t -> t -> bool
val intersect : t -> t -> bool
type 'a mapping = 'a map
val mapping : (elt -> 'a) -> t -> 'a mapping
end
end
module W :
sig
type elt = Warning.t
type t = Warning.Set.t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val choose : t -> elt
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val of_list : elt list -> t
val min_elt : t -> elt
val max_elt : t -> elt
val nearest_elt_le : elt -> t -> elt
val nearest_elt_ge : elt -> t -> elt
end
module D :
sig
type elt = Property.t
type t = Property.Set.t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val choose : t -> elt
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val of_list : elt list -> t
val min_elt : t -> elt
val max_elt : t -> elt
val nearest_elt_le : elt -> t -> elt
val nearest_elt_ge : elt -> t -> elt
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
module S :
sig
type elt = Cil_datatype.Stmt.t
type t = Cil_datatype.Stmt.Set.t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val choose : t -> elt
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val of_list : elt list -> t
val min_elt : t -> elt
val max_elt : t -> elt
val nearest_elt_le : elt -> t -> elt
val nearest_elt_ge : elt -> t -> elt
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
module Eset :
sig
type elt = EFFECT.t
type t = FCSet.Make(EFFECT).t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val choose : t -> elt
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val of_list : elt list -> t
val min_elt : t -> elt
val max_elt : t -> elt
val nearest_elt_le : elt -> t -> elt
val nearest_elt_ge : elt -> t -> elt
end
module Gset :
sig
type elt = G.t
type t = G.set
val empty : t
val add : elt -> t -> t
val singleton : elt -> t
val elements : t -> elt list
val mem : elt -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val iter_sorted : (elt -> unit) -> t -> unit
val fold_sorted : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val union : t -> t -> t
val inter : t -> t -> t
val subset : t -> t -> bool
val intersect : t -> t -> bool
type 'a mapping = 'a G.map
val mapping : (elt -> 'a) -> t -> 'a mapping
end
module Gmap :
sig
type key = G.t
type 'a t = 'a G.map
val empty : 'a t
val add : key -> 'a -> 'a t -> 'a t
val mem : key -> 'a t -> bool
val find : key -> 'a t -> 'a
val findk : key -> 'a t -> key * 'a
val size : 'a t -> int
val insert : (key -> 'a -> 'a -> 'a) -> key -> 'a -> 'a t -> 'a t
val change :
(key -> 'b -> 'a option -> 'a option) -> key -> 'b -> 'a t -> 'a t
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
val mapf : (key -> 'a -> 'b option) -> 'a t -> 'b t
val mapq : (key -> 'a -> 'a option) -> 'a t -> 'a t
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val iter_sorted : (key -> 'a -> unit) -> 'a t -> unit
val fold_sorted : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val union : (key -> 'a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
val inter : (key -> 'a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
val interf : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
val interq : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val diffq : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val subset : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iterk : (key -> 'a -> 'b -> unit) -> 'a t -> 'b t -> unit
val iter2 :
(key -> 'a option -> 'b option -> unit) -> 'a t -> 'b t -> unit
val merge :
(key -> 'a option -> 'b option -> 'c option) ->
'a t -> 'b t -> 'c t
type domain = G.set
val domain : 'a t -> domain
end
type vc = {
hyps : Conditions.bundle;
goal : Lang.F.pred;
vars : Lang.F.Vars.t;
warn : CfgWP.VC.W.t;
deps : CfgWP.VC.D.t;
path : CfgWP.VC.S.t;
}
type t_env = { frame : CfgWP.VC.L.frame; main : CfgWP.VC.L.env; }
type t_prop = {
sigma : CfgWP.VC.L.sigma option;
effects : CfgWP.VC.Eset.t;
vcs : CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t;
}
val pp_vc : Format.formatter -> CfgWP.VC.vc -> unit
val pp_vcs : Format.formatter -> CfgWP.VC.vc Splitter.t -> unit
val pp_gvcs :
Format.formatter -> CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t -> unit
val pretty : Format.formatter -> CfgWP.VC.t_prop -> unit
val empty_vc : CfgWP.VC.vc
val sigma_opt : M.Sigma.t option -> M.Sigma.t
val sigma_at : CfgWP.VC.t_prop -> CfgWP.VC.L.sigma
val sigma_any : call:bool -> CfgWP.VC.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 : CfgWP.VC.vc -> Lang.F.Vars.elt -> bool
val intersect_vc : CfgWP.VC.vc -> Lang.F.pred -> bool
val assume_vc :
descr:string ->
?hpid:WpPropId.prop_id ->
?stmt:CfgWP.VC.S.elt ->
?warn:Warning.Set.t -> Lang.F.pred list -> CfgWP.VC.vc -> CfgWP.VC.vc
val passify_vc : Passive.t -> CfgWP.VC.vc -> CfgWP.VC.vc
val branch_vc :
stmt:Cil_types.stmt ->
Lang.F.pred -> CfgWP.VC.vc -> CfgWP.VC.vc -> CfgWP.VC.vc
val merge_vc : CfgWP.VC.vc -> CfgWP.VC.vc -> CfgWP.VC.vc
val merge_vcs : CfgWP.VC.vc list -> CfgWP.VC.vc
val gmerge :
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
val gmap :
('a -> 'b) ->
'a Splitter.t CfgWP.VC.Gmap.t -> 'b Splitter.t CfgWP.VC.Gmap.t
val gbranch :
left:('a -> 'b) ->
both:('a -> 'c -> 'b) ->
right:('c -> 'b) ->
'a Splitter.t CfgWP.VC.Gmap.t ->
'c Splitter.t CfgWP.VC.Gmap.t -> 'b Splitter.t CfgWP.VC.Gmap.t
val merge_all_vcs :
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t list ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
val empty : CfgWP.VC.t_prop
val merge :
CfgWP.VC.t_env -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
val new_env :
?lvars:Cil_types.logic_var list ->
Cil_types.kernel_function -> CfgWP.VC.t_env
val in_wenv :
CfgWP.VC.t_env ->
CfgWP.VC.t_prop -> (CfgWP.VC.L.env -> CfgWP.VC.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 :
CfgWP.VC.Gmap.key ->
?warn:CfgWP.VC.W.t ->
Lang.F.pred ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
val cc_effect :
CfgWP.VC.L.env ->
CfgWP.VC.P.t -> WpPropId.assigns_desc -> CfgWP.VC.effect option
val cc_posteffect :
CfgWP.VC.effect ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
val add_axiom : 'a -> 'b -> unit
val add_hyp :
CfgWP.VC.t_env ->
WpPropId.prop_id * Cil_types.predicate Cil_types.named ->
CfgWP.VC.t_prop -> CfgWP.VC.t_prop
val add_goal :
CfgWP.VC.t_env ->
CfgWP.VC.P.t * Cil_types.predicate Cil_types.named ->
CfgWP.VC.t_prop -> CfgWP.VC.t_prop
val add_assigns :
CfgWP.VC.t_env ->
CfgWP.VC.P.t * WpPropId.assigns_desc ->
CfgWP.VC.t_prop -> CfgWP.VC.t_prop
val add_warnings :
CfgWP.VC.W.t ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
val assigns_condition :
CfgWP.VC.A.region -> CfgWP.VC.effect -> Lang.F.pred
exception COLLECTED
val is_collected : 'a Splitter.t CfgWP.VC.Gmap.t -> CfgWP.VC.P.t -> bool
val check_nothing :
CfgWP.VC.Eset.t ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
val check_assigns :
Cil_datatype.Stmt.t option ->
WpPropId.effect_source ->
?warn:Warning.Set.t ->
CfgWP.VC.A.region ->
CfgWP.VC.Eset.t ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
CfgWP.VC.vc Splitter.t CfgWP.VC.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 ->
CfgWP.VC.A.region ->
CfgWP.VC.Eset.t ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
val do_assigns_everything :
?stmt:Cil_datatype.Stmt.t ->
?warn:CfgWP.VC.W.t ->
CfgWP.VC.Eset.t ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
val cc_assigned :
CfgWP.VC.L.env ->
WpPropId.a_kind ->
Cil_types.identified_term Cil_types.from list ->
CfgWP.VC.L.sigma Memory.sequence *
(Ctypes.c_object * CfgWP.VC.L.region) list
val use_assigns :
CfgWP.VC.t_env ->
Cil_datatype.Stmt.t option ->
WpPropId.prop_id option ->
WpPropId.assigns_desc -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
val is_stopeffect : Clabels.c_label -> CfgWP.VC.effect -> bool
val not_posteffect : CfgWP.VC.Eset.t -> CfgWP.VC.target -> 'a -> bool
val label :
CfgWP.VC.t_env -> Clabels.c_label -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
val cc_lval :
CfgWP.VC.L.env ->
Cil_types.lval ->
Ctypes.c_object * M.Heap.set * CfgWP.VC.L.sigma Memory.sequence *
CfgWP.VC.C.loc
val cc_stored :
M.sigma Memory.sequence ->
M.loc -> Ctypes.c_object -> Cil_types.exp -> Lang.F.pred list
val assign :
CfgWP.VC.t_env ->
Cil_datatype.Stmt.t ->
Cil_types.lval -> Cil_types.exp -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
val return :
CfgWP.VC.t_env ->
CfgWP.VC.S.elt ->
Cil_types.exp option -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
val condition :
descr:string ->
?stmt:CfgWP.VC.S.elt ->
?warn:Warning.Set.t ->
Passive.t -> Lang.F.pred list -> CfgWP.VC.vc -> CfgWP.VC.vc
val mark :
Splitter.tag -> CfgWP.VC.vc Splitter.t option -> CfgWP.VC.vc Splitter.t
val random : unit -> Lang.F.pred
val pp_opt :
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a option -> unit
val test :
CfgWP.VC.t_env ->
CfgWP.VC.S.elt ->
Cil_types.exp -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
val cc_case_values :
int64 list ->
Lang.F.term list ->
CfgWP.VC.C.sigma -> Cil_types.exp list -> int64 list * Lang.F.term list
val cc_group_case :
CfgWP.VC.S.elt ->
Warning.Set.t ->
string ->
Splitter.tag ->
Passive.t ->
Lang.F.pred list ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
val cc_case :
CfgWP.VC.S.elt ->
Warning.Set.t ->
CfgWP.VC.C.sigma ->
Lang.F.term ->
Cil_types.exp list * CfgWP.VC.t_prop ->
Lang.F.term list * CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
val cc_default :
CfgWP.VC.S.elt ->
M.Sigma.t ->
Lang.F.pred list ->
CfgWP.VC.t_prop -> CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
val switch :
CfgWP.VC.t_env ->
CfgWP.VC.S.elt ->
Cil_types.exp ->
(Cil_types.exp list * CfgWP.VC.t_prop) list ->
CfgWP.VC.t_prop -> CfgWP.VC.t_prop
val init_value :
CfgWP.VC.t_env ->
Cil_types.lval ->
Cil_types.typ ->
Cil_types.exp option -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
val init_range :
CfgWP.VC.t_env ->
Cil_types.lval ->
Cil_types.typ -> int64 -> int64 -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
val loop_step : 'a -> 'a
val loop_entry : 'a -> 'a
val call_instances :
CfgWP.VC.C.sigma ->
CfgWP.VC.P.t ->
Cil_types.exp ->
Cil_types.kernel_function list ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
val call_contract :
CfgWP.VC.S.elt ->
M.Sigma.t ->
(Warning.Set.t * CfgWP.VC.C.loc) option ->
Kernel_function.t * CfgWP.VC.t_prop ->
CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t
val call_dynamic :
CfgWP.VC.t_env ->
CfgWP.VC.S.elt ->
CfgWP.VC.P.t ->
Cil_types.exp ->
(Kernel_function.t * CfgWP.VC.t_prop) list -> CfgWP.VC.t_prop
val call_goal_precond :
CfgWP.VC.t_env ->
'a ->
Cil_types.kernel_function ->
Cil_types.exp list ->
pre:(CfgWP.VC.P.t * Cil_types.predicate Cil_types.named) list ->
CfgWP.VC.t_prop -> CfgWP.VC.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 : CfgWP.VC.L.frame;
frame_post : CfgWP.VC.L.frame;
frame_exit : CfgWP.VC.L.frame;
}
val cc_result_domain : Cil_types.lval option -> M.Heap.Set.t option
val cc_call_domain :
CfgWP.VC.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 :
CfgWP.VC.L.env ->
Cil_types.lval option ->
Cil_types.kernel_function ->
Cil_types.exp list ->
Cil_types.identified_term Cil_types.assigns ->
CfgWP.VC.t_prop -> CfgWP.VC.t_prop -> CfgWP.VC.callenv
type call_vcs = {
vcs_post : CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t;
vcs_exit : CfgWP.VC.vc Splitter.t CfgWP.VC.Gmap.t;
}
val cc_call_effects :
Cil_datatype.Stmt.t ->
CfgWP.VC.callenv ->
CfgWP.VC.L.env ->
Cil_types.identified_term Cil_types.assigns ->
CfgWP.VC.t_prop -> CfgWP.VC.t_prop -> CfgWP.VC.call_vcs
val cc_contract_hyp :
CfgWP.VC.L.frame ->
CfgWP.VC.L.env ->
('a * Cil_types.predicate Cil_types.named) list -> Lang.F.pred list
val cc_result : CfgWP.VC.callenv -> Lang.F.pred list
val cc_status : CfgWP.VC.L.frame -> CfgWP.VC.L.frame -> Lang.F.pred
val call_proper :
CfgWP.VC.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:CfgWP.VC.t_prop ->
p_exit:CfgWP.VC.t_prop -> unit -> CfgWP.VC.t_prop
val call :
CfgWP.VC.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:CfgWP.VC.t_prop -> p_exit:CfgWP.VC.t_prop -> CfgWP.VC.t_prop
val scope :
CfgWP.VC.t_env ->
Cil_types.varinfo list ->
Mcfg.scope -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
val close : CfgWP.VC.t_env -> CfgWP.VC.t_prop -> CfgWP.VC.t_prop
val cc_from :
CfgWP.VC.D.t -> Lang.F.pred list -> CfgWP.VC.vc -> CfgWP.VC.vc
val build_prop_of_from :
CfgWP.VC.t_env ->
(WpPropId.prop_id * Cil_types.predicate Cil_types.named) list ->
CfgWP.VC.t_prop -> CfgWP.VC.t_prop
val is_trivial : CfgWP.VC.vc -> bool
val is_empty : CfgWP.VC.vc -> bool
val make_vcqs :
CfgWP.VC.target ->
Splitter.tag list -> CfgWP.VC.vc -> Wpo.VC_Annot.t Bag.t
val make_trivial : CfgWP.VC.vc -> Wpo.VC_Annot.t
val make_oblig :
Wpo.index -> WpPropId.prop_id -> Emitter.t -> Wpo.VC_Annot.t -> Wpo.t
module PMAP :
sig
type key = P.t
type 'a t = 'a FCMap.Make(P).t
val empty : 'a t
val is_empty : 'a t -> bool
val mem : key -> 'a t -> bool
val add : key -> 'a -> 'a t -> 'a t
val singleton : key -> 'a -> 'a t
val remove : key -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) ->
'a t -> 'b t -> 'c t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val for_all : (key -> 'a -> bool) -> 'a t -> bool
val exists : (key -> 'a -> bool) -> 'a t -> bool
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val cardinal : 'a t -> int
val bindings : 'a t -> (key * 'a) list
val min_binding : 'a t -> key * 'a
val max_binding : 'a t -> key * 'a
val choose : 'a t -> key * 'a
val split : key -> 'a t -> 'a t * 'a option * 'a t
val find : key -> 'a t -> 'a
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
end
type group = {
mutable verifs : Wpo.VC_Annot.t Bag.t;
mutable trivial : CfgWP.VC.vc;
}
val group_vc :
CfgWP.VC.group CfgWP.VC.PMAP.t Pervasives.ref ->
CfgWP.VC.target -> Splitter.tag list -> CfgWP.VC.vc -> unit
val compile :
Wpo.t Bag.t Pervasives.ref -> Wpo.index -> CfgWP.VC.t_prop -> unit
val compile_lemma : LogicUsage.logic_lemma -> unit
val prove_lemma :
Wpo.t Bag.t Pervasives.ref -> LogicUsage.logic_lemma -> unit
end