sig
val bool_val : Lang.F.unop
val bool_eq : Lang.F.binop
val bool_lt : Lang.F.binop
val bool_neq : Lang.F.binop
val bool_leq : Lang.F.binop
val bool_and : Lang.F.binop
val bool_or : Lang.F.binop
val is_true : Lang.F.pred -> Lang.F.term
val is_false : Lang.F.pred -> Lang.F.term
val null : (Lang.F.term -> Lang.F.pred) Context.value
val is_null : Ctypes.c_object -> Lang.F.term -> Lang.F.pred
val is_object : Ctypes.c_object -> 'a Memory.value -> Lang.F.pred
val has_ctype : Cil_types.typ -> Lang.F.term -> Lang.F.pred
val has_ltype : Cil_types.logic_type -> Lang.F.term -> Lang.F.pred
val cdomain : Cil_types.typ -> (Lang.F.term -> Lang.F.pred) option
val ldomain : Cil_types.logic_type -> (Lang.F.term -> Lang.F.pred) option
val equal_object :
Ctypes.c_object -> Lang.F.term -> Lang.F.term -> Lang.F.pred
val equal_comp :
Cil_types.compinfo -> Lang.F.term -> Lang.F.term -> Lang.F.pred
val equal_array :
Matrix.matrix -> Lang.F.term -> Lang.F.term -> Lang.F.pred
val ainf : Lang.F.term option
val asup : int -> Lang.F.term option
val constant : Cil_types.constant -> Lang.F.term
val logic_constant : Cil_types.logic_constant -> Lang.F.term
val constant_exp : Cil_types.exp -> Lang.F.term
val constant_term : Cil_types.term -> Lang.F.term
val map_sloc : ('a -> 'b) -> 'a Memory.sloc -> 'b Memory.sloc
val map_value : ('a -> 'b) -> 'a Memory.value -> 'b Memory.value
val map_logic : ('a -> 'b) -> 'a Memory.logic -> 'b Memory.logic
val plain : Cil_types.logic_type -> Lang.F.term -> 'a Memory.logic
type polarity = [ `Negative | `NoPolarity | `Positive ]
val negate : Cvalues.polarity -> Cvalues.polarity
module Logic :
functor (M : Memory.Model) ->
sig
type logic = M.loc Memory.logic
val value : Cvalues.Logic.logic -> Lang.F.term
val loc : Cvalues.Logic.logic -> M.loc
val vset : Cvalues.Logic.logic -> Vset.set
val sloc : Cvalues.Logic.logic -> M.loc Memory.sloc list
val rdescr :
M.loc Memory.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
type region = M.loc Memory.sloc list
val separated :
(Ctypes.c_object * Cvalues.Logic.region) list -> Lang.F.pred
val included :
Ctypes.c_object ->
Cvalues.Logic.region ->
Ctypes.c_object -> Cvalues.Logic.region -> Lang.F.pred
val valid :
M.Sigma.t ->
Memory.acs ->
Ctypes.c_object -> Cvalues.Logic.region -> Lang.F.pred
end
end