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

fixes utf-8

parent 6ead6d86
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
doc/acsl_tutorial_slides/script
+ 20
− 20
View file @ 7955ef20
* 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 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 * 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. en introduisant une erreur de syntaxe et en compilant depuis Emacs.
Localiser l'erreur avec Emacs. Localiser l'erreur avec Emacs.
Alors que l'idée des prés et posts est de prouver que la post tient 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é 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 é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 de l'analyse de valeurs pour vérifier ces propriétés avec une
exécution symbolique. exécution symbolique.
* slide 2maxp.c * slide 2maxp.c
...@@ -23,29 +23,29 @@ C'est pour montrer que ACSL supporte les pointeurs. ...@@ -23,29 +23,29 @@ C'est pour montrer que ACSL supporte les pointeurs.
Avertissements sur le fait que le langage logique est Avertissements sur le fait que le langage logique est
un langage pur. un langage pur.
Le && est commutatif. Parler de (*p) n'a pas de sens en 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 général mais des propriétés telles que *p==*p sont
vraies même si p n'est pas valide. Mieux vaut vraies même si p n'est pas valide. Mieux vaut
toujours écrire "\valid(p) && *p == ..." toujours écrire "\valid(p) && *p == ..."
* slide 4comp_part.c * slide 4comp_part.c
Attirer l'attention sur ce que c'est une spécification Attirer l'attention sur ce que c'est une spécification
complète. Insister sur le fait que c'est très difficile complète. Insister sur le fait que c'est très difficile
d'en écrire en pratique (formelles ou non formelles) mais d'en écrire en pratique (formelles ou non formelles) mais
que les spécifications partielles sont utiles aussi que les spécifications partielles sont utiles aussi
(et qu'on peut se servir d'ACSL pour en faire). (et qu'on peut se servir d'ACSL pour en faire).
* slide 5assigns_term.c * 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. pour parler des assigns et de la terminaison.
* slide 6pred.c * slide 6pred.c
Les spécifications peuvent devenir plus élaborée en Les spécifications peuvent devenir plus élaborée en
commençant par définir des prédicats utilisateurs. commençant par définir des prédicats utilisateurs.
Ici, défini comme une fonction Ici, défini comme une fonction
* slide 7pred.c * 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.
doc/index.html
+ 2
− 2
View file @ 7955ef20
...@@ -4,7 +4,7 @@ PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" ...@@ -4,7 +4,7 @@ PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
<html> <html>
<head> <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"/> <link rel="stylesheet" href="style.css" type="text/css"/>
<title>Frama-C</title> <title>Frama-C</title>
</head> </head>
...@@ -125,7 +125,7 @@ PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" ...@@ -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/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/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/Implem/index.html">implementation</a> : <tt>cd wp/Implem; make</tt>)
(<a href="wp/Coq/doc/toc.html">modlisation 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>) (<a href="code/wp/metrics.html">metrics</a> : <tt>make Wp_metrics)</tt>)
</li><li> </li><li>
<a href="code/cxx_elsa/index.html">cxx</a> <a href="code/cxx_elsa/index.html">cxx</a>
......
doc/value/README
+ 14
− 14
View file @ 7955ef20
Si vous n'êtes pas un développeur de Value, vous avez Si vous n'êtes pas un développeur de Value, vous avez
reçu ce document par erreur, et vous pouvez l'ignorer. reçu ce document par erreur, et vous pouvez l'ignorer.
Conventions s'appliquant dans la documentation de Value : Conventions s'appliquant dans la documentation de Value :
* Le "plug-in d'analyse de valeur" s'appelle "the value analysis plug-in", * Le "plug-in d'analyse de valeur" s'appelle "the value analysis plug-in",
"the plug-in", "the value analysis" ou "the analysis". "the plug-in", "the value analysis" ou "the analysis".
Les deux derniers sont à utiliser quand le sujet de l'action Les deux derniers sont à utiliser quand le sujet de l'action
peut être une analyse particulière d'un code particulier. peut être une analyse particulière d'un code particulier.
Utiliser "Frama-C" si et seulement si Frama-C est Utiliser "Frama-C" si et seulement si Frama-C est
l'interface visible pour l'action dont il est question, par exemple : l'interface visible pour l'action dont il est question, par exemple :
...@@ -20,19 +20,19 @@ synthetic information on the behavior of analyzed functions: ...@@ -20,19 +20,19 @@ synthetic information on the behavior of analyzed functions:
inputs, outputs, and alarms. inputs, outputs, and alarms.
* La personne qui utilise Value s'appelle "l'utilisateur" ; * 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. mais on n'a pas souvent de raison de parler d'elle.
* Sauf cas particulier, si un exemple contient le point d'entrée, * 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 alors ce point d'entrée s'appelle \verb|main|. Un exemple peut
aussi ne pas contenir de fonction \verb|main|, ce qui indique 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. 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 * 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 peut avoir été customisé par l'utilisateur, ou l'utilisateur peut
être sous Windows et avoir un prompt de la forme "C:\>". Donc, ê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 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. 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 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 les commandes qui peuvent être tappées, et puis on peut/pourra aussi
tout faire dans l'interface graphique. tout faire dans l'interface graphique.
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