diff --git a/.gitattributes b/.gitattributes
index 05c7469486844c9223482b05ded245e68a95d361..91434116d050a224e0f676a68ea47b63279057e0 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -5,36 +5,70 @@
.git-blame-ignore-revs merge=union
Changelog merge=union
-###############
-# BINARY: set #
-###############
-# built-in macro that also unsets the "text" and "diff" attributes
+##################################################
+# BINARY/CHECK-SYNTAX/INDENT/EOL-EOF: set/-unset #
+##################################################
-*.ico binary -check-eoleof
-*.icns binary -check-eoleof
+# note: "binary" is a built-in macro that also
+# unsets the "text" and "diff" attributes
-*.eps binary -check-eoleof
-*.ps binary -check-eoleof
-*.gif binary -check-eoleof
-*.jpg binary -check-eoleof
-*.png binary -check-eoleof
-*.svg binary -check-eoleof
+# note: set "check-eoleof" and "check-utf8" by default to all files
+* check-eoleof check-utf8
-*.odg binary -check-eoleof
-*.pdf binary -check-eoleof
+# note: unset "-check-eoleof" and "-check-utf8" for "binary"
+*.ico binary -check-eoleof -check-utf8
+*.icns binary -check-eoleof -check-utf8
-*.eot binary -check-eoleof
-*.woff binary -check-eoleof
+*.eps binary -check-eoleof -check-utf8
+*.ps binary -check-eoleof -check-utf8
+*.gif binary -check-eoleof -check-utf8
+*.jpg binary -check-eoleof -check-utf8
+*.png binary -check-eoleof -check-utf8
+*.svg binary -check-eoleof -check-utf8
+
+*.odg binary -check-eoleof -check-utf8
+*.pdf binary -check-eoleof -check-utf8
+
+*.eot binary -check-eoleof -check-utf8
+*.woff binary -check-eoleof -check-utf8
###########################################
# CHECK-SYNTAX/INDENT/EOL-EOF: set/-unset #
###########################################
+## Set "check-syntax" and "check-indent"
+
+# note: "check-syntax" includes already "check-eoleof"
*.ml check-syntax check-indent -check-eoleof
*.mli check-syntax check-indent -check-eoleof
+## Unset "-check-eoleof"
+
+*.dot -check-eoleof
+
+/tests/spec/unfinished-oneline-acsl-comment.i -check-eoleof
/doc/developer/check_api/run.oracle -check-eoleof
+## Unset "-check-utf8"
+
+/doc/training/developer/macros.tex -check-utf8
+
+/src/plugins/wp/doc/coqdoc/coqdoc.sty -check-utf8
+/src/plugins/wp/doc/manual/wp_logicvar.tex -check-utf8
+/src/plugins/wp/doc/manual/wp_store.tex -check-utf8
+
+# Don't check symbolic links (that gives an error)
+
+## Unset all: "-check-syntax -check-indent -check-eoleof -check-utf8"
+
+# Don't check symbolic links (that gives an error for check-utf8). Please checks only the linked target.
+/src/plugins/e-acsl/tests/builtin/utils -check-syntax -check-indent -check-eoleof -check-utf8
+/src/plugins/e-acsl/tests/format/utils -check-syntax -check-indent -check-eoleof -check-utf8
+
+# File names that cannot be checked (due to sh: 1: Syntax error: Unterminated quoted string)
+/tests/syntax/foo\".c -check-syntax -check-indent -check-eoleof -check-utf8
+/tests/syntax/oracle/foo\".res.oracle -check-syntax -check-indent -check-eoleof -check-utf8
+
#########################
# HEADER_SPEC: CEA_LGPL #
#########################
diff --git a/.gitignore b/.gitignore
index ebba842a7fe2aaac5df6d5b5400e80dd4d74b097..cb2bdbdfb9740ffd81853e6294b477ee066c4b99 100644
--- a/.gitignore
+++ b/.gitignore
@@ -61,8 +61,6 @@ autom4te.cache
/devel_tools/fc-time
/devel_tools/fc-memuse
/bin/ocamldep_transitive_closure
-/bin/isutf8
-/bin/isutf8.exe
#share
/share/Makefile.config
diff --git a/bin/isutf8.ml b/bin/isutf8.ml
deleted file mode 100644
index 0e775f13502710afea395fa9aadb2686ca72b40d..0000000000000000000000000000000000000000
--- a/bin/isutf8.ml
+++ /dev/null
@@ -1,97 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-module StringSet = Set.Make(String)
-
-exception False
-
-let is_valid_utf8 filename =
- let buf = Bytes.create 1024 in
- try
- let ic = open_in_bin filename in
- let extra = ref 0 in
- try
- while true do
- let n_bytes_read = input ic buf 0 1024 in
- if n_bytes_read = 0 then raise End_of_file;
- for i = 0 to n_bytes_read - 1 do
- let c = Bytes.get_uint8 buf i in
- (*Format.printf "extra: %d, read byte: %d (0x%x, char %c)@."
- !extra c c (Char.chr c);*)
- if !extra > 0 then begin
- decr extra;
- if c lsr 6 <> 2 then raise False
- end
- else
- if c > 127 then begin
- if c lsr 5 = 6 then extra := 1
- else if c lsr 4 = 14 then extra := 2
- else if c lsr 3 = 30 then extra := 3
- else raise False
- end;
- done;
- done;
- close_in ic;
- !extra = 0
- with
- | End_of_file ->
- close_in ic;
- !extra = 0
- | False ->
- close_in ic;
- false
- with
- | Sys_error msg ->
- (* possibly a non-existing file (e.g. with spaces); ignoring *)
- Format.printf "isutf8: cannot open, ignoring file: %s (%s)@."
- filename msg;
- true
-
-(* usage: first argument is a file name containing a list of files
- (one per line) to be checked; the remaining arguments are filenames
- to be ignored during checking. *)
-let () =
- if Array.length Sys.argv < 2 then begin
- Format.printf "usage: %s file_list.txt [ignore1 ignore2 ...]@." Sys.argv.(0);
- exit 0
- end;
- let errors = ref 0 in
- let file_list_ic = open_in Sys.argv.(1) in
- let to_ignore = StringSet.of_list (List.tl (Array.to_list Sys.argv)) in
- begin
- try
- while true; do
- let filename = input_line file_list_ic in
- if not (StringSet.mem filename to_ignore)
- && not (is_valid_utf8 filename) then begin
- incr errors;
- Format.printf "error: invalid UTF-8 in file: %s@." filename
- end
- done
- with End_of_file ->
- close_in file_list_ic
- end;
- if !errors > 0 then begin
- Format.printf "Found %d file(s) with errors.@." !errors;
- exit 1
- end else
- exit 0
diff --git a/doc/acsl_tutorial_slides/script b/doc/acsl_tutorial_slides/script
index 9ae7ac14fc9a221bdd569e7ab72818de6fcb03ee..cdc4a4df21dc4e088a7a06f8887812c150d8d51d 100644
--- a/doc/acsl_tutorial_slides/script
+++ b/doc/acsl_tutorial_slides/script
@@ -1,18 +1,18 @@
-* Faire un slide 0 avec le nom de celui qui présente et
+* Faire un slide 0 avec le nom de celui qui présente et
l'URL pour Frama-C. Faire le discours sur ACSL qui est la
-glue faisant marcher plusieurs plug-ins complémentaires.
+glue faisant marcher plusieurs plug-ins complémentaires.
* slide 1max.c
-montrer que l'on peut déjà vérifier la syntaxe des annotation
+montrer que l'on peut déjà vérifier la syntaxe des annotation
en introduisant une erreur de syntaxe et en compilant depuis Emacs.
Localiser l'erreur avec Emacs.
-Alors que l'idée des prés et posts est de prouver que la post tient
-en n'utilisant que le code de la fonction en supposant que la pré
-était satisfaite en entrée, la deuxième page montre l'utilisation
-de l'analyse de valeurs pour vérifier ces propriétés avec une
-exécution symbolique.
+Alors que l'idée des prés et posts est de prouver que la post tient
+en n'utilisant que le code de la fonction en supposant que la pré
+était satisfaite en entrée, la deuxième page montre l'utilisation
+de l'analyse de valeurs pour vérifier ces propriétés avec une
+exécution symbolique.
* slide 2maxp.c
@@ -23,29 +23,29 @@ C'est pour montrer que ACSL supporte les pointeurs.
Avertissements sur le fait que le langage logique est
un langage pur.
Le && est commutatif. Parler de (*p) n'a pas de sens en
-général mais des propriétés telles que *p==*p sont
-vraies même si p n'est pas valide. Mieux vaut
-toujours écrire "\valid(p) && *p == ..."
+général mais des propriétés telles que *p==*p sont
+vraies même si p n'est pas valide. Mieux vaut
+toujours écrire "\valid(p) && *p == ..."
* slide 4comp_part.c
-Attirer l'attention sur ce que c'est une spécification
-complète. Insister sur le fait que c'est très difficile
-d'en écrire en pratique (formelles ou non formelles) mais
-que les spécifications partielles sont utiles aussi
+Attirer l'attention sur ce que c'est une spécification
+complète. Insister sur le fait que c'est très difficile
+d'en écrire en pratique (formelles ou non formelles) mais
+que les spécifications partielles sont utiles aussi
(et qu'on peut se servir d'ACSL pour en faire).
* slide 5assigns_term.c
-A propos de spécifications complètes, c'est le bon moment
+A propos de spécifications complètes, c'est le bon moment
pour parler des assigns et de la terminaison.
* slide 6pred.c
-Les spécifications peuvent devenir plus élaborée en
-commençant par définir des prédicats utilisateurs.
-Ici, défini comme une fonction
+Les spécifications peuvent devenir plus élaborée en
+commençant par définir des prédicats utilisateurs.
+Ici, défini comme une fonction
* slide 7pred.c
-Définition dans le style prolog du même prédicat.
+Définition dans le style prolog du même prédicat.
diff --git a/doc/developer/METADOC.txt b/doc/developer/METADOC.txt
index 229eedcfa07ba3b040e5d870fbc39729d26d2224..e17f478eed5b7fead89092dcdbd419fd6f54e0f8 100644
--- a/doc/developer/METADOC.txt
+++ b/doc/developer/METADOC.txt
@@ -1,25 +1,25 @@
=========================================================================
-Ce fichier contient les règles à suivre pour écrire la doc du développeur
+Ce fichier contient les règles à suivre pour écrire la doc du développeur
=========================================================================
-* Les instructions de "doc/www/src/metadoc.NE_PAS_ECRIRE" doivent être
- appliquées.
+* Les instructions de "doc/www/src/metadoc.NE_PAS_ECRIRE" doivent être
+ appliquées.
* Les fichiers portent l'extension .pretex pour permettre leur preprocessing
-* L'index doit être tenu à jour
+* L'index doit être tenu à jour
-* Les redondances dans l'index (deux entrées différentes correspondant à la
- même chose) ne sont autorisées seulement si une des deux entrées référence
- proprement l'autre à l'aide d'un tag "see".
+* Les redondances dans l'index (deux entrées différentes correspondant à la
+ même chose) ne sont autorisées seulement si une des deux entrées référence
+ proprement l'autre à l'aide d'un tag "see".
-* L'annexe "Changes" doit être tenue à jour.
+* L'annexe "Changes" doit être tenue à jour.
-* Les macros doivent être définies dans macros.tex
+* Les macros doivent être définies dans macros.tex
-* Les macros doivent être au maximum utilisées.
+* Les macros doivent être au maximum utilisées.
En particulier:
- o les environnements dérivés de "code" pour le code
+ o les environnements dérivés de "code" pour le code
- autoconfcode pour les configure.in
- makecode pour les makefile
- ccode pour le C
@@ -27,10 +27,10 @@ Ce fichier contient les r
- code pour les autres codes (ligne de commandes par exemple)
o l'environnement "example" pour les exemples
o l'environnement "important" pour les choses importantes
- o l'environnement "convention" pour les conventions qu'un développeur doit
+ o l'environnement "convention" pour les conventions qu'un développeur doit
respecter
- o l'environnement "prereq" pour les prérequis nécessaires à la bonne
- compréhension
- o les macros pour les noms de langage/d'outils (c'est la même macro
- \langage à l'origine)
- o les macros pour les entrées d'index
+ o l'environnement "prereq" pour les prérequis nécessaires à la bonne
+ compréhension
+ o les macros pour les noms de langage/d'outils (c'est la même macro
+ \langage à l'origine)
+ o les macros pour les entrées d'index
diff --git a/doc/developer/TODO b/doc/developer/TODO
index b0d6d62fa4cd6003f481eaa747e38b6542c4ffac..489e0e1eebfc19d2b2b4009d7afda72c794fead4 100644
--- a/doc/developer/TODO
+++ b/doc/developer/TODO
@@ -18,26 +18,26 @@ Advance
[advanced plugin development]
o lien avec les exemples de chargement dynamique
[refman]
- o spécification du module "Type" dans répertoire "lib":
- ajouté un lien vers Section "Journalisation" quand cette
- dernière sera écrite.
+ o spécification du module "Type" dans répertoire "lib":
+ ajouté un lien vers Section "Journalisation" quand cette
+ dernière sera écrite.
* Documentation des sources:
- o test d'intégrité du code wrt plugin dev guide
+ o test d'intégrité du code wrt plugin dev guide
* GUI:
- o améliorer la doc: mieux expliquer comment utiliser les hooks pour coder
- les parties similaires à chaque greffon (panneau latéral, etc).
+ o améliorer la doc: mieux expliquer comment utiliser les hooks pour coder
+ les parties similaires à chaque greffon (panneau latéral, etc).
o GUI des greffons dynamiques
Refman
======
* Figure des makefiles:
- o ajouter le fait que Makefile.dynamic est généré à partir de
+ o ajouter le fait que Makefile.dynamic est généré à partir de
Makefile.dynamic.internal/external
-* Makefile.dynamic: ce qui lui est spécifique
+* Makefile.dynamic: ce qui lui est spécifique
List of recommendations (?)
=======================
diff --git a/doc/index.html b/doc/index.html
index 961f99ad1f9635f02b6a19a1fc852f072d334592..67520447c419c95d4faca4fc20d469b793d83318 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -4,7 +4,7 @@ PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
<html>
<head>
-<meta http-equiv="Content-Type" content="text/xhtml; charset=ISO-8859-1"/>
+<meta http-equiv="Content-Type" content="text/xhtml; charset=utf-8"/>
<link rel="stylesheet" href="style.css" type="text/css"/>
<title>Frama-C</title>
</head>
@@ -125,7 +125,7 @@ PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
(<a href="wp/Spec/index.html">spec</a> : <tt>cd wp/Spec; make</tt>)
(<a href="wp/Notes/index.html">informal notes</a> : <tt>cd wp/Notes; make</tt>)
(<a href="wp/Implem/index.html">implementation</a> : <tt>cd wp/Implem; make</tt>)
- (<a href="wp/Coq/doc/toc.html">modélisation COQ</a>)
+ (<a href="wp/Coq/doc/toc.html">modélisation COQ</a>)
(<a href="code/wp/metrics.html">metrics</a> : <tt>make Wp_metrics)</tt>)
</li><li>
<a href="code/cxx_elsa/index.html">cxx</a>
diff --git a/doc/makeLatex b/doc/makeLatex
index c0414b80e350006f150b066e500f4afddf609f94..abcd85df97cf381080aa0ecbcea9b005930f6174 100644
--- a/doc/makeLatex
+++ b/doc/makeLatex
@@ -1,22 +1,22 @@
-# Fichier à inclure dans son makefile pour faire des compilation latex.
-# L'utilisateur doit définir certaines variables (notées +)
-# et peut en option en (re)définir d'autres (notées *) :
+# Fichier à inclure dans son makefile pour faire des compilation latex.
+# L'utilisateur doit définir certaines variables (notées +)
+# et peut en option en (re)définir d'autres (notées *) :
#
-# === outils (peuvent être redéfinis si on veut préciser le path par exemple) :
+# === outils (peuvent être redéfinis si on veut préciser le path par exemple) :
# TEXI (= texi2dvi)
# HEVEA (HEVEAOPTS), HACHA
# === fichiers :
-# * TOPTEX=top.tex : déterminé par défaut par un grep de documentclass
-# * GENERATED_TEX= : fichiers .tex générés (vide par défaut)
+# * TOPTEX=top.tex : déterminé par défaut par un grep de documentclass
+# * GENERATED_TEX= : fichiers .tex générés (vide par défaut)
#
# * FIGURES_TODO= : noms de figures sans extension (-> .eps + .pdf)
# (suppose qu'on a le .eps et le .pdf
# ou qu'on sait a une cible pour les fabriquer...)
#
-# * HVA=macros.hva : si on a besoin de définir des choses pour hevea
+# * HVA=macros.hva : si on a besoin de définir des choses pour hevea
#
-# Les figures (fichiers .fig) sont compilés en postscript et/ou en pdf
+# Les figures (fichiers .fig) sont compilés en postscript et/ou en pdf
# en fonction des besoins. Si on souhaite compiler une figure en latex
# (formules, etc) il faut simplement nommer le fichier *.tex.fig
#
@@ -25,14 +25,14 @@
# debug_latex,
# clean_latex, clean_hevea, clean
#
-# loop : lance gv sur TOPTEX.ps et une boucle de compilation qui met à jour
-# le contenu visualisé.
-# Il est conseillé d'utiliser plutôt la cible 'sloop' pour ne pas avoir
-# un écran qui défile en permanence.
+# loop : lance gv sur TOPTEX.ps et une boucle de compilation qui met à jour
+# le contenu visualisé.
+# Il est conseillé d'utiliser plutôt la cible 'sloop' pour ne pas avoir
+# un écran qui défile en permanence.
#------------------------------------------------------------------------------
-# l'avantage de texi2dvi par rapport à latex,
+# l'avantage de texi2dvi par rapport à latex,
# c'est qu'il s'occupe de l'index, de la biblio,
# et de lancer latex autant de fois qu'il le faut.
TEXI?=texi2dvi
@@ -73,13 +73,13 @@ FIGURES_EPS = $(SIMPLE_FIGURES_EPS) $(FIGURES_PSTEX)
FIGURES_PDF = $(SIMPLE_FIGURES_PDF) $(FIGURES_PDFTEX)
GENERATED_FIGURES = $(FIGURES_EPS) $(FIGURES_PDF) $(FIGURES_TEX)
-# plus utile : hevea se débrouille tout seul.
+# plus utile : hevea se débrouille tout seul.
#IMAGES_GIF = $(shell grep -s gif $(SRC).html | grep "^[ ]*<IMG" | sed -e 's=[^"]*"\(.*.gif\).*=\1=')
-# TODO : à étendre au cas d'une biblio multiple (plusieurs fichiers .bib).
+# TODO : à étendre au cas d'une biblio multiple (plusieurs fichiers .bib).
BIB_NAME = $(shell grep -h "bibliography{" $(TOPTEX) \
| sed -e 's/\\bibliography{\(.*\)}/\1.bib/')
-# TODO: à modifier pour chercher dans BIBINPUTS
+# TODO: Ã modifier pour chercher dans BIBINPUTS
ifneq ($(strip $(BIB_NAME)),)
BIB_FILE = $(BIB_NAME)
@@ -115,7 +115,7 @@ debug_latex :
@echo "HVA = $(HVA)"
#------------------------------------------------------------------------------
-# Dépendances :
+# Dépendances :
$(SRC).dvi : $(ALL_TEX) $(FIGURES_TEX) $(FIGURES_EPS) $(BBL_FILE) $(FIGURES_PDF)
# no <TAB> here
@@ -129,7 +129,7 @@ $(SRC).html : $(ALL_TEX) $(SRC).pdf $(SRC).bbl
#------------------------------------------------------------------------------
# Regles de production :
-# dessins .eps à partir des .fig de xfig
+# dessins .eps à partir des .fig de xfig
%.eps : %.tex.fig
fig2dev -L pstex $< $@
@@ -160,7 +160,7 @@ $(SRC).html : $(ALL_TEX) $(SRC).pdf $(SRC).bbl
$(TEXI2DVI) $<
$(SRC).bbl : $(BIB_FILE)
- @echo "=== Fichier .bib plus récent -> effacement du .bbl"
+ @echo "=== Fichier .bib plus récent -> effacement du .bbl"
rm -f $(SRC).bbl
@@ -193,9 +193,9 @@ $(SRC).html: $(HVA) $(SRC).tex
index.html: $(SRC).html
$(HACHA) -o index.html $(SRC).html
-# ceci n'est normalement plus utile sous UNIX grace à l'option -fix de hevea
+# ceci n'est normalement plus utile sous UNIX grace à l'option -fix de hevea
#$(IMAGES_GIF) : $(SRC).image.tex
- #@echo "=== Génération des images gif"
+ #@echo "=== Génération des images gif"
#imagen $(SRC)
#------------------------------------------------------------------------------
@@ -228,14 +228,14 @@ sloop:
#------------------------------------------------------------------------------
clean_hevea :
- @echo "=== Ménage des fichiers hevea"
+ @echo "=== Ménage des fichiers hevea"
rm -f $(SRC).html $(SRC).h{toc,aux,ind,idx} $(SRC).cb
rm -f index.html $(SRC)[0-9][0-9][0-9].html $(SRC).css
rm -f $(SRC).image.cb $(SRC).image.tex $(SRC)[0-9][0-9][0-9].gif
rm -f previous_motif.gif next_motif.gif contents_motif.gif
clean_tmp_tex :
- @echo "=== Ménage des fichiers temporaires de latex"
+ @echo "=== Ménage des fichiers temporaires de latex"
rm -f $(SRC).aux
rm -f $(SRC).log
rm -f $(SRC).blg
@@ -249,12 +249,12 @@ clean_tmp_tex :
rm -f $(SRC).out
clean_latex : clean_tmp_tex
- @echo "=== Ménage des fichiers latex"
+ @echo "=== Ménage des fichiers latex"
rm -f $(SRC).bbl
rm -f $(SRC).dvi
rm -f $(SRC).ps
rm -f $(SRC).pdf
- @echo "=== Ménage des figures"
+ @echo "=== Ménage des figures"
rm -f *.~[0-9]*~ *.bak *~
rm -f $(GENERATED_FIGURES)
diff --git a/doc/scope/M.v b/doc/scope/M.v
index f9758e8a131b33ca06f9d75c757a8a3a0da352d3..f57ee83e7a37cf88dfeffbd9e2a7b290900979a4 100644
--- a/doc/scope/M.v
+++ b/doc/scope/M.v
@@ -175,7 +175,7 @@ Parameter ma : inst -> inst -> mark.
Axiom maStart : forall L I, ma L I = Start -> L = I.
Axiom maL : forall L, ma L L = Start.
-(** propriété du marquage après stabilité *)
+(** propriété du marquage après stabilité *)
Axiom Pma : forall L i',
ma L i' = lmerge (List.map (fun i => trans i (ma L i)) (pred i')).
diff --git a/doc/scope/Makefile b/doc/scope/Makefile
index ac55e30f1991ffdb38612fdfcb1ee248d6e01ce8..5f47605deb544a3fe1371695312c2207b21d11f3 100644
--- a/doc/scope/Makefile
+++ b/doc/scope/Makefile
@@ -20,7 +20,7 @@
# #
##########################################################################
-#vide : pour ne pas utiliser de règles implicites
+#vide : pour ne pas utiliser de règles implicites
.SUFFIXE:
.PHONY: clean all debug
diff --git a/doc/value/README b/doc/value/README
index 8c0abd89e17425eda471574f518ff91775e453d0..cf8e721bb34ecc977620a5554f410251bfe47912 100644
--- a/doc/value/README
+++ b/doc/value/README
@@ -1,13 +1,13 @@
-Si vous n'êtes pas un développeur de Value, vous avez
-reçu ce document par erreur, et vous pouvez l'ignorer.
+Si vous n'êtes pas un développeur de Value, vous avez
+reçu ce document par erreur, et vous pouvez l'ignorer.
Conventions s'appliquant dans la documentation de Value :
* Le "plug-in d'analyse de valeur" s'appelle "the value analysis plug-in",
"the plug-in", "the value analysis" ou "the analysis".
- Les deux derniers sont à utiliser quand le sujet de l'action
- peut être une analyse particulière d'un code particulier.
+ Les deux derniers sont à utiliser quand le sujet de l'action
+ peut être une analyse particulière d'un code particulier.
Utiliser "Frama-C" si et seulement si Frama-C est
l'interface visible pour l'action dont il est question, par exemple :
@@ -20,19 +20,19 @@ synthetic information on the behavior of analyzed functions:
inputs, outputs, and alarms.
* La personne qui utilise Value s'appelle "l'utilisateur" ;
-la personne qui a écrit l'application s'appelle "programmeur",
+la personne qui a écrit l'application s'appelle "programmeur",
mais on n'a pas souvent de raison de parler d'elle.
-* Sauf cas particulier, si un exemple contient le point d'entrée,
-alors ce point d'entrée s'appelle \verb|main|. Un exemple peut
+* Sauf cas particulier, si un exemple contient le point d'entrée,
+alors ce point d'entrée s'appelle \verb|main|. Un exemple peut
aussi ne pas contenir de fonction \verb|main|, ce qui indique
qu'il ne s'agit que d'une partie d'un projet plus grand.
-* Le shell n'est pas csh. Le shell peut être bash, zsh, le prompt
-peut avoir été customisé par l'utilisateur, ou l'utilisateur peut
-être sous Windows et avoir un prompt de la forme "C:\>". Donc,
-on n'écrit pas de prompt précédant les commandes à taper au
-prompt, sinon l'utilisateur il croit que ça fait partie de la commande.
-Le style "verbatim" fait partie des éléments qui aident à reconnaître
-les commandes qui peuvent être tappées, et puis on peut/pourra aussi
+* Le shell n'est pas csh. Le shell peut être bash, zsh, le prompt
+peut avoir été customisé par l'utilisateur, ou l'utilisateur peut
+être sous Windows et avoir un prompt de la forme "C:\>". Donc,
+on n'écrit pas de prompt précédant les commandes à taper au
+prompt, sinon l'utilisateur il croit que ça fait partie de la commande.
+Le style "verbatim" fait partie des éléments qui aident à reconnaître
+les commandes qui peuvent être tappées, et puis on peut/pourra aussi
tout faire dans l'interface graphique.
diff --git a/share/Makefile.linting b/share/Makefile.linting
index af2e2ae506d5aeda0f2c47753616c40e9c579d8f..f22e52a19904ae005b929704a521debee43381e8 100644
--- a/share/Makefile.linting
+++ b/share/Makefile.linting
@@ -24,14 +24,53 @@
# Code prettyfication and lint #
################################
-SED?=sed
-ISED?=sed -i
+# make lint includes:
+# - make check-utf8: valid UTF-8 encoding
+# - make check-eoleof: EOF preceded by an EOL
+# - make check-syntax: EOF preceded by an EOL + no TAB + no BLANK at the end
+# - make check-indent: valid indentation
+# For all these targets (and the corresponding fix-XXX), it is possible to restrict the search to a sub-directory:
+# - make LINT_DIR=<subdir> <lint-target>
+# It is possible to force the action to given files:
+# - make LINT_FILE=<file> <lint-target>
+# Notes:
+# - when LINT_FILE is given, .gitattributes and LINT_DIR are ignored;
+# - to use fix-utf8 target, the variable LINT_FROM_ENCODING=<from-encoding-name>
+# has to be set.
+
+# make clean-lint (removing linting targets) includes
+# - make clean-utf8
+# - make clean-eoleof
+# - make clean-syntax
+# - make clean-indent
+
+################################
+## Default variables
+
+IS_UTF8 ?= iconv -f UTF-8 -t UTF-8
+TO_UTF8 ?= iconv -t UTF-8 -f
+
+OCP_INDENT ?= ocp-indent
+
+# Default values necessary for
+# LINT_MAKEFILE=<this-makefile> make -f <this-makefile> <lint-target>`
+# Otherwise theses variables are defined into share/Makefile.common
+SED ?= LC_ALL=C sed
+ISED ?= sed -i
+GIT ?= git
+MKDIR ?= mkdir -p
+MV ?= mv
+RM ?= rm -f
+TOUCH ?= touch
############
# Can be set to the path of that makefile
LINT_MAKEFILE ?=
+# Can be set to a sub-directory to restrict the checking
+LINT_DIR ?= .
+
################################
LINT.makefile=$(wildcard $(LINT_MAKEFILE))
@@ -48,21 +87,21 @@ endif
## CHECK ocp-indent VERSION
.lint/check-ocp-indent-version:
- if command -v ocp-indent >/dev/null; then \
- if [ -z "$(shell ocp-indent --version)" ]; then echo "warning: ocp-indent returned an empty string, assuming it is the correct version"; \
+ if command -v $(OCP_INDENT) >/dev/null; then \
+ if [ -z "$(shell $(OCP_INDENT) --version)" ]; then echo "warning: $(OCP_INDENT) returned an empty string, assuming it is the correct version"; \
else \
- $(eval ocp_version_major := $(shell ocp-indent --version | $(SED) -E "s/^([0-9]+)\.[0-9]+\..*/\1/")) \
- $(eval ocp_version_minor := $(shell ocp-indent --version | $(SED) -E "s/^[0-9]+\.([0-9]+)\..*/\1/")) \
+ $(eval ocp_version_major := $(shell $(OCP_INDENT) --version | $(SED) -E "s/^([0-9]+)\.[0-9]+\..*/\1/")) \
+ $(eval ocp_version_minor := $(shell $(OCP_INDENT) --version | $(SED) -E "s/^[0-9]+\.([0-9]+)\..*/\1/")) \
if [ "$(ocp_version_major)" -lt 1 -o "$(ocp_version_minor)" -lt 7 ]; then \
- echo "error: ocp-indent 1.7.0 required for linting (got $(ocp_version_major).$(ocp_version_minor))"; \
+ echo "error: $(OCP_INDENT) 1.7.0 required for linting (got $(ocp_version_major).$(ocp_version_minor))"; \
exit 1; \
fi; \
fi; \
else \
exit 1; \
fi;
- mkdir -p $(dir $@)
- touch $@
+ $(MKDIR) $(dir $@)
+ $(TOUCH) $@
###############
## Main target
@@ -72,12 +111,12 @@ ifeq ($(LINT.HAS_GIT),)
.PHONY:
lint:
- echo "'make lint' requires git"
- echo "but,that is not the case of 'make LINT_FILE=<file> check-syntax'"
+ echo "'make lint' requires a git repository but, that is not"
+ echo "the case for example with 'make LINT_FILE=<file> check-syntax'"
else
-lint: check-eoleof check-syntax check-indent
+lint: check-eoleof check-syntax check-indent check-utf8
endif
@@ -93,32 +132,53 @@ clean-lint:
clean:: clean-lint
+#### clean-check-XXX targets
+
+LINT.clean-targets= \
+ clean-check-eoleof clean-check-utf8 clean-check-syntax clean-check-ident
+.PHONY: clean-check-eoleof clean-check-utf8 clean-check-syntax clean-check-ident
+
+# Generic rule
+$(LINT.clean-targets):
+ echo "[LINT] Cleaning $(patsubst clean-%,%,$@) targets..."
+ find .lint -type f -name \*.$(patsubst clean-%,%,$@) | xargs -n 10 $(RM)
+
###############################
ifeq ($(LINT_FILE),)
# No lint file given
-.PHONY: check-eoleof
-check-eoleof:
- git ls-files -z \
- | git check-attr --stdin -z check-eoleof \
- | $(SED) -zne 'x;n;n;s/^set$$//;t print;b;:print;x;p' \
- | xargs --null -IXX sh -c '$(LINT.make) LINT_FILE="XX" check-eoleof || exit 255'
+LINT.dir=$(wildcard $(LINT_DIR))
-.PHONY: check-syntax
-check-syntax:
- git ls-files -z \
- | git check-attr --stdin -z check-syntax \
+#### check-XXX targets
+
+LINT.check-targets= \
+ check-syntax check-indent check-eoleof check-utf8
+.PHONY: check-syntax check-indent check-eoleof check-utf8
+
+# Generic rule
+$(LINT.check-targets):
+ echo "[LINT] Checking from GIT attribute $@..."
+ $(GIT) ls-files $(LINT.dir) -z \
+ | $(GIT) check-attr --stdin -z $@ \
| $(SED) -zne 'x;n;n;s/^set$$//;t print;b;:print;x;p' \
- | xargs --null -IXX sh -c '$(LINT.make) LINT_FILE="XX" check-syntax || exit 255'
+ | xargs --null -IXX sh -c '$(LINT.make) LINT_FILE="XX" $@ || exit 255'
-.PHONY: check-indent
-check-indent:
- git ls-files -z \
- | git check-attr --stdin -z check-indent \
+#### fix-XXX targets
+
+LINT.fix-targets= \
+ fix-eoleof fix-utf8 fix-syntax fix-ident
+.PHONY: fix-eoleof fix-utf8 fix-syntax fix-ident
+
+# Generic rule
+$(LINT.fix-targets):
+ echo "[LINT] Fixing from GIT attribute $(patsubst fix-%,check-%,$@)..."
+ $(GIT) ls-files $(LINT.dir) -z \
+ | $(GIT) check-attr --stdin -z $(patsubst fix-%,check-%,$@) \
| $(SED) -zne 'x;n;n;s/^set$$//;t print;b;:print;x;p' \
- | xargs --null -IXX sh -c '$(LINT.make) LINT_FILE="XX" check-indent || exit 255'
+ | xargs --null -IXX sh -c '$(LINT.make) LINT_FILE="XX" $@ || exit 255'
+
else # LINT_FILE are given
@@ -126,16 +186,21 @@ else # LINT_FILE are given
LINT_FILE.list=$(addprefix .lint/,$(wildcard $(LINT_FILE)))
+LINT_FILE.check-utf8= $(addsuffix .check-utf8,$(LINT_FILE.list))
LINT_FILE.check-eoleof= $(addsuffix .check-eoleof,$(LINT_FILE.list))
LINT_FILE.check-syntax= $(addsuffix .check-syntax,$(LINT_FILE.list))
LINT_FILE.check-indent= $(addsuffix .check-indent,$(LINT_FILE.list))
+LINT_FILE.fix-utf8= $(addsuffix .fix-utf8,$(LINT_FILE.list))
LINT_FILE.fix-eoleof= $(addsuffix .fix-eoleof,$(LINT_FILE.list))
LINT_FILE.fix-syntax= $(addsuffix .fix-syntax,$(LINT_FILE.list))
LINT_FILE.fix-indent= $(addsuffix .fix-indent,$(LINT_FILE.list))
## check-XXX targets
+.PHONY: check-utf8
+check-utf8: $(LINT_FILE.check-utf8)
+
.PHONY: check-eoleof
check-eoleof: $(LINT_FILE.check-eoleof)
@@ -147,39 +212,78 @@ check-indent: $(LINT_FILE.check-indent)
## fix-XXX targets
-.PHONY: fix-syntax
-fix-syntax: $(LINT_FILE.fix-syntax)
+.PHONY: fix-utf8
+fix-utf8: $(LINT_FILE.fix-utf8)
.PHONY: fix-eoleof
fix-eoleof: $(LINT_FILE.fix-eoleof)
+.PHONY: fix-syntax
+fix-syntax: $(LINT_FILE.fix-syntax)
+
.PHONY: fix-indent
fix-indent: $(LINT_FILE.fix-indent)
endif
+###############################
+## UTF8 ASPECT
+
+$(LINT_FILE.check-utf8): .lint/%.check-utf8: %
+ echo "Check UTF8: $<"
+ if ! $(IS_UTF8) $< > /dev/null; \
+ then \
+ echo "File $< uses an invalid UTF-8 encoding."; \
+ echo "Please fixe it manualy or in running: make LINT_FROM_ENCODING=<ENCODING-NAME> LINT_FILE=$< fix-utf8";\
+ echo "The next command may help you to find that <ENCODING-NAME>: file $<";\
+ exit 1; \
+ fi
+ $(MKDIR) $(dir $@)
+ $(TOUCH) $@
+
+ifneq ($(LINT_FROM_ENCODING),)
+
+.PHONY: $(LINT_FILE.fix-utf8)
+$(LINT_FILE.fix-utf8): .lint/%.fix-utf8: %
+ if ! $(IS_UTF8) $< > /dev/null 2> /dev/null; \
+ then \
+ echo "Fixes UTF8 (from $(LINT_FROM_ENCODING)): $<"; \
+ if ! $(TO_UTF8) $(LINT_FROM_ENCODING) $< > $<.tmp; then exit 1; fi; \
+ $(MV) $<.tmp $<; \
+ fi
+ $(MKDIR) $(dir $@)
+ $(TOUCH) .lint/$<.check-utf8 # no more need of check-indent
+
+else
+
+$(LINT_FILE.fix-utf8): .lint/%.fix-utf8: % .lint/check-ocp-indent-version
+ $(error "Target fix-utf8 requires to define LINT_FROM_ENCODING variable")
+
+endif # LINT_FROM_ENCODING
+
###############################
## INDENTATION ASPECT
$(LINT_FILE.check-indent): .lint/%.check-indent: % .lint/check-ocp-indent-version
echo "Check indent: $<"
- ocp-indent $< > $<.tmp
+ $(OCP_INDENT) $< > $<.tmp
if cmp -s $< $<.tmp; \
- then rm -f $<.tmp; \
+ then $(RM) $<.tmp; \
else \
echo "File $< is not indented correctly."; \
echo "Please run: make LINT_FILE=$< fix-indent";\
- rm $<.tmp; \
+ $(RM) $<.tmp; \
exit 1; \
fi
- mkdir -p $(dir $@)
- touch $@
+ $(MKDIR) $(dir $@)
+ $(TOUCH) $@
+.PHONY: $(LINT_FILE.fix-indent)
$(LINT_FILE.fix-indent): .lint/%.fix-indent: % .lint/check-ocp-indent-version
echo "Fixes indent: $<"
- ocp-indent -i $<
- mkdir -p $(dir $@)
- touch .lint/$<.check-indent # no more need of check-indent
+ $(OCP_INDENT) -i $<
+ $(MKDIR) $(dir $@)
+ $(TOUCH) .lint/$<.check-indent # no more need of check-indent
###############################
## EOL EOF ASPECT (included by check-syntax target)
@@ -198,14 +302,16 @@ $(LINT_FILE.check-eoleof): .lint/%.check-eoleof: %
echo "Please run: make LINT_FILE=$< fix-eoleof"; \
exit 1 ; \
fi
- mkdir -p $(dir $@)
- touch $@
+ $(MKDIR) $(dir $@)
+ $(TOUCH) $@
+# The real target is a check-XXX one
+.PHONY: $(LINT_FILE.fix-eoleof)
$(LINT_FILE.fix-eoleof): .lint/%.fix-eoleof: %
echo "Fixes EOL EOF: $<"
$(ISED) -e '$$a\' $<
- mkdir -p $(dir $@)
- touch .lint/$<.check-eoleof # no more need of this checking
+ $(MKDIR) $(dir $@)
+ $(TOUCH) .lint/$<.check-eoleof # no more need of this checking
%.fix-eoleof: LC_ALL = C
@@ -233,9 +339,11 @@ $(LINT_FILE.check-syntax): .lint/%.check-syntax: %
echo "Please run: make LINT_FILE=$< fix-syntax"; \
exit 1 ; \
fi
- mkdir -p $(dir $@)
- touch $@
+ $(MKDIR) $(dir $@)
+ $(TOUCH) $@
+# The real target is a check-XXX one
+.PHONY: $(LINT_FILE.fix-syntax)
$(LINT_FILE.fix-syntax): .lint/%.fix-syntax: %
echo "Fixes syntax: $<"
$(ISED) -e 's/^ *\t\+/ /' $<
@@ -246,11 +354,11 @@ $(LINT_FILE.fix-syntax): .lint/%.fix-syntax: %
else \
while tail -n -1 $< | grep -l -e '^[ \t]*$$'; do \
head -n -1 $< > $<.tmp; \
- mv $<.tmp $<; \
+ $(MV) $<.tmp $<; \
done; \
fi
- mkdir -p $(dir $@)
- touch .lint/$<.check-syntax # no more need of check-syntax
+ $(MKDIR) $(dir $@)
+ $(TOUCH) .lint/$<.check-syntax # no more need of check-syntax
# Avoid a UTF-8 locale at all cost: in such setting, sed does not work
# reliably if you happen to have latin-1 encoding somewhere,
diff --git a/src/plugins/e-acsl/examples/ensuresec/.gitignore b/src/plugins/e-acsl/examples/ensuresec/.gitignore
index 624a0d90452b7edfc6a43b3a7409e123d5dd0ac3..48f917578b41ed6b873e778abb6c5869fd01af2f 100644
--- a/src/plugins/e-acsl/examples/ensuresec/.gitignore
+++ b/src/plugins/e-acsl/examples/ensuresec/.gitignore
@@ -1,3 +1,3 @@
build/
__pycache__/
-.env
\ No newline at end of file
+.env
diff --git a/src/plugins/instantiate/README.md b/src/plugins/instantiate/README.md
index bf55ae2cf31a74fe80eb1d587adaa83803c8a03e..f54df561537931255c333ad87e782322275b535c 100644
--- a/src/plugins/instantiate/README.md
+++ b/src/plugins/instantiate/README.md
@@ -127,4 +127,4 @@ let () = Transform.register (module struct
end)
```
-The role and types of each function is documented in `Instantiator_builder.mli`.
\ No newline at end of file
+The role and types of each function is documented in `Instantiator_builder.mli`.
diff --git a/src/plugins/server/tests/batch/wrong.json b/src/plugins/server/tests/batch/wrong.json
index 0178e8af2950cbc6b6a49d98367265e2bf993989..3c5f5262d12e7719a49df8d8fca4607f8db4b1b0 100644
--- a/src/plugins/server/tests/batch/wrong.json
+++ b/src/plugins/server/tests/batch/wrong.json
@@ -1,4 +1,4 @@
[
{ id:"unknown request", request:"kernel.unknown", data:null, comment:"the request doesn't exist" },
{ id:"wrong data", request:"kernel.ast.printFunction", data:{f1:1, f2:{x:1, y:2}, f3:null}, comment:"ident is expected, object is given" }
-]
\ No newline at end of file
+]
diff --git a/src/plugins/value/legacy/TOREMOVE b/src/plugins/value/legacy/TOREMOVE
index ffa44b40808f3595a318a93d84a20e6dd73f20ad..a45847d25ad5d534973f2563e1c31130ecacab8f 100644
--- a/src/plugins/value/legacy/TOREMOVE
+++ b/src/plugins/value/legacy/TOREMOVE
@@ -8,4 +8,4 @@
To be moved elsewhere, probably in domains/cvalue or in engine:
- eval_annots, eval_terms
\ No newline at end of file
+ eval_annots, eval_terms