Skip to content
Snippets Groups Projects
Commit 0231db99 authored by Virgile Prevosto's avatar Virgile Prevosto Committed by Andre Maroneze
Browse files

headers and lint

parent b455a824
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 166 additions and 24 deletions
share/machdeps/Makefile
+ 22
− 0
View file @ 0231db99
##########################################################################
# #
# 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 \
......
share/machdeps/make_machdep/make_machdep.py
+ 20
− 10
View file @ 0231db99
......@@ -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
......
share/machdeps/make_machdep/posix_version.c
+ 22
− 0
View file @ 0231db99
/**************************************************************************/
/* */
/* 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;
share/machdeps/make_machdep/weof.c
+ 22
− 0
View file @ 0231db99
/**************************************************************************/
/* */
/* 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;
share/machdeps/make_machdep/wordsize.c
+ 22
− 0
View file @ 0231db99
/**************************************************************************/
/* */
/* 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;
src/kernel_internals/runtime/machdep.ml
+ 28
− 6
View file @ 0231db99
(**************************************************************************)
(* *)
(* 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"
......
src/kernel_internals/runtime/machdep.mli
+ 22
− 0
View file @ 0231db99
(**************************************************************************)
(* *)
(* 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
......
src/kernel_services/ast_queries/file.ml
+ 8
− 8
View file @ 0231db99
......@@ -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 =
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment