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