CODEWITHSUNDEEP
frama-c
Thuy Nguyen
Thuy Nguyen

Reputation: 353

Why Eva plugin of Frama-c return unkown when it acctually found a counter example of an assertion

I am trying to insert an assertion inside a function. Here is what I did:

void foo(int a) {
    //@ assert a == 1;
}

void main() {
   foo(1);
   foo(2);
}

I expect to get an invalid result, but Frama-C returns an unknown result while it can provide a counterexample with the call stack.

Here is the screenshot when I run my example with Frama-C:

Screenshot of the Frama-C GUI with the values per callstack computed by Eva

Upvotes: 3

Views: 205

Answers (1)

Virgile
Virgile

Reputation: 10148

Eva indicates that the status is unknown because it has observed a callstack where the assertion was valid and another were it was invalid. However, because the plug-in performs over-approximations (well, not here, as your program is trivial, but in the general case there will be), it has no way to be sure that both can happen in a concrete execution: one of the branch (either the one validating the assertion or the one invalidating it) might be impossible to reach in the concrete world, because of conditions that are out of reach of the abstractions that are used by Eva. Hence the only sound possibility, which encompasses all possibilities, is to put an Unknown status here.

You can also see the same issue arise if you comment out the foo(1) call. Eva will then report that the assertion is invalid, but only provided that it can indeed be reached.

Finally, this kind of annotations are indeed the ones you usually want to investigate about first (as opposed to annotations with a "plain" Unknown status), and in newer versions of Frama-C (starting from v17.0), you have an additional panel Red Alarms that lists properties that are invalid for at least one callstack.

Upvotes: 3

Related Questions