functor (M : Sigs.Model) ->
sig
type logic = M.loc Sigs.logic
type segment = Ctypes.c_object * M.loc Sigs.sloc
type region = M.loc Sigs.region
val value : Cvalues.Logic.logic -> Lang.F.term
val loc : Cvalues.Logic.logic -> M.loc
val vset : Cvalues.Logic.logic -> Vset.set
val region :
Ctypes.c_object -> Cvalues.Logic.logic -> Cvalues.Logic.region
val rdescr : M.loc Sigs.sloc -> Lang.F.var list * M.loc * Lang.F.pred
val map : Lang.F.unop -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val map_opp : Cvalues.Logic.logic -> Cvalues.Logic.logic
val map_loc :
(M.loc -> M.loc) -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val map_l2t :
(M.loc -> Lang.F.term) -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val map_t2l :
(Lang.F.term -> M.loc) -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val apply :
Lang.F.binop ->
Cvalues.Logic.logic -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val apply_add :
Cvalues.Logic.logic -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val apply_sub :
Cvalues.Logic.logic -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val field :
Cvalues.Logic.logic -> Cil_types.fieldinfo -> Cvalues.Logic.logic
val shift :
Cvalues.Logic.logic ->
Ctypes.c_object ->
?size:int -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val load :
M.Sigma.t ->
Ctypes.c_object -> Cvalues.Logic.logic -> Cvalues.Logic.logic
val union :
Cil_types.logic_type -> Cvalues.Logic.logic list -> Cvalues.Logic.logic
val inter :
Cil_types.logic_type -> Cvalues.Logic.logic list -> Cvalues.Logic.logic
val subset :
Cil_types.logic_type ->
Cvalues.Logic.logic ->
Cil_types.logic_type -> Cvalues.Logic.logic -> Lang.F.pred
val separated : Cvalues.Logic.region list -> Lang.F.pred
val included :
Cvalues.Logic.segment -> Cvalues.Logic.segment -> Lang.F.pred
val valid : M.Sigma.t -> Sigs.acs -> Cvalues.Logic.segment -> Lang.F.pred
val invalid : M.Sigma.t -> Cvalues.Logic.segment -> Lang.F.pred
end