Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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