package frama-c

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

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_version : 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) ref

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

Deprecated access

type machine = private {
  1. mutable useLogicalOperators : bool;
    (*

    Whether to use the logical operands LAnd and LOr. By default, do not use them because they are unlike other expressions and do not evaluate both of their operands.

    *)
  2. mutable machdep : Machdep.mach;
    (*

    Machine.init will set this to the current machine description.

    *)
  3. mutable lowerConstants : bool;
    (*

    Do lower constants (default true)

    *)
  4. mutable insertImplicitCasts : bool;
    (*

    Do insert implicit casts (default true)

    *)
  5. mutable stringLiteralType : Cil_types.typ;
  6. mutable upointType : Cil_types.typ;
    (*

    An unsigned integer type that fits pointers.

    *)
  7. mutable upointKind : Cil_types.ikind;
    (*

    The integer kind of upointType.

    *)
  8. mutable wcharType : Cil_types.typ;
    (*

    An integer type that fits wchar_t.

    *)
  9. mutable wcharKind : Cil_types.ikind;
    (*

    The integer kind of wcharType.

    *)
  10. mutable ptrdiffType : Cil_types.typ;
    (*

    An integer type that fits ptrdiff_t.

    *)
  11. mutable ptrdiffKind : Cil_types.ikind;
    (*

    The integer kind of ptrdiffType.

    *)
  12. mutable typeOfSizeOf : Cil_types.typ;
    (*

    An integer type that is the type of sizeof.

    *)
  13. mutable kindOfSizeOf : Cil_types.ikind;
    (*

    The integer kind of typeOfSizeOf.

    *)
}
val theMachine : machine
  • deprecated Prefer using Machine functions
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