diff --git a/src/plugins/wp/tests/wp_gallery/oracle/string-compare.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/string-compare.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0c5741ea36b8b38350a2110b5dbc622c93d6c527
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle/string-compare.res.oracle
@@ -0,0 +1,67 @@
+# 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
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..48ad48fb860195d2301df4b58092b1e8086305dc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle
@@ -0,0 +1,89 @@
+# 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%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/string-compare.c b/src/plugins/wp/tests/wp_gallery/string-compare.c
new file mode 100644
index 0000000000000000000000000000000000000000..950ed7f72d78a0e34da6241c20251f29787cde37
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/string-compare.c
@@ -0,0 +1,75 @@
+/* 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);
+}