[klee-dev] [BUG?] Write failures only triggered once per state

[Jonathan Neuschäfer]

Dear KLEE developers,

reading the source code I noticed the following:

runtime/POSIX/fd.c:314:
  if (__exe_fs.max_failures && *__exe_fs.write_fail == n_calls) {
    __exe_fs.max_failures--;
    errno = EIO;
    return -1;
  }
Write failures can only be triggered once per state: When the "if"
header is reached by a state where __exe_fs.write_fail is still
symbolic, the state is forked. In one of the child states it will be
known to be different from the current value of n_calls, but still be
symbolic. In the other state it will be concretized to the current value
of n_calls, __exe_fs.max_failures will be decremented and the write call
will fail. But the next time this state reaches line 314
__exe_fs.write_fail will provably be smaller than n_calls, even if
__exe_fs.max_failures indicates that another failure should happen.

I think __exe_fs.write_fail should be assigned a new symbolic value
greater than n_calls in the if block.

Feedback is appreciated.

Thanks,
Jonathan Neuschäfer