--- layout: fc_discuss_archives title: Message 54 from Frama-C-discuss on March 2009 ---
Hello, I have following C code: """ /*@ assigns \nothing; ensures \result >= 0 && \result < num_candidates; */ int f(void) { char buf[MAX_STRING_SIZE]; char *s; while (1) { s = fgets(buf, MAX_STRING_SIZE, stdin); [...] """ In the Default behavior part of this function, I need to prove the following "precondition to user call" and Alt-Ergo fails to prove it: offset_min(char_xP_stdin_8_alloc_table, stdin) <= 0 In the GUI, the "s" is highlighted in above code. I don't understand what I exactly need to prove. I have the same issue with another "precondition to user call" on exactly the same part of the code: offset_max(char_xP_stdin_8_alloc_table, stdin) >= 0