From 036d849b5faf173cff13c5f97b59c0516bfff959 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 22 Oct 2019 13:57:06 +0200
Subject: [PATCH] [wp] remove garbage files
---
src/plugins/wp/MakeDistrib | 55 -----
src/plugins/wp/Partitioning.ml | 163 --------------
src/plugins/wp/Partitioning.mli | 38 ----
src/plugins/wp/PrecisionLoss.mli | 37 ----
src/plugins/wp/REVISION | 18 --
src/plugins/wp/doc/tutorial/.gitignore | 10 -
src/plugins/wp/doc/tutorial/Makefile | 207 ------------------
src/plugins/wp/doc/tutorial/README | 15 --
.../wp/doc/tutorial/adjacent/adjacent.c | 2 -
.../wp/doc/tutorial/adjacent/adjacent.h | 6 -
.../wp/doc/tutorial/adjacent/adjacent.impl | 15 --
.../wp/doc/tutorial/adjacent/adjacent.spec | 18 --
.../wp/doc/tutorial/adjacent/adjacent.tex | 23 --
.../doc/tutorial/adjacent/adjacent_report.tex | 1 -
.../wp/doc/tutorial/adjacent/neighbors.spec | 4 -
src/plugins/wp/doc/tutorial/binary/binary.h | 6 -
.../wp/doc/tutorial/binary/division.spec | 7 -
.../wp/doc/tutorial/binary/sorted.spec | 4 -
.../doc/tutorial/binarysearch/binarysearch.c | 3 -
.../doc/tutorial/binarysearch/binarysearch.h | 7 -
.../tutorial/binarysearch/binarysearch.impl | 5 -
.../tutorial/binarysearch/binarysearch.spec | 9 -
.../tutorial/binarysearch/binarysearch.tex | 26 ---
.../binarysearch/binarysearch_report.tex | 1 -
src/plugins/wp/doc/tutorial/compare/compare.c | 2 -
.../wp/doc/tutorial/compare/compare.report | 5 -
.../wp/doc/tutorial/compare/compare.spec | 19 --
.../wp/doc/tutorial/compare/compare.tex | 22 --
.../doc/tutorial/compare/compare_report.tex | 1 -
src/plugins/wp/doc/tutorial/compare/greater.c | 2 -
.../wp/doc/tutorial/compare/greater.spec | 9 -
src/plugins/wp/doc/tutorial/compare/less.c | 2 -
src/plugins/wp/doc/tutorial/compare/less.spec | 9 -
src/plugins/wp/doc/tutorial/console.report | 12 -
src/plugins/wp/doc/tutorial/copy/copy.c | 2 -
src/plugins/wp/doc/tutorial/copy/copy.h | 6 -
src/plugins/wp/doc/tutorial/copy/copy.impl | 12 -
src/plugins/wp/doc/tutorial/copy/copy.spec | 11 -
src/plugins/wp/doc/tutorial/copy/copy.tex | 20 --
.../wp/doc/tutorial/copy/copy_report.tex | 1 -
.../wp/doc/tutorial/count/count.axioms | 22 --
src/plugins/wp/doc/tutorial/count/count.c | 2 -
src/plugins/wp/doc/tutorial/count/count.h | 7 -
src/plugins/wp/doc/tutorial/count/count.impl | 15 --
src/plugins/wp/doc/tutorial/count/count.lemma | 5 -
src/plugins/wp/doc/tutorial/count/count.spec | 8 -
src/plugins/wp/doc/tutorial/count/count.tex | 35 ---
.../wp/doc/tutorial/count/count_report.tex | 1 -
.../wp/doc/tutorial/count/original.axioms | 22 --
src/plugins/wp/doc/tutorial/equal/equal.c | 2 -
src/plugins/wp/doc/tutorial/equal/equal.h | 6 -
src/plugins/wp/doc/tutorial/equal/equal.impl | 13 --
src/plugins/wp/doc/tutorial/equal/equal.spec | 9 -
src/plugins/wp/doc/tutorial/equal/equal.tex | 40 ----
.../wp/doc/tutorial/equal/equal_report.tex | 1 -
.../doc/tutorial/equal/equal_rte_report.tex | 1 -
src/plugins/wp/doc/tutorial/fill/fill.c | 2 -
src/plugins/wp/doc/tutorial/fill/fill.h | 6 -
src/plugins/wp/doc/tutorial/fill/fill.impl | 11 -
src/plugins/wp/doc/tutorial/fill/fill.spec | 8 -
src/plugins/wp/doc/tutorial/fill/fill.tex | 23 --
.../wp/doc/tutorial/fill/fill_report.tex | 1 -
src/plugins/wp/doc/tutorial/find/find.c | 2 -
src/plugins/wp/doc/tutorial/find/find.h | 6 -
src/plugins/wp/doc/tutorial/find/find.impl | 13 --
src/plugins/wp/doc/tutorial/find/find.spec | 18 --
src/plugins/wp/doc/tutorial/find/find.tex | 25 ---
.../wp/doc/tutorial/find/find_report.tex | 1 -
.../wp/doc/tutorial/find/hasvalue.spec | 4 -
.../wp/doc/tutorial/findfirst/findfirst.c | 2 -
.../wp/doc/tutorial/findfirst/findfirst.h | 7 -
.../wp/doc/tutorial/findfirst/findfirst.impl | 14 --
.../wp/doc/tutorial/findfirst/findfirst.spec | 20 --
.../wp/doc/tutorial/findfirst/findfirst.tex | 25 ---
.../tutorial/findfirst/findfirst_report.tex | 1 -
.../wp/doc/tutorial/findfirst/hasvalueof.spec | 6 -
src/plugins/wp/doc/tutorial/iota/iota.c | 2 -
src/plugins/wp/doc/tutorial/iota/iota.h | 6 -
src/plugins/wp/doc/tutorial/iota/iota.impl | 14 --
src/plugins/wp/doc/tutorial/iota/iota.spec | 9 -
src/plugins/wp/doc/tutorial/iota/iota.tex | 23 --
.../wp/doc/tutorial/iota/iota_report.tex | 1 -
src/plugins/wp/doc/tutorial/library.h | 4 -
src/plugins/wp/doc/tutorial/library.spec | 11 -
.../wp/doc/tutorial/lowerbound/lowerbound.c | 2 -
.../wp/doc/tutorial/lowerbound/lowerbound.h | 5 -
.../doc/tutorial/lowerbound/lowerbound.impl | 23 --
.../doc/tutorial/lowerbound/lowerbound.spec | 11 -
.../wp/doc/tutorial/lowerbound/lowerbound.tex | 26 ---
.../tutorial/lowerbound/lowerbound_report.tex | 1 -
src/plugins/wp/doc/tutorial/maxelt/maxelt.c | 2 -
src/plugins/wp/doc/tutorial/maxelt/maxelt.h | 5 -
.../wp/doc/tutorial/maxelt/maxelt.impl | 19 --
.../wp/doc/tutorial/maxelt/maxelt.spec | 18 --
src/plugins/wp/doc/tutorial/maxelt/maxelt.tex | 19 --
.../wp/doc/tutorial/maxelt/maxelt_report.tex | 1 -
src/plugins/wp/doc/tutorial/maxeltp/maxelt.c | 2 -
src/plugins/wp/doc/tutorial/maxeltp/maxelt.h | 6 -
.../wp/doc/tutorial/maxeltp/maxelt.impl | 19 --
.../wp/doc/tutorial/maxeltp/maxelt.report | 5 -
.../wp/doc/tutorial/maxeltp/maxelt.spec | 17 --
.../wp/doc/tutorial/maxeltp/maxelt.tex | 25 ---
.../wp/doc/tutorial/maxeltp/maxelt_report.tex | 1 -
.../wp/doc/tutorial/maxeltp/maximum.spec | 7 -
src/plugins/wp/doc/tutorial/maxseq/maxseq.c | 3 -
src/plugins/wp/doc/tutorial/maxseq/maxseq.h | 5 -
.../wp/doc/tutorial/maxseq/maxseq.impl | 4 -
.../wp/doc/tutorial/maxseq/maxseq.spec | 9 -
src/plugins/wp/doc/tutorial/maxseq/maxseq.tex | 22 --
.../wp/doc/tutorial/maxseq/maxseq_report.tex | 1 -
src/plugins/wp/doc/tutorial/minelt/minelt.c | 2 -
src/plugins/wp/doc/tutorial/minelt/minelt.h | 5 -
.../wp/doc/tutorial/minelt/minelt.impl | 19 --
.../wp/doc/tutorial/minelt/minelt.spec | 18 --
src/plugins/wp/doc/tutorial/minelt/minelt.tex | 20 --
.../wp/doc/tutorial/minelt/minelt_report.tex | 1 -
.../doc/tutorial/mismatch/eqmismatch.report | 5 -
.../tutorial/mismatch/eqmismatch_report.tex | 1 -
src/plugins/wp/doc/tutorial/mismatch/equal.c | 8 -
.../wp/doc/tutorial/mismatch/mismatch.c | 2 -
.../wp/doc/tutorial/mismatch/mismatch.h | 6 -
.../wp/doc/tutorial/mismatch/mismatch.impl | 14 --
.../wp/doc/tutorial/mismatch/mismatch.spec | 20 --
.../wp/doc/tutorial/mismatch/mismatch.tex | 34 ---
.../doc/tutorial/mismatch/mismatch_report.tex | 1 -
.../wp/doc/tutorial/ptests_local_config.in | 6 -
.../doc/tutorial/removecopy/original.axioms | 22 --
.../doc/tutorial/removecopy/removecopy.axioms | 22 --
.../wp/doc/tutorial/removecopy/removecopy.c | 2 -
.../wp/doc/tutorial/removecopy/removecopy.h | 7 -
.../doc/tutorial/removecopy/removecopy.impl | 16 --
.../doc/tutorial/removecopy/removecopy.spec | 22 --
.../wp/doc/tutorial/removecopy/removecopy.tex | 40 ----
.../tutorial/removecopy/removecopy_report.tex | 1 -
.../wp/doc/tutorial/replacecopy/replacecopy.c | 2 -
.../wp/doc/tutorial/replacecopy/replacecopy.h | 6 -
.../doc/tutorial/replacecopy/replacecopy.impl | 19 --
.../doc/tutorial/replacecopy/replacecopy.spec | 15 --
.../doc/tutorial/replacecopy/replacecopy.tex | 21 --
.../replacecopy/replacecopy_report.tex | 1 -
.../wp/doc/tutorial/reversecopy/reverse.c | 2 -
.../wp/doc/tutorial/reversecopy/reverse.h | 7 -
.../wp/doc/tutorial/reversecopy/reverse.impl | 33 ---
.../wp/doc/tutorial/reversecopy/reverse.spec | 9 -
.../tutorial/reversecopy/reverse_report.tex | 1 -
.../wp/doc/tutorial/reversecopy/reversecopy.c | 2 -
.../wp/doc/tutorial/reversecopy/reversecopy.h | 6 -
.../doc/tutorial/reversecopy/reversecopy.impl | 12 -
.../doc/tutorial/reversecopy/reversecopy.spec | 9 -
.../doc/tutorial/reversecopy/reversecopy.tex | 41 ----
.../reversecopy/reversecopy_report.tex | 1 -
.../wp/doc/tutorial/rotatecopy/rotatecopy.c | 3 -
.../wp/doc/tutorial/rotatecopy/rotatecopy.h | 6 -
.../doc/tutorial/rotatecopy/rotatecopy.impl | 5 -
.../doc/tutorial/rotatecopy/rotatecopy.spec | 13 --
.../wp/doc/tutorial/rotatecopy/rotatecopy.tex | 21 --
.../tutorial/rotatecopy/rotatecopy_report.tex | 1 -
.../wp/doc/tutorial/search/hasrange.spec | 5 -
src/plugins/wp/doc/tutorial/search/search.c | 2 -
src/plugins/wp/doc/tutorial/search/search.h | 6 -
.../wp/doc/tutorial/search/search.impl | 18 --
.../wp/doc/tutorial/search/search.spec | 20 --
src/plugins/wp/doc/tutorial/search/search.tex | 32 ---
.../wp/doc/tutorial/search/search_report.tex | 1 -
src/plugins/wp/doc/tutorial/summary.report | 5 -
src/plugins/wp/doc/tutorial/swap/swap.c | 2 -
src/plugins/wp/doc/tutorial/swap/swap.h | 6 -
src/plugins/wp/doc/tutorial/swap/swap.impl | 5 -
src/plugins/wp/doc/tutorial/swap/swap.spec | 12 -
src/plugins/wp/doc/tutorial/swap/swap.tex | 21 --
.../wp/doc/tutorial/swap/swap_report.tex | 1 -
.../wp/doc/tutorial/swapranges/swapranges.c | 3 -
.../wp/doc/tutorial/swapranges/swapranges.h | 6 -
.../doc/tutorial/swapranges/swapranges.impl | 16 --
.../doc/tutorial/swapranges/swapranges.spec | 12 -
.../wp/doc/tutorial/swapranges/swapranges.tex | 26 ---
.../tutorial/swapranges/swapranges_report.tex | 1 -
.../swapvalues/swapvalues-withassert.c | 2 -
.../swapvalues/swapvalues-withassert.impl | 6 -
.../wp/doc/tutorial/swapvalues/swapvalues.c | 2 -
.../wp/doc/tutorial/swapvalues/swapvalues.h | 6 -
.../doc/tutorial/swapvalues/swapvalues.impl | 6 -
.../doc/tutorial/swapvalues/swapvalues.spec | 22 --
.../wp/doc/tutorial/swapvalues/swapvalues.tex | 23 --
.../tutorial/swapvalues/swapvalues_report.tex | 1 -
.../doc/tutorial/tests/binary/binarysearch.i | 4 -
.../wp/doc/tutorial/tests/binary/lowerbound.i | 4 -
.../binary/oracle/binarysearch.res.oracle | 9 -
.../tests/binary/oracle/lowerbound.res.oracle | 9 -
.../tests/binary/oracle/upperbound.res.oracle | 8 -
.../wp/doc/tutorial/tests/binary/upperbound.i | 4 -
.../wp/doc/tutorial/tests/maxmin/compare.i | 4 -
.../wp/doc/tutorial/tests/maxmin/maxelt.i | 4 -
.../wp/doc/tutorial/tests/maxmin/maxeltp.i | 4 -
.../wp/doc/tutorial/tests/maxmin/maxseq.i | 4 -
.../wp/doc/tutorial/tests/maxmin/minelt.i | 4 -
.../tests/maxmin/oracle/compare.res.oracle | 7 -
.../tests/maxmin/oracle/maxelt.res.oracle | 8 -
.../tests/maxmin/oracle/maxeltp.res.oracle | 8 -
.../tests/maxmin/oracle/maxseq.res.oracle | 8 -
.../tests/maxmin/oracle/minelt.res.oracle | 8 -
.../wp/doc/tutorial/tests/mutating/copy.i | 4 -
.../wp/doc/tutorial/tests/mutating/fill.i | 4 -
.../wp/doc/tutorial/tests/mutating/iota.i | 4 -
.../tests/mutating/oracle/copy.res.oracle | 8 -
.../tests/mutating/oracle/fill.res.oracle | 9 -
.../tests/mutating/oracle/iota.res.oracle | 9 -
.../mutating/oracle/removecopy.res.oracle | 8 -
.../mutating/oracle/replacecopy.res.oracle | 8 -
.../tests/mutating/oracle/reverse.res.oracle | 8 -
.../mutating/oracle/reversecopy.res.oracle | 8 -
.../mutating/oracle/rotatecopy.res.oracle | 8 -
.../tests/mutating/oracle/swap.res.oracle | 8 -
.../mutating/oracle/swapranges.res.oracle | 8 -
.../oracle/swapvalues-withassert.res.oracle | 8 -
.../mutating/oracle/swapvalues.res.oracle | 9 -
.../mutating/oracle/uniquecopy.res.oracle | 8 -
.../doc/tutorial/tests/mutating/removecopy.i | 4 -
.../doc/tutorial/tests/mutating/replacecopy.i | 4 -
.../wp/doc/tutorial/tests/mutating/reverse.i | 4 -
.../doc/tutorial/tests/mutating/reversecopy.i | 4 -
.../doc/tutorial/tests/mutating/rotatecopy.i | 4 -
.../wp/doc/tutorial/tests/mutating/swap.i | 4 -
.../doc/tutorial/tests/mutating/swapranges.i | 4 -
.../tests/mutating/swapvalues-withassert.i | 4 -
.../doc/tutorial/tests/mutating/swapvalues.i | 4 -
.../doc/tutorial/tests/mutating/uniquecopy.i | 4 -
.../doc/tutorial/tests/nonmutating/adjacent.i | 5 -
.../wp/doc/tutorial/tests/nonmutating/count.i | 4 -
.../tutorial/tests/nonmutating/eqmismatch.i | 4 -
.../wp/doc/tutorial/tests/nonmutating/equal.i | 4 -
.../tutorial/tests/nonmutating/equal_rte.i | 4 -
.../wp/doc/tutorial/tests/nonmutating/find.i | 4 -
.../tutorial/tests/nonmutating/findfirst.i | 4 -
.../doc/tutorial/tests/nonmutating/mismatch.i | 4 -
.../nonmutating/oracle/adjacent.res.oracle | 8 -
.../tests/nonmutating/oracle/count.res.oracle | 9 -
.../nonmutating/oracle/eqmismatch.res.oracle | 8 -
.../tests/nonmutating/oracle/equal.res.oracle | 8 -
.../nonmutating/oracle/equal_rte.res.oracle | 8 -
.../tests/nonmutating/oracle/find.res.oracle | 8 -
.../nonmutating/oracle/findfirst.res.oracle | 8 -
.../nonmutating/oracle/mismatch.res.oracle | 8 -
.../nonmutating/oracle/search.res.oracle | 8 -
.../doc/tutorial/tests/nonmutating/search.i | 4 -
src/plugins/wp/doc/tutorial/tests/test_config | 2 -
.../wp/doc/tutorial/tests/test_config.in | 2 -
src/plugins/wp/doc/tutorial/tut_binary.tex | 30 ---
src/plugins/wp/doc/tutorial/tut_function.tex | 12 -
src/plugins/wp/doc/tutorial/tut_intro.tex | 49 -----
src/plugins/wp/doc/tutorial/tut_maxmin.tex | 10 -
src/plugins/wp/doc/tutorial/tut_mutating.tex | 17 --
src/plugins/wp/doc/tutorial/tut_rationale.tex | 105 ---------
src/plugins/wp/doc/tutorial/tutorial.tex | 42 ----
src/plugins/wp/doc/tutorial/tutorial.tgz | Bin 8504 -> 0 bytes
.../doc/tutorial/uniquecopy/original.axioms | 29 ---
.../doc/tutorial/uniquecopy/uniquecopy.axioms | 29 ---
.../wp/doc/tutorial/uniquecopy/uniquecopy.c | 2 -
.../wp/doc/tutorial/uniquecopy/uniquecopy.h | 7 -
.../doc/tutorial/uniquecopy/uniquecopy.impl | 24 --
.../doc/tutorial/uniquecopy/uniquecopy.spec | 24 --
.../wp/doc/tutorial/uniquecopy/uniquecopy.tex | 40 ----
.../tutorial/uniquecopy/uniquecopy_report.tex | 1 -
.../wp/doc/tutorial/upperbound/upperbound.c | 2 -
.../wp/doc/tutorial/upperbound/upperbound.h | 5 -
.../doc/tutorial/upperbound/upperbound.impl | 23 --
.../doc/tutorial/upperbound/upperbound.spec | 11 -
.../wp/doc/tutorial/upperbound/upperbound.tex | 19 --
.../tutorial/upperbound/upperbound_report.tex | 1 -
.../wp/share/ergo/int.Exponentiation.mlw | 50 -----
src/plugins/wp/share/ergo/int.Power.mlw | 44 ----
src/plugins/wp/share/wp.driver | 1 -
272 files changed, 3272 deletions(-)
delete mode 100644 src/plugins/wp/MakeDistrib
delete mode 100644 src/plugins/wp/Partitioning.ml
delete mode 100644 src/plugins/wp/Partitioning.mli
delete mode 100644 src/plugins/wp/PrecisionLoss.mli
delete mode 100644 src/plugins/wp/REVISION
delete mode 100644 src/plugins/wp/doc/tutorial/.gitignore
delete mode 100644 src/plugins/wp/doc/tutorial/Makefile
delete mode 100644 src/plugins/wp/doc/tutorial/README
delete mode 100644 src/plugins/wp/doc/tutorial/adjacent/adjacent.c
delete mode 100644 src/plugins/wp/doc/tutorial/adjacent/adjacent.h
delete mode 100644 src/plugins/wp/doc/tutorial/adjacent/adjacent.impl
delete mode 100644 src/plugins/wp/doc/tutorial/adjacent/adjacent.spec
delete mode 100644 src/plugins/wp/doc/tutorial/adjacent/adjacent.tex
delete mode 100644 src/plugins/wp/doc/tutorial/adjacent/adjacent_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/adjacent/neighbors.spec
delete mode 100644 src/plugins/wp/doc/tutorial/binary/binary.h
delete mode 100644 src/plugins/wp/doc/tutorial/binary/division.spec
delete mode 100644 src/plugins/wp/doc/tutorial/binary/sorted.spec
delete mode 100644 src/plugins/wp/doc/tutorial/binarysearch/binarysearch.c
delete mode 100644 src/plugins/wp/doc/tutorial/binarysearch/binarysearch.h
delete mode 100644 src/plugins/wp/doc/tutorial/binarysearch/binarysearch.impl
delete mode 100644 src/plugins/wp/doc/tutorial/binarysearch/binarysearch.spec
delete mode 100644 src/plugins/wp/doc/tutorial/binarysearch/binarysearch.tex
delete mode 100644 src/plugins/wp/doc/tutorial/binarysearch/binarysearch_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/compare/compare.c
delete mode 100644 src/plugins/wp/doc/tutorial/compare/compare.report
delete mode 100644 src/plugins/wp/doc/tutorial/compare/compare.spec
delete mode 100644 src/plugins/wp/doc/tutorial/compare/compare.tex
delete mode 100644 src/plugins/wp/doc/tutorial/compare/compare_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/compare/greater.c
delete mode 100644 src/plugins/wp/doc/tutorial/compare/greater.spec
delete mode 100644 src/plugins/wp/doc/tutorial/compare/less.c
delete mode 100644 src/plugins/wp/doc/tutorial/compare/less.spec
delete mode 100644 src/plugins/wp/doc/tutorial/console.report
delete mode 100644 src/plugins/wp/doc/tutorial/copy/copy.c
delete mode 100644 src/plugins/wp/doc/tutorial/copy/copy.h
delete mode 100644 src/plugins/wp/doc/tutorial/copy/copy.impl
delete mode 100644 src/plugins/wp/doc/tutorial/copy/copy.spec
delete mode 100644 src/plugins/wp/doc/tutorial/copy/copy.tex
delete mode 100644 src/plugins/wp/doc/tutorial/copy/copy_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/count/count.axioms
delete mode 100644 src/plugins/wp/doc/tutorial/count/count.c
delete mode 100644 src/plugins/wp/doc/tutorial/count/count.h
delete mode 100644 src/plugins/wp/doc/tutorial/count/count.impl
delete mode 100644 src/plugins/wp/doc/tutorial/count/count.lemma
delete mode 100644 src/plugins/wp/doc/tutorial/count/count.spec
delete mode 100644 src/plugins/wp/doc/tutorial/count/count.tex
delete mode 100644 src/plugins/wp/doc/tutorial/count/count_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/count/original.axioms
delete mode 100644 src/plugins/wp/doc/tutorial/equal/equal.c
delete mode 100644 src/plugins/wp/doc/tutorial/equal/equal.h
delete mode 100644 src/plugins/wp/doc/tutorial/equal/equal.impl
delete mode 100644 src/plugins/wp/doc/tutorial/equal/equal.spec
delete mode 100644 src/plugins/wp/doc/tutorial/equal/equal.tex
delete mode 100644 src/plugins/wp/doc/tutorial/equal/equal_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/equal/equal_rte_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/fill/fill.c
delete mode 100644 src/plugins/wp/doc/tutorial/fill/fill.h
delete mode 100644 src/plugins/wp/doc/tutorial/fill/fill.impl
delete mode 100644 src/plugins/wp/doc/tutorial/fill/fill.spec
delete mode 100644 src/plugins/wp/doc/tutorial/fill/fill.tex
delete mode 100644 src/plugins/wp/doc/tutorial/fill/fill_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/find/find.c
delete mode 100644 src/plugins/wp/doc/tutorial/find/find.h
delete mode 100644 src/plugins/wp/doc/tutorial/find/find.impl
delete mode 100644 src/plugins/wp/doc/tutorial/find/find.spec
delete mode 100644 src/plugins/wp/doc/tutorial/find/find.tex
delete mode 100644 src/plugins/wp/doc/tutorial/find/find_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/find/hasvalue.spec
delete mode 100644 src/plugins/wp/doc/tutorial/findfirst/findfirst.c
delete mode 100644 src/plugins/wp/doc/tutorial/findfirst/findfirst.h
delete mode 100644 src/plugins/wp/doc/tutorial/findfirst/findfirst.impl
delete mode 100644 src/plugins/wp/doc/tutorial/findfirst/findfirst.spec
delete mode 100644 src/plugins/wp/doc/tutorial/findfirst/findfirst.tex
delete mode 100644 src/plugins/wp/doc/tutorial/findfirst/findfirst_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/findfirst/hasvalueof.spec
delete mode 100644 src/plugins/wp/doc/tutorial/iota/iota.c
delete mode 100644 src/plugins/wp/doc/tutorial/iota/iota.h
delete mode 100644 src/plugins/wp/doc/tutorial/iota/iota.impl
delete mode 100644 src/plugins/wp/doc/tutorial/iota/iota.spec
delete mode 100644 src/plugins/wp/doc/tutorial/iota/iota.tex
delete mode 100644 src/plugins/wp/doc/tutorial/iota/iota_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/library.h
delete mode 100644 src/plugins/wp/doc/tutorial/library.spec
delete mode 100644 src/plugins/wp/doc/tutorial/lowerbound/lowerbound.c
delete mode 100644 src/plugins/wp/doc/tutorial/lowerbound/lowerbound.h
delete mode 100644 src/plugins/wp/doc/tutorial/lowerbound/lowerbound.impl
delete mode 100644 src/plugins/wp/doc/tutorial/lowerbound/lowerbound.spec
delete mode 100644 src/plugins/wp/doc/tutorial/lowerbound/lowerbound.tex
delete mode 100644 src/plugins/wp/doc/tutorial/lowerbound/lowerbound_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/maxelt/maxelt.c
delete mode 100644 src/plugins/wp/doc/tutorial/maxelt/maxelt.h
delete mode 100644 src/plugins/wp/doc/tutorial/maxelt/maxelt.impl
delete mode 100644 src/plugins/wp/doc/tutorial/maxelt/maxelt.spec
delete mode 100644 src/plugins/wp/doc/tutorial/maxelt/maxelt.tex
delete mode 100644 src/plugins/wp/doc/tutorial/maxelt/maxelt_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/maxeltp/maxelt.c
delete mode 100644 src/plugins/wp/doc/tutorial/maxeltp/maxelt.h
delete mode 100644 src/plugins/wp/doc/tutorial/maxeltp/maxelt.impl
delete mode 100644 src/plugins/wp/doc/tutorial/maxeltp/maxelt.report
delete mode 100644 src/plugins/wp/doc/tutorial/maxeltp/maxelt.spec
delete mode 100644 src/plugins/wp/doc/tutorial/maxeltp/maxelt.tex
delete mode 100644 src/plugins/wp/doc/tutorial/maxeltp/maxelt_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/maxeltp/maximum.spec
delete mode 100644 src/plugins/wp/doc/tutorial/maxseq/maxseq.c
delete mode 100644 src/plugins/wp/doc/tutorial/maxseq/maxseq.h
delete mode 100644 src/plugins/wp/doc/tutorial/maxseq/maxseq.impl
delete mode 100644 src/plugins/wp/doc/tutorial/maxseq/maxseq.spec
delete mode 100644 src/plugins/wp/doc/tutorial/maxseq/maxseq.tex
delete mode 100644 src/plugins/wp/doc/tutorial/maxseq/maxseq_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/minelt/minelt.c
delete mode 100644 src/plugins/wp/doc/tutorial/minelt/minelt.h
delete mode 100644 src/plugins/wp/doc/tutorial/minelt/minelt.impl
delete mode 100644 src/plugins/wp/doc/tutorial/minelt/minelt.spec
delete mode 100644 src/plugins/wp/doc/tutorial/minelt/minelt.tex
delete mode 100644 src/plugins/wp/doc/tutorial/minelt/minelt_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/mismatch/eqmismatch.report
delete mode 100644 src/plugins/wp/doc/tutorial/mismatch/eqmismatch_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/mismatch/equal.c
delete mode 100644 src/plugins/wp/doc/tutorial/mismatch/mismatch.c
delete mode 100644 src/plugins/wp/doc/tutorial/mismatch/mismatch.h
delete mode 100644 src/plugins/wp/doc/tutorial/mismatch/mismatch.impl
delete mode 100644 src/plugins/wp/doc/tutorial/mismatch/mismatch.spec
delete mode 100644 src/plugins/wp/doc/tutorial/mismatch/mismatch.tex
delete mode 100644 src/plugins/wp/doc/tutorial/mismatch/mismatch_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/ptests_local_config.in
delete mode 100644 src/plugins/wp/doc/tutorial/removecopy/original.axioms
delete mode 100644 src/plugins/wp/doc/tutorial/removecopy/removecopy.axioms
delete mode 100644 src/plugins/wp/doc/tutorial/removecopy/removecopy.c
delete mode 100644 src/plugins/wp/doc/tutorial/removecopy/removecopy.h
delete mode 100644 src/plugins/wp/doc/tutorial/removecopy/removecopy.impl
delete mode 100644 src/plugins/wp/doc/tutorial/removecopy/removecopy.spec
delete mode 100644 src/plugins/wp/doc/tutorial/removecopy/removecopy.tex
delete mode 100644 src/plugins/wp/doc/tutorial/removecopy/removecopy_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/replacecopy/replacecopy.c
delete mode 100644 src/plugins/wp/doc/tutorial/replacecopy/replacecopy.h
delete mode 100644 src/plugins/wp/doc/tutorial/replacecopy/replacecopy.impl
delete mode 100644 src/plugins/wp/doc/tutorial/replacecopy/replacecopy.spec
delete mode 100644 src/plugins/wp/doc/tutorial/replacecopy/replacecopy.tex
delete mode 100644 src/plugins/wp/doc/tutorial/replacecopy/replacecopy_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/reversecopy/reverse.c
delete mode 100644 src/plugins/wp/doc/tutorial/reversecopy/reverse.h
delete mode 100644 src/plugins/wp/doc/tutorial/reversecopy/reverse.impl
delete mode 100644 src/plugins/wp/doc/tutorial/reversecopy/reverse.spec
delete mode 100644 src/plugins/wp/doc/tutorial/reversecopy/reverse_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/reversecopy/reversecopy.c
delete mode 100644 src/plugins/wp/doc/tutorial/reversecopy/reversecopy.h
delete mode 100644 src/plugins/wp/doc/tutorial/reversecopy/reversecopy.impl
delete mode 100644 src/plugins/wp/doc/tutorial/reversecopy/reversecopy.spec
delete mode 100644 src/plugins/wp/doc/tutorial/reversecopy/reversecopy.tex
delete mode 100644 src/plugins/wp/doc/tutorial/reversecopy/reversecopy_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.c
delete mode 100644 src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.h
delete mode 100644 src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.impl
delete mode 100644 src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.spec
delete mode 100644 src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.tex
delete mode 100644 src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/search/hasrange.spec
delete mode 100644 src/plugins/wp/doc/tutorial/search/search.c
delete mode 100644 src/plugins/wp/doc/tutorial/search/search.h
delete mode 100644 src/plugins/wp/doc/tutorial/search/search.impl
delete mode 100644 src/plugins/wp/doc/tutorial/search/search.spec
delete mode 100644 src/plugins/wp/doc/tutorial/search/search.tex
delete mode 100644 src/plugins/wp/doc/tutorial/search/search_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/summary.report
delete mode 100644 src/plugins/wp/doc/tutorial/swap/swap.c
delete mode 100644 src/plugins/wp/doc/tutorial/swap/swap.h
delete mode 100644 src/plugins/wp/doc/tutorial/swap/swap.impl
delete mode 100644 src/plugins/wp/doc/tutorial/swap/swap.spec
delete mode 100644 src/plugins/wp/doc/tutorial/swap/swap.tex
delete mode 100644 src/plugins/wp/doc/tutorial/swap/swap_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/swapranges/swapranges.c
delete mode 100644 src/plugins/wp/doc/tutorial/swapranges/swapranges.h
delete mode 100644 src/plugins/wp/doc/tutorial/swapranges/swapranges.impl
delete mode 100644 src/plugins/wp/doc/tutorial/swapranges/swapranges.spec
delete mode 100644 src/plugins/wp/doc/tutorial/swapranges/swapranges.tex
delete mode 100644 src/plugins/wp/doc/tutorial/swapranges/swapranges_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/swapvalues/swapvalues-withassert.c
delete mode 100644 src/plugins/wp/doc/tutorial/swapvalues/swapvalues-withassert.impl
delete mode 100644 src/plugins/wp/doc/tutorial/swapvalues/swapvalues.c
delete mode 100644 src/plugins/wp/doc/tutorial/swapvalues/swapvalues.h
delete mode 100644 src/plugins/wp/doc/tutorial/swapvalues/swapvalues.impl
delete mode 100644 src/plugins/wp/doc/tutorial/swapvalues/swapvalues.spec
delete mode 100644 src/plugins/wp/doc/tutorial/swapvalues/swapvalues.tex
delete mode 100644 src/plugins/wp/doc/tutorial/swapvalues/swapvalues_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/tests/binary/binarysearch.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/binary/lowerbound.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/binary/oracle/binarysearch.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/binary/oracle/lowerbound.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/binary/oracle/upperbound.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/binary/upperbound.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/maxmin/compare.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/maxmin/maxelt.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/maxmin/maxeltp.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/maxmin/maxseq.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/maxmin/minelt.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/maxmin/oracle/compare.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/maxmin/oracle/maxelt.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/maxmin/oracle/maxeltp.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/maxmin/oracle/maxseq.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/maxmin/oracle/minelt.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/copy.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/fill.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/iota.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/oracle/copy.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/oracle/fill.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/oracle/iota.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/oracle/removecopy.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/oracle/replacecopy.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/oracle/reverse.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/oracle/reversecopy.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/oracle/rotatecopy.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/oracle/swap.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/oracle/swapranges.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/oracle/swapvalues-withassert.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/oracle/swapvalues.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/oracle/uniquecopy.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/removecopy.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/replacecopy.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/reverse.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/reversecopy.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/rotatecopy.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/swap.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/swapranges.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/swapvalues-withassert.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/swapvalues.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/mutating/uniquecopy.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/adjacent.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/count.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/eqmismatch.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/equal.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/equal_rte.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/find.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/findfirst.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/mismatch.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/adjacent.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/count.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/eqmismatch.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/equal.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/equal_rte.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/find.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/findfirst.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/mismatch.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/search.res.oracle
delete mode 100644 src/plugins/wp/doc/tutorial/tests/nonmutating/search.i
delete mode 100644 src/plugins/wp/doc/tutorial/tests/test_config
delete mode 100644 src/plugins/wp/doc/tutorial/tests/test_config.in
delete mode 100644 src/plugins/wp/doc/tutorial/tut_binary.tex
delete mode 100644 src/plugins/wp/doc/tutorial/tut_function.tex
delete mode 100644 src/plugins/wp/doc/tutorial/tut_intro.tex
delete mode 100644 src/plugins/wp/doc/tutorial/tut_maxmin.tex
delete mode 100644 src/plugins/wp/doc/tutorial/tut_mutating.tex
delete mode 100644 src/plugins/wp/doc/tutorial/tut_rationale.tex
delete mode 100644 src/plugins/wp/doc/tutorial/tutorial.tex
delete mode 100644 src/plugins/wp/doc/tutorial/tutorial.tgz
delete mode 100644 src/plugins/wp/doc/tutorial/uniquecopy/original.axioms
delete mode 100644 src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.axioms
delete mode 100644 src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.c
delete mode 100644 src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.h
delete mode 100644 src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.impl
delete mode 100644 src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.spec
delete mode 100644 src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.tex
delete mode 100644 src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy_report.tex
delete mode 100644 src/plugins/wp/doc/tutorial/upperbound/upperbound.c
delete mode 100644 src/plugins/wp/doc/tutorial/upperbound/upperbound.h
delete mode 100644 src/plugins/wp/doc/tutorial/upperbound/upperbound.impl
delete mode 100644 src/plugins/wp/doc/tutorial/upperbound/upperbound.spec
delete mode 100644 src/plugins/wp/doc/tutorial/upperbound/upperbound.tex
delete mode 100644 src/plugins/wp/doc/tutorial/upperbound/upperbound_report.tex
delete mode 100644 src/plugins/wp/share/ergo/int.Exponentiation.mlw
delete mode 100644 src/plugins/wp/share/ergo/int.Power.mlw
diff --git a/src/plugins/wp/MakeDistrib b/src/plugins/wp/MakeDistrib
deleted file mode 100644
index 3f0d12127b3..00000000000
--- a/src/plugins/wp/MakeDistrib
+++ /dev/null
@@ -1,55 +0,0 @@
-# --------------------------------------------------------------------------
-# --- Makefile for WP Distribution ---
-# --- Do not distribute this file ---
-# --------------------------------------------------------------------------
-
-.PHONY: doc changes headers instructions distrib
-
-TARBALL=wp-$(WP_VERSION)-$(WP_KERNEL)
-MANUAL=doc/WP-$(WP_VERSION).pdf
-WPINSTALL=install-wp-$(WP_VERSION)-$(WP_KERNEL).prehtml
-
-HEADERS= \
- Makefile.in configure.ac \
- *.ml *.mll *.mli \
- $(MODELS)
-
-DISTRIB_FILES:= \
- README INSTALL $(MANUAL) licenses/LGPLv2.1 \
- Makefile.in configure.ac configure .depend \
- *.ml *.mll *.mli $(MODELS)
-
-distrib: $(DISTRIB_FILES) headers instructions
- @echo "Preparing distribution"
- @rm -fr tmp.tar $(TARBALL) $(TARBALL).tgz
- @tar cf tmp.tar $(DISTRIB_FILES)
- @mkdir $(TARBALL)
- @tar xf tmp.tar -C $(TARBALL)
- @echo "Archive $(TARBALL).tgz"
- @tar zcf $(TARBALL).tgz $(TARBALL)
- @rm -fr tmp.tar $(TARBALL)
- @echo "Distribute '$(TARBALL).tgz' into '<distrib>/download/$(TARBALL).tar.gz'"
- @echo "Distribute '$(MANUAL)' into '<distrib>/download/frama-c-wp-manual.pdf'"
- @echo "Distribute '$(MANUAL)' into '<distrib>/download/wp-$(WP_VERSION)-$(WP_KERNEL).pdf'"
- @echo "Distribute '$(WPINSTALL)' into '<trunk>/doc/www/src/"
- @echo "Distribute 'Changelog' into '<trunk>/doc/www/src/wpChangelog'"
-
-instructions:
- @echo "Installation instructions"
- @ocaml htmlfilter.ml < INSTALL > $(WPINSTALL)
-
-headers::
- @echo "Applying Headers"
- @headache -c headers/headache_config.txt -h headers/open-source/CEA_LGPL $(HEADERS)
-
-doc/WP-$(WP_VERSION).pdf: doc
-
-doc::
- @echo "WP $(WP_VERSION) Manual"
- @make -C doc/manual
- @cp -f doc/manual/wp.pdf doc/WP-$(WP_VERSION).pdf
-
-changes:
- changelog -html /usr/local/shared/changelog -plugin WP -o Changelog.html Changelog
-
-# --------------------------------------------------------------------------
diff --git a/src/plugins/wp/Partitioning.ml b/src/plugins/wp/Partitioning.ml
deleted file mode 100644
index d8490466d97..00000000000
--- a/src/plugins/wp/Partitioning.ml
+++ /dev/null
@@ -1,163 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2019 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Variables Partitioning --- *)
-(* -------------------------------------------------------------------------- *)
-
-open Qed.Logic
-open Lang
-open Lang.F
-
-type partition = {
- mutable color : var Vmap.t ;
- mutable depend : Vars.t Vmap.t ;
- mutable mem : var Tmap.t ;
-}
-
-let zero = Var.dummy
-let create () = {
- color = Vmap.empty ;
- depend = Vmap.empty ;
- mem = Tmap.empty ;
-}
-
-(* -------------------------------------------------------------------------- *)
-(* --- Current Partition --- *)
-(* -------------------------------------------------------------------------- *)
-
-let rec color w x =
- try
- let y = Vmap.find x w.color in
- let z = color w y in
- if z != y then w.color <- Vmap.add x z w.color ; z
- with Not_found -> x
-
-let depend w x =
- try Vmap.find (color w x) w.depend
- with Not_found -> Vars.empty
-
-(* -------------------------------------------------------------------------- *)
-(* --- Unification & Dependencies --- *)
-(* -------------------------------------------------------------------------- *)
-
-(* keep x, bind y *)
-let merge w x y =
- w.color <- Vmap.add y x w.color ;
- let xs = depend w x in
- let ys = depend w y in
- let zs = Vars.union xs ys in
- w.depend <- Vmap.add x zs (Vmap.remove y w.depend)
-
-let unify w x y =
- if x == zero then y else
- if y == zero then x else
- let x = color w x in
- let y = color w y in
- let cmp = Var.compare x y in
- if cmp < 0 then (merge w x y ; x) else
- if cmp > 0 then (merge w y x ; y) else
- x
-
-let add_depend w x xs =
- let x = color w x in
- let ys = depend w x in
- w.depend <- Vmap.add x (Vars.union xs ys) w.depend
-
-(* -------------------------------------------------------------------------- *)
-(* --- Segregation --- *)
-(* -------------------------------------------------------------------------- *)
-
-let is_varray x = match Var.sort x with Sarray _ -> true | _ -> false
-
-let color_of w c e =
- let ms,xs = Vars.partition is_varray (F.vars e) in
- let c = Vars.fold (unify w) ms c in
- let d = Vars.fold (unify w) xs zero in
- if c == zero then d else
- (if d != zero then add_depend w c (Vars.singleton d) ; c)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Collection --- *)
-(* -------------------------------------------------------------------------- *)
-
-let rec collect w p =
- match F.repr p with
- | Eq(a,b) | Leq(a,b) | Lt(a,b) | Neq(a,b) ->
- let ca = color_of w zero a in
- let cb = color_of w zero b in
- ignore (unify w ca cb)
- | Fun(_,es) ->
- ignore
- (List.fold_left
- (fun c e ->
- let ce = color_of w zero e in
- unify w c ce)
- zero es)
- | And ps | Or ps -> List.iter (collect w) ps
- | Not p -> collect w p
- | Imply(hs,p) -> List.iter (collect w) (p::hs)
- | Bind(_,_,p) -> collect w (lc_repr p)
- | _ -> ignore (color_of w zero p)
-
-let collect w p = collect w (F.e_bool p)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Partition --- *)
-(* -------------------------------------------------------------------------- *)
-
-type classeq = partition * Vars.t
-
-(* dependencies must be normalized *)
-let rec closure w x xs =
- let x = color w x in
- if Vars.mem x xs then xs else
- Vars.fold (closure w) (depend w x) (Vars.add x xs)
-
-let classes w =
- w.depend <- Vmap.map (fun _ xs -> Vars.map (color w) xs) w.depend ;
- Vars.fold
- (fun x cs -> ( w , closure w x Vars.empty ) :: cs)
- (Vmap.fold
- (fun _ x xs -> Vars.add (color w x) xs)
- w.color Vars.empty)
- []
-
-(* Tautologies: False ==> P and P ==> True for all P *)
-(* Requires: filter false p ==> p *)
-(* Requires: p ==> filter true p *)
-let rec filter w positive xs p =
- match F.pred p with
- | And ps -> F.p_all (filter w positive xs) ps
- | Or ps -> F.p_any (filter w positive xs) ps
- | Not p -> F.p_not (filter w (not positive) xs p)
- | Imply(hs,p) ->
- let hs = List.map (filter w (not positive) xs) hs in
- F.p_hyps hs (filter w positive xs p)
- | Bind(q,x,p) -> F.p_bind q x (filter w positive (Vars.add x xs) p)
- | _ ->
- if Vars.exists (fun x -> Vars.mem (color w x) xs) (F.varsp p)
- then p
- else if positive then p_true else p_false
-
-let filter_hyp (w,xs) = filter w true xs
-let filter_goal (w,xs) = filter w false xs
diff --git a/src/plugins/wp/Partitioning.mli b/src/plugins/wp/Partitioning.mli
deleted file mode 100644
index ae3501d9293..00000000000
--- a/src/plugins/wp/Partitioning.mli
+++ /dev/null
@@ -1,38 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2019 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Variables Cleaning --- *)
-(* -------------------------------------------------------------------------- *)
-
-open Cil_types
-open Lang
-open Lang.F
-
-type partition
-type classeq
-
-val create : unit -> partition
-val collect : partition -> F.pred -> unit
-val classes : partition -> classeq list
-val filter_hyp : classeq -> F.pred -> F.pred
-val filter_goal : classeq -> F.pred -> F.pred
diff --git a/src/plugins/wp/PrecisionLoss.mli b/src/plugins/wp/PrecisionLoss.mli
deleted file mode 100644
index 791197b43d9..00000000000
--- a/src/plugins/wp/PrecisionLoss.mli
+++ /dev/null
@@ -1,37 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2019 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Qed.Logic
-open Lang
-open Conditions
-open Epsilon
-
-type term = F.term
-
-type system
-val fixpoint : system -> int -> int
-val assume : system -> term -> unit
-val target : system -> term -> unit
-
-val dump : Format.formatter -> system -> unit
-
-class simplifier : Conditions.simplifier
diff --git a/src/plugins/wp/REVISION b/src/plugins/wp/REVISION
deleted file mode 100644
index 083a9563227..00000000000
--- a/src/plugins/wp/REVISION
+++ /dev/null
@@ -1,18 +0,0 @@
-# --------------------------------------------------------------------------
-# --- REVISION HISTORY ---
-# --------------------------------------------------------------------------
-
-R11810 create wp/carbon
-R11881 create wp/work-record
-R12158 create wp/work/engine
-R12896 moveto wp/main
-R12978 main development branch (against trunk kernel)
-R12975 merged with trunk
-R13113 create wp/work/init
-R13372 merged with trunk
-R13474 merged with trunk
-R13504 merged with trunk
-R13540 merged with wp/work/init
-R13543 plugins/wp/main back into trunk/src/wp
-R13553 create wp/work/HoareRef
-R14288 merged wp/work/HoareRef into trunk/scr/wp
\ No newline at end of file
diff --git a/src/plugins/wp/doc/tutorial/.gitignore b/src/plugins/wp/doc/tutorial/.gitignore
deleted file mode 100644
index d38b2f1f1b7..00000000000
--- a/src/plugins/wp/doc/tutorial/.gitignore
+++ /dev/null
@@ -1,10 +0,0 @@
-/tutorial.pdf
-/cealistlogo.jpg
-/frama-c-book.cls
-/frama-c-cover.pdf
-/frama-c-left.pdf
-/frama-c-right.pdf
-/feedback/
-/tests/test_config
-/tests/ptests_config
-/tests/*/result
diff --git a/src/plugins/wp/doc/tutorial/Makefile b/src/plugins/wp/doc/tutorial/Makefile
deleted file mode 100644
index ccecf0ee412..00000000000
--- a/src/plugins/wp/doc/tutorial/Makefile
+++ /dev/null
@@ -1,207 +0,0 @@
-# --------------------------------------------------------------------------
-# --- WP User & Reference Manual ---
-# --------------------------------------------------------------------------
-
-.PHONY: all clean
-
-all: tutorial.pdf
-
-include ../MakeDoc
-
-TEX= \
- tutorial.tex \
- tut_intro.tex \
- tut_function.tex \
- tut_maxmin.tex \
- tut_binary.tex \
- tut_rationale.tex \
- tut_mutating.tex \
- library.spec \
- equal/equal.tex \
- equal/equal.spec \
- equal/equal.impl \
- mismatch/mismatch.tex \
- mismatch/mismatch.spec \
- mismatch/mismatch.impl \
- mismatch/equal.c \
- find/find.tex \
- find/hasvalue.spec \
- find/find.spec \
- find/find.impl \
- findfirst/findfirst.tex \
- findfirst/hasvalueof.spec \
- findfirst/findfirst.spec \
- findfirst/findfirst.impl \
- adjacent/adjacent.tex \
- adjacent/neighbors.spec \
- adjacent/adjacent.spec \
- adjacent/adjacent.impl \
- count/count.tex \
- count/count.axioms \
- count/count.lemma \
- count/count.axioms \
- count/count.spec \
- count/count.impl \
- search/search.tex \
- search/hasrange.spec \
- search/search.spec \
- search/search.impl \
- compare/compare.tex \
- compare/less.spec \
- compare/greater.spec \
- maxelt/maxelt.tex \
- maxelt/maxelt.spec \
- maxelt/maxelt.impl \
- maxeltp/maxelt.tex \
- maxeltp/maximum.spec \
- maxeltp/maxelt.spec \
- maxeltp/maxelt.impl \
- maxseq/maxseq.tex \
- maxseq/maxseq.spec \
- maxseq/maxseq.impl \
- minelt/minelt.tex \
- minelt/minelt.spec \
- minelt/minelt.impl \
- binary/sorted.spec \
- binary/division.spec \
- lowerbound/lowerbound.tex \
- lowerbound/lowerbound.spec \
- lowerbound/lowerbound.impl \
- upperbound/upperbound.tex \
- upperbound/upperbound.spec \
- upperbound/upperbound.impl \
- binarysearch/binarysearch.tex \
- binarysearch/binarysearch.spec \
- binarysearch/binarysearch.impl \
- fill/fill.tex \
- fill/fill.spec \
- fill/fill.impl \
- swap/swap.tex \
- swap/swap.spec \
- swap/swap.impl \
- swapvalues/swapvalues.tex \
- swapvalues/swapvalues.spec \
- swapvalues/swapvalues.impl \
- swapranges/swapranges.tex \
- swapranges/swapranges.spec \
- swapranges/swapranges.impl \
- copy/copy.tex \
- copy/copy.spec \
- copy/copy.impl \
- reversecopy/reversecopy.tex \
- reversecopy/reversecopy.spec \
- reversecopy/reversecopy.impl \
- reversecopy/reverse.spec \
- reversecopy/reverse.impl \
- rotatecopy/rotatecopy.tex \
- rotatecopy/rotatecopy.spec \
- rotatecopy/rotatecopy.impl \
- replacecopy/replacecopy.tex \
- replacecopy/replacecopy.spec \
- replacecopy/replacecopy.impl \
- removecopy/removecopy.tex \
- removecopy/removecopy.spec \
- removecopy/removecopy.impl \
- removecopy/removecopy.axioms \
- removecopy/original.axioms \
- uniquecopy/uniquecopy.tex \
- uniquecopy/uniquecopy.spec \
- uniquecopy/uniquecopy.impl \
- uniquecopy/uniquecopy.axioms \
- uniquecopy/original.axioms \
- iota/iota.tex \
- iota/iota.spec \
- iota/iota.impl \
-
-NONMUTATING= \
- equal equal_rte mismatch eqmismatch \
- find findfirst adjacent \
- count search
-
-MAXMIN= compare maxelt maxeltp minelt maxseq
-BINARY= lowerbound upperbound binarysearch
-MUTATING= \
- fill swap
-
-ORACLES= \
- $(addprefix tests/nonmutating/oracle/, $(addsuffix .res.oracle, $(NONMUTATING))) \
- $(addprefix tests/maxmin/oracle/, $(addsuffix .res.oracle, $(MAXMIN))) \
- $(addprefix tests/binary/oracle/, $(addsuffix .res.oracle, $(BINARY))) \
- $(addprefix tests/mutating/oracle/, $(addsuffix .res.oracle, $(MUTATING))) \
-
-OLD= \
- swapvalues/swapvalues.log \
- swapvalues/swapvalues-withassert.log \
- swapranges/swapranges.log \
- copy/copy.log \
- reversecopy/reversecopy.log \
- reversecopy/reverse.log \
- rotatecopy/rotatecopy.log \
- replacecopy/replacecopy.log \
- removecopy/removecopy.log \
- uniquecopy/uniquecopy.log \
- iota/iota.log \
-
-# --------------------------------------------------------------------------
-# --- General ---
-# --------------------------------------------------------------------------
-
-clean::
- @echo "Cleaning Tutorial"
- rm -f tutorial.pdf *.cb *.cb2 *.log *.out *.toc *.aux *.blg *.bbl *~
-
-tutorial.pdf: $(FRAMAC_DOC) $(TEX) $(SOURCE) $(ORACLES)
- rubber -d tutorial
-
-# --------------------------------------------------------------------------
-# --- Generated Logs via ptests ---
-# --------------------------------------------------------------------------
-
-.PHONY: config tests kdiff3 update
-
-tests: config
- ptests.opt -j 2
-
-kdiff3: config
- ptests.opt -j 2 -diff kdiff3
-
-update: config
- ptests.opt -update
-
-
-config: tests/test_config tests/ptests_config
-
-LIB_PATH=`frama-c -print-lib-path`
-SHARE_PATH=`frama-c -print-share-path`
-
-tests/test_config: tests/test_config.in
- rm -f $@
- @echo "SED $< -> $@"
- sed "s|@LIB_PATH@|-add-path ${LIB_PATH}/plugins -add-path .|" $< > $@
- chmod -f a-w $@
-
-tests/ptests_config: ptests_local_config.in
- rm -f $@
- @echo "SED $< -> $@"
- sed "s|@LIB_PATH@|${LIB_PATH}|" $< \
- | sed "s|@SHARE_PATH@|${SHARE_PATH}|" > $@
- chmod -f a-w $@
-
-# --------------------------------------------------------------------------
-# --- ZIP of Examples
-# --------------------------------------------------------------------------
-
-.PHONY: archive
-
-archive:
- cd .. && (find tutorial -name "README" -or -name "*.spec" -or -name "*.impl" -or -name "*.h" -or -name "*.c" | \
- xargs tar zcf tutorial/tutorial.tgz)
-
-# --------------------------------------------------------------------------
-.PHONY: help
-
-help:
- @echo "step 1: make tests -> Runs tests"
- @echo "step 2: make update -> Updates oracles (ptests -update)"
- @echo "step 3: make all -> Build tutorial.pdf file from oracles"
- @echo "step 4: make archive -> Build tutorial.tgz archive file"
diff --git a/src/plugins/wp/doc/tutorial/README b/src/plugins/wp/doc/tutorial/README
deleted file mode 100644
index e5c1c8bbdc0..00000000000
--- a/src/plugins/wp/doc/tutorial/README
+++ /dev/null
@@ -1,15 +0,0 @@
-----------------------------------------------------------
-SOURCE EXAMPLES FOR FRAMA-C WP 0.5 TUTORIAL
-
-http://frama-c.com
-----------------------------------------------------------
-LICENSE INFORMATION
-
-The example source files in the present archive are
-inspired from the book "ACSL By Example",
-produced by the Fraunhofer FIRST Institute for
-the Device-Soft project.
-
-"ACSL By Example" Version 7.1.0 of December 2011,
-http://www.first.fraunhofer.de
-----------------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/adjacent/adjacent.c b/src/plugins/wp/doc/tutorial/adjacent/adjacent.c
deleted file mode 100644
index 9b1e6753259..00000000000
--- a/src/plugins/wp/doc/tutorial/adjacent/adjacent.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "adjacent.h"
-#include "adjacent.impl"
diff --git a/src/plugins/wp/doc/tutorial/adjacent/adjacent.h b/src/plugins/wp/doc/tutorial/adjacent/adjacent.h
deleted file mode 100644
index 3e6373ebea8..00000000000
--- a/src/plugins/wp/doc/tutorial/adjacent/adjacent.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef ADJACENT_H
-#define ADJACENT_H
-#include "../library.h"
-#include "neighbors.spec"
-#include "adjacent.spec"
-#endif
diff --git a/src/plugins/wp/doc/tutorial/adjacent/adjacent.impl b/src/plugins/wp/doc/tutorial/adjacent/adjacent.impl
deleted file mode 100644
index 3540a564c33..00000000000
--- a/src/plugins/wp/doc/tutorial/adjacent/adjacent.impl
+++ /dev/null
@@ -1,15 +0,0 @@
-size_type adjacent_find(const value_type* a, size_type n)
-{
- if (0==n) return n ;
-
- /*@
- loop invariant 0 <= i < n;
- loop invariant !HasEqualNeighbors(a, i+1);
- loop assigns i;
- loop variant n-i;
- */
- for (size_type i = 0; i < n-1; i++)
- if (a[i] == a[i+1])
- return i;
- return n;
-}
diff --git a/src/plugins/wp/doc/tutorial/adjacent/adjacent.spec b/src/plugins/wp/doc/tutorial/adjacent/adjacent.spec
deleted file mode 100644
index 5f2b995c955..00000000000
--- a/src/plugins/wp/doc/tutorial/adjacent/adjacent.spec
+++ /dev/null
@@ -1,18 +0,0 @@
-/*@
- requires IsValidRange(a, n);
- assigns \nothing;
-
- behavior some:
- assumes HasEqualNeighbors(a, n);
- ensures 0 <= \result < n-1 ;
- ensures a[\result] == a[\result+1];
- ensures !HasEqualNeighbors(a, \result);
-
- behavior none:
- assumes !HasEqualNeighbors(a, n);
- ensures \result == n;
-
- complete behaviors;
- disjoint behaviors;
-*/
-size_type adjacent_find(const value_type* a, size_type n) ;
diff --git a/src/plugins/wp/doc/tutorial/adjacent/adjacent.tex b/src/plugins/wp/doc/tutorial/adjacent/adjacent.tex
deleted file mode 100644
index 2b1e8d088d5..00000000000
--- a/src/plugins/wp/doc/tutorial/adjacent/adjacent.tex
+++ /dev/null
@@ -1,23 +0,0 @@
-\section{The \textsf{adjacent-find} Algorithm}
-\label{adjacent-find}
-
-This algorithm looks for the first two consecutive equal elements in a sequence.
-The formal definition of equal neighbors is:
-
-\listingname{adjacent.h}
-\cinput{adjacent/neighbors.spec}
-
-The specification of the algorithm is:
-
-\listingname{adjacent.h}
-\cinput{adjacent/adjacent.spec}
-
-The implementation of the algorithm is:
-
-\listingname{adjacent.c}
-\cinput{adjacent/adjacent.impl}
-
-The implementation is proved correct against its specification by
-simply running the \textsf{WP} plug-in:
-\fclogs{nonmutating}{adjacent}
-
diff --git a/src/plugins/wp/doc/tutorial/adjacent/adjacent_report.tex b/src/plugins/wp/doc/tutorial/adjacent/adjacent_report.tex
deleted file mode 100644
index b8d4ece1619..00000000000
--- a/src/plugins/wp/doc/tutorial/adjacent/adjacent_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+adjacent_find+ & 23 & 11 & 12 & 100\% (95) \\
diff --git a/src/plugins/wp/doc/tutorial/adjacent/neighbors.spec b/src/plugins/wp/doc/tutorial/adjacent/neighbors.spec
deleted file mode 100644
index d883104e0c5..00000000000
--- a/src/plugins/wp/doc/tutorial/adjacent/neighbors.spec
+++ /dev/null
@@ -1,4 +0,0 @@
-/*@
- predicate HasEqualNeighbors{A}(value_type* a, integer n) =
- \exists integer i; 0 <= i < n-1 && a[i] == a[i+1];
-*/
diff --git a/src/plugins/wp/doc/tutorial/binary/binary.h b/src/plugins/wp/doc/tutorial/binary/binary.h
deleted file mode 100644
index 1e7c98964ac..00000000000
--- a/src/plugins/wp/doc/tutorial/binary/binary.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef BINARY_H
-#define BINARY_H
-#include "../library.h"
-#include "sorted.spec"
-#include "division.spec"
-#endif
diff --git a/src/plugins/wp/doc/tutorial/binary/division.spec b/src/plugins/wp/doc/tutorial/binary/division.spec
deleted file mode 100644
index 579961aff2e..00000000000
--- a/src/plugins/wp/doc/tutorial/binary/division.spec
+++ /dev/null
@@ -1,7 +0,0 @@
-/*@
- axiomatic Division {
- axiom div: \forall integer i; 0 <= i ==> 0 <= 2*(i/2) <= i;
- axiom dec: \forall integer a; 0 <= a ==> 0 <= (a/2) <= a ;
- axiom mean: \forall integer a,b; a <= a + (b-a)/2 <= b ;
- }
-*/
diff --git a/src/plugins/wp/doc/tutorial/binary/sorted.spec b/src/plugins/wp/doc/tutorial/binary/sorted.spec
deleted file mode 100644
index 17abd7b7138..00000000000
--- a/src/plugins/wp/doc/tutorial/binary/sorted.spec
+++ /dev/null
@@ -1,4 +0,0 @@
-/*@
- predicate IsSorted{L}(value_type* a, integer n) =
- \forall integer i,j; 0<=i<=j<n ==> a[i]<=a[j];
-*/
\ No newline at end of file
diff --git a/src/plugins/wp/doc/tutorial/binarysearch/binarysearch.c b/src/plugins/wp/doc/tutorial/binarysearch/binarysearch.c
deleted file mode 100644
index 772f73fa216..00000000000
--- a/src/plugins/wp/doc/tutorial/binarysearch/binarysearch.c
+++ /dev/null
@@ -1,3 +0,0 @@
-#include "binarysearch.h"
-#include "../lowerbound/lowerbound.h"
-#include "binarysearch.impl"
diff --git a/src/plugins/wp/doc/tutorial/binarysearch/binarysearch.h b/src/plugins/wp/doc/tutorial/binarysearch/binarysearch.h
deleted file mode 100644
index ad348d2f1d4..00000000000
--- a/src/plugins/wp/doc/tutorial/binarysearch/binarysearch.h
+++ /dev/null
@@ -1,7 +0,0 @@
-#ifndef BINARYSEARCH_H
-#define BINARYSEARCH_H
-#include "../library.h"
-#include "../find/hasvalue.spec"
-#include "../binary/binary.h"
-#include "binarysearch.spec"
-#endif
diff --git a/src/plugins/wp/doc/tutorial/binarysearch/binarysearch.impl b/src/plugins/wp/doc/tutorial/binarysearch/binarysearch.impl
deleted file mode 100644
index 46b94a7d63f..00000000000
--- a/src/plugins/wp/doc/tutorial/binarysearch/binarysearch.impl
+++ /dev/null
@@ -1,5 +0,0 @@
-bool binary_search(const value_type* a, size_type n, value_type val)
-{
- size_type lwb = lower_bound(a, n, val);
- return lwb < n && a[lwb] <= val;
-}
diff --git a/src/plugins/wp/doc/tutorial/binarysearch/binarysearch.spec b/src/plugins/wp/doc/tutorial/binarysearch/binarysearch.spec
deleted file mode 100644
index f958c43592b..00000000000
--- a/src/plugins/wp/doc/tutorial/binarysearch/binarysearch.spec
+++ /dev/null
@@ -1,9 +0,0 @@
-/*@
- requires IsValidRange(a, n);
- requires IsSorted(a, n);
-
- assigns \nothing;
-
- ensures \result <==> HasValue(a, n, val);
-*/
-bool binary_search(const value_type* a, size_type n, value_type val);
diff --git a/src/plugins/wp/doc/tutorial/binarysearch/binarysearch.tex b/src/plugins/wp/doc/tutorial/binarysearch/binarysearch.tex
deleted file mode 100644
index 74c6307e586..00000000000
--- a/src/plugins/wp/doc/tutorial/binarysearch/binarysearch.tex
+++ /dev/null
@@ -1,26 +0,0 @@
-\clearpage
-\section{The \textsf{binary-search} algorithm}
-
-We study here the \texttt{binary-search}
-algorithm from ``ACSL By Example''.
-Its specification is:
-
-\listingname{binarysearch.h}
-\cinput{binarysearch/binarysearch.spec}
-
-The implementation of the algorithm is:
-
-\listingname{binarysearch.c}
-\cinput{binarysearch/binarysearch.impl}
-
-\paragraph{Remark:} the original specification of loop-assigns in ``ACSL By Example''
-is \emph{wrong} since the loop \emph{do} assigns the local variables
-of the function. The original specification works with \textsf{Jessie}
-since local variables rarely live in the assignable heap, but it is
-not correct for \textsf{WP} where assigns clauses are more strictly
-verified.
-
-The implementation is proved correct against its specification by
-simply running the \textsf{WP} plug-in:
-\fclogs{binary}{binarysearch}
-
diff --git a/src/plugins/wp/doc/tutorial/binarysearch/binarysearch_report.tex b/src/plugins/wp/doc/tutorial/binarysearch/binarysearch_report.tex
deleted file mode 100644
index 6feee078a9e..00000000000
--- a/src/plugins/wp/doc/tutorial/binarysearch/binarysearch_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+binary_search+ & 10 & 8 & 2 & 100\% (91) \\
diff --git a/src/plugins/wp/doc/tutorial/compare/compare.c b/src/plugins/wp/doc/tutorial/compare/compare.c
deleted file mode 100644
index 075082e4929..00000000000
--- a/src/plugins/wp/doc/tutorial/compare/compare.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "../library.h"
-#include "compare.spec"
diff --git a/src/plugins/wp/doc/tutorial/compare/compare.report b/src/plugins/wp/doc/tutorial/compare/compare.report
deleted file mode 100644
index addd77e1a4f..00000000000
--- a/src/plugins/wp/doc/tutorial/compare/compare.report
+++ /dev/null
@@ -1,5 +0,0 @@
-@SUFFIX "_report.tex"
-@ZERO "-"
-@HEAD
-\textit{partial orders} & %total & %wp & %ergo & %success\% (%time) \\
-@END
diff --git a/src/plugins/wp/doc/tutorial/compare/compare.spec b/src/plugins/wp/doc/tutorial/compare/compare.spec
deleted file mode 100644
index c07f6483c3e..00000000000
--- a/src/plugins/wp/doc/tutorial/compare/compare.spec
+++ /dev/null
@@ -1,19 +0,0 @@
-/*@
- axiomatic Comparison {
-
- lemma LessIrreflexivity:
- \forall value_type a; !(a < a);
- lemma LessAntisymetry:
- \forall value_type a, b; (a < b) ==> !(b < a);
- lemma LessTransitivity:
- \forall value_type a, b, c; (a < b) && (b < c) ==> (a < c);
-
- lemma Greater:
- \forall value_type a, b; (a > b) <==> (b < a);
- lemma LessOrEqual:
- \forall value_type a, b; (a <= b) <==> !(b < a);
- lemma GreaterOrEqual:
- \forall value_type a, b; (a >= b) <==> !(a < b);
-
- }
-*/
diff --git a/src/plugins/wp/doc/tutorial/compare/compare.tex b/src/plugins/wp/doc/tutorial/compare/compare.tex
deleted file mode 100644
index 0872264002a..00000000000
--- a/src/plugins/wp/doc/tutorial/compare/compare.tex
+++ /dev/null
@@ -1,22 +0,0 @@
-\section{Partial Order Properties}
-\label{compare}
-
-In the case study, the partial order \verb$<$ is used with integer
-types only. With decision procedures supported by \textsf{WP} plug-in,
-the \emph{irrreflexivity}, \emph{antisymmetry} and \emph{transitivity}
-properties naturally holds and are not necessary to be included in the
-specifications.
-
-However, for \emph{genericity} purpose, we can still manage to prove
-them using \textsf{ACSL}. This can be implemented with an axiomatic
-definition:
-
-\begin{feature}{0.7}
- Proving lemmas is now supported by \textsf{WP}.
-\end{feature}
-
-\listingname{compare.spec}
-\cinput{compare/compare.spec}
-
-All these lemmas are easily discharged:
-\fclogs{maxmin}{compare}
diff --git a/src/plugins/wp/doc/tutorial/compare/compare_report.tex b/src/plugins/wp/doc/tutorial/compare/compare_report.tex
deleted file mode 100644
index 1c177e25279..00000000000
--- a/src/plugins/wp/doc/tutorial/compare/compare_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\textit{partial orders} & 6 & 4 & 2 & 100\% (1s) \\
diff --git a/src/plugins/wp/doc/tutorial/compare/greater.c b/src/plugins/wp/doc/tutorial/compare/greater.c
deleted file mode 100644
index 857cdc7a547..00000000000
--- a/src/plugins/wp/doc/tutorial/compare/greater.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "../library.h"
-#include "greater.spec"
diff --git a/src/plugins/wp/doc/tutorial/compare/greater.spec b/src/plugins/wp/doc/tutorial/compare/greater.spec
deleted file mode 100644
index eca77c4dd20..00000000000
--- a/src/plugins/wp/doc/tutorial/compare/greater.spec
+++ /dev/null
@@ -1,9 +0,0 @@
-/*@
- ensures Greater:
- \forall value_type a, b; (a > b) <==> (b < a);
- ensures LessOrEqual:
- \forall value_type a, b; (a <= b) <==> !(b < a);
- ensures GreaterOrEqual:
- \forall value_type a, b; (a >= b) <==> !(a < b);
-*/
-void greater(void) { }
diff --git a/src/plugins/wp/doc/tutorial/compare/less.c b/src/plugins/wp/doc/tutorial/compare/less.c
deleted file mode 100644
index fe789f6c422..00000000000
--- a/src/plugins/wp/doc/tutorial/compare/less.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "../library.h"
-#include "less.spec"
diff --git a/src/plugins/wp/doc/tutorial/compare/less.spec b/src/plugins/wp/doc/tutorial/compare/less.spec
deleted file mode 100644
index c3e4ae03f26..00000000000
--- a/src/plugins/wp/doc/tutorial/compare/less.spec
+++ /dev/null
@@ -1,9 +0,0 @@
-/*@
- ensures LessIrreflexivity:
- \forall value_type a; !(a < a);
- ensures LessAntisymetry:
- \forall value_type a, b; (a < b) ==> !(b < a);
- ensures LessTransitivity:
- \forall value_type a, b, c; (a < b) && (b < c) ==> (a < c);
-*/
-void less(void) { }
diff --git a/src/plugins/wp/doc/tutorial/console.report b/src/plugins/wp/doc/tutorial/console.report
deleted file mode 100644
index 5c90877059f..00000000000
--- a/src/plugins/wp/doc/tutorial/console.report
+++ /dev/null
@@ -1,12 +0,0 @@
-@CONSOLE
-@ZERO " -"
-@HEAD
-------------------------------------------------
-Module &20: #VC WP Ergo &39:Success
-@AXIOMATIC
-%name &20:%total %wp %ergo &40:%success%%
-@FUNCTION
-%function &20:%total %wp %ergo &40:%success%%
-@TAIL
-------------------------------------------------
-@END
diff --git a/src/plugins/wp/doc/tutorial/copy/copy.c b/src/plugins/wp/doc/tutorial/copy/copy.c
deleted file mode 100644
index 2837cf34c8c..00000000000
--- a/src/plugins/wp/doc/tutorial/copy/copy.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "copy.h"
-#include "copy.impl"
diff --git a/src/plugins/wp/doc/tutorial/copy/copy.h b/src/plugins/wp/doc/tutorial/copy/copy.h
deleted file mode 100644
index c1174f633f0..00000000000
--- a/src/plugins/wp/doc/tutorial/copy/copy.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef _COPY_H
-#define _COPY_H
-#include "../library.h"
-#include "copy.spec"
-#endif
-
diff --git a/src/plugins/wp/doc/tutorial/copy/copy.impl b/src/plugins/wp/doc/tutorial/copy/copy.impl
deleted file mode 100644
index 83061061aaf..00000000000
--- a/src/plugins/wp/doc/tutorial/copy/copy.impl
+++ /dev/null
@@ -1,12 +0,0 @@
-void copy(const value_type* a, size_type n, value_type* b) {
- /*@
- loop invariant 0 <= i <= n;
-
- loop assigns i,b[0..i-1];
-
- loop invariant IsEqual{Here,Here}(a, i, b);
- loop variant n-i;
- */
- for (size_type i = 0; i < n; i++)
- b[i] = a[i];
-}
diff --git a/src/plugins/wp/doc/tutorial/copy/copy.spec b/src/plugins/wp/doc/tutorial/copy/copy.spec
deleted file mode 100644
index b9dc882e464..00000000000
--- a/src/plugins/wp/doc/tutorial/copy/copy.spec
+++ /dev/null
@@ -1,11 +0,0 @@
-/*@
- requires IsValidRange(a, n);
- requires IsValidRange(b, n);
- requires \separated(a+(0..n-1), b+(0..n-1));
-
- assigns b[0..n-1];
-
- ensures IsEqual{Here,Here}(a, n, b);
-
-*/
-void copy(const value_type* a, size_type n, value_type* b);
\ No newline at end of file
diff --git a/src/plugins/wp/doc/tutorial/copy/copy.tex b/src/plugins/wp/doc/tutorial/copy/copy.tex
deleted file mode 100644
index da973b08823..00000000000
--- a/src/plugins/wp/doc/tutorial/copy/copy.tex
+++ /dev/null
@@ -1,20 +0,0 @@
-\clearpage
-\section{The \textsf{copy} Algorithm}
-\label{copy}
-
-We now study the \texttt{copy} algorithm from ``ACSL By Example''.
-This algorithm copies the contents from a source sequence to a destination sequence.
-
-The specification of the \texttt{copy} algorithm is as follows:
-
-\listingname{copy.h}
-\cinput{copy/copy.spec}
-
-The implementation of the algorithm is:
-
-\listingname{copy.c}
-\cinput{copy/copy.impl}
-
-The implementation is proved correct against its specification by
-simply running the \textsf{WP} plug-in:
-\fclogs{mutating}{copy}
diff --git a/src/plugins/wp/doc/tutorial/copy/copy_report.tex b/src/plugins/wp/doc/tutorial/copy/copy_report.tex
deleted file mode 100644
index 60b60a1ce1e..00000000000
--- a/src/plugins/wp/doc/tutorial/copy/copy_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+copy+ & 15 & 4 & 9 & 86.7\% (291) \\
diff --git a/src/plugins/wp/doc/tutorial/count/count.axioms b/src/plugins/wp/doc/tutorial/count/count.axioms
deleted file mode 100644
index fe6624335be..00000000000
--- a/src/plugins/wp/doc/tutorial/count/count.axioms
+++ /dev/null
@@ -1,22 +0,0 @@
-/*@
- axiomatic Counting
- {
- logic integer Count{L}(value_type* a, value_type val,
- integer i, integer j)
- reads a[i],a[j-1];
-
- axiom Count0{L}:
- \forall value_type *a, v, integer i;
- Count(a, v, i, i) == 0;
-
- axiom Count1{L}:
- \forall value_type* a, v, integer i, integer i, j, k;
- i <= j <= k ==> Count(a, v, i, k) ==
- Count(a, v, i, j) + Count(a, v, j, k);
-
- axiom Count2{L}:
- \forall value_type* a, v, integer i;
- (a[i] != v ==> Count(a, v, i, i+1) == 0) &&
- (a[i] == v ==> Count(a, v, i, i+1) == 1) ;
- }
-*/
diff --git a/src/plugins/wp/doc/tutorial/count/count.c b/src/plugins/wp/doc/tutorial/count/count.c
deleted file mode 100644
index b9566979105..00000000000
--- a/src/plugins/wp/doc/tutorial/count/count.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "count.h"
-#include "count.impl"
diff --git a/src/plugins/wp/doc/tutorial/count/count.h b/src/plugins/wp/doc/tutorial/count/count.h
deleted file mode 100644
index 1dc7bc21cf5..00000000000
--- a/src/plugins/wp/doc/tutorial/count/count.h
+++ /dev/null
@@ -1,7 +0,0 @@
-#ifndef COUNT_H
-#define COUNT_H
-#include "../library.h"
-#include "count.axioms"
-#include "count.lemma"
-#include "count.spec"
-#endif
diff --git a/src/plugins/wp/doc/tutorial/count/count.impl b/src/plugins/wp/doc/tutorial/count/count.impl
deleted file mode 100644
index ce3f24f0aae..00000000000
--- a/src/plugins/wp/doc/tutorial/count/count.impl
+++ /dev/null
@@ -1,15 +0,0 @@
-size_type count(const value_type* a, size_type n, value_type val)
-{
- size_type cnt = 0 ;
- /*@
- loop invariant 0 <= i <= n;
- loop invariant 0 <= cnt <= i;
- loop invariant cnt == Count(a, val, 0, i);
- loop assigns i,cnt;
- loop variant n-i;
- */
- for (size_type i = 0; i < n; i++)
- if (a[i] == val)
- cnt++;
- return cnt;
-}
diff --git a/src/plugins/wp/doc/tutorial/count/count.lemma b/src/plugins/wp/doc/tutorial/count/count.lemma
deleted file mode 100644
index cc7533c3b48..00000000000
--- a/src/plugins/wp/doc/tutorial/count/count.lemma
+++ /dev/null
@@ -1,5 +0,0 @@
-/*@
- lemma CountLemma: \forall value_type *a, v, integer i;
- 0 <= i ==> Count(a, v, 0, i+1) ==
- Count(a, v, 0, i) + Count(a, v, i, i+1);
-*/
\ No newline at end of file
diff --git a/src/plugins/wp/doc/tutorial/count/count.spec b/src/plugins/wp/doc/tutorial/count/count.spec
deleted file mode 100644
index 81f198ffd81..00000000000
--- a/src/plugins/wp/doc/tutorial/count/count.spec
+++ /dev/null
@@ -1,8 +0,0 @@
-/*@
- requires IsValidRange(a, n);
-
- ensures \result == Count(a, val, 0, n);
-
- assigns \nothing;
-*/
-size_type count(const value_type* a, size_type n, value_type val) ;
diff --git a/src/plugins/wp/doc/tutorial/count/count.tex b/src/plugins/wp/doc/tutorial/count/count.tex
deleted file mode 100644
index c975eaf8c56..00000000000
--- a/src/plugins/wp/doc/tutorial/count/count.tex
+++ /dev/null
@@ -1,35 +0,0 @@
-\section{The \textsf{count} Algorithm}
-\label{count}
-
-The algorithm presented here counts the number of occurrences for a
-given element in a sequence. The axiomatization of counting
-occurrences proposed in ``ACSL By Example'' is:
-
-\listingname{count.axioms}
-\cinput{count/original.axioms}
-
-\begin{feature}{0.7}
-The \texttt{read} clause in \texttt{count} predicate definition is now
-correctly handled. Moreover, proof obligations for lemmas are now generated.
-\end{feature}
-
-The specification of the function is as follows:
-
-\listingname{count.h}
-\cinput{count/count.spec}
-
-Then comes the implementation of the \texttt{count} algorithm:
-
-\listingname{count.c}
-\cinput{count/count.impl}
-
-In order to prove the algorithm, it is necessary to prove an
-intermediate lemma:
-
-\listingname{count.lemma}
-\cinput{count/count.lemma}
-
-The algorithm can now be proved correct against its specification by
-simply running the \textsf{WP} plug-in:
-\fclogs{nonmutating}{count}
-
diff --git a/src/plugins/wp/doc/tutorial/count/count_report.tex b/src/plugins/wp/doc/tutorial/count/count_report.tex
deleted file mode 100644
index 9fbbff20b18..00000000000
--- a/src/plugins/wp/doc/tutorial/count/count_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+count+ & 16 & 8 & 8 & 100\% (65) \\
diff --git a/src/plugins/wp/doc/tutorial/count/original.axioms b/src/plugins/wp/doc/tutorial/count/original.axioms
deleted file mode 100644
index e83b1959999..00000000000
--- a/src/plugins/wp/doc/tutorial/count/original.axioms
+++ /dev/null
@@ -1,22 +0,0 @@
-/*@
- axiomatic Counting
- {
- logic integer Count{L}(value_type* a, value_type val,
- integer i, integer j)
- reads a[i..j-1];
-
- axiom Count0{L}:
- \forall value_type *a, v, integer i;
- Count(a, v, i, i) == 0;
-
- axiom Count1{L}:
- \forall value_type* a, v, integer i, integer i, j, k;
- i <= j <= k ==> Count(a, v, i, k) ==
- Count(a, v, i, j) + Count(a, v, j, k);
-
- axiom Count2{L}:
- \forall value_type* a, v, integer i;
- (a[i] != v ==> Count(a, v, i, i+1) == 0) &&
- (a[i] == v ==> Count(a, v, i, i+1) == 1) ;
- }
-*/
diff --git a/src/plugins/wp/doc/tutorial/equal/equal.c b/src/plugins/wp/doc/tutorial/equal/equal.c
deleted file mode 100644
index fd3834d869c..00000000000
--- a/src/plugins/wp/doc/tutorial/equal/equal.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "equal.h"
-#include "equal.impl"
diff --git a/src/plugins/wp/doc/tutorial/equal/equal.h b/src/plugins/wp/doc/tutorial/equal/equal.h
deleted file mode 100644
index c4be22ed824..00000000000
--- a/src/plugins/wp/doc/tutorial/equal/equal.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef _EQUAL_H
-#define _EQUAL_H
-#include "../library.h"
-#include "equal.spec"
-#endif
-
diff --git a/src/plugins/wp/doc/tutorial/equal/equal.impl b/src/plugins/wp/doc/tutorial/equal/equal.impl
deleted file mode 100644
index 70c0536a191..00000000000
--- a/src/plugins/wp/doc/tutorial/equal/equal.impl
+++ /dev/null
@@ -1,13 +0,0 @@
-bool equal(const value_type* a, size_type n, const value_type* b)
-{
- /*@
- loop invariant 0 <= i <= n;
- loop invariant \forall int k; 0 <= k < i ==> a[k] == b[k];
- loop assigns i;
- loop variant n-i;
- */
- for (int i = 0; i < n; i++)
- if (a[i] != b[i])
- return 0;
- return 1;
-}
diff --git a/src/plugins/wp/doc/tutorial/equal/equal.spec b/src/plugins/wp/doc/tutorial/equal/equal.spec
deleted file mode 100644
index 9b1c7ac9a13..00000000000
--- a/src/plugins/wp/doc/tutorial/equal/equal.spec
+++ /dev/null
@@ -1,9 +0,0 @@
-/*@
- requires IsValidRange(a, n);
- requires IsValidRange(b, n);
-
- assigns \nothing;
-
- ensures \result <==> IsEqual{Here,Here}(a, n, b);
-*/
-bool equal(const value_type* a, size_type n, const value_type* b);
diff --git a/src/plugins/wp/doc/tutorial/equal/equal.tex b/src/plugins/wp/doc/tutorial/equal/equal.tex
deleted file mode 100644
index a4b7e43688e..00000000000
--- a/src/plugins/wp/doc/tutorial/equal/equal.tex
+++ /dev/null
@@ -1,40 +0,0 @@
-\section{The \textsf{equal} Algorithm}
-\label{equal}
-
-This algorithm implements a comparison over two generic sequences.
-The specification of the algorithm is:
-
-\listingname{equal.h}
-\cinput{equal/equal.spec}
-
-The implementation is:
-
-\listingname{equal.c}
-\cinput{equal/equal.impl}
-
-\clearpage
-\subsection{Correctness}
-
-The implementation is proved correct against its specification by
-simply running the \textsf{WP} plug-in:
-\fclogs{nonmutating}{equal}
-
-The reader should notice the warning emitted by \textsf{WP}. Actually,
-the plug-in is not responsible for proving the absence of runtime
-errors during program execution, since other plug-ins can be used
-for this, for instance \emph{Value Analysis}.
-
-\subsection{Safety}
-
-However, it is still possible to completely prove the program with
-\textsf{WP} thanks to \textsf{RTE} plug-in. This last plug-in
-generates assertions in the program wherever a runtime error might
-occur. Then, the \textsf{WP} plug-in can try to discharge the
-generated assertions.
-
-This all-together method is easily performed with \texttt{wp-rte}
-option of \textsf{WP}:
-\fclogs{nonmutating}{equal_rte}
-
-In this book, we will always use this technique to prove the
-correctness and the safety of studied algorithm.
diff --git a/src/plugins/wp/doc/tutorial/equal/equal_report.tex b/src/plugins/wp/doc/tutorial/equal/equal_report.tex
deleted file mode 100644
index a742c088480..00000000000
--- a/src/plugins/wp/doc/tutorial/equal/equal_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+equal+ & 12 & 8 & 4 & 100\% (88) \\
diff --git a/src/plugins/wp/doc/tutorial/equal/equal_rte_report.tex b/src/plugins/wp/doc/tutorial/equal/equal_rte_report.tex
deleted file mode 100644
index 68ced662220..00000000000
--- a/src/plugins/wp/doc/tutorial/equal/equal_rte_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+equal+ & 15 & 8 & 7 & 100\% (94) \\
diff --git a/src/plugins/wp/doc/tutorial/fill/fill.c b/src/plugins/wp/doc/tutorial/fill/fill.c
deleted file mode 100644
index a874b62754c..00000000000
--- a/src/plugins/wp/doc/tutorial/fill/fill.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "fill.h"
-#include "fill.impl"
diff --git a/src/plugins/wp/doc/tutorial/fill/fill.h b/src/plugins/wp/doc/tutorial/fill/fill.h
deleted file mode 100644
index 0e659d8f6b8..00000000000
--- a/src/plugins/wp/doc/tutorial/fill/fill.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef _FILL_H
-#define _FILL_H
-#include "../library.h"
-#include "fill.spec"
-#endif
-
diff --git a/src/plugins/wp/doc/tutorial/fill/fill.impl b/src/plugins/wp/doc/tutorial/fill/fill.impl
deleted file mode 100644
index 6be0419195f..00000000000
--- a/src/plugins/wp/doc/tutorial/fill/fill.impl
+++ /dev/null
@@ -1,11 +0,0 @@
-void fill(value_type* a, size_type n, value_type val)
-{
- /*@
- loop invariant 0 <= i <= n;
- loop invariant \forall integer k; 0 <= k < i ==> a[k] == val;
- loop assigns a[0..n-1], i;
- loop variant n-i;
- */
- for (size_type i = 0 ; i < n ; i++)
- a[i] = val;
-}
diff --git a/src/plugins/wp/doc/tutorial/fill/fill.spec b/src/plugins/wp/doc/tutorial/fill/fill.spec
deleted file mode 100644
index 21bdf01b361..00000000000
--- a/src/plugins/wp/doc/tutorial/fill/fill.spec
+++ /dev/null
@@ -1,8 +0,0 @@
-/*@
- requires IsValidRange(a, n);
-
- assigns a[0..n-1];
-
- ensures \forall integer i; 0 <= i < n ==> a[i] == val;
-*/
-void fill(value_type* a, size_type n, value_type val);
diff --git a/src/plugins/wp/doc/tutorial/fill/fill.tex b/src/plugins/wp/doc/tutorial/fill/fill.tex
deleted file mode 100644
index be30fb066ea..00000000000
--- a/src/plugins/wp/doc/tutorial/fill/fill.tex
+++ /dev/null
@@ -1,23 +0,0 @@
-\section{The \textsf{fill} Algorithm}
-\label{fill}
-
-We now study the \texttt{fill} algorithm from ``ACSL By Example''.
-This algorithm initializes a sequence with a particular value.
-
-The specification of the \texttt{fill} algorithm is as follows:
-
-\listingname{fill.h}
-\cinput{fill/fill.spec}
-
-The implementation of the algorithm is:
-
-\listingname{fill.c}
-\cinput{fill/fill.impl}
-
-
-From the original specification from ``ACSL By Example'', we only add
-the \emph{loop assigns} clause.
-The implementation is proved correct against its specification by
-simply running the \textsf{WP} plug-in:
-\fclogs{mutating}{fill}
-
diff --git a/src/plugins/wp/doc/tutorial/fill/fill_report.tex b/src/plugins/wp/doc/tutorial/fill/fill_report.tex
deleted file mode 100644
index e8cce5cc437..00000000000
--- a/src/plugins/wp/doc/tutorial/fill/fill_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+fill+ & 14 & 5 & 9 & 100\% (85) \\
diff --git a/src/plugins/wp/doc/tutorial/find/find.c b/src/plugins/wp/doc/tutorial/find/find.c
deleted file mode 100644
index 541e019a9c2..00000000000
--- a/src/plugins/wp/doc/tutorial/find/find.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "find.h"
-#include "find.impl"
diff --git a/src/plugins/wp/doc/tutorial/find/find.h b/src/plugins/wp/doc/tutorial/find/find.h
deleted file mode 100644
index 33cb76383ef..00000000000
--- a/src/plugins/wp/doc/tutorial/find/find.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef FIND_H
-#define FIND_H
-#include "../library.h"
-#include "hasvalue.spec"
-#include "find.spec"
-#endif
diff --git a/src/plugins/wp/doc/tutorial/find/find.impl b/src/plugins/wp/doc/tutorial/find/find.impl
deleted file mode 100644
index 82cfa1ddb37..00000000000
--- a/src/plugins/wp/doc/tutorial/find/find.impl
+++ /dev/null
@@ -1,13 +0,0 @@
-size_type find(const value_type* a, size_type n, value_type val)
-{
- /*@
- loop invariant 0 <= i <= n;
- loop invariant !HasValue(a, i, val);
- loop assigns i;
- loop variant n-i;
- */
- for (size_type i = 0; i < n; i++)
- if (a[i] == val)
- return i;
- return n;
-}
diff --git a/src/plugins/wp/doc/tutorial/find/find.spec b/src/plugins/wp/doc/tutorial/find/find.spec
deleted file mode 100644
index 53348154c4a..00000000000
--- a/src/plugins/wp/doc/tutorial/find/find.spec
+++ /dev/null
@@ -1,18 +0,0 @@
-/*@
- requires IsValidRange(a, n);
- assigns \nothing;
-
- behavior some:
- assumes HasValue(a, n, val);
- ensures 0 <= \result < n;
- ensures a[\result] == val;
- ensures !HasValue(a, \result, val);
-
- behavior none:
- assumes !HasValue(a, n, val);
- ensures \result == n;
-
- complete behaviors;
- disjoint behaviors;
-*/
-size_type find(const value_type* a, size_type n, value_type val) ;
diff --git a/src/plugins/wp/doc/tutorial/find/find.tex b/src/plugins/wp/doc/tutorial/find/find.tex
deleted file mode 100644
index d442aa09ea0..00000000000
--- a/src/plugins/wp/doc/tutorial/find/find.tex
+++ /dev/null
@@ -1,25 +0,0 @@
-\section{The \textsf{find} Algorithm}
-\label{find}
-
-We study now the \emph{reconsidered} version of the \texttt{find}
-algorithm from ``ACSL By Example''. This algorithm looks for the
-first occurrence of an element into a sequence. We makes use of the
-following helper predicate:
-
-\listingname{find.h}
-\cinput{find/hasvalue.spec}
-
-Then follows the specification of the \texttt{find} algorithm:
-
-\listingname{find.h}
-\cinput{find/find.spec}
-
-The implementation of the algorithm is:
-
-\listingname{find.c}
-\cinput{find/find.impl}
-
-The implementation is proved correct against its specification by
-simply running the \textsf{WP} plug-in:
-\fclogs{nonmutating}{find}
-
diff --git a/src/plugins/wp/doc/tutorial/find/find_report.tex b/src/plugins/wp/doc/tutorial/find/find_report.tex
deleted file mode 100644
index 671e8edeba0..00000000000
--- a/src/plugins/wp/doc/tutorial/find/find_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+find+ & 19 & 9 & 10 & 100\% (64) \\
diff --git a/src/plugins/wp/doc/tutorial/find/hasvalue.spec b/src/plugins/wp/doc/tutorial/find/hasvalue.spec
deleted file mode 100644
index 905586a015e..00000000000
--- a/src/plugins/wp/doc/tutorial/find/hasvalue.spec
+++ /dev/null
@@ -1,4 +0,0 @@
-/*@
- predicate HasValue{A}(value_type* a, integer n, value_type val) =
- \exists integer i; 0 <= i < n && a[i] == val;
-*/
diff --git a/src/plugins/wp/doc/tutorial/findfirst/findfirst.c b/src/plugins/wp/doc/tutorial/findfirst/findfirst.c
deleted file mode 100644
index efb8501f463..00000000000
--- a/src/plugins/wp/doc/tutorial/findfirst/findfirst.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "findfirst.h"
-#include "findfirst.impl"
diff --git a/src/plugins/wp/doc/tutorial/findfirst/findfirst.h b/src/plugins/wp/doc/tutorial/findfirst/findfirst.h
deleted file mode 100644
index a5571e11fa4..00000000000
--- a/src/plugins/wp/doc/tutorial/findfirst/findfirst.h
+++ /dev/null
@@ -1,7 +0,0 @@
-#ifndef FINDFIRST_H
-#define FINDFIRST_H
-#include "../library.h"
-#include "../find/find.h"
-#include "hasvalueof.spec"
-#include "findfirst.spec"
-#endif
diff --git a/src/plugins/wp/doc/tutorial/findfirst/findfirst.impl b/src/plugins/wp/doc/tutorial/findfirst/findfirst.impl
deleted file mode 100644
index 88234d3b1f5..00000000000
--- a/src/plugins/wp/doc/tutorial/findfirst/findfirst.impl
+++ /dev/null
@@ -1,14 +0,0 @@
-size_type find_first_of(const value_type* a, size_type m,
- const value_type* b, size_type n)
-{
- /*@
- loop invariant 0 <= i && i <= m;
- loop invariant !HasValueOf(a, i, b, n);
- loop assigns i;
- loop variant m-i;
- */
- for (size_type i = 0; i < m; i++)
- if (find(b, n, a[i]) < n)
- return i;
- return m;
-}
diff --git a/src/plugins/wp/doc/tutorial/findfirst/findfirst.spec b/src/plugins/wp/doc/tutorial/findfirst/findfirst.spec
deleted file mode 100644
index 977c9dbd0c3..00000000000
--- a/src/plugins/wp/doc/tutorial/findfirst/findfirst.spec
+++ /dev/null
@@ -1,20 +0,0 @@
-/*@
- requires IsValidRange(a, m);
- requires IsValidRange(b, n);
- assigns \nothing;
-
- behavior found:
- assumes HasValueOf(a, m, b, n);
- ensures (0 <= \result < m);
- ensures HasValue(b, n, a[\result]);
- ensures !HasValueOf(a, \result, b, n);
-
- behavior not_found:
- assumes !HasValueOf(a, m, b, n);
- ensures \result == m;
-
- complete behaviors;
- disjoint behaviors;
-*/
-size_type find_first_of(const value_type* a, size_type m,
- const value_type* b, size_type n);
diff --git a/src/plugins/wp/doc/tutorial/findfirst/findfirst.tex b/src/plugins/wp/doc/tutorial/findfirst/findfirst.tex
deleted file mode 100644
index 8911c7c0038..00000000000
--- a/src/plugins/wp/doc/tutorial/findfirst/findfirst.tex
+++ /dev/null
@@ -1,25 +0,0 @@
-\section{The \textsf{find-first-of} Algorithm}
-\label{find-first-of}
-
-This algorithm is an extension of \texttt{find}: it looks for the
-first element of sequence $a$ that belongs to sequence $b$. We also
-makes use of the \texttt{HasValue} predicate. But we also need its
-extension to sequence, as in the original specification from
-``ACSL By Example'':
-
-\listingname{findfirst.h}
-\cinput{findfirst/hasvalueof.spec}
-
-The specification of the algorithm is:
-
-\listingname{findfirst.h}
-\cinput{findfirst/findfirst.spec}
-
-The implementation of the algorithm is:
-
-\listingname{findfirst.c}
-\cinput{findfirst/findfirst.impl}
-
-The implementation is proved correct against its specification by
-simply running the \textsf{WP} plug-in:
-\fclogs{nonmutating}{findfirst}
diff --git a/src/plugins/wp/doc/tutorial/findfirst/findfirst_report.tex b/src/plugins/wp/doc/tutorial/findfirst/findfirst_report.tex
deleted file mode 100644
index d70d08a0506..00000000000
--- a/src/plugins/wp/doc/tutorial/findfirst/findfirst_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+find_first_of+ & 26 & 16 & 10 & 100\% (101) \\
diff --git a/src/plugins/wp/doc/tutorial/findfirst/hasvalueof.spec b/src/plugins/wp/doc/tutorial/findfirst/hasvalueof.spec
deleted file mode 100644
index 9feb4e9a420..00000000000
--- a/src/plugins/wp/doc/tutorial/findfirst/hasvalueof.spec
+++ /dev/null
@@ -1,6 +0,0 @@
-/*@
- predicate HasValueOf{A}(value_type* a, integer m,
- value_type* b, integer n) =
- \exists integer i; 0 <= i < m &&
- HasValue{A}(b, n, \at(a[i],A));
-*/
diff --git a/src/plugins/wp/doc/tutorial/iota/iota.c b/src/plugins/wp/doc/tutorial/iota/iota.c
deleted file mode 100644
index 00e7267a3db..00000000000
--- a/src/plugins/wp/doc/tutorial/iota/iota.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "iota.h"
-#include "iota.impl"
diff --git a/src/plugins/wp/doc/tutorial/iota/iota.h b/src/plugins/wp/doc/tutorial/iota/iota.h
deleted file mode 100644
index 9a04eada1be..00000000000
--- a/src/plugins/wp/doc/tutorial/iota/iota.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef _IOTA_H
-#define _IOTA_H
-#include "../library.h"
-#include "iota.spec"
-#endif
-
diff --git a/src/plugins/wp/doc/tutorial/iota/iota.impl b/src/plugins/wp/doc/tutorial/iota/iota.impl
deleted file mode 100644
index a88a675487a..00000000000
--- a/src/plugins/wp/doc/tutorial/iota/iota.impl
+++ /dev/null
@@ -1,14 +0,0 @@
-void iota(value_type* a, size_type n, value_type val)
-{
- /*@
-
- loop invariant 0 <= i <= n;
- loop assigns i, a[0..n-1];
-
- loop invariant \forall integer k; 0 <= k < i
- ==> a[k] == val + k;
- loop variant n-i;
- */
- for (size_type i = 0; i < n; i++)
- a[i] = val + i;
-}
diff --git a/src/plugins/wp/doc/tutorial/iota/iota.spec b/src/plugins/wp/doc/tutorial/iota/iota.spec
deleted file mode 100644
index 8ecc4240c22..00000000000
--- a/src/plugins/wp/doc/tutorial/iota/iota.spec
+++ /dev/null
@@ -1,9 +0,0 @@
-/*@
- requires IsValidRange(a, n);
- requires val + n < 2147483647 ; // INT_MAX
-
- assigns a[0..n-1];
-
- ensures \forall integer k; 0 <= k < n ==> a[k] == val + k;
-*/
-void iota(value_type* a, size_type n, value_type val);
\ No newline at end of file
diff --git a/src/plugins/wp/doc/tutorial/iota/iota.tex b/src/plugins/wp/doc/tutorial/iota/iota.tex
deleted file mode 100644
index b1cca9dccbb..00000000000
--- a/src/plugins/wp/doc/tutorial/iota/iota.tex
+++ /dev/null
@@ -1,23 +0,0 @@
-\clearpage
-\section{The \textsf{iota} Algorithm}
-\label{iota}
-
-We now study the \texttt{iota} algorithm from ``ACSL By Example''.
-This algorithm assigns sequentially increasing values to a range, with a
-user-defined start value.
-
-We slightly modify the specification of the \texttt{iota} algorithm
-to replace the \texttt{INT\_MAX} macro-definition by its value on 32-bit
-architectures:
-
-\listingname{iota.h}
-\cinput{iota/iota.spec}
-
-The implementation of the algorithm is:
-
-\listingname{iota.c}
-\cinput{iota/iota.impl}
-
-The implementation is proved correct against its specification by
-running the \textsf{WP} plug-in:
-\fclogs{mutating}{iota}
diff --git a/src/plugins/wp/doc/tutorial/iota/iota_report.tex b/src/plugins/wp/doc/tutorial/iota/iota_report.tex
deleted file mode 100644
index e2eaac29659..00000000000
--- a/src/plugins/wp/doc/tutorial/iota/iota_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+iota+ & 16 & 5 & 11 & 100\% (91) \\
diff --git a/src/plugins/wp/doc/tutorial/library.h b/src/plugins/wp/doc/tutorial/library.h
deleted file mode 100644
index 05ed0eccfbf..00000000000
--- a/src/plugins/wp/doc/tutorial/library.h
+++ /dev/null
@@ -1,4 +0,0 @@
-#ifndef _LIBRARY_H
-#define _LIBRARY_H
-#include "library.spec"
-#endif
diff --git a/src/plugins/wp/doc/tutorial/library.spec b/src/plugins/wp/doc/tutorial/library.spec
deleted file mode 100644
index 389cbfad428..00000000000
--- a/src/plugins/wp/doc/tutorial/library.spec
+++ /dev/null
@@ -1,11 +0,0 @@
-typedef int value_type;
-typedef int size_type;
-typedef int bool;
-
-/*@ predicate IsValidRange(value_type* a, integer n) =
- @ (0 <= n) && \valid(a+(0..n-1));
- @*/
-
-/*@ predicate IsEqual{A,B}(value_type* a, integer n, value_type* b) =
- @ \forall integer i; 0 <= i < n ==> \at(a[i], A) == \at(b[i], B) ;
- @*/
diff --git a/src/plugins/wp/doc/tutorial/lowerbound/lowerbound.c b/src/plugins/wp/doc/tutorial/lowerbound/lowerbound.c
deleted file mode 100644
index 5651556635a..00000000000
--- a/src/plugins/wp/doc/tutorial/lowerbound/lowerbound.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "lowerbound.h"
-#include "lowerbound.impl"
diff --git a/src/plugins/wp/doc/tutorial/lowerbound/lowerbound.h b/src/plugins/wp/doc/tutorial/lowerbound/lowerbound.h
deleted file mode 100644
index 4ca3f6079cd..00000000000
--- a/src/plugins/wp/doc/tutorial/lowerbound/lowerbound.h
+++ /dev/null
@@ -1,5 +0,0 @@
-#ifndef LOWERBOUND_H
-#define LOWERBOUND_H
-#include "../binary/binary.h"
-#include "lowerbound.spec"
-#endif
diff --git a/src/plugins/wp/doc/tutorial/lowerbound/lowerbound.impl b/src/plugins/wp/doc/tutorial/lowerbound/lowerbound.impl
deleted file mode 100644
index 2c93372d5e7..00000000000
--- a/src/plugins/wp/doc/tutorial/lowerbound/lowerbound.impl
+++ /dev/null
@@ -1,23 +0,0 @@
-size_type lower_bound(const value_type *a, size_type n, value_type val)
-{
- size_type left = 0;
- size_type right = n;
- size_type middle = 0;
-
- /*@
- loop invariant 0 <= left <= right <= n;
- loop invariant \forall integer i; 0 <= i < left ==> a[i] < val;
- loop invariant \forall integer i; right <= i < n ==> val <= a[i];
- loop assigns middle,left,right;
- loop variant right - left;
- */
- while (left < right) {
- middle = left + (right - left) / 2;
- if (a[middle] < val)
- left = middle + 1;
- else
- right = middle;
- }
-
- return left;
-}
diff --git a/src/plugins/wp/doc/tutorial/lowerbound/lowerbound.spec b/src/plugins/wp/doc/tutorial/lowerbound/lowerbound.spec
deleted file mode 100644
index c92ff8d0a59..00000000000
--- a/src/plugins/wp/doc/tutorial/lowerbound/lowerbound.spec
+++ /dev/null
@@ -1,11 +0,0 @@
-/*@
- requires IsValidRange(a, n);
- requires IsSorted(a, n);
-
- assigns \nothing;
-
- ensures 0 <= \result <= n;
- ensures \forall integer k; 0 <= k < \result ==> a[k] < val;
- ensures \forall integer k; \result <= k < n ==> val <= a[k];
-*/
-size_type lower_bound(const value_type* a, size_type n, value_type val);
diff --git a/src/plugins/wp/doc/tutorial/lowerbound/lowerbound.tex b/src/plugins/wp/doc/tutorial/lowerbound/lowerbound.tex
deleted file mode 100644
index 5f8d9314763..00000000000
--- a/src/plugins/wp/doc/tutorial/lowerbound/lowerbound.tex
+++ /dev/null
@@ -1,26 +0,0 @@
-\clearpage
-\section{The \textsf{lower-bound} algorithm}
-
-We study here the \texttt{lower-bound}
-algorithm from ``ACSL By Example''.
-Its specification is:
-
-\listingname{lowerbound.h}
-\cinput{lowerbound/lowerbound.spec}
-
-The implementation of the algorithm is:
-
-\listingname{lowerbound.c}
-\cinput{lowerbound/lowerbound.impl}
-
-\paragraph{Remark:} the original specification of loop-assigns in ``ACSL By Example''
-is \emph{wrong} since the loop \emph{do} assigns the local variables
-of the function. The original specification works with \textsf{Jessie}
-since local variables rarely live in the assignable heap, but it is
-not correct for \textsf{WP} where assigns clauses are more strictly
-verified.
-
-The implementation is proved correct against its specification by
-simply running the \textsf{WP} plug-in:
-\fclogs{binary}{lowerbound}
-
diff --git a/src/plugins/wp/doc/tutorial/lowerbound/lowerbound_report.tex b/src/plugins/wp/doc/tutorial/lowerbound/lowerbound_report.tex
deleted file mode 100644
index 4d77444a0af..00000000000
--- a/src/plugins/wp/doc/tutorial/lowerbound/lowerbound_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+lower_bound+ & 22 & 9 & 13 & 100\% (198) \\
diff --git a/src/plugins/wp/doc/tutorial/maxelt/maxelt.c b/src/plugins/wp/doc/tutorial/maxelt/maxelt.c
deleted file mode 100644
index 2f0974f61f5..00000000000
--- a/src/plugins/wp/doc/tutorial/maxelt/maxelt.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "maxelt.h"
-#include "maxelt.impl"
diff --git a/src/plugins/wp/doc/tutorial/maxelt/maxelt.h b/src/plugins/wp/doc/tutorial/maxelt/maxelt.h
deleted file mode 100644
index cbb75f978f9..00000000000
--- a/src/plugins/wp/doc/tutorial/maxelt/maxelt.h
+++ /dev/null
@@ -1,5 +0,0 @@
-#ifndef MAXELT_H
-#define MAXELT_H
-#include "../library.h"
-#include "maxelt.spec"
-#endif
diff --git a/src/plugins/wp/doc/tutorial/maxelt/maxelt.impl b/src/plugins/wp/doc/tutorial/maxelt/maxelt.impl
deleted file mode 100644
index 6b92f962d88..00000000000
--- a/src/plugins/wp/doc/tutorial/maxelt/maxelt.impl
+++ /dev/null
@@ -1,19 +0,0 @@
-size_type max_element(const value_type* a, size_type n)
-{
- if (n == 0) return 0;
-
- size_type max = 0;
- /*@
- loop invariant 0 <= i <= n;
- loop invariant 0 <= max < n;
- loop invariant \forall integer k; 0 <= k < i ==> a[k] <= a[max];
- loop invariant \forall integer k; 0 <= k < max ==> a[k] < a[max];
- loop assigns max,i;
- loop variant n-i;
- */
- for (size_type i = 0; i < n; i++)
- if (a[max] < a[i])
- max = i;
-
- return max;
-}
diff --git a/src/plugins/wp/doc/tutorial/maxelt/maxelt.spec b/src/plugins/wp/doc/tutorial/maxelt/maxelt.spec
deleted file mode 100644
index 876bd28bfa3..00000000000
--- a/src/plugins/wp/doc/tutorial/maxelt/maxelt.spec
+++ /dev/null
@@ -1,18 +0,0 @@
-/*@
- requires IsValidRange(a, n);
- assigns \nothing;
-
- behavior empty:
- assumes n == 0;
- ensures \result == 0;
-
- behavior not_empty:
- assumes 0 < n;
- ensures 0 <= \result < n;
- ensures \forall integer i; 0 <= i < n ==> a[i] <= a[\result];
- ensures \forall integer i; 0 <= i < \result ==> a[i] < a[\result];
-
- complete behaviors;
- disjoint behaviors;
-*/
-size_type max_element(const value_type* a, size_type n);
diff --git a/src/plugins/wp/doc/tutorial/maxelt/maxelt.tex b/src/plugins/wp/doc/tutorial/maxelt/maxelt.tex
deleted file mode 100644
index 8ae31ba54ac..00000000000
--- a/src/plugins/wp/doc/tutorial/maxelt/maxelt.tex
+++ /dev/null
@@ -1,19 +0,0 @@
-\section{The \textsf{max-element} Algorithm}
-\label{max-element}
-
-We study now the first version of the \texttt{max-element}
-algorithm from ``ACSL By Example''.
-The specification of the \texttt{max-element} algorithm is as follows:
-
-\listingname{maxelt.h}
-\cinput{maxelt/maxelt.spec}
-
-The implementation of the algorithm is:
-
-\listingname{maxelt.c}
-\cinput{maxelt/maxelt.impl}
-
-The implementation is proved correct against its specification by
-simply running the \textsf{WP} plug-in:
-\fclogs{maxmin}{maxelt}
-
diff --git a/src/plugins/wp/doc/tutorial/maxelt/maxelt_report.tex b/src/plugins/wp/doc/tutorial/maxelt/maxelt_report.tex
deleted file mode 100644
index 741718dd777..00000000000
--- a/src/plugins/wp/doc/tutorial/maxelt/maxelt_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+max_element+ & 25 & 13 & 12 & 100\% (119) \\
diff --git a/src/plugins/wp/doc/tutorial/maxeltp/maxelt.c b/src/plugins/wp/doc/tutorial/maxeltp/maxelt.c
deleted file mode 100644
index 2f0974f61f5..00000000000
--- a/src/plugins/wp/doc/tutorial/maxeltp/maxelt.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "maxelt.h"
-#include "maxelt.impl"
diff --git a/src/plugins/wp/doc/tutorial/maxeltp/maxelt.h b/src/plugins/wp/doc/tutorial/maxeltp/maxelt.h
deleted file mode 100644
index c0b3da8c7c5..00000000000
--- a/src/plugins/wp/doc/tutorial/maxeltp/maxelt.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef MAXELT_H
-#define MAXELT_H
-#include "../library.h"
-#include "maximum.spec"
-#include "maxelt.spec"
-#endif
diff --git a/src/plugins/wp/doc/tutorial/maxeltp/maxelt.impl b/src/plugins/wp/doc/tutorial/maxeltp/maxelt.impl
deleted file mode 100644
index a6dafbeadef..00000000000
--- a/src/plugins/wp/doc/tutorial/maxeltp/maxelt.impl
+++ /dev/null
@@ -1,19 +0,0 @@
-size_type max_element(const value_type* a, size_type n)
-{
- if (n == 0) return 0;
-
- size_type max = 0;
- /*@
- loop invariant 0 <= i <= n;
- loop invariant 0 <= max < n;
- loop invariant IsMaximum(a, i, max);
- loop invariant IsFirstMaximum(a, max);
- loop assigns i,max;
- loop variant n-i;
- */
- for (size_type i = 0; i < n; i++)
- if (a[max] < a[i])
- max = i;
-
- return max;
-}
diff --git a/src/plugins/wp/doc/tutorial/maxeltp/maxelt.report b/src/plugins/wp/doc/tutorial/maxeltp/maxelt.report
deleted file mode 100644
index 4d0ffbba1fe..00000000000
--- a/src/plugins/wp/doc/tutorial/maxeltp/maxelt.report
+++ /dev/null
@@ -1,5 +0,0 @@
-@SUFFIX "_report.tex"
-@ZERO "-"
-@FUNCTION
-\textit{max with predicates} & %total & %wp & %ergo & %success\% (%time) \\
-@END
diff --git a/src/plugins/wp/doc/tutorial/maxeltp/maxelt.spec b/src/plugins/wp/doc/tutorial/maxeltp/maxelt.spec
deleted file mode 100644
index c7fb3459b99..00000000000
--- a/src/plugins/wp/doc/tutorial/maxeltp/maxelt.spec
+++ /dev/null
@@ -1,17 +0,0 @@
-/*@
- requires IsValidRange(a, n);
- assigns \nothing;
-
- behavior empty:
- assumes n == 0;
- ensures \result == 0;
-
- behavior not_empty:
- assumes 0 < n;
- ensures 0 <= \result < n;
- ensures IsMaximum(a, n, \result);
- ensures IsFirstMaximum(a, \result);
-
- complete behaviors; disjoint behaviors;
-*/
-size_type max_element(const value_type* a, size_type n);
diff --git a/src/plugins/wp/doc/tutorial/maxeltp/maxelt.tex b/src/plugins/wp/doc/tutorial/maxeltp/maxelt.tex
deleted file mode 100644
index 3e2d87fc879..00000000000
--- a/src/plugins/wp/doc/tutorial/maxeltp/maxelt.tex
+++ /dev/null
@@ -1,25 +0,0 @@
-\section{The \textsf{max-element} Algorithm with Predicates}
-\label{max-element-pred}
-
-We study now the \emph{reconsidered} version of the \texttt{max-element}
-algorithm from ``ACSL By Example'' with predicates:
-
-\listingname{maximum.spec}
-\cinput{maxeltp/maximum.spec}
-
-Remark that we rephrased the original specification of \texttt{IsMaximum}.
-The specification of the \texttt{max-element} algorithm
-becomes:
-
-\listingname{maxelt.h}
-\cinput{maxeltp/maxelt.spec}
-
-The implementation of the algorithm is now:
-
-\listingname{maxelt.c}
-\cinput{maxeltp/maxelt.impl}
-
-The implementation is proved correct against its specification by
-running the \textsf{WP} plug-in:
-\fclogs{maxmin}{maxeltp}
-
diff --git a/src/plugins/wp/doc/tutorial/maxeltp/maxelt_report.tex b/src/plugins/wp/doc/tutorial/maxeltp/maxelt_report.tex
deleted file mode 100644
index 52169f842f7..00000000000
--- a/src/plugins/wp/doc/tutorial/maxeltp/maxelt_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\textit{max with predicates} & 25 & 12 & 13 & 100\% (1s) \\
diff --git a/src/plugins/wp/doc/tutorial/maxeltp/maximum.spec b/src/plugins/wp/doc/tutorial/maxeltp/maximum.spec
deleted file mode 100644
index 7576b4d86b2..00000000000
--- a/src/plugins/wp/doc/tutorial/maxeltp/maximum.spec
+++ /dev/null
@@ -1,7 +0,0 @@
-/*@
- predicate IsMaximum{L}(value_type* a, integer n, integer max) =
- !(\exists integer i; 0 <= i < n && (a[max] < a[i]));
-
- predicate IsFirstMaximum{L}(value_type* a, integer max) =
- \forall integer i; 0 <= i < max ==> a[i] < a[max];
-*/
\ No newline at end of file
diff --git a/src/plugins/wp/doc/tutorial/maxseq/maxseq.c b/src/plugins/wp/doc/tutorial/maxseq/maxseq.c
deleted file mode 100644
index b847d485ed8..00000000000
--- a/src/plugins/wp/doc/tutorial/maxseq/maxseq.c
+++ /dev/null
@@ -1,3 +0,0 @@
-#include "maxseq.h"
-#include "../maxeltp/maxelt.h"
-#include "maxseq.impl"
diff --git a/src/plugins/wp/doc/tutorial/maxseq/maxseq.h b/src/plugins/wp/doc/tutorial/maxseq/maxseq.h
deleted file mode 100644
index b656136af23..00000000000
--- a/src/plugins/wp/doc/tutorial/maxseq/maxseq.h
+++ /dev/null
@@ -1,5 +0,0 @@
-#ifndef MAXSEQ_H
-#define MAXSEQ_H
-#include "../library.h"
-#include "maxseq.spec"
-#endif
diff --git a/src/plugins/wp/doc/tutorial/maxseq/maxseq.impl b/src/plugins/wp/doc/tutorial/maxseq/maxseq.impl
deleted file mode 100644
index 6df811c7c29..00000000000
--- a/src/plugins/wp/doc/tutorial/maxseq/maxseq.impl
+++ /dev/null
@@ -1,4 +0,0 @@
-size_type max_seq(const value_type* a, size_type n)
-{
- return a[max_element(a,n)];
-}
diff --git a/src/plugins/wp/doc/tutorial/maxseq/maxseq.spec b/src/plugins/wp/doc/tutorial/maxseq/maxseq.spec
deleted file mode 100644
index dfe720cdefd..00000000000
--- a/src/plugins/wp/doc/tutorial/maxseq/maxseq.spec
+++ /dev/null
@@ -1,9 +0,0 @@
-/*@
- requires n>0 ;
- requires IsValidRange(a, n);
- assigns \nothing;
-
- ensures \forall integer i; 0 <= i <= n-1 ==> \result >= a[i];
- ensures \exists integer e; 0 <= e <= n-1 && \result == a[e];
-*/
-size_type max_seq(const value_type* a, size_type n);
diff --git a/src/plugins/wp/doc/tutorial/maxseq/maxseq.tex b/src/plugins/wp/doc/tutorial/maxseq/maxseq.tex
deleted file mode 100644
index a57ed273c7c..00000000000
--- a/src/plugins/wp/doc/tutorial/maxseq/maxseq.tex
+++ /dev/null
@@ -1,22 +0,0 @@
-\section{The \textsf{max-seq} Algorithm}
-\label{max-seq}
-
-We study now the \texttt{max-seq} algorithm from ``ACSL By Example''.
-Its specification is to return the maximal value in a sequence, not
-its index like in the \texttt{max-element} algorithm.
-
-The specification is as follows:
-
-\listingname{maxseq.h}
-\cinput{maxseq/maxseq.spec}
-
-The algorithm is implemented in terms of algorithm
-\texttt{max-element}, as follows:
-
-\listingname{maxseq.c}
-\cinput{maxseq/maxseq.impl}
-
-The implementation is proved correct against its specification thanks to the
-specification of the \texttt{max-element} function:
-\fclogs{maxmin}{maxseq}
-
diff --git a/src/plugins/wp/doc/tutorial/maxseq/maxseq_report.tex b/src/plugins/wp/doc/tutorial/maxseq/maxseq_report.tex
deleted file mode 100644
index c8191f091f4..00000000000
--- a/src/plugins/wp/doc/tutorial/maxseq/maxseq_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+max_seq+ & 8 & 5 & 3 & 100\% (55) \\
diff --git a/src/plugins/wp/doc/tutorial/minelt/minelt.c b/src/plugins/wp/doc/tutorial/minelt/minelt.c
deleted file mode 100644
index 07b4f320690..00000000000
--- a/src/plugins/wp/doc/tutorial/minelt/minelt.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "minelt.h"
-#include "minelt.impl"
diff --git a/src/plugins/wp/doc/tutorial/minelt/minelt.h b/src/plugins/wp/doc/tutorial/minelt/minelt.h
deleted file mode 100644
index 7d67cdf7476..00000000000
--- a/src/plugins/wp/doc/tutorial/minelt/minelt.h
+++ /dev/null
@@ -1,5 +0,0 @@
-#ifndef MINELT_H
-#define MINELT_H
-#include "../library.h"
-#include "minelt.spec"
-#endif
diff --git a/src/plugins/wp/doc/tutorial/minelt/minelt.impl b/src/plugins/wp/doc/tutorial/minelt/minelt.impl
deleted file mode 100644
index 347716f761f..00000000000
--- a/src/plugins/wp/doc/tutorial/minelt/minelt.impl
+++ /dev/null
@@ -1,19 +0,0 @@
-size_type min_element(const value_type* a, size_type n)
-{
- if (n == 0) return 0;
-
- size_type min = 0;
- /*@
- loop invariant 0 <= i <= n;
- loop invariant 0 <= min < n;
- loop invariant \forall integer k; 0 <= k < i ==> a[min] <= a[k];
- loop invariant \forall integer k; 0 <= k < min ==> a[min] < a[k];
- loop assigns i,min;
- loop variant n-i;
- */
- for (size_type i = 0; i < n; i++)
- if (a[i] < a[min])
- min = i;
-
- return min;
-}
diff --git a/src/plugins/wp/doc/tutorial/minelt/minelt.spec b/src/plugins/wp/doc/tutorial/minelt/minelt.spec
deleted file mode 100644
index ff1166419c8..00000000000
--- a/src/plugins/wp/doc/tutorial/minelt/minelt.spec
+++ /dev/null
@@ -1,18 +0,0 @@
-/*@
- requires IsValidRange(a, n);
- assigns \nothing;
-
- behavior empty:
- assumes n == 0;
- ensures \result == 0;
-
- behavior not_empty:
- assumes 0 < n;
- ensures 0 <= \result < n;
- ensures \forall integer i; 0 <= i < n ==> a[\result] <= a[i];
- ensures \forall integer i; 0 <= i < \result ==> a[\result] < a[i];
-
- complete behaviors;
- disjoint behaviors;
-*/
-size_type min_element(const value_type* a, size_type n);
diff --git a/src/plugins/wp/doc/tutorial/minelt/minelt.tex b/src/plugins/wp/doc/tutorial/minelt/minelt.tex
deleted file mode 100644
index 04d70543f78..00000000000
--- a/src/plugins/wp/doc/tutorial/minelt/minelt.tex
+++ /dev/null
@@ -1,20 +0,0 @@
-\clearpage
-\section{The \textsf{min-element} Algorithm}
-\label{min-element}
-
-We study now the first version of the \texttt{min-element}
-algorithm from ``ACSL By Example''.
-The specification of the \texttt{min-element} algorithm:
-
-\listingname{minelt.h}
-\cinput{minelt/minelt.spec}
-
-The implementation of the algorithm is:
-
-\listingname{minelt.c}
-\cinput{minelt/minelt.impl}
-
-The implementation is proved correct against its specification by
-simply running the \textsf{WP} plug-in:
-\fclogs{maxmin}{minelt}
-
diff --git a/src/plugins/wp/doc/tutorial/minelt/minelt_report.tex b/src/plugins/wp/doc/tutorial/minelt/minelt_report.tex
deleted file mode 100644
index bff388eed3e..00000000000
--- a/src/plugins/wp/doc/tutorial/minelt/minelt_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+min_element+ & 25 & 13 & 12 & 100\% (119) \\
diff --git a/src/plugins/wp/doc/tutorial/mismatch/eqmismatch.report b/src/plugins/wp/doc/tutorial/mismatch/eqmismatch.report
deleted file mode 100644
index 62953448443..00000000000
--- a/src/plugins/wp/doc/tutorial/mismatch/eqmismatch.report
+++ /dev/null
@@ -1,5 +0,0 @@
-@SUFFIX "_report.tex"
-@ZERO "-"
-@FUNCTION
-\verb+equal+ (mismatch) & %total & %wp & %ergo & %success\% (%time) \\
-@END
diff --git a/src/plugins/wp/doc/tutorial/mismatch/eqmismatch_report.tex b/src/plugins/wp/doc/tutorial/mismatch/eqmismatch_report.tex
deleted file mode 100644
index a47029927cd..00000000000
--- a/src/plugins/wp/doc/tutorial/mismatch/eqmismatch_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+equal+ (mismatch) & 7 & 6 & 1 & 100\% (1s) \\
diff --git a/src/plugins/wp/doc/tutorial/mismatch/equal.c b/src/plugins/wp/doc/tutorial/mismatch/equal.c
deleted file mode 100644
index 0d8279753d7..00000000000
--- a/src/plugins/wp/doc/tutorial/mismatch/equal.c
+++ /dev/null
@@ -1,8 +0,0 @@
-#include "mismatch.h"
-#include "../equal/equal.h"
-bool equal(const value_type* p, size_type m, const value_type* q)
-{
- return mismatch(p, m, q) == m;
-}
-
-
diff --git a/src/plugins/wp/doc/tutorial/mismatch/mismatch.c b/src/plugins/wp/doc/tutorial/mismatch/mismatch.c
deleted file mode 100644
index 31308027dc6..00000000000
--- a/src/plugins/wp/doc/tutorial/mismatch/mismatch.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "mismatch.h"
-#include "mismatch.impl"
diff --git a/src/plugins/wp/doc/tutorial/mismatch/mismatch.h b/src/plugins/wp/doc/tutorial/mismatch/mismatch.h
deleted file mode 100644
index ef3a0bba86a..00000000000
--- a/src/plugins/wp/doc/tutorial/mismatch/mismatch.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef _MISMATCH_H
-#define _MISMATCH_H
-#include "../library.h"
-#include "mismatch.spec"
-#endif
-
diff --git a/src/plugins/wp/doc/tutorial/mismatch/mismatch.impl b/src/plugins/wp/doc/tutorial/mismatch/mismatch.impl
deleted file mode 100644
index 20e70af48c4..00000000000
--- a/src/plugins/wp/doc/tutorial/mismatch/mismatch.impl
+++ /dev/null
@@ -1,14 +0,0 @@
-size_type mismatch(const value_type* a, size_type n, const value_type* b)
-{
- /*@
- loop invariant 0 <= i <= n;
- loop invariant IsEqual{Here,Here}(a, i, b);
- loop assigns i;
- loop variant n-i;
- */
- for (size_type i = 0; i < n; i++)
- if (a[i] != b[i])
- return i;
- return n;
-}
-
diff --git a/src/plugins/wp/doc/tutorial/mismatch/mismatch.spec b/src/plugins/wp/doc/tutorial/mismatch/mismatch.spec
deleted file mode 100644
index a8779c18ec4..00000000000
--- a/src/plugins/wp/doc/tutorial/mismatch/mismatch.spec
+++ /dev/null
@@ -1,20 +0,0 @@
-/*@
- requires IsValidRange(a, n);
- requires IsValidRange(b, n);
-
- assigns \nothing;
-
- behavior all_equal:
- assumes IsEqual{Here,Here}(a, n, b);
- ensures \result == n;
-
- behavior some_not_equal:
- assumes !IsEqual{Here,Here}(a, n, b);
- ensures 0 <= \result < n;
- ensures a[\result] != b[\result];
- ensures IsEqual{Here,Here}(a, \result, b);
-
- complete behaviors;
- disjoint behaviors;
-*/
-size_type mismatch(const value_type* a, size_type n, const value_type* b);
diff --git a/src/plugins/wp/doc/tutorial/mismatch/mismatch.tex b/src/plugins/wp/doc/tutorial/mismatch/mismatch.tex
deleted file mode 100644
index 96be419b4b4..00000000000
--- a/src/plugins/wp/doc/tutorial/mismatch/mismatch.tex
+++ /dev/null
@@ -1,34 +0,0 @@
-\clearpage
-\section{The \textsf{mismatch} Algorithm}
-
-We now present the \texttt{mismatch} algorithm that returns the index
-of the first different element between two sequences, and (-1) otherwise.
-
-\listingname{mismatch.h}
-\cinput{mismatch/mismatch.spec}
-
-The implementation is simply:
-
-\listingname{mismatch.c}
-\cinput{mismatch/mismatch.impl}
-
-Once again, \textsf{WP} simply proves the algorithm:
-\fclogs{nonmutating}{mismatch}
-
-\clearpage
-\section{Alternate \textsf{equal} with \textsf{mismatch}}
-
-It is also possible to implement the \texttt{equal} algorithm in terms
-of \texttt{mismatch}. Using the same specification file given for
-\texttt{equal} in \ref{equal}, the implementation is now:
-
-\listingname{equal.c [alt]}
-\cinput{mismatch/equal.c}
-
-The entire program is proven correct by \textsf{WP} plug-in (here,
-the proofs steps for function \texttt{mismatch} are omitted):
-\fclogs{nonmutating}{eqmismatch}
-
-As the reader may observe, the \textsf{WP} has proven the precondition
-of \texttt{mismatch} from the one of \texttt{equal}, and the
-post-condition of \texttt{equal} from the one of \texttt{mismatch}.
diff --git a/src/plugins/wp/doc/tutorial/mismatch/mismatch_report.tex b/src/plugins/wp/doc/tutorial/mismatch/mismatch_report.tex
deleted file mode 100644
index 40749040ebf..00000000000
--- a/src/plugins/wp/doc/tutorial/mismatch/mismatch_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+mismatch+ & 20 & 9 & 11 & 100\% (79) \\
diff --git a/src/plugins/wp/doc/tutorial/ptests_local_config.in b/src/plugins/wp/doc/tutorial/ptests_local_config.in
deleted file mode 100644
index 340c6454f72..00000000000
--- a/src/plugins/wp/doc/tutorial/ptests_local_config.in
+++ /dev/null
@@ -1,6 +0,0 @@
-DEFAULT_SUITES=nonmutating maxmin binary mutating
-TOPLEVEL_PATH=frama-c
-FRAMAC_SHARE=@SHARE_PATH@
-FRAMAC_LIBC=@LIB_PATH@
-FRAMAC_PLUGIN=.
-FRAMAC_PLUGIN_GUI=./gui
diff --git a/src/plugins/wp/doc/tutorial/removecopy/original.axioms b/src/plugins/wp/doc/tutorial/removecopy/original.axioms
deleted file mode 100644
index e3d60afaa38..00000000000
--- a/src/plugins/wp/doc/tutorial/removecopy/original.axioms
+++ /dev/null
@@ -1,22 +0,0 @@
-/*@
- axiomatic WhitherRemove_Function
- {
- logic integer WhitherRemove{L}(value_type* a, value_type v,
- integer i) reads a[0..(i-1)];
-
- axiom whither_1:
- \forall value_type *a, v; WhitherRemove(a, v, 0) == 0;
-
- axiom whither_2:
- \forall value_type *a, v, integer i; a[i] == v ==>
- WhitherRemove(a, v, i+1) == WhitherRemove(a, v, i);
-
- axiom whither_3:
- \forall value_type *a, v, integer i; a[i] != v ==>
- WhitherRemove(a, v, i+1) == WhitherRemove(a, v, i) + 1;
-
- axiom whither_lemma:
- \forall value_type *a, v, integer i, j; i < j && a[i] != v ==>
- WhitherRemove(a, v, i) < WhitherRemove(a, v, j);
- }
-*/
diff --git a/src/plugins/wp/doc/tutorial/removecopy/removecopy.axioms b/src/plugins/wp/doc/tutorial/removecopy/removecopy.axioms
deleted file mode 100644
index 7f4c67e868f..00000000000
--- a/src/plugins/wp/doc/tutorial/removecopy/removecopy.axioms
+++ /dev/null
@@ -1,22 +0,0 @@
-/*@
- axiomatic WhitherRemove_Function
- {
- logic integer WhitherRemove{L}(value_type* a, value_type v,
- integer i) reads a[0], a[i-1];
-
- axiom whither_1:
- \forall value_type *a, v; WhitherRemove(a, v, 0) == 0;
-
- axiom whither_2:
- \forall value_type *a, v, integer i; a[i] == v ==>
- WhitherRemove(a, v, i+1) == WhitherRemove(a, v, i);
-
- axiom whither_3:
- \forall value_type *a, v, integer i; a[i] != v ==>
- WhitherRemove(a, v, i+1) == WhitherRemove(a, v, i) + 1;
-
- axiom whither_lemma:
- \forall value_type *a, v, integer i, j; i < j && a[i] != v ==>
- WhitherRemove(a, v, i) < WhitherRemove(a, v, j);
- }
-*/
diff --git a/src/plugins/wp/doc/tutorial/removecopy/removecopy.c b/src/plugins/wp/doc/tutorial/removecopy/removecopy.c
deleted file mode 100644
index a03905b4b3c..00000000000
--- a/src/plugins/wp/doc/tutorial/removecopy/removecopy.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "removecopy.h"
-#include "removecopy.impl"
diff --git a/src/plugins/wp/doc/tutorial/removecopy/removecopy.h b/src/plugins/wp/doc/tutorial/removecopy/removecopy.h
deleted file mode 100644
index 41847d52fca..00000000000
--- a/src/plugins/wp/doc/tutorial/removecopy/removecopy.h
+++ /dev/null
@@ -1,7 +0,0 @@
-#ifndef _REMOVECOPY_H
-#define _REMOVECOPY_H
-#include "../library.h"
-#include "removecopy.axioms"
-#include "removecopy.spec"
-#endif
-
diff --git a/src/plugins/wp/doc/tutorial/removecopy/removecopy.impl b/src/plugins/wp/doc/tutorial/removecopy/removecopy.impl
deleted file mode 100644
index 617b2828d18..00000000000
--- a/src/plugins/wp/doc/tutorial/removecopy/removecopy.impl
+++ /dev/null
@@ -1,16 +0,0 @@
-size_type remove_copy(const value_type* a, size_type n,
- value_type* b, value_type v)
-{
- size_type j = 0;
- /*@
- loop assigns b[0..j-1], i, j;
- loop invariant 0 <= j <= i <= n;
- loop invariant RemoveCopy(a, i, b, j, v);
- loop variant n-i;
- */
- for (size_type i = 0; i < n; i++) {
- if (a[i] != v)
- b[j++] = a[i];
- }
- return j;
-}
diff --git a/src/plugins/wp/doc/tutorial/removecopy/removecopy.spec b/src/plugins/wp/doc/tutorial/removecopy/removecopy.spec
deleted file mode 100644
index 43465a13665..00000000000
--- a/src/plugins/wp/doc/tutorial/removecopy/removecopy.spec
+++ /dev/null
@@ -1,22 +0,0 @@
-/*@
- predicate
- RemoveCopy{L}(value_type* a, integer n,
- value_type* b, integer m, value_type v) =
- m == WhitherRemove(a, v, n) &&
- \forall integer i;
- 0 <= i < n && a[i] != v ==> b[WhitherRemove(a, v, i)] == a[i];
-*/
-
-/*@
- requires IsValidRange(a, n);
- requires IsValidRange(b, n);
- requires \separated(a+(0..n-1), b+(0..n-1));
-
- assigns b[0..n-1];
-
- ensures \forall integer k; \result <= k < n ==> b[k] == \old(b[k]);
-
- ensures RemoveCopy(a, n, b, \result, val);
-*/
-size_type remove_copy(const value_type* a, size_type n,
- value_type* b, value_type val);
\ No newline at end of file
diff --git a/src/plugins/wp/doc/tutorial/removecopy/removecopy.tex b/src/plugins/wp/doc/tutorial/removecopy/removecopy.tex
deleted file mode 100644
index 97e150a2aed..00000000000
--- a/src/plugins/wp/doc/tutorial/removecopy/removecopy.tex
+++ /dev/null
@@ -1,40 +0,0 @@
-\section{The \textsf{remove-copy} Algorithm}
-\label{remove-copy}
-
-We now study the \texttt{remove-copy} algorithm from ``ACSL By Example''.
-This algorithm copies the contents from a source sequence to a destination
-sequence whilst removing elements having a given value. The return value is the
-length of the range.
-
-\subsection{Adapting the Axiomatics}
-
-The axiomatization provided in ``ACSL By Example'' is:
-
-\listingname{remove-copy.axioms}
-\cinput{removecopy/original.axioms}
-
-The predicate \texttt{WhitherRemove} is defined by a \texttt{read} clause.
-It must be adapted for the current version of the \textsf{WP} plug-in which
-only implements a limited subset of \texttt{read} clauses:
-
-\listingname{remove-copy.axioms [adapted]}
-\cinput{removecopy/removecopy.axioms}
-
-\subsection{Proving the Algorithm}
-
-The specification of the \texttt{remove-copy} algorithm bases itself on the
-\texttt{RemoveCopy} predicate, itself based on the \texttt{WhitherRemove}
-function:
-
-\listingname{removecopy.h}
-\cinput{removecopy/removecopy.spec}
-
-The implementation of the algorithm is:
-
-\listingname{removecopy.c}
-\cinput{removecopy/removecopy.impl}
-
-\clearpage
-The implementation can be partially proved correct against its specification by
-running the \textsf{WP} plug-in:
-\fclogs{mutating}{removecopy}
diff --git a/src/plugins/wp/doc/tutorial/removecopy/removecopy_report.tex b/src/plugins/wp/doc/tutorial/removecopy/removecopy_report.tex
deleted file mode 100644
index 4e08fe3c7fb..00000000000
--- a/src/plugins/wp/doc/tutorial/removecopy/removecopy_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+remove_copy+ & 20 & 7 & 11 & 90.0\% (496) \\
diff --git a/src/plugins/wp/doc/tutorial/replacecopy/replacecopy.c b/src/plugins/wp/doc/tutorial/replacecopy/replacecopy.c
deleted file mode 100644
index 1f19aba55c6..00000000000
--- a/src/plugins/wp/doc/tutorial/replacecopy/replacecopy.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "replacecopy.h"
-#include "replacecopy.impl"
diff --git a/src/plugins/wp/doc/tutorial/replacecopy/replacecopy.h b/src/plugins/wp/doc/tutorial/replacecopy/replacecopy.h
deleted file mode 100644
index c4e646d020a..00000000000
--- a/src/plugins/wp/doc/tutorial/replacecopy/replacecopy.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef _REPLACE_COPY_H
-#define _REPLACE_COPY_H
-#include "../library.h"
-#include "replacecopy.spec"
-#endif
-
diff --git a/src/plugins/wp/doc/tutorial/replacecopy/replacecopy.impl b/src/plugins/wp/doc/tutorial/replacecopy/replacecopy.impl
deleted file mode 100644
index dd41f3e81c6..00000000000
--- a/src/plugins/wp/doc/tutorial/replacecopy/replacecopy.impl
+++ /dev/null
@@ -1,19 +0,0 @@
-size_type replace_copy(const value_type* a, size_type n,
- value_type* b,
- value_type old_val, value_type new_val)
-{
- /*@
- loop invariant 0 <= i <= n;
-
- loop assigns i,b[0..i-1];
-
- loop invariant \forall integer j; 0 <= j < i ==>
- (a[j] == old_val && b[j] == new_val) ||
- (a[j] != old_val && b[j] == a[j]);
- loop variant n-i;
- */
- for(size_type i = 0; i < n; i++)
- b[i] = (a[i] == old_val ? new_val : a[i]);
-
- return n;
-}
diff --git a/src/plugins/wp/doc/tutorial/replacecopy/replacecopy.spec b/src/plugins/wp/doc/tutorial/replacecopy/replacecopy.spec
deleted file mode 100644
index b69f67eb5a4..00000000000
--- a/src/plugins/wp/doc/tutorial/replacecopy/replacecopy.spec
+++ /dev/null
@@ -1,15 +0,0 @@
-/*@
- requires IsValidRange(a, n);
- requires IsValidRange(b, n);
- requires \separated(a+(0..n-1), b+(0..n-1));
-
- assigns b[0..(n-1)];
-
- ensures \forall integer j; 0 <= j < n ==>
- (a[j] == old_val && b[j] == new_val) ||
- (a[j] != old_val && b[j] == a[j]);
- ensures \result == n;
-*/
-size_type replace_copy(const value_type* a, size_type n,
- value_type* b,
- value_type old_val, value_type new_val);
diff --git a/src/plugins/wp/doc/tutorial/replacecopy/replacecopy.tex b/src/plugins/wp/doc/tutorial/replacecopy/replacecopy.tex
deleted file mode 100644
index cecdd9632c0..00000000000
--- a/src/plugins/wp/doc/tutorial/replacecopy/replacecopy.tex
+++ /dev/null
@@ -1,21 +0,0 @@
-\section{The \textsf{replace-copy} Algorithm}
-\label{replace-copy}
-
-We now study the \texttt{replace-copy} algorithm from ``ACSL By Example''.
-This algorithm copies a source sequence to a destination sequence whilst
-substituting every occurrence of a given value by another value.
-
-The specification of the \texttt{replace-copy} algorithm is as follows:
-
-\listingname{replacecopy.h}
-\cinput{replacecopy/replacecopy.spec}
-
-The implementation of the algorithm is:
-
-\listingname{replacecopy.c}
-\cinput{replacecopy/replacecopy.impl}
-
-A partial proof of correctness is obtained by running the \textsf{WP} plug-in:
-\fclogs{mutating}{replacecopy}
-
-%% loop invariant preservation proven by Simplify though
diff --git a/src/plugins/wp/doc/tutorial/replacecopy/replacecopy_report.tex b/src/plugins/wp/doc/tutorial/replacecopy/replacecopy_report.tex
deleted file mode 100644
index 1ff6a4887dd..00000000000
--- a/src/plugins/wp/doc/tutorial/replacecopy/replacecopy_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+replace_copy+ & 19 & 7 & 10 & 89.5\% (522) \\
diff --git a/src/plugins/wp/doc/tutorial/reversecopy/reverse.c b/src/plugins/wp/doc/tutorial/reversecopy/reverse.c
deleted file mode 100644
index d3de6c759a4..00000000000
--- a/src/plugins/wp/doc/tutorial/reversecopy/reverse.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "reverse.h"
-#include "reverse.impl"
diff --git a/src/plugins/wp/doc/tutorial/reversecopy/reverse.h b/src/plugins/wp/doc/tutorial/reversecopy/reverse.h
deleted file mode 100644
index e22adb305fb..00000000000
--- a/src/plugins/wp/doc/tutorial/reversecopy/reverse.h
+++ /dev/null
@@ -1,7 +0,0 @@
-#ifndef _REVERSE_H
-#define _REVERSE_H
-#include "../library.h"
-#include "../swapvalues/swapvalues.h"
-#include "reverse.spec"
-#endif
-
diff --git a/src/plugins/wp/doc/tutorial/reversecopy/reverse.impl b/src/plugins/wp/doc/tutorial/reversecopy/reverse.impl
deleted file mode 100644
index b237af53c84..00000000000
--- a/src/plugins/wp/doc/tutorial/reversecopy/reverse.impl
+++ /dev/null
@@ -1,33 +0,0 @@
-void reverse(value_type* a, size_type n) {
- size_type first = 0;
- size_type last = n-1;
-
- /*@
- loop invariant 0 <= first;
- loop invariant last < n;
- // next 2 are added for proving "normal" assigns with alt-ergo
- loop invariant n > 0 ==> first <= n ;
- loop invariant n <= 0 ==> first == 0;
-
- // false, though simplify is ok with it ...
- // loop invariant n > 0 ==> first <= last;
-
- loop invariant first + last == n - 1;
-
- loop invariant \forall integer k;
- 0 <= k < first ==> a[k] == \at(a[n-1-k], Pre);
-
- loop invariant \forall integer k;
- last < k < n ==> a[k] == \at(a[n-1-k], Pre);
-
- loop assigns a[0..(first-1)];
- loop assigns a[(last+1)..(n-1)];
- loop assigns first, last;
-
- loop variant last;
- */
- while (first < last) {
- swap_values(a, n, first++, last--);
- }
-
-}
diff --git a/src/plugins/wp/doc/tutorial/reversecopy/reverse.spec b/src/plugins/wp/doc/tutorial/reversecopy/reverse.spec
deleted file mode 100644
index be294d74919..00000000000
--- a/src/plugins/wp/doc/tutorial/reversecopy/reverse.spec
+++ /dev/null
@@ -1,9 +0,0 @@
-/*@
- requires IsValidRange(a, n);
-
- assigns a[0..(n-1)];
-
- ensures \forall integer i; 0 <= i < n ==>
- a[i] == \old(a[n-1-i]);
-*/
-void reverse(value_type* a, size_type n);
diff --git a/src/plugins/wp/doc/tutorial/reversecopy/reverse_report.tex b/src/plugins/wp/doc/tutorial/reversecopy/reverse_report.tex
deleted file mode 100644
index fd12238c708..00000000000
--- a/src/plugins/wp/doc/tutorial/reversecopy/reverse_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+reverse+ & 39 & 25 & 12 & 94.9\% (3086) \\
diff --git a/src/plugins/wp/doc/tutorial/reversecopy/reversecopy.c b/src/plugins/wp/doc/tutorial/reversecopy/reversecopy.c
deleted file mode 100644
index b7c7a4731ad..00000000000
--- a/src/plugins/wp/doc/tutorial/reversecopy/reversecopy.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "reversecopy.h"
-#include "reversecopy.impl"
diff --git a/src/plugins/wp/doc/tutorial/reversecopy/reversecopy.h b/src/plugins/wp/doc/tutorial/reversecopy/reversecopy.h
deleted file mode 100644
index 4262124342e..00000000000
--- a/src/plugins/wp/doc/tutorial/reversecopy/reversecopy.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef _REVERSE_COPY_H
-#define _REVERSE_COPY_H
-#include "../library.h"
-#include "reversecopy.spec"
-#endif
-
diff --git a/src/plugins/wp/doc/tutorial/reversecopy/reversecopy.impl b/src/plugins/wp/doc/tutorial/reversecopy/reversecopy.impl
deleted file mode 100644
index ed518bc3e63..00000000000
--- a/src/plugins/wp/doc/tutorial/reversecopy/reversecopy.impl
+++ /dev/null
@@ -1,12 +0,0 @@
-void reverse_copy(const value_type* a, size_type n, value_type* b) {
- /*@
- loop invariant 0 <= i <= n;
- loop invariant \forall integer k; 0 <= k < i ==>
- b[k] == a[n-1-k];
-
- loop assigns b[0..i-1], i ;
- loop variant n-i;
- */
- for (size_type i = 0; i < n; i++)
- b[i] = a[n-1-i];
-}
diff --git a/src/plugins/wp/doc/tutorial/reversecopy/reversecopy.spec b/src/plugins/wp/doc/tutorial/reversecopy/reversecopy.spec
deleted file mode 100644
index db02b3f827d..00000000000
--- a/src/plugins/wp/doc/tutorial/reversecopy/reversecopy.spec
+++ /dev/null
@@ -1,9 +0,0 @@
-/*@
- requires IsValidRange(a, n);
- requires IsValidRange(b, n);
-
- assigns b[0..(n-1)];
-
- ensures \forall integer i; 0 <= i < n ==> b[i] == a[n-1-i];
-*/
-void reverse_copy(const value_type* a, size_type n, value_type* b);
diff --git a/src/plugins/wp/doc/tutorial/reversecopy/reversecopy.tex b/src/plugins/wp/doc/tutorial/reversecopy/reversecopy.tex
deleted file mode 100644
index 69a948e79ad..00000000000
--- a/src/plugins/wp/doc/tutorial/reversecopy/reversecopy.tex
+++ /dev/null
@@ -1,41 +0,0 @@
-\clearpage
-\section{The \textsf{reverse-copy} and \textsf{reverse} Algorithms}
-\label{reversecopy}
-
-\subsection{\textsf{reverse-copy}}
-
-We now study the \texttt{reverse-copy} algorithm from ``ACSL By Example''.
-This algorithm copies the contents from a source sequence to a destination
-sequence in reverse order.
-
-The specification of the \texttt{reverse-copy} algorithm is as follows:
-
-\listingname{reversecopy.h}
-\cinput{reversecopy/reversecopy.spec}
-
-The implementation of the algorithm is:
-
-\listingname{reversecopy.c}
-\cinput{reversecopy/reversecopy.impl}
-
-Running the \textsf{WP} plug-in does not allow proving all properties:
-\fclogs{mutating}{reversecopy}
-
-\subsection{\textsf{reverse}}
-
-The \texttt{reverse} algorithm is an in place version of the
-\texttt{reverse-copy} algorithm.
-
-Its specification is as follows:
-
-\listingname{reverse.h}
-\cinput{reversecopy/reverse.spec}
-
-The implementation is:
-
-\listingname{reverse.c}
-\cinput{reversecopy/reverse.impl}
-
-Running the \textsf{WP} plug-in does not allow proving some loop invariants
-preservation nor certain loop assigns:
-\fclogs{mutating}{reverse}
diff --git a/src/plugins/wp/doc/tutorial/reversecopy/reversecopy_report.tex b/src/plugins/wp/doc/tutorial/reversecopy/reversecopy_report.tex
deleted file mode 100644
index cdaf8f03008..00000000000
--- a/src/plugins/wp/doc/tutorial/reversecopy/reversecopy_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+reverse_copy+ & 18 & 5 & 11 & 88.9\% (201) \\
diff --git a/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.c b/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.c
deleted file mode 100644
index 3a0a9ac708f..00000000000
--- a/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.c
+++ /dev/null
@@ -1,3 +0,0 @@
-#include "rotatecopy.h"
-#include "../copy/copy.h"
-#include "rotatecopy.impl"
diff --git a/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.h b/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.h
deleted file mode 100644
index 419390f5995..00000000000
--- a/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef _ROTATE_COPY_H
-#define _ROTATE_COPY_H
-#include "../library.h"
-#include "rotatecopy.spec"
-#endif
-
diff --git a/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.impl b/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.impl
deleted file mode 100644
index 4c0d081fe57..00000000000
--- a/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.impl
+++ /dev/null
@@ -1,5 +0,0 @@
-void rotate_copy(const value_type* a, size_type m, size_type n,
- value_type* b) {
- copy(a, m, b+(n-m));
- copy(a+m, n-m, b);
-}
\ No newline at end of file
diff --git a/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.spec b/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.spec
deleted file mode 100644
index 24f91a20d32..00000000000
--- a/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.spec
+++ /dev/null
@@ -1,13 +0,0 @@
-/*@
- requires IsValidRange(a, n);
- requires IsValidRange(b, n);
- requires \separated(a+(0..n-1), b+(0..n-1));
- requires 0 <= m <= n;
-
- assigns b[0..(n-1)];
-
- ensures IsEqual{Here,Here}(a, m, b+(n-m));
- ensures IsEqual{Here,Here}(a+m, n-m, b);
-*/
-void rotate_copy(const value_type* a, size_type m, size_type n,
- value_type* b);
\ No newline at end of file
diff --git a/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.tex b/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.tex
deleted file mode 100644
index 8b80e17532b..00000000000
--- a/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy.tex
+++ /dev/null
@@ -1,21 +0,0 @@
-\section{The \textsf{rotate-copy} Algorithm}
-\label{rotate-copy}
-
-We now study the \texttt{rotate-copy} algorithm from ``ACSL By Example''.
-This algorithm rotates a source sequence by a certain number of positions and
-copies the result to a destination sequence of same size.
-
-The specification of the \texttt{rotate-copy} algorithm is as follows:
-
-\listingname{rotatecopy.h}
-\cinput{rotatecopy/rotatecopy.spec}
-
-The implementation of the algorithm is:
-
-\listingname{rotatecopy.c}
-\cinput{rotatecopy/rotatecopy.impl}
-
-A partial proof of correctness is obtained by running the \textsf{WP} plug-in:
-\fclogs{mutating}{rotatecopy}
-
-%% simplify does better on the unproven post (which is symmetrical to other post btw)
diff --git a/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy_report.tex b/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy_report.tex
deleted file mode 100644
index 791e263de29..00000000000
--- a/src/plugins/wp/doc/tutorial/rotatecopy/rotatecopy_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+rotate_copy+ & 16 & 3 & 13 & 100\% (2187) \\
diff --git a/src/plugins/wp/doc/tutorial/search/hasrange.spec b/src/plugins/wp/doc/tutorial/search/hasrange.spec
deleted file mode 100644
index 1a91379dc1e..00000000000
--- a/src/plugins/wp/doc/tutorial/search/hasrange.spec
+++ /dev/null
@@ -1,5 +0,0 @@
-/*@
- predicate HasSubRange{A}(value_type* a, integer m,
- value_type* b, integer n) =
- \exists size_type k; (0 <= k <= m-n) && IsEqual{A,A}(a+k, n, b);
-*/
\ No newline at end of file
diff --git a/src/plugins/wp/doc/tutorial/search/search.c b/src/plugins/wp/doc/tutorial/search/search.c
deleted file mode 100644
index 19201ce5a54..00000000000
--- a/src/plugins/wp/doc/tutorial/search/search.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "search.h"
-#include "search.impl"
diff --git a/src/plugins/wp/doc/tutorial/search/search.h b/src/plugins/wp/doc/tutorial/search/search.h
deleted file mode 100644
index 4e5fa933de4..00000000000
--- a/src/plugins/wp/doc/tutorial/search/search.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef SEARCH_H
-#define SEARCH_H
-#include "../library.h"
-#include "hasrange.spec"
-#include "search.spec"
-#endif
diff --git a/src/plugins/wp/doc/tutorial/search/search.impl b/src/plugins/wp/doc/tutorial/search/search.impl
deleted file mode 100644
index 7520d28497b..00000000000
--- a/src/plugins/wp/doc/tutorial/search/search.impl
+++ /dev/null
@@ -1,18 +0,0 @@
-#include "../equal/equal.h"
-
-size_type search(const value_type* a, size_type m, const value_type* b, size_type n)
-{
- if ((n == 0) || (m == 0)) return 0;
- if (n > m) return m;
- /*@
- loop invariant 0 <= i <= m-n+1;
- loop invariant !HasSubRange(a, n+i-1, b, n);
- loop assigns i;
- loop variant m-i;
- */
- for(size_type i = 0; i <= m-n; i++) {
- if (equal(a+i, n, b)) // Is there a match?
- return i;
- }
- return m;
-}
diff --git a/src/plugins/wp/doc/tutorial/search/search.spec b/src/plugins/wp/doc/tutorial/search/search.spec
deleted file mode 100644
index d7bf72a5d79..00000000000
--- a/src/plugins/wp/doc/tutorial/search/search.spec
+++ /dev/null
@@ -1,20 +0,0 @@
-/*@
- requires IsValidRange(a, m);
- requires IsValidRange(b, n);
- assigns \nothing;
-
- behavior has_match:
- assumes HasSubRange(a, m, b, n);
- ensures (n == 0 || m ==0) ==> \result == 0;
- ensures 0 <= \result <= m-n;
- ensures IsEqual{Here,Here}(a+\result, n, b);
- ensures !HasSubRange(a, \result+n-1, b, n);
-
- behavior no_match:
- assumes !HasSubRange(a, m, b, n);
- ensures \result == m;
-
- complete behaviors;
- disjoint behaviors;
-*/
-size_type search(const value_type* a, size_type m, const value_type* b, size_type n);
\ No newline at end of file
diff --git a/src/plugins/wp/doc/tutorial/search/search.tex b/src/plugins/wp/doc/tutorial/search/search.tex
deleted file mode 100644
index 4f1a82a226f..00000000000
--- a/src/plugins/wp/doc/tutorial/search/search.tex
+++ /dev/null
@@ -1,32 +0,0 @@
-\clearpage
-\section{The \textsf{search} Algorithm}
-\label{search}
-
-We study now the \texttt{search} algorithm from ``ACSL By Example''.
-This algorithm looks for a subsequence inside a sequence.
-We use the same definition as in the original specification:
-
-\listingname{search.h}
-\cinput{search/hasrange.spec}
-
-Then follows the specification of the \texttt{search} algorithm:
-
-\listingname{search.h}
-\cinput{search/search.spec}
-
-The implementation of the algorithm is:
-
-\listingname{search.c}
-\cinput{search/search.impl}
-
-Remark that \texttt{search} is defined in terms of \texttt{equal}, and
-its specification should be included from the \texttt{equal.h} header
-file.
-
-\clearpage
-From the original specification from ``ACSL By Example'', we only add
-the \emph{loop assigns} clause.
-The implementation is proved correct against its specification by
-simply running the \textsf{WP} plug-in:
-\fclogs{nonmutating}{search}
-
diff --git a/src/plugins/wp/doc/tutorial/search/search_report.tex b/src/plugins/wp/doc/tutorial/search/search_report.tex
deleted file mode 100644
index 78d75bff82d..00000000000
--- a/src/plugins/wp/doc/tutorial/search/search_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+search+ & 32 & 19 & 13 & 100\% (90) \\
diff --git a/src/plugins/wp/doc/tutorial/summary.report b/src/plugins/wp/doc/tutorial/summary.report
deleted file mode 100644
index 4d502e0e01f..00000000000
--- a/src/plugins/wp/doc/tutorial/summary.report
+++ /dev/null
@@ -1,5 +0,0 @@
-@SUFFIX "_report.tex"
-@ZERO "-"
-@FUNCTION
-\verb+%function+ & %total & %wp & %ergo & %success\% %ergo:steps \\
-@END
diff --git a/src/plugins/wp/doc/tutorial/swap/swap.c b/src/plugins/wp/doc/tutorial/swap/swap.c
deleted file mode 100644
index 900958c47db..00000000000
--- a/src/plugins/wp/doc/tutorial/swap/swap.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "swap.h"
-#include "swap.impl"
diff --git a/src/plugins/wp/doc/tutorial/swap/swap.h b/src/plugins/wp/doc/tutorial/swap/swap.h
deleted file mode 100644
index fe13ddae37e..00000000000
--- a/src/plugins/wp/doc/tutorial/swap/swap.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef _SWAP_H
-#define _SWAP_H
-#include "../library.h"
-#include "swap.spec"
-#endif
-
diff --git a/src/plugins/wp/doc/tutorial/swap/swap.impl b/src/plugins/wp/doc/tutorial/swap/swap.impl
deleted file mode 100644
index c1220390d58..00000000000
--- a/src/plugins/wp/doc/tutorial/swap/swap.impl
+++ /dev/null
@@ -1,5 +0,0 @@
-void swap(value_type* p, value_type* q) {
- const value_type save = *p;
- *p = *q;
- *q = save;
-}
diff --git a/src/plugins/wp/doc/tutorial/swap/swap.spec b/src/plugins/wp/doc/tutorial/swap/swap.spec
deleted file mode 100644
index 861054e15ee..00000000000
--- a/src/plugins/wp/doc/tutorial/swap/swap.spec
+++ /dev/null
@@ -1,12 +0,0 @@
-/*@
- requires \valid(p);
- requires \valid(q);
- requires \separated(p,q);
-
- assigns *p;
- assigns *q;
-
- ensures *p == \old(*q);
- ensures *q == \old(*p);
-*/
-void swap(value_type* p, value_type* q);
\ No newline at end of file
diff --git a/src/plugins/wp/doc/tutorial/swap/swap.tex b/src/plugins/wp/doc/tutorial/swap/swap.tex
deleted file mode 100644
index 625aeeffbc9..00000000000
--- a/src/plugins/wp/doc/tutorial/swap/swap.tex
+++ /dev/null
@@ -1,21 +0,0 @@
-\clearpage
-\section{The \textsf{swap} Algorithm}
-\label{swap}
-
-We now study the \texttt{swap} algorithm from ``ACSL By Example''.
-This algorithm exchanges the value of two variables.
-
-The specification of the \texttt{swap} algorithm is as follows:
-
-\listingname{swap.h}
-\cinput{swap/swap.spec}
-
-The implementation of the algorithm is:
-
-\listingname{swap.c}
-\cinput{swap/swap.impl}
-
-The implementation is proved correct against its specification by
-simply running the \textsf{WP} plug-in:
-\fclogs{mutating}{swap}
-
diff --git a/src/plugins/wp/doc/tutorial/swap/swap_report.tex b/src/plugins/wp/doc/tutorial/swap/swap_report.tex
deleted file mode 100644
index d3f0aea66f4..00000000000
--- a/src/plugins/wp/doc/tutorial/swap/swap_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+swap+ & 9 & 6 & 3 & 100\% (21) \\
diff --git a/src/plugins/wp/doc/tutorial/swapranges/swapranges.c b/src/plugins/wp/doc/tutorial/swapranges/swapranges.c
deleted file mode 100644
index 33a59c589c9..00000000000
--- a/src/plugins/wp/doc/tutorial/swapranges/swapranges.c
+++ /dev/null
@@ -1,3 +0,0 @@
-#include "swapranges.h"
-#include "../swap/swap.h"
-#include "swapranges.impl"
diff --git a/src/plugins/wp/doc/tutorial/swapranges/swapranges.h b/src/plugins/wp/doc/tutorial/swapranges/swapranges.h
deleted file mode 100644
index e09793267fc..00000000000
--- a/src/plugins/wp/doc/tutorial/swapranges/swapranges.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef _SWAP_RANGES_H
-#define _SWAP_RANGES_H
-#include "../library.h"
-#include "swapranges.spec"
-#endif
-
diff --git a/src/plugins/wp/doc/tutorial/swapranges/swapranges.impl b/src/plugins/wp/doc/tutorial/swapranges/swapranges.impl
deleted file mode 100644
index 638829b68e7..00000000000
--- a/src/plugins/wp/doc/tutorial/swapranges/swapranges.impl
+++ /dev/null
@@ -1,16 +0,0 @@
-void swap_ranges(value_type* a, size_type n, value_type* b) {
- /*@
- loop invariant 0 <= i <= n;
-
- loop assigns a[0..i-1];
- loop assigns b[0..i-1];
- loop assigns i;
-
- loop invariant IsEqual{Pre,Here}(a, i, b);
- loop invariant IsEqual{Here,Pre}(a, i, b);
- loop variant n-i;
- */
- for (size_type i = 0 ; i < n ; i++) {
- swap(&a[i], &b[i]);
- }
-}
diff --git a/src/plugins/wp/doc/tutorial/swapranges/swapranges.spec b/src/plugins/wp/doc/tutorial/swapranges/swapranges.spec
deleted file mode 100644
index 60e173c455d..00000000000
--- a/src/plugins/wp/doc/tutorial/swapranges/swapranges.spec
+++ /dev/null
@@ -1,12 +0,0 @@
-/*@
- requires IsValidRange(a, n);
- requires IsValidRange(b, n);
- requires \separated(a+(0..n-1), b+(0..n-1));
-
- assigns a[0..n-1];
- assigns b[0..n-1];
-
- ensures IsEqual{Here,Old}(a, n, b);
- ensures IsEqual{Old,Here}(a, n, b);
-*/
-void swap_ranges(value_type* a, size_type n, value_type* b);
diff --git a/src/plugins/wp/doc/tutorial/swapranges/swapranges.tex b/src/plugins/wp/doc/tutorial/swapranges/swapranges.tex
deleted file mode 100644
index f908540bd0c..00000000000
--- a/src/plugins/wp/doc/tutorial/swapranges/swapranges.tex
+++ /dev/null
@@ -1,26 +0,0 @@
-\clearpage
-\section{The \textsf{swap-ranges} Algorithm}
-\label{swap-ranges}
-
-We now study the \texttt{swap-ranges} algorithm from ``ACSL By Example''.
-This algorithm exchanges the contents of two ranges element-wise.
-The specification of the \texttt{swap-ranges} algorithm is as follows:
-
-\listingname{swapranges.h}
-\cinput{swapranges/swapranges.spec}
-
-The implementation of the algorithm is:
-
-\listingname{swapranges.c}
-\cinput{swapranges/swapranges.impl}
-
-Within \texttt{Store} model, the preservation of loop invariants are
-hardly discharged by \textsf{Alt-Ergo}:
-%. The implementation is proven
-%correct with model \texttt{Logic} that takes benefit from arrays
-%passed by reference:
-\fclogs{mutating}{swapranges}
-
-%%\logsinput{swapranges/swapranges.log}
-
-%% can be proven using Jessie + simplify if \separated requires removed
diff --git a/src/plugins/wp/doc/tutorial/swapranges/swapranges_report.tex b/src/plugins/wp/doc/tutorial/swapranges/swapranges_report.tex
deleted file mode 100644
index 35d5fee8805..00000000000
--- a/src/plugins/wp/doc/tutorial/swapranges/swapranges_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+swap_ranges+ & 22 & 5 & 13 & 81.8\% (2385) \\
diff --git a/src/plugins/wp/doc/tutorial/swapvalues/swapvalues-withassert.c b/src/plugins/wp/doc/tutorial/swapvalues/swapvalues-withassert.c
deleted file mode 100644
index c9b33917bb9..00000000000
--- a/src/plugins/wp/doc/tutorial/swapvalues/swapvalues-withassert.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "swapvalues.h"
-#include "swapvalues-withassert.impl"
diff --git a/src/plugins/wp/doc/tutorial/swapvalues/swapvalues-withassert.impl b/src/plugins/wp/doc/tutorial/swapvalues/swapvalues-withassert.impl
deleted file mode 100644
index abed2a54e32..00000000000
--- a/src/plugins/wp/doc/tutorial/swapvalues/swapvalues-withassert.impl
+++ /dev/null
@@ -1,6 +0,0 @@
-void swap_values(value_type* a, size_type n,
- size_type i, size_type j) {
- value_type tmp = a[i];
- a[i] = a[j];
- a[j] = tmp;
-}
diff --git a/src/plugins/wp/doc/tutorial/swapvalues/swapvalues.c b/src/plugins/wp/doc/tutorial/swapvalues/swapvalues.c
deleted file mode 100644
index 17ffb560c44..00000000000
--- a/src/plugins/wp/doc/tutorial/swapvalues/swapvalues.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "swapvalues.h"
-#include "swapvalues.impl"
diff --git a/src/plugins/wp/doc/tutorial/swapvalues/swapvalues.h b/src/plugins/wp/doc/tutorial/swapvalues/swapvalues.h
deleted file mode 100644
index 836070ec3f3..00000000000
--- a/src/plugins/wp/doc/tutorial/swapvalues/swapvalues.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#ifndef _SWAP_VALUES_H
-#define _SWAP_VALUES_H
-#include "../library.h"
-#include "swapvalues.spec"
-#endif
-
diff --git a/src/plugins/wp/doc/tutorial/swapvalues/swapvalues.impl b/src/plugins/wp/doc/tutorial/swapvalues/swapvalues.impl
deleted file mode 100644
index abed2a54e32..00000000000
--- a/src/plugins/wp/doc/tutorial/swapvalues/swapvalues.impl
+++ /dev/null
@@ -1,6 +0,0 @@
-void swap_values(value_type* a, size_type n,
- size_type i, size_type j) {
- value_type tmp = a[i];
- a[i] = a[j];
- a[j] = tmp;
-}
diff --git a/src/plugins/wp/doc/tutorial/swapvalues/swapvalues.spec b/src/plugins/wp/doc/tutorial/swapvalues/swapvalues.spec
deleted file mode 100644
index d1e446023da..00000000000
--- a/src/plugins/wp/doc/tutorial/swapvalues/swapvalues.spec
+++ /dev/null
@@ -1,22 +0,0 @@
-/*@
- predicate
- SwapValues{L1,L2}(value_type* a, size_type i, size_type j) =
- 0 <= i && 0 <= j &&
- \at(a[i],L1) == \at(a[j],L2) &&
- \at(a[j],L1) == \at(a[i],L2) &&
- (\forall integer k; 0 <= k && k != i && k != j ==>
- \at(a[k],L1) == \at(a[k],L2));
-*/
-
-/*@
- requires IsValidRange(a, n);
- requires 0 <= i < n;
- requires 0 <= j < n;
-
- assigns a[i];
- assigns a[j];
-
- ensures SwapValues{Old,Here}(a, i, j);
-*/
-void swap_values(value_type* a, size_type n,
- size_type i, size_type j);
\ No newline at end of file
diff --git a/src/plugins/wp/doc/tutorial/swapvalues/swapvalues.tex b/src/plugins/wp/doc/tutorial/swapvalues/swapvalues.tex
deleted file mode 100644
index 60e04a1907b..00000000000
--- a/src/plugins/wp/doc/tutorial/swapvalues/swapvalues.tex
+++ /dev/null
@@ -1,23 +0,0 @@
-\clearpage
-\section{The \textsf{swap-values} Algorithm}
-\label{swap-values}
-
-We now study the \texttt{swap-values} algorithm from ``ACSL By Example''.
-This algorithm exchanges the value of two variables.
-
-The specification of the \texttt{swap-values} algorithm is as follows:
-
-\listingname{swapvalues.h}
-\cinput{swapvalues/swapvalues.spec}
-
-The implementation of the algorithm is:
-
-\listingname{swapvalues.c}
-\cinput{swapvalues/swapvalues.impl}
-
-The implementation is proved correct:
-\fclogs{mutating}{swapvalues}
-
-%With \texttt{Store} memory model, the proof obligations are not discharged by \textsf{Alt-Ergo}:
-%\fclogs{mutating}{swapvalues-withassert}
-
diff --git a/src/plugins/wp/doc/tutorial/swapvalues/swapvalues_report.tex b/src/plugins/wp/doc/tutorial/swapvalues/swapvalues_report.tex
deleted file mode 100644
index 1b248b7e580..00000000000
--- a/src/plugins/wp/doc/tutorial/swapvalues/swapvalues_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+swap_values+ & 8 & 3 & 5 & 100\% (61) \\
diff --git a/src/plugins/wp/doc/tutorial/tests/binary/binarysearch.i b/src/plugins/wp/doc/tutorial/tests/binary/binarysearch.i
deleted file mode 100644
index 77a41a5002f..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/binary/binarysearch.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- OPT: -wp -wp-par 1 -wp-msg-key shell -wp-verbose 0 binarysearch/binarysearch.c -then -wp-rte -wp -wp-report console.report -wp-report summary.report -wp-report-basename binarysearch/binarysearch
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/binary/lowerbound.i b/src/plugins/wp/doc/tutorial/tests/binary/lowerbound.i
deleted file mode 100644
index 39a854de9c3..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/binary/lowerbound.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- OPT: -wp -wp-par 1 -wp-msg-key shell -wp-verbose 0 -then -wp-rte -wp -wp-report console.report -wp-report summary.report -wp-report-basename lowerbound/lowerbound lowerbound/lowerbound.c
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/binary/oracle/binarysearch.res.oracle b/src/plugins/wp/doc/tutorial/tests/binary/oracle/binarysearch.res.oracle
deleted file mode 100644
index 7b138b4ca17..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/binary/oracle/binarysearch.res.oracle
+++ /dev/null
@@ -1,9 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/binary/binarysearch.i (no preprocessing)
-[kernel] Parsing binarysearch/binarysearch.c (with preprocessing)
-[wp] warning: Missing RTE guards
-[rte] annotating function binary_search
-------------------------------------------------
-Module #VC WP Ergo Success
-binary_search 10 8 2 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/binary/oracle/lowerbound.res.oracle b/src/plugins/wp/doc/tutorial/tests/binary/oracle/lowerbound.res.oracle
deleted file mode 100644
index dafee56c3b9..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/binary/oracle/lowerbound.res.oracle
+++ /dev/null
@@ -1,9 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/binary/lowerbound.i (no preprocessing)
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing lowerbound/lowerbound.c (with preprocessing)
-[rte] annotating function lower_bound
-------------------------------------------------
-Module #VC WP Ergo Success
-lower_bound 22 9 13 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/binary/oracle/upperbound.res.oracle b/src/plugins/wp/doc/tutorial/tests/binary/oracle/upperbound.res.oracle
deleted file mode 100644
index 3fca20e9581..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/binary/oracle/upperbound.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/binary/upperbound.i (no preprocessing)
-[kernel] Parsing upperbound/upperbound.c (with preprocessing)
-[rte] annotating function upper_bound
-------------------------------------------------
-Module #VC WP Ergo Success
-upper_bound 22 8 14 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/binary/upperbound.i b/src/plugins/wp/doc/tutorial/tests/binary/upperbound.i
deleted file mode 100644
index a031083b0bf..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/binary/upperbound.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename upperbound/upperbound" +"upperbound/upperbound.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/maxmin/compare.i b/src/plugins/wp/doc/tutorial/tests/maxmin/compare.i
deleted file mode 100644
index 4a912f7b7cc..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/maxmin/compare.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report compare/compare.report" +"-wp-report-basename compare/compare" +"compare/compare.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/maxmin/maxelt.i b/src/plugins/wp/doc/tutorial/tests/maxmin/maxelt.i
deleted file mode 100644
index a5805ee2d9b..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/maxmin/maxelt.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename maxelt/maxelt" +"maxelt/maxelt.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/maxmin/maxeltp.i b/src/plugins/wp/doc/tutorial/tests/maxmin/maxeltp.i
deleted file mode 100644
index 06be70fe898..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/maxmin/maxeltp.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report maxeltp/maxelt.report" +"-wp-report-basename maxeltp/maxelt" +"maxeltp/maxelt.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/maxmin/maxseq.i b/src/plugins/wp/doc/tutorial/tests/maxmin/maxseq.i
deleted file mode 100644
index 6f6a79ff3af..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/maxmin/maxseq.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename maxseq/maxseq" +"maxseq/maxseq.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/maxmin/minelt.i b/src/plugins/wp/doc/tutorial/tests/maxmin/minelt.i
deleted file mode 100644
index d96f773ef22..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/maxmin/minelt.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename minelt/minelt" +"minelt/minelt.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/maxmin/oracle/compare.res.oracle b/src/plugins/wp/doc/tutorial/tests/maxmin/oracle/compare.res.oracle
deleted file mode 100644
index de32d853ef4..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/maxmin/oracle/compare.res.oracle
+++ /dev/null
@@ -1,7 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/maxmin/compare.i (no preprocessing)
-[kernel] Parsing compare/compare.c (with preprocessing)
-------------------------------------------------
-Module #VC WP Ergo Success
-Axiomatic Comparison 6 4 2 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/maxmin/oracle/maxelt.res.oracle b/src/plugins/wp/doc/tutorial/tests/maxmin/oracle/maxelt.res.oracle
deleted file mode 100644
index c57f6f5b0d1..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/maxmin/oracle/maxelt.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/maxmin/maxelt.i (no preprocessing)
-[kernel] Parsing maxelt/maxelt.c (with preprocessing)
-[rte] annotating function max_element
-------------------------------------------------
-Module #VC WP Ergo Success
-max_element 25 13 12 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/maxmin/oracle/maxeltp.res.oracle b/src/plugins/wp/doc/tutorial/tests/maxmin/oracle/maxeltp.res.oracle
deleted file mode 100644
index 7e73d6924ab..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/maxmin/oracle/maxeltp.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/maxmin/maxeltp.i (no preprocessing)
-[kernel] Parsing maxeltp/maxelt.c (with preprocessing)
-[rte] annotating function max_element
-------------------------------------------------
-Module #VC WP Ergo Success
-max_element 25 12 13 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/maxmin/oracle/maxseq.res.oracle b/src/plugins/wp/doc/tutorial/tests/maxmin/oracle/maxseq.res.oracle
deleted file mode 100644
index 66e1995e102..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/maxmin/oracle/maxseq.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/maxmin/maxseq.i (no preprocessing)
-[kernel] Parsing maxseq/maxseq.c (with preprocessing)
-[rte] annotating function max_seq
-------------------------------------------------
-Module #VC WP Ergo Success
-max_seq 8 5 3 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/maxmin/oracle/minelt.res.oracle b/src/plugins/wp/doc/tutorial/tests/maxmin/oracle/minelt.res.oracle
deleted file mode 100644
index 1c725b37f63..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/maxmin/oracle/minelt.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/maxmin/minelt.i (no preprocessing)
-[kernel] Parsing minelt/minelt.c (with preprocessing)
-[rte] annotating function min_element
-------------------------------------------------
-Module #VC WP Ergo Success
-min_element 25 13 12 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/copy.i b/src/plugins/wp/doc/tutorial/tests/mutating/copy.i
deleted file mode 100644
index a58d777553c..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/copy.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename copy/copy" +"copy/copy.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/fill.i b/src/plugins/wp/doc/tutorial/tests/mutating/fill.i
deleted file mode 100644
index 00eb8b0c422..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/fill.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- OPT:-wp -wp-par 1 -wp-msg-key shell -wp-verbose 0 @PTEST_FILE@ @PTEST_NAME@/@PTEST_NAME@.c -then -wp -wp-rte -wp-report console.report -wp-report summary.report -wp-report-basename @PTEST_NAME@/@PTEST_NAME@
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/iota.i b/src/plugins/wp/doc/tutorial/tests/mutating/iota.i
deleted file mode 100644
index 00eb8b0c422..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/iota.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- OPT:-wp -wp-par 1 -wp-msg-key shell -wp-verbose 0 @PTEST_FILE@ @PTEST_NAME@/@PTEST_NAME@.c -then -wp -wp-rte -wp-report console.report -wp-report summary.report -wp-report-basename @PTEST_NAME@/@PTEST_NAME@
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/copy.res.oracle b/src/plugins/wp/doc/tutorial/tests/mutating/oracle/copy.res.oracle
deleted file mode 100644
index 3d13dba59cf..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/copy.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/mutating/copy.i (no preprocessing)
-[kernel] Parsing copy/copy.c (with preprocessing)
-[rte] annotating function copy
-------------------------------------------------
-Module #VC WP Ergo Success
-copy 15 4 9 86.7%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/fill.res.oracle b/src/plugins/wp/doc/tutorial/tests/mutating/oracle/fill.res.oracle
deleted file mode 100644
index 542dfd8b745..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/fill.res.oracle
+++ /dev/null
@@ -1,9 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/mutating/fill.i (no preprocessing)
-[kernel] Parsing fill/fill.c (with preprocessing)
-[wp] warning: Missing RTE guards
-[rte] annotating function fill
-------------------------------------------------
-Module #VC WP Ergo Success
-fill 14 5 9 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/iota.res.oracle b/src/plugins/wp/doc/tutorial/tests/mutating/oracle/iota.res.oracle
deleted file mode 100644
index 53a2a88968a..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/iota.res.oracle
+++ /dev/null
@@ -1,9 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/mutating/iota.i (no preprocessing)
-[kernel] Parsing iota/iota.c (with preprocessing)
-[wp] warning: Missing RTE guards
-[rte] annotating function iota
-------------------------------------------------
-Module #VC WP Ergo Success
-iota 16 5 11 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/removecopy.res.oracle b/src/plugins/wp/doc/tutorial/tests/mutating/oracle/removecopy.res.oracle
deleted file mode 100644
index 4492d9cf953..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/removecopy.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/mutating/removecopy.i (no preprocessing)
-[kernel] Parsing removecopy/removecopy.c (with preprocessing)
-[rte] annotating function remove_copy
-------------------------------------------------
-Module #VC WP Ergo Success
-remove_copy 20 7 11 90.0%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/replacecopy.res.oracle b/src/plugins/wp/doc/tutorial/tests/mutating/oracle/replacecopy.res.oracle
deleted file mode 100644
index 55ab4468e5b..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/replacecopy.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/mutating/replacecopy.i (no preprocessing)
-[kernel] Parsing replacecopy/replacecopy.c (with preprocessing)
-[rte] annotating function replace_copy
-------------------------------------------------
-Module #VC WP Ergo Success
-replace_copy 19 7 10 89.5%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/reverse.res.oracle b/src/plugins/wp/doc/tutorial/tests/mutating/oracle/reverse.res.oracle
deleted file mode 100644
index 7c954059cc6..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/reverse.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/mutating/reverse.i (no preprocessing)
-[kernel] Parsing reversecopy/reverse.c (with preprocessing)
-[rte] annotating function reverse
-------------------------------------------------
-Module #VC WP Ergo Success
-reverse 39 25 12 94.9%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/reversecopy.res.oracle b/src/plugins/wp/doc/tutorial/tests/mutating/oracle/reversecopy.res.oracle
deleted file mode 100644
index 2f1a1e505be..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/reversecopy.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/mutating/reversecopy.i (no preprocessing)
-[kernel] Parsing reversecopy/reversecopy.c (with preprocessing)
-[rte] annotating function reverse_copy
-------------------------------------------------
-Module #VC WP Ergo Success
-reverse_copy 18 5 11 88.9%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/rotatecopy.res.oracle b/src/plugins/wp/doc/tutorial/tests/mutating/oracle/rotatecopy.res.oracle
deleted file mode 100644
index 8f2becab5a5..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/rotatecopy.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/mutating/rotatecopy.i (no preprocessing)
-[kernel] Parsing rotatecopy/rotatecopy.c (with preprocessing)
-[rte] annotating function rotate_copy
-------------------------------------------------
-Module #VC WP Ergo Success
-rotate_copy 16 3 13 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/swap.res.oracle b/src/plugins/wp/doc/tutorial/tests/mutating/oracle/swap.res.oracle
deleted file mode 100644
index b05f75df8ee..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/swap.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/mutating/swap.i (no preprocessing)
-[kernel] Parsing swap/swap.c (with preprocessing)
-[rte] annotating function swap
-------------------------------------------------
-Module #VC WP Ergo Success
-swap 9 6 3 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/swapranges.res.oracle b/src/plugins/wp/doc/tutorial/tests/mutating/oracle/swapranges.res.oracle
deleted file mode 100644
index 404d2414e3a..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/swapranges.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/mutating/swapranges.i (no preprocessing)
-[kernel] Parsing swapranges/swapranges.c (with preprocessing)
-[rte] annotating function swap_ranges
-------------------------------------------------
-Module #VC WP Ergo Success
-swap_ranges 22 5 13 81.8%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/swapvalues-withassert.res.oracle b/src/plugins/wp/doc/tutorial/tests/mutating/oracle/swapvalues-withassert.res.oracle
deleted file mode 100644
index 1a23c9f627c..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/swapvalues-withassert.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/mutating/swapvalues-withassert.i (no preprocessing)
-[kernel] Parsing swapvalues/swapvalues-withassert.c (with preprocessing)
-[rte] annotating function swap_values
-------------------------------------------------
-Module #VC WP Ergo Success
-swap_values 8 3 4 87.5%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/swapvalues.res.oracle b/src/plugins/wp/doc/tutorial/tests/mutating/oracle/swapvalues.res.oracle
deleted file mode 100644
index e217634d7e9..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/swapvalues.res.oracle
+++ /dev/null
@@ -1,9 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/mutating/swapvalues.i (no preprocessing)
-[kernel] Parsing swapvalues/swapvalues.c (with preprocessing)
-[wp] warning: Missing RTE guards
-[rte] annotating function swap_values
-------------------------------------------------
-Module #VC WP Ergo Success
-swap_values 8 3 5 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/uniquecopy.res.oracle b/src/plugins/wp/doc/tutorial/tests/mutating/oracle/uniquecopy.res.oracle
deleted file mode 100644
index 8888733622e..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/oracle/uniquecopy.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/mutating/uniquecopy.i (no preprocessing)
-[kernel] Parsing uniquecopy/uniquecopy.c (with preprocessing)
-[rte] annotating function unique_copy
-------------------------------------------------
-Module #VC WP Ergo Success
-unique_copy 33 13 3 48.5%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/removecopy.i b/src/plugins/wp/doc/tutorial/tests/mutating/removecopy.i
deleted file mode 100644
index 23a92d8e210..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/removecopy.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename removecopy/removecopy" +"removecopy/removecopy.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/replacecopy.i b/src/plugins/wp/doc/tutorial/tests/mutating/replacecopy.i
deleted file mode 100644
index 18a6058cf56..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/replacecopy.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename replacecopy/replacecopy" +"replacecopy/replacecopy.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/reverse.i b/src/plugins/wp/doc/tutorial/tests/mutating/reverse.i
deleted file mode 100644
index 8a12874cbab..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/reverse.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-timeout 5" +"-wp-report summary.report" +"-wp-report-basename reversecopy/reverse" +"reversecopy/reverse.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/reversecopy.i b/src/plugins/wp/doc/tutorial/tests/mutating/reversecopy.i
deleted file mode 100644
index 1cf01894857..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/reversecopy.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename reversecopy/reversecopy" +"reversecopy/reversecopy.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/rotatecopy.i b/src/plugins/wp/doc/tutorial/tests/mutating/rotatecopy.i
deleted file mode 100644
index 2c72649a2d5..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/rotatecopy.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename rotatecopy/rotatecopy" +"rotatecopy/rotatecopy.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/swap.i b/src/plugins/wp/doc/tutorial/tests/mutating/swap.i
deleted file mode 100644
index 5f756508f21..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/swap.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename swap/swap" +"swap/swap.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/swapranges.i b/src/plugins/wp/doc/tutorial/tests/mutating/swapranges.i
deleted file mode 100644
index ce1af5dc858..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/swapranges.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename swapranges/swapranges" +"swapranges/swapranges.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/swapvalues-withassert.i b/src/plugins/wp/doc/tutorial/tests/mutating/swapvalues-withassert.i
deleted file mode 100644
index e5b947e8e23..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/swapvalues-withassert.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"swapvalues/swapvalues-withassert.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/swapvalues.i b/src/plugins/wp/doc/tutorial/tests/mutating/swapvalues.i
deleted file mode 100644
index 00eb8b0c422..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/swapvalues.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- OPT:-wp -wp-par 1 -wp-msg-key shell -wp-verbose 0 @PTEST_FILE@ @PTEST_NAME@/@PTEST_NAME@.c -then -wp -wp-rte -wp-report console.report -wp-report summary.report -wp-report-basename @PTEST_NAME@/@PTEST_NAME@
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/mutating/uniquecopy.i b/src/plugins/wp/doc/tutorial/tests/mutating/uniquecopy.i
deleted file mode 100644
index 7da97640313..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/mutating/uniquecopy.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename uniquecopy/uniquecopy" +"uniquecopy/uniquecopy.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/adjacent.i b/src/plugins/wp/doc/tutorial/tests/nonmutating/adjacent.i
deleted file mode 100644
index dea079729dd..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/adjacent.i
+++ /dev/null
@@ -1,5 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename adjacent/adjacent" +"adjacent/adjacent.c"
-*/
-
-
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/count.i b/src/plugins/wp/doc/tutorial/tests/nonmutating/count.i
deleted file mode 100644
index 963aa89eaf1..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/count.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename count/count" +"count/count.c"
- */
-
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/eqmismatch.i b/src/plugins/wp/doc/tutorial/tests/nonmutating/eqmismatch.i
deleted file mode 100644
index 238975e0129..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/eqmismatch.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report mismatch/eqmismatch.report" +"-wp-report-basename mismatch/eqmismatch" +"mismatch/equal.c"
- */
-
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/equal.i b/src/plugins/wp/doc/tutorial/tests/nonmutating/equal.i
deleted file mode 100644
index b4de719217f..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/equal.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: -"-wp-rte" +"-wp-report summary.report" +"-wp-report-basename equal/equal" +"equal/equal.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/equal_rte.i b/src/plugins/wp/doc/tutorial/tests/nonmutating/equal_rte.i
deleted file mode 100644
index 6a36817b365..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/equal_rte.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename equal/equal_rte" +"equal/equal.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/find.i b/src/plugins/wp/doc/tutorial/tests/nonmutating/find.i
deleted file mode 100644
index 1f25c3b212e..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/find.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename find/find" +"find/find.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/findfirst.i b/src/plugins/wp/doc/tutorial/tests/nonmutating/findfirst.i
deleted file mode 100644
index 5a7b60e7f63..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/findfirst.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename findfirst/findfirst" +"findfirst/findfirst.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/mismatch.i b/src/plugins/wp/doc/tutorial/tests/nonmutating/mismatch.i
deleted file mode 100644
index fcaf18df649..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/mismatch.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename mismatch/mismatch" +"mismatch/mismatch.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/adjacent.res.oracle b/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/adjacent.res.oracle
deleted file mode 100644
index 8805de5ec86..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/adjacent.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/nonmutating/adjacent.i (no preprocessing)
-[kernel] Parsing adjacent/adjacent.c (with preprocessing)
-[rte] annotating function adjacent_find
-------------------------------------------------
-Module #VC WP Ergo Success
-adjacent_find 23 11 12 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/count.res.oracle b/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/count.res.oracle
deleted file mode 100644
index ea361f2e9c0..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/count.res.oracle
+++ /dev/null
@@ -1,9 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/nonmutating/count.i (no preprocessing)
-[kernel] Parsing count/count.c (with preprocessing)
-[rte] annotating function count
-------------------------------------------------
-Module #VC WP Ergo Success
-Lemma 1 - 1 100%
-count 16 8 8 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/eqmismatch.res.oracle b/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/eqmismatch.res.oracle
deleted file mode 100644
index d814045627c..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/eqmismatch.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/nonmutating/eqmismatch.i (no preprocessing)
-[kernel] Parsing mismatch/equal.c (with preprocessing)
-[rte] annotating function equal
-------------------------------------------------
-Module #VC WP Ergo Success
-equal 7 6 1 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/equal.res.oracle b/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/equal.res.oracle
deleted file mode 100644
index 267c8fb5bd3..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/equal.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/nonmutating/equal.i (no preprocessing)
-[kernel] Parsing equal/equal.c (with preprocessing)
-[wp] warning: Missing RTE guards
-------------------------------------------------
-Module #VC WP Ergo Success
-equal 12 8 4 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/equal_rte.res.oracle b/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/equal_rte.res.oracle
deleted file mode 100644
index 77ed294c38f..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/equal_rte.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/nonmutating/equal_rte.i (no preprocessing)
-[kernel] Parsing equal/equal.c (with preprocessing)
-[rte] annotating function equal
-------------------------------------------------
-Module #VC WP Ergo Success
-equal 15 8 7 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/find.res.oracle b/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/find.res.oracle
deleted file mode 100644
index d022459964f..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/find.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/nonmutating/find.i (no preprocessing)
-[kernel] Parsing find/find.c (with preprocessing)
-[rte] annotating function find
-------------------------------------------------
-Module #VC WP Ergo Success
-find 19 9 10 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/findfirst.res.oracle b/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/findfirst.res.oracle
deleted file mode 100644
index b138d449c53..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/findfirst.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/nonmutating/findfirst.i (no preprocessing)
-[kernel] Parsing findfirst/findfirst.c (with preprocessing)
-[rte] annotating function find_first_of
-------------------------------------------------
-Module #VC WP Ergo Success
-find_first_of 26 16 10 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/mismatch.res.oracle b/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/mismatch.res.oracle
deleted file mode 100644
index 1f70ace71c3..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/mismatch.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/nonmutating/mismatch.i (no preprocessing)
-[kernel] Parsing mismatch/mismatch.c (with preprocessing)
-[rte] annotating function mismatch
-------------------------------------------------
-Module #VC WP Ergo Success
-mismatch 20 9 11 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/search.res.oracle b/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/search.res.oracle
deleted file mode 100644
index 00d18c5d9b7..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/oracle/search.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/nonmutating/search.i (no preprocessing)
-[kernel] Parsing search/search.c (with preprocessing)
-[rte] annotating function search
-------------------------------------------------
-Module #VC WP Ergo Success
-search 32 19 13 100%
-------------------------------------------------
diff --git a/src/plugins/wp/doc/tutorial/tests/nonmutating/search.i b/src/plugins/wp/doc/tutorial/tests/nonmutating/search.i
deleted file mode 100644
index bf426a6687c..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/nonmutating/search.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config
- STDOPT: +"-wp-report summary.report" +"-wp-report-basename search/search" +"search/search.c"
-*/
-
diff --git a/src/plugins/wp/doc/tutorial/tests/test_config b/src/plugins/wp/doc/tutorial/tests/test_config
deleted file mode 100644
index 0370931cb79..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/test_config
+++ /dev/null
@@ -1,2 +0,0 @@
-CMD: @frama-c@ -add-path /usr/local/lib/frama-c/plugins -add-path . -journal-disable
-OPT: -wp -wp-par 1 -wp-log shell -wp-verbose 0 -wp-rte -wp-report console.report
diff --git a/src/plugins/wp/doc/tutorial/tests/test_config.in b/src/plugins/wp/doc/tutorial/tests/test_config.in
deleted file mode 100644
index 4425f4ef1ad..00000000000
--- a/src/plugins/wp/doc/tutorial/tests/test_config.in
+++ /dev/null
@@ -1,2 +0,0 @@
-CMD: @frama-c@ @LIB_PATH@ -journal-disable
-OPT: -wp -wp-par 1 -wp-msg-key shell -wp-verbose 0 -wp-rte -wp-report console.report
diff --git a/src/plugins/wp/doc/tutorial/tut_binary.tex b/src/plugins/wp/doc/tutorial/tut_binary.tex
deleted file mode 100644
index 9d9b0ab39e6..00000000000
--- a/src/plugins/wp/doc/tutorial/tut_binary.tex
+++ /dev/null
@@ -1,30 +0,0 @@
-\chapter{Binary Search Algorithms}
-\label{binary}
-
-In this chapter, we study the binary search algorithms defined in ``ACSL By Example''.
-
-\section{Specification Helpers}
-\label{binary-helpers}
-Like in the original book, we must introduce in our library the
-definition for sorted sequences:
-
-\listingname{binary.h}
-\cinput{binary/sorted.spec}
-
-We also require the introduction of an helper axiom for division:
-
-\listingname{binary.h}
-\cinput{binary/division.spec}
-
-\section{By-Reference Arguments}
-The generated proof obligations for lowerbound and upperbound functions
-are rather difficult to discharge with the \texttt{Store} memory model.
-It is better here to use the \texttt{Logic} memory model that combines \textsf{Store}
-and arrays passed by references detection, which is quite effective here.
-
-This experimental memory model is activated by \texttt{-wp-model Logic}. However,
-the proofs can be handled in \texttt{Store} model with a timeout of one minute.
-
-\input{lowerbound/lowerbound.tex}
-\input{upperbound/upperbound.tex}
-\input{binarysearch/binarysearch.tex}
diff --git a/src/plugins/wp/doc/tutorial/tut_function.tex b/src/plugins/wp/doc/tutorial/tut_function.tex
deleted file mode 100644
index 39a9c53f116..00000000000
--- a/src/plugins/wp/doc/tutorial/tut_function.tex
+++ /dev/null
@@ -1,12 +0,0 @@
-\chapter{Non-Mutating Algorithm}
-
-We focus here on the non-mutating algorithm presented in ``ACSL By
-Example'', chapter §3.
-
-\input{equal/equal.tex}
-\input{mismatch/mismatch.tex}
-\input{find/find.tex}
-\input{findfirst/findfirst.tex}
-\input{adjacent/adjacent.tex}
-\input{count/count.tex}
-\input{search/search.tex}
diff --git a/src/plugins/wp/doc/tutorial/tut_intro.tex b/src/plugins/wp/doc/tutorial/tut_intro.tex
deleted file mode 100644
index b48e5486357..00000000000
--- a/src/plugins/wp/doc/tutorial/tut_intro.tex
+++ /dev/null
@@ -1,49 +0,0 @@
-\chapter{Introduction}
-
-This book is a guided tour on how to use \textsf{WP} plug-in of
-\textsf{Frama-C} for proving \textsf{C} programs annotated with
-\textsf{ACSL} notations. It is based on the excellent ``ACSL By
-Example'' book produced by the Fraunhofer FIRST Institute for
-the Device-Soft project\footnote{Version 7.1.0 of December 2011,
- see \url{http://www.first.fraunhofer.de}}.
-
-We assume the reader to be familiar with \textsf{ACSL} in general and
-already equipped with the \textsf{WP} plug-in, which is distributed
-with \textsf{Frama-C} releases. Please refer to the \textsf{WP} user's
-manual\footnote{\url{http://frama-c.com/download/frama-c-wp-manual.pdf}}
-for installation and general overview of the plug-in.
-
-\section{Library}
-
-The case studies presented in this document are exact copies of the
-ones presented in the original ``ACSL By Example'' book. Sometimes, we
-indicate some modifications of the specification that makes
-\textsf{WP} better prove the programs.
-
-All examples uses the following \emph{library} of \textsf{C} and
-\textsf{ACSL} definitions:
-
-\listingname{library.h}
-\cinput{library.h}
-
-\section{Examples}
-
-Source of case studies are generally presented in two separated files:
-one for the header and specification of the algorithm, and one of its
-implementation. To ease the presentation in the book, we have omitted
-the necessary \texttt{include} lines from sources.
-
-Thus, a header file \texttt{A.h} should be enclosed by the following lines:
-\begin{ccode}
- #ifndef _A_H
- #define _A_H
- #include "../library.h"
- [...]
- #endif
-\end{ccode}
-
-Similarly, an implementation file \texttt{A.c} should start by including its header:
-\begin{ccode}
- #include "A.h"
- [...]
-\end{ccode}
diff --git a/src/plugins/wp/doc/tutorial/tut_maxmin.tex b/src/plugins/wp/doc/tutorial/tut_maxmin.tex
deleted file mode 100644
index 082b761661d..00000000000
--- a/src/plugins/wp/doc/tutorial/tut_maxmin.tex
+++ /dev/null
@@ -1,10 +0,0 @@
-\chapter{Maximum and Minimum Algorithms}
-
-In this chapter we study the algorithms for computing the extremum
-elements in a sequence.
-
-\input{compare/compare.tex}
-\input{maxelt/maxelt.tex}
-\input{maxeltp/maxelt.tex}
-\input{maxseq/maxseq.tex}
-\input{minelt/minelt.tex}
diff --git a/src/plugins/wp/doc/tutorial/tut_mutating.tex b/src/plugins/wp/doc/tutorial/tut_mutating.tex
deleted file mode 100644
index 2ea5d7f818a..00000000000
--- a/src/plugins/wp/doc/tutorial/tut_mutating.tex
+++ /dev/null
@@ -1,17 +0,0 @@
-\chapter{Mutating Algorithms}
-\label{mutating}
-
-In this chapter, we study the mutating algorithms defined in ``ACSL By
-Example''.
-
-\input{fill/fill.tex}
-\input{iota/iota.tex}
-\input{swap/swap.tex}
-\input{swapvalues/swapvalues.tex}
-\input{swapranges/swapranges.tex}
-\input{copy/copy.tex}
-\input{reversecopy/reversecopy.tex}
-\input{rotatecopy/rotatecopy.tex}
-\input{replacecopy/replacecopy.tex}
-\input{removecopy/removecopy.tex}
-\input{uniquecopy/uniquecopy.tex}
diff --git a/src/plugins/wp/doc/tutorial/tut_rationale.tex b/src/plugins/wp/doc/tutorial/tut_rationale.tex
deleted file mode 100644
index 185c7e699e4..00000000000
--- a/src/plugins/wp/doc/tutorial/tut_rationale.tex
+++ /dev/null
@@ -1,105 +0,0 @@
-\chapter{Rationale}
-
-This chapter summurize the results of using \textsf{WP} for proving
-the algorithms of ``ACSL By Example'' book.
-
-\section{General Observations}
-
-\paragraph{Missing Assigns.}
-Most of assigns clauses of the original specifications version 5.1.1
-were incomplete. This is not a problem when using \textsf{Jessie}
-because its memory model handles local variables in a different way
-than \textsf{WP} does. It should be noticed that in pure
-\textsf{ACSL}, the absence of an assigns clause means
-\emph{everything} is assigned. Actually, it is always a correct
-over-approximation, but in general, it is very difficult to prove
-something after everything has been assigned. \textsf{WP} complains
-with a warning for missing assigns clauses.
-
-\paragraph{Proving Safety.}
-The \textsf{WP} plug-in does not prove the absence of runtime errors
-ny its own. In this book, we use \textsf{RTE} plug-in to generate the
-necessary assertions to guarantee the absence of runtime erros, and
-finally prove them by \textsf{WP}. This is done very simply by using
-the \texttt{-wp-rte} option of \textsf{WP}.
-
-However, it is often the case where annotations generated by \textsf{RTE}
-introduce caveats for the \textsf{SMT} solvers. In this book, we choose to
-prove separately safety from functional behaviors. We typically use:
-
-\begin{shell}
-# frama-c -wp [...] file.c -then -wp-rte -wp
-\end{shell}
-
-Using this tip, we first prove functional properties without \textsf{RTE},
-annotation generated, \emph{then} we prove safety. Remark that proving safety
-may take advantage of functional specifications, but not the opposite.
-
-\section{Tool Chain}
-
-All examples presented in this book are automatically produced by
-\textsf{Frama-C}. Dedicated \textit{wp-reports} have been used to
-produce the logs and summary reports of this book.
-
-The reference version and tools are:
-\begin{center}
- \begin{tabular}{lc}
- \hline
- \textsf{Frama-C} & Nitrogen-20111001+dev \\
- \textsf{WP} plug-in & 0.9 \\
- \textsf{Alt-Ergo} & 0.99.1 \\
- \hline
- \end{tabular}
-\end{center}
-
-\newpage
-
-\newenvironment{summary}%
-{\begin{quote}\begin{tabular}{lcccl}
- Algorithm & \#VC\, & \textsf{WP} & \textsf{Alt-Ergo} & ~~Success \\
- \hline
-}{\end{tabular}\end{quote}}
-
-\section{Non-Mutating Algorithms}
-\begin{summary}
- \input{equal/equal_rte_report}
- \input{mismatch/mismatch_report}
- \input{mismatch/eqmismatch_report}
- \input{find/find_report}
- \input{findfirst/findfirst_report}
- \input{adjacent/adjacent_report}
- \input{count/count_report}
- \input{search/search_report}
-\end{summary}
-
-\section{Maximum and Minimum Algorithms}
-\begin{summary}
- \input{compare/compare_report}
- \input{maxelt/maxelt_report}
- \input{maxeltp/maxelt_report}
- \input{minelt/minelt_report}
- \input{maxseq/maxseq_report}
-\end{summary}
-
-\section{Binary Search Algorithms}
-\begin{summary}
- \input{lowerbound/lowerbound_report}
- \input{upperbound/upperbound_report}
- \input{binarysearch/binarysearch_report}
-\end{summary}
-
-\section{Mutating Algorithms}
-\begin{summary}
- \input{fill/fill_report}
- \input{iota/iota_report}
- \input{swap/swap_report}
- \input{swapvalues/swapvalues_report}
- \input{swapranges/swapranges_report}
- \input{copy/copy_report}
- \input{reversecopy/reversecopy_report}
- \input{reversecopy/reverse_report}
- \input{rotatecopy/rotatecopy_report}
- \input{replacecopy/replacecopy_report}
- \input{removecopy/removecopy_report}
- \input{uniquecopy/uniquecopy_report}
-\end{summary}
diff --git a/src/plugins/wp/doc/tutorial/tutorial.tex b/src/plugins/wp/doc/tutorial/tutorial.tex
deleted file mode 100644
index 011caded87b..00000000000
--- a/src/plugins/wp/doc/tutorial/tutorial.tex
+++ /dev/null
@@ -1,42 +0,0 @@
-\documentclass[web]{frama-c-book}
-\usepackage{longtable}
-\usepackage{pifont}
-\newcommand{\fclogs}[2]{\logsinput{tests/#1/oracle/#2.res.oracle}}
-\newenvironment{feature}[1]%
-{\footnotesize\begin{description}\item[\scriptsize WP #1]\color{blue}}
-{\end{description}}
-
-\begin{document}
-\coverpage{WP Tutorial}
-\begin{titlepage}
-\includegraphics[height=14mm]{cealistlogo.jpg}
-\hfill~
-\vfill
-\title{WP Tutorial}%
-{WP 0.8 for Neon-20140201}
-\author{Patrick Baudin, Loïc Correnson, Philippe Hermann}
-\begin{center}
-CEA LIST, Software Safety Laboratory
-\end{center}
-\vfill
-\begin{flushleft}
- \textcopyright 2010-2014 CEA LIST
-
- This work is based on the book ``\textsf{ACSL by Example}''
- published by the FOKUS Team at Fraunhofer Institute.
-\end{flushleft}
-\end{titlepage}
-
-\cleardoublepage
-\markright{}
-\tableofcontents
-
-\input{tut_intro}
-\input{tut_function}
-\input{tut_maxmin}
-\input{tut_binary}
-\input{tut_mutating}
-\input{tut_rationale}
-
-\end{document}
-
diff --git a/src/plugins/wp/doc/tutorial/tutorial.tgz b/src/plugins/wp/doc/tutorial/tutorial.tgz
deleted file mode 100644
index 52960d62a04e27c5c7843e61f852bb938670bb4e..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001
literal 8504
zcmXw;bzBr**!Guh_z4n<gi5C%3Q`M#ARP)wxzZvjNXH-{CEX=Rh!~)tfC4UEqNF0Z
zbV)3|EW2}_^?Ba+ulZ+YKKGe9_jO;__wXgsB7zP2?;<F+Y{Ps<8^5k%epLQfm{%12
z>U|OC>d$N+!)!^HkXOcr3{4@GPh<@jO&dP4**CO0oori3*GuU6EM3<MQfJX$?5%b0
zf!Bi$n!6iz9aowbXA=7k7~neJ-PiWD{5Oi2@$QEbgo*9X?$gOtqaltBlgW#pf{U^b
zduyk7Do<(enW5sIdzSqvBEvpZ{AB&!a8PtZKDk>_N?V@T!6Mz=aG6E9Z4lnjNpjnb
zTF2>lOysz(DVaztfHxbyud!YYUoXKS)If2K4|Y=6lWLpm+ARP)g!`v7goW7qM@2uW
zm6VzsAO&BSTFXoM!JHq48MI-i9|IhJHCPE{=g=dhmtZ~y5jxNwQ4r4)`CV;<$`QUx
z;JLl`YO+_0I>Bi}h02pn69#Es{O&79Ox$yBOc67cAQB?uG7`Eo7aJfIn$ym8Z*D>r
zJ6!C|vNNdo#bgPhy*wu$>+<_>Nhf-?sKKb6HeM!#3{k&g_6&DH5}REhPvk6Yu{<
zZt-}YzCK)+BKY3Odm8M2sQQQIH}6-0z+0`D$wzY?u`ck9>BaVxmdOUb$Fu2kd_R`6
zUTDOCdWT(H18Lz_afrZ`u;xRT`;=tIu}VkU!k)M`4PyqGpG!@#?c2v`@_sI!n@Jnn
z<~*fJ)Aii{y?es#A4?n+MHnIMWXW2=eXg1Gx?W>G*0FK^W<FKdEy>g4``7HTe6234
zTgfdVZvyF!_W?%=RO!G?_{$#&&IV~?=lOm*&o2Kt-Nc;i=AdY;!&xS(lz6W`Am8Q<
zv<bL~^xM7AnmokffW)%~?lSVSBxpxO%u)n0iWqF}AY&<*D=5AdeX(2WSxQ)88mHu(
zh(iKKY#^tj_jD*(kD>5?2d~D5InFw@vh)%7*ymBwpy6vI!K*=u^rLULe5+(^dq^gq
zN=blngN!2z%tXmWPS9QZz_ZC|36i8dL5c^10%hVCeGcD0t8pEw9ii9eCn6jsd#*}!
zy^Rg7H|j~JL-Yw&bX0Z4uWklva`fhg?*#*FC{mCN^i>)Xj=we&Yo<K8Pm4Kpu{+^M
z!cVzRIp?Ut;cz*+Hj7X9_(Ig@q&{5fO|EgYOl7jzDve-nnPbeg#gy)&wtYAXiE}0x
zL_S5#DykP;s|J!LVD-;4;CAsdVURxBneKz@-CmHB1bv@F(PVwxaUp-%240=%0)cyd
z1x&&X^KldJoY_lkfX3MJ?v6tJE*QQUPe2YLdbf~810SBI+yh*`v!~vysFQh`>D=ns
zkHW1XjebhW@kqp5;oDS}$mcCAvy9W5X%wC%)A_v70+z>{D;KV-2U++j_=?Hhj$?`K
zc}Xot|C`d0`X=EG3$`g-+WOLDbO3s@vOz%<i;6#6vI0DKf%)JZia{nA-mF?Z1eQ&^
zRI>`Eb7)qS8WrqeJp?phuT5a}`hqy65&OFj&kD)%J~n^P4V+%icY$NY$9R3Vo+8gD
zwJafGEH3h%4^RIn%c4;&EqxvrGA1hXMNz^W_wJsF^MAoss7%uKUokbUikr4(E2@iU
z$ySg`S8v#jF=6R8vQQ-$Y%GQAa4z`L)nXWSrpf*MBdGsSN&2t?*0GtZBT8R}slS+{
zs+KywmVA(*(foKxP-Ud@*4H`Inl;n+$lWaoeW@euhT?ZhqANhxUOjV{&(;oZNCFMK
zx{Ju<WT32Ya)_Jxi^=6r4ZZwU^gRBh(rJ3=+5W^YuTz~cRTs~h5NNhtye=3GSMp6$
zD{i4Zv_AlU2?y}&W<2boxUU7raEHuY3BENOQKOC7D3le*ifVUf`zFQoAw}?6&*AZ`
z3o_wy)eyV=sCcH<^x*BY>LaEL%s*e8Rv;7Y52;e?R+3)UX0(UDE7AU$d{^x|JYn(7
z5f@vW6&&$~hzuecRWjs6Q-kv&i&K43gS&g>Ki0yoXD47$PLy%<V1{=G%y^swMk;sP
z;X95C=YlP^i;#I_(z&LwSN`l@k67gYb-NVUZC)EIrwB;Pl~$y^5X8^jd+B1qm&bcr
z6?Z8zV^RdkHCeA^KXLbtT8d#B%kkF?h#i=9V4)XWXV(gOu%tcCCgO6%BgmJPa<G*<
z<SA#juJ6dB+?0Pcu+lE$Q3qhnD!C2KtUC^B@DR_17N_5^Wz>j9w5_aeIZYYWJv*^>
zC`*U`E-qlQejezR((Fk^Fsb%_Q{xJ|{F(k<ZqSNW#j_IDzDwoKT+?Js2k%~MCoi8G
zyyFwu=<^Mmw#Y6f-xe{HHIe;J`C#kH^OegoA5&31!sazgoSl`woXub2ih}}XCHB0}
z(>gaL#6*|^n&ahNOq~HNuX6VmOru(%!BY`Dm!UXtXY`Dcm`-;jV-*(X0hAdgb!U6p
zI!sl$@*J2&cTrC{)V4rZ4Ja}kC+&Wx5yjIX-vyPXj)&y(&ogl~YG+F7!9D@AuFwti
z7={Tc!Zgr@!a`o!ApR5oit7=ayaraiX0L*9HT|@&>j51eRJWmdS-r)n>gG=ibbWVG
zX=l`8Kz7$Y6bCtg@tfoz=L0Nj!&k3eJS}=ZSbN}AsG^Kd+nXU9g2fVLNhkUN2r$lQ
zLsN^D0f&Q-ZE}2z=Bh!jL1x&F@S=&zFWfcCEWRB?qtDU4U*#8EO)u^1R`iU=?h({z
z_pd!A{-~+8{$)KkthUhI(HZuok-hXr9?wc10n0TqC#lSM_?N7yiT^;gr-W)ck7jzf
zm)q|9)RXI9_B&YSbQJQawsCYt6{;t@?A|@Q_421z(u(*g2j{Pq=)_Oc)~b-NS42PL
zo65pT4Kp-7=}8->-2Jt5)WJ>=<hLh$mu^jIU3z8{%NJEt#1pI*uczKnTp0OR|Es$o
z`s&xUEjjPE`h-b?y(nk(qjeR*i$@P{`Y$@Fe!JlnDSx#ljrU2-Re_W%iEYL5-yVhu
zhEk(!``w~>{hlOCHnqtLRI~Axh!RRRL%MsW1dYgc^cJ^L6_oh*+!yXV3-Rzsd)d&i
z>vizH{@Jj%F42ohSxpf51&0!}2gksWX5y5^jv0;SjWEYM8PfDgna}zh(+ve`MWeGh
zUE5#2dC!qPSvk(KO>ROcyW#n)6ONl0%K#l58$cm@7;L=Mm+w&a%X6jyeLHr^SMc-K
z1gYS|C9tsv7aKOX>;bozPQSt92|O~rRPA$Qx?0cT8S68*H>s3p{h~~}ShJV=rc_*7
zPCFFRM6orZASwd-E`#Tj)Z9W=LPr=zLwpSg^X{LFXmqaNiCg69?yXxWZ$&2)Q0X|M
zo{vdH3kJznw$T{q@jy3$zQpqzTp7A6l{k?4SL@CSaK2wP6gg7r)o;$xb$oG@BSO;_
zk=~f1|M(s_H}N%p&ZS(HKcT(&5e92iyBQ1O+Q8P6{1vGGdQJ}LTLPmRq5wKxNy-JH
zn0vB-ZT~2@cQ8ws3eL#}O-=;lry<2<FpH8PYm@-;;lB*votp%=ejwfnDM)sJ&&D@I
z+@HW0qAn|<MxAth#D)+Ks3X%F;>$g|4{A4%e}q6KZ+i7q!f)U1{-(#7>yS!-|KqIC
zyZP{2O;~ys9(B#bK`NOWkRc0RSUTM036dlwE56HG_ktt@5PJ88%BZbu#af}Pb@bQ?
znv!TVE_(tU8Z*!E*2blxY3HB6h;HT(W7ip?v`?{9O^py@F3anHVeT=C+8?jZ=#3_-
z(2#jB`vi3+co??%H#!OHDSjJY#LTQ6_~*Jd))PFqbK;q~zi7yYuubJNvn|bNSIm~-
zZu(GPe4>Xte&1vrzECitW=9r#Cay;L>@0#@{#zs7<*UBl_J!h2?gt~$W_5f2TOO2!
z=hMT2wUTr!NxpAa047Re%>adac=!VmK1QtGkBXz^2(Bgd+>OADAaVn?huI%)&mY-{
z%?C|9Wn=WIg3e8O*^AHWCg0}i-qXfrXpIDk54=jAmW*Xv=h^Q#J1y($t8OQ2|L5I+
zw$03^mWEBvUqb;G!{NccJ@z6ELGZZ~FYU1i%3|Xrva%l73B9f%F5txtf^3*CdY*r2
z<}h+o#x*b3J^afA#o-t>R(O;84M&FIDAAeEU`YPC^iC~QpY)Raq^5sQnxzViY*_ts
zV8*{~bj~Vh?KFMV+=bR-FB2*!Kl5FxfGdBT0)O|ZPVn$$I*e>5XBqSPWnHQ>M{Jkg
zhShx3SR<o|PG`+*_L^qu9Ql$De&`=;rayo2RBASTe`(zQVt_}=FU}r`w)Q3G@6zpR
z;q1?h{h*yoC0#8dDUb+p@$JwX@X;#U7*vd3C7>AS4*Bjp97ux&cOF?KnwTME4Nf)Z
z7)@$7Pr<NGJ9z5^r|9+qo^T>&`(8INVsNTe4L`cE&ey;-0hQ@Q0$mSuTqX>7+F*w%
zA(+%qVimvpsmXMemM9-1h2!=wLL<4#YLR>Wj#xW!8IyD67w=h~V-Wwkk`&;XHHS9E
zNNef>X>~wzg0>{}`xyAUY$vrRO|<Gh7Ppq6Z;#p~So!sLfs6}AlPBnzc_La-G73`B
zTm-&}L|4_{;PPV>YiZ=AW9C~gm5c0+UW-l=;^dL-2A_Pr{K#jRbVxO3-2(;qlwgtK
zFWLjk4!=Qx0V~0+0etp&Ox)oDMv|S&AOwni2OWy$jHi4Gml!yb_Xr<YCFj3HMm&<q
zVMFN9>nz7s^7+ycQs+{)^L%tpR~SUPk-K&RZD{xqN^JP&;;=O_dnW+b2{~Pb^K78M
zx@UonR;AeB%T6>Gn5Z{^A<4`IFy1jvWUI%z{VsVy=B>rAPNA^3L+CAz)?#RE?_4Yn
z%FZg%cn>%?&{iIG@c7MU0Oe!;{x$h{%5u24TDK@ya~yH#j)CeSqD1*Q{})?LF5|1+
zZjfMn59B#gy>_Ah5VDQ~o(1@t;J7&qanp!g{z$sjt8d?EA#0Zzfl5HFIF8*^>nV6&
z=?69ZYJDHFxjP#Z*j#X7$GK;GX6Yg4hgg~y+`7qL%*PM3r$ZRVVy8SE8e+aNlT~#)
zH8be_*99SBzCA7sU0Vi*DgV220`$q44nR(!4V?Om(l+J3B8dY(sXWHjq#_Z?%Bf6_
zIyWhzd!G_4GqWD%4Ux-*m2`%c9Q=3ETt1<uL*7bN`uXA!_3R&p<}2ok_GVe3pAaB;
z9C)+=v<EkllpaWKh#AHA&kX^~C?Db=ma%RCbycht)Gk6(-N1r{P9*!{6b|7o!9Is_
zgB$J_)PUj7ibAk9gNiYpQZC6lze`eYy1U|t+4T~Z^;TqJ2knsBU_$Uf&1FVbOCIJl
zT7vxQF&_<v?ke+t-7kmf4gQohCK&gnci6PH*DZA>3D`d+e2|mpDLBVm)a*V--UW$G
zm~9j9l){|JU`ye>VG~UN|0zV8iNhLe%Nlz~s~qRRSTFXbsBf=qPQ7K-?V7KZYd$cb
zeNJze%tY2w3nIOw`Uo1Pu)qr~DQlUtN0D)74AWPr@t<u9WvlOL4Oaa=(;Tp<C_4Si
z>p`UeE-VfWCJ|hI;AWck_wevU({3;`n0734au3F%JxC5Et{R*|MZAO@TQEv}h%auw
z>P$pGyBh($$Ae_SG++R;NOt}O9jhE7QYR`He&d@V%qN8UBE30$XtDXvmp#6gn$1gr
z(ki_4^zS6wRQ7RS?_;m=wjSRrI3MOwg#cFLz+Z0w%w9W!Bo7e1a}`kS?`SvEz<Y15
zdl%R(PT!5T5*BMkn-kF<`vml;=Q$#pgS8x2=*S`%{%133(RELhosbmtAS`|uXe&6V
z%)B<FA^EaYP?=~N$whGEKM(ddum@(qqnh$=_4{Z}wY}NgdnMOOZ{TX&nMgrSDUz^r
z@EoLY*h~5?eaY!16RP5fl!$zgcK1PTzJ!ACALBb(A9_v^>&JTKl-AIDNb3@;b5bM5
zi4Y?+OokG7412JUioiUEKp*jzKK6Nd#Ml+K)u&ap)k8gnaD<`a9UI1Vho~{-n<7_B
zqnPtMfOs952oVa7gfTKF=tJW^0;xju)BFK`gaQZ;Q0ASpjN0GH*$=a1x~?h+g@@jK
z`XC~TRzNt&29{WU%lhEyMWT6W`-M9d4{`~Qj>Sb0kFs>!LaG?A(txaZ#3O)u3FpjQ
zI{}|k6Tqr@lvZEEW6~^;`NHI|*YJo>t%87IUjm*}IN*9w3gl!G$IF#*RKaG(e7%<W
zt)<tD1=H1j%B7$_nn}j)cch&K>@Em%JV-bJO&(=n^d`e1Yt2fYNy%8kn`=9gr3{@s
zL$@t2kyX>ECOI<iafh(l+OheAS$4`f(fax$*&o!3%jd^fQWww*2*hWC^c+U^5F8i_
zt!HQ#v%yzA9|!;@K~Y%zC*n;ekW_~oth7i1RYe3{yG`TnI3%(9(`kkUwaZ3)=g~(_
z%IZJv_EhH4BCt!wpQM(5Jgd&~hknTcID<nwG%%7p`xsbVB4vlIf4GVJI)e!2T_IC$
zKo5@WJ=wqbETq;4Jnn-X1tA#4GJk+yddf1yW+94*Y`)HKNs#RfqDuR!?rp=#jf=HD
z^j6|GX(<n4sBaf?XL}oFeKfe+kw#8Ze)3E_x;_pfeGiRCM07hIWqd{;ajvJtrR>Bt
zAbmV)jm+|U8<x?(rVL*F(s=WWNl}5>il6i9dBj7%v>kck`*1T>Dp-7&QfwJ27zA4+
z+f~e)uDjh#!yhi*sZv<@@JY1W?Q?L;`k$8DLJ{sw3GA&zA_%VkM^Q2#*Dbxwv5%7d
zDLfDTm^4DtZ9S0XW%|&P?8?w$L}70rZf(?@EzrX19(FGn+u(6YN#stbt#BVz_2V}m
zh{V+qrMG3Q)V)hNHp;r{SM>AOJ_BNa54!x=!PV>2Ta&^I5<i%(kF&<7@Y-K?bbhWs
zcsO_v*($A2N50!%LdLj6Uu9<+59sA09ufI!K)@s^TXOUtKr~*-cxeH8wQAe<WRCZF
z%gAl~Oc&7POcC@XMb7~t=7VeCbL!C{6z>NsbMWj*e3f&N`kqrUPaVYBeHyPjr_`sL
zrJyNBih0y(>tK=gFYq5910y$mzS;H;{ZNED;@$%GpzX~Cv16ylbZRls-OY?eu=OGh
zd>$e$g4<!OcNL6R$n`I;8~;ROY~}Fpb2?|w2vOe<XBHLOnT}|Fa(t|DeV&Y^lof}%
zNAda-U^oH6Jl{J>4neG>CkF8x$<(IGWuzKZ*XHfRo$TXX`9@@nsc+wyI$&^)voN3U
zNalpX&y<cJ{f_MJ0x4JfUT`3F#0ef#Nkh!Ap}+FYvWghBg>4<)&f=c8y!o1*S;@O%
zWuhf=&b2TaEuGa0+Rq~@V6@~rz(bM^$-4*@-qG9w2j`#eKc7|)v%RCEJA}lNiR$H@
z=&nWdOzm^nh{5C(Gdy1-ocgQo74lVlX`v*WQ{X<HtqWPO?6JO!-g?moYGP#_M=7Du
zjQM45eN%#4GGPA;sS~*2nivs)#O*Y}XTB3%qkMiC-9Nwhw=P+r3%x=>ZISF+8OgW=
zKYR>|Lo5-i%k$;gt))xt6|C0zd8_yT@2;ZiIPjthl*MpR+iZM5^`p>#IE%$64Cp;D
z4+fhriq+YEBUek3{E(z2g)Qb}1*`k8_4BHcS(^gV^T>ExLM5JlP8XK$1pb@J^T28?
zoWOT7;Q92wOI1z*!9~DTsfhOvMN`up_He50EsT06H}~R94T^F0#&(OuUdM&KzID%|
zhvibi$dgAH-=fHD;(oQV4i+VIEZqTuKyh*(cpuM8Dc-;T{VGvHHKmBNpK@)PlA=ny
z<w?Kscj|sxC05HE#&xe(jQnj-*Cb%Y1Li?6#ghT7S)8nt37fvbD*a5)k01w<sq0rk
zWa2^g1F-WciBJ>s8U`c~QEUb(F<Fz)S7*6?a7`cq=t26hggV?q8iJ!6t<H^D?LBDf
z-&VZ`Yo`#^_kg`3(xiFyR!|>#WHoR8vRp)ACJU<!-|c0>kIdcGG)f@eMw*?{Dw-$Y
zdq-K}2}$Ob0Io=e02$~+LR)xX-XM+z+5hmO-~sT-f-l5;Lu*$c-V7aI&3+-aza#F)
zH3|pt)4>)ufeSam?P79DV&TjhxSr2Nh%M8DIJzdx&BVzB0p|i}vh4te#$o`i97>$}
z-jQ*qp4zzj{gWkWd<G_?o7_k$=Hc9??Nzc{dM`<g;-O$kE1C)H?xNq5(zNSEGq_l-
z7hDcRPy`L5#tMJe(Bz2R$8nZ=B$iGgk~4)U6u;@$;YNpRD{k>f3%q7{9DKu)Cg1d7
z+)Ug|UAb4jgZ$R90`#@q!r%1BeqM!9fRoTT#(ve6B5KK^F<0$ef1*n8Gg`i@du4y=
ze2g6ne1oXZu+nfPMD<mCl~Xr)p`M3v_N;QsHb+Y6tU$@O(&5Y%pt9=}QrdcvM@qD^
zz{q8`7wtWNA<MuAb&3f*)PFNimynT9A7rquZbz}1(J>oROcY5jr!PYYM(ffTNmJX>
z=gnc7WR501kGPp+ZKX~*ZM^cufmu17=>~K`6>gfkhUZfeuuib;vv{b*_UWk{CrNoC
zNyicF3rHT^4-y<!3H`XshCmX_Z7egZR>{w)`g748mA5qd<rJd=L><~AJ&K=%ePvkr
z8cx$GNIA52<sfm$uL7D?TY0A?Rv_@wPL)mQSv536&=!HcG{B;y4tU|QQ3afDgu*U8
z*AG#L#@%aql`q&3x&D{Q+%J$&L>c_n<G2%FlT3;<7Z*U9B#;RRiA6<lVySS!cVAP`
zexxnAw@>5!qxi~zq7T(m3BHpk%D}odiNpEX)zem?kcMGl+<t#bP4l@gT$|4$#d=#E
z(ls<2*xqD_cq7lf*mc0aJ{TCCvGQ2=^X{kWckYwR^`5X>xN;gU`)rS%Fw*;Fb;)ck
z9_9J<YRH)DCFVC5yu8i4dOuyMTr+s8`?|H#MP*~rQ}G|lRYqhUL3*!&%L2G|<`9G(
z<FV)+X50pJVqU?5*k5TZChGjhzA3le{`Mw4!J?GRv>&pKC%7D-t=4!qRZyc+@6B^u
z*2=@BO<zRc9*ekiKig2)LSX6qU)$7Q#LZwgh8Rqv3kOGp&*NKpagIBiHW{yrg&MQ9
zI3{$GS|tdy$CEQH+O(|7{!@l5i*$Wf&4{2;H5xj5!OY!lK4Q7PCx3s9e3I{a(4IYy
zNuF(vh|<8@?oAtWN~~FLAtiGDj*hRe49jQ_=aJ-SvMmT~GjmhZC-yw>$;pQF<v$Mq
za|=^YK~hhvILSu|FYsZjkmt<cGk1XjHQ7~8{oQPzgobF*`y=a=7+U$`HocJ61DC2-
z=qA77le4(-GQhTnEG0!w9)VxLiPq{K=rN+Jx_;$>T<Fph+IIoBv;0v^d{X>5tun*0
zebh(XIz=wfzFGK*=#|P}4*j00f!jHMPgXvVXC!!;>Bs<S128Uogp$-egoJ5olEHrm
z|2{OF66C8%<P$dMB4Wf+$${QJxN?F#NIm=FR_=9}k6ZgJczQa)-P5Q2`352rx3h=a
zDM{!52eUhZ_LhAA7)>&6%V*PLQLfDV>~Ilp3aI`igB!p328SwLN#(%3+^xNTB?(O+
z_i3x`oOr8n{kQH}zAq)#6KWj8=#}pI$jFY+*Is>3GzX9J9@@b-R~gf0G!_3-GTgeq
z`z=V4v2*tS@oGtZvx`ksxEeW{5_(`yMD~Itk|Y2By!vAwvX*-JP4WCWp{SmG6Eax*
z2id!J<Rk|UO>!Q={Kt00(4*CplU5UTG1|;tE}IKN&!~gV$I2W{?FRPd)kqnP3PZ!A
zEvqkfsqJW`u(Q+2;K%cdb47H;vTsea!p(}8Bz4LLrw3U+T)jgmzHk7A_+f2lWwMBz
z@G6!i?coNAnrzYB**d_@^d(YwV=ch1g0iSP*gYI&v+_E6!wZdozLEVl<ZKQ*KEf@1
zfbPDv?b<!anVI>X$K5!^sbs8KE$O{c*1<_rW5m)r?-n>>L2QWasd4+<V8M%3ZMuC#
zJ-p=a|J2^9hgbJ1nSG-dz0(tgFJvV2wu}kFj#6AhK7Zvsf0aC^PA8&?NjQTWTMiZu
zXbE_#3#nwqa&Ds&j!#0!LYUEW;nFVK9)Z`sM6*#Drc*P|7p`k42XW0_8(Wp%`H9BX
z8wuygC=-_^o8kf<U9<DX#>yuWbZCQ>j*_W_a<Huo(p>E?t+PGk)$#jb_ygD2XlK+&
z-OlsoTjBjq=!j?8x=-K$?eT4@Xc|(~qQ2V)@tA-`62q}(aJqRLKTV^sX)8)*N;Wi!
zVX4A#l1l(la+qOR;p|2VgC_cjz+%zSC($kyYVE)N5L}5rvY<MRovIgcJ*kQv$_|sF
z#z*P@rnmT0wi7N#iZkmGnfPMf8nA991Z%KV;EQ1|u&$Ap@C)(LK$pijm)!jJt}aHn
zjL%A)b+;HwH!IXgg1*6t6fxxgTI)N=S#9+lL1celqp_4c9In{(8!X?pru)ATCccHf
zNpukb+$2^*I-Ri=Li@_mDPL@<6X|1^NDtDJDimwv&GX38=k1f1i&;|YA7_@!p(<Xu
zanQN>Q&1{b#x6GTRlv8^1cuNQi66dLR31g#BuGpF&-TzHpL6?CB}%6vV3DFeO>>to
z%%?JNFFyCjmQi>pmCJ3f`Zz`7bD-@M`sDt73>w#HWaSQ?quA?QWp`v-{8rn7pqi9@
z`Ay(nc05^PlqefdL8gu0V0A{#_?q};oyF-h>g#MtLis6>$}S*>J$htFj5W0lq!`c>
z+~UEfE&`uF=>(Hu7&kbIJoTc64pL@$3Tw$qZ0bgsTbq@HdVQH*Hxq!jUxW`4vv>eW
ze(!`_FNyjv{P&}VI!W;XQKt=jUII@8IrjnADVigF1>A^{MpQSR2~(*p(3WgN^fr!p
zo02G!u=rNm(q?};zMQ=|d6U}EE((q6*m+Nl`J4ZD*|%k*OKJ)`ATJ`AYSd7jMj_vC
zsoDK?zWZC7gFJ6Kcidw)*8Ccss}343-T3iDymC%U?8!+=PuU9TEdDgRT((JQ{CLLP
qLr8CsMJwS1ay>!n6N-7irVw1BRW+V5o}0XYhwf~BQb*8|BmM`{|H@qe
diff --git a/src/plugins/wp/doc/tutorial/uniquecopy/original.axioms b/src/plugins/wp/doc/tutorial/uniquecopy/original.axioms
deleted file mode 100644
index bbe63ce4199..00000000000
--- a/src/plugins/wp/doc/tutorial/uniquecopy/original.axioms
+++ /dev/null
@@ -1,29 +0,0 @@
-/*@
- axiomatic WhitherUnique_Function
- {
- logic integer WhitherUnique{L}(value_type* a, integer i)
- reads a[0..i];
-
- axiom unique_1:
- \forall value_type *a; WhitherUnique(a, 0) == 0;
-
- axiom unique_2:
- \forall value_type *a, integer i;
- a[i] == a[i+1] ==>
- WhitherUnique(a, i+1) == WhitherUnique(a, i);
-
- axiom unique_3:
- \forall value_type *a, v, integer i;
- a[i] != a[i+1] ==>
- WhitherUnique(a, i+1) == WhitherUnique(a, i) + 1;
-
- axiom unique_lemma_4:
- \forall value_type *a, integer i, j;
- i < j && a[i] != a[i+1] ==>
- WhitherUnique(a, i) < WhitherUnique(a, j);
-
- axiom unique_lemma_5:
- \forall value_type *a, integer i, j;
- i < j ==> WhitherUnique(a, i) <= WhitherUnique(a, j);
- }
-*/
diff --git a/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.axioms b/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.axioms
deleted file mode 100644
index 896a637257b..00000000000
--- a/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.axioms
+++ /dev/null
@@ -1,29 +0,0 @@
-/*@
- axiomatic WhitherUnique_Function
- {
- logic integer WhitherUnique{L}(value_type* a, integer i)
- reads a[0], a[i];
-
- axiom unique_1:
- \forall value_type *a; WhitherUnique(a, 0) == 0;
-
- axiom unique_2:
- \forall value_type *a, integer i;
- a[i] == a[i+1] ==>
- WhitherUnique(a, i+1) == WhitherUnique(a, i);
-
- axiom unique_3:
- \forall value_type *a, v, integer i;
- a[i] != a[i+1] ==>
- WhitherUnique(a, i+1) == WhitherUnique(a, i) + 1;
-
- axiom unique_lemma_4:
- \forall value_type *a, integer i, j;
- i < j && a[i] != a[i+1] ==>
- WhitherUnique(a, i) < WhitherUnique(a, j);
-
- axiom unique_lemma_5:
- \forall value_type *a, integer i, j;
- i < j ==> WhitherUnique(a, i) <= WhitherUnique(a, j);
- }
-*/
diff --git a/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.c b/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.c
deleted file mode 100644
index ad0dd30ddc8..00000000000
--- a/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "uniquecopy.h"
-#include "uniquecopy.impl"
diff --git a/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.h b/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.h
deleted file mode 100644
index 5cfea9e9037..00000000000
--- a/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.h
+++ /dev/null
@@ -1,7 +0,0 @@
-#ifndef _UNIQUECOPY_H
-#define _UNIQUECOPY_H
-#include "../library.h"
-#include "uniquecopy.axioms"
-#include "uniquecopy.spec"
-#endif
-
diff --git a/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.impl b/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.impl
deleted file mode 100644
index c1fdb1d1ed0..00000000000
--- a/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.impl
+++ /dev/null
@@ -1,24 +0,0 @@
-size_type unique_copy(const value_type* a, size_type n,
- value_type* b)
-{
- if (n <= 0) return 0;
-
- size_type j = 0;
- b[j++] = a[0];
- /*@
- loop assigns b[1..j-1], i, j;
- loop invariant 1 <= j <= i <= n;
-
- // loop invariant \forall integer k; 0 <= k <= i-1
- // ==> WhitherUnique(a,k) <= WhitherUnique(a,i-1);
- loop invariant \forall integer k; 0 <= k < i
- ==> a[k] == b[WhitherUnique(a,k)];
- loop invariant UniqueCopy(a, i, b, j);
- loop variant n-i;
- */
- for (size_type i = 1; i < n; i++) {
- if (a[i] != a[i-1])
- b[j++] = a[i];
- }
- return j;
-}
diff --git a/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.spec b/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.spec
deleted file mode 100644
index 1f60bc931c8..00000000000
--- a/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.spec
+++ /dev/null
@@ -1,24 +0,0 @@
-/*@
- predicate
- UniqueCopy{L}(value_type* a, integer n,
- value_type* b, integer m) =
- (n == 0 ==> m == 0) &&
- (n >= 1 ==> m-1 == WhitherUnique(a, n-1)) &&
- \forall integer i;
- 0 <= i < n ==> a[i] == b[WhitherUnique(a,i)];
-*/
-
-/*@
- requires IsValidRange(a, n);
- requires IsValidRange(b, n);
- requires \separated(a+(0..n-1), b+(0..n-1));
-
- assigns b[0..n-1];
-
- ensures \forall integer k; \result <= k < n ==> b[k] == \old(b[k]);
-
- ensures 0 <= \result <= n;
- ensures UniqueCopy(a, n, b, \result);
-*/
-size_type unique_copy(const value_type* a,
- size_type n, value_type* b);
\ No newline at end of file
diff --git a/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.tex b/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.tex
deleted file mode 100644
index cfc896e2f91..00000000000
--- a/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy.tex
+++ /dev/null
@@ -1,40 +0,0 @@
-\section{The \textsf{unique-copy} Algorithm}
-\label{unique-copy}
-
-We now study the \texttt{unique-copy} algorithm from ``ACSL By Example''.
-This algorithm copies the contents from a source sequence to a destination
-sequence whilst removing elements consecutive groups of duplicate elements once
-the first one is copied. The return value is the length of the range.
-
-\subsection{Adapting the Axiomatics}
-
-The axiomatization provided in ``ACSL By Example'' is:
-
-\listingname{unique-copy.axioms}
-\cinput{uniquecopy/original.axioms}
-
-The predicate \texttt{WhitherUnique} is defined by a \texttt{read} clause.
-It must be adapted for the current version of the \textsf{WP} plug-in which
-only implements a limited subset of \texttt{read} clauses:
-
-\listingname{unique-copy.axioms [adapted]}
-\cinput{uniquecopy/uniquecopy.axioms}
-
-\subsection{Proving the Algorithm}
-
-The specification of the \texttt{unique-copy} algorithm bases itself on the
-\texttt{UniqueCopy} predicate, itself based on the \texttt{WhitherUnique}
-function:
-
-\listingname{uniquecopy.h}
-\cinput{uniquecopy/uniquecopy.spec}
-
-\clearpage
-The implementation of the algorithm is:
-
-\listingname{uniquecopy.c}
-\cinput{uniquecopy/uniquecopy.impl}
-
-The implementation can be partially proved correct against its specification by
-running the \textsf{WP} plug-in:
-\fclogs{mutating}{uniquecopy}
diff --git a/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy_report.tex b/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy_report.tex
deleted file mode 100644
index b19f9865956..00000000000
--- a/src/plugins/wp/doc/tutorial/uniquecopy/uniquecopy_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+unique_copy+ & 33 & 13 & 3 & 48.5\% (44) \\
diff --git a/src/plugins/wp/doc/tutorial/upperbound/upperbound.c b/src/plugins/wp/doc/tutorial/upperbound/upperbound.c
deleted file mode 100644
index 1210b256cce..00000000000
--- a/src/plugins/wp/doc/tutorial/upperbound/upperbound.c
+++ /dev/null
@@ -1,2 +0,0 @@
-#include "upperbound.h"
-#include "upperbound.impl"
diff --git a/src/plugins/wp/doc/tutorial/upperbound/upperbound.h b/src/plugins/wp/doc/tutorial/upperbound/upperbound.h
deleted file mode 100644
index 87433aa2f1c..00000000000
--- a/src/plugins/wp/doc/tutorial/upperbound/upperbound.h
+++ /dev/null
@@ -1,5 +0,0 @@
-#ifndef UPPERBOUND_H
-#define UPPERBOUND_H
-#include "../binary/binary.h"
-#include "upperbound.spec"
-#endif
diff --git a/src/plugins/wp/doc/tutorial/upperbound/upperbound.impl b/src/plugins/wp/doc/tutorial/upperbound/upperbound.impl
deleted file mode 100644
index 97e47f49b5e..00000000000
--- a/src/plugins/wp/doc/tutorial/upperbound/upperbound.impl
+++ /dev/null
@@ -1,23 +0,0 @@
-size_type upper_bound(const value_type *a, size_type n, value_type val)
-{
- size_type left = 0;
- size_type right = n;
- size_type middle = 0;
-
- /*@
- loop invariant 0 <= left <= right <= n;
- loop invariant \forall integer i; 0 <= i < left ==> a[i] <= val;
- loop invariant \forall integer i; right <= i < n ==> val < a[i];
- loop assigns middle,left,right;
- loop variant right - left;
- */
- while (left < right) {
- middle = left + (right - left) / 2;
- if (a[middle] <= val)
- left = middle + 1;
- else
- right = middle;
- }
-
- return right;
-}
diff --git a/src/plugins/wp/doc/tutorial/upperbound/upperbound.spec b/src/plugins/wp/doc/tutorial/upperbound/upperbound.spec
deleted file mode 100644
index 6fc18831773..00000000000
--- a/src/plugins/wp/doc/tutorial/upperbound/upperbound.spec
+++ /dev/null
@@ -1,11 +0,0 @@
-/*@
- requires IsValidRange(a, n);
- requires IsSorted(a, n);
-
- assigns \nothing;
-
- ensures 0 <= \result <= n;
- ensures \forall integer k; 0 <= k < \result ==> a[k] <= val;
- ensures \forall integer k; \result <= k < n ==> val < a[k];
-*/
-size_type upper_bound(const value_type* a, size_type n, value_type val);
diff --git a/src/plugins/wp/doc/tutorial/upperbound/upperbound.tex b/src/plugins/wp/doc/tutorial/upperbound/upperbound.tex
deleted file mode 100644
index 91b01afc4e6..00000000000
--- a/src/plugins/wp/doc/tutorial/upperbound/upperbound.tex
+++ /dev/null
@@ -1,19 +0,0 @@
-\clearpage
-\section{The \textsf{upper-bound} algorithm}
-
-We study here the \texttt{upper-bound}
-algorithm from ``ACSL By Example''.
-Its specification is:
-
-\listingname{upperbound.h}
-\cinput{upperbound/upperbound.spec}
-
-The implementation of the algorithm is:
-
-\listingname{upperbound.c}
-\cinput{upperbound/upperbound.impl}
-
-The implementation is proved correct against its specification by
-simply running the \textsf{WP} plug-in:
-\fclogs{binary}{upperbound}
-
diff --git a/src/plugins/wp/doc/tutorial/upperbound/upperbound_report.tex b/src/plugins/wp/doc/tutorial/upperbound/upperbound_report.tex
deleted file mode 100644
index 019c9239199..00000000000
--- a/src/plugins/wp/doc/tutorial/upperbound/upperbound_report.tex
+++ /dev/null
@@ -1 +0,0 @@
-\verb+upper_bound+ & 22 & 8 & 14 & 100\% (198) \\
diff --git a/src/plugins/wp/share/ergo/int.Exponentiation.mlw b/src/plugins/wp/share/ergo/int.Exponentiation.mlw
deleted file mode 100644
index 63c0d3569f4..00000000000
--- a/src/plugins/wp/share/ergo/int.Exponentiation.mlw
+++ /dev/null
@@ -1,50 +0,0 @@
-(* this is the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** The theory BuiltIn_ must be appended to this file*)
-(** The theory Bool_ must be appended to this file*)
-(** The theory int_Int_ must be appended to this file*)
-type t
-
-logic one : t
-
-logic infix_as : t, t -> t
-
-axiom Assoc :
- (forall x:t. forall y:t. forall z:t. (infix_as(infix_as(x, y),
- z) = infix_as(x, infix_as(y, z))))
-
-axiom Unit_def_l : (forall x:t. (infix_as(one, x) = x))
-
-axiom Unit_def_r : (forall x:t. (infix_as(x, one) = x))
-
-logic power : t, int -> t
-
-axiom Power_0 : (forall x:t. (power(x, 0) = one))
-
-axiom Power_s :
- (forall x:t. forall n:int. ((0 <= n) -> (power(x, (n + 1)) = infix_as(x,
- power(x, n)))))
-
-axiom Power_s_alt :
- (forall x:t. forall n:int. ((0 < n) -> (power(x, n) = infix_as(x, power(x,
- (n - 1))))))
-
-axiom Power_1 : (forall x:t. (power(x, 1) = x))
-
-axiom Power_sum :
- (forall x:t. forall n:int. forall m:int. ((0 <= n) -> ((0 <= m) ->
- (power(x, (n + m)) = infix_as(power(x, n), power(x, m))))))
-
-axiom Power_mult :
- (forall x:t. forall n:int. forall m:int. ((0 <= n) -> ((0 <= m) ->
- (power(x, (n * m)) = power(power(x, n), m)))))
-
-axiom Power_comm1 :
- (forall x:t. forall y:t. ((infix_as(x, y) = infix_as(y, x)) ->
- (forall n:int. ((0 <= n) -> (infix_as(power(x, n), y) = infix_as(y,
- power(x, n)))))))
-
-axiom Power_comm2 :
- (forall x:t. forall y:t. ((infix_as(x, y) = infix_as(y, x)) ->
- (forall n:int. ((0 <= n) -> (power(infix_as(x, y), n) = infix_as(power(x,
- n), power(y, n)))))))
-
diff --git a/src/plugins/wp/share/ergo/int.Power.mlw b/src/plugins/wp/share/ergo/int.Power.mlw
deleted file mode 100644
index c5e16444dce..00000000000
--- a/src/plugins/wp/share/ergo/int.Power.mlw
+++ /dev/null
@@ -1,44 +0,0 @@
-(* this is the prelude for Alt-Ergo, version >= 0.95.2 *)
-(** The theory BuiltIn_ must be appended to this file*)
-(** The theory Bool_ must be appended to this file*)
-(** The theory int_Int_ must be appended to this file*)
-(** The theory int_Exponentiation_ must be appended to this file*)
-logic power : int, int -> int
-
-axiom Power_0 : (forall x:int. (power(x, 0) = 1))
-
-axiom Power_s :
- (forall x:int. forall n:int. ((0 <= n) -> (power(x,
- (n + 1)) = (x * power(x, n)))))
-
-axiom Power_s_alt :
- (forall x:int. forall n:int. ((0 < n) -> (power(x, n) = (x * power(x,
- (n - 1))))))
-
-axiom Power_1 : (forall x:int. (power(x, 1) = x))
-
-axiom Power_sum :
- (forall x:int. forall n:int. forall m:int. ((0 <= n) -> ((0 <= m) ->
- (power(x, (n + m)) = (power(x, n) * power(x, m))))))
-
-axiom Power_mult :
- (forall x:int. forall n:int. forall m:int. ((0 <= n) -> ((0 <= m) ->
- (power(x, (n * m)) = power(power(x, n), m)))))
-
-axiom Power_comm1 :
- (forall x:int. forall y:int. (((x * y) = (y * x)) ->
- (forall n:int. ((0 <= n) -> ((power(x, n) * y) = (y * power(x, n)))))))
-
-axiom Power_comm2 :
- (forall x:int. forall y:int. (((x * y) = (y * x)) ->
- (forall n:int. ((0 <= n) -> (power((x * y), n) = (power(x, n) * power(y,
- n)))))))
-
-axiom Power_non_neg :
- (forall x:int. forall y:int. (((0 <= x) and (0 <= y)) -> (0 <= power(x,
- y))))
-
-axiom Power_monotonic :
- (forall x:int. forall n:int. forall m:int. (((0 < x) and ((0 <= n) and
- (n <= m))) -> (power(x, n) <= power(x, m))))
-
diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver
index 1b6b435d6c0..8054baaeedd 100644
--- a/src/plugins/wp/share/wp.driver
+++ b/src/plugins/wp/share/wp.driver
@@ -151,7 +151,6 @@ why3.import += "real.PowerReal" ;
coq.file += "coqwp:int/Exponentiation.v" ;
coq.file += "coqwp:int/Power.v" ;
coq.file += "coqwp:real/PowerReal.v" ;
-altergo.file += "ergo/int.Power.mlw" ;
altergo.file += "ergo/real.PowerReal.mlw" ;
library truncate: qed
--
GitLab