Frama-C:
Plug-ins:
Libraries:

Frama-C API - Ctypes

C-Types

type c_int =
  1. | CBool
  2. | UInt8
  3. | SInt8
  4. | UInt16
  5. | SInt16
  6. | UInt32
  7. | SInt32
  8. | UInt64
  9. | SInt64

Runtime integers.

type c_float =
  1. | Float32
  2. | Float64

Runtime floats.

type arrayflat = {
  1. arr_size : int;
    (*

    number of elements in the array

    *)
  2. arr_dim : int;
    (*

    number of dimensions in the array

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

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

    *)
  4. 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 = {
  1. arr_element : Frama_c_kernel.Cil_types.typ;
    (*

    type of the elements of the array

    *)
  2. arr_flat : arrayflat option;
}
type c_object =
  1. | C_int of c_int
  2. | C_float of c_float
  3. | C_pointer of Frama_c_kernel.Cil_types.typ
  4. | C_comp of Frama_c_kernel.Cil_types.compinfo
  5. | 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 Machine.theMachine

Conforms to Machine.theMachine

  • raises Not_found
  • raises Not_found
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