Skip to content
Snippets Groups Projects
Commit 57cfeff2 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[WP] add an example about string comparison into wp_gallery

parent 1e956a4d
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/oracle/string-compare.res.oracle 0 → 100644
+ 67
− 0
View file @ 57cfeff2
# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp_gallery/string-compare.c (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function main
[rte] annotating function stringCompare
[rte] annotating function stringLength
[wp] [CFG] Goal stringCompare_exits_never : Valid (Unreachable)
[wp] [CFG] Goal stringLength_exits_never : Valid (Unreachable)
[wp] Goal typed_stringCompare_complete_SomeDifferent_allEqual : trivial
[wp] Goal typed_stringCompare_disjoint_SomeDifferent_allEqual : trivial
[wp] Goal typed_stringCompare_loop_invariant_equal_preserved : not tried
[wp] Goal typed_stringCompare_loop_invariant_equal_established : not tried
[wp] Goal typed_stringCompare_loop_invariant_gauge_preserved : not tried
[wp] Goal typed_stringCompare_loop_invariant_gauge_established : not tried
[wp] Goal typed_stringCompare_loop_invariant_gauge_s1_preserved : not tried
[wp] Goal typed_stringCompare_loop_invariant_gauge_s1_established : not tried
[wp] Goal typed_stringCompare_loop_invariant_gauge_s2_preserved : not tried
[wp] Goal typed_stringCompare_loop_invariant_gauge_s2_established : not tried
[wp] Goal typed_stringCompare_loop_invariant_not_eos_preserved : not tried
[wp] Goal typed_stringCompare_loop_invariant_not_eos_established : not tried
[wp] Goal typed_stringCompare_loop_invariant_strlen_s1_preserved : not tried
[wp] Goal typed_stringCompare_loop_invariant_strlen_s1_established : not tried
[wp] Goal typed_stringCompare_loop_invariant_strlen_s2_preserved : not tried
[wp] Goal typed_stringCompare_loop_invariant_strlen_s2_established : not tried
[wp] Goal typed_stringCompare_assert_rte_mem_access : not tried
[wp] Goal typed_stringCompare_assert_rte_mem_access_2 : not tried
[wp] Goal typed_stringCompare_assert_rte_mem_access_3 : not tried
[wp] Goal typed_stringCompare_assert_different : not tried
[wp] Goal typed_stringCompare_assert_rte_mem_access_4 : not tried
[wp] Goal typed_stringCompare_assert_rte_mem_access_5 : not tried
[wp] Goal typed_stringCompare_assert_rte_signed_overflow : not tried
[wp] Goal typed_stringCompare_assert_rte_signed_overflow_2 : not tried
[wp] Goal typed_stringCompare_loop_assigns_part1 : trivial
[wp] Goal typed_stringCompare_loop_assigns_part2 : not tried
[wp] Goal typed_stringCompare_loop_assigns_part3 : not tried
[wp] Goal typed_stringCompare_assigns_part1 : not tried
[wp] Goal typed_stringCompare_assigns_part2 : not tried
[wp] Goal typed_stringCompare_assigns_part3 : not tried
[wp] Goal typed_stringCompare_assigns_part4 : not tried
[wp] Goal typed_stringCompare_assigns_part5 : not tried
[wp] Goal typed_stringCompare_assigns_part6 : not tried
[wp] Goal typed_stringCompare_assigns_part7 : not tried
[wp] Goal typed_stringCompare_assigns_part8 : not tried
[wp] Goal typed_stringCompare_assigns_part9 : not tried
[wp] Goal typed_stringCompare_allEqual_ensures : not tried
[wp] Goal typed_stringCompare_SomeDifferent_ensures : not tried
[wp] Goal typed_stringLength_ensures_rightResult : not tried
[wp] Goal typed_stringLength_ensures_rightEndCharacter : not tried
[wp] Goal typed_stringLength_loop_invariant_preserved : not tried
[wp] Goal typed_stringLength_loop_invariant_established : not tried
[wp] Goal typed_stringLength_loop_invariant_2_preserved : not tried
[wp] Goal typed_stringLength_loop_invariant_2_established : not tried
[wp] Goal typed_stringLength_assert_rte_mem_access : not tried
[wp] Goal typed_stringLength_loop_assigns_part1 : trivial
[wp] Goal typed_stringLength_loop_assigns_part2 : not tried
[wp] Goal typed_stringLength_assigns_part1 : not tried
[wp] Goal typed_stringLength_assigns_part2 : not tried
[wp] Goal typed_stringLength_assigns_part3 : not tried
[wp] Goal typed_stringLength_assigns_part4 : not tried
[wp] Goal typed_stringLength_assigns_part5 : not tried
[wp] Goal typed_main_ensures : not tried
[wp] Goal typed_main_exits_never : trivial
[wp] Goal typed_main_assert : not tried
[wp] Goal typed_main_assigns_exit : trivial
[wp] Goal typed_main_assigns_normal_part1 : trivial
[wp] Goal typed_main_assigns_normal_part2 : not tried
[wp] Goal typed_main_call_stringCompare_requires_validStrings : not tried
src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle 0 → 100644
+ 89
− 0
View file @ 57cfeff2
# frama-c -wp [...]
[kernel] Parsing tests/wp_gallery/string-compare.c (with preprocessing)
[wp] Running WP plugin...
[wp] [CFG] Goal stringCompare_exits_never : Valid (Unreachable)
[wp] [CFG] Goal stringLength_exits_never : Valid (Unreachable)
[wp] Warning: Missing RTE guards
[wp] 51 goals scheduled
[wp] [Qed] Goal typed_stringCompare_complete_SomeDifferent_allEqual : Valid
[wp] [Qed] Goal typed_stringCompare_disjoint_SomeDifferent_allEqual : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_loop_invariant_equal_preserved : Valid
[wp] [Qed] Goal typed_stringCompare_loop_invariant_equal_established : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_loop_invariant_gauge_preserved : Valid
[wp] [Qed] Goal typed_stringCompare_loop_invariant_gauge_established : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_loop_invariant_gauge_s1_preserved : Valid
[wp] [Qed] Goal typed_stringCompare_loop_invariant_gauge_s1_established : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_loop_invariant_gauge_s2_preserved : Valid
[wp] [Qed] Goal typed_stringCompare_loop_invariant_gauge_s2_established : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_loop_invariant_not_eos_preserved : Valid
[wp] [Qed] Goal typed_stringCompare_loop_invariant_not_eos_established : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_loop_invariant_strlen_s1_preserved : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_loop_invariant_strlen_s1_established : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_loop_invariant_strlen_s2_preserved : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_loop_invariant_strlen_s2_established : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_assert_different : Valid
[wp] [Qed] Goal typed_stringCompare_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_stringCompare_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_stringCompare_loop_assigns_part3 : Valid
[wp] [Qed] Goal typed_stringCompare_assigns_part1 : Valid
[wp] [Qed] Goal typed_stringCompare_assigns_part2 : Valid
[wp] [Qed] Goal typed_stringCompare_assigns_part3 : Valid
[wp] [Qed] Goal typed_stringCompare_assigns_part4 : Valid
[wp] [Qed] Goal typed_stringCompare_assigns_part5 : Valid
[wp] [Qed] Goal typed_stringCompare_assigns_part6 : Valid
[wp] [Qed] Goal typed_stringCompare_assigns_part7 : Valid
[wp] [Qed] Goal typed_stringCompare_assigns_part8 : Valid
[wp] [Qed] Goal typed_stringCompare_assigns_part9 : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_allEqual_ensures : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_SomeDifferent_ensures : Valid
[wp] [Alt-Ergo] Goal typed_stringLength_ensures_rightResult : Valid
[wp] [Alt-Ergo] Goal typed_stringLength_ensures_rightEndCharacter : Valid
[wp] [Alt-Ergo] Goal typed_stringLength_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_stringLength_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_stringLength_loop_invariant_2_preserved : Valid
[wp] [Qed] Goal typed_stringLength_loop_invariant_2_established : Valid
[wp] [Qed] Goal typed_stringLength_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_stringLength_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_stringLength_assigns_part1 : Valid
[wp] [Qed] Goal typed_stringLength_assigns_part2 : Valid
[wp] [Qed] Goal typed_stringLength_assigns_part3 : Valid
[wp] [Qed] Goal typed_stringLength_assigns_part4 : Valid
[wp] [Qed] Goal typed_stringLength_assigns_part5 : Valid
[wp] [Alt-Ergo] Goal typed_main_ensures : Valid
[wp] [Qed] Goal typed_main_exits_never : Valid
[wp] [Qed] Goal typed_main_assert : Valid
[wp] [Qed] Goal typed_main_assigns_exit : Valid
[wp] [Qed] Goal typed_main_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_main_assigns_normal_part2 : Valid
[wp] [Alt-Ergo] Goal typed_main_call_stringCompare_requires_validStrings : Valid
[wp] Proved goals: 51 / 51
Qed: 33
Alt-Ergo: 18
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
stringCompare 19 12 31 100%
stringLength 9 4 13 100%
main 5 2 7 100%
------------------------------------------------------------
[wp] Running WP plugin...
[rte] annotating function main
[rte] annotating function stringCompare
[rte] annotating function stringLength
[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_stringCompare_assert_rte_mem_access : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_assert_rte_mem_access_2 : Valid
[wp] [Qed] Goal typed_stringCompare_assert_rte_mem_access_3 : Valid
[wp] [Qed] Goal typed_stringCompare_assert_rte_mem_access_4 : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_assert_rte_mem_access_5 : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_assert_rte_signed_overflow : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_assert_rte_signed_overflow_2 : Valid
[wp] [Alt-Ergo] Goal typed_stringLength_assert_rte_mem_access : Valid
[wp] Proved goals: 8 / 8
Qed: 2
Alt-Ergo: 6
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
stringCompare 21 17 38 100%
stringLength 9 5 14 100%
main 5 2 7 100%
------------------------------------------------------------
src/plugins/wp/tests/wp_gallery/string-compare.c 0 → 100644
+ 75
− 0
View file @ 57cfeff2
/* run.config
OPT: -wp-no-print -wp-rte
*/
/* run.config_qualif
OPT: -then -wp-rte -wp
*/
#include <stdint.h>
#include <string.h>
#include <stdio.h>
/*@ requires validStrings: valid_read_string(s1) && valid_read_string(s2);
assigns \nothing ;
allocates \nothing ;
frees \nothing ;
exits never: \false ;
behavior allEqual:
assumes \forall integer k; 0 <= k <= strlen(s1) ==> s1[k] == s2[k];
ensures \result == 0;
behavior SomeDifferent:
assumes \exists integer k; 0 <= k <= strlen(s1) && s1[k] != s2[k];
ensures \result != 0;
disjoint behaviors;
complete behaviors; */
int stringCompare(const char* s1, const char* s2) {
if (s1 == s2)
return 0;
/*@ loop invariant strlen_s1: 0 <= strlen(s1) <= \at(strlen(s1), Pre);
loop invariant strlen_s2: 0 <= strlen(s2) <= \at(strlen(s2), Pre);
loop invariant gauge_s1: s1 + strlen(s1) == \at(s1 + strlen(s1), Pre);
loop invariant gauge_s2: s2 + strlen(s2) == \at(s2 + strlen(s2), Pre);
loop invariant gauge: \at(strlen(s1), Pre) - strlen(s1) == \at(strlen(s2), Pre) - strlen(s2);
loop invariant equal: \forall integer j; 0<= j < \at(strlen(s1), Pre) - strlen(s1) ==> \at(s1,Pre)[j] == \at(s2,Pre)[j];
loop invariant not_eos: \forall integer j; 0<= j < \at(strlen(s1), Pre) - strlen(s1) ==> \at(s1,Pre)[j] != 0;
loop assigns s1, s2; */
while (*s1 == *(s2++))
{
if (*(s1++) == '\0')
return 0;
}
//@ assert different: \let k = \at(strlen(s1), Pre) - strlen(s1) ; \at(s1,Pre)[k] != \at(s2,Pre)[k];
return *(s1) - *(--s2);
}
/*@ requires validString: valid_string(str);
requires validLength: 0 <= strlen(str) < SIZE_MAX;
assigns \nothing ;
exits never: \false ;
ensures rightResult: \result == strlen(\old(str));
ensures rightEndCharacter: str[\result] == '\0' ; */
size_t stringLength(const char* str) {
const char* s = str ;
/*@ loop assigns s ;
loop invariant s + strlen(s) == \at(str + strlen(str),Pre);
loop invariant 0 <= strlen(s) <= \at(strlen(str),Pre); */
while (*s++ != '\0');
return --s - str;
}
/*@ assigns \nothing ;
exits never: \false ;
ensures \result != 0 ;*/
int main(void) {
const char hello[] = { 'h', 'e', 'l', 'l', 'o', '\0'};
const char helli[] = { 'h', 'e', 'l', 'l', 'i', '\0'};
/*@ assert \valid_read(&hello[0]) && \valid_read(&helli[0]) ; */
return stringCompare(hello, helli);
}
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