diff --git a/share/machdeps/Makefile b/share/machdeps/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..348bb70e14067eb739f8c0ff6142c98fcd1e76c8
--- /dev/null
+++ b/share/machdeps/Makefile
@@ -0,0 +1,20 @@
+update-all: machdep_*.yaml
+
+machdep_avr_16.yaml \
+machdep_gcc_x86_32.yaml \
+machdep_gcc_x86_64.yaml \
+machdep_ppc_32.yaml : \
+%.yaml: machdep-schema.yaml make_machdep/make_machdep.py
+ @./make_machdep/make_machdep.py -i --from-file $@ --check
+
+machdep_x86_16.yaml machdep_x86_32.yaml machdep_x86_64.yaml: \
+machdep_%.yaml: machdep_gcc_%.yaml Makefile
+ @sed -e 's/sizeof_fun: .*/sizeof_fun: -1/' \
+ -e 's/sizeof_void: .*/sizeof_void: -1/' \
+ -e 's/alignof_fun: .*/alignof_fun: -1/' \
+ -e 's/compiler: .*/compiler: generic/' \
+ $< > $@
+
+machdep_gcc_x86_16.yaml machdep_msvc_x86_64.yaml: %.yaml: machdep-schema.yaml
+ @echo "$@ is newer than $< and must be updated manually"
+ @exit 1
diff --git a/share/machdeps/machdep-schema.yaml b/share/machdeps/machdep-schema.yaml
index cbc7163ae36cc55e682dc13672c750a3d0ffe1c2..a48241896c2dfe48f15b7f8fa332b8ea96372879 100644
--- a/share/machdeps/machdep-schema.yaml
+++ b/share/machdeps/machdep-schema.yaml
@@ -179,6 +179,12 @@ sizeof_void:
type: integer
+ssize_t:
+
+ description: definition of 'ssize_t' (POSIX standard type)
+
+ type: string
+
uintptr_t:
description: definition of 'uintptr_t'
@@ -197,6 +203,12 @@ wchar_t:
type: string
+weof:
+
+ description: value of 'WEOF' macro
+
+ type: string
+
wint_t:
description: definition of 'wint_t'
diff --git a/share/machdeps/machdep_avr_16.yaml b/share/machdeps/machdep_avr_16.yaml
index ec24d4f54c5a410a9e982632cb644ed93d4f0519..be755d979fb9ee3c1efc3d444c26e36ca5af0ad5 100644
--- a/share/machdeps/machdep_avr_16.yaml
+++ b/share/machdeps/machdep_avr_16.yaml
@@ -30,8 +30,9 @@ sizeof_longlong: 8
sizeof_ptr: 2
sizeof_short: 2
sizeof_void: 1
+ssize_t: int
uintptr_t: unsigned int
version: clang version 15.0.7
wchar_t: int
+weof: (0xffffffffu)
wint_t: int
-
diff --git a/share/machdeps/machdep_gcc_x86_16.yaml b/share/machdeps/machdep_gcc_x86_16.yaml
index 7e4f537bb2ca800a9d7b8ae539bb0128b48e2826..f15c429e025d97de6fdb70e45b899a113ee8009b 100644
--- a/share/machdeps/machdep_gcc_x86_16.yaml
+++ b/share/machdeps/machdep_gcc_x86_16.yaml
@@ -28,7 +28,9 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: 1
+ssize_t: int
uintptr_t: unsigned long
version: none
wchar_t: int
+weof: (0xffffffffUL)
wint_t: unsigned long
diff --git a/share/machdeps/machdep_gcc_x86_32.yaml b/share/machdeps/machdep_gcc_x86_32.yaml
index 66e15e9ca00e4664aef85b54bb5f2695c260112c..c2b6c927b7b4dc00b32e42a40dec1435496a5713 100644
--- a/share/machdeps/machdep_gcc_x86_32.yaml
+++ b/share/machdeps/machdep_gcc_x86_32.yaml
@@ -28,7 +28,9 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: 1
+ssize_t: int
uintptr_t: unsigned int
version: gcc (GCC) 12.2.1 20230201
wchar_t: long
+weof: (0xffffffffu)
wint_t: unsigned int
diff --git a/share/machdeps/machdep_gcc_x86_64.yaml b/share/machdeps/machdep_gcc_x86_64.yaml
index cd58ca56090b673c1306ec2e7ab044691c935831..be370464cd6bdfc476ba6fe64d791ea46c6dfecd 100644
--- a/share/machdeps/machdep_gcc_x86_64.yaml
+++ b/share/machdeps/machdep_gcc_x86_64.yaml
@@ -28,8 +28,9 @@ sizeof_longlong: 8
sizeof_ptr: 8
sizeof_short: 2
sizeof_void: 1
+ssize_t: long
uintptr_t: unsigned long
version: gcc (GCC) 12.2.1 20230201
wchar_t: int
+weof: (0xffffffffu)
wint_t: unsigned int
-
diff --git a/share/machdeps/machdep_msvc_x86_64.yaml b/share/machdeps/machdep_msvc_x86_64.yaml
index b39d6e20ca8fef14d3615786e5727787708f7e1c..b530584b9900646ac8d427e4bd2d2fb9354b0ece 100644
--- a/share/machdeps/machdep_msvc_x86_64.yaml
+++ b/share/machdeps/machdep_msvc_x86_64.yaml
@@ -28,7 +28,9 @@ sizeof_longlong: 8
sizeof_ptr: 8
sizeof_short: 2
sizeof_void: 0
+ssize_t: long long
uintptr_t: unsigned long long
version: MSVC - X86-64bits mode
wchar_t: unsigned short
+weof: (0xffffU)
wint_t: unsigned short
diff --git a/share/machdeps/machdep_ppc_32.yaml b/share/machdeps/machdep_ppc_32.yaml
index 304e2140688eef69932395e84fe5435eaadfab36..7f0e1a922d1f076f1dba66842620654de2114b36 100644
--- a/share/machdeps/machdep_ppc_32.yaml
+++ b/share/machdeps/machdep_ppc_32.yaml
@@ -30,8 +30,9 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: 1
+ssize_t: int
uintptr_t: unsigned int
version: clang version 15.0.7
wchar_t: int
+weof: (0xffffffffu)
wint_t: unsigned int
-
diff --git a/share/machdeps/machdep_x86_16.yaml b/share/machdeps/machdep_x86_16.yaml
index cf3183d345866e1a9145031af588e5c9f1a2d60b..0ef5ad977a00c290a405a2148bcd361b4bbe195f 100644
--- a/share/machdeps/machdep_x86_16.yaml
+++ b/share/machdeps/machdep_x86_16.yaml
@@ -28,7 +28,9 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: -1
+ssize_t: int
uintptr_t: unsigned long
version: none
wchar_t: int
+weof: (0xffffffffUL)
wint_t: unsigned long
diff --git a/share/machdeps/machdep_x86_32.yaml b/share/machdeps/machdep_x86_32.yaml
index 344ef9ad0361afda50fc977b862309d2e7f6bd2f..cf02c8f3bfcce6035924a40be41c4f77d8aac7f6 100644
--- a/share/machdeps/machdep_x86_32.yaml
+++ b/share/machdeps/machdep_x86_32.yaml
@@ -28,7 +28,9 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: -1
-uintptr_t: unsigned
+ssize_t: int
+uintptr_t: unsigned int
version: gcc (GCC) 12.2.1 20230201
wchar_t: long
+weof: (0xffffffffu)
wint_t: unsigned int
diff --git a/share/machdeps/machdep_x86_64.yaml b/share/machdeps/machdep_x86_64.yaml
index ff21378b9038c300341c84cb692c12c9035ec1a1..8d9a2386e8f835f029c2238601e8d2aecd1baa38 100644
--- a/share/machdeps/machdep_x86_64.yaml
+++ b/share/machdeps/machdep_x86_64.yaml
@@ -28,7 +28,9 @@ sizeof_longlong: 8
sizeof_ptr: 8
sizeof_short: 2
sizeof_void: -1
+ssize_t: long
uintptr_t: unsigned long
-version: clang version 15.0.7
+version: gcc (GCC) 12.2.1 20230201
wchar_t: int
+weof: (0xffffffffu)
wint_t: unsigned int
diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py
index 0a61c5e6693446251d6f5253cc249245807e20a9..e8766ab6ceebd649985b7f309ac9311594c26bbd 100755
--- a/share/machdeps/make_machdep/make_machdep.py
+++ b/share/machdeps/make_machdep/make_machdep.py
@@ -108,8 +108,6 @@ def print_machdep(machdep):
if args.in_place:
args.dest_file = open(args.from_file, "w")
yaml.dump(machdep, args.dest_file, indent=4, sort_keys=True)
- # 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"
@@ -162,6 +160,7 @@ source_files = [
("alignof_str.c", "number"),
("alignof_aligned.c", "number"),
("size_t.c", "type"),
+ ("ssize_t.c", "type"),
("wchar_t.c", "type"),
("ptrdiff_t.c", "type"),
("intptr_t.c", "type"),
@@ -170,6 +169,7 @@ source_files = [
("char_is_unsigned.c", "bool"),
("little_endian.c", "bool"),
("has__builtin_va_list.c", "has__builtin_va_list"),
+ ("weof.c", "macro"),
]
@@ -191,7 +191,6 @@ def find_value(name, typ, output):
def conversion(x):
return x
-
else:
warnings.warn(f"unexpected type '{typ}' for field '{name}', skipping")
return
@@ -210,14 +209,47 @@ def find_value(name, typ, output):
if args.verbose:
print(f"compiler output is:{output}")
+def cleanup_cpp(output):
+ lines = output.splitlines()
+ macro = filter(lambda s: s != '' and s[0] != '#', lines)
+ macro = map(lambda s: s.strip(),macro)
+ return ' '.join(macro)
+
+def find_macro_value(name,output):
+ msg = re.compile(name + "_is = ([^;]+);")
+ res = re.search(msg,output)
+ if res:
+ if name in machdep:
+ value = res.group(1).strip()
+ if args.verbose:
+ print(f"[INFO] setting {name} to {value}")
+ machdep[name] = value
+ else:
+ warnings.warn(f"unexpected symbol '{name}', ignoring")
+ else:
+ warnings.warn(f"cannot find value of field '{name}', skipping")
+ if args.verbose:
+ print(f"compiler output is:{output}")
for (f, typ) in source_files:
p = my_path / f
cmd = compilation_command + [str(p)]
+ if typ == "macro":
+ # We're just interested in expanding a macro,
+ # treatment is a bit different than the rest.
+ cmd = cmd + ["-E"]
if args.verbose:
print(f"[INFO] running command: {' '.join(cmd)}")
proc = subprocess.run(cmd, capture_output=True)
Path(f).with_suffix(".o").unlink(missing_ok=True)
+ if typ == "macro":
+ if proc.returncode != 0:
+ warnings.warn(f"error in determining value of '{p,stem}', skipping")
+ if args.verbose:
+ print(f"compiler output is:{proc.stderr.decode()}")
+ continue
+ find_macro_value(p.stem,cleanup_cpp(proc.stdout.decode()))
+ continue
if typ == "has__builtin_va_list":
# Special case: compilation success determines presence or absence
machdep["has__builtin_va_list"] = proc.returncode == 0
diff --git a/share/machdeps/make_machdep/ssize_t.c b/share/machdeps/make_machdep/ssize_t.c
new file mode 100644
index 0000000000000000000000000000000000000000..95260cbfc104dff21dff8ee2209828879fa532cf
--- /dev/null
+++ b/share/machdeps/make_machdep/ssize_t.c
@@ -0,0 +1,30 @@
+/**************************************************************************/
+/* */
+/* 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 <sys/types.h>
+
+#define TEST_TYPE ssize_t
+
+TEST_TYPE_IS(int)
+TEST_TYPE_IS(long)
+TEST_TYPE_IS(long long)
diff --git a/share/machdeps/make_machdep/weof.c b/share/machdeps/make_machdep/weof.c
new file mode 100644
index 0000000000000000000000000000000000000000..67d58eb031ccc0cc8c5e6310a9d9572586ecdc8e
--- /dev/null
+++ b/share/machdeps/make_machdep/weof.c
@@ -0,0 +1,3 @@
+#include <wchar.h>
+
+const wint_t weof_is = WEOF;
diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml
index e2daa153cec1adf6e926a1be95309957e99b8900..1caae68014cec49b2135dd7ac67a8aedc80c359b 100644
--- a/src/kernel_internals/runtime/machdep.ml
+++ b/src/kernel_internals/runtime/machdep.ml
@@ -189,19 +189,19 @@ let gen_all_defines fmt mach =
gen_define_string fmt "__UINTPTR_T" mach.uintptr_t;
gen_define_string fmt "__PTRDIFF_T" mach.ptrdiff_t;
gen_define_string fmt "__WINT_T" mach.wint_t;
- (* gen_define_string fmt "__SSIZE_T" mach.ssize_t; *)
+ gen_define_string fmt "__SSIZE_T" mach.ssize_t;
gen_intlike_max fmt "__FC_SIZE" mach.size_t mach;
gen_intlike_min fmt "__FC_INTPTR" mach.intptr_t mach;
gen_intlike_max fmt "__FC_INTPTR" mach.intptr_t mach;
gen_intlike_max fmt "__FC_UINTPTR" mach.uintptr_t mach;
gen_intlike_min fmt "__FC_WCHAR" mach.wchar_t mach;
gen_intlike_max fmt "__FC_WCHAR" mach.wchar_t mach;
- (* TODO: __SSIZE_MAX *)
+ gen_intlike_max fmt "__SSIZE_MAX" mach.ssize_t mach;
gen_intlike_min fmt "__FC_PTRDIFF" mach.ptrdiff_t mach;
gen_intlike_max fmt "__FC_PTRDIFF" mach.ptrdiff_t mach;
gen_intlike_min fmt "__FC_WINT" mach.wint_t mach;
gen_intlike_max fmt "__FC_WINT" mach.wint_t mach;
- (* TODO: __FC_WEOF *)
+ gen_define_string fmt "__FC_WEOF" mach.weof;
(* NB: Frama-C's inttypes.h is assuming that intptr_t and uintptr_t have the
same rank when it comes to define PRI.?PTR macros. *)
gen_define_literal_string fmt "__PRIPTR_PREFIX"
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index b80ed81244c0260b9fa53272450e615d913aa310..1b77b2e58561cc57a9363a03a15464530a211785 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1876,6 +1876,7 @@ type mach = {
sizeof_void: int; (* Size of "void" *)
sizeof_fun: int; (* Size of function. Negative if unsupported. *)
size_t: string; (* Type of "sizeof(T)" *)
+ ssize_t: string; (* representation of ssize_t *)
wchar_t: string; (* Type of "wchar_t" *)
ptrdiff_t: string; (* Type of "ptrdiff_t" *)
intptr_t: string; (* Type of "intptr_t" *)
@@ -1900,6 +1901,7 @@ type mach = {
cpp_arch_flags: string list; (* Architecture-specific flags to be given to
the preprocessor (if supported) *)
version: string; (* Information on this machdep *)
+ weof: string; (* expansion of WEOF macro *)
}
(*
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 72e9e135a1ea228efd12012eacfd6716c33e5681..8819cba4a61430f8b2497245f1725dd9301c705c 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2640,6 +2640,7 @@ let dummy_machdep =
sizeof_void = -1;
sizeof_fun = -1;
size_t = "unsigned long";
+ ssize_t = "long";
wchar_t = "int";
ptrdiff_t = "long";
intptr_t = "long"; (* Type of "intptr_t" *)
@@ -2662,6 +2663,7 @@ let dummy_machdep =
compiler = "none";
cpp_arch_flags = [];
version = "N/A";
+ weof = "(-1)"
}
module Machdep = Datatype.Make_with_collections(struct
diff --git a/tests/misc/custom_machdep.ml b/tests/misc/custom_machdep.ml
index 7d929b77693aef27ea2ffebd598f4791214c0101..fc497312b0954cb876499b7b7a298db8dd9d47c6 100644
--- a/tests/misc/custom_machdep.ml
+++ b/tests/misc/custom_machdep.ml
@@ -16,6 +16,7 @@ let mach =
sizeof_void = 1;
sizeof_fun = 1;
size_t = "unsigned long";
+ ssize_t = "long";
intptr_t = "long";
uintptr_t = "unsigned long";
wint_t = "int";
@@ -35,6 +36,7 @@ let mach =
char_is_unsigned = false;
little_endian = true;
has__builtin_va_list = true;
+ weof = "(-1)";
}
let mach2 = { mach with compiler = "baz" }
diff --git a/tests/misc/custom_machdep.yaml b/tests/misc/custom_machdep.yaml
index 67b759afe501b21ecba938fa818ae5dd41ad055e..11e6ed0cab15d267049281edbd055056be3bfc7c 100644
--- a/tests/misc/custom_machdep.yaml
+++ b/tests/misc/custom_machdep.yaml
@@ -29,5 +29,7 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: 1
+ssize_t: long
version: foo
wchar_t: int
+weof: (-1)
diff --git a/tests/syntax/machdep_char_unsigned.ml b/tests/syntax/machdep_char_unsigned.ml
index 9ccf6d9691e3be291e0102820b8aaa71d5d0b133..51b9b7655e24e412e81e73b8045e4d083b9d514f 100644
--- a/tests/syntax/machdep_char_unsigned.ml
+++ b/tests/syntax/machdep_char_unsigned.ml
@@ -1,4 +1,3 @@
-
open Cil_types
let md = {
@@ -29,12 +28,14 @@ let md = {
char_is_unsigned = true;
little_endian = true;
size_t = "unsigned int";
+ ssize_t = "int";
wchar_t = "int";
intptr_t = "int";
uintptr_t = "unsigned int";
ptrdiff_t = "int";
wint_t = "long";
has__builtin_va_list = true;
+ weof = "(-1L)"
}
let () =