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 =
VC(M).target =
Gprop of P.t
| Geffect of P.t * Cil_datatype.Stmt.t * WpPropId.effect_source
| Gposteffect of P.t
module TARGET :
sig
type t = target
val hsrc : WpPropId.effect_source -> int
val hash : target -> int
val compare : target -> target -> int
val equal : target -> target -> bool
val prop_id : target -> P.t
val source :
target -> (Cil_datatype.Stmt.t * WpPropId.effect_source) option
val pretty : Format.formatter -> target -> unit
end
type effect =
VC(M).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 type t = effect val compare : effect -> 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 =
VC(M).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 = VC(M).t_env = { frame : L.frame; main : L.env; }
type t_prop =
VC(M).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 =
VC(M).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 =
VC(M).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 :
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 =
VC(M).group = {
mutable verifs : Wpo.VC_Annot.t Bag.t;
mutable trivial : vc;
}
val group_vc :
group PMAP.t ref -> target -> Splitter.tag list -> vc -> unit
val compile : Wpo.t Bag.t ref -> Wpo.index -> t_prop -> unit
val compile_lemma : LogicUsage.logic_lemma -> unit
val prove_lemma : Wpo.t Bag.t ref -> LogicUsage.logic_lemma -> unit
end