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] proving stack axioms with jessie

Le mar. 17 ao?t 2010 17:06:02 CEST,
"Kerstin Hartig" <kerstin.hartig at first.fraunhofer.de> a ?crit :

> 
> This problem only ocurs with the Simplify prover right now.
> So maybe it is just a prover problem? And Simplify is not safe to use?

I have not taken the time to dig much further, but if you enable debug
mode in GWhy (in the Proof menu), you can see on the terminal that
Simplify rightly answers Invalid...

... but in that case, it outputs a counter-example (i.e. a model of the
negation of the formula), which of course contains occurences of the
Valid predicate. My guess is that the regexp used by Why to check
Simplify's answer needs to be refined.

In the mean time, renaming Valid to something else might help ;-)

-- 
E tutto per oggi, a la prossima volta.
Virgile