diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 5e81e4c5acbbe5a1a3b63694c770ce232b130838..770627e22ec1fc35553ea74e5755bdbd1fb2d24d 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -3206,9 +3206,9 @@ We present below a thorough description of each field.
\item[\texttt{compiler}]: defines whether special compiler-specific extensions
will be enabled. It should be one of the strings below:
\begin{itemize}
- \item[\texttt{msvc}]: enables \verb+Cil.msvcMode+, that is,
+ \item[\texttt{msvc}]: enables \verb+Machine.msvcMode+, that is,
MSVC (Visual Studio)-specific extensions;
- \item[\texttt{gcc}]: enables \verb+Cil.gccMode+, that is,
+ \item[\texttt{gcc}]: enables \verb+Machine.gccMode+, that is,
GCC-specific extensions;
\item[\texttt{generic}] (or any other string): no special
compiler-specific extensions.
diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 89dbe33f7d5e5467fd8fe0435d48c6b50a7c882d..6acfc8312b27e7d2505c3b392ccdd9a4c12b0fc4 100644
--- a/src/kernel_internals/parsing/clexer.mll
+++ b/src/kernel_internals/parsing/clexer.mll
@@ -116,7 +116,7 @@ let thread_keyword () =
let wkey = Kernel.wkey_conditional_feature in
let s = "__thread is a GCC extension, use a GCC-based machdep to enable it" in
let warning () = Kernel.warning ~wkey "%s" s ; IDENT "__thread" in
- add "__thread" (fun loc -> if Cil.gccMode () then THREAD loc else warning ())
+ add "__thread" (fun loc -> if Machine.gccMode () then THREAD loc else warning ())
let filename_keyword () =
let convert acc c = int64_of_char c :: acc in
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 414df24d4048e6e7e8500351b1241c00dc86f700..f6d7ffc1b679ebb7ff1f5759fdd3b1fbf134f34f 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -239,7 +239,7 @@ let sizeofType () =
else
Kernel.fatal
~current:true
- "initCIL: cannot find the right specifier for type %s" name
+ "Cparser.sizeofType: cannot find the right specifier for type %s" name
in
let add_one_specifier s acc =
(Cabs.SpecType (convert_one_specifier s)) :: acc
@@ -247,7 +247,7 @@ let sizeofType () =
let specs = Str.split (Str.regexp " +") name in
List.fold_right add_one_specifier specs []
in
- findSpecifier Cil.theMachine.Cil.theMachine.Cil_types.size_t
+ findSpecifier (Machine.size_t ())
(*
diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml
index e65d13d8169ef81b0cfa6c05f07d0d2068ca7fbd..243e63c4964ba05726d7770b6733fb06462e69db 100644
--- a/src/kernel_internals/runtime/machdep.ml
+++ b/src/kernel_internals/runtime/machdep.ml
@@ -20,7 +20,258 @@
(* *)
(**************************************************************************)
-open Cil_types
+let yaml_dict_to_list = function
+ | `O l ->
+ let make_one acc (k,v) =
+ Result.(
+ bind acc
+ (fun l ->
+ match Yaml.Util.to_string v with
+ | Ok s -> Ok((k,s) :: l)
+ | Error (`Msg s) ->
+ Error (`Msg ("Unexpected value for key " ^ k ^ ": " ^ s))))
+ in
+ List.fold_left make_one (Ok []) l
+ | _ -> Error (`Msg "Unexpected YAML value instead of dictionary of strings")
+
+type mach = {
+ sizeof_short: int;
+ sizeof_int: int;
+ sizeof_long: int;
+ sizeof_longlong: int;
+ sizeof_ptr: int;
+ sizeof_float: int;
+ sizeof_double: int;
+ sizeof_longdouble: int;
+ sizeof_void: int;
+ sizeof_fun: int;
+ size_t: string;
+ ssize_t: string;
+ wchar_t: string;
+ ptrdiff_t: string;
+ intptr_t: string;
+ uintptr_t: string;
+ int_fast8_t: string;
+ int_fast16_t: string;
+ int_fast32_t: string;
+ int_fast64_t: string;
+ uint_fast8_t: string;
+ uint_fast16_t: string;
+ uint_fast32_t: string;
+ uint_fast64_t: string;
+ wint_t: string;
+ sig_atomic_t: string;
+ time_t: string;
+ alignof_short: int;
+ alignof_int: int;
+ alignof_long: int;
+ alignof_longlong: int;
+ alignof_ptr: int;
+ alignof_float: int;
+ alignof_double: int;
+ alignof_longdouble: int;
+ alignof_str: int;
+ alignof_fun: int;
+ alignof_aligned: int;
+ char_is_unsigned: bool;
+ little_endian: bool;
+ has__builtin_va_list: bool;
+ compiler: string;
+ cpp_arch_flags: string list;
+ version: string;
+ weof: string;
+ wordsize: string;
+ posix_version: string;
+ bufsiz: string;
+ eof: string;
+ fopen_max: string;
+ filename_max: string;
+ host_name_max: string;
+ tty_name_max: string;
+ l_tmpnam: string;
+ path_max: string;
+ tmp_max: string;
+ rand_max: string;
+ mb_cur_max: string;
+ nsig: string;
+ errno: (string * string) list [@of_yaml yaml_dict_to_list];
+ machdep_name: string;
+ custom_defs: (string * string) list [@of_yaml yaml_dict_to_list];
+} [@@deriving yaml]
+
+let dummy = {
+ sizeof_short = 2;
+ sizeof_int = 4;
+ sizeof_long = 8;
+ sizeof_longlong = 8;
+ sizeof_ptr = 8;
+ sizeof_float = 4;
+ sizeof_double = 8;
+ sizeof_longdouble = 16;
+ sizeof_void = -1;
+ sizeof_fun = -1;
+ size_t = "unsigned long";
+ ssize_t = "long";
+ wchar_t = "int";
+ ptrdiff_t = "long";
+ intptr_t = "long";
+ uintptr_t = "unsigned long";
+ int_fast8_t = "signed char";
+ int_fast16_t = "long";
+ int_fast32_t = "long";
+ int_fast64_t = "long";
+ uint_fast8_t = "unsigned char";
+ uint_fast16_t = "unsigned long";
+ uint_fast32_t = "unsigned long";
+ uint_fast64_t = "unsigned long";
+ wint_t = "int";
+ sig_atomic_t = "int";
+ time_t = "long";
+ alignof_short = 2;
+ alignof_int = 4;
+ alignof_long = 8;
+ alignof_longlong = 8;
+ alignof_ptr = 8;
+ alignof_float = 4;
+ alignof_double = 8;
+ alignof_longdouble = 16;
+ alignof_str = 1;
+ alignof_fun = -1;
+ alignof_aligned = 16;
+ char_is_unsigned = true;
+ little_endian = true;
+ has__builtin_va_list = true;
+ compiler = "none";
+ cpp_arch_flags = [];
+ version = "N/A";
+ weof = "(-1)";
+ wordsize = "64";
+ posix_version = "";
+ bufsiz = "255";
+ eof = "(-1)";
+ fopen_max = "255";
+ filename_max = "4095";
+ path_max = "256";
+ tty_name_max = "255";
+ host_name_max = "255";
+ l_tmpnam = "63";
+ tmp_max = "1024";
+ rand_max = "0xFFFFFFFE";
+ mb_cur_max = "16";
+ nsig = "";
+ errno = [
+ "edom", "33";
+ "eilseq", "84";
+ "erange", "34";
+ ];
+ machdep_name = "dummy";
+ custom_defs = [];
+}
+
+module Machdep = struct
+
+ include Datatype.Make_with_collections(struct
+ include Datatype.Serializable_undefined
+ type t = mach
+ let name = "Machdep"
+ let reprs = [dummy]
+ let compare: t -> t -> int = Stdlib.compare
+ let equal: t -> t -> bool = (=)
+ let hash: t -> int = Hashtbl.hash
+ let copy = Datatype.identity
+ end)
+
+ let pretty fmt mach =
+ let open Format in
+ let pp_pair fmt (a, b) = fprintf fmt "(%s, %s)" a b in
+ fprintf fmt
+ "{sizeof_short=%d;sizeof_int=%d;sizeof_long=%d;sizeof_longlong=%d;\
+ sizeof_ptr=%d;sizeof_float=%d;sizeof_double=%d;sizeof_longdouble=%d;\
+ sizeof_void=%d;sizeof_fun=%d;size_t=%s;ssize_t=%s;wchar_t=%s;
+ ptrdiff_t=%s;intptr_t=%s;uintptr_t=%s;\
+ int_fast8_t=%s;int_fast16_t=%s;int_fast32_t=%s;int_fast64_t=%s;\
+ uint_fast8_t=%s;uint_fast16_t=%s;uint_fast32_t=%s;uint_fast64_t=%s;\
+ wint_t=%s;sig_atomic_t=%s;time_t=%s;\
+ alignof_short=%d;alignof_int=%d;alignof_long=%d;alignof_longlong=%d;\
+ alignof_ptr=%d;alignof_float=%d;alignof_double=%d;alignof_longdouble=%d;\
+ alignof_str=%d;alignof_fun=%d;alignof_aligned=%d;\
+ char_is_unsigned=%b;little_endian=%b;has__builtin_va_list=%b;
+ compiler=%s;cpp_arch_flags=%a;version=%s;weof=%s;wordsize=%s;
+ posix_version=%s;bufsiz=%s;eof=%s;fopen_max=%s;filename_max=%s;
+ path_max=%s;tty_name_max=%s;host_name_max=%s;l_tmpnam=%s;tmp_max=%s;\
+ rand_max=%s;mb_cur_max=%s;nsig=%s;errno=%a;machdep_name=%s;custom_defs=%a}"
+ mach.sizeof_short
+ mach.sizeof_int
+ mach.sizeof_long
+ mach.sizeof_longlong
+ mach.sizeof_ptr
+ mach.sizeof_float
+ mach.sizeof_double
+ mach.sizeof_longdouble
+ mach.sizeof_void
+ mach.sizeof_fun
+ mach.size_t
+ mach.ssize_t
+ mach.wchar_t
+ mach.ptrdiff_t
+ mach.intptr_t
+ mach.uintptr_t
+ mach.int_fast8_t
+ mach.int_fast16_t
+ mach.int_fast32_t
+ mach.int_fast64_t
+ mach.uint_fast8_t
+ mach.uint_fast16_t
+ mach.uint_fast32_t
+ mach.uint_fast64_t
+ mach.wint_t
+ mach.sig_atomic_t
+ mach.time_t
+ mach.alignof_short
+ mach.alignof_int
+ mach.alignof_long
+ mach.alignof_longlong
+ mach.alignof_ptr
+ mach.alignof_float
+ mach.alignof_double
+ mach.alignof_longdouble
+ mach.alignof_str
+ mach.alignof_fun
+ mach.alignof_aligned
+ mach.char_is_unsigned
+ mach.little_endian
+ mach.has__builtin_va_list
+ mach.compiler
+ (pp_print_list pp_print_string) mach.cpp_arch_flags
+ mach.version
+ mach.weof
+ mach.wordsize
+ mach.posix_version
+ mach.bufsiz
+ mach.eof
+ mach.fopen_max
+ mach.filename_max
+ mach.path_max
+ mach.tty_name_max
+ mach.host_name_max
+ mach.l_tmpnam
+ mach.tmp_max
+ mach.rand_max
+ mach.mb_cur_max
+ mach.nsig
+ (pp_print_list pp_pair) mach.errno
+ mach.machdep_name
+ (pp_print_list pp_pair) mach.custom_defs
+end
+
+let msvcMode machdep = machdep.compiler = "msvc"
+let gccMode machdep = machdep.compiler = "gcc" || machdep.compiler = "clang"
+
+let allowed_machdep machdep =
+ Format.asprintf
+ "only allowed for %s machdeps; see option -machdep or \
+ run 'frama-c -machdep help' for the list of available machdeps"
+ machdep
let gen_define fmt macro pp def =
Format.fprintf fmt "#define %s %a@\n" macro pp def
@@ -350,8 +601,7 @@ let gen_all_defines fmt ?(censored_macros=Datatype.String.Set.empty) mach =
List.iter (gen_define_errno_macro fmt) mach.errno;
gen_define_macro fmt "__FC_TIME_T" mach.time_t;
gen_define_macro fmt "__FC_NSIG" mach.nsig;
- (* NB: should we use Cil.gccMode() here? *)
- if mach.compiler = "gcc" then
+ if gccMode mach then
gen_include fmt "__fc_gcc_builtins.h";
gen_define_custom_macros fmt censored_macros mach.custom_defs;
diff --git a/src/kernel_internals/runtime/machdep.mli b/src/kernel_internals/runtime/machdep.mli
index d84b3bed6003f44bb8e9583bb20bc2aea535acfa..01b77696b6e5eaa199d08e3129d36894f4b29d00 100644
--- a/src/kernel_internals/runtime/machdep.mli
+++ b/src/kernel_internals/runtime/machdep.mli
@@ -22,6 +22,103 @@
(** Managing machine-dependent information. *)
+(* ***********************************************************************)
+(** {2 Machdep} *)
+(* ***********************************************************************)
+
+(** Definition of a machine model (architecture + compiler).
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
+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 being used. Currently recognized names are 'gcc', 'msvc' and 'generic'. *)
+ 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 *)
+} [@@deriving yaml]
+(** @since Frama-C+dev *)
+
+module Machdep: Datatype.S_with_collections with type t = mach
+(** @since Frama-C+dev *)
+
+(* ***********************************************************************)
+(** {2 Compiler } *)
+(* ***********************************************************************)
+
+val msvcMode: mach -> bool
+(** Short for [machdep.compiler = "msvc"]
+ @since Frama-C+dev *)
+
+val gccMode: mach -> bool
+(** Short for [machdep.compiler = "gcc"]
+ @since Frama-C+dev *)
+
+val allowed_machdep: string -> string
+(** [allowed_machdep "machdep family"] provides a standard message for features
+ only allowed for a particular machdep.
+ @since Frama-C+dev *)
+
+(* ***********************************************************************)
+(** {2 Generation } *)
+(* ***********************************************************************)
(** Prints on the given formatter all [#define] directives
required by [share/libc/features.h] and other system-dependent headers.
@@ -30,10 +127,7 @@
@before 29.0-Copper censored_macros did not exist
*)
val gen_all_defines:
- Format.formatter ->
- ?censored_macros:Datatype.String.Set.t ->
- Cil_types.mach ->
- unit
+ Format.formatter -> ?censored_macros:Datatype.String.Set.t -> mach -> unit
(** 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.
@@ -41,6 +135,4 @@ val gen_all_defines:
@before 29.0-Copper censored_macros did not exist.
*)
val generate_machdep_header:
- ?censored_macros:Datatype.String.Set.t ->
- Cil_types.mach ->
- Filepath.Normalized.t
+ ?censored_macros:Datatype.String.Set.t -> mach -> Filepath.Normalized.t
diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index d888e026716f7371c4ad6c5ec839af847ee34e26..73a2a2275c3d5b8fc7de3b38eb01ba70616d28d8 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -269,7 +269,7 @@ let warn_if_another_compiler_builtin name =
Kernel.warning ~wkey:Kernel.wkey_implicit_function_declaration
~current:true ~once:true
"%s is a compiler builtin, %s" name
- (Cil.allowed_machdep (Cil_builtins.string_of_compiler compiler));
+ (Machdep.allowed_machdep (Cil_builtins.string_of_compiler compiler));
true
with Not_found -> false
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 6c2cd09b4ae3b7d7309a91cddaa17d97c76b9915..1753414b85b25a9e1a7bcbe0fb05360a7dce6e97 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -367,7 +367,7 @@ let pragma_align_by_struct = H.create 17
let process_align_pragma name args =
let aux pname v =
- (if Cil.msvcMode () || Cil.gccMode ()
+ (if Machine.(msvcMode () || gccMode ())
then Kernel.warning ?wkey:None else Kernel.debug ~level:1 ?dkey:None)
~current:true "Parsing ICC '%s' pragma." pname;
match args with
@@ -404,7 +404,7 @@ let packing_pragma_stack = Stack.create ()
let current_packing_pragma = ref None
let pretty_current_packing_pragma fmt =
let align =
- Option.value ~default:(Integer.of_int theMachine.theMachine.alignof_aligned)
+ Option.value ~default:(Integer.of_int (Machine.alignof_aligned ()))
!current_packing_pragma
in
Integer.pretty fmt align
@@ -420,7 +420,7 @@ let pretty_current_packing_pragma fmt =
with such pragmas, we emulate GCC's current behavior but emit a warning.
This is the only case when this function returns [None]. *)
let get_valid_pragma_pack_alignment n =
- if Integer.is_zero n && Cil.gccMode () then begin
+ if Integer.is_zero n && Machine.gccMode () then begin
Kernel.warning ~current:true "GCC accepts pack(0) but does not specify its \
behavior; considering it equivalent to pack()";
true, None
@@ -442,7 +442,7 @@ let process_pack_pragma name args =
| [ACons ("",[])] (* #pragma pack() *) ->
Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true
"packing pragma: restoring alignment to default (%d)"
- theMachine.theMachine.alignof_aligned;
+ (Machine.alignof_aligned ());
current_packing_pragma := None; None
| [AInt n] (* #pragma pack(n) *) ->
let is_valid, new_pragma = get_valid_pragma_pack_alignment n in
@@ -518,7 +518,7 @@ let is_power_of_two i = i > 0 && i land (i-1) = 0
also return [None]. *)
let eval_aligned_attrparams aps =
match aps with
- | [] -> Some (Integer.of_int theMachine.theMachine.alignof_aligned)
+ | [] -> Some (Integer.of_int (Machine.alignof_aligned ()))
| [ap] ->
begin
match Cil.intOfAttrparam ap with
@@ -560,7 +560,7 @@ let warn_incompatible_pragmas_attributes apragma has_attrs =
Kernel.warning ~current:true ~once:true
"ignoring 'align' pragma due to presence of 'pack' pragma.@ \
No compiler was supposed to accept both syntaxes.";
- if Cil.msvcMode () && has_attrs then
+ if Machine.msvcMode () && has_attrs then
(* MSVC does not allow attributes *)
Kernel.warning ~current:true ~once:true
"field attributes should not be present in MSVC-compatible sources"
@@ -651,7 +651,7 @@ let process_pragmas_pack_align_field_attributes fi fattrs cattr =
if Cil.isUnsizedArrayType fi.ftype
then
(* flexible array member: use size of pointer *)
- Cil.bitsSizeOf theMachine.upointType
+ Cil.bitsSizeOf (Machine.uintptr_type ())
else
Cil.bytesSizeOf fi.ftype
in
@@ -712,11 +712,11 @@ let convLoc (l : cabsloc) =
l
let isOldStyleVarArgName n =
- if Cil.msvcMode () then n = "va_alist"
+ if Machine.msvcMode () then n = "va_alist"
else n = "__builtin_va_alist"
let isOldStyleVarArgTypeName n =
- if Cil.msvcMode () then n = "va_list" || n = "__ccured_va_list"
+ if Machine.msvcMode () then n = "va_list" || n = "__ccured_va_list"
else n = "__builtin_va_alist_t"
(* CERT EXP 46 rule: operands of bitwise operators should not be of type _Bool
@@ -1390,13 +1390,13 @@ let canDropStatement (s: stmt) : bool =
!pRes
let fail_if_incompatible_sizeof ~ensure_complete op typ =
- if Cil.isFunctionType typ && Cil.theMachine.theMachine.sizeof_fun < 0 then
+ if Cil.isFunctionType typ && Machine.sizeof_fun () < 0 then
Kernel.error ~current:true "%s called on function %s" op
- (Cil.allowed_machdep "GCC");
+ (Machdep.allowed_machdep "GCC");
let is_void = Cil.isVoidType typ in
- if is_void && Cil.theMachine.theMachine.sizeof_void < 0 then
+ if is_void && Machine.sizeof_void () < 0 then
Kernel.error ~current:true "%s on void type %s" op
- (Cil.allowed_machdep "GCC/MSVC");
+ (Machdep.allowed_machdep "GCC/MSVC");
if ensure_complete && not (Cil.isCompleteType typ) && not is_void then
Kernel.error ~current:true
"%s on incomplete type '%a'" op Cil_datatype.Typ.pretty typ
@@ -2166,7 +2166,7 @@ struct
was too big *)
let e' = mkCast ~newt:t e in
let constFold = constFold true in
- let e'' = if theMachine.lowerConstants then constFold e' else e' in
+ let e'' = if Machine.lower_constants () then constFold e' else e' in
(match constFoldToInt e, constFoldToInt e'' with
| Some i1, Some i2 when not (Integer.equal i1 i2) ->
Kernel.feedback ~once:true ~source:(fst e.eloc)
@@ -2844,7 +2844,7 @@ let memoBuiltin ?force_keep ?spec name proto =
let vla_alloc_fun () =
let size_arg =
- Cil.makeVarinfo false true "size" theMachine.typeOfSizeOf
+ Cil.makeVarinfo false true "size" (Machine.sizeof_type ())
in
let res_iterm =
Logic_const.new_identified_term
@@ -2929,9 +2929,9 @@ let rec _pp_preInit fmt = function
(* special case for treating GNU extension on empty compound initializers. *)
let empty_preinit() =
- if Cil.gccMode () || Cil.msvcMode () then
+ if Machine.(gccMode () || msvcMode ()) then
CompoundPre (ref (-1), ref [| |])
- else abort_context "empty initializers %s" (Cil.allowed_machdep "GCC/MSVC")
+ else abort_context "empty initializers %s" (Machdep.allowed_machdep "GCC/MSVC")
(* Set an initializer *)
let rec setOneInit this o preinit =
@@ -3116,7 +3116,7 @@ let rec collectInitializer
else
begin
(* not a flexible array member *)
- if len = 0 && not (Cil.gccMode() || Cil.msvcMode ()) then
+ if len = 0 && not Machine.(gccMode () || msvcMode ()) then
Kernel.error ~once:true ~current:true
"arrays of size zero not supported in C99@ \
(only allowed as compiler extensions)";
@@ -3177,7 +3177,7 @@ let rec collectInitializer
| _ ->
abort_context "Can initialize only one field for union"
in
- if Cil.msvcMode () && !pMaxIdx != 0 then
+ if Machine.msvcMode () && !pMaxIdx != 0 then
Kernel.warning ~current:true
"On MSVC we can initialize only the first field of a union";
let init, reads = findField 0 (Option.value ~default:[] comp.cfields) in
@@ -3536,7 +3536,7 @@ let suggestAnonName (nl: Cabs.name list) =
(** Optional constant folding of binary operations *)
let optConstFoldBinOp loc machdep bop e1 e2 t =
- if theMachine.lowerConstants then
+ if Machine.lower_constants () then
constFoldBinOp ~loc machdep bop e1 e2 t
else
new_exp ~loc (BinOp(bop, e1, e2, t))
@@ -4057,7 +4057,7 @@ let checkTypedefSize name typ =
Kernel.warning ~current:true
"bad type '%a' (%d bits) for typedef '%s' using machdep %s;@ \
check for mismatch between -machdep flag and headers used"
- Typ.pretty typ size name Cil.theMachine.theMachine.machdep_name
+ Typ.pretty typ size name (Machine.machdep_name ())
with
(* Not a standard integer type, ignore it. *)
Not_found -> ()
@@ -4158,7 +4158,7 @@ let rec doSpecList loc ghost (suggestedAnonName: string)
(* GCC allows a named type that appears first to be followed by things
* like "short", "signed", "unsigned" or "long". *)
match tspecs with
- | Cabs.Tnamed _ :: (_ :: _ as rest) when Cil.gccMode () ->
+ | Cabs.Tnamed _ :: (_ :: _ as rest) when Machine.gccMode () ->
(* If rest contains "short" or "long" then drop the Tnamed *)
if List.exists (function Cabs.Tshort -> true
| Cabs.Tlong -> true | _ -> false) rest then
@@ -4263,9 +4263,9 @@ let rec doSpecList loc ghost (suggestedAnonName: string)
(* Now the other type specifiers *)
| [Cabs.Tnamed "__builtin_va_list"]
- when Cil.theMachine.theMachine.has__builtin_va_list ->
+ when Machine.has_builtin_va_list () ->
TBuiltin_va_list []
- | [Cabs.Tnamed "__fc_builtin_size_t"] -> Cil.theMachine.typeOfSizeOf
+ | [Cabs.Tnamed "__fc_builtin_size_t"] -> Machine.sizeof_type ()
| [Cabs.Tnamed n] ->
(match lookupType ghost "type" n with
| (TNamed _) as x, _ -> x
@@ -4336,7 +4336,7 @@ let rec doSpecList loc ghost (suggestedAnonName: string)
smallest := i;
if Integer.gt i !largest then
largest := i;
- if Cil.msvcMode () then
+ if Machine.msvcMode () then
IInt
else begin
match Kernel.Enums.get () with
@@ -4387,7 +4387,7 @@ let rec doSpecList loc ghost (suggestedAnonName: string)
Cil_printer.pp_exp e'
| Some i ->
let ik = updateEnum i in
- if theMachine.lowerConstants then
+ if Machine.lower_constants () then
kinteger64 ~loc:e.expr_loc ~kind:ik i
else
e'
@@ -4528,7 +4528,7 @@ and makeVarSizeVarInfo ghost (ldecl : location)
(n,ndt,a)
: varinfo * chunk * exp * bool =
let kind = `LocalDecl in
- if not (Cil.msvcMode ()) then
+ if not (Machine.msvcMode ()) then
match isVariableSizedArray ghost ndt with
| None ->
makeVarInfoCabs ~ghost ~kind ldecl spec_res (n,ndt,a),
@@ -4569,7 +4569,7 @@ and doAttr ghost (a: Cabs.attribute) : attribute list =
match Datatype.String.Hashtbl.find env n' with
| EnvEnum item, _ -> begin
match constFoldToInt item.eival with
- | Some i64 when theMachine.lowerConstants ->
+ | Some i64 when Machine.lower_constants () ->
AInt i64
| _ -> ACons(n', [])
end
@@ -4712,7 +4712,7 @@ and doType (ghost:bool) (context: type_context)
else
cabsTypeAddAttributes a2f
(cabsTypeAddAttributes a1f restyp)
- | TPtr ((TFun _ as tf), ap) when not (Cil.msvcMode ()) ->
+ | TPtr ((TFun _ as tf), ap) when not (Machine.msvcMode ()) ->
if a1fadded then
TPtr(cabsTypeAddAttributes a2f tf, ap)
else
@@ -4768,7 +4768,7 @@ and doType (ghost:bool) (context: type_context)
then
(* because we tested previously for incomplete types and now tested again
forbidding zero-length arrays, bt is necessarily a zero-length array *)
- if Cil.gccMode () || Cil.msvcMode () then
+ if Machine.(gccMode () || msvcMode ()) then
Kernel.warning ~once:true ~current:true
"declaration of array of 'zero-length arrays' ('%a`);@ \
zero-length arrays are a compiler extension"
@@ -4814,7 +4814,7 @@ and doType (ghost:bool) (context: type_context)
we just check here that the size is not widely off.*)
Integer.one
in
- let size_t = bitsSizeOfInt theMachine.kindOfSizeOf in
+ let size_t = bitsSizeOfInt (Machine.sizeof_kind ()) in
let size_max = Cil.max_unsigned_number size_t in
let array_size = Integer.mul i elem_size in
if Integer.gt array_size size_max then
@@ -4863,10 +4863,10 @@ and doType (ghost:bool) (context: type_context)
end
| _ -> ());
if Cil.isZero len' && not allowZeroSizeArrays &&
- not (Cil.gccMode () || Cil.msvcMode ())
+ not Machine.(gccMode () || msvcMode ())
then
Kernel.error ~once:true ~current:true
- "zero-length arrays %s" (Cil.allowed_machdep "GCC/MSVC");
+ "zero-length arrays %s" (Machdep.allowed_machdep "GCC/MSVC");
Some len'
in
let al' = doAttributes ghost al in
@@ -4884,7 +4884,7 @@ and doType (ghost:bool) (context: type_context)
* builtin_va_alist_t". On MSVC we do not have the ellipsis and we
* have a last argument "va_alist: va_list" *)
let args', isva' =
- if args != [] && Cil.msvcMode () = not isva then begin
+ if args != [] && Machine.msvcMode () = not isva then begin
let newisva = ref isva in
let rec doLast = function
[([Cabs.SpecType (Cabs.Tnamed atn)], (an, Cabs.JUSTBASE, [], _))]
@@ -5113,7 +5113,7 @@ and makeCompType loc ghost (isstruct: bool)
let<> UpdatedCurrentLoc = cloc in
if sto <> NoStorage || inl then
Kernel.error ~once:true ~source "Storage or inline not allowed for fields";
- let allowZeroSizeArrays = Cil.gccMode () || Cil.msvcMode () in
+ let allowZeroSizeArrays = Machine.(gccMode () || msvcMode ()) in
let ftype, fattr =
doType
~allowZeroSizeArrays ghost `FieldDecl (AttrName false) bt
@@ -5133,11 +5133,11 @@ and makeCompType loc ghost (isstruct: bool)
"non-final field `%s' declared with a type containing a flexible \
array member."
n
- else if not (Cil.gccMode() || Cil.msvcMode ()) then
+ else if not Machine.(gccMode() || msvcMode ()) then
Kernel.error ~source
"field `%s' declared with a type containing a flexible array \
member %s."
- n (Cil.allowed_machdep "GCC/MSVC")
+ n (Machdep.allowed_machdep "GCC/MSVC")
end
else if not (Cil.isCompleteType ~allowZeroSizeArrays ftype)
then begin
@@ -5290,11 +5290,11 @@ and makeCompType loc ghost (isstruct: bool)
(* Do not add unnamed bitfields: they can share the empty name. *)
if f.fname <> "" then Hashtbl.add fld_table f.fname f
in
- if flds = [] && not (Cil.acceptEmptyCompinfo ()) then
+ if flds = [] && not (Machine.acceptEmptyCompinfo ()) then
Kernel.error ~current:true ~once:true
"empty %ss %s"
(if comp.cstruct then "struct" else "union")
- (Cil.allowed_machdep "GCC/MSVC");
+ (Machdep.allowed_machdep "GCC/MSVC");
List.iter check flds;
if comp.cfields <> None then begin
let old_fields = Option.get comp.cfields in
@@ -5525,7 +5525,7 @@ and doExp local_env
(*Kernel.debug "Looking for %s got enum %s : %a of type %a"
n item.einame Cil_printer.pp_exp item.eival
Cil_datatype.Typ.pretty typ; *)
- if Cil.theMachine.Cil.lowerConstants then
+ if Machine.lower_constants () then
finishExp [] (unspecified_chunk empty) item.eival typ
else
finishExp []
@@ -5727,8 +5727,8 @@ and doExp local_env
* the value. But L'abc' has type wchar, and so is equivalent to
* L'c'). But gcc allows L'abc', so I'll leave this here in case
* I'm missing some architecture dependent behavior. *)
- let value = reduce_multichar theMachine.wcharType char_list in
- let result = kinteger64 ~loc ~kind:theMachine.wcharKind
+ let value = reduce_multichar (Machine.wchar_type ()) char_list in
+ let result = kinteger64 ~loc ~kind:(Machine.wchar_kind ())
(Integer.of_int64 value)
in
finishExp [] (unspecified_chunk empty) result (typeOf result)
@@ -5753,7 +5753,7 @@ and doExp local_env
let typ = doOnlyType loc local_env.is_ghost bt dt in
fail_if_incompatible_sizeof ~ensure_complete:true "sizeof" typ;
let res = new_exp ~loc (SizeOf typ) in
- finishExp [] (unspecified_chunk empty) res theMachine.typeOfSizeOf
+ finishExp [] (unspecified_chunk empty) res (Machine.sizeof_type ())
| Cabs.EXPR_SIZEOF e ->
(* Allow non-constants in sizeof *)
@@ -5774,13 +5774,13 @@ and doExp local_env
| Const (CStr s) -> new_exp ~loc (SizeOfStr s)
| _ -> new_exp ~loc (SizeOfE e')
in
- finishExp [] scope_chunk size theMachine.typeOfSizeOf
+ finishExp [] scope_chunk size (Machine.sizeof_type ())
| Cabs.TYPE_ALIGNOF (bt, dt) ->
let typ = doOnlyType loc local_env.is_ghost bt dt in
fail_if_incompatible_sizeof ~ensure_complete:true "alignof" typ;
let res = new_exp ~loc (AlignOf typ) in
- finishExp [] (unspecified_chunk empty) res theMachine.typeOfSizeOf
+ finishExp [] (unspecified_chunk empty) res (Machine.sizeof_type ())
| Cabs.EXPR_ALIGNOF e ->
let (_, se, e', lvt) =
@@ -5796,7 +5796,7 @@ and doExp local_env
| _ -> e'
in
finishExp [] scope_chunk (new_exp ~loc (AlignOfE(e'')))
- theMachine.typeOfSizeOf
+ (Machine.sizeof_type ())
| Cabs.CAST ((specs, dt), ie) ->
let s', dt', ie' = preprocessCast loc local_env.is_ghost specs dt ie in
@@ -5937,7 +5937,7 @@ and doExp local_env
* taking the address of the argument that was removed while
* processing the function type. We compute the address based on
* the address of the last real argument *)
- if Cil.msvcMode () then begin
+ if Machine.msvcMode () then begin
let rec getLast = function
| [] ->
abort_context
@@ -6842,7 +6842,7 @@ and doExp local_env
| [ ] -> begin
piscall := false;
pres := new_exp ~loc:e.expr_loc (SizeOfE !pf);
- prestype := theMachine.typeOfSizeOf
+ prestype := (Machine.sizeof_type ())
end
| _ ->
Kernel.warning ~current:true
@@ -6899,13 +6899,13 @@ and doExp local_env
| [{ enode = CastE (_, {enode = AddrOf (host, offset)}) } as e] ->
begin
piscall := false;
- prestype := Cil.theMachine.Cil.typeOfSizeOf;
+ prestype := Machine.sizeof_type ();
let typ = Cil.typeOfLhost host in
try
let start, _width = Cil.bitsOffset typ offset in
if start mod 8 <> 0 then
Kernel.error ~current:true "Using offset of bitfield";
- let kind = Cil.theMachine.kindOfSizeOf in
+ let kind = Machine.sizeof_kind () in
pres := Cil.kinteger ~loc:e.eloc kind (start / 8);
with SizeOfError (s, _) ->
pres := e;
@@ -7625,7 +7625,7 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
| (Mod|BAnd|BOr|BXor) -> doIntegralArithmetic ()
| (Shiftlt|Shiftrt) -> (* ISO 6.5.7. Only integral promotions. The result
* has the same type as the left hand side *)
- if Cil.msvcMode () then
+ if Machine.msvcMode () then
(* MSVC has a bug. We duplicate it here *)
doIntegralArithmetic ()
else
@@ -7654,8 +7654,8 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
(Cil.type_remove_qualifier_attributes_deep t1)
(Cil.type_remove_qualifier_attributes_deep t2)
then
- theMachine.ptrdiffType,
- optConstFoldBinOp loc false MinusPP e1 e2 theMachine.ptrdiffType
+ Machine.ptrdiff_type (),
+ optConstFoldBinOp loc false MinusPP e1 e2 (Machine.ptrdiff_type ())
else abort_context "incompatible types in pointer subtraction"
(* Two special cases for comparisons with the NULL pointer. We are a bit
@@ -7726,7 +7726,7 @@ and doCondExp local_env asconst
clean_up_cond_locals ce2; ce1
end else CEAnd (ce1, ce2))
| CEExp(se1, e1'), CEExp (se2, e2') when
- theMachine.useLogicalOperators && isEmpty se1 && isEmpty se2 ->
+ Machine.use_logical_operators () && isEmpty se1 && isEmpty se2 ->
CEExp (empty, new_exp ~loc (BinOp(LAnd, e1', e2', intType)))
| _ -> CEAnd (ce1, ce2)
end
@@ -7745,7 +7745,7 @@ and doCondExp local_env asconst
clean_up_cond_locals ce2; ce1
end else CEOr (ce1, ce2))
| CEExp (se1, e1'), CEExp (se2, e2') when
- theMachine.useLogicalOperators && isEmpty se1 && isEmpty se2 ->
+ Machine.use_logical_operators () && isEmpty se1 && isEmpty se2 ->
CEExp (empty, new_exp ~loc (BinOp(LOr, e1', e2', intType)))
| _ -> CEOr (ce1, ce2)
end
@@ -7777,7 +7777,7 @@ and doCondExp local_env asconst
ConditionalSideEffectHook.apply (orig,e));
ignore (checkBool t e');
CEExp (add_reads ~ghost e.expr_loc r se,
- if asconst <> CNoConst || theMachine.lowerConstants then
+ if asconst <> CNoConst || Machine.lower_constants () then
constFold true e'
else e')
in
@@ -8149,7 +8149,7 @@ and doInit local_env asconst preinit so acc initl =
match bt' with
(* compare bt to wchar_t, ignoring signed vs. unsigned *)
| TInt _ when (bitsSizeOf bt') =
- (bitsSizeOf theMachine.wcharType) ->
+ (bitsSizeOf (Machine.wchar_type ())) ->
true
| TInt _ ->
(*Base type is a scalar other than wchar_t.
@@ -8163,8 +8163,8 @@ and doInit local_env asconst preinit so acc initl =
)
->
let maxWChar = (* (2**(bitsSizeOf !wcharType)) - 1 *)
- Int64.sub (Int64.shift_left Int64.one (bitsSizeOf theMachine.wcharType))
- Int64.one in
+ Int64.(sub (shift_left one (bitsSizeOf (Machine.wchar_type ()))) one)
+ in
let charinits =
let init c =
if Int64.compare c maxWChar > 0 then (* if c > maxWChar *)
@@ -8254,7 +8254,7 @@ and doInit local_env asconst preinit so acc initl =
Cil_printer.pp_exp oneinit' Cil_datatype.Typ.pretty t'
Cil_datatype.Typ.pretty so.soTyp;
let init_expr =
- if theMachine.insertImplicitCasts then snd (castTo t' so.soTyp oneinit')
+ if Machine.insert_implicit_casts () then snd (castTo t' so.soTyp oneinit')
else oneinit'
in
let preinit' = setOneInit preinit so.soOff (SinglePre (init_expr,r)) in
@@ -8891,7 +8891,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
~ghost
~kind:`LocalDecl
loc
- (theMachine.typeOfSizeOf, NoStorage, false, [])
+ (Machine.sizeof_type (), NoStorage, false, [])
("__lengthof_" ^ vi.vname,JUSTBASE, [])
in
(* Register it *)
@@ -8904,7 +8904,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
(BinOp(Mult,
elt_size,
new_exp ~loc (Lval (var savelen)),
- theMachine.typeOfSizeOf))
+ Machine.sizeof_type ()))
in
(* Register the length *)
IH.add varSizeArrays vi.vid alloca_size;
@@ -8928,7 +8928,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
Logic_const.prel ~loc:castloc (Rlt, zero, talloca_size)
in
let max_size =
- let szTo = Cil.bitsSizeOf theMachine.typeOfSizeOf in
+ let szTo = Cil.bitsSizeOf (Machine.sizeof_type ()) in
let max_bound = Logic_const.tint ~loc:castloc (Cil.max_unsigned_number szTo) in
Logic_const.prel ~loc:castloc (Rle, talloca_size, max_bound)
in
@@ -10076,7 +10076,7 @@ and doStatement local_env (s : Cabs.statement) : chunk =
"Case statement with a non-constant";
let chunk =
caseRangeChunk ~ghost
- [if theMachine.lowerConstants then constFold false e' else e']
+ [if Machine.lower_constants () then constFold false e' else e']
loc' (doStatement local_env s)
in
(* se has no statement, but can contain local variables, in
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index 01c1b346c1d653475d7b488fdbc96ad91133bcd6..7dcb102cb801783c5d6370ed0c8fcce4e0bca1c4 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -263,7 +263,7 @@ let isExportedRoot global =
else if v.vstorage = Static then
v.vname, not !rmUnusedStatic, "static function"
else if v.vinline && v.vstorage != Extern
- && (Cil.msvcMode () || !rmUnusedInlines) then
+ && (Machine.msvcMode () || !rmUnusedInlines) then
v.vname, false, "inline function"
else
v.vname, true, "other function"
@@ -378,7 +378,7 @@ class markReachableVisitor
| _ -> DoChildren
method! vinst = function
- | Asm (_, tmpls, _, _) when Cil.msvcMode () ->
+ | Asm (_, tmpls, _, _) when Machine.msvcMode () ->
(* If we have inline assembly on MSVC, we cannot tell which locals
* are referenced. Keep them all *)
(match !currentFunc with
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 87b585b9c4894500291e4c53141699f9a1b0de7d..da6d647b22a0351d28453d60d385fd10d8793462 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -158,7 +158,7 @@ let cstring_bitlength s =
| CSString s ->
bitsSizeOf Cil_const.charType, (String.length s)
| CSWstring s ->
- bitsSizeOf theMachine.wcharType, (List.length s)
+ bitsSizeOf (Machine.wchar_type ()), (List.length s)
in
Int.of_int (u*(succ l))
diff --git a/src/kernel_services/abstract_interp/cvalue.ml b/src/kernel_services/abstract_interp/cvalue.ml
index bd0e040f33fdc691af23237e227e77fe161bfca4..0f70fa34a69c724a18bfa008569ffc981e691867 100644
--- a/src/kernel_services/abstract_interp/cvalue.ml
+++ b/src/kernel_services/abstract_interp/cvalue.ml
@@ -609,7 +609,7 @@ module V = struct
else
(* Keep precision if we are reading all the bits of an address *)
let ptr_size =
- Integer.of_int (Cil.(bitsSizeOfInt theMachine.upointKind))
+ Integer.of_int (Cil.bitsSizeOfInt (Machine.uintptr_kind ()))
in
if Int.equal start Int.zero &&
Int.equal (Int.succ stop) ptr_size &&
@@ -943,7 +943,7 @@ module V_Offsetmap = struct
let from_wstring s =
let conv v = V_Or_Uninitialized.initialized (V.of_int64 v) in
let fold f acc l = List.fold_left (fun acc v -> f acc (conv v)) acc l in
- let size_wchar = Integer.of_int Cil.(bitsSizeOf theMachine.wcharType) in
+ let size_wchar = Integer.of_int (Cil.bitsSizeOf (Machine.wchar_type ())) in
of_list fold (s @ [0L]) size_wchar
let from_cstring = function
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 43fe9f3436bfe5ec33cd1110eebdf858558f11ac..cce3aad86684f1a42066c0f350b138d45b95563b 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -1032,7 +1032,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
let extract_bits ~start ~stop ~modu v =
assert (start <=~ stop && stop <=~ modu);
let start,stop =
- if Cil.theMachine.Cil.theMachine.Cil_types.little_endian then
+ if Machine.little_endian () then
start,stop
else
let mmodu = pred modu in
@@ -1044,7 +1044,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
let merge_bits ~topify ~conflate_bottom ~offset ~length ~value ~total_length acc =
assert (length +~ offset <=~ total_length);
let offset =
- if Cil.theMachine.Cil.theMachine.Cil_types.little_endian then
+ if Machine.little_endian () then
offset
else
Int.sub (Int.sub total_length offset) length
diff --git a/src/kernel_services/analysis/bit_utils.ml b/src/kernel_services/analysis/bit_utils.ml
index affb4f40dcf0ccff9abc19e8111a220971f31725..c086012ea79b0804512176d6e867045616b3dbc2 100644
--- a/src/kernel_services/analysis/bit_utils.ml
+++ b/src/kernel_services/analysis/bit_utils.ml
@@ -31,7 +31,7 @@ open Cil
let sizeofchar () = Integer.of_int (bitsSizeOf Cil_const.charType)
(** [sizeof(char* )] in bits *)
-let sizeofpointer () = bitsSizeOf theMachine.upointType
+let sizeofpointer () = bitsSizeOf (Machine.uintptr_type ())
(** 2^(8 * sizeof( void * )) *)
let max_byte_size () =
diff --git a/src/kernel_services/analysis/destructors.ml b/src/kernel_services/analysis/destructors.ml
index 81f9c24b559d1ef79f6ad02f0d97b37330db65c7..1eecb32fc658d269f22b801ed6ceab3a6e8cd336 100644
--- a/src/kernel_services/analysis/destructors.ml
+++ b/src/kernel_services/analysis/destructors.ml
@@ -58,7 +58,7 @@ let add_destructor (_, l as acc) var =
| ACons (f, [n]) ->
(match Cil.intOfAttrparam n with
| Some n ->
- mk_call f e [Cil.kinteger ~loc Cil.(theMachine.kindOfSizeOf) n]
+ mk_call f e [Cil.kinteger ~loc (Machine.sizeof_kind ()) n]
| None ->
Kernel.fatal
"unexpected argument of attribute %s: %a"
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 5ad2bc112494c9947014a0e3ba3ccd69f989284c..3977959164ace720b634db4bd85bcf646964a935 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -547,7 +547,7 @@ let create_predicate ?(loc=Location.unknown) alarm =
let t = match kind with
| Pointer_downcast ->
let t = Logic_utils.expr_to_term e in
- Logic_const.tcast ~loc t Cil.theMachine.upointType
+ Logic_const.tcast ~loc t (Machine.uintptr_type ())
| Signed_downcast | Unsigned_downcast ->
Logic_utils.expr_to_term ~coerce:true e
| _ ->
diff --git a/src/kernel_services/ast_data/ast.ml b/src/kernel_services/ast_data/ast.ml
index 05a5e0158e7026370dcd79e5a2e6dde44e79aa13..c76daf23efd01f39221765b506358f5ae1871147 100644
--- a/src/kernel_services/ast_data/ast.ml
+++ b/src/kernel_services/ast_data/ast.ml
@@ -31,7 +31,7 @@ include
let name = "AST"
let dependencies =
- [ Cil.selfMachine;
+ [ Machine.self;
Kernel.SimplifyCfg.self;
Kernel.KeepSwitch.self;
Kernel.Constfold.self;
@@ -148,7 +148,7 @@ module UntypedFiles = struct
(struct
let name = "Untyped AST"
let dependencies = (* the others delayed until file.ml *)
- [ Cil.selfMachine;
+ [ Machine.self;
self (* can't be computed without the AST *) ]
end)
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 5beace6ba488d30b9c027c7fef661e6d78c03c2a..185a7fa68fe5f8f67c3219062965e23866e6e546 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -754,9 +754,9 @@ and exp_node =
| Const of constant (** Constant *)
| Lval of lval (** Lvalue *)
| SizeOf of typ
- (** sizeof(<type>). Has [unsigned int] type (ISO 6.5.3.4). This is not
- turned into a constant because some transformations might want to change
- types *)
+ (** sizeof(<type>). Has [size_t] type (ISO 6.5.3.4) which depends on machine
+ configuration (cf. {!Machine}). This is not turned into a constant
+ because some transformations might want to change types *)
| SizeOfE of exp (** sizeof(<expression>) *)
@@ -766,7 +766,8 @@ and exp_node =
type pointer to character. *)
| AlignOf of typ
- (** This corresponds to the GCC __alignof_. Has [unsigned int] type *)
+ (** This corresponds to the GCC __alignof_. Has [size_t] type which depends on
+ machine configuration (cf. {!Machine}). *)
| AlignOfE of exp
@@ -813,13 +814,13 @@ and constant =
| CWStr of int64 list
(** Wide character string constant. Note that the local interpretation of such
- a literal depends on {!Cil.theMachine.wcharType} and
- {!Cil.theMachine.wcharKind}. Such a constant has type pointer to
- {!Cil.theMachine.wcharType}. The escape characters in the string have not
- been "interpreted" in the sense that L"A\xabcd" remains "A\xabcd" rather
- than being represented as the wide character list with two elements: 65
- and 43981. That "interpretation" depends on the underlying wide character
- type. *)
+ a literal depends on {!Machine.theMachine.wcharType} and
+ {!Machine.theMachine.wcharKind}. Such a constant has type pointer to
+ {!Machine.theMachine.wcharType}. The escape characters in the string
+ have not been "interpreted" in the sense that L"A\xabcd" remains
+ "A\xabcd" rather than being represented as the wide character list with
+ two elements: 65 and 43981. That "interpretation" depends on the
+ underlying wide character type. *)
| CChr of char
(** Character constant. This has type int, so use charConstToInt to read the
@@ -1879,88 +1880,3 @@ type syntactic_scope =
the block to which it is tied, will be considered.
@since 27.0-Cobalt
*)
-
-let yaml_dict_to_list = function
- | `O l ->
- let make_one acc (k,v) =
- Result.(
- bind acc
- (fun l ->
- match Yaml.Util.to_string v with
- | Ok s -> Ok((k,s) :: l)
- | Error (`Msg s) ->
- Error (`Msg ("Unexpected value for key " ^ k ^ ": " ^ s))))
- in
- List.fold_left make_one (Ok []) l
- | _ -> Error (`Msg "Unexpected YAML value instead of dictionary of strings")
-
-(** Definition of a machine model (architecture + compiler).
- @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
-type mach = {
- sizeof_short: int; (* Size of "short" *)
- sizeof_int: int; (* Size of "int" *)
- 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_void: int; (* Size of "void" *)
- sizeof_fun: int; (* Size of function. Negative if unsupported. *)
- size_t: string; (* Type of "sizeof(T)" *)
- 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; (* Alignment of "short" *)
- alignof_int: int; (* Alignment of "int" *)
- alignof_long: int; (* Alignment of "long" *)
- alignof_longlong: int; (* Alignment of "long long" *)
- alignof_ptr: int; (* Alignment of pointers *)
- alignof_float: int; (* Alignment of "float" *)
- alignof_double: int; (* Alignment of "double" *)
- alignof_longdouble: int; (* Alignment of "long double" *)
- alignof_str: int; (* Alignment of strings *)
- alignof_fun: int; (* Alignment of function. Negative if unsupported. *)
- char_is_unsigned: bool; (* Whether "char" is unsigned *)
- little_endian: bool; (* whether the machine is little endian *)
- alignof_aligned: int (* Alignment of a type with aligned attribute *);
- has__builtin_va_list: bool (* Whether [__builtin_va_list] is a known type *);
- compiler: string; (* Compiler being used. Currently recognized names
- are 'gcc', 'msvc' and 'generic'. *)
- cpp_arch_flags: string list; (* Architecture-specific flags to be given to
- the preprocessor (if supported) *)
- 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 *)
- (* list of macros defining errors in errno.h*)
- errno: (string * string) list [@of_yaml yaml_dict_to_list];
- machdep_name: string; (* name of the machdep *)
- (* sequence of key/value for C macros *)
- custom_defs: (string * string) list [@of_yaml yaml_dict_to_list];
-} [@@deriving yaml]
diff --git a/src/kernel_services/ast_data/machine.ml b/src/kernel_services/ast_data/machine.ml
new file mode 100644
index 0000000000000000000000000000000000000000..71b9081ba626e69a37e37a9a8caa488db8e995f5
--- /dev/null
+++ b/src/kernel_services/ast_data/machine.ml
@@ -0,0 +1,300 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Machdep
+
+(******************************************************************************)
+(*** Machine parameters *)
+(******************************************************************************)
+
+type machine = {
+ 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. *)
+ mutable machdep: mach;
+ (* Machine.init will set this to the current machine description. *)
+ mutable lowerConstants: bool;
+ (* Do lower constants (default true) *)
+ mutable insertImplicitCasts: bool;
+ (* Do insert implicit casts (default true) *)
+ mutable stringLiteralType: typ;
+ mutable upointType: typ;
+ (* An unsigned integer type that fits pointers. *)
+ mutable upointKind: ikind;
+ (* The integer kind of {!upointType}. *)
+ mutable wcharType: typ;
+ (* An integer type that fits wchar_t. *)
+ mutable wcharKind: ikind;
+ (* The integer kind of {!wcharType}. *)
+ mutable ptrdiffType: typ;
+ (* An integer type that fits ptrdiff_t. *)
+ mutable ptrdiffKind: ikind;
+ (* The integer kind of {!ptrdiffType}. *)
+ mutable typeOfSizeOf: typ;
+ (* An integer type that is the type of sizeof. *)
+ mutable kindOfSizeOf: ikind;
+ (* The integer kind of {!typeOfSizeOf}. *)
+}
+
+(* Contain dummy values *)
+let create_machine () = {
+ useLogicalOperators = false;
+ machdep = List.hd Machdep.reprs;
+ lowerConstants = false;
+ insertImplicitCasts = true;
+ stringLiteralType = Cil_const.charConstPtrType;
+ upointType = Cil_const.voidType;
+ upointKind = IChar;
+ wcharType = Cil_const.voidType;
+ wcharKind = IChar;
+ ptrdiffType = Cil_const.voidType;
+ ptrdiffKind = IChar;
+ typeOfSizeOf = Cil_const.voidType;
+ kindOfSizeOf = IUInt;
+}
+
+let copy_machine src dst =
+ dst.useLogicalOperators <- src.useLogicalOperators;
+ dst.machdep <- src.machdep;
+ dst.lowerConstants <- src.lowerConstants;
+ dst.insertImplicitCasts <- src.insertImplicitCasts;
+ dst.stringLiteralType <- src.stringLiteralType;
+ dst.upointType <- src.upointType;
+ dst.upointKind <- src.upointKind;
+ dst.wcharType <- src.wcharType;
+ dst.wcharKind <- src.wcharKind;
+ dst.ptrdiffType <- src.ptrdiffType;
+ dst.ptrdiffKind <- src.ptrdiffKind;
+ dst.typeOfSizeOf <- src.typeOfSizeOf;
+ dst.kindOfSizeOf <- src.kindOfSizeOf
+
+let the_machine = create_machine ()
+
+let use_logical_operators () = the_machine.useLogicalOperators
+let get_machdep () = the_machine.machdep
+let lower_constants () = the_machine.lowerConstants
+let insert_implicit_casts () = the_machine.insertImplicitCasts
+let string_literal_type () = the_machine.stringLiteralType
+let uintptr_type () = the_machine.upointType
+let uintptr_kind () = the_machine.upointKind
+let ptrdiff_type () = the_machine.ptrdiffType
+let ptrdiff_kind () = the_machine.ptrdiffKind
+let wchar_type () = the_machine.wcharType
+let wchar_kind () = the_machine.wcharKind
+let sizeof_type () = the_machine.typeOfSizeOf
+let sizeof_kind () = the_machine.kindOfSizeOf
+
+(******************************************************************************)
+(*** Machdep getters *)
+(******************************************************************************)
+
+(* Sizeof *)
+let sizeof_short () = the_machine.machdep.sizeof_short
+let sizeof_int () = the_machine.machdep.sizeof_int
+let sizeof_long () = the_machine.machdep.sizeof_long
+let sizeof_longlong () = the_machine.machdep.sizeof_longlong
+let sizeof_ptr () = the_machine.machdep.sizeof_ptr
+let sizeof_float () = the_machine.machdep.sizeof_float
+let sizeof_double () = the_machine.machdep.sizeof_double
+let sizeof_longdouble () = the_machine.machdep.sizeof_longdouble
+let sizeof_void () = the_machine.machdep.sizeof_void
+let sizeof_fun () = the_machine.machdep.sizeof_fun
+
+(* Names *)
+let size_t () = the_machine.machdep.size_t
+let ssize_t () = the_machine.machdep.ssize_t
+let wchar_t () = the_machine.machdep.wchar_t
+let ptrdiff_t () = the_machine.machdep.ptrdiff_t
+let intptr_t () = the_machine.machdep.intptr_t
+let uintptr_t () = the_machine.machdep.uintptr_t
+let int_fast8_t () = the_machine.machdep.int_fast8_t
+let int_fast16_t () = the_machine.machdep. int_fast16_t
+let int_fast32_t () = the_machine.machdep. int_fast32_t
+let int_fast64_t () = the_machine.machdep. int_fast64_t
+let uint_fast8_t () = the_machine.machdep.uint_fast8_t
+let uint_fast16_t () = the_machine.machdep.uint_fast16_t
+let uint_fast32_t () = the_machine.machdep.uint_fast32_t
+let uint_fast64_t () = the_machine.machdep.uint_fast64_t
+let wint_t () = the_machine.machdep.wint_t
+let sig_atomic_t () = the_machine.machdep.sig_atomic_t
+let time_t () = the_machine.machdep.time_t
+
+(* Alignof *)
+let alignof_short () = the_machine.machdep.alignof_short
+let alignof_int () = the_machine.machdep.alignof_int
+let alignof_long () = the_machine.machdep.alignof_long
+let alignof_longlong () = the_machine.machdep.alignof_longlong
+let alignof_ptr () = the_machine.machdep.alignof_ptr
+let alignof_float () = the_machine.machdep.alignof_float
+let alignof_double () = the_machine.machdep.alignof_double
+let alignof_longdouble () = the_machine.machdep.alignof_longdouble
+let alignof_str () = the_machine.machdep.alignof_str
+let alignof_aligned () = the_machine.machdep.alignof_aligned
+let alignof_fun () = the_machine.machdep.alignof_fun
+
+(* Misc *)
+let char_is_unsigned () = the_machine.machdep.char_is_unsigned
+let little_endian () = the_machine.machdep.little_endian
+let has_builtin_va_list () = the_machine.machdep.has__builtin_va_list
+let compiler () = the_machine.machdep.compiler
+let cpp_arch_flags () = the_machine.machdep.cpp_arch_flags
+let version () = the_machine.machdep.version
+let machdep_name () = the_machine.machdep.machdep_name
+let errno () = the_machine.machdep.errno
+let custom_defs () = the_machine.machdep.custom_defs
+
+(* Macro expansion *)
+let weof () = the_machine.machdep.weof
+let wordsize () = the_machine.machdep.wordsize
+let posix_version () = the_machine.machdep.posix_version
+let bufsiz () = the_machine.machdep.bufsiz
+let eof () = the_machine.machdep.eof
+let fopen_max () = the_machine.machdep.fopen_max
+let filename_max () = the_machine.machdep.filename_max
+let host_name_max () = the_machine.machdep.host_name_max
+let tty_name_max () = the_machine.machdep.tty_name_max
+let l_tmpnam () = the_machine.machdep.l_tmpnam
+let path_max () = the_machine.machdep.path_max
+let tmp_max () = the_machine.machdep.tmp_max
+let rand_max () = the_machine.machdep.rand_max
+let mb_cur_max () = the_machine.machdep.mb_cur_max
+let nsig () = the_machine.machdep.nsig
+
+let msvcMode () = msvcMode (get_machdep ())
+let gccMode () = gccMode (get_machdep ())
+
+let acceptEmptyCompinfo = ref false
+let set_acceptEmptyCompinfo () = acceptEmptyCompinfo := true
+
+let acceptEmptyCompinfo () =
+ msvcMode () || gccMode () || !acceptEmptyCompinfo
+
+let theMachineProject = ref (create_machine ())
+
+module Machine_datatype =
+ Datatype.Make
+ (struct
+ include Datatype.Serializable_undefined
+ type t = machine
+ let name = "theMachine"
+ let reprs = [ the_machine ]
+ let copy x =
+ let m = create_machine () in
+ copy_machine x m;
+ m
+ let mem_project = Datatype.never_any_project
+ end)
+
+module TheMachine =
+ State_builder.Register
+ (Machine_datatype)
+ (struct
+ type t = machine
+ let create = create_machine
+ let get () = !theMachineProject
+ let set m =
+ theMachineProject := m;
+ copy_machine !theMachineProject the_machine
+ let clear m = copy_machine (create_machine ()) m
+ let clear_some_projects _ _ = false
+ end)
+ (struct
+ let name = "theMachine"
+ let unique_name = name
+ let dependencies = [ Kernel.Machdep.self; Kernel.LogicalOperators.self ]
+ end)
+
+let self = TheMachine.self
+
+let () =
+ State_dependency_graph.add_dependencies
+ ~from:self
+ Logic_env.builtin_states
+
+let is_computed = TheMachine.is_computed
+
+let init_builtins_ref : (unit -> unit) ref = Extlib.mk_fun "init_builtins_ref"
+
+let init ~initLogicBuiltins machdep =
+ if not (TheMachine.is_computed ()) then begin
+ (* Set the machine *)
+ the_machine.machdep <- machdep;
+ (* Pick type for string literals *)
+ the_machine.stringLiteralType <- Cil_const.charConstPtrType;
+ (* Find the right ikind given the size *)
+ let findIkindSz (unsigned: bool) (sz: int) : ikind =
+ (* Test the most common sizes first *)
+ if sz = sizeof_int () then
+ if unsigned then IUInt else IInt
+ else if sz = sizeof_long () then
+ if unsigned then IULong else ILong
+ else if sz = 1 then
+ if unsigned then IUChar else IChar
+ else if sz = sizeof_short () then
+ if unsigned then IUShort else IShort
+ else if sz = sizeof_longlong () then
+ if unsigned then IULongLong else ILongLong
+ else
+ Kernel.fatal ~current:true
+ "Machine.init: cannot find the right ikind for size %d\n" sz
+ in
+ (* Find the right ikind given the name *)
+ let findIkindName (name: string) : ikind =
+ (* Test the most common sizes first *)
+ if name = "int" then IInt
+ else if name = "unsigned int" then IUInt
+ else if name = "long" then ILong
+ else if name = "unsigned long" then IULong
+ else if name = "short" then IShort
+ else if name = "unsigned short" then IUShort
+ else if name = "char" then IChar
+ else if name = "unsigned char" then IUChar
+ else if name = "long long" then ILongLong
+ else if name = "unsigned long long" then IULongLong
+ else
+ Kernel.fatal ~current:true
+ "Machine.init: cannot find the right ikind for type %s" name
+ in
+ the_machine.upointKind <- findIkindSz true (sizeof_ptr ());
+ the_machine.upointType <- TInt(the_machine.upointKind, []);
+ the_machine.kindOfSizeOf <- findIkindName (size_t ());
+ the_machine.typeOfSizeOf <- TInt(the_machine.kindOfSizeOf, []);
+ the_machine.wcharKind <- findIkindName (wchar_t ());
+ the_machine.wcharType <- TInt(the_machine.wcharKind, []);
+ the_machine.ptrdiffKind <- findIkindName (ptrdiff_t ());
+ the_machine.ptrdiffType <- TInt(the_machine.ptrdiffKind, []);
+ the_machine.useLogicalOperators <- Kernel.LogicalOperators.get ();
+ (* Have to be marked before calling [init*Builtins] below. *)
+ TheMachine.mark_as_computed ();
+ (* projectify theMachine *)
+ copy_machine the_machine !theMachineProject;
+
+ !init_builtins_ref ();
+
+ Logic_env.Builtins.extend initLogicBuiltins;
+
+ end
+
+(* To be removed ideally *)
+let theMachine = the_machine
diff --git a/src/kernel_services/ast_data/machine.mli b/src/kernel_services/ast_data/machine.mli
new file mode 100644
index 0000000000000000000000000000000000000000..f0bc17c381a580e1c7e115f126ee55661e84ff03
--- /dev/null
+++ b/src/kernel_services/ast_data/machine.mli
@@ -0,0 +1,247 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** This module handle the machine configuration. Previous Frama-C
+ versions handled this in {!Cil}.
+
+ @since Frama-C+dev
+*)
+
+open Cil_types
+
+(* ***********************************************************************)
+(** {2 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. *)
+
+(* ***********************************************************************)
+(** {2 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
+
+(* ***********************************************************************)
+(** {2 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
+
+(* ***********************************************************************)
+(** {2 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
+
+(* ***********************************************************************)
+(** {2 Typ/kind getters} *)
+(* ***********************************************************************)
+
+val ptrdiff_kind: unit -> ikind
+val ptrdiff_type: unit -> typ
+
+val sizeof_kind: unit -> ikind
+val sizeof_type: unit -> typ
+
+val wchar_kind: unit -> ikind
+val wchar_type: unit -> typ
+
+val uintptr_kind: unit -> ikind
+val uintptr_type: unit -> typ
+
+val string_literal_type: unit -> typ
+
+(* ***********************************************************************)
+(** {2 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
+
+(* ***********************************************************************)
+(** {2 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
+
+(* ***********************************************************************)
+(** {2 Compiler } *)
+(* ***********************************************************************)
+
+val msvcMode: unit -> bool
+(** Short for [Machdep.msvcMode (get_machdep ())]
+ @since Frama-C+dev *)
+
+val gccMode: unit -> bool
+(** Short for [Machdep.gccMode (get_machdep ())]
+ @since Frama-C+dev *)
+
+val acceptEmptyCompinfo: unit -> bool
+(** whether we accept empty struct. Implied by {!msvcMode} and {!gccMode}, and
+ can be forced by {!set_acceptEmptyCompinfo} otherwise.
+ @since Frama-C+dev
+*)
+
+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 Frama-C+dev
+*)
+
+(* ***********************************************************************)
+(** {2 Initializer } *)
+(* ***********************************************************************)
+
+(** 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. *)
+val init: initLogicBuiltins:(unit -> unit) -> Machdep.mach -> unit
+
+(* ***********************************************************************)
+(** {2 Forward references} *)
+(* ***********************************************************************)
+
+(** Unless your name is {!Cil_builtins}, you should not call this. *)
+val init_builtins_ref: (unit -> unit) ref
+
+(* ***********************************************************************)
+(** {2 Deprecated access } *)
+(* ***********************************************************************)
+
+(* Prefer using previous functions *)
+
+type machine = private
+ { 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. *)
+ mutable machdep: Machdep.mach;
+ (** Machine.init will set this to the current machine description. *)
+ mutable lowerConstants: bool;
+ (** Do lower constants (default true) *)
+ mutable insertImplicitCasts: bool;
+ (** Do insert implicit casts (default true) *)
+ mutable stringLiteralType: typ;
+ mutable upointType: typ;
+ (** An unsigned integer type that fits pointers. *)
+ mutable upointKind: ikind;
+ (** The integer kind of {!upointType}. *)
+ mutable wcharType: typ;
+ (** An integer type that fits wchar_t. *)
+ mutable wcharKind: ikind;
+ (** The integer kind of {!wcharType}. *)
+ mutable ptrdiffType: typ;
+ (** An integer type that fits ptrdiff_t. *)
+ mutable ptrdiffKind: ikind;
+ (** The integer kind of {!ptrdiffType}. *)
+ mutable typeOfSizeOf: typ;
+ (** An integer type that is the type of sizeof. *)
+ mutable kindOfSizeOf: ikind;
+ (** The integer kind of {!typeOfSizeOf}. *)
+ }
+
+val theMachine: machine
+[@@alert deprecated "Prefer using Machine functions"]
+
+(* ***********************************************************************)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 1bd22b76984617a2e48455be50c9c3440938e295..c89f78044299d72f91be0c91f4924d4ff75e0faa 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -650,8 +650,8 @@ class cil_printer () = object (self)
| IUInt -> "U"
| ILong -> "L"
| IULong -> "UL"
- | ILongLong -> if Cil.msvcMode () then "L" else "LL"
- | IULongLong -> if Cil.msvcMode () then "UL" else "ULL"
+ | ILongLong -> if Machine.msvcMode () then "L" else "LL"
+ | IULongLong -> if Machine.msvcMode () then "UL" else "ULL"
| IInt | IBool | IShort | IUShort | IChar | ISChar | IUChar -> ""
in
let prefix =
@@ -1144,7 +1144,7 @@ class cil_printer () = object (self)
let goto =
match ext_asm with Some { asm_gotos = _::_ } -> " goto" | _ -> ""
in
- if Cil.msvcMode () then
+ if Machine.msvcMode () then
fprintf fmt "__asm%s {@[%a@]}%s"
goto
(Pretty_utils.pp_list ~sep:"@\n"
@@ -1426,7 +1426,7 @@ class cil_printer () = object (self)
| Some style ->
let directive = match style with
| Line_comment | Line_comment_sparse -> "//#line"
- | Line_preprocessor_output when not (Cil.msvcMode ()) -> "#"
+ | Line_preprocessor_output when not (Machine.msvcMode ()) -> "#"
| Line_preprocessor_output | Line_preprocessor_input -> "#line"
in
let pos = fst l in
@@ -1849,7 +1849,7 @@ class cil_printer () = object (self)
(* nor 'cilnoremove' *)
let suppress =
not state.print_cil_input
- && not (Cil.msvcMode ())
+ && not (Machine.msvcMode ())
&& (String.starts_with ~prefix:"box" an
|| String.starts_with ~prefix:"ccured" an
|| an = "merger"
@@ -1957,9 +1957,9 @@ class cil_printer () = object (self)
| ILong -> "long"
| IULong -> "unsigned long"
| ILongLong ->
- if Cil.msvcMode () then "__int64" else "long long"
+ if Machine.msvcMode () then "__int64" else "long long"
| IULongLong ->
- if Cil.msvcMode () then "unsigned __int64" else "unsigned long long"
+ if Machine.msvcMode () then "unsigned __int64" else "unsigned long long"
)
method compkind fmt ci =
@@ -1984,7 +1984,7 @@ class cil_printer () = object (self)
| Some pp -> if space then pp_print_char fmt ' '; pp fmt in
let printAttributes fmt (a: attributes) =
match nameOpt with
- | None when not state.print_cil_input && not (Cil.msvcMode ()) -> ()
+ | None when not state.print_cil_input && not (Machine.msvcMode ()) -> ()
(* Cannot print the attributes in this case because gcc does not like them
here, except if we are printing for CIL, or for MSVC. In fact, for
MSVC we MUST print attributes such as __stdcall *)
@@ -2023,7 +2023,7 @@ class cil_printer () = object (self)
* the parenthesis. *)
let (paren: (formatter -> unit) option), (bt': typ) =
match bt with
- | TFun(rt, args, isva, fa) when Cil.msvcMode () ->
+ | TFun(rt, args, isva, fa) when Machine.msvcMode () ->
let an, af', at = Cil.partitionAttributes ~default:Cil.AttrType fa in
(* We take the af' and we put them into the parentheses *)
Some
@@ -2166,15 +2166,15 @@ class cil_printer () = object (self)
(match an, args with
| "const", [] -> self#pp_keyword fmt "const"; false
(* Put the aconst inside the attribute list *)
- | "aconst", [] when not (Cil.msvcMode ()) -> fprintf fmt "__const__"; true
+ | "aconst", [] when not (Machine.msvcMode ()) -> fprintf fmt "__const__"; true
| "thread", [ ACons ("c11",[]) ]
when not state.print_cil_as_is ->
fprintf fmt "_Thread_local"; false
- | "thread", [] when not (Cil.msvcMode ()) -> fprintf fmt "__thread"; false
+ | "thread", [] when not (Machine.msvcMode ()) -> fprintf fmt "__thread"; false
| "volatile", [] -> self#pp_keyword fmt "volatile"; false
| "ghost", [] -> self#pp_keyword fmt "\\ghost"; false
| "restrict", [] ->
- if Cil.msvcMode () then
+ if Machine.msvcMode () then
fprintf fmt "__restrict"
else
self#pp_keyword fmt "restrict";
@@ -2182,17 +2182,17 @@ class cil_printer () = object (self)
| "missingproto", [] ->
if self#display_comment () then fprintf fmt "/* missing proto */";
false
- | "cdecl", [] when Cil.msvcMode () ->
+ | "cdecl", [] when Machine.msvcMode () ->
fprintf fmt "__cdecl"; false
- | "stdcall", [] when Cil.msvcMode () ->
+ | "stdcall", [] when Machine.msvcMode () ->
fprintf fmt "__stdcall"; false
- | "fastcall", [] when Cil.msvcMode () ->
+ | "fastcall", [] when Machine.msvcMode () ->
fprintf fmt "__fastcall"; false
- | "declspec", args when Cil.msvcMode () ->
+ | "declspec", args when Machine.msvcMode () ->
fprintf fmt "__declspec(%a)"
(Pretty_utils.pp_list ~sep:"" self#attrparam) args;
false
- | "w64", [] when Cil.msvcMode () ->
+ | "w64", [] when Machine.msvcMode () ->
fprintf fmt "__w64"; false
| "asm", args ->
fprintf fmt "__asm__(%a)"
@@ -2240,7 +2240,7 @@ class cil_printer () = object (self)
| _ -> (* This is the default case *)
(* Add underscores to the name *)
let an' =
- if Cil.msvcMode () then "__" ^ an else "__" ^ an ^ "__"
+ if Machine.msvcMode () then "__" ^ an else "__" ^ an ^ "__"
in
(match args with
| [] -> fprintf fmt "%s" an'
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 05b20100bcd7fc590286082dd44ea4601035536d..f5892672e43757632789c1ed84c89334b32060a4 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -1032,45 +1032,3 @@ let pp_syntactic_scope fmt = function
| Block_scope stmt -> Format.fprintf fmt "Local %a" pp_stmt stmt
| Whole_function kf ->
Format.fprintf fmt "Whole_function %a" pp_kernel_function kf
-
-let pp_mach fmt mach =
- Format.fprintf fmt
- "{sizeof_short=%a;sizeof_int=%a;sizeof_long=%a;sizeof_longlong=%a;\
- sizeof_ptr=%a;sizeof_float=%a;sizeof_double=%a;sizeof_longdouble=%a;\
- sizeof_void=%a;sizeof_fun=%a;size_t=%a;wchar_t=%a;ptrdiff_t=%a;\
- alignof_short=%a;alignof_int=%a;alignof_long=%a;alignof_longlong=%a;\
- alignof_ptr=%a;alignof_float=%a;alignof_double=%a;alignof_longdouble=%a;\
- alignof_str=%a;alignof_fun=%a;char_is_unsigned=%a;\
- little_endian=%a;alignof_aligned=%a;\
- has__builtin_va_list=%a;compiler=%a;\
- cpp_arch_flags=%a;version=%a}"
- pp_int mach.sizeof_short
- pp_int mach.sizeof_int
- pp_int mach.sizeof_long
- pp_int mach.sizeof_longlong
- pp_int mach.sizeof_ptr
- pp_int mach.sizeof_float
- pp_int mach.sizeof_double
- pp_int mach.sizeof_longdouble
- pp_int mach.sizeof_void
- pp_int mach.sizeof_fun
- pp_string mach.size_t
- pp_string mach.wchar_t
- pp_string mach.ptrdiff_t
- pp_int mach.alignof_short
- pp_int mach.alignof_int
- pp_int mach.alignof_long
- pp_int mach.alignof_longlong
- pp_int mach.alignof_ptr
- pp_int mach.alignof_float
- pp_int mach.alignof_double
- pp_int mach.alignof_longdouble
- pp_int mach.alignof_str
- pp_int mach.alignof_fun
- pp_bool mach.char_is_unsigned
- pp_bool mach.little_endian
- pp_int mach.alignof_aligned
- pp_bool mach.has__builtin_va_list
- pp_string mach.compiler
- (pp_list pp_string) mach.cpp_arch_flags
- pp_string mach.version
diff --git a/src/kernel_services/ast_printing/cil_types_debug.mli b/src/kernel_services/ast_printing/cil_types_debug.mli
index 7998dfb1d740497012a2c0be2ec4583b55d22937..7cc180218f31b1bd248acdd32dc140321372fea9 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.mli
+++ b/src/kernel_services/ast_printing/cil_types_debug.mli
@@ -156,4 +156,3 @@ val pp_kinstr : Format.formatter -> Cil_types.kinstr -> unit
val pp_cil_function : Format.formatter -> Cil_types.cil_function -> unit
val pp_kernel_function : Format.formatter -> Cil_types.kernel_function -> unit
val pp_syntactic_scope: Format.formatter -> Cil_types.syntactic_scope -> unit
-val pp_mach : Format.formatter -> Cil_types.mach -> unit
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 996ee1d5e536d7a144169972f57aeddac42442a1..9d9cfeac0df3a608cf3e335ad8d14109793e37b0 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -56,6 +56,7 @@ open Logic_const
open Cil_datatype
open Cil_types
open Cil_const
+open Machine
(* ************************************************************************* *)
(* Reporting messages *)
@@ -75,132 +76,16 @@ let abort_context msg =
in
Kernel.abort ~current:true ~append msg
-type theMachine =
- { mutable useLogicalOperators: bool;
- mutable theMachine: mach;
- (** Cil.initCil will set this to the current machine description. *)
- mutable lowerConstants: bool; (** Do lower constants (default true) *)
- mutable insertImplicitCasts: bool; (** Do insert implicit casts
- (default true) *)
- mutable stringLiteralType: typ;
- mutable upointKind: ikind;
- mutable upointType: typ;
- mutable wcharKind: ikind; (** An integer type that fits wchar_t. *)
- mutable wcharType: typ;
- mutable ptrdiffKind: ikind; (** An integer type that fits ptrdiff_t. *)
- mutable ptrdiffType: typ;
- mutable typeOfSizeOf: typ; (** An integer type that is the type of
- sizeof. *)
- mutable kindOfSizeOf: ikind;
- }
-
-let createMachine () = (* Contain dummy values *)
- { useLogicalOperators = false;
- theMachine = List.hd Cil_datatype.Machdep.reprs;
- lowerConstants = false(*true*);
- insertImplicitCasts = true;
- stringLiteralType = charConstPtrType;
- upointKind = IUChar;
- upointType = voidType;
- wcharKind = IChar;
- wcharType = voidType;
- ptrdiffKind = IChar;
- ptrdiffType = voidType;
- typeOfSizeOf = voidType;
- kindOfSizeOf = IUInt;
- }
-
-let copyMachine src dst =
- dst.useLogicalOperators <- src.useLogicalOperators;
- dst.theMachine <- src.theMachine;
- dst.lowerConstants <- src.lowerConstants;
- dst.insertImplicitCasts <- src.insertImplicitCasts;
- dst.stringLiteralType <- src.stringLiteralType;
- dst.upointKind <- src.upointKind;
- dst.upointType <- src.upointType;
- dst.wcharKind <- src.wcharKind;
- dst.wcharType <- src.wcharType;
- dst.ptrdiffKind <- src.ptrdiffKind;
- dst.ptrdiffType <- src.ptrdiffType;
- dst.typeOfSizeOf <- src.typeOfSizeOf;
- dst.kindOfSizeOf <- src.kindOfSizeOf
-
-(* A few globals that control the interpretation of C source *)
-let theMachine = createMachine ()
-
-let msvcMode () = (theMachine.theMachine.compiler = "msvc")
-let gccMode () = (theMachine.theMachine.compiler = "gcc"
- || theMachine.theMachine.compiler = "clang")
-
-let acceptEmptyCompinfo = ref false
-
-let set_acceptEmptyCompinfo () = acceptEmptyCompinfo := true
-
-let acceptEmptyCompinfo () =
- msvcMode () || gccMode () || !acceptEmptyCompinfo
-
-let allowed_machdep machdep =
- Format.asprintf
- "only allowed for %s machdeps; see option -machdep or \
- run 'frama-c -machdep help' for the list of available machdeps"
- machdep
-
-let theMachineProject = ref (createMachine ())
-
-module Machine_datatype =
- Datatype.Make
- (struct
- include Datatype.Serializable_undefined
- type t = theMachine
- let name = "theMachine"
- let reprs = [ theMachine ]
- let copy x =
- let m = createMachine () in
- copyMachine x m;
- m
- let mem_project = Datatype.never_any_project
- end)
-
-module TheMachine =
- State_builder.Register
- (Machine_datatype)
- (struct
- type t = theMachine
- let create = createMachine
- let get () = !theMachineProject
- let set m =
- theMachineProject := m;
- copyMachine !theMachineProject theMachine
- let clear m = copyMachine (createMachine ()) m
- let clear_some_projects _ _ = false
- end)
- (struct
- let name = "theMachine"
- let unique_name = name
- let dependencies = [ Kernel.Machdep.self; Kernel.LogicalOperators.self ]
- end)
-
-let selfMachine = TheMachine.self
-
-let () =
- State_dependency_graph.add_dependencies
- ~from:selfMachine
- Logic_env.builtin_states
-
-let selfMachine_is_computed = TheMachine.is_computed
-
let new_exp ~loc e = { eloc = loc; eid = Cil_const.Eid.next (); enode = e }
let dummy_exp e = { eid = -1; enode = e; eloc = Cil_datatype.Location.unknown }
-
let argsToList : (string * typ * attributes) list option
-> (string * typ * attributes) list
= function
None -> []
| Some al -> al
-
(* A hack to allow forward reference of d_exp *)
let pp_typ_ref = Extlib.mk_fun "Cil.pp_typ_ref"
let pp_global_ref = Extlib.mk_fun "Cil.pp_global_ref"
@@ -2836,10 +2721,10 @@ and childrenGlobal (vis: cilVisitor) (g: global) : global =
let bytesSizeOfInt (ik: ikind): int =
match ik with
| IChar | ISChar | IUChar | IBool -> 1
- | IInt | IUInt -> theMachine.theMachine.sizeof_int
- | IShort | IUShort -> theMachine.theMachine.sizeof_short
- | ILong | IULong -> theMachine.theMachine.sizeof_long
- | ILongLong | IULongLong -> theMachine.theMachine.sizeof_longlong
+ | IInt | IUInt -> sizeof_int ()
+ | IShort | IUShort -> sizeof_short ()
+ | ILong | IULong -> sizeof_long ()
+ | ILongLong | IULongLong -> sizeof_longlong ()
let bitsSizeOfInt ik = 8 * bytesSizeOfInt ik
@@ -2847,18 +2732,18 @@ let intKindForSize (s:int) (unsigned:bool) : ikind =
if unsigned then
(* Test the most common sizes first *)
if s = 1 then IUChar
- else if s = theMachine.theMachine.sizeof_int then IUInt
- else if s = theMachine.theMachine.sizeof_long then IULong
- else if s = theMachine.theMachine.sizeof_short then IUShort
- else if s = theMachine.theMachine.sizeof_longlong then IULongLong
+ else if s = sizeof_int () then IUInt
+ else if s = sizeof_long () then IULong
+ else if s = sizeof_short () then IUShort
+ else if s = sizeof_longlong () then IULongLong
else raise Not_found
else
(* Test the most common sizes first *)
if s = 1 then ISChar
- else if s = theMachine.theMachine.sizeof_int then IInt
- else if s = theMachine.theMachine.sizeof_long then ILong
- else if s = theMachine.theMachine.sizeof_short then IShort
- else if s = theMachine.theMachine.sizeof_longlong then ILongLong
+ else if s = sizeof_int () then IInt
+ else if s = sizeof_long () then ILong
+ else if s = sizeof_short () then IShort
+ else if s = sizeof_longlong () then ILongLong
else raise Not_found
let uint64_t () = TInt(intKindForSize 8 true,[])
@@ -2869,9 +2754,9 @@ let int32_t () = TInt(intKindForSize 4 false,[])
let int16_t () = TInt(intKindForSize 2 false,[])
let floatKindForSize (s:int) =
- if s = theMachine.theMachine.sizeof_double then FDouble
- else if s = theMachine.theMachine.sizeof_float then FFloat
- else if s = theMachine.theMachine.sizeof_longdouble then FLongDouble
+ if s = sizeof_double () then FDouble
+ else if s = sizeof_float () then FFloat
+ else if s = sizeof_longdouble () then FLongDouble
else raise Not_found
(** Returns true if and only if the given integer type is signed. *)
@@ -2889,7 +2774,7 @@ let isSigned = function
| ILongLong ->
true
| IChar ->
- not theMachine.theMachine.Cil_types.char_is_unsigned
+ not (char_is_unsigned ())
let max_signed_number nrBits =
let n = nrBits-1 in
@@ -3596,10 +3481,10 @@ let rec typeOf (e: exp) : typ =
(* The type of a string is a pointer to characters ! The only case when
* you would want it to be an array is as an argument to sizeof, but we
* have SizeOfStr for that *)
- | Const(CStr _s) -> theMachine.stringLiteralType
+ | Const(CStr _s) -> string_literal_type ()
| Const(CWStr _s) ->
- let typ = typeAddAttributes [Attr("const",[])] theMachine.wcharType in
+ let typ = typeAddAttributes [Attr("const",[])] (wchar_type ()) in
TPtr(typ,[])
| Const(CReal (_, fk, _)) -> TFloat(fk, [])
@@ -3609,8 +3494,8 @@ let rec typeOf (e: exp) : typ =
(* l-values used as r-values lose their qualifiers (C99 6.3.2.1:2) *)
| Lval lv -> type_remove_qualifier_attributes (typeOfLval lv)
- | SizeOf _ | SizeOfE _ | SizeOfStr _ -> theMachine.typeOfSizeOf
- | AlignOf _ | AlignOfE _ -> theMachine.typeOfSizeOf
+ | SizeOf _ | SizeOfE _ | SizeOfStr _ -> (sizeof_type ())
+ | AlignOf _ | AlignOfE _ -> (sizeof_type ())
| UnOp (_, _, t) -> t
| BinOp (_, _, _, t) -> t
| CastE (t, _) -> t
@@ -3808,11 +3693,8 @@ and isWFNonGhostType t =
| TPtr(t, _) | TArray(t, _, _) -> isWFNonGhostType t
| _ -> true
-(**
- **
- ** MACHINE DEPENDENT PART
- **
- **)
+(**** MACHINE DEPENDENT PART ****)
+
exception SizeOfError of string * typ
type sizeof_or_error =
@@ -3951,20 +3833,17 @@ let ignoreAlignmentAttrs = ref false
let rec bytesAlignOf t =
let alignOfType () = match t with
| TInt((IChar|ISChar|IUChar|IBool), _) -> 1
- | TInt((IShort|IUShort), _) -> theMachine.theMachine.alignof_short
- | TInt((IInt|IUInt), _) -> theMachine.theMachine.alignof_int
- | TInt((ILong|IULong), _) -> theMachine.theMachine.alignof_long
- | TInt((ILongLong|IULongLong), _) ->
- theMachine.theMachine.alignof_longlong
+ | TInt((IShort|IUShort), _) -> alignof_short ()
+ | TInt((IInt|IUInt), _) -> alignof_int ()
+ | TInt((ILong|IULong), _) -> alignof_long ()
+ | TInt((ILongLong|IULongLong), _) -> alignof_longlong ()
| TEnum (ei,_) -> bytesAlignOf (TInt(ei.ekind, []))
- | TFloat(FFloat, _) -> theMachine.theMachine.alignof_float
- | TFloat(FDouble, _) -> theMachine.theMachine.alignof_double
- | TFloat(FLongDouble, _) ->
- theMachine.theMachine.alignof_longdouble
+ | TFloat(FFloat, _) -> alignof_float ()
+ | TFloat(FDouble, _) -> alignof_double ()
+ | TFloat(FLongDouble, _) -> alignof_longdouble ()
| TNamed (t, _) -> bytesAlignOf t.ttype
| TArray (t, _, _) -> bytesAlignOf t
- | TPtr _ | TBuiltin_va_list _ ->
- theMachine.theMachine.alignof_ptr
+ | TPtr _ | TBuiltin_va_list _ -> alignof_ptr ()
(* For composite types get the maximum alignment of any field inside *)
| TComp (c, _) ->
@@ -3987,12 +3866,11 @@ let rec bytesAlignOf t =
if not (msvcMode ()) && f.fbitfield = Some 0 then sofar else
max sofar (alignOfField f)) 1 fields
(* These are some error cases *)
- | TFun _ when not (msvcMode ()) ->
- theMachine.theMachine.alignof_fun
+ | TFun _ when not (msvcMode ()) -> alignof_fun ()
| TFun _ as t -> raise (SizeOfError ("Undefined sizeof on a function.", t))
| TVoid _ as t ->
- if theMachine.theMachine.sizeof_void > 0 then
- theMachine.theMachine.sizeof_void
+ if sizeof_void () > 0 then
+ sizeof_void ()
else
raise (SizeOfError ("Undefined sizeof(void).", t))
in
@@ -4106,7 +3984,7 @@ and process_aligned_attribute (pp:Format.formatter->unit) ~may_reduce attrs defa
if rest <> [] then
Kernel.warning ~current:true "ignoring duplicate align attributes on %t"
pp;
- theMachine.theMachine.alignof_aligned
+ alignof_aligned ()
| at::_ ->
Kernel.warning ~current:true "alignment attribute \"%a\" not understood on %t"
!pp_attribute_ref at pp;
@@ -4271,19 +4149,18 @@ and bitsSizeOfEmptyArray typ =
and bitsSizeOf t =
match t with
| TInt (ik,_) -> 8 * (bytesSizeOfInt ik)
- | TFloat(FDouble, _) -> 8 * theMachine.theMachine.sizeof_double
- | TFloat(FLongDouble, _) ->
- 8 * theMachine.theMachine.sizeof_longdouble
- | TFloat _ -> 8 * theMachine.theMachine.sizeof_float
+ | TFloat(FDouble, _) -> 8 * sizeof_double ()
+ | TFloat(FLongDouble, _) -> 8 * sizeof_longdouble ()
+ | TFloat _ -> 8 * sizeof_float ()
| TEnum (ei,_) -> bitsSizeOf (TInt(ei.ekind, []))
- | TPtr _ -> 8 * theMachine.theMachine.sizeof_ptr
- | TBuiltin_va_list _ -> 8 * theMachine.theMachine.sizeof_ptr
+ | TPtr _ -> 8 * sizeof_ptr ()
+ | TBuiltin_va_list _ -> 8 * sizeof_ptr ()
| TNamed (t, _) -> bitsSizeOf t.ttype
| TComp ({cfields=None} as comp, _) ->
raise
(SizeOfError
(Format.sprintf "abstract type '%s'" (compFullName comp), t))
- | TComp ({cfields=Some[]}, _) when acceptEmptyCompinfo() ->
+ | TComp ({cfields=Some[]}, _) when acceptEmptyCompinfo () ->
find_sizeof t (fun () -> t,0)
| TComp ({cfields=Some[]} as comp,_) ->
find_sizeof t
@@ -4360,13 +4237,13 @@ and bitsSizeOf t =
raise (SizeOfError ("Array with non-constant length.", norm_typ))
end)
| TVoid _ ->
- if theMachine.theMachine.sizeof_void >= 0 then
- 8 * theMachine.theMachine.sizeof_void
+ if sizeof_void () >= 0 then
+ 8 * sizeof_void ()
else
raise (SizeOfError ("Undefined sizeof(void).", t))
| TFun _ ->
- if theMachine.theMachine.sizeof_fun >= 0 then
- 8 * theMachine.theMachine.sizeof_fun
+ if sizeof_fun () >= 0 then
+ 8 * sizeof_fun ()
else
raise (SizeOfError ("Undefined sizeof on a function.", t))
@@ -4492,20 +4369,20 @@ and constFold (machdep: bool) (e: exp) : exp =
| Const (CReal _ | CWStr _ | CStr _ | CInt64 _) -> e (* a constant *)
| SizeOf t when machdep ->
begin
- try kinteger ~loc theMachine.kindOfSizeOf (bytesSizeOf t)
+ try kinteger ~loc (sizeof_kind ()) (bytesSizeOf t)
with SizeOfError _ -> e
end
| SizeOfE { enode = Const (CWStr l) } when machdep ->
let len = List.length l in
- let wchar_size = bitsSizeOfInt theMachine.wcharKind / 8 in
- kinteger ~loc theMachine.kindOfSizeOf ((len + 1) * wchar_size)
+ let wchar_size = bitsSizeOfInt (wchar_kind ()) / 8 in
+ kinteger ~loc (sizeof_kind ()) ((len + 1) * wchar_size)
| SizeOfE e when machdep ->
constFold machdep (new_exp ~loc:e.eloc (SizeOf (typeOf e)))
| SizeOfStr s when machdep ->
- kinteger ~loc theMachine.kindOfSizeOf (1 + String.length s)
+ kinteger ~loc (sizeof_kind ()) (1 + String.length s)
| AlignOf t when machdep ->
begin
- try kinteger ~loc theMachine.kindOfSizeOf (bytesAlignOf t)
+ try kinteger ~loc (sizeof_kind ()) (bytesAlignOf t)
with SizeOfError _ -> e
end
| AlignOfE e when machdep -> begin
@@ -4513,8 +4390,7 @@ and constFold (machdep: bool) (e: exp) : exp =
* type. I know that for strings this is not true *)
match e.enode with
| Const (CStr _) when not (msvcMode ()) ->
- kinteger ~loc
- theMachine.kindOfSizeOf theMachine.theMachine.alignof_str
+ kinteger ~loc (sizeof_kind ()) (alignof_str ())
(* For an array, it is the alignment of the array ! *)
| _ -> constFold machdep (new_exp ~loc:e.eloc (AlignOf (typeOf e)))
end
@@ -4771,7 +4647,7 @@ and constFoldToInt ?(machdep=true) e =
(* Those casts are left left by constFold *)
match constFoldToInt ~machdep e with
| None -> None
- | Some i as r -> if fitsInInt theMachine.upointKind i then r else None
+ | Some i as r -> if fitsInInt (uintptr_kind ()) i then r else None
end
| _ -> None
@@ -5809,7 +5685,7 @@ let rec isConstantGen is_varinfo_cst f e = match e.enode with
to be constant. If it is truncated, we consider it non-const
in any case.
*)
- bytesSizeOfInt theMachine.upointKind <= bytesSizeOfInt i &&
+ bytesSizeOfInt (uintptr_kind ()) <= bytesSizeOfInt i &&
isConstantGen is_varinfo_cst f e
| _ -> isConstantGen is_varinfo_cst f e
end
@@ -6307,7 +6183,7 @@ let checkCast ?context ?(nullptr_cast=false) ?(fromsource=false) =
(* ISO 6.3.2.3.1 *) ()
| TInt _, TPtr _ -> (* ISO 6.3.2.3.5 *) ()
| TPtr _, TInt _ -> (* ISO 6.3.2.3.6 *)
- if not fromsource && newt != theMachine.upointType
+ if not fromsource && newt != uintptr_type ()
then
Kernel.warning
~wkey:Kernel.wkey_int_conversion
@@ -6607,7 +6483,7 @@ and mkBinOp ~loc op e1 e2 =
Kernel.debug ~level:3 "Comparison of zero and va_list";
compare_pointer ~cast1:t2 op (zero ~loc) e2
| (Le|Lt|Ge|Gt|Eq|Ne) when isPointerType t1 && isPointerType t2 ->
- compare_pointer ~cast1:theMachine.upointType ~cast2:theMachine.upointType
+ compare_pointer ~cast1:(uintptr_type ()) ~cast2:(uintptr_type ())
op e1 e2
| _ ->
Kernel.fatal
@@ -6627,8 +6503,8 @@ let mkBinOp_safe_ptr_cmp ~loc op e1 e2 =
if isPointerType t1 && isPointerType t2
&& not (isZero e1) && not (isZero e2)
then begin
- mkCast ~force:true ~newt:theMachine.upointType e1,
- mkCast ~force:true ~newt:theMachine.upointType e2
+ mkCast ~force:true ~newt:(uintptr_type ()) e1,
+ mkCast ~force:true ~newt:(uintptr_type ()) e2
end else e1, e2
| _ -> e1, e2
in
@@ -6760,7 +6636,7 @@ let rec makeZeroInit ~loc (t: typ) : init =
| TPtr _ as t ->
SingleInit(
- if theMachine.insertImplicitCasts then mkCast ~newt:t (zero ~loc)
+ if (insert_implicit_casts ()) then mkCast ~newt:t (zero ~loc)
else zero ~loc)
| x -> Kernel.fatal ~current:true "Cannot initialize type: %a" !pp_typ_ref x
@@ -6841,20 +6717,21 @@ let rec has_flexible_array_member t =
let is_flexible_array t =
match unrollType t with
| TArray (_, None, _) -> true
- | TArray (_, Some z, _) -> (msvcMode() || gccMode()) && isZero z
+ | TArray (_, Some z, _) -> (msvcMode () || gccMode ()) && isZero z
| _ -> false
in
match unrollType t with
| TComp ({ cfields = Some ((_::_) as l) },_) ->
let last = (Extlib.last l).ftype in
is_flexible_array last ||
- ((gccMode() || msvcMode()) && has_flexible_array_member last)
+ ((gccMode () || msvcMode ()) && has_flexible_array_member last)
| _ -> false
(* last_field is [true] if the given type is the type of the last field of
a struct (which could be a FAM, making the whole struct complete even if
the array type isn't. *)
-let rec isCompleteType ?(allowZeroSizeArrays=gccMode()) ?(last_field=false) t =
+let rec isCompleteType ?(allowZeroSizeArrays=gccMode ())
+ ?(last_field=false) t =
match unrollType t with
| TVoid _ -> false (* void is an incomplete type by definition (6.2.5§19) *)
| TArray(t, None, _) ->
@@ -7052,72 +6929,6 @@ let is_case_label l = match l with
| Case _ | Default _ -> true
| _ -> false
-let init_builtins_ref : (unit -> unit) ref = Extlib.mk_fun "init_builtins_ref"
-
-let initCIL ~initLogicBuiltins machdep =
- if not (TheMachine.is_computed ()) then begin
- (* Set the machine *)
- theMachine.theMachine <- machdep;
- (* Pick type for string literals *)
- theMachine.stringLiteralType <- charConstPtrType;
- (* Find the right ikind given the size *)
- let findIkindSz (unsigned: bool) (sz: int) : ikind =
- (* Test the most common sizes first *)
- if sz = theMachine.theMachine.sizeof_int then
- if unsigned then IUInt else IInt
- else if sz = theMachine.theMachine.sizeof_long then
- if unsigned then IULong else ILong
- else if sz = 1 then
- if unsigned then IUChar else IChar
- else if sz = theMachine.theMachine.sizeof_short then
- if unsigned then IUShort else IShort
- else if sz = theMachine.theMachine.sizeof_longlong then
- if unsigned then IULongLong else ILongLong
- else
- Kernel.fatal ~current:true "initCIL: cannot find the right ikind for size %d\n" sz
- in
- (* Find the right ikind given the name *)
- let findIkindName (name: string) : ikind =
- (* Test the most common sizes first *)
- if name = "int" then IInt
- else if name = "unsigned int" then IUInt
- else if name = "long" then ILong
- else if name = "unsigned long" then IULong
- else if name = "short" then IShort
- else if name = "unsigned short" then IUShort
- else if name = "char" then IChar
- else if name = "unsigned char" then IUChar
- else if name = "long long" then ILongLong
- else if name = "unsigned long long" then IULongLong
- else
- Kernel.fatal
- ~current:true "initCIL: cannot find the right ikind for type %s" name
- in
- theMachine.upointKind <- findIkindSz true theMachine.theMachine.sizeof_ptr;
- theMachine.upointType <- TInt(theMachine.upointKind, []);
- theMachine.kindOfSizeOf <-
- findIkindName theMachine.theMachine.size_t;
- theMachine.typeOfSizeOf <- TInt(theMachine.kindOfSizeOf, []);
- theMachine.wcharKind <- findIkindName theMachine.theMachine.wchar_t;
- theMachine.wcharType <- TInt(theMachine.wcharKind, []);
- theMachine.ptrdiffKind <- findIkindName theMachine.theMachine.ptrdiff_t;
- theMachine.ptrdiffType <- TInt(theMachine.ptrdiffKind, []);
- theMachine.useLogicalOperators <- Kernel.LogicalOperators.get() (* do not use lazy LAND and LOR *);
- (*nextGlobalVID <- 1 ;
- nextCompinfoKey <- 1;*)
-
- (* Have to be marked before calling [init*Builtins] below. *)
- TheMachine.mark_as_computed ();
- (* projectify theMachine *)
- copyMachine theMachine !theMachineProject;
-
- !init_builtins_ref ();
-
- Logic_env.Builtins.extend initLogicBuiltins;
-
- end
-
-
(* We want to bring all type declarations before the data declarations. This
* is needed for code of the following form:
@@ -7620,6 +7431,19 @@ let mapNoCopyList = Extlib.map_no_copy_list
let optMapNoCopy = Extlib.opt_map_no_copy
+(******************************************************************************)
+(** Forward the machine *)
+(******************************************************************************)
+
+let acceptEmptyCompinfo = acceptEmptyCompinfo
+let set_acceptEmptyCompinfo = set_acceptEmptyCompinfo
+let msvcMode = msvcMode
+let gccMode = gccMode
+
+type theMachine = machine
+
+let theMachine = theMachine [@@alert "-deprecated"]
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 0dd5e5931da9ad56dd62b294d0c5e40ef11defca..8de18151bda5db701e1d4c64d908073119b882b3 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -52,75 +52,31 @@
open Cil_types
open Cil_datatype
-(** Call this function to perform some initialization, and only after you have
- set [Cil.msvcMode]. [initLogicBuiltins] is the function to call to init
- logic builtins. The [Machdeps] argument is a description of the hardware
- platform and of the compiler used. *)
-val initCIL: initLogicBuiltins:(unit -> unit) -> mach -> unit
-
(* ************************************************************************* *)
(** {2 Customization} *)
(* ************************************************************************* *)
-type theMachine = private
- { 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 *)
- mutable theMachine: mach;
- mutable lowerConstants: bool; (** Do lower constants (default true) *)
- mutable insertImplicitCasts: bool;
- (** Do insert implicit casts (default true) *)
- mutable stringLiteralType: typ;
- mutable upointKind: ikind
- (** An unsigned integer type that fits pointers. *);
- mutable upointType: typ;
- mutable wcharKind: ikind; (** An integer type that fits wchar_t. *)
- mutable wcharType: typ;
- mutable ptrdiffKind: ikind; (** An integer type that fits ptrdiff_t. *)
- mutable ptrdiffType: typ;
- mutable typeOfSizeOf: typ;
- (** An integer type that is the type of sizeof. *)
- mutable kindOfSizeOf: ikind;
- (** The integer kind of {!Cil.typeOfSizeOf}. *)
- }
+type theMachine = Machine.machine
+(** @deprecated Frama-C+dev *)
val theMachine : theMachine
-(** Current machine description *)
-
-val selfMachine: State.t
-
-val selfMachine_is_computed: ?project:Project.project -> unit -> bool
-(** whether current project has set its machine description. *)
+[@@alert deprecated "Use Machine getter functions instead"]
+(** @deprecated Frama-C+dev *)
val msvcMode: unit -> bool
+[@@alert deprecated "Use Machine.msvcMode instead"]
+
+(** @deprecated Frama-C+dev *)
val gccMode: unit -> bool
+[@@alert deprecated "Use Machine.gccMode instead"]
+(** @deprecated Frama-C+dev *)
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 23.0-Vanadium
-*)
+[@@alert deprecated "Use Machine.set_acceptEmptyCompinfo instead"]
+(** @deprecated Frama-C+dev *)
val acceptEmptyCompinfo: unit -> bool
-(** whether we accept empty struct. Implied by {!Cil.msvcMode} and
- {!Cil.gccMode}, and can be forced by {!Cil.set_acceptEmptyCompinfo}
- otherwise.
-
- @since 23.0-Vanadium
-*)
-
-val allowed_machdep: string -> string
-(** [allowed_machdep "machdep family"] provides a standard message for features
- only allowed for a particular machdep.
-
- @since 25.0-Manganese
-*)
+[@@alert deprecated "Use Machine.acceptEmptyCompinfo instead"]
(* ************************************************************************* *)
(** {2 Values for manipulating globals} *)
@@ -2287,7 +2243,7 @@ val floatKindForSize : int-> fkind
(** The size of a type, in bits. Trailing padding is added for structs and
arrays. Raises {!Cil.SizeOfError} when it cannot compute the size. This
function is architecture dependent, so you should only call this after you
- call {!Cil.initCIL}. Remember that on GCC sizeof(void) is 1! *)
+ call {!Machine.init}. Remember that on GCC sizeof(void) is 1! *)
val bitsSizeOf: typ -> int
(** The size of a type, in bytes. Raises {!Cil.SizeOfError} when it cannot
@@ -2362,12 +2318,12 @@ val intKindForValue: Integer.t -> bool -> ikind
(** The size of a type, in bytes. Returns a constant expression or a "sizeof"
expression if it cannot compute the size. This function is architecture
- dependent, so you should only call this after you call {!Cil.initCIL}. *)
+ dependent, so you should only call this after you call {!Machine.init}. *)
val sizeOf: loc:location -> typ -> exp
(** The minimum alignment (in bytes) for a type. This function is
architecture dependent, so you should only call this after you call
- {!Cil.initCIL}.
+ {!Machine.init}.
@raise {!SizeOfError} when it cannot compute the alignment. *)
val bytesAlignOf: typ -> int
@@ -2380,14 +2336,14 @@ val intOfAttrparam: attrparam -> int option
base address and the width (also expressed in bits) for the subobject
denoted by the offset. Raises {!Cil.SizeOfError} when it cannot compute
the size. This function is architecture dependent, so you should only call
- this after you call {!Cil.initCIL}. *)
+ this after you call {!Machine.init}. *)
val bitsOffset: typ -> offset -> int * int
(** Give a field, returns the number of bits from the structure or union
containing the field and the width (also expressed in bits) for the subobject
denoted by the field. Raises {!Cil.SizeOfError} when it cannot compute
the size. This function is architecture dependent, so you should only call
- this after you call {!Cil.initCIL}. *)
+ this after you call {!Machine.init}. *)
val fieldBitsOffset: fieldinfo -> int * int
(** Like map but try not to make a copy of the list
@@ -2513,12 +2469,6 @@ val set_extension_handler:
@since 21.0-Scandium
*)
-(* ***********************************************************************)
-(** {2 Forward references} *)
-(* ***********************************************************************)
-
-val init_builtins_ref: (unit -> unit) ref
-
(** void
@deprecated Frama-C+dev *)
val voidType: typ
diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index 1a6dc1cdbda38ab9379de4084625ef1b51742409..d12e5ddc27e37268c58667fb25095345ed2ec9d7 100644
--- a/src/kernel_services/ast_queries/cil_builtins.ml
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -90,7 +90,7 @@ module Builtin_functions =
(Datatype.Triple(Typ)(Datatype.List(Typ))(Datatype.Bool))
(struct
let name = "Builtin_functions"
- let dependencies = [ Cil.selfMachine ]
+ let dependencies = [ Machine.self ]
let size = 49
end)
@@ -261,7 +261,7 @@ let build_type_table () : (string, typ option) Hashtbl.t =
let types =
[
("__builtin_va_list",
- Some (if Cil.theMachine.theMachine.has__builtin_va_list
+ Some (if Machine.has_builtin_va_list ()
then TBuiltin_va_list []
else Cil_const.voidPtrType));
("char *", Some Cil_const.charPtrType);
@@ -294,7 +294,7 @@ let build_type_table () : (string, typ option) Hashtbl.t =
("void", Some Cil_const.voidType);
("void *", Some Cil_const.voidPtrType);
("void const *", Some Cil_const.voidConstPtrType);
- ("size_t", Some Cil.theMachine.typeOfSizeOf);
+ ("size_t", Some (Machine.sizeof_type ()));
("int8_t", int8_t);
("int16_t", int16_t);
("int32_t", int32_t);
@@ -337,7 +337,7 @@ let parse_type ?(template="") type_table s =
Kernel.fatal "invalid type '%s' in compiler_builtins JSON" s
let is_machdep_active compiler =
- match compiler, Cil.gccMode (), Cil.msvcMode () with
+ match compiler, Machine.gccMode (), Machine.msvcMode () with
| None, _, _ (* always active *)
| Some GCC, true, _
| Some MSVC, _, true
@@ -401,7 +401,7 @@ let init_other_builtin_templates () =
let init_builtins_from_json () =
(* For performance reasons, we avoid loading GCC builtins unless we are
using a GCC machdep *)
- if Cil.gccMode () then init_gcc_builtin_templates ();
+ if Machine.gccMode () then init_gcc_builtin_templates ();
init_other_builtin_templates ();
let type_table = build_type_table () in
Builtin_templates.iter (fun name entry ->
@@ -412,8 +412,9 @@ let init_builtins_from_json () =
)
let init_builtins () =
- if not (Cil.selfMachine_is_computed ()) then
- Kernel.fatal ~current:true "You must call initCIL before init_builtins" ;
+ if not (Machine.is_computed ()) then
+ Kernel.fatal ~current:true
+ "You must call Machine.init before init_builtins" ;
if Builtin_functions.length () <> 0 then
Kernel.fatal ~current:true "Cil builtins already initialized." ;
init_builtins_from_json ();
@@ -423,4 +424,4 @@ let init_builtins () =
let builtinLoc: location = Location.unknown
let () =
- Cil.init_builtins_ref := init_builtins
+ Machine.init_builtins_ref := init_builtins
diff --git a/src/kernel_services/ast_queries/cil_builtins.mli b/src/kernel_services/ast_queries/cil_builtins.mli
index ca5ff1cbd912c1e69493fa6e6368f0ea8a91badc..78f9f25aec01012ab65b3a4e24a69dfcf5808e7e 100644
--- a/src/kernel_services/ast_queries/cil_builtins.mli
+++ b/src/kernel_services/ast_queries/cil_builtins.mli
@@ -90,9 +90,9 @@ val add_special_builtin_family: (string -> bool) -> unit
val init_builtins: unit -> unit
(** A list of the built-in functions for the current compiler (GCC or
- MSVC, depending on [!msvcMode]). Maps the name to the
+ MSVC, depending on [!Machine.msvcMode]). Maps the name to the
result and argument types, and whether it is vararg.
- Initialized by {!Cil.initCIL}. Do not add builtins directly, use
+ Initialized by {!Machine.init}. Do not add builtins directly, use
{! add_custom_builtin } below for that.
This map replaces [gccBuiltins] and [msvcBuiltins] in previous
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index ba258b3485f0075d75ee68d337d6bc5a172f7925..799e52d1780be8acb3b81c5e2cea92f2c4bf2abe 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2677,88 +2677,6 @@ module Syntactic_scope =
Location.pretty (Stmt.loc s) Stmt.pretty s
end)
-let dummy_machdep =
- {
- sizeof_short = 2;
- sizeof_int = 4;
- sizeof_long = 8;
- sizeof_longlong = 8;
- sizeof_ptr = 8;
- sizeof_float = 4;
- sizeof_double = 8;
- sizeof_longdouble = 16;
- sizeof_void = -1;
- sizeof_fun = -1;
- size_t = "unsigned long";
- ssize_t = "long";
- wchar_t = "int";
- ptrdiff_t = "long";
- intptr_t = "long"; (* Type of "intptr_t" *)
- uintptr_t = "unsigned long"; (* Type of "uintptr_t" *)
- int_fast8_t = "signed char";
- int_fast16_t = "long";
- int_fast32_t = "long";
- int_fast64_t = "long";
- uint_fast8_t = "unsigned char";
- uint_fast16_t = "unsigned long";
- uint_fast32_t = "unsigned long";
- uint_fast64_t = "unsigned long";
- wint_t = "int";
- sig_atomic_t = "int";
- time_t = "long";
- alignof_short = 2;
- alignof_int = 4;
- alignof_long = 8;
- alignof_longlong = 8;
- alignof_ptr = 8;
- alignof_float = 4;
- alignof_double = 8;
- alignof_longdouble = 16;
- alignof_str = 1;
- alignof_fun = -1;
- char_is_unsigned = true;
- little_endian = true;
- alignof_aligned = 16;
- has__builtin_va_list = true;
- compiler = "none";
- cpp_arch_flags = [];
- version = "N/A";
- weof = "(-1)";
- wordsize = "64";
- posix_version = "";
- bufsiz = "255";
- eof = "(-1)";
- fopen_max = "255";
- filename_max = "4095";
- path_max = "256";
- tty_name_max = "255";
- host_name_max = "255";
- l_tmpnam = "63";
- tmp_max = "1024";
- rand_max = "0xFFFFFFFE";
- mb_cur_max = "16";
- nsig = "";
- errno = [
- "edom", "33";
- "eilseq", "84";
- "erange", "34";
- ];
- machdep_name = "dummy";
- custom_defs = [];
- }
-
-module Machdep = Datatype.Make_with_collections(struct
- include Datatype.Serializable_undefined
- let reprs = [dummy_machdep]
- let name = "Machdep"
- type t = Cil_types.mach
- let compare : t -> t -> int = Stdlib.compare
- let equal : t -> t -> bool = (=)
- let hash : t -> int = Hashtbl.hash
- let copy = Datatype.identity
- end)
-
-
(* -------------------------------------------------------------------------- *)
(* --- Internal --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index 3e83fb181b5df9076b47317d62204a23b9bdf46f..7721ea20804f2149b9e1834aadb0463f878a0e31 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -385,13 +385,6 @@ module PredicateStructEq: S_with_collections_pretty with type t = predicate
module Lexpr: S with type t = Logic_ptree.lexpr
(** Beware: no pretty-printer is available. *)
-(**************************************************************************)
-(** {3 Machdep} *)
-(**************************************************************************)
-
-module Machdep: S_with_collections with type t = mach
-(** since 27.0-Cobalt *)
-
(**/**)
(* ****************************************************************************)
(** {2 Internal API} *)
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 234bd09e5f6a41fd1fc26b8e4cdbfa6958764ba3..9159303d7abd765876d7a098d2dfccaee8840ff2 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -220,9 +220,8 @@ let pre_register = Files.pre_register
(* ************************************************************************* *)
(* not exported, see [pretty_machdep] below. *)
-let print_machdep fmt (m : Cil_types.mach) =
+let print_machdep fmt (m : Machdep.mach) =
begin
- let open Cil_types in
Format.fprintf fmt "Machine: %s@\n" m.version ;
let pp_size_error fmt v =
if v < 0
@@ -314,7 +313,7 @@ let set_machdep () =
let () = Cmdline.run_after_configuring_stage set_machdep
-(* Local to this module. Use Cil.theMachine.theMachine outside *)
+(* Local to this module. Use Machine module instead. *)
let get_machdep () =
let m = Kernel.Machdep.get () in
let file =
@@ -324,7 +323,7 @@ let get_machdep () =
let res =
Result.bind
(Yaml_unix.of_file (Fpath.v (file:>string)))
- Cil_types.mach_of_yaml
+ Machdep.mach_of_yaml
in
match res with
| Ok machdep -> machdep
@@ -1199,12 +1198,12 @@ let prepare_cil_file ast =
Ast.set_file ast
let fill_built_ins () =
- if Cil.selfMachine_is_computed () then begin
+ if Machine.is_computed () then begin
Kernel.debug "Machine is computed, just fill the built-ins";
Cil_builtins.init_builtins ();
end else begin
Kernel.debug "Machine is not computed, initialize everything";
- Cil.initCIL ~initLogicBuiltins:(Logic_builtin.init()) (get_machdep ());
+ Machine.init ~initLogicBuiltins:(Logic_builtin.init()) (get_machdep ());
end;
(* Fill logic tables with builtins *)
Logic_env.Builtins.apply ();
@@ -1622,7 +1621,7 @@ let reorder_ast () = reorder_custom_ast (Ast.get())
(* Fill logic tables with builtins *)
let init_cil () =
- Cil.initCIL ~initLogicBuiltins:(Logic_builtin.init()) (get_machdep ());
+ Machine.init ~initLogicBuiltins:(Logic_builtin.init()) (get_machdep ());
Logic_env.Builtins.apply ();
Logic_env.prepare_tables ()
diff --git a/src/kernel_services/ast_queries/file.mli b/src/kernel_services/ast_queries/file.mli
index 71522e5e2951d31b84c50feac5550c999d1b92ca..094063499a002f73dd2287747bd8e01bebabe686 100644
--- a/src/kernel_services/ast_queries/file.mli
+++ b/src/kernel_services/ast_queries/file.mli
@@ -231,7 +231,7 @@ val reorder_custom_ast: Cil_types.file -> unit
(* ************************************************************************* *)
val pretty_machdep :
- ?fmt:Format.formatter -> ?machdep:Cil_types.mach -> unit -> unit
+ ?fmt:Format.formatter -> ?machdep:Machdep.mach -> unit -> unit
(** Prints the associated [machdep], or the current one in current project
by default. Default output formatter is [Log.print_on_output]. *)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index bb10728f604db1e0ae4887571518a7400d81b121..7fbbc120b5405515bcdc851714bce589bc832134 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -907,7 +907,7 @@ struct
| 'L' -> (* L'wide_char' *)
let content = String.sub s 2 (String.length s - 3) in
let tokens = explode content in
- let value = Cil.reduce_multichar Cil.theMachine.Cil.wcharType tokens
+ let value = Cil.reduce_multichar (Machine.wchar_type ()) tokens
in
tinteger_s64 ~loc value
| '\'' -> (* 'char' *)
@@ -2576,7 +2576,7 @@ struct
TConst (LStr (unescape s)), Ctype Cil_const.charPtrType
| PLconstant (WStringConstant s) ->
TConst (LWStr (wcharlist_of_string s)),
- Ctype (TPtr(Cil.theMachine.wcharType,[]))
+ Ctype (TPtr(Machine.wchar_type (),[]))
| PLvar x ->
let old_val info =
let typ =
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 7867e987c3d7d102ff7f996afd7225820674e48d..690e9c8def3c19e111e4d27f3a62ec67a2cf9760 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -2458,7 +2458,7 @@ and constFoldCastToInt ~machdep typ e =
try
let ik = match Cil.unrollType typ with
| TInt (ik, _) -> ik
- | TPtr _ -> theMachine.upointKind
+ | TPtr _ -> Machine.uintptr_kind ()
| TEnum (ei,_) -> ei.ekind
| _ -> raise Exit
in
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index faccb2fa50e841c7849a6d455e19dee60aa7d351..542efe1f658b28233203430cb2bc78d2fffd3556 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -744,7 +744,7 @@ let type_expr metaenv env ?tr ?current e =
let t =
Logic_const.term
(TConst (LWStr (Logic_typing.wcharlist_of_string s)))
- (Ctype (TPtr(Cil.theMachine.wcharType,[])))
+ (Ctype (TPtr(Machine.wchar_type (),[])))
in env,t,cond
| PBinop(bop,e1,e2) ->
let op = Logic_typing.type_binop bop in
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index ed2bd6ff624a609e08000761168a1e4f62901104..ad5a3600c9e441c2ed9675ef887191f9c8bff5ba 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -228,11 +228,11 @@ let replace_all_args_ival li args_ival =
let infer_sizeof ty =
try singleton_of_int (Cil.bytesSizeOf ty)
- with Cil.SizeOfError _ -> interv_of_typ Cil.theMachine.Cil.typeOfSizeOf
+ with Cil.SizeOfError _ -> interv_of_typ (Machine.sizeof_type ())
let infer_alignof ty =
try singleton_of_int (Cil.bytesAlignOf ty)
- with Cil.SizeOfError _ -> interv_of_typ Cil.theMachine.Cil.typeOfSizeOf
+ with Cil.SizeOfError _ -> interv_of_typ (Machine.sizeof_type ())
(* Infer the interval of an extended quantifier \sum or \product.
[lambda] is the interval of the lambda term, [min] (resp. [max]) is the
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index 324c524514be8d7c321bd78e21042f47028979b2..51d50aaa5186fb5403f70bc17617a4b971bf2bef 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -58,7 +58,7 @@ let get_set_suffix_and_arg res_ty e =
| Gmpz, Rational -> "_z", [ e ]
| Rational, Gmpz -> "_q", [ e ]
| C_integer IChar, _ ->
- (if Cil.theMachine.Cil.theMachine.char_is_unsigned then "_ui"
+ (if Machine.char_is_unsigned () then "_ui"
else "_si"),
args_uisi e
| C_integer (IBool | IUChar | IUInt | IUShort | IULong), _ ->
diff --git a/src/plugins/e-acsl/src/code_generator/libc.ml b/src/plugins/e-acsl/src/code_generator/libc.ml
index 766c93a81c36301c2e0086117a5ace68f1061eab..36b3973bd43e68618ed8063cbe73998b1aed73e0 100644
--- a/src/plugins/e-acsl/src/code_generator/libc.ml
+++ b/src/plugins/e-acsl/src/code_generator/libc.ml
@@ -125,7 +125,7 @@ let strlen ~loc ~name env kf e =
~name
env
kf
- Cil.theMachine.typeOfSizeOf
+ (Machine.sizeof_type ())
"builtin_strlen"
[ e ]
@@ -206,8 +206,8 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
(* We know that [t] can be translated to a C type, so we start with that *)
let e, _, env = Translate_terms.to_exp ~adata:Assert.no_data kf env t in
(* Then we can check if the expression will fit in a [size_t] *)
- let sizet = Cil.(theMachine.typeOfSizeOf) in
- let sizet_kind = Cil.(theMachine.kindOfSizeOf) in
+ let sizet = Machine.sizeof_type () in
+ let sizet_kind = Machine.sizeof_kind () in
let check_lower_bound, check_upper_bound =
let lower, upper =
match nty with
@@ -360,7 +360,7 @@ let update_memory_model ~loc ?result env kf caller args =
| "fread", [ buffer_e; size_e; _; _ ] ->
let result, env =
- get_result_var ~loc ~name kf Cil.theMachine.typeOfSizeOf env result
+ get_result_var ~loc ~name kf (Machine.sizeof_type ()) env result
in
let env = Env.push env in
let result_t = lval_to_term ~loc result in
@@ -476,7 +476,7 @@ let update_memory_model ~loc ?result env kf caller args =
env
kf
None
- Cil.theMachine.typeOfSizeOf
+ (Machine.sizeof_type ())
(fun _ _ -> [])
in
let env = Env.push env in
diff --git a/src/plugins/e-acsl/src/code_generator/logic_array.ml b/src/plugins/e-acsl/src/code_generator/logic_array.ml
index 2b8566382d0c12de0f3f849ef7da6141a6ca2bdd..97ca7bdcb6d14c2806f47597508ca83c0f4fce31 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_array.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_array.ml
@@ -56,7 +56,7 @@ let length_exp ~loc kf env ~name array =
env
kf
None
- Cil.theMachine.typeOfSizeOf
+ (Machine.sizeof_type ())
name
[ array ]
in
@@ -74,7 +74,7 @@ let length_exp ~loc kf env ~name array =
kf
None
~name
- Cil.theMachine.typeOfSizeOf
+ (Machine.sizeof_type ())
(fun v _ -> [
Smart_stmt.assigns
~loc
@@ -166,7 +166,7 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
kf
None
~name:"iter"
- Cil.theMachine.typeOfSizeOf
+ (Machine.sizeof_type ())
(fun _ _ -> [])
in
diff --git a/src/plugins/e-acsl/src/code_generator/translate_ats.ml b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
index 670f7316b9e3d9aa1d86a3617fc0efa4341d1e5e..f7bfcc06715baad3b6fdba56a872043391ba7f00 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_ats.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
@@ -341,7 +341,7 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
ty_ptr
(fun vi e ->
(* Handle [malloc] and [free] stmts *)
- let lty_sizeof = Ctype Cil.(theMachine.typeOfSizeOf) in
+ let lty_sizeof = Ctype (Machine.sizeof_type ()) in
let t_sizeof = Logic_const.term ~loc (TSizeOf ty) lty_sizeof in
let t_size = size_from_sizes_and_shifts ~loc sizes_and_shifts in
let t_size =
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index e0693bd7f5e9036398966778435a77744f0bf4e1..a2dcfd36b7b8c12fc540734a0ebad5fdf3739609 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -820,7 +820,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
e, adata, env, Analyses_types.C_number, name
| Tbase_addr _ -> Env.not_yet env "labeled \\base_addr"
| Toffset(BuiltinLabel Here, t') ->
- let size_t = Cil.theMachine.Cil.typeOfSizeOf in
+ let size_t = Machine.sizeof_type () in
let name = "offset" in
let e, adata, env =
Memory_translate.call ~adata ~loc kf name size_t env t'
@@ -829,7 +829,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
e, adata, env, Analyses_types.C_number, name
| Toffset _ -> Env.not_yet env "labeled \\offset"
| Tblock_length(BuiltinLabel Here, t') ->
- let size_t = Cil.theMachine.Cil.typeOfSizeOf in
+ let size_t = Machine.sizeof_type () in
let name = "block_length" in
let e, adata, env =
Memory_translate.call ~adata ~loc kf name size_t env t'
diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.ml b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
index 0a97fa252a8d8709c4d23fbd9a784d9d7954810f..cea3235a866d0e0ec8355b138709f28edf10f86c 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_utils.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
@@ -86,7 +86,7 @@ let () =
let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
let logic_env = Env.Logic_env.get env in
let pp = match pp with Some size_pp -> size_pp | None -> t in
- let sizet = Cil.(theMachine.typeOfSizeOf) in
+ let sizet = Machine.sizeof_type () in
let stmts = [] in
(* Lower guard *)
let stmts, env =
diff --git a/src/plugins/eva/ast/eva_ast_builder.ml b/src/plugins/eva/ast/eva_ast_builder.ml
index b0e7b16dd059be1c1c3bc3fb5c0d4df822f07074..1faa1e6f1dc9af1562e723b2e979439ee994ff4b 100644
--- a/src/plugins/eva/ast/eva_ast_builder.ml
+++ b/src/plugins/eva/ast/eva_ast_builder.ml
@@ -82,7 +82,7 @@ let rec translate_exp (e : Cil_types.exp) =
| SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ ->
match (Cil.constFold true e).enode with
| Const c -> Const (translate_constant c)
- | _ -> Const (CTopInt Cil.theMachine.kindOfSizeOf)
+ | _ -> Const (CTopInt (Machine.sizeof_kind ()))
in
mk_exp ~origin:(Exp e) node
@@ -191,7 +191,7 @@ struct
Cil.arithmeticConversion e1.typ e2.typ
else if Cil.isPointerType e1.typ && Cil.isPointerType e2.typ then
if Cil.need_cast ~force:true e1.typ e2.typ then
- Cil.theMachine.upointType
+ Machine.uintptr_type ()
else
e1.typ
else
@@ -241,7 +241,7 @@ let zero_typed (typ : Cil_types.typ) =
| TEnum ({ekind = ik },_)
| TInt (ik, _) -> mk_exp (Const (CInt64 (Integer.zero, ik, None)))
| TPtr _ ->
- let ik = Cil.(theMachine.upointKind) in
+ let ik = Machine.uintptr_kind () in
let zero = mk_exp (Const (CInt64 (Integer.zero, ik, None))) in
Build.cast typ zero
| typ ->
diff --git a/src/plugins/eva/ast/eva_ast_typing.ml b/src/plugins/eva/ast/eva_ast_typing.ml
index 5ea656ded20229f94b1fee48d9fffbe7b1fd08bb..7b68db5d9c0617b4be735588e77270d0361631e7 100644
--- a/src/plugins/eva/ast/eva_ast_typing.ml
+++ b/src/plugins/eva/ast/eva_ast_typing.ml
@@ -26,8 +26,8 @@ let type_of_const : constant -> typ = function
| CTopInt ik -> Cil_types.TInt (ik, [])
| CInt64 (_, ik, _) -> Cil_types.TInt (ik, [])
| CChr _ -> Cil_const.intType
- | CString (String (_, Base.CSString _)) -> Cil.theMachine.stringLiteralType
- | CString (String (_, Base.CSWstring _)) -> TPtr (Cil.theMachine.wcharType, [])
+ | CString (String (_, Base.CSString _)) -> Machine.string_literal_type ()
+ | CString (String (_, Base.CSWstring _)) -> TPtr (Machine.wchar_type (), [])
| CString (_) -> assert false (* it must be a String base*)
| CReal (_, fk, _) -> TFloat (fk, [])
| CEnum (_ei, e) -> e.typ
diff --git a/src/plugins/eva/ast/eva_ast_utils.ml b/src/plugins/eva/ast/eva_ast_utils.ml
index 49e282a4613db3579499801005caf11a70209b04..205521b9bb4c25350555015a7e5c6769077ae6dc 100644
--- a/src/plugins/eva/ast/eva_ast_utils.ml
+++ b/src/plugins/eva/ast/eva_ast_utils.ml
@@ -254,7 +254,7 @@ let rec to_integer e =
| CastE (typ, e) when Cil.isPointerType typ ->
begin
match to_integer e with
- | Some i as r when Cil.fitsInInt Cil.theMachine.upointKind i -> r
+ | Some i as r when Cil.fitsInInt (Machine.uintptr_kind ()) i -> r
| _ -> None
end
| _ -> None
diff --git a/src/plugins/eva/domains/cvalue/builtins.ml b/src/plugins/eva/domains/cvalue/builtins.ml
index 8cfee381861efc145d1e16ebd17f91d670211f49..caea7c82475f1357a685857730e5471d074e5972 100644
--- a/src/plugins/eva/domains/cvalue/builtins.ml
+++ b/src/plugins/eva/domains/cvalue/builtins.ml
@@ -171,7 +171,7 @@ let prepare_builtin kf (name, builtin, cacheable, expected_typ) =
(got: %a. Machdep is %s)."
name Kernel_function.pretty kf
Printer.pp_typ (Kernel_function.get_type kf)
- Cil.theMachine.theMachine.machdep_name
+ (Machine.machdep_name ())
else
match find_builtin_specification kf with
| None ->
diff --git a/src/plugins/eva/domains/cvalue/builtins_malloc.ml b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
index b3be407a16dc51214105da5fa528e8022ab01f9b..6a76e17173e060dbf7cd7aec605e8dc3cf931154 100644
--- a/src/plugins/eva/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
@@ -493,7 +493,7 @@ let register_malloc ?replace name ?returns_null prefix region =
Builtins.Full { c_values; c_clobbered; c_assigns = None; }
in
let name = "Frama_C_" ^ name in
- let typ () = Cil_const.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf] in
+ let typ () = Cil_const.voidPtrType, [Machine.sizeof_type ()] in
Builtins.register_builtin ?replace name NoCacheCallers builtin ~typ
let () =
@@ -548,7 +548,7 @@ let () =
let name = "Frama_C_calloc" in
let replace = "calloc" in
let typ () =
- let sizeof_typ = Cil.theMachine.Cil.typeOfSizeOf in
+ let sizeof_typ = Machine.sizeof_type () in
Cil_const.voidPtrType, [ sizeof_typ; sizeof_typ ]
in
Builtins.register_builtin ~replace name NoCacheCallers calloc_builtin ~typ
@@ -840,7 +840,7 @@ let realloc_builtin state args =
let () =
let name = "Frama_C_realloc" in
let replace = "realloc" in
- let typ () = Cil_const.(voidPtrType, [voidPtrType; Cil.theMachine.typeOfSizeOf]) in
+ let typ () = Cil_const.(voidPtrType, [voidPtrType; Machine.sizeof_type ()]) in
Builtins.register_builtin ~replace name NoCacheCallers realloc_builtin ~typ
let reallocarray_builtin state args =
@@ -875,7 +875,7 @@ let () =
let replace = "reallocarray" in
let typ () =
Cil_const.voidPtrType,
- [Cil_const.voidPtrType; Cil.theMachine.typeOfSizeOf; Cil.theMachine.typeOfSizeOf]
+ [Cil_const.voidPtrType; Machine.sizeof_type (); Machine.sizeof_type ()]
in
Builtins.register_builtin
~replace name NoCacheCallers reallocarray_builtin ~typ
diff --git a/src/plugins/eva/domains/cvalue/builtins_string.ml b/src/plugins/eva/domains/cvalue/builtins_string.ml
index 6700057446dfe5eea01141f97a5b600266f55769..3de4a2bc5f763419dad8cba6ece4409052f05ed0 100644
--- a/src/plugins/eva/domains/cvalue/builtins_string.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_string.ml
@@ -353,11 +353,11 @@ type char = Char | Wide
let bits_size = function
| Char -> Integer.eight
- | Wide -> Integer.of_int (Cil.bitsSizeOf Cil.theMachine.Cil.wcharType)
+ | Wide -> Integer.of_int (Cil.bitsSizeOf (Machine.wchar_type ()))
let signed_char = function
- | Char -> not Cil.(theMachine.theMachine.Cil_types.char_is_unsigned)
- | Wide -> Cil.isSignedInteger Cil.theMachine.Cil.wcharType
+ | Char -> not (Machine.char_is_unsigned ())
+ | Wide -> Cil.isSignedInteger (Machine.wchar_type ())
(* Converts the searched characters into char; needed for strchr and memchr. *)
let searched_char ~size ~signed cvalue =
diff --git a/src/plugins/eva/domains/cvalue/cvalue_init.ml b/src/plugins/eva/domains/cvalue/cvalue_init.ml
index 8d4cc1bdc56ca48bbdcdf1d95bde7b30ead79932..2d812edf25cfd1ddad185468426eb0bb78c42b0b 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_init.ml
@@ -99,7 +99,7 @@ let create_hidden_base ~libc ~valid ~hidden_var_name ~name_desc pointed_typ =
let reject_empty_struct b offset typ =
match Cil.unrollType typ with
| TComp (ci, _) ->
- if ci.cfields = Some [] && not (Cil.acceptEmptyCompinfo ()) then
+ if ci.cfields = Some [] && not (Machine.acceptEmptyCompinfo ()) then
Self.abort ~current:true
"@[empty %ss@ are unsupported@ (type '%a',@ location %a%a)@ \
in C99 (only allowed on GCC/MSVC machdep).@ Aborting.@]"
diff --git a/src/plugins/eva/engine/evaluation.ml b/src/plugins/eva/engine/evaluation.ml
index b2c7612309d6ec61dd52cb24c6206d94bf1d94fb..2226ae760c9f8e4fb479b46d1d769c9fccbd2c02 100644
--- a/src/plugins/eva/engine/evaluation.ml
+++ b/src/plugins/eva/engine/evaluation.ml
@@ -166,7 +166,7 @@ let rec signed_counterpart typ =
| TEnum ({ekind = ik} as info, attrs) ->
let info = { info with ekind = signed_ikind ik} in
TEnum (info, attrs)
- | TPtr _ -> signed_counterpart Cil.(theMachine.upointType)
+ | TPtr _ -> signed_counterpart ((Machine.uintptr_type ()))
| _ -> assert false
let return t = `Value t, Alarmset.none
diff --git a/src/plugins/eva/utils/eval_typ.ml b/src/plugins/eva/utils/eval_typ.ml
index 9b2cc6ad98f71eb78cadd6ccde53e6c7c72ea74b..69649a738b3b319bb93158709b0077273d87d59b 100644
--- a/src/plugins/eva/utils/eval_typ.ml
+++ b/src/plugins/eva/utils/eval_typ.ml
@@ -180,7 +180,7 @@ type scalar_typ =
| TSFloat of fkind
let pointer_range () =
- { i_bits = Cil.bitsSizeOfInt Cil.theMachine.Cil.upointKind;
+ { i_bits = Cil.bitsSizeOfInt (Machine.uintptr_kind ());
i_signed = false; }
let classify_as_scalar typ =
diff --git a/src/plugins/eva/values/cvalue_backward.ml b/src/plugins/eva/values/cvalue_backward.ml
index b4ba8bff308f2cb7303e551bdaf2125b49d7dd13..9ef10661e36bddb37d7b1453820bde16d0af4843 100644
--- a/src/plugins/eva/values/cvalue_backward.ml
+++ b/src/plugins/eva/values/cvalue_backward.ml
@@ -357,7 +357,7 @@ let backward_unop ~typ_arg op ~arg:_ ~res =
(* ikind of an (unrolled) integer type *)
let ikind = function
| TInt (ik, _) | TEnum ({ekind = ik}, _) -> ik
- | TPtr _ -> Cil.(theMachine.upointKind)
+ | TPtr _ -> Machine.uintptr_kind ()
| _ -> assert false
(* does [v] fits in the integer type corresponding to [ik]? *)
diff --git a/src/plugins/eva/values/offsm_value.ml b/src/plugins/eva/values/offsm_value.ml
index fd657c92ee4eed9e274e71018eb4eceb00246e94..9118e16727e56e6663f176b43e60c583a141298c 100644
--- a/src/plugins/eva/values/offsm_value.ml
+++ b/src/plugins/eva/values/offsm_value.ml
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
-open Cil_types
open Eval
open Cvalue
open Abstract_interp
@@ -281,7 +280,7 @@ type shift_direction = Left | Right
(* The value of the sign bit, expressed as a cvalue. *)
let sign_bit size offsm =
let sign_bit =
- if Cil.theMachine.theMachine.little_endian
+ if Machine.little_endian ()
then Int.pred size
else Int.zero
in
@@ -304,7 +303,7 @@ let shift ~size ~signed offsm shift_direction n =
then result (* Undefined behavior: we don't care about the result. *)
else
let size_copy = Int.sub size n in
- let little_endian = Cil.theMachine.theMachine.little_endian in
+ let little_endian = Machine.little_endian () in
let start_copy, start_paste =
if (shift_direction = Left) = little_endian
then Int.zero, n
@@ -316,7 +315,7 @@ let shift ~size ~signed offsm shift_direction n =
(** Casts *)
let cast ~old_size ~new_size ~signed offsm =
- let little_endian = Cil.theMachine.theMachine.little_endian in
+ let little_endian = Machine.little_endian () in
if Int.equal old_size new_size then offsm
else if Int.lt new_size old_size then (* Truncation *)
let start = if little_endian then Int.zero else Int.sub old_size new_size in
diff --git a/src/plugins/variadic/standard.ml b/src/plugins/variadic/standard.ml
index 964ef79b02beeb52c2144ad316eef76ef3c00864..043273fdc5cebdc93f9ada849fd504b8b63748d6 100644
--- a/src/plugins/variadic/standard.ml
+++ b/src/plugins/variadic/standard.ml
@@ -425,7 +425,7 @@ let find_predicate_by_width typ narrow_name wide_name =
(* drop attributes to remove 'const' qualifiers and fc_stdlib attributes *)
Cil_datatype.Typ.equal
(Cil.typeDeepDropAllAttributes (Cil.unrollTypeDeep t))
- Cil.theMachine.Cil.wcharType ->
+ (Machine.wchar_type ()) ->
find_predicate wide_name
| _ ->
Self.warning ~current:true ~wkey:wkey_typing
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index 0eabe5d5f690a1566d86a63f1edaa6c318df9734..ef9898edec49d940caf3922d379b809c4e3f100f 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -158,7 +158,7 @@ module OPAQUE_COMP_BYTES_LENGTH = WpContext.Generator(Cil_datatype.Compinfo)
d_lfun = size ; d_types = 0 ; d_params = [] ;
d_definition = Logic result ;
} ;
- let min_size = if Cil.acceptEmptyCompinfo () then e_zero else e_one in
+ let min_size = if Machine.acceptEmptyCompinfo () then e_zero else e_one in
Definitions.define_lemma {
l_kind = Admit ; l_name ;
l_triggers = [] ; l_forall = [] ;
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index 302d9ffa31c89ecdee07d769882e1fa0f37991b6..eba61ce0010a6e6c23e66022e3ac36c98d1a7fbe 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -69,33 +69,32 @@ let make_c_int signed = function
| size -> WpLog.not_yet_implemented "%d-bytes integers" size
let is_char = function
- | UInt8 -> Cil.theMachine.Cil.theMachine.char_is_unsigned
- | SInt8 -> not Cil.theMachine.Cil.theMachine.char_is_unsigned
+ | UInt8 -> Machine.char_is_unsigned ()
+ | SInt8 -> not (Machine.char_is_unsigned ())
| UInt16 | SInt16
| UInt32 | SInt32
| UInt64 | SInt64
| CBool -> false
let c_int ikind =
- let mach = Cil.theMachine.Cil.theMachine in
match ikind with
| IBool -> CBool
- | IChar -> if mach.char_is_unsigned then UInt8 else SInt8
+ | IChar -> if Machine.char_is_unsigned () then UInt8 else SInt8
| ISChar -> SInt8
| IUChar -> UInt8
- | IInt -> make_c_int true mach.sizeof_int
- | IUInt -> make_c_int false mach.sizeof_int
- | IShort -> make_c_int true mach.sizeof_short
- | IUShort -> make_c_int false mach.sizeof_short
- | ILong -> make_c_int true mach.sizeof_long
- | IULong -> make_c_int false mach.sizeof_long
- | ILongLong -> make_c_int true mach.sizeof_longlong
- | IULongLong -> make_c_int false mach.sizeof_longlong
+ | IInt -> make_c_int true (Machine.sizeof_int ())
+ | IUInt -> make_c_int false (Machine.sizeof_int ())
+ | IShort -> make_c_int true (Machine.sizeof_short ())
+ | IUShort -> make_c_int false (Machine.sizeof_short ())
+ | ILong -> make_c_int true (Machine.sizeof_long ())
+ | IULong -> make_c_int false (Machine.sizeof_long ())
+ | ILongLong -> make_c_int true (Machine.sizeof_longlong ())
+ | IULongLong -> make_c_int false (Machine.sizeof_longlong ())
let c_bool () = c_int IBool
let c_char () = c_int IChar
-let p_bytes () = Cil.theMachine.Cil.theMachine.sizeof_ptr
+let p_bytes () = Machine.sizeof_ptr ()
let p_bits () = 8 * p_bytes ()
let c_ptr () = make_c_int false (p_bytes ())
@@ -124,11 +123,10 @@ let make_c_float = function
| size -> WpLog.not_yet_implemented "%d-bits floats" (8*size)
let c_float fkind =
- let mach = Cil.theMachine.Cil.theMachine in
match fkind with
- | FFloat -> make_c_float mach.sizeof_float
- | FDouble -> make_c_float mach.sizeof_double
- | FLongDouble -> make_c_float mach.sizeof_longdouble
+ | FFloat -> make_c_float (Machine.sizeof_float ())
+ | FDouble -> make_c_float (Machine.sizeof_double ())
+ | FLongDouble -> make_c_float (Machine.sizeof_longdouble ())
let equal_float f1 f2 = f_bits f1 = f_bits f2
@@ -251,8 +249,8 @@ let array_size = function
| None -> None
| Some e ->
match constant e with
- | 0L when Cil.gccMode () || Cil.msvcMode () -> None
- | 0L -> Warning.error "0 sized array %s" (Cil.allowed_machdep "GCC/MSVC")
+ | 0L when Machine.(gccMode () || msvcMode ()) -> None
+ | 0L -> Warning.error "0 sized array %s" (Machdep.allowed_machdep "GCC/MSVC")
| n -> Some n
let get_int e =
diff --git a/src/plugins/wp/ctypes.mli b/src/plugins/wp/ctypes.mli
index 91740ec33dfef70dfc4f928a7387343c8ae07d96..f38d4d05826751e7eef0f5ff6ad06028eefb6764 100644
--- a/src/plugins/wp/ctypes.mli
+++ b/src/plugins/wp/ctypes.mli
@@ -92,10 +92,10 @@ val c_ptr : unit -> c_int
(** Returns the type of pointers *)
val c_int : ikind -> c_int
-(** Conforms to {!Cil.theMachine} *)
+(** Conforms to {!Machine.theMachine} *)
val c_float : fkind -> c_float
-(** Conforms to {!Cil.theMachine} *)
+(** Conforms to {!Machine.theMachine} *)
val object_of : typ -> c_object
diff --git a/tests/crowbar/complete_type.ml b/tests/crowbar/complete_type.ml
index 39dc30e45bc0257958644136f7e24c296fe17611..8b7a54b42386b2f92dd19e7655765c4c52c56d0b 100644
--- a/tests/crowbar/complete_type.ml
+++ b/tests/crowbar/complete_type.ml
@@ -42,7 +42,7 @@ let mk_array_type (is_gcc, typ, types, kind) length =
| Complete, Some _ -> Complete
in
let length =
- Option.map (Cil.kinteger ~loc Cil.(theMachine.kindOfSizeOf)) length
+ Option.map (Cil.kinteger ~loc (Machine.sizeof_kind ())) length
in
(is_gcc, TArray (typ, length, []), types, kind)
diff --git a/tests/syntax/machdep_char_unsigned.ml b/tests/syntax/machdep_char_unsigned.ml
deleted file mode 100644
index 034b0ca6fe72d47b36ca1056bd8b8297d424a59e..0000000000000000000000000000000000000000
--- a/tests/syntax/machdep_char_unsigned.ml
+++ /dev/null
@@ -1,73 +0,0 @@
-open Cil_types
-
-let md = {
- version = "";
- compiler = "gcc";
- cpp_arch_flags = ["-m32"];
- sizeof_short = 2;
- sizeof_int = 2;
- sizeof_long = 4;
- sizeof_longlong = 8;
- sizeof_ptr = 4;
- sizeof_float = 4;
- sizeof_double = 8;
- sizeof_longdouble = 8;
- sizeof_void = -1;
- sizeof_fun = 0;
- alignof_short = 2;
- alignof_int = 2;
- alignof_long = 2;
- alignof_longlong = 2;
- alignof_ptr = 2;
- alignof_float = 2;
- alignof_double = 2;
- alignof_longdouble = 2;
- alignof_str = 0;
- alignof_fun = 0;
- alignof_aligned= 0;
- char_is_unsigned = true;
- little_endian = true;
- size_t = "unsigned int";
- ssize_t = "int";
- wchar_t = "int";
- intptr_t = "int";
- uintptr_t = "unsigned int";
- int_fast8_t = "signed char";
- int_fast16_t = "long";
- int_fast32_t = "long";
- int_fast64_t = "long";
- uint_fast8_t = "unsigned char";
- uint_fast16_t = "unsigned long";
- uint_fast32_t = "unsigned long";
- uint_fast64_t = "usigned long";
- ptrdiff_t = "int";
- wint_t = "long";
- sig_atomic_t = "int";
- time_t = "long";
- has__builtin_va_list = true;
- weof = "(-1L)";
- wordsize = "16";
- posix_version = "";
- bufsiz = "8192";
- eof = "(-1)";
- fopen_max = "16";
- host_name_max = "255";
- tty_name_max = "255";
- path_max = "255";
- filename_max = "2048";
- l_tmpnam = "2048";
- tmp_max = "0xFFFFFFFF";
- rand_max = "0xFFFFFFFE";
- mb_cur_max = "16";
- nsig = "64";
- errno = [
- "edom", "33";
- "eilseq", "84";
- "erange", "34";
- ];
- machdep_name = "machdep_char_unsigned";
- custom_defs = "";
-}
-
-let () =
- File.new_machdep "unsigned_char" md