--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on June 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] multiple switch on one variable



> In that case, frama-c/ Jessie will check the postcondition for the cases
> that (x=1 and x=3) as well as (x=1 and x=4) and go on..
>
> Unless that normally we will never have both x= 1 and x= 3 at the same time.

Oh, I think I understand your question now.

You are looking at the various goals generated for the single
post-condition and you
see things such as:

integer_of_int32(x_0) = 3

and:

integer_of_int32(x_0) = 5

as hypotheses for the same goal,
and you are wondering why Why considers this impossible case.

This is normal. It has not started to think yet at the time it has
generated these two incompatible hypotheses. Don't worry, automated
theorem provers are very good at noticing that there is \false in the
hypotheses and concluding directly (here, reproducing the reasoning
that whatever logical property needs to be verified is true because
the case where x is both 3 and 5 simultaneously never happens).

If you are worried that with all these impossible cases, the total
number of goals will be too large, use option
-jessie-why-opt="-fast-wp". This will generate a single goal, which
will of course be more complex.

Pascal