package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c.kernel/Frama_c_kernel/Machine/index.html

Module `Frama_c_kernel.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.

Sizeof getters

val sizeof_short : unit -> int

val sizeof_int : unit -> int

val sizeof_long : unit -> int

val sizeof_longlong : unit -> int

val sizeof_ptr : unit -> int

val sizeof_float : unit -> int

val sizeof_double : unit -> int

val sizeof_longdouble : unit -> int

val sizeof_void : unit -> int

val sizeof_fun : unit -> int

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

Alignof getters

val alignof_short : unit -> int

val alignof_int : unit -> int

val alignof_long : unit -> int

val alignof_longlong : unit -> int

val alignof_ptr : unit -> int

val alignof_float : unit -> int

val alignof_double : unit -> int

val alignof_longdouble : unit -> int

val alignof_str : unit -> int

val alignof_aligned : unit -> int

val alignof_fun : unit -> int

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

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

On This Page

State
Sizeof getters
Names getters
Alignof getters
Typ/kind getters
Expansions getters
Other getters
Compiler
Initializer
Forward references