--- layout: fc_discuss_archives title: Message 68 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,

I have following (simplified) code:
===
#define _GNU_SOURCE

#include <stdio.h>
#include <stdlib.h>

#define MAX_STRING_SIZE 255
#define MAX_VAL 10

int num;

/*@ requires \valid(stdin);
    assigns \nothing;
    ensures \result >= 0 && \result < num;
 */
int get(void)
{
  char buf[MAX_STRING_SIZE];
  char *s = NULL;

  while (1) {
    s = fgets(buf, MAX_STRING_SIZE, stdin);

    if (s != NULL) {
      int choice;

      choice = atoi(s);
      if (choice >= 0 && choice < num) {
        s = fgets(buf, MAX_STRING_SIZE, stdin);
        if (s != NULL && strncmp(s, "y", 1) == 0) {
          return choice;
        } else {
        }
      } else {
      }
    } else {
    }
  }
}

/*@ requires \valid(stdin);
 */
int main(void)
{
  int a;

  num = MAX_VAL - 1;
  a = get();

  return a;
}
====

I'm launching Jessie with:
  "frama-c -jessie-analysis -jessie-std-stubs -jessie-atp alt-ergo
-jessie-cpu-limit 2 -jessie-gui fgets-issue.c"

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.

Could somebody explain to me what is exactly needed? What are the
three arguments to valid_string?

I looked into Jessie prolog but found only "#define FRAMA_C_STRING
__declspec(valid_string)" which is not very verbose. :-)

Many thanks in advance for any help,
Sincerely yours,
david