diff --git a/sessions/match_string.av/whole_program/why3session.xml b/sessions/match_string.av/whole_program/why3session.xml index 13e45d9..4f30d7b 100644 --- a/sessions/match_string.av/whole_program/why3session.xml +++ b/sessions/match_string.av/whole_program/why3session.xml @@ -2,42 +2,51 @@ - - - - + + + - + - - - + + + - + - + - + - + - + - + - - + + + + + + + + + + + + - - + + @@ -366,17 +375,17 @@ - - - - - - - - - - - + + + + + + + + + + + @@ -878,6 +887,30 @@ + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/match_string.h b/src/match_string.h index d021c01..9783cbe 100644 --- a/src/match_string.h +++ b/src/match_string.h @@ -20,6 +20,8 @@ * be overflowed */ +#ifndef LEMMA_FUNCTIONS + /*@ axiomatic MatchString { logic size_t match_string(char **a, size_t n, char *s) = @@ -65,6 +67,98 @@ } */ +#else + +/*@ axiomatic Strchrnul { + logic size_t match_string(char **a, size_t n, char *s) = + n == 0 ? + 0 + : + (strcmp(a[0], s) == 0 ? 0 : match_string(a + 1, (size_t)(n - 1), s)); + + logic size_t real_len(char **a, size_t n) = + ((a[0] == NULL) || (n == 0)) ? + 0 + : + (size_t)(1 + real_len(a + 1, (size_t)(n - 1))); + } + */ + +/*@ ghost + @ /@ lemma + @ @ requires 0 <= i < real_len(a, len); + @ @ decreases i; + @ @ ensures a[i] != NULL; + @ @/ + @ void real_len_iteration_1(char **a, size_t i, size_t len) + @ { + @ if (a[i] != NULL && len > 0) + @ real_len_iteration_1(a + 1, i + 1, len - 1); + @ } + @*/ + +/*@ ghost + @ /@ lemma + @ @ requires i == real_len(a, len); + @ @ decreases i; + @ @ ensures a[i] == NULL || i == len; + @ @/ + @ void real_len_iteration_2(char **a, size_t i, size_t len) + @ { + @ if (a[i] != NULL && len > 0) + @ real_len_iteration_2(a + 1, i + 1, len - 1); + @ } + @*/ + +/*@ ghost + @ /@ lemma + @ @ requires (\forall size_t i; i < len ==> a[i] != NULL); + @ @ decreases len; + @ @ ensures real_len(a, len) == len; + @ @/ + @ void real_len_iteration_4(char** a, size_t len) + @ { + @ if (*a != NULL && len > 0) + @ real_len_iteration_4(a + 1, len - 1); + @ } + @*/ + +/*@ ghost + @ /@ lemma + @ @ requires 0 <= i < real_len(array, len) && + @ (\forall size_t j; 0 <= j < i ==> strcmp(array[j], string) != 0) && + @ strcmp(array[i], string) == 0; + @ @ decreases len; + @ @ ensures match_string(array, real_len(array, len), string) == i; + @ @/ + @ void real_len_iteration_5(char** array, char* string, size_t i, size_t len) + @ { + @ if (srrcmp(array[i], string) != 0 && len > 0) + @ real_len_iteration_5(array, string, i + 1, len - 1); + @ } + @*/ + +/*@ ghost + @ /@ lemma + @ @ requires valid_str(string1) && + @ valid_str(string2) && + @ strcmp(string1, string2) != 0; + @ @ decreases strlen(string1); + @ @ ensures (\exists size_t i; + @ 0 <= i <= \min(strlen(string1), strlen(string2)) && + @ string1[i] != string2[i]); + @ @/ + @ void real_len_iteration_6(char* string1, char* string2) + @ { + @ if (*string1 != *string2 && *string1 != '\0' && *string2 != '\0') + @ real_len_iteration_6(string1 + 1, string2 + 1); + @ } + @*/ + + + +#endif /* LEMMA_FUNCTIONS */ + /*@ requires n <= INT_MAX; requires (real_len(array, n) == n) ==> \valid(array+(0..n-1)); requires (real_len(array, n) < n) ==> \valid(array+(0..real_len(array, n)));