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

[Frama-c-discuss] How to prove "offset_min(char_xP_stdin_8_alloc_table, stdin) <= 0"?



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