diff --git a/src/kernel_internals/runtime/machdeps.ml b/src/kernel_internals/runtime/machdeps.ml
deleted file mode 100644
index 440a51e9374326fa164a447993e8ec215d6d8514..0000000000000000000000000000000000000000
--- a/src/kernel_internals/runtime/machdeps.ml
+++ /dev/null
@@ -1,229 +0,0 @@
-(****************************************************************************)
-(* *)
-(* Copyright (C) 2001-2003 *)
-(* George C. Necula <necula@cs.berkeley.edu> *)
-(* Scott McPeak <smcpeak@cs.berkeley.edu> *)
-(* Wes Weimer <weimer@cs.berkeley.edu> *)
-(* Ben Liblit <liblit@cs.berkeley.edu> *)
-(* All rights reserved. *)
-(* *)
-(* Redistribution and use in source and binary forms, with or without *)
-(* modification, are permitted provided that the following conditions *)
-(* are met: *)
-(* *)
-(* 1. Redistributions of source code must retain the above copyright *)
-(* notice, this list of conditions and the following disclaimer. *)
-(* *)
-(* 2. Redistributions in binary form must reproduce the above copyright *)
-(* notice, this list of conditions and the following disclaimer in the *)
-(* documentation and/or other materials provided with the distribution. *)
-(* *)
-(* 3. The names of the contributors may not be used to endorse or *)
-(* promote products derived from this software without specific prior *)
-(* written permission. *)
-(* *)
-(* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS *)
-(* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT *)
-(* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS *)
-(* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE *)
-(* COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, *)
-(* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, *)
-(* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; *)
-(* LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER *)
-(* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT *)
-(* LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN *)
-(* ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE *)
-(* POSSIBILITY OF SUCH DAMAGE. *)
-(* *)
-(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
-(* énergies alternatives) *)
-(* and INRIA (Institut National de Recherche en Informatique *)
-(* et Automatique). *)
-(****************************************************************************)
-
-open Cil_types
-
-let x86_16 = {
- version =
- "x86 16 bits mode (gcc like compiler) with big or huge memory model";
- compiler = "generic";
- cpp_arch_flags = ["-m16"];
- sizeof_short = 2;
- sizeof_int = 2;
- sizeof_long = 4;
- sizeof_longlong = 8;
- sizeof_ptr = 4;
- sizeof_float = 4;
- sizeof_double = 8;
- sizeof_longdouble = 16;
- sizeof_void = -1;
- sizeof_fun = -1;
- size_t = "unsigned int";
- wchar_t = "int";
- ptrdiff_t = "int";
- alignof_short = 2;
- alignof_int = 2;
- alignof_long = 4;
- alignof_longlong = 4;
- alignof_ptr = 4;
- alignof_float = 2;
- alignof_double = 8;
- alignof_longdouble = 16;
- alignof_str = 1;
- alignof_fun = -1;
- alignof_aligned= 8;
- (* I don't know if attribute aligned is supported by any 16bits
- compiler. *)
- char_is_unsigned = false;
- little_endian = true;
- has__builtin_va_list = true;
-}
-
-let gcc_x86_16 = { x86_16 with
- compiler = "gcc";
- sizeof_void = 1; sizeof_fun = 1; alignof_fun = 1;
- }
-
-let x86_32 = {
- version = "gcc 4.0.3 - X86-32bits mode";
- compiler = "generic";
- cpp_arch_flags = ["-m32"];
- sizeof_short = 2;
- sizeof_int = 4;
- sizeof_long = 4;
- sizeof_longlong = 8;
- sizeof_ptr = 4;
- sizeof_float = 4;
- sizeof_double = 8;
- sizeof_longdouble = 12;
- sizeof_void = -1;
- sizeof_fun = -1;
- size_t = "unsigned int";
- wchar_t = "int";
- ptrdiff_t = "int";
- alignof_short = 2;
- alignof_int = 4;
- alignof_long = 4;
- alignof_longlong = 4;
- alignof_ptr = 4;
- alignof_float = 4;
- alignof_double = 4;
- alignof_longdouble = 4;
- alignof_str = 1;
- alignof_fun = -1;
- alignof_aligned= 16;
- char_is_unsigned = false;
- little_endian = true;
- has__builtin_va_list = true;
-}
-
-let gcc_x86_32 = { x86_32 with
- compiler = "gcc";
- sizeof_void = 1; sizeof_fun = 1; alignof_fun = 1;
- }
-
-let x86_64 = {
- version = "gcc 4.0.3 AMD64";
- compiler = "generic";
- cpp_arch_flags = ["-m64"];
- sizeof_short = 2;
- sizeof_int = 4;
- sizeof_long = 8;
- sizeof_longlong = 8;
- sizeof_ptr = 8;
- sizeof_float = 4;
- sizeof_double = 8;
- sizeof_longdouble = 16;
- sizeof_void = -1;
- sizeof_fun = -1;
- size_t = "unsigned long";
- wchar_t = "int";
- ptrdiff_t = "long";
- alignof_short = 2;
- alignof_int = 4;
- alignof_long = 8;
- alignof_longlong = 8;
- alignof_ptr = 8;
- alignof_float = 4;
- alignof_double = 8;
- alignof_longdouble = 16;
- alignof_str = 1;
- alignof_fun = -1;
- alignof_aligned= 16;
- char_is_unsigned = false;
- little_endian = true;
- has__builtin_va_list = true;
-}
-
-let gcc_x86_64 = { x86_64 with
- compiler = "gcc";
- sizeof_void = 1; sizeof_fun = 1; alignof_fun = 1;
- }
-
-let ppc_32 = {
- version = "4.0.1 (Apple Computer, Inc. build 5367)";
- compiler = "standard";
- cpp_arch_flags = ["-m32"];
- sizeof_short = 2;
- sizeof_int = 4;
- sizeof_long = 4;
- sizeof_longlong = 8;
- sizeof_ptr = 4;
- sizeof_float = 4;
- sizeof_double = 8;
- sizeof_longdouble = 16;
- sizeof_void = 1;
- sizeof_fun = 1;
- size_t = "unsigned int";
- wchar_t = "int";
- ptrdiff_t = "int";
- alignof_short = 2;
- alignof_int = 4;
- alignof_long = 4;
- alignof_longlong = 4;
- alignof_ptr = 4;
- alignof_float = 4;
- alignof_double = 4;
- alignof_longdouble = 16;
- alignof_str = 1;
- alignof_fun = 4;
- alignof_aligned= 16;
- char_is_unsigned = false;
- little_endian = false;
- has__builtin_va_list = true;
-}
-
-let msvc_x86_64 = {
- version = "MSVC - X86-64bits mode";
- compiler = "msvc";
- cpp_arch_flags = ["-m64"];
- sizeof_short = 2;
- sizeof_int = 4;
- sizeof_long = 4;
- sizeof_longlong = 8;
- sizeof_ptr = 8;
- sizeof_float = 4;
- sizeof_double = 8;
- sizeof_longdouble = 8;
- sizeof_void = 0;
- sizeof_fun = -1;
- size_t = "unsigned long long"; (* defined as 'unsigned __int64' *)
- wchar_t = "unsigned short";
- ptrdiff_t = "long long"; (* defined as '__int64' *)
- alignof_short = 2;
- alignof_int = 4;
- alignof_long = 4;
- alignof_longlong = 8;
- alignof_ptr = 8;
- alignof_float = 4;
- alignof_double = 8;
- alignof_longdouble = 8;
- alignof_str = 1; (* __alignof("a") results in compilation error C2059:
- syntax error: 'string' *)
- alignof_fun = -1;
- alignof_aligned= 1; (* MSVC does not seem to have an 'align' attribute
- equivalent to GCC's *)
- char_is_unsigned = false;
- little_endian = true;
- has__builtin_va_list = false;
-}
diff --git a/src/kernel_internals/runtime/machdeps.mli b/src/kernel_internals/runtime/machdeps.mli
deleted file mode 100644
index 3959c84cf536c23ebd24c750f3695ef68911cefc..0000000000000000000000000000000000000000
--- a/src/kernel_internals/runtime/machdeps.mli
+++ /dev/null
@@ -1,54 +0,0 @@
-(****************************************************************************)
-(* *)
-(* Copyright (C) 2001-2003 *)
-(* George C. Necula <necula@cs.berkeley.edu> *)
-(* Scott McPeak <smcpeak@cs.berkeley.edu> *)
-(* Wes Weimer <weimer@cs.berkeley.edu> *)
-(* Ben Liblit <liblit@cs.berkeley.edu> *)
-(* All rights reserved. *)
-(* *)
-(* Redistribution and use in source and binary forms, with or without *)
-(* modification, are permitted provided that the following conditions *)
-(* are met: *)
-(* *)
-(* 1. Redistributions of source code must retain the above copyright *)
-(* notice, this list of conditions and the following disclaimer. *)
-(* *)
-(* 2. Redistributions in binary form must reproduce the above copyright *)
-(* notice, this list of conditions and the following disclaimer in the *)
-(* documentation and/or other materials provided with the distribution. *)
-(* *)
-(* 3. The names of the contributors may not be used to endorse or *)
-(* promote products derived from this software without specific prior *)
-(* written permission. *)
-(* *)
-(* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS *)
-(* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT *)
-(* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS *)
-(* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE *)
-(* COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, *)
-(* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, *)
-(* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; *)
-(* LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER *)
-(* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT *)
-(* LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN *)
-(* ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE *)
-(* POSSIBILITY OF SUCH DAMAGE. *)
-(* *)
-(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
-(* énergies alternatives) *)
-(* and INRIA (Institut National de Recherche en Informatique *)
-(* et Automatique). *)
-(****************************************************************************)
-
-(** Some predefined {!Cil_types.mach} which specifies machine-dependent
- data about C programs. *)
-
-val x86_16: Cil_types.mach
-val gcc_x86_16: Cil_types.mach
-val x86_32: Cil_types.mach
-val gcc_x86_32: Cil_types.mach
-val x86_64: Cil_types.mach
-val gcc_x86_64: Cil_types.mach
-val ppc_32: Cil_types.mach
-val msvc_x86_64: Cil_types.mach
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 042383450a81c604625ad0bb5d332a63a10560cc..b80ed81244c0260b9fa53272450e615d913aa310 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1878,6 +1878,9 @@ type mach = {
size_t: string; (* Type of "sizeof(T)" *)
wchar_t: string; (* Type of "wchar_t" *)
ptrdiff_t: string; (* Type of "ptrdiff_t" *)
+ intptr_t: string; (* Type of "intptr_t" *)
+ uintptr_t: string; (* Type of "uintptr_t" *)
+ wint_t: string; (* Type of "wint_t" *)
alignof_short: int; (* Alignment of "short" *)
alignof_int: int; (* Alignment of "int" *)
alignof_long: int; (* Alignment of "long" *)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index a65d727bb6b2641f19dbd5dbe81ac9768e2e3a1d..29afbd7f9f52f9a85259a963fa315da6447650e9 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -119,7 +119,7 @@ type theMachine =
let createMachine () = (* Contain dummy values *)
{ useLogicalOperators = false;
- theMachine = Machdeps.x86_64;
+ theMachine = List.hd Cil_datatype.Machdep.reprs;
lowerConstants = false(*true*);
insertImplicitCasts = true;
stringLiteralType = charConstPtrType;
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index d08d58bc8b1aeaf61d6b1364621e54c2a1122f45..72e9e135a1ea228efd12012eacfd6716c33e5681 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2627,6 +2627,55 @@ module Syntactic_scope =
Location.pretty (Stmt.loc s) Stmt.pretty s
end)
+let dummy_machdep =
+ {
+ sizeof_short = 2;
+ sizeof_int = 4;
+ sizeof_long = 8;
+ sizeof_longlong = 8;
+ sizeof_ptr = 8;
+ sizeof_float = 4;
+ sizeof_double = 8;
+ sizeof_longdouble = 16;
+ sizeof_void = -1;
+ sizeof_fun = -1;
+ size_t = "unsigned long";
+ wchar_t = "int";
+ ptrdiff_t = "long";
+ intptr_t = "long"; (* Type of "intptr_t" *)
+ uintptr_t = "unsigned long"; (* Type of "uintptr_t" *)
+ wint_t = "int";
+ alignof_short = 2;
+ alignof_int = 4;
+ alignof_long = 8;
+ alignof_longlong = 8;
+ alignof_ptr = 8;
+ alignof_float = 4;
+ alignof_double = 8;
+ alignof_longdouble = 16;
+ alignof_str = 1;
+ alignof_fun = -1;
+ char_is_unsigned = true;
+ little_endian = true;
+ alignof_aligned = 16;
+ has__builtin_va_list = true;
+ compiler = "none";
+ cpp_arch_flags = [];
+ version = "N/A";
+ }
+
+module Machdep = Datatype.Make_with_collections(struct
+ include Datatype.Serializable_undefined
+ let reprs = [dummy_machdep]
+ let name = "Machdep"
+ type t = Cil_types.mach
+ let compare : t -> t -> int = Stdlib.compare
+ let equal : t -> t -> bool = (=)
+ let hash : t -> int = Hashtbl.hash
+ let copy = Datatype.identity
+ end)
+
+
(* -------------------------------------------------------------------------- *)
(* --- Internal --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index de601cca4d4a3031b9b1b6ead68d4150b26d6d4c..15029092fff8b4779fce6de3f90008947595d2c5 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -367,6 +367,13 @@ module PredicateStructEq: S_with_collections_pretty with type t = predicate
module Lexpr: S with type t = Logic_ptree.lexpr
(** Beware: no pretty-printer is available. *)
+(**************************************************************************)
+(** {3 Machdep} *)
+(**************************************************************************)
+
+module Machdep: S_with_collections with type t = mach
+(** since Frama-C+dev *)
+
(**/**)
(* ****************************************************************************)
(** {2 Internal API} *)
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 6ee4c8d90eb2d6adee171537fad6869f849da191..597efe8b6cc0221c579b804aeb365a186215cf83 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -271,17 +271,6 @@ let print_machdep fmt (m : Cil_types.mach) =
(if m.has__builtin_va_list then "has" else "has not") ;
end
-module DatatypeMachdep = Datatype.Make_with_collections(struct
- include Datatype.Serializable_undefined
- let reprs = [Machdeps.x86_32]
- let name = "File.Machdep"
- type t = Cil_types.mach
- let compare : t -> t -> int = Stdlib.compare
- let equal : t -> t -> bool = (=)
- let hash : t -> int = Hashtbl.hash
- let copy = Datatype.identity
- end)
-
let regexp_existing_machdep_macro = Str.regexp "-D[ ]*__FC_MACHDEP_"
let existing_machdep_macro () =
@@ -307,7 +296,7 @@ let machdep_macro = function
res
module CustomMachdeps =
- State_builder.Hashtbl(Datatype.String.Hashtbl)(DatatypeMachdep)
+ State_builder.Hashtbl(Datatype.String.Hashtbl)(Cil_datatype.Machdep)
(struct
let name = " File.CustomMachdeps"
let size = 5
diff --git a/tests/misc/custom_machdep.c b/tests/misc/custom_machdep.c
index b28d8660679fc128f7cc31daed65c2b62e2e5cb2..1e4388831b27dbee4287855c97700278b425b7f2 100644
--- a/tests/misc/custom_machdep.c
+++ b/tests/misc/custom_machdep.c
@@ -6,7 +6,7 @@
COMMENT: we need a -then to test double registering of a machdep
EXIT: 0
DEPS: @PTEST_NAME@/__fc_machdep_custom.h
- OPT: -cpp-extra-args="-I./@PTEST_NAME@ -D__FC_MACHDEP_CUSTOM" -machdep %{dep:@PTEST_DIR@/@PTEST_NAME@.json} -print
+ OPT: -cpp-extra-args="-I./@PTEST_NAME@ -D__FC_MACHDEP_CUSTOM" -machdep %{dep:@PTEST_DIR@/@PTEST_NAME@.yaml} -print
*/
#include "__fc_machdep_custom.h"
// most of the following includes are not directly used, but they test if
diff --git a/tests/misc/custom_machdep.json b/tests/misc/custom_machdep.json
deleted file mode 100644
index 0761e8060aefaa3ede539ff108e0ba32be392367..0000000000000000000000000000000000000000
--- a/tests/misc/custom_machdep.json
+++ /dev/null
@@ -1,32 +0,0 @@
- {
- "version": "foo",
- "compiler": "bar",
- "cpp_arch_flags" : [],
- "sizeof_short" : 2,
- "sizeof_int": 3,
- "sizeof_long": 4,
- "sizeof_longlong" : 8,
- "sizeof_ptr" : 4,
- "sizeof_float": 4,
- "sizeof_double": 8,
- "sizeof_longdouble": 12,
- "sizeof_void": 1,
- "sizeof_fun" : 1,
- "size_t" : "unsigned long",
- "wchar_t" : "int",
- "ptrdiff_t": "int",
- "alignof_short" : 2,
- "alignof_int": 3,
- "alignof_long": 4,
- "alignof_longlong": 4,
- "alignof_ptr" : 4,
- "alignof_float": 4,
- "alignof_double": 4,
- "alignof_longdouble": 4,
- "alignof_str": 1,
- "alignof_fun": 1,
- "alignof_aligned": 16,
- "char_is_unsigned": false,
- "little_endian": true,
- "has__builtin_va_list": true
- }
diff --git a/tests/misc/custom_machdep.ml b/tests/misc/custom_machdep.ml
index e7a740d59b40bc6b4f2b3a28c1a41998195bb0bb..7d929b77693aef27ea2ffebd598f4791214c0101 100644
--- a/tests/misc/custom_machdep.ml
+++ b/tests/misc/custom_machdep.ml
@@ -16,6 +16,9 @@ let mach =
sizeof_void = 1;
sizeof_fun = 1;
size_t = "unsigned long";
+ intptr_t = "long";
+ uintptr_t = "unsigned long";
+ wint_t = "int";
wchar_t = "int";
ptrdiff_t = "int";
alignof_short = 2;
diff --git a/tests/misc/custom_machdep.yaml b/tests/misc/custom_machdep.yaml
new file mode 100644
index 0000000000000000000000000000000000000000..67b759afe501b21ecba938fa818ae5dd41ad055e
--- /dev/null
+++ b/tests/misc/custom_machdep.yaml
@@ -0,0 +1,33 @@
+alignof_aligned: 16
+alignof_double: 4
+alignof_float: 4
+alignof_fun: 1
+alignof_int: 3
+alignof_long: 4
+alignof_longdouble: 4
+alignof_longlong: 4
+alignof_ptr: 4
+alignof_short: 2
+alignof_str: 1
+char_is_unsigned: false
+compiler: bar
+cpp_arch_flags: []
+has__builtin_va_list: true
+little_endian: true
+ptrdiff_t: int
+intptr_t: long
+uintptr_t: unsigned long
+wint_t: int
+size_t: unsigned long
+sizeof_double: 8
+sizeof_float: 4
+sizeof_fun: 1
+sizeof_int: 3
+sizeof_long: 4
+sizeof_longdouble: 12
+sizeof_longlong: 8
+sizeof_ptr: 4
+sizeof_short: 2
+sizeof_void: 1
+version: foo
+wchar_t: int
diff --git a/tests/syntax/machdep_char_unsigned.ml b/tests/syntax/machdep_char_unsigned.ml
index 1bdbdbc1d6a22a071cdaa9b7fb74f1d94caf287d..9ccf6d9691e3be291e0102820b8aaa71d5d0b133 100644
--- a/tests/syntax/machdep_char_unsigned.ml
+++ b/tests/syntax/machdep_char_unsigned.ml
@@ -30,7 +30,10 @@ let md = {
little_endian = true;
size_t = "unsigned int";
wchar_t = "int";
+ intptr_t = "int";
+ uintptr_t = "unsigned int";
ptrdiff_t = "int";
+ wint_t = "long";
has__builtin_va_list = true;
}