From 7955ef2039b2010cc30b88da7a47d4f07e298042 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 17 Jun 2022 11:14:41 +0200
Subject: [PATCH] fixes utf-8
---
doc/acsl_tutorial_slides/script | 40 ++++++++++++++++-----------------
doc/index.html | 4 ++--
doc/value/README | 28 +++++++++++------------
3 files changed, 36 insertions(+), 36 deletions(-)
diff --git a/doc/acsl_tutorial_slides/script b/doc/acsl_tutorial_slides/script
index 9ae7ac14fc9..cdc4a4df21d 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/index.html b/doc/index.html
index 961f99ad1f9..67520447c41 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/value/README b/doc/value/README
index 8c0abd89e17..cf8e721bb34 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.
--
GitLab