make sizes of primitive types configurable with current machine as default
vogler opened this issue · 2 comments
Cil's defaults are generated from src/machdep-ml.c.in
and then stored in _build/machdep.ml
.
- make
Machdep.theMachine
configurable in goblint - provide default configurations {intel, arm} {32bit, 64bit} {linux, macOS}
Some more context from other comments:
Current generated machdep.ml
attached below.
Remove the msvc stuff, gcc
-> gcc_arm64_macos
, generate and add the same for x86_64_linux
etc.
theMachine
is already a reference, just need to set it from goblint to the current machine or option if provided (and then also pass it for preprocessing as mentioned by Michael above).
(* 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_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" *)
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_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 *)
const_string_literals: bool; (* Whether string literals have const chars *)
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 src/machdep-ml.c *)
version_major = 11;
version_minor = 1;
version = "11.1.0";
sizeof_short = 2;
sizeof_int = 4;
sizeof_bool = 1;
sizeof_long = 8;
sizeof_longlong = 8;
sizeof_ptr = 8;
sizeof_float = 4;
sizeof_double = 8;
sizeof_longdouble = 8;
sizeof_floatcomplex = 8;
sizeof_doublecomplex = 16;
sizeof_longdoublecomplex = 16;
sizeof_void = 1;
sizeof_fun = 1;
size_t = "unsigned long";
wchar_t = "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_double = 8;
alignof_longdouble = 8;
alignof_floatcomplex = 4;
alignof_doublecomplex = 8;
alignof_longdoublecomplex = 8;
alignof_str = 1;
alignof_fun = 4;
alignof_aligned = 16;
char_is_unsigned = false;
const_string_literals = true;
underscore_name = false;
__builtin_va_list = true;
__thread_is_keyword = true;
little_endian = true;
}
let hasMSVC = false
let msvc = gcc
let theMachine : mach ref = ref gcc
Originally posted by @vogler in #293 (comment)
That is true. Didn't go through the record, but hopefully all those things (or the ones we care about) are determined by your combination of OS+Arch+GCC which can be detected.
Originally posted by @vogler in #293 (comment)
For future reference, Frama-C contains a bunch of machdep definitions for different architectures: https://git.frama-c.com/pub/frama-c/-/blob/master/src/kernel_internals/runtime/machdeps.ml.