--- layout: fc_discuss_archives title: Message 69 from Frama-C-discuss on March 2009 ---
Hello, On Tue, Mar 24, 2009 at 11:27, David MENTRE <dmentre at linux-france.org> wrote: > I am failing to prove "get_ensures_default_po_7" which is > "valid_string(s_0_0_0, result1, result0)". I am puzzled by this proof > obligation. Ok, found it! I rewrote the code as: ----- s = fgets(buf, MAX_STRING_SIZE, stdin); if (s != NULL) { int choice; choice = atoi(buf); // <-- here ----- instead of: ----- s = fgets(buf, MAX_STRING_SIZE, stdin); if (s != NULL) { int choice; choice = atoi(s); ----- That does the trick. Apparently, the string_valid property is not true for "s" while it is true for "buf". That might come from the specification of fgets: """ /*@ requires \valid_range(s,0,size-1) && \valid(stream); @ assigns s[0..size-1]; @ ensures \result == NULL @ || (\result == s && valid_string(s) && strlen(s) <= size-1); @*/ extern char *fgets(char *s, int size, FILE *stream); """ Apparently, we don't have: "\result == s && valid_string(s) ==> valid_string(\result)". I'm not claiming this should be true. :-) However, from the manual, the string returned by fgets() is equal to s (and thus is a valid_string): """ SYNOPSIS [...] char *fgets(char *s, int size, FILE *stream); [...] RETURN VALUE [...] gets() and fgets() return s on success, and NULL on error or when end of file occurs while no characters have been read. """ Yours, d.