diff --git a/src/plugins/wp/MakeDistrib b/src/plugins/wp/MakeDistrib
deleted file mode 100644
index 3f0d12127b38710e533f5495e4359e48fa5a231a..0000000000000000000000000000000000000000
--- 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 d8490466d97760335742e961c84e7c13a06b27ee..0000000000000000000000000000000000000000
--- 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 ae3501d929342b216bc7b9f4d68c3213ecf6706b..0000000000000000000000000000000000000000
--- 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 791197b43d9f8b4689339fa56331635712fe1820..0000000000000000000000000000000000000000
--- 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 083a9563227c4d82e8f83b67a9bd788dc8ee2b3f..0000000000000000000000000000000000000000
--- 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 d38b2f1f1b745175a3d4328b7533ca7ed0498cb5..0000000000000000000000000000000000000000
--- 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 ccecf0ee41220c676698d38565a5227db0c215c3..0000000000000000000000000000000000000000
--- 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 e5c1c8bbdc08e0de7ef3c8e807c3a5afc9e50f72..0000000000000000000000000000000000000000
--- 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 9b1e6753259b5b985692dc653833fe776fb7d987..0000000000000000000000000000000000000000
--- 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 3e6373ebea8132bc0c1d4bafc4da6772a728af2b..0000000000000000000000000000000000000000
--- 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 3540a564c33bdf15c1ace83ce4913cdd1ad9a975..0000000000000000000000000000000000000000
--- 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 5f2b995c955ca6ab6f19fbdf62f6962a9c1ccdf4..0000000000000000000000000000000000000000
--- 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 2b1e8d088d549a465a97001813dbc3e785f50c83..0000000000000000000000000000000000000000
--- 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 b8d4ece1619be33eed547b1115265720ffa1d81e..0000000000000000000000000000000000000000
--- 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 d883104e0c5555a7bd4a3f6057045ab3ffec8474..0000000000000000000000000000000000000000
--- 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 1e7c98964acda6f0dbf64642e774b447f57568ae..0000000000000000000000000000000000000000
--- 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 579961aff2e898f5675736e1e32df02d9c7dd980..0000000000000000000000000000000000000000
--- 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 17abd7b7138a0074609ae3596a87075e212dc58f..0000000000000000000000000000000000000000
--- 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 772f73fa21621864bb3f99ac65fa99825c8f3b3d..0000000000000000000000000000000000000000
--- 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 ad348d2f1d49a85cc1f220cbb28339964a6f532d..0000000000000000000000000000000000000000
--- 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 46b94a7d63f1e99c8236e9714ad46339a35fa6cf..0000000000000000000000000000000000000000
--- 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 f958c43592bd3604d741ffc4073455b88a17b0a3..0000000000000000000000000000000000000000
--- 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 74c6307e586329ef526b263fea83a81ed92a340e..0000000000000000000000000000000000000000
--- 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 6feee078a9ec86b596b0f1fec460f8a5e6070194..0000000000000000000000000000000000000000
--- 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 075082e4929f35491cdef6e26582081e61be3ce5..0000000000000000000000000000000000000000
--- 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 addd77e1a4f2e6a422e340e9b78316d0ea5b4e0c..0000000000000000000000000000000000000000
--- 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 c07f6483c3ea3823d1d2658753942b9f9f51e1f7..0000000000000000000000000000000000000000
--- 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 0872264002af988fc07f9b23cb399f3c40b68ba1..0000000000000000000000000000000000000000
--- 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 1c177e2527923a0a6d905f6226cf67f7e4ae155d..0000000000000000000000000000000000000000
--- 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 857cdc7a547a755256c241581e090590b2113788..0000000000000000000000000000000000000000
--- 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 eca77c4dd2045af3bd30359691d5d2df80b5f7d9..0000000000000000000000000000000000000000
--- 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 fe789f6c422c4a9905263fac80c4a4700ab10e08..0000000000000000000000000000000000000000
--- 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 c3e4ae03f26f7511a3fe28d944585cd7b4cfe8c4..0000000000000000000000000000000000000000
--- 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 5c90877059f502488533b58b361d99f1be8751ab..0000000000000000000000000000000000000000
--- 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 2837cf34c8cda289bb11c2e11b7fc7e257d15e82..0000000000000000000000000000000000000000
--- 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 c1174f633f0b3e2e34024b5a2c2f4c29326f73b7..0000000000000000000000000000000000000000
--- 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 83061061aaf695ed0b104c0a6802152bfb272a0d..0000000000000000000000000000000000000000
--- 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 b9dc882e46419490cfcc3e65ef6c18d5dd4bbf33..0000000000000000000000000000000000000000
--- 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 da973b08823f44cd9c9a554d1ebfa2d68e8e4ac4..0000000000000000000000000000000000000000
--- 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 60b60a1ce1e3ca69b5831603d3174594c1812c99..0000000000000000000000000000000000000000
--- 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 fe6624335be52114a24d5d76a9fa23a36f859527..0000000000000000000000000000000000000000
--- 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 b9566979105de93f0ae49594f7d4cfc8fd7548ce..0000000000000000000000000000000000000000
--- 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 1dc7bc21cf5a9ace11d031439d42cace6cbd65e5..0000000000000000000000000000000000000000
--- 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 ce3f24f0aae5e85e780569811ee176b5e0814c00..0000000000000000000000000000000000000000
--- 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 cc7533c3b48c9b93802f98176e5c17bc1c219473..0000000000000000000000000000000000000000
--- 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 81f198ffd81c5ace6c7aa565fe4401087437cc4b..0000000000000000000000000000000000000000
--- 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 c975eaf8c564f1a99cd9dc57c011a8fb5af16899..0000000000000000000000000000000000000000
--- 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 9fbbff20b1848cee961303f71c81e9c388ffb6a9..0000000000000000000000000000000000000000
--- 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 e83b19599991546f7e3625b5d7afbfeb62f059f1..0000000000000000000000000000000000000000
--- 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 fd3834d869c8ec13fa743a26ccc53ef165131c7f..0000000000000000000000000000000000000000
--- 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 c4be22ed82478d65c67faa25c45ef76af0fc9c3e..0000000000000000000000000000000000000000
--- 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 70c0536a19160dbc83a8865a9beeb22ab3ce9391..0000000000000000000000000000000000000000
--- 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 9b1c7ac9a13fbfab0aa98b08bf4699123a1516f0..0000000000000000000000000000000000000000
--- 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 a4b7e43688e787449cedbe53d04711402c0112c2..0000000000000000000000000000000000000000
--- 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 a742c088480c7e19808edba459f05be52f37d500..0000000000000000000000000000000000000000
--- 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 68ced6622208c7f7897afbb8554236a9c30dcbc2..0000000000000000000000000000000000000000
--- 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 a874b62754c90d9cfd5a0ecc31a9bad3625a1603..0000000000000000000000000000000000000000
--- 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 0e659d8f6b8ef4bbdc5b325088412d456739ca47..0000000000000000000000000000000000000000
--- 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 6be0419195fbab5a701156e62e050e7219e3598e..0000000000000000000000000000000000000000
--- 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 21bdf01b36160576afa020d4b4bb1737adb5cf68..0000000000000000000000000000000000000000
--- 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 be30fb066ea9e6c118831d5f2926ecdebebff46c..0000000000000000000000000000000000000000
--- 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 e8cce5cc4376590a2f9f8b44e04d5460f6a08784..0000000000000000000000000000000000000000
--- 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 541e019a9c2d632642eb4ab757d3d04b80034873..0000000000000000000000000000000000000000
--- 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 33cb76383ef20172537d000e91f65e7ebe0ef90f..0000000000000000000000000000000000000000
--- 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 82cfa1ddb379a9d9809d2bc96c87d92866b59e89..0000000000000000000000000000000000000000
--- 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 53348154c4ac7e5f2eaadc909bf28b73857583ad..0000000000000000000000000000000000000000
--- 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 d442aa09ea0bd4afacb7a28bd7998b3d3bb6e8c4..0000000000000000000000000000000000000000
--- 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 671e8edeba08768a76435d47a9a69dadc4a8369c..0000000000000000000000000000000000000000
--- 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 905586a015e9d1ec916aec218b8e2a1f0417f667..0000000000000000000000000000000000000000
--- 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 efb8501f463e8ba0cefd7e234102fb1dface2e2e..0000000000000000000000000000000000000000
--- 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 a5571e11fa445d58d88042c2440596318a80b994..0000000000000000000000000000000000000000
--- 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 88234d3b1f5258871276fb5dd2ad95bf8384b1e1..0000000000000000000000000000000000000000
--- 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 977c9dbd0c30474a8c9b4a8435fdb90929c993eb..0000000000000000000000000000000000000000
--- 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 8911c7c003821206ae127fa19455ae004391d25a..0000000000000000000000000000000000000000
--- 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 d70d08a0506b296fa521802157915ba0ca9e22cd..0000000000000000000000000000000000000000
--- 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 9feb4e9a420a829a0d68660e21ef2a2a532ed877..0000000000000000000000000000000000000000
--- 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 00e7267a3db5a39ea9c307eafbdf0d262b811d84..0000000000000000000000000000000000000000
--- 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 9a04eada1be817e6ee90f11b3035f8402f16a651..0000000000000000000000000000000000000000
--- 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 a88a675487a6c668ed0bc76c5f64c3d4264affa6..0000000000000000000000000000000000000000
--- 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 8ecc4240c22b8cd632256b7c2f979fdb81c62f0d..0000000000000000000000000000000000000000
--- 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 b1cca9dccbbaf9323037a297fdeaa1c8340094df..0000000000000000000000000000000000000000
--- 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 e2eaac29659ff8d481d81f7134ac3f04e59fc728..0000000000000000000000000000000000000000
--- 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 05ed0eccfbf281c60ae5d055b5aa71da7578a8d8..0000000000000000000000000000000000000000
--- 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 389cbfad42832cc81b8af6bf696a8f4278a0803d..0000000000000000000000000000000000000000
--- 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 5651556635a95ad7a06df0ccf6c8e9c3e793ed77..0000000000000000000000000000000000000000
--- 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 4ca3f6079cd99268987bfd27cb7c7fa1a16220c6..0000000000000000000000000000000000000000
--- 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 2c93372d5e76b55236ffedd20576773e994eca09..0000000000000000000000000000000000000000
--- 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 c92ff8d0a59655ed2c6525a2c7fb66d5348c6a2b..0000000000000000000000000000000000000000
--- 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 5f8d931476367b546d86f6d1ab1f33d8cf61cf7e..0000000000000000000000000000000000000000
--- 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 4d77444a0af453c56ca4e26698306c631c5e961d..0000000000000000000000000000000000000000
--- 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 2f0974f61f51f65bb84db53d3bb626b67a0822bc..0000000000000000000000000000000000000000
--- 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 cbb75f978f9e82124c6e3174a2f3bd789ee0f7f0..0000000000000000000000000000000000000000
--- 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 6b92f962d88b42f1ff6c9127254942203d4d3c27..0000000000000000000000000000000000000000
--- 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 876bd28bfa3eef452a31f1af6ad909e6700ecbfd..0000000000000000000000000000000000000000
--- 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 8ae31ba54ac0200c10d6bc0b5d7cb0191e059d09..0000000000000000000000000000000000000000
--- 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 741718dd7776fd25ec7fc060ca4b73072e50cc13..0000000000000000000000000000000000000000
--- 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 2f0974f61f51f65bb84db53d3bb626b67a0822bc..0000000000000000000000000000000000000000
--- 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 c0b3da8c7c5354fde00267b08be24cc5268b1840..0000000000000000000000000000000000000000
--- 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 a6dafbeadefd265a78e73a6f1cfc77d373d7b73a..0000000000000000000000000000000000000000
--- 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 4d0ffbba1fe98aee5f99f6f0aefe6e96e100fdcf..0000000000000000000000000000000000000000
--- 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 c7fb3459b99aff6e4a3295ee47bda71aff75291b..0000000000000000000000000000000000000000
--- 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 3e2d87fc879e39e27c5895ee747c38522923717e..0000000000000000000000000000000000000000
--- 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 52169f842f746ff9a4ec4ffe147a90144de7592c..0000000000000000000000000000000000000000
--- 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 7576b4d86b2e5a682e1db7ef8636354c89496936..0000000000000000000000000000000000000000
--- 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 b847d485ed8c4ac1296efde4a725d15e8b703f3a..0000000000000000000000000000000000000000
--- 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 b656136af231e09860898d3588e0ee821bfbf3ba..0000000000000000000000000000000000000000
--- 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 6df811c7c2946cd606089cb6e3a28ae4fd8ba513..0000000000000000000000000000000000000000
--- 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 dfe720cdefd1d55b325d4700e4626e9e646ee362..0000000000000000000000000000000000000000
--- 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 a57ed273c7c4a95d78c189a444882d6be98d005c..0000000000000000000000000000000000000000
--- 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 c8191f091f447949491e977a339a67b6446defd3..0000000000000000000000000000000000000000
--- 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 07b4f320690f3c99f79b88899f168bf466417c06..0000000000000000000000000000000000000000
--- 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 7d67cdf7476eb11d3b896caf7c42c0823d3a17e8..0000000000000000000000000000000000000000
--- 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 347716f761f9b2a0d654ffb8cbb337e97581fe86..0000000000000000000000000000000000000000
--- 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 ff1166419c8fc30fcea2a7f04e255f5c8d7c36a1..0000000000000000000000000000000000000000
--- 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 04d70543f787bacce7f26d412750e37c9fba4664..0000000000000000000000000000000000000000
--- 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 bff388eed3e7f13146879f0ba59c8433ce5757f0..0000000000000000000000000000000000000000
--- 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 6295344844345bf58f0e023c3c332b050321a9d5..0000000000000000000000000000000000000000
--- 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 a47029927cd432eeaad08d86cae791f07e4af0cd..0000000000000000000000000000000000000000
--- 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 0d8279753d717c6b03c9cea56d540be092f24111..0000000000000000000000000000000000000000
--- 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 31308027dc626cb6b152681d417a40495011fe0d..0000000000000000000000000000000000000000
--- 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 ef3a0bba86a2303f1908dcc0abdabdaec32c4897..0000000000000000000000000000000000000000
--- 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 20e70af48c4f8ff123a64f1130d428362dcd21b1..0000000000000000000000000000000000000000
--- 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 a8779c18ec4a0315db6d5c5226d36535605a79f1..0000000000000000000000000000000000000000
--- 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 96be419b4b412de4b7f42727907562f9813c622b..0000000000000000000000000000000000000000
--- 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 40749040ebfb03a6ab9de43edf3ca185d8e727cb..0000000000000000000000000000000000000000
--- 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 340c6454f724eed659c2638ac1efd1f190210ec5..0000000000000000000000000000000000000000
--- 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 e3d60afaa38cdb6a332084b7bf194d704f88c5be..0000000000000000000000000000000000000000
--- 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 7f4c67e868f086ae86589c346f0690db5b99cabd..0000000000000000000000000000000000000000
--- 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 a03905b4b3c2c6cc7cf139912784f65335b7393b..0000000000000000000000000000000000000000
--- 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 41847d52fcaccb28c34b7c32f26b8b10e106b5c8..0000000000000000000000000000000000000000
--- 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 617b2828d1850c1f25bde981e4fd89f25b537c2e..0000000000000000000000000000000000000000
--- 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 43465a136659e336a423a353ec8eb35b8aea9942..0000000000000000000000000000000000000000
--- 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 97e150a2aedfc6df02dc500b574ff7672486fc4c..0000000000000000000000000000000000000000
--- 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 4e08fe3c7fbb0fb6dcfbdb3b2cec09eb07f884aa..0000000000000000000000000000000000000000
--- 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 1f19aba55c6f691101edc3fe01c677f5a41e25de..0000000000000000000000000000000000000000
--- 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 c4e646d020a37ed58c2693e3f6aebc13452204de..0000000000000000000000000000000000000000
--- 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 dd41f3e81c66e3f3860d04e162021a60dc10e2e4..0000000000000000000000000000000000000000
--- 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 b69f67eb5a4f5bc89fcaa0e79be31830ed6ab570..0000000000000000000000000000000000000000
--- 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 cecdd9632c0f5287882c7676267c3069059f0132..0000000000000000000000000000000000000000
--- 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 1ff6a4887dd23b7c2a9ecc1352925efc51b130b0..0000000000000000000000000000000000000000
--- 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 d3de6c759a4baabad4f87644263d4539c2ef5687..0000000000000000000000000000000000000000
--- 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 e22adb305fb68e15b00499ad4087d67ef58bfe44..0000000000000000000000000000000000000000
--- 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 b237af53c84d36217cdf6bd15e561b34c870f014..0000000000000000000000000000000000000000
--- 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 be294d74919502af79db01a92ff7c78baa20ce71..0000000000000000000000000000000000000000
--- 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 fd12238c7089b8a9f1927d11226a4fee175718ab..0000000000000000000000000000000000000000
--- 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 b7c7a4731ad06d1b7e6311c461ca5dd663767da8..0000000000000000000000000000000000000000
--- 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 4262124342e7b56c4c9a2791b19ece78832989c1..0000000000000000000000000000000000000000
--- 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 ed518bc3e63ad19cc58db8f4f8901fa56e2e0855..0000000000000000000000000000000000000000
--- 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 db02b3f827dcbb220c798feb721fb5fa9ccd970f..0000000000000000000000000000000000000000
--- 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 69a948e79ad0ac9367599a92a454c504fb473961..0000000000000000000000000000000000000000
--- 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 cdaf8f03008643d096d0290dce41d5bbde63937a..0000000000000000000000000000000000000000
--- 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 3a0a9ac708f55b96ab405abfcca47d14482df707..0000000000000000000000000000000000000000
--- 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 419390f59958546bdeaeb25ec9b4e91f2cb89564..0000000000000000000000000000000000000000
--- 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 4c0d081fe5705ba35bb15d360a2649741c3d0813..0000000000000000000000000000000000000000
--- 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 24f91a20d326bc8a16efa20a4d621ec0126ef7c9..0000000000000000000000000000000000000000
--- 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 8b80e17532bd849b11414b9853372d3a190eb88f..0000000000000000000000000000000000000000
--- 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 791e263de29730e1bcc2862d7affed9c0423a78c..0000000000000000000000000000000000000000
--- 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 1a91379dc1e6c270a982d3c1478fe84799e3f271..0000000000000000000000000000000000000000
--- 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 19201ce5a5471293fb9c8716d51337f56f3a7f0c..0000000000000000000000000000000000000000
--- 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 4e5fa933de4bb9db369158d8a2f197ab91ffece2..0000000000000000000000000000000000000000
--- 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 7520d28497b39c4a4102d5316562b39698d7526c..0000000000000000000000000000000000000000
--- 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 d7bf72a5d79d4cf9062bbede67fe7ce9f7cfcd69..0000000000000000000000000000000000000000
--- 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 4f1a82a226f562f98b8faaaf4ba596c3eeacca01..0000000000000000000000000000000000000000
--- 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 78d75bff82d1bf7eacaddd8a555323da1f28785e..0000000000000000000000000000000000000000
--- 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 4d502e0e01fdbef5aec1fb6a68c29214cfd1943a..0000000000000000000000000000000000000000
--- 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 900958c47db092b75f0eee4a6ead599538934d46..0000000000000000000000000000000000000000
--- 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 fe13ddae37ea2409dac934f4846b183daddcd44c..0000000000000000000000000000000000000000
--- 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 c1220390d58b2d1d4fb8a33a328f61bd4ac7d6cc..0000000000000000000000000000000000000000
--- 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 861054e15ee63cf7270a144ba90f082b89b28cd2..0000000000000000000000000000000000000000
--- 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 625aeeffbc96e5058c051db75d1458cdee36b93b..0000000000000000000000000000000000000000
--- 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 d3f0aea66f4a6f1537cf6a5ec8c100272cc26bbe..0000000000000000000000000000000000000000
--- 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 33a59c589c924dbf7047b8dc9909b738fa0987e2..0000000000000000000000000000000000000000
--- 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 e09793267fc212ed44d637d643175a7da1ab393f..0000000000000000000000000000000000000000
--- 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 638829b68e770e74780afa2ee4fb039a67f1638c..0000000000000000000000000000000000000000
--- 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 60e173c455d31949330e7dfc457318f780ff1485..0000000000000000000000000000000000000000
--- 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 f908540bd0c98cfb21663521868638b60ad91899..0000000000000000000000000000000000000000
--- 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 35d5fee8805d0a6180cbf2969edb6224d63ed33a..0000000000000000000000000000000000000000
--- 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 c9b33917bb9aeb86f2c39e39c5fa4ede2ef0e0c5..0000000000000000000000000000000000000000
--- 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 abed2a54e32ca0e5b45047717779fa2227ca0812..0000000000000000000000000000000000000000
--- 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 17ffb560c44a78eaa1052e8411ccb3df9f5a956b..0000000000000000000000000000000000000000
--- 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 836070ec3f3452911328e791462a48e20a96e05e..0000000000000000000000000000000000000000
--- 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 abed2a54e32ca0e5b45047717779fa2227ca0812..0000000000000000000000000000000000000000
--- 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 d1e446023da0bca74c7c03be0ea9cf55f202176a..0000000000000000000000000000000000000000
--- 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 60e04a1907bd00113cb19cd043def3049859951d..0000000000000000000000000000000000000000
--- 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 1b248b7e5802ce370721770c7ac591f657b543c6..0000000000000000000000000000000000000000
--- 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 77a41a5002f267ea12f12c9a4ced8cca88d9ad10..0000000000000000000000000000000000000000
--- 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 39a854de9c3fcd4adb1c40311ef58211499a8b64..0000000000000000000000000000000000000000
--- 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 7b138b4ca17781128aed97ea5ee58a62d3acb40e..0000000000000000000000000000000000000000
--- 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 dafee56c3b91d5e290bddf07e1a3991dd11f82ad..0000000000000000000000000000000000000000
--- 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 3fca20e9581db651e96695c0d8475add293dc554..0000000000000000000000000000000000000000
--- 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 a031083b0bf5d2d088201494ce7b7d05d7122e07..0000000000000000000000000000000000000000
--- 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 4a912f7b7cc664f20b3155cb8a5a9b9926bfd358..0000000000000000000000000000000000000000
--- 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 a5805ee2d9b67ca6e51c256acd445602eec94b23..0000000000000000000000000000000000000000
--- 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 06be70fe89843fb24f09692802ec26d62f11d9cb..0000000000000000000000000000000000000000
--- 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 6f6a79ff3af919ed29c978a2ed8ec4cd6faafc1f..0000000000000000000000000000000000000000
--- 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 d96f773ef2282e0f3250a371b477db9035908af2..0000000000000000000000000000000000000000
--- 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 de32d853ef4d3b9b0d3cafc9c35181d998f416fa..0000000000000000000000000000000000000000
--- 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 c57f6f5b0d1677bad94a2bc2bdc165d6dfc156a2..0000000000000000000000000000000000000000
--- 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 7e73d6924ab3331f3669feb255c8b2113b1869f0..0000000000000000000000000000000000000000
--- 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 66e1995e102445cbefaa536c43a8da4ff5224e55..0000000000000000000000000000000000000000
--- 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 1c725b37f632b869ba2d816220ca0aa6955afdc6..0000000000000000000000000000000000000000
--- 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 a58d777553c847226d65130b86ddf741c374c03d..0000000000000000000000000000000000000000
--- 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 00eb8b0c422ad74cfd1378ee210a7d55d76bab82..0000000000000000000000000000000000000000
--- 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 00eb8b0c422ad74cfd1378ee210a7d55d76bab82..0000000000000000000000000000000000000000
--- 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 3d13dba59cff1cf4a6252aaba23def3a4808ba3d..0000000000000000000000000000000000000000
--- 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 542dfd8b74525abf2f1d24f9397eecbcdad002b2..0000000000000000000000000000000000000000
--- 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 53a2a88968abd45142de399b4ae3c69ddc4d74af..0000000000000000000000000000000000000000
--- 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 4492d9cf9531ef8e8323298f3f99524bce7dd077..0000000000000000000000000000000000000000
--- 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 55ab4468e5b2cded661c05412846c67addad0fc7..0000000000000000000000000000000000000000
--- 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 7c954059cc6919710db196e6cf21a867f3190e3c..0000000000000000000000000000000000000000
--- 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 2f1a1e505be1c66c6575f4d753e040a7e9a404c8..0000000000000000000000000000000000000000
--- 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 8f2becab5a5969712c59bdcd0ac8989e978e1b17..0000000000000000000000000000000000000000
--- 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 b05f75df8ee46e823381dc4dbe0a5df8ab8cdf1e..0000000000000000000000000000000000000000
--- 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 404d2414e3a8e1f3f7a4a8fc618ad241c933c9a0..0000000000000000000000000000000000000000
--- 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 1a23c9f627cfba7cf299f943693ea5fe2e0becd4..0000000000000000000000000000000000000000
--- 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 e217634d7e9b915483379f7d8e43f0ca9eade13a..0000000000000000000000000000000000000000
--- 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 8888733622ef84baa928dac52cce772b3ca6ca40..0000000000000000000000000000000000000000
--- 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 23a92d8e21030c03ac64c85744664130ce3fa329..0000000000000000000000000000000000000000
--- 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 18a6058cf5618bbd55535a730af95755e2899491..0000000000000000000000000000000000000000
--- 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 8a12874cbab9df28d546b428f754f84af7526d88..0000000000000000000000000000000000000000
--- 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 1cf01894857b611ac62278f8e8c76382e1295db9..0000000000000000000000000000000000000000
--- 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 2c72649a2d5285de49e2c9f300b7755604bc35e7..0000000000000000000000000000000000000000
--- 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 5f756508f21ff0575b0368dfdbbeaaa189f6c051..0000000000000000000000000000000000000000
--- 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 ce1af5dc8586bb8eba81a572226e0ddd0590a84b..0000000000000000000000000000000000000000
--- 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 e5b947e8e232f00bbcafba55a540b24d1c42bc2c..0000000000000000000000000000000000000000
--- 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 00eb8b0c422ad74cfd1378ee210a7d55d76bab82..0000000000000000000000000000000000000000
--- 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 7da97640313cbee63654bc1460e1c1337f18b2b5..0000000000000000000000000000000000000000
--- 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 dea079729dde7098902534b6f489501150d79383..0000000000000000000000000000000000000000
--- 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 963aa89eaf1da6e187ea9da6e9cba817b8362ed7..0000000000000000000000000000000000000000
--- 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 238975e0129aabceb8cd5d37a8599b8f996593d2..0000000000000000000000000000000000000000
--- 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 b4de719217fd17fe577dd24659055ff74f7a63a4..0000000000000000000000000000000000000000
--- 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 6a36817b36559eb90bfeb3a44f720962cdde086f..0000000000000000000000000000000000000000
--- 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 1f25c3b212e3a4d08205b9de240971494717797d..0000000000000000000000000000000000000000
--- 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 5a7b60e7f635d496c4ededd706131c6b5ad2dc6e..0000000000000000000000000000000000000000
--- 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 fcaf18df6493ed107db19d9afcc3c070f30cf74e..0000000000000000000000000000000000000000
--- 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 8805de5ec86f02984f62fff9541f5879d38cd99b..0000000000000000000000000000000000000000
--- 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 ea361f2e9c0eaa26d93e0b03f14454546e0c3efb..0000000000000000000000000000000000000000
--- 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 d814045627c3774cb15d35b41784cfd272a5aa1b..0000000000000000000000000000000000000000
--- 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 267c8fb5bd318538dfd5308c9c768c4e1b250749..0000000000000000000000000000000000000000
--- 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 77ed294c38fd022a7616a3219ec92ad3317d3a3c..0000000000000000000000000000000000000000
--- 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 d022459964fad4c9320eeaa652ef534b93deec0a..0000000000000000000000000000000000000000
--- 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 b138d449c537cf8324bb7c6ebadff092fcb11384..0000000000000000000000000000000000000000
--- 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 1f70ace71c3cbc521078b9a0c28a1a5a89f73985..0000000000000000000000000000000000000000
--- 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 00d18c5d9b7598639aaec2a3434829f2a3996d1d..0000000000000000000000000000000000000000
--- 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 bf426a6687c01e0b05dc889c9a58485bcc6e29c0..0000000000000000000000000000000000000000
--- 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 0370931cb7977670f06c476eaf57af67886ebb74..0000000000000000000000000000000000000000
--- 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 4425f4ef1ad944e2acbd6a7fb24bd959c9870ea7..0000000000000000000000000000000000000000
--- 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 9d9b0ab39e6da9ea73975209c5037a1e47592534..0000000000000000000000000000000000000000
--- 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 39a9c53f1162ab1050a96c26cb451f561bdb287e..0000000000000000000000000000000000000000
--- 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 b48e5486357e1f517ffa3bb243882c987500db6c..0000000000000000000000000000000000000000
--- 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 082b761661ddf9075ade344f482d6f35e6e41456..0000000000000000000000000000000000000000
--- 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 2ea5d7f818a59de3d331d610dc8d65fee51c26a5..0000000000000000000000000000000000000000
--- 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 185c7e699e428fed76630c91111e50420c6e57d0..0000000000000000000000000000000000000000
--- 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 011caded87bc0a1c1f031fd2724e0e3e65ac24c1..0000000000000000000000000000000000000000
--- 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
Binary files a/src/plugins/wp/doc/tutorial/tutorial.tgz and /dev/null differ
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 bbe63ce41997f8954bea6f64637c28267ce6a3ef..0000000000000000000000000000000000000000
--- 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 896a637257b59d0a080de131bfa3d8b94132e5d6..0000000000000000000000000000000000000000
--- 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 ad0dd30ddc8dadf35f3a8053f389dfdb401e1532..0000000000000000000000000000000000000000
--- 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 5cfea9e9037b306bcdd26447e88dd92be3d8a4fb..0000000000000000000000000000000000000000
--- 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 c1fdb1d1ed048d77a7702b6d2c917fc165f0be93..0000000000000000000000000000000000000000
--- 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 1f60bc931c81b9ea5af47a0bb7cfad58d663589d..0000000000000000000000000000000000000000
--- 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 cfc896e2f9108fcdb3e902249db4f7150bb81b12..0000000000000000000000000000000000000000
--- 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 b19f98659566bc573f8199c3c11244b1b02169e3..0000000000000000000000000000000000000000
--- 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 1210b256cce31aa99ca221e0955273468119fde5..0000000000000000000000000000000000000000
--- 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 87433aa2f1cce2c0960da0db47dab60f35282388..0000000000000000000000000000000000000000
--- 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 97e47f49b5edf4940283453bc6fef682405aa06e..0000000000000000000000000000000000000000
--- 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 6fc18831773d568cc28f57ed01d08af07915b65e..0000000000000000000000000000000000000000
--- 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 91b01afc4e69dea281612b3f656c23a5d88a77d5..0000000000000000000000000000000000000000
--- 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 019c92391993fb00aa60932acc6dd8dc59dc3f1a..0000000000000000000000000000000000000000
--- 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 63c0d3569f4a36cdae9e270507d1bbc6809e04b6..0000000000000000000000000000000000000000
--- 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 c5e16444dcefddb2047018168da6416f8cf33bb7..0000000000000000000000000000000000000000
--- 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 1b6b435d6c0365ba1c646919fdd8e489599a0c44..8054baaeedd3fb9dc4b3d8287b9bec9a3a89e79c 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