Frama-C Behavior and Value Analysis

Question

I want to use Frama-C to analyze a program containing an a- readlike function: taking into account the buffer bufand its length, the lenfunction writes exactly lenbytes to buf(if there is no error).

I used ACSL to indicate it, but analyzing the values ​​gives me strange results.

Here is my specification, plus a function mainfor 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;
}

On startup frama-c -val test.c(I use Frama-C Neon), I get 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 put the sentences assigns/ from, and there are no prerequisites for the behavior error(so by default they are checked).

What's going on here? How can I do an analysis in this case?

Answer 1

, , read : , assumes (, assumes \true). ensures , \result == 0 && \result == 1.

, 0 1 (), , , , .

, _read_state, , disjoint assumes :

//@ 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;
 */

, == 0 != 0 ; .

, :

[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}