Skip to content
Snippets Groups Projects
Commit 786eea2f authored by Allan Blanchard's avatar Allan Blanchard Committed by Virgile Prevosto
Browse files

Follows frama-c/frama-c!2936: update oracles

parent 19c8e9e2
No related branches found
No related tags found
No related merge requests found
......@@ -1216,7 +1216,7 @@ size_t strcspn(char const *s, char const *reject);
/*@ requires valid_string_s: valid_read_string(s);
requires valid_string_accept: valid_read_string(accept);
ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
assigns \result, \result;
assigns \result;
assigns \result \from *(s + (0 ..)), *(accept + (0 ..));
assigns \result
\from (indirect: *(s + (0 ..))), (indirect: *(accept + (0 ..)));
......
......@@ -945,7 +945,7 @@ size_t strcspn(char const *s, char const *reject);
/*@ requires valid_string_s: valid_read_string(s);
requires valid_string_accept: valid_read_string(accept);
ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
assigns \result, \result;
assigns \result;
assigns \result \from *(s + (0 ..)), *(accept + (0 ..));
assigns \result
\from (indirect: *(s + (0 ..))), (indirect: *(accept + (0 ..)));
......
......@@ -948,7 +948,7 @@ size_t strcspn(char const *s, char const *reject);
/*@ requires valid_string_s: valid_read_string(s);
requires valid_string_accept: valid_read_string(accept);
ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
assigns \result, \result;
assigns \result;
assigns \result \from *(s + (0 ..)), *(accept + (0 ..));
assigns \result
\from (indirect: *(s + (0 ..))), (indirect: *(accept + (0 ..)));
......
......@@ -945,7 +945,7 @@ size_t strcspn(char const *s, char const *reject);
/*@ requires valid_string_s: valid_read_string(s);
requires valid_string_accept: valid_read_string(accept);
ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
assigns \result, \result;
assigns \result;
assigns \result \from *(s + (0 ..)), *(accept + (0 ..));
assigns \result
\from (indirect: *(s + (0 ..))), (indirect: *(accept + (0 ..)));
......
......@@ -926,7 +926,7 @@ size_t strcspn(char const *s, char const *reject);
/*@ requires valid_string_s: valid_read_string(s);
requires valid_string_accept: valid_read_string(accept);
ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
assigns \result, \result;
assigns \result;
assigns \result \from *(s + (0 ..)), *(accept + (0 ..));
assigns \result
\from (indirect: *(s + (0 ..))), (indirect: *(accept + (0 ..)));
......
......@@ -927,7 +927,7 @@ size_t strcspn(char const *s, char const *reject);
/*@ requires valid_string_s: valid_read_string(s);
requires valid_string_accept: valid_read_string(accept);
ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
assigns \result, \result;
assigns \result;
assigns \result \from *(s + (0 ..)), *(accept + (0 ..));
assigns \result
\from (indirect: *(s + (0 ..))), (indirect: *(accept + (0 ..)));
......
......@@ -801,7 +801,7 @@ size_t strcspn(char const *s, char const *reject);
/*@ requires valid_string_s: valid_read_string(s);
requires valid_string_accept: valid_read_string(accept);
ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
assigns \result, \result;
assigns \result;
assigns \result \from *(s + (0 ..)), *(accept + (0 ..));
assigns \result
\from (indirect: *(s + (0 ..))), (indirect: *(accept + (0 ..)));
......
......@@ -636,7 +636,7 @@ size_t strcspn(char const *s, char const *reject);
/*@ requires valid_string_s: valid_read_string(s);
requires valid_string_accept: valid_read_string(accept);
ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s));
assigns \result, \result;
assigns \result;
assigns \result \from *(s + (0 ..)), *(accept + (0 ..));
assigns \result
\from (indirect: *(s + (0 ..))), (indirect: *(accept + (0 ..)));
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment