diff --git a/.gitattributes b/.gitattributes
index badf7a93a94c5e0c33d6937494a3730f314ddd4e..da0339854bcd1a350ee820db02fa0870470034a8 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -52,23 +52,20 @@ Changelog merge=union
## Unset "-check-utf8"
-/doc/acsl_tutorial_slides/script -check-utf8
-/doc/developer/METADOC.txt -check-utf8
-/doc/developer/TODO -check-utf8
-/doc/index.html -check-utf8
-/doc/makeLatex -check-utf8
/doc/training/developer/macros.tex -check-utf8
-/doc/value/README -check-utf8
-
-/src/plugins/e-acsl/tests/builtin/utils -check-utf8
-/src/plugins/e-acsl/tests/format/utils -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
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/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.