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

[wp] Removes an example from gallery

parent 60782321
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/tests/wp_gallery/frama_c_hashtbl_solved.c deleted 100644 → 0
+ 0
− 329
View file @ 60782321
/* 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;
}
src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle deleted 100644 → 0
+ 0
− 153
View file @ 60782321
# 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
src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle deleted 100644 → 0
+ 0
− 181
View file @ 60782321
# 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%
------------------------------------------------------------
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment