From 5c1af63612ffebeb883dfbef1b08de71ed49c680 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 10 Mar 2023 18:36:02 +0100
Subject: [PATCH] [machdep] various fixes on machdeps, __fc_machdep.h
generation and tests
- fix various typos and inconsistencies
- add an option in make_machdep.py to validate an existing yaml file,
and use it to validate manually written machdeps
- add macro with the name of the machdep (used in tests/syntax/assembly_gmp.c)
- add option to Frama-C to print the content of __fc_machdep.h on stdout
and use that to compile our libc with gcc outside of Frama-C
(as in tests/libc/runtime.c)
---
share/libc/stdint.h | 6 +-
share/libc/sys/socket.h | 2 +-
share/libc/sys/types.h | 2 +-
.../.machdep_gcc_x86_16.yaml.validated | 0
.../.machdep_msvc_x86_64.yaml.validated | 0
share/machdeps/Makefile | 11 +--
share/machdeps/machdep-schema.yaml | 8 +++
share/machdeps/machdep_avr_16.yaml | 1 +
share/machdeps/machdep_gcc_x86_16.yaml | 1 +
share/machdeps/machdep_gcc_x86_32.yaml | 1 +
share/machdeps/machdep_gcc_x86_64.yaml | 1 +
share/machdeps/machdep_msvc_x86_64.yaml | 5 +-
share/machdeps/machdep_ppc_32.yaml | 1 +
share/machdeps/machdep_x86_16.yaml | 1 +
share/machdeps/machdep_x86_32.yaml | 1 +
share/machdeps/machdep_x86_64.yaml | 1 +
share/machdeps/make_machdep/make_machdep.py | 70 ++++++++++++-------
src/kernel_internals/runtime/machdep.ml | 6 +-
src/kernel_internals/runtime/machdep.mli | 8 ++-
src/kernel_services/ast_data/cil_types.ml | 1 +
.../ast_queries/cil_datatype.ml | 1 +
src/kernel_services/ast_queries/file.ml | 9 +++
.../plugin_entry_points/kernel.ml | 12 ++++
.../plugin_entry_points/kernel.mli | 4 ++
tests/libc/runtime.c | 2 +-
tests/misc/custom_machdep.c | 2 +-
tests/misc/custom_machdep.ml | 1 +
tests/misc/custom_machdep.yaml | 5 +-
tests/syntax/assembly_gmp.c | 2 +-
tests/syntax/machdep_char_unsigned.ml | 1 +
30 files changed, 121 insertions(+), 45 deletions(-)
create mode 100644 share/machdeps/.machdep_gcc_x86_16.yaml.validated
create mode 100644 share/machdeps/.machdep_msvc_x86_64.yaml.validated
diff --git a/share/libc/stdint.h b/share/libc/stdint.h
index 77d5775d9d5..839a90e3dc1 100644
--- a/share/libc/stdint.h
+++ b/share/libc/stdint.h
@@ -147,9 +147,9 @@ typedef __UINTMAX_T uintmax_t;
/* ISO C: 7.18.2.4 - Done directly with definition of corresponding types. */
/* ISO C: 7.18.2.5 */
-#define INTMAX_MIN __FC_INTMAX_MIN
-#define INTMAX_MAX __FC_INTMAX_MAX
-#define UINTMAX_MAX __FC_UINTMAX_MAX
+#define INTMAX_MIN __INTMAX_MIN
+#define INTMAX_MAX __INTMAX_MAX
+#define UINTMAX_MAX __UINTMAX_MAX
/* ISO C: 7.18.3 */
diff --git a/share/libc/sys/socket.h b/share/libc/sys/socket.h
index 5885125caaf..f96e482a5e5 100644
--- a/share/libc/sys/socket.h
+++ b/share/libc/sys/socket.h
@@ -25,7 +25,7 @@
#include "../features.h"
__PUSH_FC_STDLIB
__BEGIN_DECLS
-#include "../__fc_machdep.h"
+#include "__fc_machdep.h"
#include "../errno.h"
diff --git a/share/libc/sys/types.h b/share/libc/sys/types.h
index 73ac60e8924..38ae7d90f8b 100644
--- a/share/libc/sys/types.h
+++ b/share/libc/sys/types.h
@@ -26,7 +26,7 @@
__PUSH_FC_STDLIB
__BEGIN_DECLS
-#include "../__fc_machdep.h"
+#include "__fc_machdep.h"
#include "../__fc_define_id_t.h"
#include "../__fc_define_pid_t.h"
#include "../__fc_define_size_t.h"
diff --git a/share/machdeps/.machdep_gcc_x86_16.yaml.validated b/share/machdeps/.machdep_gcc_x86_16.yaml.validated
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/share/machdeps/.machdep_msvc_x86_64.yaml.validated b/share/machdeps/.machdep_msvc_x86_64.yaml.validated
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/share/machdeps/Makefile b/share/machdeps/Makefile
index 3a71d5b18f2..4c402758ded 100644
--- a/share/machdeps/Makefile
+++ b/share/machdeps/Makefile
@@ -19,8 +19,9 @@
# for more details (enclosed in the file licenses/LGPLv2.1). #
# #
##########################################################################
+MANUAL_MACHDEPS=machdep_gcc_x86_16.yaml machdep_msvc_x86_64.yaml
-update-all: machdep_*.yaml
+update-all: machdep_*.yaml $(MANUAL_MACHDEPS:%=.%.validated)
machdep_avr_16.yaml \
machdep_gcc_x86_32.yaml \
@@ -35,8 +36,10 @@ machdep_%.yaml: machdep_gcc_%.yaml Makefile
-e 's/sizeof_void: .*/sizeof_void: -1/' \
-e 's/alignof_fun: .*/alignof_fun: -1/' \
-e 's/compiler: .*/compiler: generic/' \
+ -e 's/machdep_name: *machdep_gcc_\([[:alnum:]]*\)/machdep_name: machdep_\1/' \
$< > $@
-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
+.%.validated: % machdep-schema.yaml
+ @echo "Checking $*"
+ @./make_machdep/make_machdep.py --from-file $* --check-only
+ @touch $@
diff --git a/share/machdeps/machdep-schema.yaml b/share/machdeps/machdep-schema.yaml
index 3d8626026e8..fd2956acbcc 100644
--- a/share/machdeps/machdep-schema.yaml
+++ b/share/machdeps/machdep-schema.yaml
@@ -153,6 +153,14 @@ little_endian:
type: boolean
+machdep_name:
+
+ description: |
+ name of the machdep. Will be used to define a macro allowing
+ to know during preprocessing which machdep has been selected.
+
+ type: string
+
mb_cur_max:
description: expansion of 'MB_CUR_MAX' macro
diff --git a/share/machdeps/machdep_avr_16.yaml b/share/machdeps/machdep_avr_16.yaml
index 3f4ec114124..be0110cb5e3 100644
--- a/share/machdeps/machdep_avr_16.yaml
+++ b/share/machdeps/machdep_avr_16.yaml
@@ -144,6 +144,7 @@ has__builtin_va_list: true
intptr_t: int
l_tmpnam: '20'
little_endian: true
+machdep_name: machdep_avr_16
mb_cur_max: ((size_t)16)
nsig: (64 + 1)
posix_version: 200809L
diff --git a/share/machdeps/machdep_gcc_x86_16.yaml b/share/machdeps/machdep_gcc_x86_16.yaml
index e93b8af1b5d..118a19fb154 100644
--- a/share/machdeps/machdep_gcc_x86_16.yaml
+++ b/share/machdeps/machdep_gcc_x86_16.yaml
@@ -168,3 +168,4 @@ l_tmpnam: '2048'
tmp_max: '0xFFFFFFFF'
rand_max: '32767'
mb_cur_max: '((size_t)16)'
+machdep_name: machdep_gcc_x86_16
diff --git a/share/machdeps/machdep_gcc_x86_32.yaml b/share/machdeps/machdep_gcc_x86_32.yaml
index be5520f7fd3..86de296ecf7 100644
--- a/share/machdeps/machdep_gcc_x86_32.yaml
+++ b/share/machdeps/machdep_gcc_x86_32.yaml
@@ -142,6 +142,7 @@ has__builtin_va_list: true
intptr_t: int
l_tmpnam: '20'
little_endian: true
+machdep_name: machdep_gcc_x86_32
mb_cur_max: ((size_t) 16 )
nsig: (64 + 1)
posix_version: 200809L
diff --git a/share/machdeps/machdep_gcc_x86_64.yaml b/share/machdeps/machdep_gcc_x86_64.yaml
index 4e076e08a4d..8e471be4afa 100644
--- a/share/machdeps/machdep_gcc_x86_64.yaml
+++ b/share/machdeps/machdep_gcc_x86_64.yaml
@@ -142,6 +142,7 @@ has__builtin_va_list: true
intptr_t: long
l_tmpnam: '20'
little_endian: true
+machdep_name: machdep_gcc_x86_64
mb_cur_max: ((size_t) 16 )
nsig: (64 + 1)
posix_version: 200809L
diff --git a/share/machdeps/machdep_msvc_x86_64.yaml b/share/machdeps/machdep_msvc_x86_64.yaml
index 6f0b88d2cd7..aec2dd33a28 100644
--- a/share/machdeps/machdep_msvc_x86_64.yaml
+++ b/share/machdeps/machdep_msvc_x86_64.yaml
@@ -96,7 +96,7 @@ errno:
has__builtin_va_list: false
intptr_t: signed long long
little_endian: true
-nsig: 23
+nsig: '23'
ptrdiff_t: long long
# NB: wasn't defined at all in old __fc_machdep.h
sig_atomic_t: int
@@ -129,5 +129,6 @@ fopen_max: '16'
filename_max: '2048'
l_tmpnam: '20'
tmp_max: '0xFFFFFFFF'
-rand_max: 32767
+rand_max: '32767'
mb_cur_max: '((size_t)16)'
+machdep_name: machdep_msvc_x86_64
diff --git a/share/machdeps/machdep_ppc_32.yaml b/share/machdeps/machdep_ppc_32.yaml
index c5d951a4130..a295dd8ab58 100644
--- a/share/machdeps/machdep_ppc_32.yaml
+++ b/share/machdeps/machdep_ppc_32.yaml
@@ -144,6 +144,7 @@ has__builtin_va_list: true
intptr_t: int
l_tmpnam: '20'
little_endian: false
+machdep_name: machdep_ppc_32
mb_cur_max: ((size_t)16)
nsig: (64 + 1)
posix_version: 200809L
diff --git a/share/machdeps/machdep_x86_16.yaml b/share/machdeps/machdep_x86_16.yaml
index a514e444974..276ec58c4c6 100644
--- a/share/machdeps/machdep_x86_16.yaml
+++ b/share/machdeps/machdep_x86_16.yaml
@@ -168,3 +168,4 @@ l_tmpnam: '2048'
tmp_max: '0xFFFFFFFF'
rand_max: '32767'
mb_cur_max: '((size_t)16)'
+machdep_name: machdep_x86_16
diff --git a/share/machdeps/machdep_x86_32.yaml b/share/machdeps/machdep_x86_32.yaml
index 1ae9be5b6d8..5b8d5ad1fe6 100644
--- a/share/machdeps/machdep_x86_32.yaml
+++ b/share/machdeps/machdep_x86_32.yaml
@@ -142,6 +142,7 @@ has__builtin_va_list: true
intptr_t: int
l_tmpnam: '20'
little_endian: true
+machdep_name: machdep_x86_32
mb_cur_max: ((size_t) 16 )
nsig: (64 + 1)
posix_version: 200809L
diff --git a/share/machdeps/machdep_x86_64.yaml b/share/machdeps/machdep_x86_64.yaml
index e0b2e7dd95c..c572ec0c4a1 100644
--- a/share/machdeps/machdep_x86_64.yaml
+++ b/share/machdeps/machdep_x86_64.yaml
@@ -142,6 +142,7 @@ has__builtin_va_list: true
intptr_t: long
l_tmpnam: '20'
little_endian: true
+machdep_name: machdep_x86_64
mb_cur_max: ((size_t) 16 )
nsig: (64 + 1)
posix_version: 200809L
diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py
index de474f0e2ea..531334e8659 100755
--- a/share/machdeps/make_machdep/make_machdep.py
+++ b/share/machdeps/make_machdep/make_machdep.py
@@ -51,7 +51,7 @@ my_path = Path(sys.argv[0]).parent
parser = argparse.ArgumentParser(prog="make_machdep")
parser.add_argument("-v", "--verbose", action="store_true")
-parser.add_argument("-o", default=sys.stdout, type=argparse.FileType("w"), dest="dest_file")
+parser.add_argument("-o", type=argparse.FileType("w"), dest="dest_file")
parser.add_argument("--compiler", default="cc", help="which compiler to use; default is 'cc'")
parser.add_argument(
"--compiler-version",
@@ -83,33 +83,22 @@ parser.add_argument(
type=str,
help="flags to be given to the compiler (other than those set by --cpp-arch-flags); default is '-c'",
)
-parser.add_argument("--check", action="store_true")
+parser.add_argument(
+ "--check",
+ action="store_true",
+ help="checks that the generated machdep is conforming to the schema"
+)
+parser.add_argument(
+ "--check-only",
+ action="store_true",
+ help="must be used in conjunction with --from-file to check that the provided input file is conforming to the schema"
+)
args, other_args = parser.parse_known_args()
if not args.compiler_flags:
args.compiler_flags = ["-c"]
-
-if args.from_file:
- orig_file = open(args.from_file, "r")
- orig_machdep = yaml.safe_load(orig_file)
- orig_file.close()
- if not "compiler" in orig_machdep or not "cpp_arch_flags" in orig_machdep:
- raise Exception("Missing fields in yaml file")
- args.compiler = orig_machdep["compiler"]
- if isinstance(orig_machdep["cpp_arch_flags"], list):
- args.cpp_arch_flags = orig_machdep["cpp_arch_flags"]
- else: # old version of the schema used a single string
- args.cpp_arch_flags = orig_machdep["cpp_arch_flags"].split()
-
-
-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)
-
-
def make_schema():
schema_filename = my_path.parent / "machdep-schema.yaml"
with open(schema_filename, "r") as schema:
@@ -124,13 +113,40 @@ def check_machdep(machdep):
from jsonschema import validate, ValidationError
validate(machdep, schema)
+ return True
except ImportError:
warnings.warn("jsonschema is not available: no validation will be performed")
+ return True
except OSError:
warnings.warn(f"error opening {schema_filename}: no validation will be performed")
+ return True
except ValidationError:
warnings.warn("machdep object is not conforming to machdep schema")
+ return False
+if args.from_file:
+ orig_file = open(args.from_file, "r")
+ orig_machdep = yaml.safe_load(orig_file)
+ orig_file.close()
+ if args.check_only:
+ if check_machdep(orig_machdep):
+ exit(0)
+ else:
+ exit(1)
+ if not "compiler" in orig_machdep or not "cpp_arch_flags" in orig_machdep:
+ raise Exception("Missing fields in yaml file")
+ args.compiler = orig_machdep["compiler"]
+ if isinstance(orig_machdep["cpp_arch_flags"], list):
+ args.cpp_arch_flags = orig_machdep["cpp_arch_flags"]
+ else: # old version of the schema used a single string
+ args.cpp_arch_flags = orig_machdep["cpp_arch_flags"].split()
+
+def print_machdep(machdep):
+ if args.from_file and args.in_place:
+ args.dest_file = open(args.from_file, "w")
+ elif args.dest_file is None:
+ args.dest_file = sys.stdout
+ yaml.dump(machdep, args.dest_file, indent=4, sort_keys=True)
def make_machdep():
machdep = {}
@@ -251,7 +267,6 @@ def find_macros_value(output,is_list=False,entry=None):
if args.verbose:
print(f"compiler output is:{output}")
-
for (f, typ) in source_files:
p = my_path / f
cmd = compilation_command + [str(p)]
@@ -304,6 +319,12 @@ version = version_output.stdout.splitlines()[0]
machdep["compiler"] = args.compiler
machdep["cpp_arch_flags"] = args.cpp_arch_flags
machdep["version"] = version
+if args.from_file and args.in_place:
+ machdep["machdep_name"] = Path(args.from_file).stem
+elif args.dest_file:
+ machdep["machdep_name"] = Path(args.dest_file.name).stem
+else:
+ machdep["machdep_name"] = "anonymous_machdep"
missing_fields = [f for [f, v] in machdep.items() if v is None]
@@ -311,7 +332,4 @@ if missing_fields:
print("WARNING: the following fields are missing from the machdep definition:")
print(", ".join(missing_fields))
-if args.check:
- check_machdep(machdep)
-
print_machdep(machdep)
diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml
index 154d2406396..a5cbdd49eb3 100644
--- a/src/kernel_internals/runtime/machdep.ml
+++ b/src/kernel_internals/runtime/machdep.ml
@@ -49,6 +49,7 @@ let gen_byte_order fmt mach =
let no_signedness s =
let s = Option.value ~default:s (Extlib.string_del_prefix "signed" s) in
let s = Option.value ~default:s (Extlib.string_del_prefix "unsigned" s) in
+ let s = String.trim s in
if s = "" then "int" else s
let suff_of_kind =
@@ -123,8 +124,10 @@ let std_type_name mach =
"unsigned", ("UINT", false);
"unsigned int", ("UINT", false);
"long", ("LONG", true);
+ "signed long", ("LONG", true);
"unsigned long", ("ULONG", false);
"long long", ("LLONG", true);
+ "signed long long", ("LLONG" ,true);
"unsigned long long", ("ULLONG", false)
]
@@ -203,6 +206,7 @@ let gen_define_errno_macro fmt (name, v) =
let gen_all_defines fmt mach =
Format.fprintf fmt "/* Machdep-specific info for Frama-C's libc */@\n";
Format.fprintf fmt "#ifndef __FC_MACHDEP@\n#define __FC_MACHDEP@\n";
+ gen_define_int fmt ("__FC_" ^ (String.uppercase_ascii mach.machdep_name)) 1;
gen_byte_order fmt mach;
gen_fixed_size_family fmt 8 mach;
gen_fixed_size_family fmt 16 mach;
@@ -228,7 +232,7 @@ let gen_all_defines fmt 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;
- gen_intlike_max fmt "__SSIZE_MAX" mach.ssize_t mach;
+ gen_intlike_max fmt "__SSIZE" 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;
diff --git a/src/kernel_internals/runtime/machdep.mli b/src/kernel_internals/runtime/machdep.mli
index bba72de4646..8b4118076ab 100644
--- a/src/kernel_internals/runtime/machdep.mli
+++ b/src/kernel_internals/runtime/machdep.mli
@@ -22,8 +22,12 @@
(** Managing machine-dependent information. *)
-(** generates a [__fc_machdep.h] file in a temp directory and returns the
- directory name. The generated header contains all [#define] directives
+
+(** Prints on the given formatter all [#define] directives
required by [share/libc/features.h] and other system-dependent headers.
*)
+val gen_all_defines: Format.formatter -> Cil_types.mach -> unit
+
+(** generates a [__fc_machdep.h] file in a temp directory and returns the
+ directory name, to be added to the search path for preprocessing stdlib *)
val generate_machdep_header: Cil_types.mach -> Filepath.Normalized.t
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 36c2d0cd235..a42c8f7076d 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1916,6 +1916,7 @@ type mach = {
mb_cur_max: string; (* expansion of MB_CUR_MAX macro *)
nsig: string; (* expansion of non-standard NSIG macro, empty if undefined *)
errno: (string * string) list; (* list of macros defining errors in errno.h*)
+ machdep_name: string; (* name of the machdep *)
}
(*
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 8a146f1e941..b92229e2a90 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2682,6 +2682,7 @@ let dummy_machdep =
"eilseq", "84";
"erange", "34";
];
+ machdep_name = "dummy";
}
module Machdep = Datatype.Make_with_collections(struct
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index bf84049df3f..2431ccb6c45 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -396,6 +396,7 @@ type mach = Cil_types.mach = {
mb_cur_max: string;
nsig: string;
errno: (string * string) list [@of_yaml yaml_dict_to_list];
+ machdep_name: string;
}
[@@deriving yaml]
@@ -419,6 +420,14 @@ let get_machdep () =
| Error (`Msg s) ->
Kernel.fatal "Error during machdep parsing: %s" s
+let print_machdep_header () =
+ if Kernel.PrintMachdepHeader.get () then begin
+ Machdep.gen_all_defines Format.std_formatter (get_machdep());
+ raise Cmdline.Exit
+ end else Cmdline.nop
+
+let () = Cmdline.run_after_exiting_stage print_machdep_header
+
let list_available_machdeps () =
CustomMachdeps.fold (fun m _ acc -> m :: acc) (default_machdeps ())
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 656d60a3774..a3507a0ac08 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -429,6 +429,18 @@ module PrintMachdep =
let help = "pretty print selected machdep"
end)
+let () = Parameter_customize.set_group help
+let () = Parameter_customize.set_cmdline_stage Cmdline.Exiting
+let () = Parameter_customize.set_negative_option_name ""
+module PrintMachdepHeader =
+ False
+ (struct
+ let module_name = "PrintMachdepHeader"
+ let option_name = "-print-machdep-header"
+ let help =
+ "print on standard output the content of the generated __fc_machdep.h"
+ end)
+
let () = Parameter_customize.set_group help
let () = Parameter_customize.set_negative_option_name ""
module DumpDependencies =
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 0c9a85462af..0685544536d 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -320,6 +320,10 @@ module PrintMachdep : Parameter_sig.Bool
(** Behavior of option "-print-machdep"
@since Phosphorus-20170501-beta1 *)
+module PrintMachdepHeader : Parameter_sig.Bool
+(** Behavior of option "-print-machdep-header"
+ @since Frama-C+dev *)
+
module PrintLibc: Parameter_sig.Bool
(** Behavior of option "-print-libc"
@since Phosphorus-20170501-beta1 *)
diff --git a/tests/libc/runtime.c b/tests/libc/runtime.c
index ec7f02cf510..4ddb32fbb5c 100644
--- a/tests/libc/runtime.c
+++ b/tests/libc/runtime.c
@@ -1,6 +1,6 @@
/* run.config*
COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...)
- CMD: gcc -D__FC_MACHDEP_X86_64 @FRAMAC_SHARE@/libc/__fc_runtime.c -Wno-attributes -std=c99 -Wall -Wwrite-strings -o @DEV_NULL@
+ CMD: @frama-c@ -print-machdep-header > __fc_machdep.h && gcc -I. -D__FC_MACHDEP_X86_64 @FRAMAC_SHARE@/libc/__fc_runtime.c -Wno-attributes -std=c99 -Wall -Wwrite-strings -o @DEV_NULL@
OPT:
*/
diff --git a/tests/misc/custom_machdep.c b/tests/misc/custom_machdep.c
index 1e4388831b2..0fb4129d94d 100644
--- a/tests/misc/custom_machdep.c
+++ b/tests/misc/custom_machdep.c
@@ -5,10 +5,10 @@
OPT: -cpp-extra-args="-I./@PTEST_NAME@ -D__FC_MACHDEP_CUSTOM" -machdep custom -print -then -print
COMMENT: we need a -then to test double registering of a machdep
EXIT: 0
+ MODULE:
DEPS: @PTEST_NAME@/__fc_machdep_custom.h
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
// the custom machdep has defined the necessary constants
#include <ctype.h>
diff --git a/tests/misc/custom_machdep.ml b/tests/misc/custom_machdep.ml
index d54408c4914..859ea43d5d7 100644
--- a/tests/misc/custom_machdep.ml
+++ b/tests/misc/custom_machdep.ml
@@ -55,6 +55,7 @@ let mach =
"eilseq", "84";
"erange", "34";
];
+ machdep_name = "custom_machdep";
}
let mach2 = { mach with compiler = "baz" }
diff --git a/tests/misc/custom_machdep.yaml b/tests/misc/custom_machdep.yaml
index 3d6c9ab0b58..6e66f3e4667 100644
--- a/tests/misc/custom_machdep.yaml
+++ b/tests/misc/custom_machdep.yaml
@@ -42,11 +42,12 @@ filename_max: '1023'
l_tmpnam: '255'
tmp_max: '255'
rand_max: '0xFFFFFE'
-mb_cur_max: 16
+mb_cur_max: '16'
sig_atomic_t: int
time_t: long
nsig: ''
errno:
edom: "33"
eilseq: "84"
- erange": "34"
+ erange: "34"
+machdep_name: custom_machdep
diff --git a/tests/syntax/assembly_gmp.c b/tests/syntax/assembly_gmp.c
index 0d39854c42e..fb707e09767 100644
--- a/tests/syntax/assembly_gmp.c
+++ b/tests/syntax/assembly_gmp.c
@@ -86,7 +86,7 @@ File modified by CEA LIST for inclusion in Frama-C test suite
#endif
#ifndef add_mssaaaa
-#error "This test must run with machdep equals to x86_32, x86_64 or ppc_32"
+#error "This test must run with machdep equals to gcc_x86_32, gcc_x86_64, or ppc_32"
#endif
#define umul_ppmm(ph, pl, m0, m1) \
diff --git a/tests/syntax/machdep_char_unsigned.ml b/tests/syntax/machdep_char_unsigned.ml
index df75a01c391..fd26eedff20 100644
--- a/tests/syntax/machdep_char_unsigned.ml
+++ b/tests/syntax/machdep_char_unsigned.ml
@@ -54,6 +54,7 @@ let md = {
"eilseq", "84";
"erange", "34";
];
+ machdep_name = "machdep_char_unsigned";
}
let () =
--
GitLab