sig
type c_int =
UInt8
| SInt8
| UInt16
| SInt16
| UInt32
| SInt32
| UInt64
| SInt64
val c_int_all : Wp.Ctypes.c_int list
type c_float = Float32 | Float64
type arrayflat = {
arr_size : int;
arr_dim : int;
arr_cell : Cil_types.typ;
arr_cell_nbr : int;
}
type arrayinfo = {
arr_element : Cil_types.typ;
arr_flat : Wp.Ctypes.arrayflat option;
}
type c_object =
C_int of Wp.Ctypes.c_int
| C_float of Wp.Ctypes.c_float
| C_pointer of Cil_types.typ
| C_comp of Cil_types.compinfo
| C_array of Wp.Ctypes.arrayinfo
val object_of_pointed : Wp.Ctypes.c_object -> Wp.Ctypes.c_object
val object_of_array_elem : Wp.Ctypes.c_object -> Wp.Ctypes.c_object
val object_of_logic_type : Cil_types.logic_type -> Wp.Ctypes.c_object
val object_of_logic_pointed : Cil_types.logic_type -> Wp.Ctypes.c_object
val imemo : (Wp.Ctypes.c_int -> 'a) -> Wp.Ctypes.c_int -> 'a
val fmemo : (Wp.Ctypes.c_float -> 'a) -> Wp.Ctypes.c_float -> 'a
val is_char : Wp.Ctypes.c_int -> bool
val c_char : unit -> Wp.Ctypes.c_int
val c_bool : unit -> Wp.Ctypes.c_int
val c_ptr : unit -> Wp.Ctypes.c_int
val c_int : Cil_types.ikind -> Wp.Ctypes.c_int
val c_float : Cil_types.fkind -> Wp.Ctypes.c_float
val object_of : Cil_types.typ -> Wp.Ctypes.c_object
val is_void : Cil_types.typ -> bool
val is_pointer : Wp.Ctypes.c_object -> bool
val char : char -> int64
val constant : Cil_types.exp -> int64
val get_int : Cil_types.exp -> int64 option
val i_bits : Wp.Ctypes.c_int -> int
val i_bytes : Wp.Ctypes.c_int -> int
val signed : Wp.Ctypes.c_int -> bool
val c_int_bounds : Wp.Ctypes.c_int -> Integer.t * Integer.t
val sub_c_int : Wp.Ctypes.c_int -> Wp.Ctypes.c_int -> bool
val sub_c_float : Wp.Ctypes.c_float -> Wp.Ctypes.c_float -> bool
val sizeof_defined : Wp.Ctypes.c_object -> bool
val sizeof_object : Wp.Ctypes.c_object -> int
val field_offset : Cil_types.fieldinfo -> int
val no_infinite_array : Wp.Ctypes.c_object -> bool
val array_dim : Wp.Ctypes.arrayinfo -> Wp.Ctypes.c_object * int
val array_size : Cil_types.typ -> int option
val array_dimensions :
Wp.Ctypes.arrayinfo -> Wp.Ctypes.c_object * int option list
val dimension_of_object : Wp.Ctypes.c_object -> (int * int) option
val i_convert : Wp.Ctypes.c_int -> Wp.Ctypes.c_int -> Wp.Ctypes.c_int
val f_convert : Wp.Ctypes.c_float -> Wp.Ctypes.c_float -> Wp.Ctypes.c_float
val promote :
Wp.Ctypes.c_object -> Wp.Ctypes.c_object -> Wp.Ctypes.c_object
val pp_int : Format.formatter -> Wp.Ctypes.c_int -> unit
val pp_float : Format.formatter -> Wp.Ctypes.c_float -> unit
val pp_object : Format.formatter -> Wp.Ctypes.c_object -> unit
val basename : Wp.Ctypes.c_object -> string
val compare : Wp.Ctypes.c_object -> Wp.Ctypes.c_object -> int
val equal : Wp.Ctypes.c_object -> Wp.Ctypes.c_object -> bool
val merge : Wp.Ctypes.c_object -> Wp.Ctypes.c_object -> Wp.Ctypes.c_object
val hash : Wp.Ctypes.c_object -> int
val pretty : Format.formatter -> Wp.Ctypes.c_object -> unit
module C_object :
sig
type t = c_object
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
module AinfoComparable :
sig
type t = Wp.Ctypes.arrayinfo
val compare :
Wp.Ctypes.AinfoComparable.t -> Wp.Ctypes.AinfoComparable.t -> int
val equal :
Wp.Ctypes.AinfoComparable.t -> Wp.Ctypes.AinfoComparable.t -> bool
val hash : Wp.Ctypes.AinfoComparable.t -> int
end
val compare_ptr_conflated : Wp.Ctypes.c_object -> Wp.Ctypes.c_object -> int
end