sig
val equation : Sigs.equation -> Lang.F.pred
type 'a printer = Format.formatter -> 'a -> unit
val pp_bound : Lang.F.term option Cvalues.printer
val pp_value : 'a Cvalues.printer -> 'a Sigs.value Cvalues.printer
val pp_logic : 'a Cvalues.printer -> 'a Sigs.logic Cvalues.printer
val pp_region : 'a Cvalues.printer -> 'a Sigs.region Cvalues.printer
val pp_sloc : 'a Cvalues.printer -> 'a Sigs.sloc Cvalues.printer
val pp_rloc : 'a Cvalues.printer -> 'a Sigs.rloc Cvalues.printer
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 startof :
shift:('a -> Ctypes.c_object -> Lang.F.term -> 'a) ->
'a -> Cil_types.typ -> 'a
val is_object : Ctypes.c_object -> 'a Sigs.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 : Ctypes.c_object -> (Lang.F.term -> Lang.F.pred) option
val ldomain : Cil_types.logic_type -> (Lang.F.term -> Lang.F.pred) option
val volatile : ?warn:string -> unit -> bool
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 Sigs.sloc -> 'b Sigs.sloc
val map_value : ('a -> 'b) -> 'a Sigs.value -> 'b Sigs.value
val map_logic : ('a -> 'b) -> 'a Sigs.logic -> 'b Sigs.logic
val plain : Cil_types.logic_type -> Lang.F.term -> 'a Sigs.logic
type polarity = [ `Negative | `NoPolarity | `Positive ]
val negate : Cvalues.polarity -> Cvalues.polarity
module Logic :
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
end