Module Wp.Ctypes

C-Types

type c_int =
| CBool
| UInt8
| SInt8
| UInt16
| SInt16
| UInt32
| SInt32
| UInt64
| SInt64

Runtime integers.

type c_float =
| Float32
| Float64

Runtime floats.

type arrayflat = {
arr_size : int;(*

number of elements in the array

*)
arr_dim : int;(*

number of dimensions in the array

*)
arr_cell : Frama_c_kernel.Cil_types.typ;(*

type of elementary cells of the flatten array. Never an array.

*)
arr_cell_nbr : int64;(*

number of elementary cells in the flatten array

*)
}

Array objects, with both the head view and the flatten view.

type arrayinfo = {
arr_element : Frama_c_kernel.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 Frama_c_kernel.Cil_types.typ
| C_comp of Frama_c_kernel.Cil_types.compinfo
| C_array of arrayinfo

Type of variable, inits, field or assignable values. Abstract view of unrolled C types without attribute.

val object_of_pointed : c_object -> c_object
val object_of_array_elem : c_object -> c_object
val object_of_logic_type : Frama_c_kernel.Cil_types.logic_type -> c_object
val object_of_logic_pointed : Frama_c_kernel.Cil_types.logic_type -> c_object

Utilities

val i_iter : ( c_int -> unit ) -> unit
val f_iter : ( c_float -> unit ) -> unit
val i_memo : ( c_int -> 'a ) -> c_int -> 'a

memoized, not-projectified

val f_memo : ( c_float -> 'a ) -> c_float -> 'a

memoized, not-projectified

val is_char : c_int -> bool
val c_char : unit -> c_int

Returns the type of char

val c_bool : unit -> c_int

Returns the type of int

val c_ptr : unit -> c_int

Returns the type of pointers

Conforms to Cil.theMachine

Conforms to Cil.theMachine

val is_pointer : c_object -> bool
val char : char -> int64
val constant : Frama_c_kernel.Cil_types.exp -> int64
val get_int : Frama_c_kernel.Cil_types.exp -> int option
val get_int64 : Frama_c_kernel.Cil_types.exp -> int64 option
val signed : c_int -> bool

true if signed

domain, bounds included

val i_bits : c_int -> int

size in bits

val i_bytes : c_int -> int

size in bytes

val f_bits : c_float -> int

size in bits

val f_bytes : c_float -> int

size in bytes

val p_bits : unit -> int

pointer size in bits

val p_bytes : unit -> int

pointer size in bits

val sub_c_int : c_int -> c_int -> bool
val equal_float : c_float -> c_float -> bool
val sizeof_defined : c_object -> bool
val sizeof_object : c_object -> int
val bits_sizeof_comp : Frama_c_kernel.Cil_types.compinfo -> int
val bits_sizeof_array : arrayinfo -> int
val bits_sizeof_object : c_object -> int
val field_offset : Frama_c_kernel.Cil_types.fieldinfo -> int
val no_infinite_array : c_object -> bool
val is_compound : c_object -> bool
val is_array : c_object -> elt:c_object -> bool
val get_array : c_object -> (c_object * int option) option
val get_array_size : c_object -> int option
val get_array_dim : c_object -> int
val array_size : arrayinfo -> int option
val array_dimensions : arrayinfo -> c_object * int option list

Returns the list of dimensions the array consists of. None-dimension means undefined one.

val dimension_of_object : c_object -> (int * int64) option

Returns None for 1-dimension objects, and Some(d,N) for d-matrix with N cells

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 pp_int : Stdlib.Format.formatter -> c_int -> unit
val pp_float : Stdlib.Format.formatter -> c_float -> unit
val pp_object : Stdlib.Format.formatter -> c_object -> unit
val i_name : c_int -> string
val f_name : c_float -> string
val basename : c_object -> string
val compare : c_object -> c_object -> int
val equal : c_object -> c_object -> bool
val hash : c_object -> int
val pretty : Stdlib.Format.formatter -> c_object -> unit
module AinfoComparable : sig ... end
val compare_c_int : c_int -> c_int -> int
val compare_c_float : c_float -> c_float -> int
val compare_ptr_conflated : c_object -> c_object -> int

same as compare but all PTR are considered the same