Module Ctypes

module Ctypes: sig .. end
C-Types

module WpLog: Wp_parameters
type c_int = 
| UInt8
| SInt8
| UInt16
| SInt16
| UInt32
| SInt32
| UInt64
| SInt64
Runtime integers.
val compare_c_int : c_int -> c_int -> int
val signed : c_int -> bool
true if signed
val i_bits : c_int -> int
size in bits
val i_bytes : c_int -> int
size in bytes
val make_c_int : bool -> int -> c_int
val is_char : c_int -> bool
val c_int : Cil_types.ikind -> c_int
Conforms to
val c_int_bounds : c_int -> Integer.t * Integer.t
val c_int_all : c_int list
val c_bool : unit -> c_int
Returns the type of int
val c_char : unit -> c_int
Returns the type of char
val c_ptr : unit -> c_int
Returns the type of pointers
val sub_c_int : c_int -> c_int -> bool
type c_float = 
| Float32
| Float64
Runtime floats.
val compare_c_float : c_float -> c_float -> int
val f_bytes : c_float -> int
val f_bits : c_float -> int
val make_c_float : int -> c_float
val c_float : Cil_types.fkind -> c_float
Conforms to
val sub_c_float : c_float -> c_float -> bool
type arrayflat = {
   arr_size : int; (*
number of elements in the array
*)
   arr_dim : int; (*
number of dimensions in the array
*)
   arr_cell : Cil_types.typ; (*
type of elementary cells of the flatten array. Never an array.
*)
   arr_cell_nbr : int; (*
number of elementary cells in the flatten array
*)
}
Array objects, with both the head view and the flatten view.
type arrayinfo = {
   arr_element : Cil_types.typ; (*
type of the elements of the array
*)
   arr_flat : arrayflat option;
}
type c_object = 
| C_int of c_int
| C_float of c_float
| C_pointer of Cil_types.typ
| C_comp of Cil_types.compinfo
| C_array of arrayinfo
Type of variable, inits, field or assignable values.
val idx : c_int -> int
val imemo : (c_int -> 'a) -> c_int -> 'a
val fdx : c_float -> int
val fmemo : (c_float -> 'a) -> c_float -> 'a
val pp_int : Format.formatter -> c_int -> unit
val pp_float : Format.formatter -> c_float -> unit
val pp_object : Format.formatter -> c_object -> unit
val char : char -> int64
val constant : Cil_types.exp -> int64
val get_int : Cil_types.exp -> int64 option
val dimension : Cil_types.typ -> int * int64 * Cil_types.typ
val is_pointer : c_object -> bool
val is_void : Cil_types.typ -> bool
val object_of : Cil_types.typ -> c_object
val object_of_pointed : c_object -> c_object
val object_of_array_elem : c_object -> c_object
val object_of_logic_type : Cil_types.logic_type -> c_object
val object_of_logic_pointed : Cil_types.logic_type -> c_object
val no_infinite_array : c_object -> bool
val array_dim : arrayinfo -> c_object * int
val array_dimensions : arrayinfo -> c_object * int option list
Returns the list of dimensions the array consists of. None-dimension means undefined one.
val array_size : Cil_types.typ -> int option
val dimension_of_object : c_object -> (int * int) option
Returns None for 1-dimension objects, and Some(d,N) for d-matrix with N cells
val int64_max : Int64.t -> Int64.t -> Int64.t
val sizeof_object : c_object -> int
val sizeof_typ : Cil_types.typ -> int
val field_offset : Cil_types.fieldinfo -> int
val i_convert : c_int -> c_int -> c_int
val f_convert : c_float -> c_float -> c_float
val promote : c_object -> c_object -> c_object
val hsh : (c_object -> int) Pervasives.ref
val cmp : (c_object -> c_object -> int) Pervasives.ref
module AinfoComparable: sig .. end
val hash : c_object -> int
val equal : c_object -> c_object -> bool
val compare : c_object -> c_object -> int
val merge : c_object -> c_object -> c_object
val basename : c_object -> string
val pretty : Format.formatter -> c_object -> unit
module C_object: Datatype.Make(sig
type t = Ctypes.c_object 
val name : string
val rehash : 'a -> 'a
val structural_descr : Structural_descr.t
val reprs : Ctypes.c_object list
val equal : Ctypes.c_object -> Ctypes.c_object -> bool
val pretty : Format.formatter -> Ctypes.c_object -> unit
val hash : Ctypes.c_object -> int
val compare : Ctypes.c_object -> Ctypes.c_object -> int
val copy : 'a -> 'a
val internal_pretty_code : Type.precedence -> Format.formatter -> 'a -> unit
val mem_project : (Project_skeleton.t -> bool) -> 'a -> bool
val varname : 'a -> string
end)
val compare_ptr_conflated : c_object -> c_object -> int
same as Ctypes.compare but all PTR are considered the same
val compare_array_ptr_conflated : arrayinfo -> arrayinfo -> int