--- layout: fc_discuss_archives title: Message 69 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Issue to prove a precondition for user call



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.