Frama-C API - Ctypes
C-Types
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_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 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
val c_int : Frama_c_kernel.Cil_types.ikind -> c_int
Conforms to Machine.theMachine
val c_float : Frama_c_kernel.Cil_types.fkind -> c_float
Conforms to Machine.theMachine
val to_ikind : c_int -> Frama_c_kernel.Cil_types.ikind
val to_fkind : c_float -> Frama_c_kernel.Cil_types.fkind
val object_of : Frama_c_kernel.Cil_types.typ -> c_object
val object_to : c_object -> Frama_c_kernel.Cil_types.typ
val is_pointer : c_object -> bool
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
val bounds : c_int -> Frama_c_kernel.Integer.t * Frama_c_kernel.Integer.t
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 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_comp : c_object -> Frama_c_kernel.Cil_types.compinfo -> bool
val get_array_size : c_object -> int option
val get_array_dim : c_object -> int
val array_size : arrayinfo -> int option
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 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 hash : c_object -> int
val pretty : Stdlib.Format.formatter -> c_object -> unit
module C_object : Frama_c_kernel.Datatype.S with type t = c_object
module AinfoComparable : sig ... end