From e2266e90907fa708ec350079d7266b741cc272e6 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 17 Mar 2023 17:47:57 +0100
Subject: [PATCH] headers & lint
---
.gitattributes | 2 +-
share/machdeps/Makefile | 1 +
share/machdeps/make_machdep/errno.c | 22 +++++++++++++++++++++
share/machdeps/make_machdep/limits_macros.c | 22 +++++++++++++++++++++
share/machdeps/make_machdep/make_machdep.py | 16 ++++++++++-----
share/machdeps/make_machdep/stdio_macros.c | 22 +++++++++++++++++++++
share/machdeps/make_machdep/stdlib_macros.c | 22 +++++++++++++++++++++
src/kernel_services/ast_queries/file.ml | 14 ++++++-------
8 files changed, 108 insertions(+), 13 deletions(-)
diff --git a/.gitattributes b/.gitattributes
index 43b37131d02..7e6f04ddfae 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -266,8 +266,8 @@ README* header_spec=.ignore
/share/win32_installer.iss header_spec=.ignore
/share/win32_manual_installation_step.txt header_spec=.ignore
/share/compliance/*.json header_spec=.ignore
+/share/machdeps/.machdep_*.validated header_spec=.ignore
/share/machdeps/machdep-schema.json header_spec=.ignore
-/share/machdeps/machdep_*.json header_spec=.ignore
/share/machdeps/machdep-schema.yaml header_spec=.ignore
/share/machdeps/machdep_*.yaml header_spec=.ignore
/tests/**/* header_spec=.ignore
diff --git a/share/machdeps/Makefile b/share/machdeps/Makefile
index 4c402758ded..b1b070ebf72 100644
--- a/share/machdeps/Makefile
+++ b/share/machdeps/Makefile
@@ -19,6 +19,7 @@
# 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 $(MANUAL_MACHDEPS:%=.%.validated)
diff --git a/share/machdeps/make_machdep/errno.c b/share/machdeps/make_machdep/errno.c
index ad0016ea9e5..34edccd40ff 100644
--- a/share/machdeps/make_machdep/errno.c
+++ b/share/machdeps/make_machdep/errno.c
@@ -1,3 +1,25 @@
+/**************************************************************************/
+/* */
+/* 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 <errno.h>
/* Mandatory */
diff --git a/share/machdeps/make_machdep/limits_macros.c b/share/machdeps/make_machdep/limits_macros.c
index fdef911d18e..4db15430855 100644
--- a/share/machdeps/make_machdep/limits_macros.c
+++ b/share/machdeps/make_machdep/limits_macros.c
@@ -1,3 +1,25 @@
+/**************************************************************************/
+/* */
+/* 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 <limits.h>
int path_max_is = PATH_MAX;
diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py
index ff6315492d8..824d286721d 100755
--- a/share/machdeps/make_machdep/make_machdep.py
+++ b/share/machdeps/make_machdep/make_machdep.py
@@ -86,12 +86,12 @@ parser.add_argument(
parser.add_argument(
"--check",
action="store_true",
- help="checks that the generated machdep is conforming to the schema"
+ 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"
+ 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()
@@ -99,6 +99,7 @@ args, other_args = parser.parse_known_args()
if not args.compiler_flags:
args.compiler_flags = ["-c"]
+
def make_schema():
schema_filename = my_path.parent / "machdep-schema.yaml"
with open(schema_filename, "r") as schema:
@@ -124,6 +125,7 @@ def check_machdep(machdep):
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)
@@ -141,6 +143,7 @@ if args.from_file:
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")
@@ -148,12 +151,14 @@ def print_machdep(machdep):
args.dest_file = sys.stdout
yaml.dump(machdep, args.dest_file, indent=4, sort_keys=True)
+
def make_machdep():
machdep = {}
for key in schema.keys():
machdep[key] = None
return machdep
+
machdep = make_machdep()
compilation_command = [args.compiler] + args.cpp_arch_flags + args.compiler_flags
@@ -256,10 +261,10 @@ def cleanup_cpp(output):
return " ".join(macro)
-def find_macros_value(output,is_list=False,entry=None):
+def find_macros_value(output, is_list=False, entry=None):
msg = re.compile("(\w+)_is = ([^;]+);")
if is_list:
- assert(entry)
+ assert entry
machdep[entry] = {}
for res in re.finditer(msg, output):
name = res.group(1)
@@ -276,6 +281,7 @@ 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)]
@@ -307,7 +313,7 @@ for (f, typ) in source_files:
if name in machdep:
machdep[name] = {}
continue
- find_macros_value(cleanup_cpp(proc.stdout.decode()),is_list=True,entry=name)
+ find_macros_value(cleanup_cpp(proc.stdout.decode()), is_list=True, entry=name)
continue
if typ == "has__builtin_va_list":
# Special case: compilation success determines presence or absence
diff --git a/share/machdeps/make_machdep/stdio_macros.c b/share/machdeps/make_machdep/stdio_macros.c
index 0655981e55c..cd96b805290 100644
--- a/share/machdeps/make_machdep/stdio_macros.c
+++ b/share/machdeps/make_machdep/stdio_macros.c
@@ -1,3 +1,25 @@
+/**************************************************************************/
+/* */
+/* 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 <stdio.h>
int bufsiz_is = BUFSIZ;
diff --git a/share/machdeps/make_machdep/stdlib_macros.c b/share/machdeps/make_machdep/stdlib_macros.c
index db6291aff28..8f81770908d 100644
--- a/share/machdeps/make_machdep/stdlib_macros.c
+++ b/share/machdeps/make_machdep/stdlib_macros.c
@@ -1,3 +1,25 @@
+/**************************************************************************/
+/* */
+/* 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 <limits.h>
#include <stdlib.h>
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 183e475c5df..ed44394dbb5 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -338,10 +338,10 @@ let yaml_dict_to_list = function
Result.(
bind acc
(fun l ->
- match Yaml.Util.to_string v with
- | Ok s -> Ok((k,s) :: l)
- | Error (`Msg s) ->
- Error (`Msg ("Unexpected value for key " ^ k ^ ": " ^ s))))
+ match Yaml.Util.to_string v with
+ | Ok s -> Ok((k,s) :: l)
+ | Error (`Msg s) ->
+ Error (`Msg ("Unexpected value for key " ^ k ^ ": " ^ s))))
in
List.fold_left make_one (Ok []) l
| _ -> Error (`Msg "Unexpected YAML value instead of dictionary of strings")
@@ -434,9 +434,9 @@ let get_machdep () =
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
+ 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
--
GitLab