diff --git a/src/plugins/wp/tests/wp_gallery/frama_c_hashtbl_solved.c b/src/plugins/wp/tests/wp_gallery/frama_c_hashtbl_solved.c
deleted file mode 100644
index f52b6b9b19f46f34e7f32691ce5d112d23ce556e..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_gallery/frama_c_hashtbl_solved.c
+++ /dev/null
@@ -1,329 +0,0 @@
-/* run.config
- OPT: -wp-no-print -wp-rte
-*/
-
-/* run.config_qualif
- OPT: -wp-prover=script,alt-ergo -wp-prop=-left_unproved -then -wp-rte -wp -wp-prop=-left_unproved
-*/
-
-/* ******************************* */
-/* Solution de TP donné par Julien */
-/* ******************************* */
-
-/* -------------------------------------------------------------------------- */
-/*
- Ce fichier fournit une petite librairie de tables de hachage simplifiées:
- elles ne sont pas dynamiques et, en particulier, pas redimensionnables.
-
- Votre but est:
- 1. écrire la spécification ACSL des fonctions fournies à partir de leurs
- spécifications informelles (mais pas du code...)
- 2. prouver que chaque fonction satisfait la spécification écrite en 1.
- 3. prouver l'absence d'erreurs à l'exécution via l'option -wp-rte.
-*/
-/* -------------------------------------------------------------------------- */
-
-#include <limits.h>
-
-/* -------------------------------------------------------------------------- */
-/*
- Chaines de caractères simplifiées:
- toutes les chaînes de caractères de ce fichier seront supposées de longueurs
- STRING_LEN.
-
- La fonction [eq_string] est fournie avec sa spécification formelle déjÃ
- prouvée. Vous n'avez donc rien à faire pour cette fonction \o/.
-
- Astuce: le prédicat [EqString] peut éventuellement être utile...
-*/
-/* -------------------------------------------------------------------------- */
-
-#define STRING_LEN 20
-
-/*@ predicate EqString(char *s1, char *s2) =
- @ \forall integer i; 0 <= i < STRING_LEN ==> s1[i] == s2[i];
- @ */
-
-/*@ requires \valid_read(s1 + (0 .. STRING_LEN - 1));
- @ requires \valid_read(s2 + (0 .. STRING_LEN - 1));
- @ assigns \nothing;
- @
- @ behavior eq:
- @ assumes EqString(s1, s2);
- @ ensures \result == 1;
- @
- @ behavior not_eq:
- @ assumes ! EqString(s1, s2);
- @ ensures \result == 0;
- @
- @ complete behaviors;
- @ disjoint behaviors;
- @ */
-int eq_string(const char *s1, const char *s2) {
- int i;
- /*@ loop invariant 0 <= i <= STRING_LEN;
- @ loop invariant \forall integer j; 0 <= j < i ==> s1[j] == s2[j];
- @ loop assigns i;
- @ loop variant STRING_LEN - i;
- @*/
- for(i = 0; i < STRING_LEN; i++)
- if (s1[i] != s2[i]) return 0;
- return 1;
-}
-
-/* -------------------------------------------------------------------------- */
-/*
- Structures de données.
-
- Les tables de hachage associent ici des clés sous forme de chaînes de
- caractères à des valeurs entières. Une fonction de hachage sur les
- chaînes de caractères vous est fournie.
-
- Les tables de hachage sont représentées par leur nombre d'éléments et un
- tableau de "buckets" de longueur HASHTBL_LEN.
-
- Les "buckets" sont eux-même des tableaux de couples (clé, valeur)
- (individuellement appelé "bucket") dont toutes les clés ont le même
- haché. Chaque tableau est de longueur fixe, BUCKET_LEN, mais le nombre
- d'éléments stockés dans celui-ci peut varier.
-*/
-/* -------------------------------------------------------------------------- */
-
-#define BUCKET_LEN 10
-#define HASHTBL_LEN 17
-
-typedef struct {
- char *key; // clé, sous forme de chaînes de caractères (simplifiées)
- int value; // valeur associée à la clé
-} Bucket;
-
-typedef struct {
- Bucket buckets[BUCKET_LEN]; // tableau de couples (clé, valeur)
- int size; // nombre d'éléments stockés dans le tableau
-} Buckets;
-
-typedef struct {
- Buckets data[HASHTBL_LEN]; // tableau de buckets
- int size; // nombre d'éléments stockés dans la table de hachage
-} Hashtbl;
-
-/* -------------------------------------------------------------------------- */
-/*
- Fonction de hachage fournie: vous n'avez là non plus rien à faire \o/.
-
- La postcondition de la fonction [hash] ne peut pas être prouvée sans donner
- une définition à la fonction logique [Hash]. Ce travail n'est pas demandé ici
- et cette postcondition restera donc toujours non prouvée. Ce devrait être
- la seule...
-
- Astuce: la fonction logique [HashIndex] de l'axiomatique [Hash] n'est pas
- donnée que pour faire jolie. Vous avez aussi le droit d'ajouter vos propres
- définitions de prédicats et de fonctions...
-*/
-/* -------------------------------------------------------------------------- */
-
-/*@ axiomatic Hash {
- @ logic unsigned long Hash(char *s) reads(s + (0 .. ));
- @ // [Hash] est un modèle abstrait de la fonction de hash codée en C
- @ // ci-dessous
- @
- @ logic integer HashIndex(Hashtbl *tbl, char *k) = Hash(k) % HASHTBL_LEN;
- @ } */
-
-/*@ requires \valid_read(s + (0 .. STRING_LEN - 1));
- @ assigns \nothing;
- @ ensures left_unproved: \result == Hash(s);
- @ */
-unsigned long hash(const char *s) {
- unsigned long h = 5381;
- int i;
- /*@ loop invariant 0 <= i <= STRING_LEN;
- @ loop assigns h, i;
- @ loop variant STRING_LEN - i; */
- for(i = 0; i < STRING_LEN; i++) {
- if (s[i]) break;
- h = ((h << 5) + h) + s[i];
- }
- return h;
-}
-
-/* -------------------------------------------------------------------------- */
-/*
- Fonctions logiques et prédicats additionnels utiles.
-*/
-/* -------------------------------------------------------------------------- */
-
-/*@
- @ predicate valid_tbl(Hashtbl *tbl) =
- @ \valid(tbl->data+(0 .. HASHTBL_LEN - 1));
- @
- @ predicate valid_buckets(Hashtbl *tbl) =
- @ \forall integer i;
- @ 0 <= i < HASHTBL_LEN ==>
- @ \valid(tbl->data[i].buckets + (0 .. BUCKET_LEN - 1));
- @
- @ predicate valid_read_keys(Hashtbl *tbl) =
- @ \forall integer i, j;
- @ 0 <= i < HASHTBL_LEN ==>
- @ 0 <= j < tbl->data[i].size ==>
- @ \valid_read(tbl->data[i].buckets[j].key + (0 .. STRING_LEN - 1));
- @
- @ logic integer buckets_size(Hashtbl *tbl, char *k) =
- @ tbl->data[HashIndex(tbl, k)].size;
- @
- @ logic Bucket bucket(Hashtbl *tbl, char *k, integer i) =
- @ tbl->data[HashIndex(tbl, k)].buckets[i];
- @
- @ */
-
-/* -------------------------------------------------------------------------- */
-/*
- Exercice 0 (échauffement):
-
- La fonction [size] retourne le nombre d'éléments d'une table.
-*/
-/* -------------------------------------------------------------------------- */
-
-/*@ requires \valid(tbl);
- @ assigns \nothing;
- @ ensures \result == tbl->size;
- @ */
-int size(const Hashtbl *tbl) {
- return tbl->size;
-}
-
-/* -------------------------------------------------------------------------- */
-/*
- Exercice 1:
-
- La fonction [init] initialise une table de hachage contenant 0 élément.
- En particulier, chaque buckets contient 0 élément.
-*/
-/* -------------------------------------------------------------------------- */
-
-/*@ requires \valid(tbl);
- @ requires valid_tbl(tbl);
- @ assigns tbl->size, tbl->data[0 .. HASHTBL_LEN - 1];
- @ ensures tbl->size == 0;
- @ ensures \forall integer i; 0 <= i < HASHTBL_LEN ==> tbl->data[i].size == 0;
- @ */
-void init(Hashtbl *tbl){
- int i;
- tbl->size = 0;
- /*@ loop invariant 0 <= i <= HASHTBL_LEN;
- @ loop invariant \forall integer k; 0 <= k < i ==> tbl->data[k].size == 0;
- @ loop assigns i, tbl->data[0 .. HASHTBL_LEN - 1].size;
- @ loop variant HASHTBL_LEN - i;
- @ */
- for(i = 0; i < HASHTBL_LEN; i++)
- tbl->data[i].size = 0;
-}
-
-/* -------------------------------------------------------------------------- */
-/*
- Exercice 2:
-
- La fonction [add] ajouter un couple (clé, valeur) dans la table de hachage
- s'il y a suffisamment de places. Si tel est le cas, elle retourne 0.
-
- S'il n'y a pas suffisamment de places, la fonction ne fait rien et retourne
- -1.
-
- Conseil: lorsque la table est modifiée, bien penser à spécifier les nouvelles
- tailles et l'emplacement du couple ajouté.
-*/
-/* -------------------------------------------------------------------------- */
-
-/*@ requires \valid(tbl);
- @ requires valid_tbl(tbl);
- @ requires valid_buckets(tbl);
- @ requires \valid_read(k + (0 .. STRING_LEN - 1));
- @ requires 0 <= tbl->size < INT_MAX;
- @ requires \forall integer i;
- @ 0 <= i < HASHTBL_LEN ==>
- @ 0 <= tbl->data[i].size <= BUCKET_LEN;
- @
- @ assigns tbl->data[HashIndex(tbl, k)], tbl->size;
- @
- @ behavior nominal:
- @ assumes buckets_size(tbl, k) < BUCKET_LEN;
- @ assigns tbl->data[HashIndex(tbl, k)], tbl->size;
- @ ensures \result == 0;
- @ ensures tbl->size == \old(tbl->size) + 1;
- @ ensures buckets_size(tbl, k) == buckets_size{Old}(tbl, k) + 1;
- @ ensures bucket(tbl, k, buckets_size{Old}(tbl, k)).key == k;
- @ ensures bucket(tbl, k, buckets_size{Old}(tbl, k)).value == d;
- @ behavior full:
- @ assumes buckets_size(tbl, k) == BUCKET_LEN;
- @ assigns \nothing;
- @ ensures \result == -1;
- @
- @ complete behaviors;
- @ disjoint behaviors;
- @ */
-int add(Hashtbl *tbl, char *k, int d) {
- Bucket new_entry;
- unsigned int h = hash(k) % HASHTBL_LEN;
- if (tbl->data[h].size >= BUCKET_LEN)
- return -1;
- new_entry.key = k;
- new_entry.value = d;
- tbl->data[h].buckets[tbl->data[h].size] = new_entry;
- tbl->data[h].size++;
- tbl->size++;
- return 0;
-}
-
-/* -------------------------------------------------------------------------- */
-/*
- Exercice 3:
-
- La fonction [mem_binding] retourne 1 si le couple (clé, valeur) [k, v] donné
- en entrée est présent dans la table de hachage. Elle retourne 0 sinon.
-*/
-/* -------------------------------------------------------------------------- */
-
-/*@ requires \valid(tbl);
- @ requires valid_tbl(tbl);
- @ requires valid_buckets(tbl);
- @ requires valid_read_keys(tbl);
- @ requires \valid_read(k + (0 .. STRING_LEN - 1));
- @ requires \forall integer i;
- @ 0 <= i < HASHTBL_LEN ==>
- @ 0 <= tbl->data[i].size < BUCKET_LEN;
- @
- @ assigns \nothing;
- @
- @ behavior found:
- @ assumes \exists integer i; 0 <= i < buckets_size(tbl, k) &&
- @ EqString(k, bucket(tbl, k, i).key) && v == bucket(tbl, k, i).value;
- @ ensures \result == 1;
- @
- @ behavior not_found:
- @ assumes \forall integer i; 0 <= i < buckets_size(tbl, k) ==>
- @ (! EqString(k, bucket(tbl, k, i).key)
- @ || tbl->data[HashIndex(tbl, k)].buckets[i].value != v);
- @ // note: Alt-Ergo does not manage to prove it if written
- @ // bucket(tbl, k, i).value != v
- @ // so disappointing :-(
- @ ensures \result == 0;
- @
- @ complete behaviors;
- @ disjoint behaviors;
- @ */
-int mem_binding(const Hashtbl *tbl, const char *k, int v) {
- int i, h = hash(k) % HASHTBL_LEN;
- /*@ loop invariant 0 <= i <= tbl->data[h].size;
- @ loop invariant \forall integer j; 0 <= j < i ==>
- @ (! EqString(k, tbl->data[h].buckets[j].key)
- @ || tbl->data[h].buckets[j].value != v);
- @ loop assigns i;
- @ loop variant tbl->data[h].size - i;
- @ */
- for(i = 0; i < tbl->data[h].size; i++) {
- if (eq_string(k, tbl->data[h].buckets[i].key)
- && tbl->data[h].buckets[i].value == v)
- return 1;
- }
- return 0;
-}
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
deleted file mode 100644
index 2429963d412aaa3b426504d27c25d7c2fc60722a..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
+++ /dev/null
@@ -1,153 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing tests/wp_gallery/frama_c_hashtbl_solved.c (with preprocessing)
-[wp] Running WP plugin...
-[rte] annotating function add
-[rte] annotating function eq_string
-[rte] annotating function hash
-[rte] annotating function init
-[rte] annotating function mem_binding
-[rte] annotating function size
-[wp] Goal typed_eq_string_complete_eq_not_eq : trivial
-[wp] Goal typed_eq_string_disjoint_eq_not_eq : trivial
-[wp] Goal typed_eq_string_loop_invariant_preserved : not tried
-[wp] Goal typed_eq_string_loop_invariant_established : not tried
-[wp] Goal typed_eq_string_loop_invariant_2_preserved : not tried
-[wp] Goal typed_eq_string_loop_invariant_2_established : not tried
-[wp] Goal typed_eq_string_assert_rte_mem_access : not tried
-[wp] Goal typed_eq_string_assert_rte_mem_access_2 : not tried
-[wp] Goal typed_eq_string_assert_rte_signed_overflow : not tried
-[wp] Goal typed_eq_string_loop_assigns : trivial
-[wp] Goal typed_eq_string_assigns_part1 : not tried
-[wp] Goal typed_eq_string_assigns_part2 : not tried
-[wp] Goal typed_eq_string_assigns_part3 : not tried
-[wp] Goal typed_eq_string_assigns_part4 : not tried
-[wp] Goal typed_eq_string_loop_variant_decrease : not tried
-[wp] Goal typed_eq_string_loop_variant_positive : not tried
-[wp] Goal typed_eq_string_eq_ensures : not tried
-[wp] Goal typed_eq_string_not_eq_ensures : not tried
-[wp] Goal typed_hash_ensures_left_unproved : not tried
-[wp] Goal typed_hash_loop_invariant_preserved : not tried
-[wp] Goal typed_hash_loop_invariant_established : not tried
-[wp] Goal typed_hash_assert_rte_mem_access : not tried
-[wp] Goal typed_hash_assert_rte_mem_access_2 : not tried
-[wp] Goal typed_hash_assert_rte_signed_overflow : not tried
-[wp] Goal typed_hash_loop_assigns : trivial
-[wp] Goal typed_hash_assigns_part1 : not tried
-[wp] Goal typed_hash_assigns_part2 : not tried
-[wp] Goal typed_hash_loop_variant_decrease : not tried
-[wp] Goal typed_hash_loop_variant_positive : not tried
-[wp] Goal typed_size_ensures : not tried
-[wp] Goal typed_size_assert_rte_mem_access : not tried
-[wp] Goal typed_size_assigns : not tried
-[wp] Goal typed_init_ensures : not tried
-[wp] Goal typed_init_ensures_2 : not tried
-[wp] Goal typed_init_assert_rte_mem_access : not tried
-[wp] Goal typed_init_loop_invariant_preserved : not tried
-[wp] Goal typed_init_loop_invariant_established : not tried
-[wp] Goal typed_init_loop_invariant_2_preserved : not tried
-[wp] Goal typed_init_loop_invariant_2_established : not tried
-[wp] Goal typed_init_assert_rte_index_bound : not tried
-[wp] Goal typed_init_assert_rte_index_bound_2 : not tried
-[wp] Goal typed_init_assert_rte_mem_access_2 : not tried
-[wp] Goal typed_init_assert_rte_signed_overflow : not tried
-[wp] Goal typed_init_loop_assigns_part1 : trivial
-[wp] Goal typed_init_loop_assigns_part2 : not tried
-[wp] Goal typed_init_assigns_part1 : not tried
-[wp] Goal typed_init_assigns_part2 : not tried
-[wp] Goal typed_init_assigns_part3 : not tried
-[wp] Goal typed_init_loop_variant_decrease : not tried
-[wp] Goal typed_init_loop_variant_positive : not tried
-[wp] Goal typed_add_complete_full_nominal : not tried
-[wp] Goal typed_add_disjoint_full_nominal : not tried
-[wp] Goal typed_add_assert_rte_index_bound : not tried
-[wp] Goal typed_add_assert_rte_mem_access : not tried
-[wp] Goal typed_add_assert_rte_index_bound_2 : not tried
-[wp] Goal typed_add_assert_rte_index_bound_3 : not tried
-[wp] Goal typed_add_assert_rte_index_bound_4 : not tried
-[wp] Goal typed_add_assert_rte_index_bound_5 : not tried
-[wp] Goal typed_add_assert_rte_mem_access_2 : not tried
-[wp] Goal typed_add_assert_rte_mem_access_3 : not tried
-[wp] Goal typed_add_assert_rte_index_bound_6 : not tried
-[wp] Goal typed_add_assert_rte_mem_access_4 : not tried
-[wp] Goal typed_add_assert_rte_mem_access_5 : not tried
-[wp] Goal typed_add_assert_rte_signed_overflow : not tried
-[wp] Goal typed_add_assert_rte_mem_access_6 : not tried
-[wp] Goal typed_add_assert_rte_mem_access_7 : not tried
-[wp] Goal typed_add_assert_rte_signed_overflow_2 : not tried
-[wp] Goal typed_add_assigns_exit : trivial
-[wp] Goal typed_add_assigns_normal_part1 : trivial
-[wp] Goal typed_add_assigns_normal_part2 : not tried
-[wp] Goal typed_add_assigns_normal_part3 : not tried
-[wp] Goal typed_add_assigns_normal_part4 : not tried
-[wp] Goal typed_add_assigns_normal_part5 : not tried
-[wp] Goal typed_add_assigns_normal_part6 : not tried
-[wp] Goal typed_add_assigns_normal_part7 : not tried
-[wp] Goal typed_add_assigns_normal_part8 : not tried
-[wp] Goal typed_add_assigns_normal_part9 : not tried
-[wp] Goal typed_add_call_hash_requires : not tried
-[wp] Goal typed_add_nominal_ensures : not tried
-[wp] Goal typed_add_nominal_ensures_2 : not tried
-[wp] Goal typed_add_nominal_ensures_3 : not tried
-[wp] Goal typed_add_nominal_ensures_4 : not tried
-[wp] Goal typed_add_nominal_ensures_5 : not tried
-[wp] Goal typed_add_nominal_assigns_exit : trivial
-[wp] Goal typed_add_nominal_assigns_normal_part1 : trivial
-[wp] Goal typed_add_nominal_assigns_normal_part2 : not tried
-[wp] Goal typed_add_nominal_assigns_normal_part3 : not tried
-[wp] Goal typed_add_nominal_assigns_normal_part4 : not tried
-[wp] Goal typed_add_nominal_assigns_normal_part5 : not tried
-[wp] Goal typed_add_nominal_assigns_normal_part6 : not tried
-[wp] Goal typed_add_nominal_assigns_normal_part7 : not tried
-[wp] Goal typed_add_nominal_assigns_normal_part8 : not tried
-[wp] Goal typed_add_nominal_assigns_normal_part9 : not tried
-[wp] Goal typed_add_full_ensures : not tried
-[wp] Goal typed_add_full_assigns_exit : trivial
-[wp] Goal typed_add_full_assigns_normal_part1 : trivial
-[wp] Goal typed_add_full_assigns_normal_part2 : not tried
-[wp] Goal typed_add_full_assigns_normal_part3 : not tried
-[wp] Goal typed_add_full_assigns_normal_part4 : not tried
-[wp] Goal typed_add_full_assigns_normal_part5 : not tried
-[wp] Goal typed_add_full_assigns_normal_part6 : not tried
-[wp] Goal typed_add_full_assigns_normal_part7 : not tried
-[wp] Goal typed_add_full_assigns_normal_part8 : not tried
-[wp] Goal typed_add_full_assigns_normal_part9 : not tried
-[wp] Goal typed_mem_binding_complete_found_not_found : not tried
-[wp] Goal typed_mem_binding_disjoint_found_not_found : not tried
-[wp] Goal typed_mem_binding_loop_invariant_preserved : not tried
-[wp] Goal typed_mem_binding_loop_invariant_established : not tried
-[wp] Goal typed_mem_binding_loop_invariant_2_preserved : not tried
-[wp] Goal typed_mem_binding_loop_invariant_2_established : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_2 : not tried
-[wp] Goal typed_mem_binding_assert_rte_mem_access : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_3 : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_4 : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_5 : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_6 : not tried
-[wp] Goal typed_mem_binding_assert_rte_mem_access_2 : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_7 : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_8 : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_9 : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_10 : not tried
-[wp] Goal typed_mem_binding_assert_rte_mem_access_3 : not tried
-[wp] Goal typed_mem_binding_assert_rte_signed_overflow : not tried
-[wp] Goal typed_mem_binding_loop_assigns_part1 : trivial
-[wp] Goal typed_mem_binding_loop_assigns_part2 : not tried
-[wp] Goal typed_mem_binding_assigns_exit_part1 : trivial
-[wp] Goal typed_mem_binding_assigns_exit_part2 : not tried
-[wp] Goal typed_mem_binding_assigns_exit_part3 : not tried
-[wp] Goal typed_mem_binding_assigns_exit_part4 : not tried
-[wp] Goal typed_mem_binding_assigns_normal_part1 : trivial
-[wp] Goal typed_mem_binding_assigns_normal_part2 : not tried
-[wp] Goal typed_mem_binding_assigns_normal_part3 : not tried
-[wp] Goal typed_mem_binding_assigns_normal_part4 : not tried
-[wp] Goal typed_mem_binding_assigns_normal_part5 : not tried
-[wp] Goal typed_mem_binding_assigns_normal_part6 : not tried
-[wp] Goal typed_mem_binding_assigns_normal_part7 : not tried
-[wp] Goal typed_mem_binding_loop_variant_decrease : not tried
-[wp] Goal typed_mem_binding_loop_variant_positive : not tried
-[wp] Goal typed_mem_binding_call_hash_requires : not tried
-[wp] Goal typed_mem_binding_call_eq_string_requires : not tried
-[wp] Goal typed_mem_binding_call_eq_string_requires_2 : not tried
-[wp] Goal typed_mem_binding_found_ensures : not tried
-[wp] Goal typed_mem_binding_not_found_ensures : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
deleted file mode 100644
index b9066d9921a764ee6e240b742d1f8f5c6387d265..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
+++ /dev/null
@@ -1,181 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/wp_gallery/frama_c_hashtbl_solved.c (with preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] 102 goals scheduled
-[wp] [Qed] Goal typed_eq_string_complete_eq_not_eq : Valid
-[wp] [Qed] Goal typed_eq_string_disjoint_eq_not_eq : Valid
-[wp] [Alt-Ergo] Goal typed_eq_string_loop_invariant_preserved : Valid
-[wp] [Qed] Goal typed_eq_string_loop_invariant_established : Valid
-[wp] [Alt-Ergo] Goal typed_eq_string_loop_invariant_2_preserved : Valid
-[wp] [Qed] Goal typed_eq_string_loop_invariant_2_established : Valid
-[wp] [Qed] Goal typed_eq_string_loop_assigns : Valid
-[wp] [Qed] Goal typed_eq_string_assigns_part1 : Valid
-[wp] [Qed] Goal typed_eq_string_assigns_part2 : Valid
-[wp] [Qed] Goal typed_eq_string_assigns_part3 : Valid
-[wp] [Qed] Goal typed_eq_string_assigns_part4 : Valid
-[wp] [Qed] Goal typed_eq_string_loop_variant_decrease : Valid
-[wp] [Qed] Goal typed_eq_string_loop_variant_positive : Valid
-[wp] [Alt-Ergo] Goal typed_eq_string_eq_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_eq_string_not_eq_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_hash_loop_invariant_preserved : Valid
-[wp] [Qed] Goal typed_hash_loop_invariant_established : Valid
-[wp] [Qed] Goal typed_hash_loop_assigns : Valid
-[wp] [Qed] Goal typed_hash_assigns_part1 : Valid
-[wp] [Qed] Goal typed_hash_assigns_part2 : Valid
-[wp] [Qed] Goal typed_hash_loop_variant_decrease : Valid
-[wp] [Qed] Goal typed_hash_loop_variant_positive : Valid
-[wp] [Qed] Goal typed_size_ensures : Valid
-[wp] [Qed] Goal typed_size_assigns : Valid
-[wp] [Alt-Ergo] Goal typed_init_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_init_ensures_2 : Valid
-[wp] [Alt-Ergo] Goal typed_init_loop_invariant_preserved : Valid
-[wp] [Qed] Goal typed_init_loop_invariant_established : Valid
-[wp] [Alt-Ergo] Goal typed_init_loop_invariant_2_preserved : Valid
-[wp] [Qed] Goal typed_init_loop_invariant_2_established : Valid
-[wp] [Qed] Goal typed_init_loop_assigns_part1 : Valid
-[wp] [Qed] Goal typed_init_loop_assigns_part2 : Valid
-[wp] [Qed] Goal typed_init_assigns_part1 : Valid
-[wp] [Qed] Goal typed_init_assigns_part2 : Valid
-[wp] [Script] Goal typed_init_assigns_part3 : Valid
-[wp] [Qed] Goal typed_init_loop_variant_decrease : Valid
-[wp] [Qed] Goal typed_init_loop_variant_positive : Valid
-[wp] [Alt-Ergo] Goal typed_add_complete_full_nominal : Valid
-[wp] [Alt-Ergo] Goal typed_add_disjoint_full_nominal : Valid
-[wp] [Qed] Goal typed_add_assigns_exit : Valid
-[wp] [Qed] Goal typed_add_assigns_normal_part1 : Valid
-[wp] [Qed] Goal typed_add_assigns_normal_part2 : Valid
-[wp] [Qed] Goal typed_add_assigns_normal_part3 : Valid
-[wp] [Qed] Goal typed_add_assigns_normal_part4 : Valid
-[wp] [Qed] Goal typed_add_assigns_normal_part5 : Valid
-[wp] [Alt-Ergo] Goal typed_add_assigns_normal_part6 : Valid
-[wp] [Alt-Ergo] Goal typed_add_assigns_normal_part7 : Valid
-[wp] [Qed] Goal typed_add_assigns_normal_part8 : Valid
-[wp] [Qed] Goal typed_add_assigns_normal_part9 : Valid
-[wp] [Qed] Goal typed_add_call_hash_requires : Valid
-[wp] [Alt-Ergo] Goal typed_add_nominal_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_add_nominal_ensures_2 : Valid
-[wp] [Alt-Ergo] Goal typed_add_nominal_ensures_3 : Valid
-[wp] [Alt-Ergo] Goal typed_add_nominal_ensures_4 : Valid
-[wp] [Alt-Ergo] Goal typed_add_nominal_ensures_5 : Valid
-[wp] [Qed] Goal typed_add_nominal_assigns_exit : Valid
-[wp] [Qed] Goal typed_add_nominal_assigns_normal_part1 : Valid
-[wp] [Qed] Goal typed_add_nominal_assigns_normal_part2 : Valid
-[wp] [Qed] Goal typed_add_nominal_assigns_normal_part3 : Valid
-[wp] [Qed] Goal typed_add_nominal_assigns_normal_part4 : Valid
-[wp] [Qed] Goal typed_add_nominal_assigns_normal_part5 : Valid
-[wp] [Alt-Ergo] Goal typed_add_nominal_assigns_normal_part6 : Valid
-[wp] [Alt-Ergo] Goal typed_add_nominal_assigns_normal_part7 : Valid
-[wp] [Qed] Goal typed_add_nominal_assigns_normal_part8 : Valid
-[wp] [Qed] Goal typed_add_nominal_assigns_normal_part9 : Valid
-[wp] [Alt-Ergo] Goal typed_add_full_ensures : Valid
-[wp] [Qed] Goal typed_add_full_assigns_exit : Valid
-[wp] [Qed] Goal typed_add_full_assigns_normal_part1 : Valid
-[wp] [Qed] Goal typed_add_full_assigns_normal_part2 : Valid
-[wp] [Qed] Goal typed_add_full_assigns_normal_part3 : Valid
-[wp] [Qed] Goal typed_add_full_assigns_normal_part4 : Valid
-[wp] [Qed] Goal typed_add_full_assigns_normal_part5 : Valid
-[wp] [Alt-Ergo] Goal typed_add_full_assigns_normal_part6 : Valid
-[wp] [Alt-Ergo] Goal typed_add_full_assigns_normal_part7 : Valid
-[wp] [Alt-Ergo] Goal typed_add_full_assigns_normal_part8 : Valid
-[wp] [Qed] Goal typed_add_full_assigns_normal_part9 : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_complete_found_not_found : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_disjoint_found_not_found : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_loop_invariant_preserved : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_loop_invariant_established : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_loop_invariant_2_preserved : Valid
-[wp] [Qed] Goal typed_mem_binding_loop_invariant_2_established : Valid
-[wp] [Qed] Goal typed_mem_binding_loop_assigns_part1 : Valid
-[wp] [Qed] Goal typed_mem_binding_loop_assigns_part2 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_exit_part1 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_exit_part2 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_exit_part3 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_exit_part4 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_normal_part1 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_normal_part2 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_normal_part3 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_normal_part4 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_normal_part5 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_normal_part6 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_normal_part7 : Valid
-[wp] [Qed] Goal typed_mem_binding_loop_variant_decrease : Valid
-[wp] [Qed] Goal typed_mem_binding_loop_variant_positive : Valid
-[wp] [Qed] Goal typed_mem_binding_call_hash_requires : Valid
-[wp] [Qed] Goal typed_mem_binding_call_eq_string_requires : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_call_eq_string_requires_2 : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_found_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_not_found_ensures : Valid
-[wp] Proved goals: 102 / 102
- Qed: 69
- Script: 1
- Alt-Ergo: 32
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- eq_string 11 4 15 100%
- hash 6 1 7 100%
- size 2 - 2 100%
- init 8 4 13 100%
- add 24 15 39 100%
- mem_binding 18 8 26 100%
-------------------------------------------------------------
-[wp] Running WP plugin...
-[rte] annotating function add
-[rte] annotating function eq_string
-[rte] annotating function hash
-[rte] annotating function init
-[rte] annotating function mem_binding
-[rte] annotating function size
-[wp] 41 goals scheduled
-[wp] [Alt-Ergo] Goal typed_eq_string_assert_rte_mem_access : Valid
-[wp] [Alt-Ergo] Goal typed_eq_string_assert_rte_mem_access_2 : Valid
-[wp] [Alt-Ergo] Goal typed_eq_string_assert_rte_signed_overflow : Valid
-[wp] [Alt-Ergo] Goal typed_hash_assert_rte_mem_access : Valid
-[wp] [Qed] Goal typed_hash_assert_rte_mem_access_2 : Valid
-[wp] [Alt-Ergo] Goal typed_hash_assert_rte_signed_overflow : Valid
-[wp] [Alt-Ergo] Goal typed_size_assert_rte_mem_access : Valid
-[wp] [Alt-Ergo] Goal typed_init_assert_rte_mem_access : Valid
-[wp] [Qed] Goal typed_init_assert_rte_index_bound : Valid
-[wp] [Qed] Goal typed_init_assert_rte_index_bound_2 : Valid
-[wp] [Alt-Ergo] Goal typed_init_assert_rte_mem_access_2 : Valid
-[wp] [Alt-Ergo] Goal typed_init_assert_rte_signed_overflow : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_index_bound : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_mem_access : Valid
-[wp] [Qed] Goal typed_add_assert_rte_index_bound_2 : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_index_bound_3 : Valid
-[wp] [Qed] Goal typed_add_assert_rte_index_bound_4 : Valid
-[wp] [Qed] Goal typed_add_assert_rte_index_bound_5 : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_mem_access_2 : Valid
-[wp] [Qed] Goal typed_add_assert_rte_mem_access_3 : Valid
-[wp] [Qed] Goal typed_add_assert_rte_index_bound_6 : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_mem_access_4 : Valid
-[wp] [Qed] Goal typed_add_assert_rte_mem_access_5 : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_signed_overflow : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_mem_access_6 : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_mem_access_7 : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_signed_overflow_2 : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_index_bound : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_index_bound_2 : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_mem_access : Valid
-[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_3 : Valid
-[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_4 : Valid
-[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_5 : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_index_bound_6 : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_mem_access_2 : Valid
-[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_7 : Valid
-[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_8 : Valid
-[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_9 : Valid
-[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_10 : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_mem_access_3 : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_signed_overflow : Valid
-[wp] Proved goals: 41 / 41
- Qed: 16
- Alt-Ergo: 25
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- eq_string 11 7 18 100%
- hash 7 3 10 100%
- size 2 1 3 100%
- init 10 7 18 100%
- add 30 24 54 100%
- mem_binding 25 15 40 100%
-------------------------------------------------------------