Frama-C:
Plug-ins:
Libraries:

Frama-C API - Machine

This module handle the machine configuration. Previous Frama-C versions handled this in Cil.

  • since 30.0-Zinc

State

val self : State.t

Internal state of the machine.

val is_computed : ?project:Project.t -> unit -> bool

Whether current project has set its machine description.

Names getters

val size_t : unit -> string
val ssize_t : unit -> string
val wchar_t : unit -> string
val ptrdiff_t : unit -> string
val intptr_t : unit -> string
val uintptr_t : unit -> string
val int_fast8_t : unit -> string
val int_fast16_t : unit -> string
val int_fast32_t : unit -> string
val int_fast64_t : unit -> string
val uint_fast8_t : unit -> string
val uint_fast16_t : unit -> string
val uint_fast32_t : unit -> string
val uint_fast64_t : unit -> string
val wint_t : unit -> string
val sig_atomic_t : unit -> string
val time_t : unit -> string

Types

module type SizeofInfo = sig ... end

sizeof getters

_Alignof and GCC __alignof__ getters

module type AlignofInfo = sig ... end

Typ/kind getters

val ptrdiff_kind : unit -> Cil_types.ikind
val ptrdiff_type : unit -> Cil_types.typ
val sizeof_kind : unit -> Cil_types.ikind
val sizeof_type : unit -> Cil_types.typ
val wchar_kind : unit -> Cil_types.ikind
val wchar_type : unit -> Cil_types.typ
val uintptr_kind : unit -> Cil_types.ikind
val uintptr_type : unit -> Cil_types.typ
val string_literal_type : unit -> Cil_types.typ

Expansions getters

val weof : unit -> string
val wordsize : unit -> string
val posix_c_source : unit -> string
val bufsiz : unit -> string
val eof : unit -> string
val fopen_max : unit -> string
val filename_max : unit -> string
val host_name_max : unit -> string
val tty_name_max : unit -> string
val l_tmpnam : unit -> string
val path_max : unit -> string
val tmp_max : unit -> string
val rand_max : unit -> string
val mb_cur_max : unit -> string
val nsig : unit -> string

Other getters

val version : unit -> string
val compiler : unit -> string
val machdep_name : unit -> string
val get_machdep : unit -> Machdep.mach
val char_is_unsigned : unit -> bool
val little_endian : unit -> bool
val has_builtin_va_list : unit -> bool
val cpp_arch_flags : unit -> string list
val errno : unit -> (string * string) list
val custom_defs : unit -> (string * string) list
val use_logical_operators : unit -> bool
val lower_constants : unit -> bool
val insert_implicit_casts : unit -> bool
val max_extended_alignment : unit -> int

-1 if the platform does not support extended alignments

  • since 32.0-Germanium

Compiler

val msvcMode : unit -> bool

Short for Machdep.msvcMode (get_machdep ())

  • since 30.0-Zinc
val gccMode : unit -> bool

Short for Machdep.gccMode (get_machdep ())

  • since 30.0-Zinc
val acceptEmptyCompinfo : unit -> bool

whether we accept empty struct. Implied by msvcMode and gccMode, and can be forced by set_acceptEmptyCompinfo otherwise.

  • since 30.0-Zinc
val set_acceptEmptyCompinfo : unit -> unit

After a call to this function, empty compinfos are allowed by the kernel, this must be used as a configuration step equivalent to a machdep, except that it is not a user configuration.

Note that if the selected machdep is GCC or MSVC, this call has no effect as these modes already allow empty compinfos.

  • since 30.0-Zinc

Initializer

val init : initLogicBuiltins:(unit -> unit) -> Machdep.mach -> unit

Call this function to perform some initialization, and only after you have set msvcMode. initLogicBuiltins is the function to call to init logic builtins. The Machdep argument is a description of the hardware platform and of the compiler used.

Forward references

val init_builtins_ref : (unit -> unit) Stdlib.ref

Unless your name is Cil_builtins, you should not call this.

  • alert machine_init_builtins_ref This function can only be called by Cil_builtins

Deprecated functions

val sizeof_short : unit -> int
  • deprecated Use Sizeof.short instead
val sizeof_int : unit -> int
  • deprecated Use Sizeof.int instead
val sizeof_long : unit -> int
  • deprecated Use Sizeof.long instead
val sizeof_longlong : unit -> int
  • deprecated Use Sizeof.longlong instead
val sizeof_ptr : unit -> int
  • deprecated Use Sizeof.ptr instead
val sizeof_float : unit -> int
  • deprecated Use Sizeof.float instead
val sizeof_double : unit -> int
  • deprecated Use Sizeof.double instead
val sizeof_longdouble : unit -> int
  • deprecated Use Sizeof.longdouble instead
val sizeof_void : unit -> int
  • deprecated Use Sizeof.void instead
val sizeof_fun : unit -> int
  • deprecated Use Sizeof.func instead
val alignof_short : unit -> int
  • deprecated Use Alignof.short instead
val alignof_int : unit -> int
  • deprecated Use Alignof.int instead
val alignof_long : unit -> int
  • deprecated Use Alignof.long instead
val alignof_longlong : unit -> int
  • deprecated Use Alignof.longlong instead
val alignof_ptr : unit -> int
  • deprecated Use Alignof.ptr instead
val alignof_float : unit -> int
  • deprecated Use Alignof.float instead
val alignof_double : unit -> int
  • deprecated Use Alignof.double instead
val alignof_longdouble : unit -> int
  • deprecated Use Alignof.longdouble instead
val alignof_void : unit -> int
  • deprecated Use Alignof.void instead
val alignof_fun : unit -> int
  • deprecated Use Alignof.func instead
val alignof_aligned : unit -> int
  • deprecated Use Alignof.aligned instead