Skip to content
Snippets Groups Projects
Commit 00ab300d authored by Patrick Baudin's avatar Patrick Baudin
Browse files

Merge branch 'feature/header-spec-in-git-attributes' into 'master' 

header spec in git attributes

See merge request frama-c/frama-c!3762
parents 506e66c5 eb185a68
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 516 additions and 608 deletions
doc/userman/Makefile
+ 22
− 0
View file @ 00ab300d
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# 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). #
# #
##########################################################################
# Require texi2pdf
.DEFAULT_GOAL := all
......
doc/userman/Makefile.config
+ 22
− 0
View file @ 00ab300d
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# 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). #
# #
##########################################################################
MAKECONFIG_DIR=../../share
include ../../share/Makefile.common
FRAMAC_VERSION=$(shell $(SED) -e 's/\\(.*\\)/\\1/' ../../VERSION)
headers/check-headers.sh deleted 100755 → 0
+ 0
− 265
View file @ 506e66c5
#!/bin/sh
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# All rights reserved. #
# Contact CEA LIST for licensing. #
# #
##########################################################################
APPLINAME="$0"
echo $0 $@
Usage() {
APPLI=$(basename $APPLINAME)
echo "Usage: $APPLI <options> <files>"
echo " $APPLI [--update] --spec-files <spec-files>"
echo " 1. Checks entries of <spec-files>"
echo " --update: updates <spec-files> by removing comments and multiple entries"
echo " $APPLI [--update] [--no-headers <header-file>]* <spec-file> ([--files-from] <file>]*"
echo " 1. Checks entries of <spec-file>"
echo " --update: updates <spec-file> by removing comments and multiple entries"
echo " 2. Checks that every <files> have an entry into the <spec-file>"
echo " 3. Checks that all the <files> are not attributed to <header-file> in <spec-file>"
echo " --no-headers <header-file>: cumulative option"
exit 0
}
Requires () {
for File in "$@"
do
where=$(which $File)
if [ "$?" != "0" ] ; then
echo "Error: executable not found: $File"
exit 1
fi
done
}
RegExp=""
Checking () {
Requires sort tr grep diff sed
if [ "$SpecFilesOpt" != "" ] && [ "$HeadersOpt" != "" ] ; then
echo "Error: given options are exclusives"
exit 1
fi
if [ "$1" = "" ] ; then
echo "Error: missing argument"
exit 1
fi
if [ ! -f "$1" ] ; then
echo "Error: file not found: $file"
exit 1
fi
if [ "$SpecFilesOpt" != "" ] ; then
shift
for file in $@ ; do
if [ "$file" != "--files-from" ] && [ ! -f $file ] ; then
echo "Error: file not found: $file"
exit 1
fi
done
fi
if [ "$HeadersOpt" != "" ] ; then
RegExp="("
for file in $HeadersOpt ; do
SyntaxOk=$(echo "$file" | tr -d "._[:alnum:]")
if [ "$SyntaxOk" != "" ] ; then
echo "Error: invalid header filename: $file"
exit 1
fi
if [ "$RegExp" != "(" ] ; then
RegExp="${RegExp}|"
fi
RegExp="${RegExp}$(echo $file | sed -e 's:\.:\\.:')"
done
RegExp="^${RegExp}):"
fi
}
Result="0"
Check () {
Warn=""
cat $1 \
| tr "[:blank:]" " " \
| sed -e 's: *: :g' \
| sed -e 's:^ ::g' \
| sed -e 's: $::g' \
| sed -e 's/ :/:/g' \
| sed -e 's/:\([^ ]\)/: \1/g' \
> $1.$$
TMP1=$1.$$
if [ "$?" != "0" ] && [ "$2" = "-step-1" ] ; then
echo " Warning: some blank characters can be cleaned:"
diff $1 $TMP1 | grep "^> "
Warn="Ok"
fi
grep -v "^#" $TMP1 > ${TMP1}.$$
TMP2=${TMP1}.$$
LC_ALL=C sort -k2 -k1 $TMP2 > $TMP1
diff -q $TMP1 $TMP2 > /dev/null
if [ "$?" != "0" ] && [ "$2" = "-step-1" ] ; then
echo " Warning: some entries are unsorted:"
diff $TMP1 $TMP2 | grep "^> "
Warn="Ok"
fi
LC_ALL=C sort -u -k2 -k1 $TMP1 > $TMP2
diff -q $TMP2 $TMP1 > /dev/null
if [ "$?" != "0" ] ; then
if [ "$2" = "-step-1" ] ; then
echo " Warning: some entries are duplicated:"
else
echo " Warning: the following given files are duplicated:"
fi
diff $TMP2 $TMP1 | sed -n -e "s/^> ~no-entry-for:/ /p"
Warn="Ok"
fi
LC_ALL=C sort -u -k2 $TMP2 > $TMP1
if [ "$3" != "" ] ; then
diff $TMP1 $3 > /dev/null
if [ "$?" != "0" ] ; then
echo " Error: some files have no entry:"
diff $3 $TMP1 | sed -n -e "s/^> ~no-entry-for:/ /p"
Warn="OkOk"
Result="1"
fi
else
diff -q $TMP1 $TMP2 > /dev/null
if [ "$?" != "0" ] ; then
if [ "$2" = "-step-1" ] ; then
echo " Error: some entries are duplicated."
echo " removed entries:"
else
echo " Error: some checked entries have unwanted headers:"
fi
diff $TMP1 $TMP2 | grep "^> "
Warn="OkOk"
Result="1"
fi
fi
}
CheckSpecFile () {
echo " Checking specification file $1..."
Check "$1" "-step-1"
if [ "$Warn" = "OkOk" ] ; then
if [ "$UpdateOpt" != "--update" ] ; then
rm $TMP1 $TMP2
echo " Use --update option to update $1 file"
exit 1
fi
fi
if [ "$UpdateOpt" = "--update" ] ; then
if [ "$Warn" = "" ] ; then
diff -q $TMP1 $1 > /dev/null
if [ "$?" != "0" ] ; then
Warn="Ok"
fi
fi
if [ "$Warn" = "" ] ; then
echo "Warning: already up to date"
else
echo " Updating file $1"
mv $TMP1 $1
fi
fi
}
UpdateOpt=""
HeadersOpt=""
SpecFilesOpt=""
while [ "$1" != "" ] ; do
case "$1" in
-h) Usage;;
-help) Usage;;
--help) Usage;;
--update) UpdateOpt="$1";;
--spec-files) SpecFilesOpt="$1";;
--no-headers) shift; HeadersOpt="${Headers} $1";;
--files-from) break;;
--*) echo "Unknown option $1"; exit 1;;
*) break;;
esac
shift
done
Checking $@
BuildTmpFile() {
TmpFile="$1"
shift
Str="$1"
shift
while [ "$1" != "" ]; do
if [ "$1" = "--files-from" ] ; then
shift
cat $1 \
| tr "[:blank:]" " " \
| sed -e 's: *: :g' \
| sed -e 's:^ ::g' \
| sed -e 's: $::g' \
| egrep -v '^#' \
| sed -e "s#^#${Str}: #" >> $TMP
else
echo "${Str}: $1" >> $TMP
fi
shift
done
}
if [ "$SpecFilesOpt" = "" ] ; then
# echo "Step 1..."
SpecFile=$1
shift
CheckSpecFile $SpecFile
# echo " Removing temporary files"
mv $TMP2 $TMP1
RefStep2=$TMP1
if [ "$1" != "" ]; then
# echo "Step 2..."
echo " Checking that all given files have an entry..."
cat $RefStep2 > $RefStep2.$$
TMP=$RefStep2.$$
BuildTmpFile $TMP "~no-entry-for" $@
Check $TMP "-step-2" $RefStep2
# echo " Removing temporary files"
rm -f $TMP $TMP1 $TMP2
fi
rm -f $RefStep2
if [ "$RegExp" != "" ] && [ "$1" != "" ]; then
# echo "Step 3..."
echo " Checking for files having unwanted headers..."
egrep -e "$RegExp" $SpecFile > $SpecFile.$$
TMP=$SpecFile.$$
BuildTmpFile $TMP "./looking-for" $@
Check $TMP "-step-3"
# echo " Removing temporary files"
rm -f $TMP $TMP1 $TMP2
fi
if test $Result -eq 0; then
echo "No issue detected. Great!"
fi
exit $Result
else
# echo "Step 1..."
for file in $@ ; do
CheckSpecFile $file
# echo " Removing temporary files"
rm -f $TMP1 $TMP2
done
fi
\ No newline at end of file
headers/close-source/ACSL_EL → headers/close-source/CEA_PR_LGPL
+ 0
− 0
View file @ 00ab300d
File moved
headers/close-source/XL_COMPCERT 0 → 100644
+ 10
− 0
View file @ 00ab300d
The Compcert verified compiler
Xavier Leroy, INRIA Paris-Rocquencourt
Copyright Institut National de Recherche en Informatique et en
Automatique. All rights reserved. This file is distributed
under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 2 of the License, or
(at your option) any later version. This file is also distributed
under the terms of the INRIA Non-Commercial License Agreement.
headers/hdrck.ml
+ 194
− 76
View file @ 00ab300d
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2022 *)
(* 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). *)
(* *)
(**************************************************************************)
type spec_format = Sep1Line1 (* <space>* FileName <space>* `:` <space>* HeaderId <space>* <eol> *)
| Sep2Line1 (* <space>* FileName <space>* `:` <space>* AttributeName <space>*`:` <space>*HeaderId <space>* <eol> *)
| Line3 (* FileName <eol> AttributeName <eol> HeaderId <eol> *)
| Zero3 (* FileName <null> AttributeName <null> HeaderId <null> *)
(* Sep1Line1
> cat headers/header_spec.txt | headers/hdrck --stdin -spec-format=2-fields-by-line -header-dirs headers/open-source
*)
(* Sep2Line1
> cat headers/header_spec.txt | tr ':' '\n' | xargs -n 2 printf " %s : header_spec : %s \n" > x-3-fields-by-line.txt
> cat x-3-fields-by-line.txt | headers/hdrck --stdin -spec-format=3-fields-by-line -header-dirs headers/open-source
*)
(* Line3
> cat headers/header_spec.txt | tr ':' '\n' | xargs -n 2 printf "%s\nheader_spec\n%s\n" > x-3-lines.txt
> cat x-3-lines.txt | headers/hdrck --stdin -spec-format=3-lines -header-dirs headers/open-source
*)
(* Zero
> cat headers/header_spec.txt | tr ':' '\n' | xargs -n 2 printf "%s\nheader_spec\n%s\n" | tr '\n' '\0' > x-3-zeros.txt
> cat x-3-zeros.txt | headers/hdrck --stdin -z -header-dirs headers/open-source
*)
(* From the git archive
> git ls-files -z | git check-attr --stdin -z header_spec \
| headers/hdrck --stdin -z -header-dirs headers/open-source -header-dirs src/plugins/e-acsl/headers/open-source
*)
(* Parameters settable from command line *)
let debug_flag = ref false
and spec_files = ref []
and from_stdin = ref false
and zero_stdin = ref false
and spec_format = ref Sep1Line1
and header_dirs = ref []
and forbidden_headers = ref []
and root_dir = ref (Sys.getcwd ())
......@@ -8,7 +58,8 @@ and distrib_file = ref None
and header_except_file = ref None
and headache_config_file = ref "headers/headache_config.txt"
and exit_on_warning = ref false
and exit_on_error = ref true (* only set to false for debugging purposes *)
and exit_on_error = ref true (* only settable to false for debugging purposes *)
type mode =
| Check
......@@ -96,18 +147,27 @@ let get_tmp_dirname () = match !tmp_dirname with
dirname
| Some dirname -> dirname
let get_string_null (ic:in_channel) =
let rec aux acc =
let c = input_char ic in
if c <> '\000' then aux (c :: acc) else acc
in
let tab = Array.of_list (List.rev (aux [])) in
String.init (Array.length tab) (Array.get tab)
(* Reads [nlines] lines of a file named [filename].
*
* Defaults to reading the file entirely since any integer will ever be greater
* or equal than [max_int].
*)
let read_lines ?nlines:(nlines=max_int) filename =
let read_lines ?nlines:(nlines=max_int) get_line filename =
let lines = ref [] in
let ic = open_in filename in
let ic = if filename = "--stdin" then stdin else open_in filename in
let n = ref 1 in
try
while !n <= nlines do
lines := input_line ic :: !lines;
lines := get_line ic :: !lines;
incr n
done;
close_in ic;
......@@ -123,7 +183,10 @@ let extract_sub_dir filename =
| sub_dir :: _ :: _ -> sub_dir
| _ -> ""
let colon_reg_exp = Str.regexp ":"
let split_line_entry =
let colon_reg_exp = Str.regexp ":" in
fun (line:string) ->
List.map String.trim (Str.split colon_reg_exp line)
module StringSet = struct
include Set.Make(struct type t = string let compare = String.compare end)
......@@ -143,68 +206,103 @@ end
@param license_name
*)
let add_spec_entry (ignored_files: StringSet.t ref) (spec_tab: (string, string) Hashtbl.t)
idx (file_name : string) (license_name: string) =
if license_name <> ".ignore" then begin
try
let previous_entry = Hashtbl.find spec_tab file_name in
if license_name <> previous_entry then
idx ~(file_name : string) ~(license_name: string) =
match license_name with
| ("set" | "unset" | "unspecified") ->
warn (* error ~exit_value:9 *)
"%s: invalid specification (%d) for that file (git attribute value=%s)@."
file_name idx license_name
| ".ignore" -> begin
try
let previous_entry = Hashtbl.find spec_tab file_name in
error ~exit_value:6
"%s: specification duplicated (%d) with a different license name (%s and %s)@."
file_name idx license_name previous_entry
else if StringSet.mem file_name !ignored_files then
error ~exit_value:6
"%s: specification duplicated (%d) with a different license name (%s and %s)@."
file_name idx license_name ".ignore"
else warn "%s: specification duplicated (%d)@." file_name idx
with Not_found -> Hashtbl.add spec_tab file_name license_name
end
else begin
try
let previous_entry = Hashtbl.find spec_tab file_name in
error ~exit_value:6
"%s: specification duplicated (%d) with a different license name (%s and %s)@."
file_name idx previous_entry ".ignore"
with Not_found ->
if StringSet.mem file_name !ignored_files then
warn "%s: specification duplicated (%d)@." file_name idx
else ignored_files := StringSet.add file_name !ignored_files
end
file_name idx previous_entry ".ignore"
with Not_found ->
if StringSet.mem file_name !ignored_files then
warn "%s: specification duplicated (%d)@." file_name idx
else ignored_files := StringSet.add file_name !ignored_files
end
| _ -> begin
try
let previous_entry = Hashtbl.find spec_tab file_name in
if license_name <> previous_entry then
error ~exit_value:6
"%s: specification duplicated (%d) with a different license name (%s and %s)@."
file_name idx license_name previous_entry
else if StringSet.mem file_name !ignored_files then
error ~exit_value:6
"%s: specification duplicated (%d) with a different license name (%s and %s)@."
file_name idx license_name ".ignore"
else warn "%s: specification duplicated (%d)@." file_name idx
with Not_found ->
if StringSet.mem file_name !ignored_files then
error ~exit_value:6
"%s: specification duplicated (%d) with a different license name (%s and %s)@."
file_name idx license_name ".ignore"
else Hashtbl.add spec_tab file_name license_name
end
(* Reads the contents of the specification.
Each line of the file is assumed to contain one association of the form:
<filename_id>\s+:\s+<license_id>
where:
- \s matches any whitespace character
- identifiers can contain anything but whitespaces.
Each line of the file using the [spec_format].
Lines that do not match this pattern are ignored.
@param spec_tab (file -> license header name) hashtable to update
@param ignored_files set of ignored files to update.
*)
let read_specs (ignored_files: StringSet.t ref) (spec_tab: (string, string) Hashtbl.t) (spec_file : string) =
debug "Specification file: %s@." spec_file;
job_head "Checking format of specification file %s... @?" spec_file;
let spec_lines = read_lines spec_file in
let sub_dir = extract_sub_dir spec_file in
List.iteri
(fun i spec_line ->
match Str.split colon_reg_exp spec_line with
| filename :: [license_name] ->
let filename = String.trim filename in
let filename =
if sub_dir <> "" then path_concat sub_dir filename else filename
in
let filename = path_concat !root_dir filename in
let license_name = String.trim license_name in
add_spec_entry ignored_files spec_tab i filename license_name
| _ ->
warn "%s (%d): bad line format@." spec_file i
) spec_lines;
let read_specs spec_format (ignored_files: StringSet.t ref) (spec_tab: (string, string) Hashtbl.t) (spec_file : string option) =
let spec_fname = match spec_file with None -> "--stdin" | Some filename -> filename in
debug "Specification file: %s@." spec_fname ;
job_head "Checking format of specification file %s... @?" spec_fname;
let sub_dir = extract_sub_dir spec_fname in
let add_spec, get_line =
let add_spec_item i ~file_name ~license_name =
let file_name =
if sub_dir <> "" then path_concat sub_dir file_name else file_name
in
let file_name = path_concat !root_dir file_name in
add_spec_entry ignored_files spec_tab i ~file_name ~license_name
in
let add_spec_Sep1Line1 spec_lines =
List.iteri
(fun i spec_line ->
match split_line_entry spec_line with
| file_name :: [license_name] ->
add_spec_item i ~file_name ~license_name
| _ -> warn "%s (%d): bad line format@." spec_fname (i+1)
) spec_lines
and add_spec_Sep2Line1 spec_lines =
List.iteri
(fun i spec_line ->
Format.printf "%s@." spec_line;
match split_line_entry spec_line with
| file_name :: "header_spec" :: [license_name] ->
add_spec_item i ~file_name ~license_name
| _ :: attr :: [_] -> warn "%s (%d): bad attribute name: %s@." spec_fname (i+1) attr
| _ -> warn "%s (%d): bad line format@." spec_fname (i+1)
) spec_lines
and add_spec_Sep0Line3 spec_lines =
let rec add_spec i = function
| [] -> ()
| file_name :: "header_spec" :: license_name :: spec_lines ->
add_spec_item i ~file_name ~license_name ;
add_spec (i+1) spec_lines
| _ :: attr :: _ :: _ ->
warn "%s (%d): (3-upplet: %d) attribute name: %s@." spec_fname ((3*i)+1) (i+1) attr
| _ -> warn "%s (%d): (3-upplet: %d) bad format@." spec_fname ((3*i)+1) (i+1)
in add_spec 0 spec_lines
in match spec_format with
| Sep1Line1 -> add_spec_Sep1Line1,input_line
| Sep2Line1 -> add_spec_Sep2Line1,input_line
| Line3 -> add_spec_Sep0Line3,input_line
| Zero3 -> add_spec_Sep0Line3, get_string_null
in
let spec_lines = read_lines get_line spec_fname in
add_spec spec_lines;
job_done ()
let coma_reg_exp = Str.regexp ","
let set_cumulative (name:string) (value: string list ref) (set : string) =
let set_cumulative ~(name:string) (value: string list ref) ~(set : string) =
debug "Register cumulative %s option: %s" name set;
value := List.fold_left
(fun acc v -> let v = String.trim v in if v="" then acc else v::acc)
......@@ -338,7 +436,7 @@ let check_spec_discrepancies
) specs ;
if !n > 0 then begin
error ~exit_value:4 "@[<v 2>%a%d / %d files with bad headers@]@."
(fun ppf l ->
(fun _ppf l ->
List.iter
(fun (file, hdr_type) ->
error_fmt "%s : header differs from spec %s@."
......@@ -352,7 +450,7 @@ let check_spec_discrepancies
let check_forbidden_headers (forbidden_headers:StringSet.t) header_specifications (distributed_files:StringSet.t) =
if not (StringSet.is_empty forbidden_headers) then begin
job_head "Checking that all distributed files have no forbidden header specification @?";
job_head "Checking that all distributed files have no forbidden header specification... @?";
let forbidden = ref [] in
let n = ref 0 in
StringSet.iter
......@@ -365,7 +463,7 @@ let check_forbidden_headers (forbidden_headers:StringSet.t) header_specification
distributed_files;
if !forbidden <> [] then
error ~exit_value:4 "@[<v 2>%a%d / %d files with bad headers@]@."
(fun ppf l ->
(fun _ppf l ->
List.iter
(fun (file, hdr_type) ->
error_fmt "%s : forbidden header %s@."
......@@ -488,42 +586,59 @@ let executable_name = Sys.argv.(0)
let umsg =
Format.sprintf "Usage: %s [options] <header spec files>@.%s"
executable_name
("The line format of each <header spec files> is:\n" ^
" <source file> ':' <license definition>\n" ^
("The default format of each <header spec files> is \"2-fields-by-line\".\n" ^
"The different formats are:\n" ^
"- \"2-fields-by-line\" format:\n\t<space>* <source file> <space>* ':' <space>* <license definition> <space>* <eol>\n" ^
"- \"3-fields-by-line\" format:\n\t<space>* <source file> <space>* ':' <space>* 'header_spec' <space>* ':' <space>* <license definition> <space>* <eol>\n" ^
"- \"3-lines\" format:\n\t<source file> <eol> 'header_spec' <eol> <license definition> <eol>\n" ^
"- \"3-zeros\" format:\n\t<source file> <zero> 'header_spec' <zero> <license definition> <zero>\n" ^
"where <license definition> is '.ignore' or a license definition file.\n" ^
"The location directory of the license definitions can be specified using the -header-dirs option.\n" ^
"When the name of a <header spec file> has the form 'path/./header-spec-file',\n"^
"then the <source file> names that it contains\n" ^
"When the name of a <header spec file> has the form 'path/./header-spec-file', "^
"then the <source file> names that it contains " ^
"are considered beeing relative to given 'path'.\n" ^
"That is done before processing the option '-C <dir>'." )
"That is done before processing the option '-C <dir>'.'\n" ^
"List of the options:")
let rec argspec = [
"--help", Arg.Unit print_usage ,
" print this option list and exits";
"--stdin", Arg.Set from_stdin,
" extract an header spec from the standard input in addition to the given header spec files";
"-help", Arg.Unit print_usage ,
" print this option list and exits";
"-debug", Arg.Set debug_flag,
" enable debug messages";
"-forbidden-headers", Arg.String (set_cumulative "-forbidden-headers" forbidden_headers) ,
" none of the distributed files may have one of these license name";
"-header-dirs", Arg.String (set_cumulative "-header-dirs" header_dirs),
" add comma separated list of directories to search for license header definitions [.]";
"-forbidden-headers", Arg.String (fun set -> set_cumulative ~name:"-forbidden-headers" forbidden_headers ~set) ,
"<license name>,... \t none of the checked files may have one of the <license name> []";
"-header-dirs", Arg.String (fun set -> set_cumulative ~name:"-header-dirs" header_dirs ~set),
"<directory>,... \t list of <directory> to search for license header definitions []";
"-distrib-file", Arg.String (set_opt distrib_file),
" set filename with a list of files set for distribution";
"<filename> \t considers only the files listed into the <filename>";
"-header-except-file", Arg.String (set_opt header_except_file),
" set filename with a list of files whose headers do not need checking";
"<filename> \t does not look at the files listed into the <filename>";
"-headache-config-file", Arg.Set_string headache_config_file,
Format.sprintf " set headache configuration file [%s]" !headache_config_file;
Format.sprintf "<filename> \t set headache configuration file [%s]" !headache_config_file;
"-no-exit-on-error", Arg.Unit (fun () -> exit_on_error := false),
" do not exit on errors ";
" does not exit on errors ";
"-exit-on-warning", Arg.Set exit_on_warning,
" considers warnings as errors (anyway, forces exit on errors too)";
"-update", Arg.Unit (fun () -> mode := Update),
" update headers w.r.t to the <header spec file>";
" updates headers w.r.t to the <header spec file>";
"-C", Arg.Set_string root_dir,
Format.sprintf
" prepend <dir> to filenames in header specification [%s] "
"<dir> \t prepends <dir> to filenames in header specification [%s] "
!root_dir;
"-spec-format", Arg.String (function
| "2-fields-by-line" -> spec_format := Sep1Line1
| "3-fields-by-line" -> spec_format := Sep2Line1
| "3-lines" -> spec_format := Line3
| "3-zeros" -> spec_format := Zero3
| s -> Format.printf "invalid spec format: %s@." s ; print_usage ()),
"<format>\t \"2-fields-by-line\"|\"3-fields-by-line\"|\"3-lines\"|\"3-zeros\"";
"-z", Arg.Set zero_stdin,
" force to use the spec format \"3-zeros\" when reading from stdin";
]
and sort argspec =
......@@ -545,25 +660,28 @@ let _ =
check_headache_config_file ();
begin
match !spec_files, !distrib_file, !header_except_file with
| [], _, _ ->
| [], _, _ when not !from_stdin ->
Format.printf "Please set a specification file@\n@.";
print_usage ();
| spec_files, distrib_file_opt, header_except_opt ->
let specified_files = Hashtbl.create 256 in
let ignored_files = ref StringSet.empty in
List.iter (read_specs ignored_files specified_files) spec_files;
if !from_stdin then read_specs (if !zero_stdin then Zero3 else !spec_format) ignored_files specified_files None;
List.iter (fun f -> read_specs !spec_format ignored_files specified_files (Some f)) spec_files;
Format.printf "- ignored=%d@.- specified=%d@." (StringSet.cardinal !ignored_files) (Hashtbl.length specified_files);
match !mode with
| Check ->
let stringset_from_opt_file = function
| None -> StringSet.empty
| Some file ->
let lines = read_lines file in
let lines = read_lines input_line file in
List.fold_left
(fun s l -> StringSet.add (path_concat !root_dir l) s)
StringSet.empty lines
in
let distributed_files = stringset_from_opt_file distrib_file_opt in
let header_exception_files = stringset_from_opt_file header_except_opt in
Format.printf "- excepted=%d@.- distributed=%d@." (StringSet.cardinal header_exception_files) (StringSet.cardinal distributed_files);
check !ignored_files specified_files distributed_files header_exception_files
| Update ->
update_headers specified_files;
......
headers/headache.sh deleted 100755 → 0
+ 0
− 55
View file @ 506e66c5
#!/bin/sh
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# All rights reserved. #
# Contact CEA LIST for licensing. #
# #
##########################################################################
APPLINAME="$0"
Usage() {
APPLI=$(basename $APPLINAME)
echo "Usage: $APPLI -c <headache-config> -h <header-file> <file>"
echo " Runs headache with the same arguments when <file> exists"
exit 1
}
Requires () {
# Looking for executables
for File in "$@" ; do
where=$(which $File)
if [ "$?" != "0" ] ; then
echo "Error: executable not found: $File"
exit 1
fi
done
}
Error() {
echo "Error: $@"
exit 1
}
CheckingVariables () {
([ "$1" = "--help" ] || [ "$1" = "-help" ] || [ "$1" = "-h" ]) && Usage
[ "$6" != "" ] && Error "too much arguments"
[ "$5" = "" ] && Error "too few arguments: $@"
[ "$1" != "-c" ] && Error "missing -c as first option"
[ ! -f "$2" ] && Error "config file not found $2"
[ "$3" != "-h" ] && Error "missing -h as second option"
[ ! -f "$4" ] && Error "header file not found $5"
}
Requires headache
CheckingVariables $@
if [ -f "$5" ]; then
headache $@
fi
headers/headache_config.txt
+ 47
− 1
View file @ 00ab300d
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# 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). #
# #
##########################################################################
# note: the skip directive requires a filename starting by ".*"
#############
# This file #
#############
| "headache_config.txt" -> frame open:"#" line:"#" close:"#"
##################
# Objective Caml #
##################
......@@ -27,13 +56,13 @@
############
# Makefile #
############
| ".*makefile.*" -> frame open:"#" line:"#" close:"#"
| ".*Make.*" -> frame open:"#" line:"#" close:"#"
| ".*\.mk" -> frame open:"#" line:"#" close:"#"
#################
# Shell scripts #
#################
#note: the skip directive requires a filename starting by ".*" ???
| "autocomplete_frama-c" -> frame open: "#" line: "#" close: "#"
| "_frama-c" -> frame open: "#" line: "#" close: "#"
| ".*_frama-c" -> skip match:"#compdef.*"
......@@ -58,12 +87,29 @@
| "frama-c.debug" -> frame open:"#" line:"#" close:"#"
| ".*frama-c.debug" -> skip match:"#!.*"
#############
# Git hooks #
#############
| "pre-commit" -> frame open:"#" line:"#" close:"#"
| ".*pre-commit" -> skip multiline_match: "#!.*" multiline_match: "# -\*-.*"
###############
# Zsh scripts #
###############
| ".*\.zsh" -> frame open:"#" line:"#" close:"#"
| ".*\.zsh" -> skip match:"#compdef .*"
| "_frama-c" -> frame open:"#" line:"#" close:"#"
| ".*_frama-c" -> skip match:"#compdef .*"
################
# Perl scripts #
################
| ".*\.perl" -> frame open:"#" line:"#" close:"#"
| ".*\.perl" -> skip match:"#!.*"
| "flamegraph.pl" -> frame open:"#" line:"#" close:"#"
| ".*flamegraph.pl" -> skip match:"#!.*"
| "duplicates.pl" -> frame open:"#" line:"#" close:"#"
| ".*duplicates.pl" -> skip match:"#!.*"
#########################
# MS-Windows Resources #
......
headers/header_spec.txt
+ 44
− 47
View file @ 00ab300d
......@@ -15,7 +15,7 @@ README.md: .ignore
VERSION: .ignore
VERSION_CODENAME: .ignore
bin/.gitignore: .ignore
bin/build-src-distrib.sh: .ignore
bin/build-src-distrib.sh: CEA_LGPL
bin/frama-c: CEA_LGPL
bin/frama-c-config: CEA_LGPL
bin/frama-c-script: CEA_LGPL
......@@ -66,13 +66,12 @@ doc/code/intro_sparecode.txt: CEA_LGPL
doc/code/style.css: CEA_LGPL
doc/code/toc_head.htm: CEA_LGPL
doc/code/toc_tail.htm: CEA_LGPL
headers/check-headers.sh: CEA_PROPRIETARY
headers/close-source/ACSL_EL: .ignore
headers/close-source/AORAI_LGPL: .ignore
headers/close-source/CEA_INRIA_LGPL: .ignore
headers/close-source/CEA_LGPL: .ignore
headers/close-source/CEA_LGPL_OR_PROPRIETARY: .ignore
headers/close-source/CEA_PROPRIETARY: .ignore
headers/close-source/CEA_PR_LGPL: .ignore
headers/close-source/CEA_WP: .ignore
headers/close-source/CIL: .ignore
headers/close-source/INRIA_BSD: .ignore
......@@ -83,15 +82,14 @@ headers/close-source/MODIFIED_OCAMLGRAPH: .ignore
headers/close-source/MODIFIED_WHY3: .ignore
headers/close-source/OCAML_STDLIB: .ignore
headers/close-source/UNMODIFIED_WHY3: .ignore
headers/headache.sh: CEA_PROPRIETARY
headers/headache_config.txt: .ignore
headers/headache_config.txt: CEA_LGPL
headers/header_spec.txt: .ignore
headers/open-source/ACSL_EL: .ignore
headers/open-source/AORAI_LGPL: .ignore
headers/open-source/CEA_INRIA_LGPL: .ignore
headers/open-source/CEA_LGPL: .ignore
headers/open-source/CEA_LGPL_OR_PROPRIETARY: .ignore
headers/open-source/CEA_PROPRIETARY: .ignore
headers/open-source/CEA_PR_LGPL: .ignore
headers/open-source/CEA_WP: .ignore
headers/open-source/CIL: .ignore
headers/open-source/INRIA_BSD: .ignore
......@@ -102,7 +100,6 @@ headers/open-source/MODIFIED_OCAMLGRAPH: .ignore
headers/open-source/MODIFIED_WHY3: .ignore
headers/open-source/OCAML_STDLIB: .ignore
headers/open-source/UNMODIFIED_WHY3: .ignore
headers/updates-headers.sh: CEA_PROPRIETARY
lib/plugins/PLUGINS.README: .ignore
licenses/CDDL-1.0: .ignore
licenses/LGPLv2: .ignore
......@@ -118,35 +115,35 @@ share/analysis-scripts/analysis.mk: CEA_LGPL
share/analysis-scripts/benchmark_database.py: CEA_LGPL
share/analysis-scripts/build.py: CEA_LGPL
share/analysis-scripts/build_callgraph.py: CEA_LGPL
share/analysis-scripts/clone.sh: .ignore
share/analysis-scripts/clone.sh: CEA_LGPL
share/analysis-scripts/creduce.sh: CEA_LGPL
share/analysis-scripts/detect_recursion.py: CEA_LGPL
share/analysis-scripts/epilogue.mk: CEA_LGPL
share/analysis-scripts/estimate_difficulty.py: CEA_LGPL
share/analysis-scripts/fc_stubs.c: .ignore
share/analysis-scripts/fc_stubs.c: CEA_LGPL
share/analysis-scripts/frama_c_results.py: CEA_LGPL
share/analysis-scripts/cmd-dep.sh: .ignore
share/analysis-scripts/concat-csv.sh: .ignore
share/analysis-scripts/cmd-dep.sh: CEA_LGPL
share/analysis-scripts/concat-csv.sh: CEA_LGPL
share/analysis-scripts/find_fun.py: CEA_LGPL
share/analysis-scripts/flamegraph.pl: CDDL
share/analysis-scripts/function_finder.py: .ignore
share/analysis-scripts/function_finder.py: CEA_LGPL
share/analysis-scripts/git_utils.py: CEA_LGPL
share/analysis-scripts/heuristic_list_functions.py: CEA_LGPL
share/analysis-scripts/list_files.py: CEA_LGPL
share/analysis-scripts/list_functions.ml: CEA_LGPL
share/analysis-scripts/make_wrapper.py: CEA_LGPL
share/analysis-scripts/normalize_jcdb.py: CEA_LGPL
share/analysis-scripts/parse-coverage.sh: .ignore
share/analysis-scripts/parse-coverage.sh: CEA_LGPL
share/analysis-scripts/print_callgraph.py: CEA_LGPL
share/analysis-scripts/prologue.mk: CEA_LGPL
share/analysis-scripts/pyproject.toml: .ignore
share/analysis-scripts/README.md: .ignore
share/analysis-scripts/results_display.py: CEA_LGPL
share/analysis-scripts/script_for_creduce_fatal.sh: .ignore
share/analysis-scripts/script_for_creduce_non_fatal.sh: .ignore
share/analysis-scripts/script_for_creduce_fatal.sh: CEA_LGPL
share/analysis-scripts/script_for_creduce_non_fatal.sh: CEA_LGPL
share/analysis-scripts/source_filter.py: CEA_LGPL
share/analysis-scripts/summary.py: CEA_LGPL
share/analysis-scripts/template.mk: .ignore
share/analysis-scripts/template.mk: CEA_LGPL
share/compliance/c11_functions.json: .ignore
share/compliance/c11_headers.json: .ignore
share/compliance/compiler_builtins.json: .ignore
......@@ -165,7 +162,7 @@ share/Makefile.generic: CEA_LGPL
share/Makefile.plugin.template: CEA_LGPL
share/META.frama-c: .ignore
share/configure.ac: CEA_LGPL
share/emacs/acsl.el: ACSL_EL
share/emacs/acsl.el: CEA_PR_LGPL
share/emacs/frama-c-dev.el: CEA_LGPL
share/emacs/frama-c-init.el: CEA_LGPL
share/emacs/frama-c-recommended.el: CEA_LGPL
......@@ -987,24 +984,24 @@ src/plugins/loop_analysis/region_analysis_stmt.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/region_analysis_stmt.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/register.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/configure.ac: CEA_LGPL
src/plugins/markdown-report/eva_info.ml: CEA_LGPL
src/plugins/markdown-report/eva_info.mli: CEA_LGPL
src/plugins/markdown-report/Makefile.in: CEA_LGPL
src/plugins/markdown-report/configure.ac: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/eva_info.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/eva_info.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/Makefile.in: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/META.in: .ignore
src/plugins/markdown-report/md_gen.ml: CEA_LGPL
src/plugins/markdown-report/md_gen.mli: CEA_LGPL
src/plugins/markdown-report/mdr_params.ml: CEA_LGPL
src/plugins/markdown-report/mdr_params.mli: CEA_LGPL
src/plugins/markdown-report/mdr_register.ml: CEA_LGPL
src/plugins/markdown-report/mdr_register.mli: CEA_LGPL
src/plugins/markdown-report/parse_remarks.ml: CEA_LGPL
src/plugins/markdown-report/parse_remarks.mli: CEA_LGPL
src/plugins/markdown-report/sarif_gen.ml: CEA_LGPL
src/plugins/markdown-report/sarif_gen.mli: CEA_LGPL
src/plugins/markdown-report/sarif.ml: CEA_LGPL
src/plugins/markdown-report/sarif.mli: CEA_LGPL
src/plugins/markdown-report/share/acsl.xml: CEA_LGPL
src/plugins/markdown-report/md_gen.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/md_gen.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/mdr_params.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/mdr_params.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/mdr_register.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/mdr_register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/parse_remarks.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/parse_remarks.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/sarif_gen.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/sarif_gen.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/sarif.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/sarif.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/share/acsl.xml: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/Metrics.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/css_html.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/css_html.mli: CEA_LGPL_OR_PROPRIETARY
......@@ -1120,13 +1117,13 @@ src/plugins/postdominators/postdominators_parameters.mli: CEA_LGPL_OR_PROPRIETAR
src/plugins/postdominators/print.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/postdominators/print.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/print_api/.gitignore: .ignore
src/plugins/print_api/Makefile: CEA_LGPL
src/plugins/print_api/Print_api.mli: CEA_LGPL
src/plugins/print_api/grammar.mly: CEA_LGPL
src/plugins/print_api/lexer.mll: CEA_LGPL
src/plugins/print_api/lexer.mli: CEA_LGPL
src/plugins/print_api/print_interface.ml: CEA_LGPL
src/plugins/print_api/print_interface.mli: CEA_LGPL
src/plugins/print_api/Makefile: CEA_LGPL_OR_PROPRIETARY
src/plugins/print_api/Print_api.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/print_api/grammar.mly: CEA_LGPL_OR_PROPRIETARY
src/plugins/print_api/lexer.mll: CEA_LGPL_OR_PROPRIETARY
src/plugins/print_api/lexer.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/print_api/print_interface.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/print_api/print_interface.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/qed/.gitignore: .ignore
src/plugins/qed/Makefile: CEA_WP
src/plugins/qed/bvars.ml: CEA_WP
......@@ -1335,15 +1332,15 @@ src/plugins/value/alarmset.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/alarmset.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/eval.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/eval.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/gen-api.sh: .ignore
src/plugins/value/gen-api.sh: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/parameters.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/parameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/register.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/self.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/self.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/test.assert.sh: .ignore
src/plugins/value/test.sh: .ignore
src/plugins/value/test.assert.sh: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/test.sh: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/general_requests.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/general_requests.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/values_request.ml: CEA_LGPL_OR_PROPRIETARY
......@@ -1844,14 +1841,14 @@ src/plugins/wp/ctypes.ml: CEA_WP
src/plugins/wp/ctypes.mli: CEA_WP
src/plugins/wp/filter_axioms.ml: CEA_WP
src/plugins/wp/filter_axioms.mli: CEA_WP
src/plugins/wp/doc/MakeDoc: .ignore
src/plugins/wp/doc/coqdoc/Makefile: .ignore
src/plugins/wp/doc/MakeDoc: CEA_WP
src/plugins/wp/doc/coqdoc/Makefile: CEA_WP
src/plugins/wp/doc/coqdoc/coqdoc.sty: .ignore
src/plugins/wp/doc/coqdoc/qed_generated.tex: .ignore
src/plugins/wp/doc/coqdoc/typed_generated.tex: .ignore
src/plugins/wp/doc/coqdoc/wpcoq.tex: .ignore
src/plugins/wp/doc/manual/.gitignore: .ignore
src/plugins/wp/doc/manual/Makefile: .ignore
src/plugins/wp/doc/manual/Makefile: CEA_WP
src/plugins/wp/doc/manual/mem.pdf: .ignore
src/plugins/wp/doc/manual/size_base.pdf: .ignore
src/plugins/wp/doc/manual/size_compl.pdf: .ignore
......
headers/open-source/ACSL_EL → headers/open-source/CEA_PR_LGPL
+ 0
− 0
View file @ 00ab300d
File moved
headers/open-source/XL_COMPCERT 0 → 100644
+ 10
− 0
View file @ 00ab300d
The Compcert verified compiler
Xavier Leroy, INRIA Paris-Rocquencourt
Copyright Institut National de Recherche en Informatique et en
Automatique. All rights reserved. This file is distributed
under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 2 of the License, or
(at your option) any later version. This file is also distributed
under the terms of the INRIA Non-Commercial License Agreement.
headers/updates-headers.sh deleted 100755 → 0
+ 0
− 152
View file @ 506e66c5
#!/bin/sh
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# All rights reserved. #
# Contact CEA LIST for licensing. #
# #
##########################################################################
APPLINAME="$0"
HEADACHE=$(dirname $APPLINAME)/headache.sh
Usage() {
APPLI=$(basename $APPLINAME)
echo "Usage: $APPLI <option>* <headers-spec> <header-dir> [<target-dir>] [<headache-config>]"
echo " <option>"
echo " --dry-run: shows the commands to perform without any file modification"
echo " --max-procs <N>: runs up to <N> jobs in parallel."
echo " --parallel: uses 'parallel' software instead of 'xargs'"
echo " <target-dir>: root pathname to the files to modify"
echo " default to ."
echo " <header-dir>: directory that should contents header files"
echo " <headache-config>: headache config file"
echo " default to ./headers"
echo " <headers-spec>: defines header files to apply on files".
echo " The format of <headers-spec> file is checked before doing anything."
echo " Syntax:"
echo " <line format>= <header-file> ':' <file-to-modify> '\n'"
echo " | '.ignore' ':' <ignored-file> '\n'"
echo " | '#' <comment-line> '\n'"
echo " | [':'] '\n'"
echo " Ignored files are not modified by the script ${APPLI}."
exit 1
}
Requires () {
# Looking for executables
for File in "$@" ; do
where=$(which $File)
if [ "$?" != "0" ] ; then
echo "Error: executable not found: $File"
exit 1
fi
done
}
SetVariables() {
FILE=$1
HEADER_SRC=$2
TARGET_DIR=${3-.}
HEADACHE_CONFIG=${4-./headers/headache_config.txt}
if [ "$5" != "" ] ; then
echo "Error: too much arguments."
exit 1
fi
if [ "${MAX_PROCS}" = "" ] && [ -f /proc/cpuinfo ] ; then
# Linux system
MAX_PROCS=$(cat /proc/cpuinfo | grep -c processor)
fi
if [ "${MAX_PROCS}" = "0" ] || [ "${MAX_PROCS}" = "" ] ; then
MAX_PROCS=""
else
MAX_PROCS="-P ${MAX_PROCS}"
fi
}
CheckingVariables () {
if [ "${FILE}" = "" ] ; then
echo "Error: missing header specification file."
exit 1
fi
if [ ! -f "${FILE}" ] ; then
echo "Error: header specification file not found: ${FILE}"
exit 1
fi
if [ "${HEADER_SRC}" = "" ] ; then
echo "Error: missing header directory."
exit 1
fi
if [ ! -d "${HEADER_SRC}" ] ; then
echo "Error: header directory not found: ${HEADER_SRC}/"
exit 1
fi
if [ ! -d "${TARGET_DIR}" ] ; then
echo "Error: target directory not found: ${TARGET_DIR}"
exit 1
fi
if [ ! -f "${HEADACHE_CONFIG}" ] ; then
echo "Error: headache config file not found: ${HEADACHE_CONFIG}"
exit 1
fi
}
PROCESS=""
MAX_PROCS=""
PARALLEL=""
REQUIREMENTS="xargs"
while [ "$1" != "" ] ; do
case "$1" in
-h) Usage;;
-help) Usage;;
--help) Usage;;
--max-procs) shift; MAX_PROCS="$1";;
--dry-run) PROCESS="echo";;
--parallel) PARALLEL="parallel"; REQUIREMENTS="${PARALLEL}";;
*) break;;
esac
shift
done
Requires ${HEADACHE} gawk grep tr ${REQUIREMENTS}
SetVariables $@
CheckingVariables
# Checking the format of the input file and extract line number of the error.
grep -v "^#" ${FILE} | \
gawk -F ":" '$1=="" || $1~/[^ ] [^ ]/ || $2==""|| $2~/[^ ] [^ ]/ || $3!="" { print "'${FILE}:'" NR ": " $0 ; exit 2 }'
if [ "$?" != "0" ] ; then
echo "Error: wrong line format."
echo "So, nothing is modified."
exit 1
fi
# Ok, go on.
if [ "${PARALLEL}" != "" ] ; then
# 'parallel' considers the full line as one argument, so
# 'tr' is used to split the line in two and empty line have to be removed.
grep -v "^#" $1 \
| grep -v "\.ignore$" \
| tr -s ":[:blank:]" "\n" | grep -v '^$' \
| ${PARALLEL} -n 2 ${MAX_PROCS} ${PROCESS} ${HEADACHE} -c ${HEADACHE_CONFIG} -h ${HEADER_SRC}/{2} ${TARGET_DIR}/{1}
else
# 'xargs' has no support for context replace, so 'gawk" is used to create the arguments.
grep -v "^#" $1 \
| grep -v "\.ignore$" \
| tr -s ":[:blank:]" " " | grep -v '^ *$' \
| gawk '{ print "'${HEADER_SRC}'/" $2 " '${TARGET_DIR}'/" $1 }' \
| xargs -n 2 ${MAX_PROCS} ${PROCESS} ${HEADACHE} -c ${HEADACHE_CONFIG} -h
fi
ivette/.gitattributes 0 → 100644
+ 25
− 0
View file @ 00ab300d
########################
# HEADER_SPEC: .ignore #
########################
/configure.js header_spec=.ignore
/sandboxer.js header_spec=.ignore
/.babelrc header_spec=.ignore
/.eslint* header_spec=.ignore
/doc/**/*.js header_spec=.ignore
/dome/doc/**/*.js header_spec=.ignore
/src/dome/doc/template/static/fonts/*-webfont.* header_spec=.ignore
/src/dome/template/git-ignore header_spec=.ignore
/src/dome/doc/template/tmpl/*.tmpl header_spec=.ignore
/src/dome/doc/**/*.js header_spec=.ignore
/src/dome/doc/**/*.htm header_spec=.ignore
/src/dome/doc/**/*.txt header_spec=.ignore
/src/dome/**/*.el header_spec=.ignore
/tests/*.i header_spec=.ignore
/**/*.css header_spec=.ignore
/**/*.html header_spec=.ignore
/**/*.json header_spec=.ignore
/**/*.lua header_spec=.ignore
/*.icns header_spec=.ignore
/*.lock header_spec=.ignore
ivette/Makefile.distrib
+ 22
− 0
View file @ 00ab300d
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# 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). #
# #
##########################################################################
HEADER_SPEC += ivette/./headers/header_spec.txt
DISTRIB_FILES += ivette/.babelrc
DISTRIB_FILES += ivette/.dome-pkg-app.lock
......
ivette/distrib.sh
+ 22
− 0
View file @ 00ab300d
#!/bin/sh -e
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# 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). #
# #
##########################################################################
# --------------------------------------------------------------------------
# --- Generate Files for Ivette Distribution
# --------------------------------------------------------------------------
......
ivette/headers/header_spec.txt
+ 12
− 12
View file @ 00ab300d
......@@ -9,13 +9,13 @@ INSTALL.md: .ignore
Makefile: CEA_LGPL
README.md: .ignore
configure.js: .ignore
distrib.sh: .ignore
distrib.sh: CEA_LGPL
doc/pandoc/href.lua: .ignore
doc/pandoc/index.json: .ignore
doc/pandoc/template.html: .ignore
electron-builder.json: .ignore
electron-webpack.json: .ignore
ivette-macos.sh: .ignore
ivette-macos.sh: CEA_LGPL
package.json: .ignore
sandboxer.js: .ignore
src/dome/.gitignore: .ignore
......@@ -130,19 +130,19 @@ src/dome/renderer/themes.tsx: CEA_LGPL
src/dome/template/Application.js: CEA_LGPL
src/dome/template/Preferences.js: CEA_LGPL
src/dome/template/babelrc.json: .ignore
src/dome/template/dome-pull.sh: .ignore
src/dome/template/dome-push.sh: .ignore
src/dome/template/dome-pull.sh: CEA_LGPL
src/dome/template/dome-push.sh: CEA_LGPL
src/dome/template/electron-webpack.json: .ignore
src/dome/template/export.sh: .ignore
src/dome/template/export.sh: CEA_LGPL
src/dome/template/git-ignore: .ignore
src/dome/template/main.js: CEA_LGPL
src/dome/template/makefile: .ignore
src/dome/template/makefile.app.packages: .ignore
src/dome/template/makefile.packages: .ignore
src/dome/template/package.sh: .ignore
src/dome/template/makefile: CEA_LGPL
src/dome/template/makefile.app.packages: CEA_LGPL
src/dome/template/makefile.packages: CEA_LGPL
src/dome/template/package.sh: CEA_LGPL
src/dome/template/renderer.js: CEA_LGPL
src/dome/template/typescript.el: .ignore
src/dome/template/update.sh: .ignore
src/dome/template/update.sh: CEA_LGPL
src/dome/template/webpack.main.js: CEA_LGPL
src/dome/template/webpack.renderer.js: CEA_LGPL
src/frama-c/api_generator.ml: CEA_LGPL
......@@ -209,6 +209,6 @@ tests/eva-1.i: .ignore
tests/eva-2.i: .ignore
tsconfig.json: .ignore
tsfmt.json: .ignore
webpack.main.js: .ignore
webpack.renderer.js: .ignore
webpack.main.js: CEA_LGPL
webpack.renderer.js: CEA_LGPL
yarn.lock: .ignore
ivette/ivette-macos.sh
+ 21
− 0
View file @ 00ab300d
#!/bin/zsh
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# 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). #
# #
##########################################################################
exec open -na /Applications/Ivette.app --args --working $PWD $*
ivette/src/dome/template/dome-pull.sh
+ 22
− 0
View file @ 00ab300d
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# 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). #
# #
##########################################################################
# --------------------------------------------------------------------------
# --- Pulling Dome Updates
# --------------------------------------------------------------------------
......
ivette/src/dome/template/dome-push.sh
+ 22
− 0
View file @ 00ab300d
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# 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). #
# #
##########################################################################
# --------------------------------------------------------------------------
# --- Pulling Dome Updates
# --------------------------------------------------------------------------
......
ivette/src/dome/template/export.sh
+ 21
− 0
View file @ 00ab300d
#!/bin/bash
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# 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). #
# #
##########################################################################
# --------------------------------------------------------------------------
# --- Export Dome API
......
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