module ConstBasic: sig .. end
Module that containts the constraints
type
constraint
type
Methods to create values
val c_true : t
val c_false : string option -> t
val create_c_demotation_lenv : Inf.Vars.LEVar.t -> Inf.Type.phi -> Inf.Vars.LEVar.t -> t
create_c_demonation_lenv lev1 mu lev2 creates a constraint that
changes all precise pointers, for which the location is part of
mu, into imprecise pointers. It is equivalant with
create_c_demonation_lenv_phi lev1 mu (create_phi_ls LSet.empty) lev2.
val create_c_demotation_lenv_phi : Inf.Vars.LEVar.t ->
Inf.Type.phi -> Inf.Type.phi -> Inf.Vars.LEVar.t -> t
create_c_demonation_lenv_ls lev1 mu ls lev2
creates a constraint that ensures that the intersection of
the domain of variables lev1 and ls is empty.
val create_c_demotation_type : Inf.Type.t -> Inf.Type.phi -> Inf.Type.t -> t
val create_c_include : Location.Loc.t -> Inf.Type.phi -> t
val create_c_exclude : Location.Loc.t -> Inf.Type.phi -> t
val create_c_subset : ?prio:int -> Inf.Type.phi -> Inf.Type.phi -> t
val create_c_disjoint : ?prio:int -> Inf.Type.phi -> Inf.Type.phi -> t
val create_c_subtype : ?prio:int -> Inf.Type.t -> Inf.Type.t -> t
val create_c_eqtype : Inf.Type.t -> Inf.Type.t -> t
val create_c_eqlenv : Inf.Type.lenv -> Inf.Type.lenv -> t
val create_c_eqobj : Inf.Type.r -> Inf.Type.r -> t
val create_c_eqset : Inf.Type.phi -> Inf.Type.phi -> t
val create_c_eqpres : Inf.Type.q -> Inf.Type.q -> t
val create_c_domain_eq : Inf.Type.phi -> Inf.Vars.LEVar.t -> t
val create_c_lev_empty_obj : Inf.Vars.LEVar.t -> Inf.Vars.LEVar.t -> Location.Loc.t -> t
val create_c_flow : Inf.Vars.LEVar.t -> Inf.Type.t -> Inf.Type.t -> t
val create_c_read : Inf.Vars.LEVar.t ->
Inf.Vars.PrVar.t ->
Inf.Vars.LSVar.t -> Syntax.label -> Inf.Vars.TVar.t -> t
val create_c_write : Inf.Vars.LEVar.t ->
Inf.Vars.TVar.t ->
Syntax.label -> Inf.Vars.TVar.t -> Inf.Vars.LEVar.t -> t
val create_c_locs : Inf.Type.phi -> Inf.Type.t -> t
Conversion into Strings
val string_of : t -> string