diff --git a/share/machdeps/machdep-schema.yaml b/share/machdeps/machdep-schema.yaml
index 2c3cec943e1dde376f6744d2c9121926df50f601..cbc7163ae36cc55e682dc13672c750a3d0ffe1c2 100644
--- a/share/machdeps/machdep-schema.yaml
+++ b/share/machdeps/machdep-schema.yaml
@@ -60,18 +60,12 @@ alignof_short:
type: integer
-alignof_string:
+alignof_str:
description: alignment of string
type: integer
-alignof_void:
-
- description: (non-standard) alignment of 'void' type. Negative if unsupported
-
- type: integer
-
char_is_unsigned:
description: whether 'char' is unsigned
@@ -102,13 +96,18 @@ has__builtin_va_list:
type: boolean
+intptr_t:
+ description: definition of 'intptr_t'
+
+ type: string
+
little_endian:
description: whether the architecture is little-endian
type: boolean
-ptr_diff_t:
+ptrdiff_t:
description: definition of 'ptrdiff_t'
@@ -180,6 +179,12 @@ sizeof_void:
type: integer
+uintptr_t:
+
+ description: definition of 'uintptr_t'
+
+ type: string
+
version:
description: information on this machdep
@@ -191,3 +196,9 @@ wchar_t:
description: definition of 'wchar_t'
type: string
+
+wint_t:
+
+ description: definition of 'wint_t'
+
+ type: string
diff --git a/share/machdeps/machdep_avr_16.yaml b/share/machdeps/machdep_avr_16.yaml
index fdfbf0d6c9f014fab7e7fabe93931cc6de5d026c..ec24d4f54c5a410a9e982632cb644ed93d4f0519 100644
--- a/share/machdeps/machdep_avr_16.yaml
+++ b/share/machdeps/machdep_avr_16.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
- avr
- -m16
has__builtin_va_list: true
+intptr_t: int
little_endian: true
ptrdiff_t: int
size_t: unsigned int
@@ -29,5 +30,8 @@ sizeof_longlong: 8
sizeof_ptr: 2
sizeof_short: 2
sizeof_void: 1
+uintptr_t: unsigned int
version: clang version 15.0.7
wchar_t: int
+wint_t: int
+
diff --git a/share/machdeps/machdep_gcc_x86_16.yaml b/share/machdeps/machdep_gcc_x86_16.yaml
index 7dc8c9fe44601e43fd43ef584880fd614fcff7d5..7e4f537bb2ca800a9d7b8ae539bb0128b48e2826 100644
--- a/share/machdeps/machdep_gcc_x86_16.yaml
+++ b/share/machdeps/machdep_gcc_x86_16.yaml
@@ -14,6 +14,7 @@ compiler: gcc
cpp_arch_flags:
- -m16
has__builtin_va_list: true
+intptr_t: long
little_endian: true
ptrdiff_t: int
size_t: unsigned int
@@ -27,5 +28,7 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: 1
+uintptr_t: unsigned long
version: none
wchar_t: int
+wint_t: unsigned long
diff --git a/share/machdeps/machdep_gcc_x86_32.yaml b/share/machdeps/machdep_gcc_x86_32.yaml
index e98f9707ad177626f2e6ae0edaaf882cfe7a4ec5..66e15e9ca00e4664aef85b54bb5f2695c260112c 100644
--- a/share/machdeps/machdep_gcc_x86_32.yaml
+++ b/share/machdeps/machdep_gcc_x86_32.yaml
@@ -14,6 +14,7 @@ compiler: gcc
cpp_arch_flags:
- -m32
has__builtin_va_list: true
+intptr_t: int
little_endian: true
ptrdiff_t: int
size_t: unsigned int
@@ -27,5 +28,7 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: 1
+uintptr_t: unsigned int
version: gcc (GCC) 12.2.1 20230201
wchar_t: long
+wint_t: unsigned int
diff --git a/share/machdeps/machdep_gcc_x86_64.yaml b/share/machdeps/machdep_gcc_x86_64.yaml
index cfc63451a76827b077dcbdf30555ace7360c2adb..cd58ca56090b673c1306ec2e7ab044691c935831 100644
--- a/share/machdeps/machdep_gcc_x86_64.yaml
+++ b/share/machdeps/machdep_gcc_x86_64.yaml
@@ -14,6 +14,7 @@ compiler: gcc
cpp_arch_flags:
- -m64
has__builtin_va_list: true
+intptr_t: long
little_endian: true
ptrdiff_t: long
size_t: unsigned long
@@ -27,5 +28,8 @@ sizeof_longlong: 8
sizeof_ptr: 8
sizeof_short: 2
sizeof_void: 1
+uintptr_t: unsigned long
version: gcc (GCC) 12.2.1 20230201
wchar_t: int
+wint_t: unsigned int
+
diff --git a/share/machdeps/machdep_msvc_x86_64.yaml b/share/machdeps/machdep_msvc_x86_64.yaml
index 73c60421095eb21a9eff6043c95d6845dca818e8..b39d6e20ca8fef14d3615786e5727787708f7e1c 100644
--- a/share/machdeps/machdep_msvc_x86_64.yaml
+++ b/share/machdeps/machdep_msvc_x86_64.yaml
@@ -14,6 +14,7 @@ compiler: msvc
cpp_arch_flags:
- -m64
has__builtin_va_list: false
+intptr_t: signed long long
little_endian: true
ptrdiff_t: long long
size_t: unsigned long long
@@ -27,5 +28,7 @@ sizeof_longlong: 8
sizeof_ptr: 8
sizeof_short: 2
sizeof_void: 0
+uintptr_t: unsigned long long
version: MSVC - X86-64bits mode
wchar_t: unsigned short
+wint_t: unsigned short
diff --git a/share/machdeps/machdep_ppc_32.yaml b/share/machdeps/machdep_ppc_32.yaml
index 43a2779dbd18ac600b588b595cb83bc5cb366c2f..304e2140688eef69932395e84fe5435eaadfab36 100644
--- a/share/machdeps/machdep_ppc_32.yaml
+++ b/share/machdeps/machdep_ppc_32.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
- powerpc-apple-linux
- -mcpu=603
has__builtin_va_list: true
+intptr_t: int
little_endian: false
ptrdiff_t: int
size_t: unsigned int
@@ -29,5 +30,8 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: 1
+uintptr_t: unsigned int
version: clang version 15.0.7
wchar_t: int
+wint_t: unsigned int
+
diff --git a/share/machdeps/machdep_x86_16.yaml b/share/machdeps/machdep_x86_16.yaml
index a139bf041da3d84a6c60c7cdf93aa63efdb29c0b..cf3183d345866e1a9145031af588e5c9f1a2d60b 100644
--- a/share/machdeps/machdep_x86_16.yaml
+++ b/share/machdeps/machdep_x86_16.yaml
@@ -14,6 +14,7 @@ compiler: generic
cpp_arch_flags:
- -m16
has__builtin_va_list: true
+intptr_t: long
little_endian: true
ptrdiff_t: int
size_t: unsigned int
@@ -27,5 +28,7 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: -1
+uintptr_t: unsigned long
version: none
wchar_t: int
+wint_t: unsigned long
diff --git a/share/machdeps/machdep_x86_32.yaml b/share/machdeps/machdep_x86_32.yaml
index df6493927a4e87573387d8d2ee23bf8bc3770847..344ef9ad0361afda50fc977b862309d2e7f6bd2f 100644
--- a/share/machdeps/machdep_x86_32.yaml
+++ b/share/machdeps/machdep_x86_32.yaml
@@ -14,6 +14,7 @@ compiler: generic
cpp_arch_flags:
- -m32
has__builtin_va_list: true
+intptr_t: int
little_endian: true
ptrdiff_t: int
size_t: unsigned int
@@ -27,5 +28,7 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: -1
+uintptr_t: unsigned
version: gcc (GCC) 12.2.1 20230201
wchar_t: long
+wint_t: unsigned int
diff --git a/share/machdeps/machdep_x86_64.yaml b/share/machdeps/machdep_x86_64.yaml
index 6ab3b343b0fcbf88fd80f5936b33621aadb2631f..ff21378b9038c300341c84cb692c12c9035ec1a1 100644
--- a/share/machdeps/machdep_x86_64.yaml
+++ b/share/machdeps/machdep_x86_64.yaml
@@ -14,6 +14,7 @@ compiler: generic
cpp_arch_flags:
- -m64
has__builtin_va_list: true
+intptr_t: long
little_endian: true
ptrdiff_t: long
size_t: unsigned long
@@ -27,5 +28,7 @@ sizeof_longlong: 8
sizeof_ptr: 8
sizeof_short: 2
sizeof_void: -1
+uintptr_t: unsigned long
version: clang version 15.0.7
wchar_t: int
+wint_t: unsigned int
diff --git a/share/machdeps/make_machdep/intptr_t.c b/share/machdeps/make_machdep/intptr_t.c
new file mode 100644
index 0000000000000000000000000000000000000000..ec1f36e633d82dd9609870cfc937498a15cf661c
--- /dev/null
+++ b/share/machdeps/make_machdep/intptr_t.c
@@ -0,0 +1,29 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2023 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+#include "make_machdep_common.h"
+#include <stdint.h>
+#define TEST_TYPE intptr_t
+
+TEST_TYPE_IS(int);
+TEST_TYPE_IS(long);
+TEST_TYPE_IS(long long);
diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py
index fe84a770ce45ec0d75b63cd2c7cc666178ab811d..0a61c5e6693446251d6f5253cc249245807e20a9 100755
--- a/share/machdeps/make_machdep/make_machdep.py
+++ b/share/machdeps/make_machdep/make_machdep.py
@@ -111,15 +111,17 @@ def print_machdep(machdep):
# Python does not end the dump with a newline by itself
args.dest_file.write("\n")
+def make_schema():
+ schema_filename = my_path.parent / "machdep-schema.yaml"
+ with open(schema_filename, "r") as schema:
+ return yaml.safe_load(schema)
+
+schema = make_schema()
def check_machdep(machdep):
try:
from jsonschema import validate, ValidationError
-
- schema_filename = my_path.parent / "machdep-schema.json"
-
- with open(schema_filename, "r") as schema:
- validate(machdep, json.load(schema))
+ validate(machdep,schema)
except ImportError:
warnings.warn("jsonschema is not available: no validation will be performed")
except OSError:
@@ -127,40 +129,13 @@ def check_machdep(machdep):
except ValidationError:
warnings.warn("machdep object is not conforming to machdep schema")
+def make_machdep():
+ machdep = { }
+ for key in schema.keys():
+ machdep[key] = None
+ return machdep
-# This must remain synchronized with cil_types.ml's 'mach' type
-machdep = {
- "sizeof_short": None,
- "sizeof_int": None,
- "sizeof_long": None,
- "sizeof_longlong": None,
- "sizeof_ptr": None,
- "sizeof_float": None,
- "sizeof_double": None,
- "sizeof_longdouble": None,
- "sizeof_void": None,
- "sizeof_fun": None,
- "size_t": None,
- "wchar_t": None,
- "ptrdiff_t": None,
- "alignof_short": None,
- "alignof_int": None,
- "alignof_long": None,
- "alignof_longlong": None,
- "alignof_ptr": None,
- "alignof_float": None,
- "alignof_double": None,
- "alignof_longdouble": None,
- "alignof_str": None,
- "alignof_fun": None,
- "char_is_unsigned": None,
- "little_endian": None,
- "alignof_aligned": None,
- "has__builtin_va_list": None,
- "compiler": None,
- "cpp_arch_flags": None,
- "version": None,
-}
+machdep = make_machdep()
compilation_command = [args.compiler] + args.cpp_arch_flags + args.compiler_flags
@@ -189,6 +164,9 @@ source_files = [
("size_t.c", "type"),
("wchar_t.c", "type"),
("ptrdiff_t.c", "type"),
+ ("intptr_t.c", "type"),
+ ("uintptr_t.c", "type"),
+ ("wint_t.c", "type"),
("char_is_unsigned.c", "bool"),
("little_endian.c", "bool"),
("has__builtin_va_list.c", "has__builtin_va_list"),
diff --git a/share/machdeps/make_machdep/uintptr_t.c b/share/machdeps/make_machdep/uintptr_t.c
new file mode 100644
index 0000000000000000000000000000000000000000..655dd30616e2fd871f4f156702d71a4ba7eba77c
--- /dev/null
+++ b/share/machdeps/make_machdep/uintptr_t.c
@@ -0,0 +1,29 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2023 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+#include "make_machdep_common.h"
+#include <stdint.h>
+#define TEST_TYPE uintptr_t
+
+TEST_TYPE_IS(unsigned int);
+TEST_TYPE_IS(unsigned long);
+TEST_TYPE_IS(unsigned long long);
diff --git a/share/machdeps/make_machdep/wint_t.c b/share/machdeps/make_machdep/wint_t.c
new file mode 100644
index 0000000000000000000000000000000000000000..233eb0986e2f816530c63c238a9c861c966a59c3
--- /dev/null
+++ b/share/machdeps/make_machdep/wint_t.c
@@ -0,0 +1,32 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2023 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+#include "make_machdep_common.h"
+#include <wchar.h>
+#define TEST_TYPE wint_t
+
+TEST_TYPE_IS(unsigned int);
+TEST_TYPE_IS(int);
+TEST_TYPE_IS(unsigned long);
+TEST_TYPE_IS(long);
+TEST_TYPE_IS(unsigned long long);
+TEST_TYPE_IS(long long);