--- layout: fc_discuss_archives title: Message 68 from Frama-C-discuss on March 2009 ---
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