From 7bfb6b675566d302d28e291bab1ef98dd6e858fa Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri, 26 Jul 2024 11:06:59 +0200
Subject: [PATCH] Replace Cil.theMachine with the new Machine module
---
convert.ml | 5 ++---
convert_env.ml | 2 +-
cxx_utils.ml | 2 +-
frama_Clang_register.ml | 4 ++--
4 files changed, 6 insertions(+), 7 deletions(-)
diff --git a/convert.ml b/convert.ml
index bb27c1ca..6b289581 100644
--- a/convert.ml
+++ b/convert.ml
@@ -22,7 +22,6 @@
open Intermediate_format
open Cabs
-open Cil
let lambda_unique_name typ infix id =
(Mangling.mangle_cc_type typ) ^ infix ^ Int64.to_string id
@@ -138,7 +137,7 @@ let is_unsigned_kind = function
| IBool -> true (* standard says that bool is neither signed nor unsigned,
but at some point you have to take sides. *)
| IChar_s | ISChar | IWChar_s -> false
- | IChar | IWChar -> Cil.theMachine.theMachine.char_is_unsigned
+ | IChar | IWChar -> Machine.char_is_unsigned ()
| IShort | IInt -> false
| IChar_u | IUChar | IChar16 | IChar32 | IWChar_u
| IUShort | IUInt -> true
@@ -4051,7 +4050,7 @@ let convert_ast file =
pos_lnum = 0; pos_bol = 0; pos_cnum = 0; }
in
let basic_loc = basic_pos, basic_pos in
- let sizeof_t = Cxx_utils.spec_of_ikind Cil.theMachine.kindOfSizeOf in
+ let sizeof_t = Cxx_utils.spec_of_ikind (Machine.sizeof_kind ()) in
let res =
(Datatype.Filepath.of_string file.filename,
(false,
diff --git a/convert_env.ml b/convert_env.ml
index f215e185..c6a9d6bb 100644
--- a/convert_env.ml
+++ b/convert_env.ml
@@ -262,7 +262,7 @@ let memo_wchar env =
let wchar_name = { prequalification=[];decl_name="wchar_t"} in
if has_typedef env wchar_name then env
else begin
- let kind = Cil.theMachine.wcharKind in
+ let kind = Machine.wchar_kind () in
let repr = Cxx_utils.(unqual_type (int_type kind)) in
let env = add_typedef env wchar_name repr in
let ghost = is_ghost env in
diff --git a/cxx_utils.ml b/cxx_utils.ml
index c4ed3ab1..dfbb2b19 100644
--- a/cxx_utils.ml
+++ b/cxx_utils.ml
@@ -396,7 +396,7 @@ let meth_name class_name tkind decl_name =
let int_kind = function
| Cil_types.IBool -> IBool
| IChar ->
- if Cil.theMachine.theMachine.char_is_unsigned then IChar_u else IChar_s
+ if Machine.char_is_unsigned () then IChar_u else IChar_s
| IUChar -> IUChar
| ISChar -> ISChar
| IInt -> IInt
diff --git a/frama_Clang_register.ml b/frama_Clang_register.ml
index 85d2114e..30d84a1a 100644
--- a/frama_Clang_register.ml
+++ b/frama_Clang_register.ml
@@ -56,7 +56,7 @@ let std_regex = Str.regexp "-std="
let run_clang debug input output =
let use_own_headers = Frama_Clang_option.Std_include.get() in
let machine = Kernel.Machdep.get () in
- let mach_descr = Cil.theMachine.theMachine in
+ let mach_descr = Machine.get_machdep () in
let clang_command = Frama_Clang_option.Clang_command.get () in
let extra_args =
if Frama_Clang_option.Clang_extra_args.is_set () then
@@ -156,7 +156,7 @@ let init_cxx_normalization () =
(* Current implementation of VMT is not compatible with this warning. *)
Kernel.set_warn_status Kernel.wkey_incompatible_types_call Log.Winactive ;
(* C++ allows this *)
- Cil.set_acceptEmptyCompinfo ()
+ Machine.set_acceptEmptyCompinfo ()
end
let parse_cxx file =
--
GitLab