Frama-C behaviors and value analysis

Question

I want to use Frama-C to analyze a program containing a read-like function: given a buffer buf and its length len, the function writes exactly len bytes in buf (unless there is an error).

I used ACSL to specify it, but the value analysis is giving me weird results.

Here's my specification, plus a main function for testing:

/*@
  assigns \result \from \nothing;
  assigns *(buf+(0..len-1)) \from \nothing;
  behavior ok:
    requires \valid(buf+(0..len-1));
    ensures  \result == 0;
    ensures  \initialized(buf+(0..len-1));
  behavior error:
    ensures  \result == -1;
 */
int read(char *buf, int len);

int main() {
  char buf[10];
  read(buf, 10);
  return 0;
}

When running frama-c -val test.c (I'm using Frama-C Neon), I obtain this result:

[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization

[value] computing for function read <- main.
        Called from test.c:16.
[value] using specification for function read
test.c:6:[value] Function read, behavior ok: precondition got status valid.
test.c:10:[value] Function read, behavior error: this postcondition evaluates to false in this
        context. If it is valid, either a precondition was not verified for this
        call, or some assigns/from clauses are incomplete (or incorrect).
[value] Done for function read
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
  NON TERMINATING FUNCTION

I did put assigns/from clauses, and there are no preconditions for the error behavior (so, by default, they are verified).

What is going on here? How can I make the analysis work in this case?

Answer 1

Despite the message, the actual issue is that there is an error in the specification of the read function: both behaviors are active at the same time, since they contain no assumes clauses (implicitly, both have assumes \true). Therefore, both ensures clauses are true, which implies \result == 0 && \result == 1.

This error leads to a contradictory state, where the result of the function is both 0 and 1 (simultaneously), thus no result can be returned, and therefore the function is considered as non-terminating.

One of the several possible solutions here consists in adding a non-deterministic ghost variable, say _read_state, to represent the internal state of the function, and then using this variable to define disjoint assumes clauses for the different behaviors:

//@ ghost volatile int _read_state;
/*@
  assigns \result \from \nothing;
  assigns *(buf+(0..len-1)) \from \nothing;
  behavior ok:
    assumes _read_state == 0;
    requires \valid(buf+(0..len-1));
    ensures  \result == 0;
    ensures  \initialized(buf+(0..len-1));
  behavior error:
    assumes _read_state != 0;
    ensures  \result == -1;
 */

Notice the == 0 and != 0 comparisons are arbitrary; any set of possibly disjoint values would work here.

Using this specification, we obtain the expected result for this program:

[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
  _read_state ∈ [--..--]
[value] computing for function read <- main.
        Called from test.c:18.
[value] using specification for function read
tread.c:7:[value] Function read, behavior ok: 
    precondition got status valid. 
    (Behavior may be inactive, no reduction performed.)
[value] Done for function read
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
  buf[0..9] ∈ [--..--] or UNINITIALIZED
  __retres ∈ {0}