package frama-c

  1. Overview
  2. Docs
On This Page
  1. Utilities
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Wp.CtypesSource

C-Types

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

Runtime integers.

Sourcetype c_float =
  1. | Float32
  2. | Float64

Runtime floats.

Sourcetype 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.

Sourcetype arrayinfo = {
  1. arr_element : Frama_c_kernel.Cil_types.typ;
    (*

    type of the elements of the array

    *)
  2. arr_flat : arrayflat option;
}
Sourcetype 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.

Sourceval object_of_pointed : c_object -> c_object
Sourceval object_of_array_elem : c_object -> c_object
Sourceval object_of_logic_pointed : Frama_c_kernel.Cil_types.logic_type -> c_object

Utilities

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

memoized, not-projectified

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

memoized, not-projectified

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

Returns the type of char

Sourceval c_bool : unit -> c_int

Returns the type of int

Sourceval c_ptr : unit -> c_int

Returns the type of pointers

Conforms to Machine.theMachine

Conforms to Machine.theMachine

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

true if signed

domain, bounds included

Sourceval i_bits : c_int -> int

size in bits

Sourceval i_bytes : c_int -> int

size in bytes

Sourceval f_bits : c_float -> int

size in bits

Sourceval f_bytes : c_float -> int

size in bytes

Sourceval p_bits : unit -> int

pointer size in bits

Sourceval p_bytes : unit -> int

pointer size in bits

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

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

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

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

Sourceval i_convert : c_int -> c_int -> c_int
Sourceval f_convert : c_float -> c_float -> c_float
Sourceval promote : c_object -> c_object -> c_object
Sourceval pp_int : Format.formatter -> c_int -> unit
Sourceval pp_float : Format.formatter -> c_float -> unit
Sourceval pp_object : Format.formatter -> c_object -> unit
Sourceval i_name : c_int -> string
Sourceval f_name : c_float -> string
Sourceval basename : c_object -> string
Sourceval compare : c_object -> c_object -> int
Sourceval equal : c_object -> c_object -> bool
Sourceval hash : c_object -> int
Sourceval pretty : Format.formatter -> c_object -> unit
Sourcemodule AinfoComparable : sig ... end
Sourceval compare_c_int : c_int -> c_int -> int
Sourceval compare_c_float : c_float -> c_float -> int
Sourceval compare_ptr_conflated : c_object -> c_object -> int

same as compare but all PTR are considered the same

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct