From f0626839717a4feb0d1336afdd4ba6bedaaee31e Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 2 Sep 2020 11:28:14 +0200
Subject: [PATCH] Removes dokuwiki pages that are now elsewhere
---
dokuwiki/ensiie.md | 14 -----------
dokuwiki/exercises.md | 16 -------------
dokuwiki/jessie.md | 42 ---------------------------------
dokuwiki/teaching.md | 25 --------------------
dokuwiki/tutorial.md | 13 ----------
dokuwiki/tutorial/ifm-2013.md | 14 -----------
dokuwiki/tutorial/lifo-2014.md | 12 ----------
dokuwiki/tutorial/merce_2013.md | 4 ----
dokuwiki/tutorial/rv-2013.md | 10 --------
dokuwiki/tutorial/stance.md | 14 -----------
dokuwiki/ufc2013-2014-pep-tp.md | 24 -------------------
dokuwiki/ups-2015.md | 20 ----------------
12 files changed, 208 deletions(-)
delete mode 100644 dokuwiki/ensiie.md
delete mode 100644 dokuwiki/exercises.md
delete mode 100644 dokuwiki/jessie.md
delete mode 100644 dokuwiki/teaching.md
delete mode 100644 dokuwiki/tutorial.md
delete mode 100755 dokuwiki/tutorial/ifm-2013.md
delete mode 100755 dokuwiki/tutorial/lifo-2014.md
delete mode 100755 dokuwiki/tutorial/merce_2013.md
delete mode 100755 dokuwiki/tutorial/rv-2013.md
delete mode 100755 dokuwiki/tutorial/stance.md
delete mode 100644 dokuwiki/ufc2013-2014-pep-tp.md
delete mode 100644 dokuwiki/ups-2015.md
diff --git a/dokuwiki/ensiie.md b/dokuwiki/ensiie.md
deleted file mode 100644
index 1f182600..00000000
--- a/dokuwiki/ensiie.md
+++ /dev/null
@@ -1,14 +0,0 @@
----
-layout: clean_page
----
-Below is the list of exercices done with Frama-C during the Static
-Analysis Course at ENSIIE:
-
- * [2010-2011](/dokuwiki/ensiie2010-2011-ias-tp.html)
- * [2011-2012](/dokuwiki/ensiie2011-2012-ias-tp.html)
- * [2012-2013](/dokuwiki/ensiie2012-2013-ias-tp.html)
- * [2013-2014](/dokuwiki/ensiie2013-2014-ias-tp.html)
- * [2014-2015](/dokuwiki/ensiie2014-2015-ias-tp.html)
- * [2015-2016](/dokuwiki/ensiie2015-2016-ias-tp.html)
- * [2016-2017](/dokuwiki/ensiie2016-2017-ias-tp.html)
- * [2017-2018](/dokuwiki/ensiie2017-2018-ias-tp.html)
diff --git a/dokuwiki/exercises.md b/dokuwiki/exercises.md
deleted file mode 100644
index de4513d2..00000000
--- a/dokuwiki/exercises.md
+++ /dev/null
@@ -1,16 +0,0 @@
----
-layout: clean_page
----
-# Exercises on Frama-C
-
-## Value Analysis plug-in
-
- - [Lab work at ENSIIE - 2014 (in French)](/dokuwiki/ensiie2013-2014-ias-tp.html)
- - [Lab work at ENSIIE - 2013 (in French)](/dokuwiki/ensiie2012-2013-ias-tp.html)
- - [Lab work at ENSIIE - 2012 (in French)](/dokuwiki/ensiie2011-2012-ias-tp.html)
- - [Lab work at ENSIIE - 2011 (in French)](/dokuwiki/ensiie2010-2011-ias-tp.html)
-
-## WP plug-in
-
- - [Deductive Verification at University Paris Saclay (since 2015)](/dokuwiki/UPS-2015.html)
- - [Lab work at UFC - 2013-2014: WP (in French)](/dokuwiki/ufc2013-2014-pep-tp.html)
diff --git a/dokuwiki/jessie.md b/dokuwiki/jessie.md
deleted file mode 100644
index 47b3f012..00000000
--- a/dokuwiki/jessie.md
+++ /dev/null
@@ -1,42 +0,0 @@
----
-layout: clean_page
----
-# Jessie
-
-This page presents some tips about the [Jessie
-plugin](http://frama-c.com/jessie.html) of Frama-C.
-
-## Extracting proof obligation from a Jessie project
-
-<http://cavale.gforge.enseeiht.fr/files/extract_obligation>
-
-```
-usage: extract_obligation -f=funname -o=obligation [-s=solver] sources
-Options:
- -s=<solver> or --solver=<solver> with solver in {coq,smtlib,alt-ergo} (default is coq)
- -f=<fun> or --function=<fun> with fun a function in sources
- -o=<obl> or --obligation=<obl> with obl an obligation associated to the function (the name in available in the frama-c gui with jessie plugin)\\
-```
-
-## Known issues
-
-To submit a bug for the tools of the Why platform, visit
-<https://gforge.inria.fr/tracker/?atid=4012&group_id=999&func=browse>
-
- - **\\sum, \\prod, etc. are not supported by Jessie**
- See [this
- message](http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-March/000985.html)
- from frama-c-discuss.
-
-<!-- end list -->
-
- - **Timeout for provers not working under MS-Windows**
- This is a known issue in Why 2.18 and earlier versions. See [this
- fix](http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-December/000301.html).
-
-<!-- end list -->
-
- - **Code highlighting in gWhy does not work**
- This may happen when processing DOS-encoded files.
- Fix: Convert file to unix encoding (C-x RET f undecided-unix in
- Emacs).
diff --git a/dokuwiki/teaching.md b/dokuwiki/teaching.md
deleted file mode 100644
index 08fcfc2e..00000000
--- a/dokuwiki/teaching.md
+++ /dev/null
@@ -1,25 +0,0 @@
----
-layout: clean_page
----
-# Frama-C in teaching
-
-This page lists various courses that are using Frama-C in their lab
-lessons.
-
-## In English
-
- - [University of Minho: Formal Methods in Software
- Engineering](http://mei.di.uminho.pt/?q=en/1112/mfes-uk)
- - [University College London: Language-based
- security](http://www.mupuf.org/blog/2014/02/10/a_return_into_the_world_of_frama-c)
-
-## In French
-
- - [ENSIIE Evry: Static Analysis of Programs](/dokuwiki/ensiie.html)
- - [École Polytechnique: Initiation to Program
- Proof](http://www.enseignement.polytechnique.fr/profs/informatique/Sylvie.Putot/Enseignement/SemantiqueValidation/TP6.html)
-
-## In other languages
-
- - [Moscow State University: Formal Specification and Verification (in
- Russian)](http://sed.ispras.ru/fmprac)
diff --git a/dokuwiki/tutorial.md b/dokuwiki/tutorial.md
deleted file mode 100644
index c79ebc03..00000000
--- a/dokuwiki/tutorial.md
+++ /dev/null
@@ -1,13 +0,0 @@
----
-layout: clean_page
----
- - [rv-2013](/dokuwiki/tutorial/rv-2013.html): tutorial held at
- [RV 2013](http://rv2013.gforge.inria.fr/) in Rennes (France).
- - [ifm-2013](/dokuwiki/tutorial/ifm-2013.html): tutorial held at
- [iFM 2013](http://www.it.abo.fi/iFM2013/) in Turku (Finland).
- - [Stance](/dokuwiki/tutorial/Stance.html): Training sessions done
- within the [Stance](http://www.stance-project.eu/) FP7 project.
- - [MERCE 2013](/dokuwiki/tutorial/MERCE_2013.html): Training
- session made by Mitsubishi Electric R\&D Centre Europe in 2013
- - [LIFO-2014](/dokuwiki/tutorial/LIFO-2014.html): presentation of WP
- made at the LIFO laboratory of Orléans University
diff --git a/dokuwiki/tutorial/ifm-2013.md b/dokuwiki/tutorial/ifm-2013.md
deleted file mode 100755
index 4477486a..00000000
--- a/dokuwiki/tutorial/ifm-2013.md
+++ /dev/null
@@ -1,14 +0,0 @@
-A tutorial on the [WP plugin](http://www.frama-c.com/wp.html) has been
-given at
-[iFM 2013](http://www.it.abo.fi/iFM2013/workshops_and_tutorials.php) in
-Turku (Finland), on June 11th, 2013.
-[Slides](/assets/dokuwiki/tutorial/ifm-2013/slides.pdf) and [C
-examples](/assets/dokuwiki/tutorial/ifm-2013/frama_c_tutorial_examples.tar.gz)
-are available.
-
-The examples archive contains both unannotated implementation as
-exercises and a solution that can be entirely verified by the WP plug-in
-as distributed in the Fluorine 2 (20130501) version of Frama-C. For the
-more advanced examples, some special options of wp are needed in order
-for the provers to complete the proof automatically. Theses options are
-given at the bottom of each file.
diff --git a/dokuwiki/tutorial/lifo-2014.md b/dokuwiki/tutorial/lifo-2014.md
deleted file mode 100755
index cb8d1ac9..00000000
--- a/dokuwiki/tutorial/lifo-2014.md
+++ /dev/null
@@ -1,12 +0,0 @@
-This page gather material that has been presented at the seminar of the
-[LIFO laboratory](http://www.univ-orleans.fr/lifo/?lang=en) of Orléans
-University on 2014-10-13.
-
- - [slides from the
- presentation](/mantis/frama-c/tutorial/lifo-2014/slides.pdf)
- - [annotated
- programs](/mantis/frama-c/tutorial/lifo-2014/solutions.tar.gz)
- corresponding to the code shown in the slides. Note that the lemmas
- in `binary_search_tree.c` cannot be discharged in the current
- version of Frama-C, because WP does not generate a complete
- environment.
diff --git a/dokuwiki/tutorial/merce_2013.md b/dokuwiki/tutorial/merce_2013.md
deleted file mode 100755
index 8eacb3db..00000000
--- a/dokuwiki/tutorial/merce_2013.md
+++ /dev/null
@@ -1,4 +0,0 @@
-Some [presentation
-slides](/assets/dokuwiki/tutorial/introduction-to-frama-c_v2.pdf) and
-[examples](/assets/dokuwiki/tutorial/introduction-slides-examples.tar.gz)
-are used within Mitsubishi Electric.
diff --git a/dokuwiki/tutorial/rv-2013.md b/dokuwiki/tutorial/rv-2013.md
deleted file mode 100755
index 6d9dc59f..00000000
--- a/dokuwiki/tutorial/rv-2013.md
+++ /dev/null
@@ -1,10 +0,0 @@
-A tutorial on the [E-ACSL plugin](http://www.frama-c.com/eacsl.html) has
-been given at [RV 2013](http://rv2013.gforge.inria.fr/) in Rennes
-(France), on September 24th, 2013.
-[Slides](/assets/dokuwiki/tutorial/slides.pdf) and [C
-examples](/assets/dokuwiki/tutorial/eacsl_examples.tgz) are available.
-
-The examples archive contains both unannotated implementation as
-exercises and a solution that can be entirely run by the E-ACSL plug-in
-version 0.3 (with Frama-C Fluorine 20130601). The exact way to run each
-example is given at the bottom of the corresponding file.
diff --git a/dokuwiki/tutorial/stance.md b/dokuwiki/tutorial/stance.md
deleted file mode 100755
index 6ff73b3e..00000000
--- a/dokuwiki/tutorial/stance.md
+++ /dev/null
@@ -1,14 +0,0 @@
-Within the Stance project, some training sessions on Frama-C have been
-organized. This includes in particular the following presentations:
-
- - Overview of the platform:
- [slides](/assets/dokuwiki/tutorial/frama_c_overview.pdf) and
- [example of a very simple
- plugin](/assets/dokuwiki/tutorial/simple_metrics.ml)
- - Value Analysis:
- [slides](/assets/dokuwiki/tutorial/stance/value_tutorial.pdf) and
- [code
- examples](/assets/dokuwiki/tutorial/stance/value_examples.tar.gz)
- - WP (advanced presentation, following a first course):
- [slides](/assets/dokuwiki/tutorial/wp_advanced_slides.pdf) and
- [code examples](/assets/dokuwiki/frama-c/tutorial/wp_examples.tar.gz)
diff --git a/dokuwiki/ufc2013-2014-pep-tp.md b/dokuwiki/ufc2013-2014-pep-tp.md
deleted file mode 100644
index b0549f3a..00000000
--- a/dokuwiki/ufc2013-2014-pep-tp.md
+++ /dev/null
@@ -1,24 +0,0 @@
----
-layout: clean_page
----
-# Travaux Pratiques Frama-C / WP
-
-Université de Franche-Comté, Master 1 Informatique PEP, Année 2013-2014
-
-Enseignants : Guillaume PETIOT, Alain GIORGETTI, Jacques JULLIAND
-
-## Introduction
-
-Le but de ces TP est d'utiliser l'outil [Frama-C](http://frama-c.com) et
-en particulier son outil de vérification déductive
-[WP](http://frama-c.com/wp.html). La version installée à l'université de
-Franche-Comté est Fluorine 3 :
-[Fluorine-20130601](http://frama-c.com/download.html).
-
-## Première séance
-
-[tp1.pdf](/assets/dokuwiki/tp1.pdf) [va.pdf](/assets/dokuwiki/va.pdf)
-
-## Seconde séance
-
-(bientôt)
diff --git a/dokuwiki/ups-2015.md b/dokuwiki/ups-2015.md
deleted file mode 100644
index 550f2da9..00000000
--- a/dokuwiki/ups-2015.md
+++ /dev/null
@@ -1,20 +0,0 @@
----
-layout: clean_page
----
-## Deductive Verification with Frama-C/WP
-
-Context: course on Deductive Verification in [master
-FIIL](https://www.universite-paris-saclay.fr/en/education/master/m2-fondements-de-linformatique-et-ingenierie-du-logiciel-foundations-of-computer#presentation-m2)
-(2d year) at [University
-Paris-Saclay](https://www.universite-paris-saclay.fr/en) (France), since
-2015.
-
-Teachers: [Andrei Paskevich](http://tertium.org/) (Why3) and [Julien
-Signoles](http://julien.signoles.free.fr/index.en.html) (Frama-C).
-
-Our exercises use both Frama-C/WP and [Why3](http://why3.lri.fr/) ([in a
-browser](http://why3.lri.fr/try/)). [A
-tarball](/assets/dokuwiki/wp-ups.tar.gz) contains most of our material
-related to Frama-C/WP (in French, still evolving each year). The
-training exercises are embedded in slides, the ones for the final
-practical session are directly provided in .c files.
--
GitLab