Module Cvalues

module Cvalues: sig .. end

Int-As-Boolans



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 is_constrained : Cil_types.typ -> bool
val is_constrained_comp : Cil_types.compinfo -> bool
module type CASES = sig .. end
module STRUCTURAL: 
functor (C : CASES) -> sig .. end
val null : (Lang.F.term -> Lang.F.pred) Context.value
test for null pointer value
module NULL: STRUCTURAL(sig
val prefix : string
val model : Cint.model
val is_int : 'a -> Lang.F.term -> Lang.F.pred
val is_float : 'a -> Lang.F.term -> Lang.F.pred
val is_pointer : Lang.F.term -> Lang.F.pred
end)
val is_null : Ctypes.c_object -> Lang.F.term -> Lang.F.pred
module TYPE: STRUCTURAL(sig
val prefix : string
val model : Cint.model
val is_int : Ctypes.c_int -> Lang.F.term -> Lang.F.pred
val is_float : Ctypes.c_float -> Lang.F.term -> Lang.F.pred
val is_pointer : 'a -> Lang.F.pred
end)
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 is_object : Ctypes.c_object -> 'a Memory.value -> 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 s_eq : (Ctypes.c_object -> Lang.F.term -> Lang.F.term -> Lang.F.pred) Pervasives.ref
module EQARRAY: Model.Generator(Matrix.NATURAL)(sig
type key = Matrix.matrix 
type data = Lang.lfun 
val name : string
val compile : Ctypes.c_object * Matrix.dim list -> Lang.lfun
end)
val equal_object : Ctypes.c_object -> Lang.F.term -> Lang.F.term -> Lang.F.pred
val equal_typ : Cil_types.typ -> 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 map_value : ('a -> 'b) -> 'a Memory.value -> 'b Memory.value
val map_sloc : ('a -> 'b) -> 'a Memory.sloc -> 'b Memory.sloc
val map_logic : ('a -> 'b) -> 'a Memory.logic -> 'b Memory.logic
val bool_eq : Lang.F.term -> Lang.F.term -> Lang.F.term
val bool_lt : Lang.F.term -> Lang.F.term -> Lang.F.term
val bool_neq : Lang.F.term -> Lang.F.term -> Lang.F.term
val bool_leq : Lang.F.term -> Lang.F.term -> Lang.F.term
val bool_and : Lang.F.term -> Lang.F.term -> Lang.F.term
val bool_or : Lang.F.term -> Lang.F.term -> Lang.F.term
val bool_val : Lang.F.term -> Lang.F.term
val is_true : Lang.F.pred -> Lang.F.term
p ? 1 : 0
val is_false : Lang.F.pred -> Lang.F.term
p ? 0 : 1
module Logic: 
functor (M : Memory.Model) -> sig .. end