sig
type link_kind =
SINGLE of Misc.component * Exp.Fld.t
| DOUBLE of Misc.component * Misc.component
| XOR of Misc.component
type can_isemp = Cem_PE | Cem_NE
type tag
type tag2
type pstate =
Pstate_one of Misc.component * Exp.exp list
| Pstate_max of Assertions.pstate * Assertions.pstate
type can_spred =
Csp_listsegi of Assertions.tag * Assertions.link_kind * Exp.exp *
Exp.exp * Exp.exp * Exp.exp * Assertions.can_isemp * Exp.Dset.t
| Csp_arr of Assertions.tag * Exp.exp * Exp.exp * Exp.exp * Exp.Fld.t *
Assertions.can_isemp * Exp.Dset.t
| Csp_node of Assertions.tag * Misc.component * Exp.exp * Exp.Fld.t *
Assertions.tag2
| Csp_indpred of Assertions.tag * string * Exp.exp list
| Csp_atomic_fld of Assertions.tag * Exp.exp * Misc.component *
Misc.component * Assertions.pstate
| Csp_escrow of Assertions.tag * Misc.component * Exp.exp list
| Csp_token of Assertions.tag * Exp.exp
and can_spatial = Assertions.can_spred list
and uform = Pure.t * Assertions.can_spatial
and cform =
Assertions.uform * (Misc.component, Assertions.cprop) Misc.plist
and cprop = Assertions.cform list
type act
exception No_frame_found of string
exception Junk
val tag_default : Assertions.tag
val tag2_default : Assertions.tag2
val spred_fold : (Exp.exp -> 'a -> 'a) -> Assertions.can_spred -> 'a -> 'a
val spat_empty : Assertions.can_spatial
val spat_one : Assertions.can_spred -> Assertions.can_spatial
val spat_star_one :
Assertions.can_spred -> Assertions.can_spatial -> Assertions.can_spatial
val spat_star :
Assertions.can_spatial ->
Assertions.can_spatial -> Assertions.can_spatial
val spat_remove :
Assertions.can_spatial -> Assertions.can_spred -> Assertions.can_spatial
val spat_fold : (Exp.exp -> 'a -> 'a) -> Assertions.can_spatial -> 'a -> 'a
val spat_fold_spred :
(Assertions.can_spred -> 'a -> 'a) -> Assertions.can_spatial -> 'a -> 'a
val spat_get :
Exp.exp ->
Assertions.can_spatial ->
(Assertions.can_spred * Assertions.can_spatial) option
val compare_can_spred : Assertions.can_spred -> Assertions.can_spred -> int
val abs_compare_can_spred :
Assertions.can_spred -> Assertions.can_spred -> int
val uform_false : Assertions.uform
val cform_false : Assertions.cform
val cprop_false : Assertions.cprop
val uform_empty : Assertions.uform
val cprop_empty : Assertions.cprop
val is_cprop_empty : Assertions.cprop -> bool
val cprop_pure : Pure.t -> Assertions.cprop
val cprop_spred : Assertions.can_spatial -> Assertions.cprop
val cprop_uform : Assertions.uform -> Assertions.cprop
val cprop_cform : Assertions.cform -> Assertions.cprop
val mk_array :
Assertions.tag ->
Exp.exp ->
Exp.exp ->
Exp.exp ->
Exp.Fld.t -> Exp.Dset.t -> Assertions.uform -> Assertions.uform
val cform_star :
Assertions.cform -> Assertions.cform -> Assertions.cform option
val cprop_star : Assertions.cprop -> Assertions.cprop -> Assertions.cprop
val and_cprop_pure : Assertions.cprop -> Pure.t -> Assertions.cprop
val cprop_or : Assertions.cprop -> Assertions.cprop -> Assertions.cprop
val cprop_box : Misc.component -> Assertions.cprop -> Assertions.cprop
val aggr_remove_cform_duplicates : Assertions.cprop -> Assertions.cprop
val compare_uform : Assertions.uform -> Assertions.uform -> int
val compare_cform : Assertions.cform -> Assertions.cform -> int
val compare_cprop : Assertions.cprop -> Assertions.cprop -> int
val compare_component_cprop :
Misc.component * Assertions.cprop ->
Misc.component * Assertions.cprop -> int
val remove_uform_duplicates :
Assertions.uform list -> Assertions.uform list
val remove_cform_duplicates :
Assertions.cform list -> Assertions.cform list
val can_spred_leq : Assertions.can_spred -> Assertions.can_spred -> Exp.exp
val equal_pstate : Assertions.pstate -> Assertions.pstate -> bool
val uform_fhd : Assertions.uform -> Exp.IdSet.t -> Exp.IdSet.t
val spred_fv : Assertions.can_spred -> Exp.IdSet.t -> Exp.IdSet.t
val spred_exfv : Assertions.can_spred -> Exp.IdSet.t -> Exp.IdSet.t
val prop_fv : Assertions.cprop -> Exp.IdSet.t -> Exp.IdSet.t
val fv_norm_cprop : Assertions.cprop -> Exp.IdSet.t
val prop_exfv : Assertions.cprop -> Exp.IdSet.t -> Exp.IdSet.t
val form_exfv : Assertions.cform -> Exp.IdSet.t -> Exp.IdSet.t
val abs_fv_uform : Assertions.uform -> Exp.Id.t list
val map_spat :
(Exp.exp -> Exp.exp) -> Assertions.can_spatial -> Assertions.can_spatial
val map_uform :
(Exp.exp -> Exp.exp) -> Assertions.uform -> Assertions.uform list
val map_cform :
(Exp.exp -> Exp.exp) -> Assertions.cform -> Assertions.cprop
val map_cprop :
(Exp.exp -> Exp.exp) -> Assertions.cprop -> Assertions.cprop
val map_ip_body :
(Exp.exp -> Exp.exp) ->
(Pure.t * Assertions.cform) list -> (Pure.t * Assertions.cform) list
val naive_map_cform :
(Exp.exp -> Exp.exp) -> Assertions.cform -> Assertions.cform
val form_kill_hd_vars : Assertions.cform -> Assertions.cform
val prop_kill_can_return : Assertions.cprop -> Assertions.cprop
val normalize_uform : Assertions.uform -> Assertions.uform list
val normalize_cform : Assertions.cform -> Assertions.cprop
val normalize_cform_aggr : Assertions.cform -> Assertions.cprop
val normalize_cprop : Assertions.cprop -> Assertions.cprop
val kill_garbage_vars : Assertions.cprop -> Assertions.cprop
val kill_garbage_vars_ufl : Assertions.uform list -> Assertions.uform list
val aggr_kill_garbage_vars : Assertions.cprop -> Assertions.cprop
val kill_dead_vars : Exp.IdSet.t -> Assertions.cprop -> Assertions.cprop
type prover = {
find_ptsto :
Misc.component ->
Exp.exp -> Assertions.can_spatial -> Exp.Fld.t * Assertions.can_spatial;
expose_ptsto : Assertions.cprop -> Exp.exp -> Assertions.cprop;
nf_cprop : Assertions.can_spatial -> Assertions.cprop -> Assertions.cprop;
nf_cform : Assertions.cform -> Assertions.cprop;
entails_cprop : Assertions.cprop -> Assertions.cprop -> Pure.t list;
find_frame_cprop :
Assertions.can_spatial ->
Assertions.cprop -> Assertions.cprop -> Assertions.cprop;
adv_entails_atom : Assertions.cprop -> Exp.exp -> bool;
}
val new_acts :
string ->
Assertions.cprop ->
Assertions.cprop -> Assertions.cprop -> Assertions.act list
val new_acts_one :
string ->
Pure.t ->
Assertions.can_spatial ->
Assertions.can_spatial -> Assertions.can_spatial -> Assertions.act list
val new_act_opt :
string ->
Pure.t ->
Assertions.can_spatial ->
(Exp.exp * Exp.Fld.t * Exp.Fld.t) list ->
Assertions.can_spatial -> Assertions.cprop -> Assertions.act
val act_name : Assertions.act -> string
val act_conj : Exp.exp -> Assertions.act -> Assertions.act
val act_changes :
Exp.exp -> Misc.component -> Assertions.act list -> Assertions.act list
val interfere_once :
Assertions.prover ->
Assertions.act -> Assertions.cprop -> Assertions.cprop
val pp_spred : Format.formatter -> Assertions.can_spred -> unit
val pp_uform : Format.formatter -> Assertions.uform -> unit
val pp_cform : Format.formatter -> Assertions.cform -> unit
val pp_cprop : Format.formatter -> Assertions.cprop -> unit
val pp_act : Format.formatter -> Assertions.act -> unit
val pp_pstate : Format.formatter -> Assertions.pstate -> unit
val allow_leaks : bool Pervasives.ref
val disable_pure_code_checking : bool Pervasives.ref
val args : (Arg.key * Arg.spec * Arg.doc) list
end