diff --git a/share/machdeps/Makefile b/share/machdeps/Makefile
index 348bb70e14067eb739f8c0ff6142c98fcd1e76c8..1b7168a5e94261fe8235f9feeeff1b0e3b7a30fb 100644
--- a/share/machdeps/Makefile
+++ b/share/machdeps/Makefile
@@ -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). #
+# #
+##########################################################################
+
update-all: machdep_*.yaml
machdep_avr_16.yaml \
diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py
index b1bbccd739aafe9fd12802d3a9d0638af8c7520d..243e7f9e9fd914d0bec96811f2bbdfae15858000 100755
--- a/share/machdeps/make_machdep/make_machdep.py
+++ b/share/machdeps/make_machdep/make_machdep.py
@@ -109,17 +109,21 @@ def print_machdep(machdep):
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:
return yaml.safe_load(schema)
+
schema = make_schema()
+
def check_machdep(machdep):
try:
from jsonschema import validate, ValidationError
- validate(machdep,schema)
+
+ validate(machdep, schema)
except ImportError:
warnings.warn("jsonschema is not available: no validation will be performed")
except OSError:
@@ -127,12 +131,14 @@ def check_machdep(machdep):
except ValidationError:
warnings.warn("machdep object is not conforming to machdep schema")
+
def make_machdep():
- 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
@@ -193,6 +199,7 @@ def find_value(name, typ, output):
def conversion(x):
return x
+
else:
warnings.warn(f"unexpected type '{typ}' for field '{name}', skipping")
return
@@ -211,15 +218,17 @@ 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)
+ 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):
+def find_macro_value(name, output):
msg = re.compile(name + "_is = ([^;]+);")
- res = re.search(msg,output)
+ res = re.search(msg, output)
if res:
if name in machdep:
value = res.group(1).strip()
@@ -231,10 +240,11 @@ def find_macro_value(name,output):
else:
warnings.warn(f"cannot find value of field '{name}', treating as empty")
if name in machdep:
- machdep[name] = ''
+ machdep[name] = ""
if args.verbose:
print(f"compiler output is:{output}")
+
for (f, typ) in source_files:
p = my_path / f
cmd = compilation_command + [str(p)]
@@ -253,9 +263,9 @@ for (f, typ) in source_files:
print(f"compiler output is:{proc.stderr.decode()}")
name = p.stem
if name in machdep:
- machdep[name] = ''
+ machdep[name] = ""
continue
- find_macro_value(p.stem,cleanup_cpp(proc.stdout.decode()))
+ 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
diff --git a/share/machdeps/make_machdep/posix_version.c b/share/machdeps/make_machdep/posix_version.c
index ded2e9b3de33fedd088a1c663337e47aa2f1d616..080e2ced861d9a6839d34f6958701e6a1d91a8ab 100644
--- a/share/machdeps/make_machdep/posix_version.c
+++ b/share/machdeps/make_machdep/posix_version.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 <unistd.h>
long posix_version_is = _POSIX_VERSION;
diff --git a/share/machdeps/make_machdep/weof.c b/share/machdeps/make_machdep/weof.c
index 67d58eb031ccc0cc8c5e6310a9d9572586ecdc8e..be6a52e55692aadcd51acdff5da6861c338eb7d4 100644
--- a/share/machdeps/make_machdep/weof.c
+++ b/share/machdeps/make_machdep/weof.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 <wchar.h>
const wint_t weof_is = WEOF;
diff --git a/share/machdeps/make_machdep/wordsize.c b/share/machdeps/make_machdep/wordsize.c
index ff430111be06b6b834f66994a65e9e5da622690e..cb12c659c36102075e5df547694e6b4b3e1d9a2f 100644
--- a/share/machdeps/make_machdep/wordsize.c
+++ b/share/machdeps/make_machdep/wordsize.c
@@ -1,2 +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). */
+/* */
+/**************************************************************************/
+
#include <features.h>
const int wordsize_is = __WORDSIZE;
diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml
index 3df712561bddd53536ea9b297fabdabe0be67b3f..707e122ae15ea7541fb56cdd9e726af54e3d3aba 100644
--- a/src/kernel_internals/runtime/machdep.ml
+++ b/src/kernel_internals/runtime/machdep.ml
@@ -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). *)
+(* *)
+(**************************************************************************)
+
open Cil_types
let gen_define fmt macro pp def =
@@ -116,12 +138,12 @@ let gen_fixed_size_family fmt bitsize mach =
match
List.find_opt (fun (s,_) -> s >= size) (existing_int_size mach)
with
- | None -> () (* No corresponding type. *)
- | Some (exact_size, kind) ->
- if size = exact_size then
- gen_int_type_family fmt (string_of_int bitsize) bitsize kind;
- gen_int_type_family fmt ("_LEAST" ^ string_of_int bitsize) bitsize kind;
- gen_int_type_family fmt ("_FAST" ^ string_of_int bitsize) bitsize kind
+ | None -> () (* No corresponding type. *)
+ | Some (exact_size, kind) ->
+ if size = exact_size then
+ gen_int_type_family fmt (string_of_int bitsize) bitsize kind;
+ gen_int_type_family fmt ("_LEAST" ^ string_of_int bitsize) bitsize kind;
+ gen_int_type_family fmt ("_FAST" ^ string_of_int bitsize) bitsize kind
let gen_max_size_int fmt mach =
gen_int_type_family fmt "MAX" (8 * mach.sizeof_longlong) "long long"
diff --git a/src/kernel_internals/runtime/machdep.mli b/src/kernel_internals/runtime/machdep.mli
index 0f51618895405a5b3222b5c74eb13fc2efa50700..bba72de46465f0e009bd4afc14f99b28c6290e94 100644
--- a/src/kernel_internals/runtime/machdep.mli
+++ b/src/kernel_internals/runtime/machdep.mli
@@ -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). *)
+(* *)
+(**************************************************************************)
+
(** Managing machine-dependent information. *)
(** generates a [__fc_machdep.h] file in a temp directory and returns the
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 787a0c808cc553c43df50a99e2d118bf29108f0a..70f10efe8cd6eaf914edc1dcb6770923610e8974 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -925,9 +925,9 @@ let cleanup file =
b.bstmts <-
List.filter
(fun x ->
- not (Cil.is_skip x.skind)
- || Cil_datatype.Stmt.Set.mem x keep_stmt
- || (changed <- true; false)
+ not (Cil.is_skip x.skind)
+ || Cil_datatype.Stmt.Set.mem x keep_stmt
+ || (changed <- true; false)
)
b.bstmts;
(* Now that annotations are in the table, we do not need to
@@ -1539,20 +1539,20 @@ module Remove_spurious = struct
kept = g :: acc.kept }
| GCompTag _ -> { acc with kept = g :: acc.kept }
| GCompTagDecl(ci,_)
- when Cil_datatype.Compinfo.Set.mem ci acc.compinfos -> acc
+ when Cil_datatype.Compinfo.Set.mem ci acc.compinfos -> acc
| GCompTagDecl(ci,_) ->
{ acc with
compinfos = Cil_datatype.Compinfo.Set.add ci acc.compinfos;
kept = g :: acc.kept }
| GEnumTag _ -> { acc with kept = g :: acc.kept }
| GEnumTagDecl(ei,_)
- when Cil_datatype.Enuminfo.Set.mem ei acc.enuminfos -> acc
+ when Cil_datatype.Enuminfo.Set.mem ei acc.enuminfos -> acc
| GEnumTagDecl(ei,_) ->
{ acc with
enuminfos = Cil_datatype.Enuminfo.Set.add ei acc.enuminfos;
kept = g :: acc.kept }
| GVarDecl(vi,_) | GFunDecl (_, vi, _)
- when Cil_datatype.Varinfo.Set.mem vi acc.varinfos -> acc
+ when Cil_datatype.Varinfo.Set.mem vi acc.varinfos -> acc
| GVarDecl(vi,_) ->
{ acc with
varinfos = Cil_datatype.Varinfo.Set.add vi acc.varinfos;
@@ -1562,8 +1562,8 @@ module Remove_spurious = struct
| GAnnot (a,_) ->
let lis = extract_logic_infos a in
if List.exists
- (fun x -> Cil_datatype.Logic_info.Set.mem x acc.logic_infos)
- lis
+ (fun x -> Cil_datatype.Logic_info.Set.mem x acc.logic_infos)
+ lis
then acc
else begin
let known_li =