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] hint assertions and understanding cooperation between wp and value plugin

  • Subject: [Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin
  • From: loic.correnson at cea.fr (Loïc Correnson)
  • Date: Thu, 21 Apr 2016 17:36:10 +0200
  • In-reply-to: <87k2jrkp3q.fsf@inria.fr>
  • References: <87k2jrkp3q.fsf@inria.fr>
> - 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.