package frama-c

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

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

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 : Format.formatter -> c_int -> unit
val pp_float : Format.formatter -> c_float -> unit
val pp_object : 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 : 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

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