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-30.0-Zinc.tar.gz

sha256=3ac0f995261ec829a7bd042bf70fc29ac6379029eb9df30bcc044748eb4d2a56

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

Module `Frama_c_kernel.Machdep`

Managing machine-dependent information.

Machdep

type mach = {

sizeof_short : int;
(*
sizeof(short)
*)
sizeof_int : int;
(*
sizeof(int)
*)
sizeof_long : int;
(*
sizeof(long)
*)
sizeof_longlong : int;
(*
sizeof(long long)
*)
sizeof_ptr : int;
(*
sizeof(<pointer type>)
*)
sizeof_float : int;
(*
sizeof(float)
*)
sizeof_double : int;
(*
sizeof(double)
*)
sizeof_longdouble : int;
(*
sizeof(long double)
*)
sizeof_void : int;
(*
sizeof(void)
*)
sizeof_fun : int;
(*
sizeof(<function type>). Negative if unsupported.
*)
size_t : string;
(*
Type of sizeof(<type>)
*)
ssize_t : string;
(*
representation of ssize_t
*)
wchar_t : string;
(*
Type of "wchar_t"
*)
ptrdiff_t : string;
(*
Type of "ptrdiff_t"
*)
intptr_t : string;
(*
Type of "intptr_t"
*)
uintptr_t : string;
(*
Type of "uintptr_t"
*)
int_fast8_t : string;
(*
Type of "int_fast8_t"
*)
int_fast16_t : string;
(*
Type of "int_fast16_t"
*)
int_fast32_t : string;
(*
Type of "int_fast32_t"
*)
int_fast64_t : string;
(*
Type of "int_fast64_t"
*)
uint_fast8_t : string;
(*
Type of "uint_fast8_t"
*)
uint_fast16_t : string;
(*
Type of "uint_fast16_t"
*)
uint_fast32_t : string;
(*
Type of "uint_fast32_t"
*)
uint_fast64_t : string;
(*
Type of "uint_fast64_t"
*)
wint_t : string;
(*
Type of "wint_t"
*)
sig_atomic_t : string;
(*
Type of "sig_atomic_t"
*)
time_t : string;
(*
Type of "time_t"
*)
alignof_short : int;
(*
_AlignOf(short)
*)
alignof_int : int;
(*
_AlignOf(int)
*)
alignof_long : int;
(*
_AlignOf(long)
*)
alignof_longlong : int;
(*
_AlignOf(long long)
*)
alignof_ptr : int;
(*
_AlignOf(<pointer type>)
*)
alignof_float : int;
(*
_AlignOf(float)
*)
alignof_double : int;
(*
_AlignOf(double)
*)
alignof_longdouble : int;
(*
_AlignOf(long double)
*)
alignof_str : int;
(*
_AlignOf(<string>)
*)
alignof_fun : int;
(*
_AlignOf(<function type>). Negative if unsupported.
*)
alignof_aligned : int;
(*
Alignment of a type with aligned attribute
*)
char_is_unsigned : bool;
(*
Whether "char" is unsigned
*)
little_endian : bool;
(*
whether the machine is little endian
*)
has__builtin_va_list : bool;
(*
Whether __builtin_va_list is a known type
*)
compiler : string;
(*
Architecture-specific flags to be given to the preprocessor (if supported)
*)
cpp_arch_flags : string list;
version : string;
(*
Information on this machdep
*)
weof : string;
(*
expansion of WEOF macro, empty if undefined
*)
wordsize : string;
(*
expansion of __WORDSIZE macro, empty if undefined
*)
posix_version : string;
(*
expansion of _POSIX_VERSION macro, empty if undefined
*)
bufsiz : string;
(*
expansion of BUFSIZ macro
*)
eof : string;
(*
expansion of EOF macro
*)
fopen_max : string;
(*
expansion of FOPEN_MAX macro
*)
filename_max : string;
(*
expansion of FILENAME_MAX macro
*)
host_name_max : string;
(*
expansion of HOST_NAME_MAX macro
*)
tty_name_max : string;
(*
expansion of TTY_NAME_MAX macro
*)
l_tmpnam : string;
(*
expansion of L_tmpnam macro
*)
path_max : string;
(*
expansion of PATH_MAX macro
*)
tmp_max : string;
(*
expansion of TMP_MAX macro
*)
rand_max : string;
(*
expansion of RAND_MAX macro
*)
mb_cur_max : string;
(*
expansion of MB_CUR_MAX macro
*)
nsig : string;
(*
expansion of non-standard NSIG macro, empty if undefined
*)
errno : (string * string) list;
(*
list of macros defining errors in errno.h
*)
machdep_name : string;
(*
name of the machdep
*)
custom_defs : (string * string) list;
(*
sequence of key/value for C macros
*)

}

Definition of a machine model (architecture + compiler).

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

since 30.0-Zinc

val mach_to_yaml : mach -> Yaml.value

val mach_of_yaml : Yaml.value -> (mach, [> `Msg of string ]) Stdlib.result

module Machdep : Datatype.S_with_collections with type t = mach

Compiler

val msvcMode : mach -> bool

Short for machdep.compiler = "msvc"

since 30.0-Zinc

val gccMode : mach -> bool

Short for machdep.compiler = "gcc"

since 30.0-Zinc

val allowed_machdep : string -> string

allowed_machdep "machdep family" provides a standard message for features only allowed for a particular machdep.

since 30.0-Zinc

Generation

val gen_all_defines : 
  Stdlib.Format.formatter ->
  ?censored_macros:Datatype.String.Set.t ->
  mach ->
  unit

Prints on the given formatter all #define directives required by share/libc/features.h and other system-dependent headers.

parameter censored_macros
prevents the generation of directives for the builtin macros in mach.custom_defs whose names match. empty by default.

before 29.0-Copper
censored_macros did not exist

val generate_machdep_header : 
  ?censored_macros:Datatype.String.Set.t ->
  mach ->
  Filepath.Normalized.t

generates a __fc_machdep.h file in a temp directory and returns the directory name, to be added to the search path for preprocessing stdlib.

parameter see
gen_all_defines

before 29.0-Copper
censored_macros did not exist.

On This Page

Machdep
Compiler
Generation