From 9c3171bcd85b674e858bb1aa93c4df34e19d5e6b Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 11 May 2023 18:25:36 +0200
Subject: [PATCH] [machdep] more robust generator
- --compile-flags="-c -I/path" works (i.e. there's no need to provide as many
--compile-flags options as you have flags to pass to the compiler itself.
Ditto for --cpp-arch-flags of course
- we start by checking that a minimal C file does not trigger a compiler error
with the given option and we abort otherwise. This ensures that subsequent
tests will not mistakenly take a configuration error for a genuine result.
---
share/machdeps/make_machdep/make_machdep.py | 14 +++++++++++-
share/machdeps/make_machdep/sanity_check.c | 24 +++++++++++++++++++++
2 files changed, 37 insertions(+), 1 deletion(-)
create mode 100644 share/machdeps/make_machdep/sanity_check.c
diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py
index c7a8cabe9fc..bd0b6cefa82 100755
--- a/share/machdeps/make_machdep/make_machdep.py
+++ b/share/machdeps/make_machdep/make_machdep.py
@@ -176,9 +176,15 @@ def make_machdep():
machdep = make_machdep()
-compilation_command = [args.compiler] + args.cpp_arch_flags + args.compiler_flags
+compilation_command = [args.compiler]
+
+for flag in args.cpp_arch_flags + args.compiler_flags:
+ compilation_command = compilation_command + flag.split(" ")
source_files = [
+ # sanity_check is juste here to ensure that the given compiler
+ # and flags are coherent. It must be kept at the top of the list.
+ ("sanity_check.c", "none"),
("sizeof_short.c", "number"),
("sizeof_int.c", "number"),
("sizeof_long.c", "number"),
@@ -317,6 +323,12 @@ for f, typ in source_files:
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 == "none":
+ if proc.returncode != 0:
+ logging.critical("cannot compile sample C file with provided compiler and flags.")
+ logging.info(f"compiler output is:{proc.stderr.decode()}")
+ sys.exit(1)
+ continue
if typ == "macro":
if proc.returncode != 0:
logging.warning(f"error in preprocessing value '{p}', some values won't be filled")
diff --git a/share/machdeps/make_machdep/sanity_check.c b/share/machdeps/make_machdep/sanity_check.c
new file mode 100644
index 00000000000..8e38b55803d
--- /dev/null
+++ b/share/machdeps/make_machdep/sanity_check.c
@@ -0,0 +1,24 @@
+/**************************************************************************/
+/* */
+/* 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). */
+/* */
+/**************************************************************************/
+
+/* ensure that the given compiler and flags support a minimal C file */
+int main () { }
--
GitLab