--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on April 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin



> - the alt-ergo file for the second assertion is not the same as the
>   first one. I understand that the first assertion is "embeded" in
>   the second one (*). How to "isolate" each assertion from the other
>   one, or in other words, how to tell frama-c and the external
>   provers that, for me and the problem I consider, the order of
>   computation of x1 and x2 does not matter ? 


No there is no way to make such a slicing at the WP level. Indeed, you what to take a possible advantage of the inserted assertions !
But, in this specific case, a variable dependency analysis shows that the proof obligation can be splitted into two.
Basically, you have to prove the following :

(0 < x) => (0 < y) => (0 < x*x) => (0 < y*y)

Dependency analysis shows that this is equivalent to prove :

( (0 < y) => (0 < y*y) ) OR ( (0 < x) => (0 < x*x) => False )

Indeed, many proof obligations generated by WP are provable because of an inconsistency in the hypotheses, which are associated to infeasible execution paths.
So, it is difficult to discard the second one. Now we have to call the solver twice !
Actually, we have no such dependency analysis already implemented.
Moreover, generating a disjunction of proof obligations requires a more complicated strategy with the solvers.

	L.