Skip to content
Snippets Groups Projects
Commit d68386a5 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Moves ENSIIE course content

parent 72e84822
No related branches found
No related tags found
1 merge request!49New tutorials and teaching pages
......@@ -38,7 +38,7 @@ mêmes options que `frama-c`.
### Calcul de puissance
On considère la fonction `pow` ci-dessous (fichier
[pow.c](/assets/dokuwiki/pow.c)), qui calcule `n` élevé à la puissance
[pow.c](/download/publications/2010-ensiie-vslg/ensiie-2011-2012/pow.c)), qui calcule `n` élevé à la puissance
`m`
``` c
......@@ -64,7 +64,7 @@ unsigned int pow(unsigned int n, unsigned int m) {
intéressants dans un contexte aussi générique. On va donc
construire un contexte d'appel un peu plus spécialisé. Pour cela, on
dispose de la fonction `interval` ci-dessous (fichier
[interval.c](/assets/dokuwiki/cexamples/interval.c))
[interval.c](/download/publications/2010-ensiie-vslg/ensiie-2011-2012/interval.c))
<!-- end list -->
......
......@@ -37,7 +37,7 @@ mêmes options que `frama-c`.
### PGCD
On considère la fonction `pgcd` ci-dessous (fichier
[ppcm.c](/assets/dokuwiki/ppcm.c)), qui calcule `n` élevé à la puissance
[ppcm.c](/download/publications/2010-ensiie-vslg/ensiie-2012-2013/ppcm.c)), qui calcule `n` élevé à la puissance
`m`
``` c
......@@ -116,7 +116,7 @@ void test() {
### PPCM
On considère maintenant la fonction `ppcm` ci-dessous (et donnée
également dans [ppcm.c](/assets/dokuwiki/ppcm.c)), avec une fonction
également dans [ppcm.c](/download/publications/2010-ensiie-vslg/ensiie-2012-2013/ppcm.c)), avec une fonction
`test2` permettant de faire un test particulier.
``` c
......@@ -177,14 +177,14 @@ fichiers `main*`, puisque nous utiliserons nos propres fonctions
`main`). Générer un fichier C faisant le link de ceux-ci à l'aide de la
commande `frama-c -print -ocode resultat.i entree1.c entree2.c ...` On
travaillera désormais avec le fichier `resultat.i`, qui alternativement
est disponible [ici](/assets/dokuwiki/keccak_reference.c)
est disponible [ici](/download/publications/2010-ensiie-vslg/ensiie-2012-2013/keccak_reference.c)
#### Analyse
Il manque à ce résultat quelques fonctions de la stdlib dont Frama-C
aura besoin, et qui sont données [ici](/assets/dokuwiki/keccak_lib.c).
aura besoin, et qui sont données [ici](/download/publications/2010-ensiie-vslg/ensiie-2012-2013/keccak_lib.c).
On s'intéresse à la fonction `main` suivante
([fichier](/assets/dokuwiki/keccak_main.c)):
([fichier](/download/publications/2010-ensiie-vslg/ensiie-2012-2013/keccak_main.c)):
``` c
#include <stdio.h>
......
......@@ -21,7 +21,7 @@ version installée à l'ENSIIE est
### Premier exemple
On s'intéresse au fichier
[exercice1.c](/assets/dokuwiki/ENSIIE-2013-2014/exercice1.c)
[exercice1.c](/download/publications/2010-ensiie-vlsg/ensiie-2013-2014/exercice1.c)
```
int x,y, *z, *idx, a[101], t;
......@@ -87,7 +87,7 @@ int main (int c) {
### Alarmes
On considère le programme suivant (fichier
[exercice2.c](/assets/dokuwiki/ENSIIE-2013-2014/exercice2.c))
[exercice2.c](/download/publications/2010-ensiie-vlsg/ensiie-2013-2014/exercice2.c))
```
int main(int c) {
......@@ -131,7 +131,7 @@ Dans les exercices précédents, `c` est considéré par l'analyse de valeur
comme pouvant être n'importe quel entier (entre `INT_MIN` et `INT_MAX`).
Il est fréquent qu'on veuille mener une analyse dans un contexte plus
restreint. On considère le programme suivant (fichier
[exercice3.c](/assets/dokuwiki/ENSIIE-2013-2014/exercice3.c)):
[exercice3.c](/download/publications/2010-ensiie-vlsg/ensiie-2013-2014/exercice3.c)):
int f(int x) {
int S = 0;
......@@ -172,7 +172,7 @@ restreint. On considère le programme suivant (fichier
Cet exercice est tiré du [problème des 1000
portes](http://ww2.ac-poitiers.fr/math/spip.php?article235). On
considère le programme suivant (fichier
[porte.c](/assets/dokuwiki/ENSIIE-2013-2014/porte.c)):
[porte.c](/download/publications/2010-ensiie-vlsg/ensiie-2013-2014/porte.c)):
#include "builtin.h"
......@@ -193,7 +193,7 @@ considère le programme suivant (fichier
## Racine carrée
On s'intéresse au programme suivant, donné dans le fichier
[sqrt.c](/assets/dokuwiki/ENSIIE-2013-2014/sqrt.c):
[sqrt.c](/download/publications/2010-ensiie-vlsg/ensiie-2013-2014/sqrt.c):
#define MAX_IDX 256
......@@ -245,7 +245,7 @@ exp:Frama_C_exp`
## Deviner un nombre
On considère la fonction suivante (fichier
[devin.c](/assets/dokuwiki/ENSIIE-2013-2014/devin.c)):
[devin.c](/download/publications/2010-ensiie-vlsg/ensiie-2013-2014/devin.c)):
#include "builtin.h"
......@@ -276,7 +276,7 @@ On s'intéresse dans cet exercice au premier problème du [Projet
Euler](https://projecteuler.net/problem%3D1): trouver la somme des
entiers inférieurs à 1000 qui sont multiples de 3 ou multiples de 5. Une
implantation est proposée dans le fichier
[euler1.c](/assets/dokuwiki/ENSIIE-2013-2014/euler1.c):
[euler1.c](/download/publications/2010-ensiie-vlsg/ensiie-2013-2014/euler1.c):
int total = 0;
......
......@@ -12,7 +12,7 @@ Prevosto et Julien Signoles
## Exercice 0: Préliminaires
Le code se trouve dans le fichier
[fact.c](/assets/dokuwiki/ensiie-2014-2015/fact.c).
[fact.c](/download/publications/2010-ensiie-vlsg/ensiie-2014-2015/fact.c).
On considère la fonction `fact` suivante, correspondant à l'exemple vu
en cours:
......@@ -95,7 +95,7 @@ pour améliorer la précision des résultats.
## Exercice 1: Suite de Fibonacci
Le code se trouve dans le fichier
[fibonacci.c](/assets/dokuwiki/ensiie-2014-2015/fibonacci.c). On
[fibonacci.c](/download/publications/2010-ensiie-vlsg/ensiie-2014-2015/fibonacci.c). On
considère la fonction `fibo` suivante:
int u[100] = { 1, 1 };
......@@ -132,7 +132,7 @@ débordement arithmétique?
## Exercice 2: Buffer Circulaire
On considère le code du fichier
[ring\_buffer.c](/assets/dokuwiki/ensiie-2014-2015/ring_buffer.c),
[ring\_buffer.c](/download/publications/2010-ensiie-vlsg/ensiie-2014-2015/ring_buffer.c),
extrait de l'[article
Wikipedia](https://en.wikipedia.org/wiki/Circular_buffer) sur les
buffers circulaires. Ce code fait des allocations mémoires, pour
......@@ -160,7 +160,7 @@ arguments suivants:
On s'intéresse à une implantation d'un algorithme de compression tiré de
la Basic Compression Library de Marcus Geelnard (fichier
[rice.c](/assets/dokuwiki/ensiie-2014-2015/rice.c), le code original se
[rice.c](/download/publications/2010-ensiie-vlsg/ensiie-2014-2015/rice.c), le code original se
trouvant [ici](http://bcl.comli.eu/)). L'en-tête `rice.h` correspondant
est le suivant:
......@@ -200,7 +200,7 @@ On s'intéresse à une implantation de l'algorithme
[AES](https://en.wikipedia.org/wiki/Advanced_Encryption_Standard)
développée pour les logiciels embarqués:
[tiny-AES](https://github.com/kokke/tiny-AES128-C), dont le fichier
principal est [aes.c](/assets/dokuwiki/ensiie-2014-2015/aes.c), avec
principal est [aes.c](/download/publications/2010-ensiie-vlsg/ensiie-2014-2015/aes.c), avec
l'en-tête `aes.h` suivant:
void AES128_ECB_encrypt(uint8_t* input, const uint8_t* key, uint8_t *output);
......
......@@ -12,7 +12,7 @@ Gall et Virgile Prevosto
## Exercice 1: Crible
On considère le programme suivant, dont le code est dans
[exemple.c](/assets/dokuwiki/ensiie-2015-2016/exemple.c):
[exemple.c](/download/publications/2010-ensiie-vlsg/ensiie-2015-2016/exemple.c):
``` c
#define MAX 128
......@@ -65,7 +65,7 @@ int main() {
## Exercice 2: Triangle de Pascal
On considère le programme suivant, dont le code est dans
[pascal.c](/assets/dokuwiki/ensiie-2015-2016/pascal.c):
[pascal.c](/download/publications/2010-ensiie-vlsg/ensiie-2015-2016/pascal.c):
``` c
#define MAX 21
......@@ -105,7 +105,7 @@ int main() {
On considère des matrices carrée de taille N, encodées dans des tableau
de longueur NxN. (Cf
[pointers.c](/assets/dokuwiki/ensiie-2015-2016/pointers.c))
[pointers.c](/download/publications/2010-ensiie-vlsg/ensiie-2015-2016/pointers.c))
``` c
void m_func (int N, int a[], int b[], int c[]) {
......@@ -148,7 +148,7 @@ On s'intéresse à la bibliothèque
[bstring](http://bstring.sourceforge.net/), qui fournit une
représentation alternative des chaînes de caractères. Le code est
disponible sur le site et dans [cette
archive](/assets/dokuwiki/ensiie-2015-2016/bstrlib.zip)
archive](/download/publications/2010-ensiie-vlsg/ensiie-2015-2016/bstrlib.zip)
1. Écrire une fonction `main` qui crée deux `bstring` à partir
de chaînes C normales de 127 caractères ASCII quelconques, et en
......@@ -171,7 +171,7 @@ archive](/assets/dokuwiki/ensiie-2015-2016/bstrlib.zip)
On considère une implantation d'un algorithme de triangulation du plan
donné dans le [livre *Computational Geometry in
C*](http://cs.smith.edu/~orourke/books/ftp.html) de J. O'Rourke, et
disponible [ici](/assets/dokuwiki/ensiie-2015-2016/tri.c)
disponible [ici](/download/publications/2010-ensiie-vlsg/ensiie-2015-2016/tri.c)
1. Modifier la fonction `ReadVertices` pour créer un environnement
de 25 points dont les coordonnées seront comprises entre `-1000`
......
......@@ -12,7 +12,7 @@ Gall et Virgile Prevosto
## Exercice 1:
On considère le programme suivant, également disponible dans le fichier
[string.c](/assets/dokuwiki/ensiie-2016-2017/string.c)
[string.c](/download/publications/2010-ensiie-vlsg/ensiie-2016-2017/string.c)
``` c
int f(char* dest, int len, const char* src) {
......@@ -87,7 +87,7 @@ contient 99 caractères arbitraires (et le `0` terminal).
## Exercice 3: Fonction de Bessel
On s'intéresse au fichier
[bessel.c](/assets/dokuwiki/ensiie-2016-2017/bessel.c) de la
[bessel.c](/download/publications/2010-ensiie-vlsg/ensiie-2016-2017/bessel.c) de la
`dietlibc`, une implantation minimaliste de bibliothèque système
(<https://www.fefe.de/dietlibc/>). Plus précisément, on cherche à
déterminer la sensibilité de la fonction `j0` à une incertitude sur
......@@ -103,7 +103,7 @@ son argument.
On s'intéresse désormais à la fonction `crypt` de la `dietlibc`,
dont l'implantation est fournie dans le fichier
[crypt.c](/assets/dokuwiki/ensiie-2016-2017/crypt.c)
[crypt.c](/download/publications/2010-ensiie-vlsg/ensiie-2016-2017/crypt.c)
1. À l'aide de `man`, retrouver le comportement attendu de la
fonction
......@@ -120,7 +120,7 @@ dont l'implantation est fournie dans le fichier
On s'intéresse à la bibliothèque `sds`
(<http://github.com/antirez/sds>), qui se présente sous la forme d'un
fichier en-tête sds.h et d'un fichier d'implantation
[sds.c](/assets/dokuwiki/ensiie-2016-2017/sds.c). On va chercher à
[sds.c](/download/publications/2010-ensiie-vlsg/ensiie-2016-2017/sds.c). On va chercher à
vérifier que la concaténation de deux `sds` obtenues à partir de
chaînes C standard de 50 caractères (quelconques) ne peut provoquer
d'erreur à l'exécution.
......@@ -145,7 +145,7 @@ On s'intéresse maintenant à la bibliothèque
compression optimisée pour les courtes chaînes ASCII. On partira de la
fonction de test `main` du fichier `smaz_test.c`. Le code est
disponible dans cette
[archive](/assets/dokuwiki/ensiie-2016-2017/smaz.zip).
[archive](/download/publications/2010-ensiie-vlsg/ensiie-2016-2017/smaz.zip).
1. `smaz` utilise des fonctions de la bibliothèque standard C pour
lesquelles il faut fournir une implantation que Value Analysis
......
......@@ -12,7 +12,7 @@ Gall et Virgile Prevosto
## Exercice 1: Préliminaires
On considère la fonction suivante, également disponible dans le fichier
[array.c](/assets/dokuwiki/ensiie-2017-2018/array.c)
[array.c](/download/publications/2010-ensiie-vslg/ensiie-2017-2018/array.c)
``` c
#include <stdlib.h>
......@@ -112,12 +112,12 @@ des versions des fonctions de manipulation de buffer et de chaînes
minimisant les possibilités de débordement de buffer. Dans cet exercice,
on s’intéressera à la fonction `strispassword_s`, telle que définie
dans le fichier
[strispassword\_s.c](/assets/dokuwiki/ensiie-2017-2018/strispassword_s.c).
[strispassword\_s.c](/download/publications/2010-ensiie-vlsg/ensiie-2017-2018/strispassword_s.c).
La bibliothèque fournit un jeu de test dans
[test\_strispassword\_s.c](/assets/dokuwiki/ensiie-2017-2018/test_strispassword_s.c).
[test\_strispassword\_s.c](/download/publications/2010-ensiie-vlsg/ensiie-2017-2018/test_strispassword_s.c).
Ces fichiers ainsi que les en-têtes nécessaires sont fournis dans
l’[archive
strispassword.zip](/assets/dokuwiki/ensiie-2017-2018/strispassword.zip)
strispassword.zip](/download/publications/2010-ensiie-vlsg/ensiie-2017-2018/strispassword.zip)
### Question 1
......@@ -141,7 +141,7 @@ un `slevel` adapté.
On s’intéresse à l’implantation de l’algorithme de chiffrement AES dans
la bibliothèque [mbedtls](https://tls.mbed.org). Les fichiers
nécessaires sont dans l’archive
[mbedtls.zip](/assets/dokuwiki/ensiie-2017-2018/mbedtls.zip)
[mbedtls.zip](/download/publications/2010-ensiie-vlsg/ensiie-2017-2018/mbedtls.zip)
### Question 1
......@@ -160,7 +160,7 @@ d’erreur à l’execution.
Le code de cet exercice est tiré du livre [*Computational Geometry in
C*](http://cs.smith.edu/~orourke/books/ftp.html) de J. O’Rourke. On le
trouvera [ici](/assets/dokuwiki/ensiie-2017-2018/extreme.c). Il s’agit
trouvera [ici](/download/publications/2010-ensiie-vlsg/ensiie-2017-2018/extreme.c). Il s’agit
d’un algorithme pour calculer le point extrême d’un polygone suivant
une direction donnée.
......@@ -192,7 +192,7 @@ Les deux fichiers nécessaires à l’analyse sont `khash.h` et
`khash.c` qui contiennent respectivement l’implantation de la
bibliothèque et le cas de test suggéré dans l’implantation. Ils sont
disponible dans [cette
archive](/assets/dokuwiki/ensiie-2017-2018/khash.zip)
archive](/download/publications/2010-ensiie-vlsg/ensiie-2017-2018/khash.zip)
### Question 1
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment