package frama-c

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

Managing machine-dependent information.

Machdep

type mach = {
  1. sizeof_short : int;
    (*

    sizeof(short)

    *)
  2. sizeof_int : int;
    (*

    sizeof(int)

    *)
  3. sizeof_long : int;
    (*

    sizeof(long)

    *)
  4. sizeof_longlong : int;
    (*

    sizeof(long long)

    *)
  5. sizeof_ptr : int;
    (*

    sizeof(<pointer type>)

    *)
  6. sizeof_float : int;
    (*

    sizeof(float)

    *)
  7. sizeof_double : int;
    (*

    sizeof(double)

    *)
  8. sizeof_longdouble : int;
    (*

    sizeof(long double)

    *)
  9. sizeof_void : int;
    (*

    sizeof(void)

    *)
  10. sizeof_fun : int;
    (*

    sizeof(<function type>). Negative if unsupported.

    *)
  11. size_t : string;
    (*

    Type of sizeof(<type>)

    *)
  12. ssize_t : string;
    (*

    representation of ssize_t

    *)
  13. wchar_t : string;
    (*

    Type of "wchar_t"

    *)
  14. ptrdiff_t : string;
    (*

    Type of "ptrdiff_t"

    *)
  15. intptr_t : string;
    (*

    Type of "intptr_t"

    *)
  16. uintptr_t : string;
    (*

    Type of "uintptr_t"

    *)
  17. int_fast8_t : string;
    (*

    Type of "int_fast8_t"

    *)
  18. int_fast16_t : string;
    (*

    Type of "int_fast16_t"

    *)
  19. int_fast32_t : string;
    (*

    Type of "int_fast32_t"

    *)
  20. int_fast64_t : string;
    (*

    Type of "int_fast64_t"

    *)
  21. uint_fast8_t : string;
    (*

    Type of "uint_fast8_t"

    *)
  22. uint_fast16_t : string;
    (*

    Type of "uint_fast16_t"

    *)
  23. uint_fast32_t : string;
    (*

    Type of "uint_fast32_t"

    *)
  24. uint_fast64_t : string;
    (*

    Type of "uint_fast64_t"

    *)
  25. wint_t : string;
    (*

    Type of "wint_t"

    *)
  26. sig_atomic_t : string;
    (*

    Type of "sig_atomic_t"

    *)
  27. time_t : string;
    (*

    Type of "time_t"

    *)
  28. alignof_short : int;
    (*

    _AlignOf(short)

    *)
  29. alignof_int : int;
    (*

    _AlignOf(int)

    *)
  30. alignof_long : int;
    (*

    _AlignOf(long)

    *)
  31. alignof_longlong : int;
    (*

    _AlignOf(long long)

    *)
  32. alignof_ptr : int;
    (*

    _AlignOf(<pointer type>)

    *)
  33. alignof_float : int;
    (*

    _AlignOf(float)

    *)
  34. alignof_double : int;
    (*

    _AlignOf(double)

    *)
  35. alignof_longdouble : int;
    (*

    _AlignOf(long double)

    *)
  36. alignof_str : int;
    (*

    _AlignOf(<string>)

    *)
  37. alignof_fun : int;
    (*

    _AlignOf(<function type>). Negative if unsupported.

    *)
  38. alignof_aligned : int;
    (*

    Alignment of a type with aligned attribute

    *)
  39. char_is_unsigned : bool;
    (*

    Whether "char" is unsigned

    *)
  40. little_endian : bool;
    (*

    whether the machine is little endian

    *)
  41. has__builtin_va_list : bool;
    (*

    Whether __builtin_va_list is a known type

    *)
  42. compiler : string;
    (*

    Architecture-specific flags to be given to the preprocessor (if supported)

    *)
  43. cpp_arch_flags : string list;
  44. version : string;
    (*

    Information on this machdep

    *)
  45. weof : string;
    (*

    expansion of WEOF macro, empty if undefined

    *)
  46. wordsize : string;
    (*

    expansion of __WORDSIZE macro, empty if undefined

    *)
  47. posix_version : string;
    (*

    expansion of _POSIX_VERSION macro, empty if undefined

    *)
  48. bufsiz : string;
    (*

    expansion of BUFSIZ macro

    *)
  49. eof : string;
    (*

    expansion of EOF macro

    *)
  50. fopen_max : string;
    (*

    expansion of FOPEN_MAX macro

    *)
  51. filename_max : string;
    (*

    expansion of FILENAME_MAX macro

    *)
  52. host_name_max : string;
    (*

    expansion of HOST_NAME_MAX macro

    *)
  53. tty_name_max : string;
    (*

    expansion of TTY_NAME_MAX macro

    *)
  54. l_tmpnam : string;
    (*

    expansion of L_tmpnam macro

    *)
  55. path_max : string;
    (*

    expansion of PATH_MAX macro

    *)
  56. tmp_max : string;
    (*

    expansion of TMP_MAX macro

    *)
  57. rand_max : string;
    (*

    expansion of RAND_MAX macro

    *)
  58. mb_cur_max : string;
    (*

    expansion of MB_CUR_MAX macro

    *)
  59. nsig : string;
    (*

    expansion of non-standard NSIG macro, empty if undefined

    *)
  60. errno : (string * string) list;
    (*

    list of macros defining errors in errno.h

    *)
  61. machdep_name : string;
    (*

    name of the machdep

    *)
  62. custom_defs : (string * string) list;
    (*

    sequence of key/value for C macros

    *)
}

Definition of a machine model (architecture + compiler).

  • since 30.0-Zinc
val mach_to_yaml : mach -> Yaml.value
val mach_of_yaml : Yaml.value -> mach Yaml.res

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 : 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.

  • before 29.0-Copper

    censored_macros did not exist.

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