package goblint-cil

You can search for identifiers within the package.

in-package search v0.2.0

A front-end for the C programming language that facilitates program analysis and transformation

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (11)

Authors

Maintainers

Sources

goblint-cil-2.0.1.tbz

sha256=5f81cb3f25c09770e77b5eb4092e6621e456122b6d1219dcc304c062075f9572

sha512=31bb753031e0ef321a2ef065373009270881b1cce7f23167b378845188aed9cb49f18a165edd2e11f751f2c7a7b84ab5ac1da50ba1f5cb975e6e8a97157838ed

doc/src/goblint-cil/machdep.ml.html

Source file `machdep.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
# 1 "machdep.cppo.ml"
(* This module was generated automatically by code in Makefile and machdep-ml.c *)
type mach = {
  version_major: int;     (* Major version number *)
  version_minor: int;     (* Minor version number *)
  version: string;        (* gcc version string *)
  underscore_name: bool;  (* If assembly names have leading underscore *)
  sizeof_short: int;      (* Size of "short" *)
  sizeof_int: int;        (* Size of "int" *)
  sizeof_bool: int;       (* Size of "_Bool" *)
  sizeof_long: int ;      (* Size of "long" *)
  sizeof_longlong: int;   (* Size of "long long" *)
  sizeof_ptr: int;        (* Size of pointers *)
  sizeof_float: int;      (* Size of "float" *)
  sizeof_float32x: int;   (* Size of "_Float32x" *)
  sizeof_float64x: int;   (* Size of "_Float64x" *)
  sizeof_double: int;     (* Size of "double" *)
  sizeof_longdouble: int; (* Size of "long double" *)
  sizeof_floatcomplex: int;      (* Size of "float _Complex" *)
  sizeof_doublecomplex: int;     (* Size of "double _Complex" *)
  sizeof_longdoublecomplex: int; (* Size of "long double _Complex" *)
  sizeof_void: int;       (* Size of "void" *)
  sizeof_fun: int;        (* Size of function *)
  size_t: string;         (* Type of "sizeof(T)" *)
  wchar_t: string;        (* Type of "wchar_t" *)
  char16_t: string;       (* Type of "char16_t" *)
  char32_t: string;       (* Type of "char32_t" *)
  alignof_short: int;     (* Alignment of "short" *)
  alignof_int: int;       (* Alignment of "int" *)
  alignof_bool: int;      (* Alignment of "_Bool" *)
  alignof_long: int;      (* Alignment of "long" *)
  alignof_longlong: int;  (* Alignment of "long long" *)
  alignof_ptr: int;       (* Alignment of pointers *)
  alignof_enum: int;      (* Alignment of enum types *)
  alignof_float: int;     (* Alignment of "float" *)
  alignof_float32x: int;  (* Alignment of "_Float32x" *)
  alignof_float64x: int;  (* Alignment of "_Float64x" *)
  alignof_double: int;    (* Alignment of "double" *)
  alignof_longdouble: int;  (* Alignment of "long double" *)
  alignof_floatcomplex: int;     (* Alignment of "float _Complex" *)
  alignof_doublecomplex: int;    (* Alignment of "double _Complex" *)
  alignof_longdoublecomplex: int;  (* Alignment of "long double _Complex" *)
  alignof_str: int;       (* Alignment of strings *)
  alignof_fun: int;       (* Alignment of function *)
  alignof_aligned: int;   (* Alignment of anything with the "aligned" attribute *)
  char_is_unsigned: bool; (* Whether "char" is unsigned *)
  little_endian: bool; (* whether the machine is little endian *)
  __thread_is_keyword: bool; (* whether __thread is a keyword *)
  __builtin_va_list: bool; (* whether __builtin_va_list is builtin (gccism) *)
}

let gcc = {
(* Generated by code in machdep-ml.c *)
	 version_major    = 12;
	 version_minor    = 2;
	 version          = "12.2.0";
	 sizeof_short               = 2;
	 sizeof_int                 = 4;
	 sizeof_bool                = 1;
	 sizeof_long                = 8;
	 sizeof_longlong            = 8;
	 sizeof_ptr                 = 8;
	 sizeof_float               = 4;
	 sizeof_float32x            = 8;
	 sizeof_float64x            = 16;
	 sizeof_double              = 8;
	 sizeof_longdouble          = 16;
	 sizeof_floatcomplex        = 8;
	 sizeof_doublecomplex       = 16;
	 sizeof_longdoublecomplex   = 32;
	 sizeof_void                = 1;
	 sizeof_fun                 = 1;
	 size_t                     = "unsigned long";
	 wchar_t                    = "int";
	 char16_t                   = "unsigned short";
	 char32_t                   = "unsigned int";
	 alignof_short              = 2;
	 alignof_int                = 4;
	 alignof_bool               = 1;
	 alignof_long               = 8;
	 alignof_longlong           = 8;
	 alignof_ptr                = 8;
	 alignof_enum               = 4;
	 alignof_float              = 4;
	 alignof_float32x           = 8;
	 alignof_float64x           = 16;
	 alignof_double             = 8;
	 alignof_longdouble         = 16;
	 alignof_floatcomplex       = 4;
	 alignof_doublecomplex      = 8;
	 alignof_longdoublecomplex  = 16;
	 alignof_str                = 1;
	 alignof_fun                = 1;
	 alignof_aligned            = 16;
	 char_is_unsigned           = false;
	 underscore_name            = false;
	 __builtin_va_list          = true;
	 __thread_is_keyword        = true;
	 little_endian              = true;
# 54 "machdep.cppo.ml"
}
let theMachine : mach ref = ref gcc