Search code examples
cframa-c

Frama-c Assertion

Recently I have been working with frama-c and I have faced a problem which is a bit confusing.

I have written a very simple program in frama-c which is this:

void main(void)
{
    int a = 3;
    int b = 4;
    /*@ assert a == b;*/
}

I expect frama-c to say the assertion is not valid which in GUI this is shown by red bullet, but instead frama-c says the assertion is not valid according to value (under hypothesis), which is shown by orange-red bullet.

My question is why would frama-c say the assertion is not valid under hypothesis?

What are the possible hypotheses?

I am asking this because my program is very simple and I can't find any hypothesis or dependency in my program which is related to the assertion and I guess frama-c should just say the assertion is not valid.

Solution

  • An alternative way to see the dependencies of a property proven under hypotheses is to use the Report plugin, on the command-line:

    $ frama-c -val c.c -then -report

    [report] Computing properties status...

--------------------------------------------------------------------------------
--- Properties of Function 'main'
--------------------------------------------------------------------------------

[  Alarm  ] Assertion (file c.c, line 5)
            By Value, with pending:
             - Unreachable program point (file c.c, line 5)

--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
     1 Alarm emitted
     1 Total
--------------------------------------------------------------------------------

    The pending information lists all the properties required to finish the proof. For statutes emitted by the Value/Eva plugin, the only dependences emitted will always be reachability ones.

    (This is actually misleading: the status of the n th property actually depends on the statuses for the properties k with k < n. This would generate a dependency graph too big, so those dependencies are not tracked.)