From b65c15b9cf4bd108dca8b130eb75c96bb019b717 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri, 26 Jul 2024 10:42:37 +0200
Subject: [PATCH] [Cil] Replace theMachine by the new Machine module
---
src/kernel_internals/parsing/clexer.mll | 2 +-
src/kernel_internals/parsing/cparser.mly | 4 +-
src/kernel_internals/runtime/special_hooks.ml | 2 +-
src/kernel_internals/typing/cabs2cil.ml | 128 +++----
src/kernel_internals/typing/rmtmps.ml | 4 +-
src/kernel_services/abstract_interp/base.ml | 2 +-
src/kernel_services/abstract_interp/cvalue.ml | 4 +-
.../abstract_interp/offsetmap.ml | 4 +-
src/kernel_services/analysis/bit_utils.ml | 2 +-
src/kernel_services/analysis/destructors.ml | 2 +-
src/kernel_services/ast_data/alarms.ml | 2 +-
src/kernel_services/ast_data/ast.ml | 4 +-
src/kernel_services/ast_data/cil_types.ml | 14 +-
.../ast_printing/cil_printer.ml | 36 +-
src/kernel_services/ast_queries/cil.ml | 319 ++++--------------
src/kernel_services/ast_queries/cil.mli | 84 +----
.../ast_queries/cil_builtins.ml | 17 +-
.../ast_queries/cil_builtins.mli | 4 +-
src/kernel_services/ast_queries/file.ml | 8 +-
.../ast_queries/logic_typing.ml | 4 +-
.../ast_queries/logic_utils.ml | 2 +-
src/plugins/aorai/data_for_aorai.ml | 2 +-
src/plugins/e-acsl/src/analyses/interval.ml | 4 +-
src/plugins/e-acsl/src/code_generator/gmp.ml | 2 +-
src/plugins/e-acsl/src/code_generator/libc.ml | 10 +-
.../e-acsl/src/code_generator/logic_array.ml | 6 +-
.../src/code_generator/translate_ats.ml | 2 +-
.../src/code_generator/translate_terms.ml | 4 +-
.../src/code_generator/translate_utils.ml | 2 +-
src/plugins/eva/ast/eva_ast_builder.ml | 6 +-
src/plugins/eva/ast/eva_ast_typing.ml | 4 +-
src/plugins/eva/ast/eva_ast_utils.ml | 2 +-
src/plugins/eva/domains/cvalue/builtins.ml | 2 +-
.../eva/domains/cvalue/builtins_malloc.ml | 8 +-
.../eva/domains/cvalue/builtins_string.ml | 6 +-
src/plugins/eva/domains/cvalue/cvalue_init.ml | 2 +-
src/plugins/eva/engine/evaluation.ml | 2 +-
src/plugins/eva/utils/eval_typ.ml | 2 +-
src/plugins/eva/values/cvalue_backward.ml | 2 +-
src/plugins/eva/values/offsm_value.ml | 7 +-
src/plugins/variadic/standard.ml | 2 +-
src/plugins/wp/Cvalues.ml | 2 +-
src/plugins/wp/ctypes.ml | 36 +-
src/plugins/wp/ctypes.mli | 4 +-
tests/crowbar/complete_type.ml | 2 +-
45 files changed, 272 insertions(+), 497 deletions(-)
diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 89dbe33f7d5..6acfc8312b2 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 414df24d404..f6d7ffc1b67 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/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index d888e026716..73a2a2275c3 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 6c2cd09b4ae..1753414b85b 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 01c1b346c1d..7dcb102cb80 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 87b585b9c48..da6d647b22a 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 bd0e040f33f..0f70fa34a69 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 43fe9f3436b..cce3aad8668 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 affb4f40dcf..c086012ea79 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 81f9c24b559..1eecb32fc65 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 5ad2bc11249..3977959164a 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 05a5e0158e7..c76daf23efd 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 cbabb5c1f2e..aaa0fa132b0 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -813,13 +813,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
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 1bd22b76984..c89f7804429 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_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 6593cc9abd4..9d9cfeac0df 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
@@ -3948,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, _) ->
@@ -3984,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
@@ -4103,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;
@@ -4268,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
@@ -4357,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))
@@ -4489,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
@@ -4510,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
@@ -4768,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
@@ -5806,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
@@ -6304,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
@@ -6604,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
@@ -6624,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
@@ -6757,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
@@ -6838,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, _) ->
@@ -7049,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:
@@ -7617,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 0dd5e5931da..8de18151bda 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 1a6dc1cdbda..d12e5ddc27e 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 ca5ff1cbd91..78f9f25aec0 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/file.ml b/src/kernel_services/ast_queries/file.ml
index 49c185aa32a..9159303d7ab 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -313,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 =
@@ -1198,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 ();
@@ -1621,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/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index bb10728f604..7fbbc120b54 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 7867e987c3d..690e9c8def3 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 faccb2fa50e..542efe1f658 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 ed2bd6ff624..ad5a3600c9e 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 324c524514b..51d50aaa518 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 766c93a81c3..36b3973bd43 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 2b8566382d0..97ca7bdcb6d 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 670f7316b9e..f7bfcc06715 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 e0693bd7f5e..a2dcfd36b7b 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 0a97fa252a8..cea3235a866 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 b0e7b16dd05..1faa1e6f1dc 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 5ea656ded20..7b68db5d9c0 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 49e282a4613..205521b9bb4 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 8cfee381861..caea7c82475 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 b3be407a16d..6a76e17173e 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 6700057446d..3de4a2bc5f7 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 8d4cc1bdc56..2d812edf25c 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 b2c7612309d..2226ae760c9 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 9b2cc6ad98f..69649a738b3 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 b4ba8bff308..9ef10661e36 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 fd657c92ee4..9118e16727e 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 964ef79b02b..043273fdc5c 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 0eabe5d5f69..ef9898edec4 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 302d9ffa31c..eba61ce0010 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 91740ec33df..f38d4d05826 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 39dc30e45bc..8b7a54b4238 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)
--
GitLab