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

Hello,

I rewrote the specification regarding to your advices.
(I attached again a simplified version of it to this mail.)
Doing that I found that using predicates in preconditions sometimes may
cause "strange" behavior.

For example:
Using the Valid predicate like 
requires Valid(s);
causes that a false postcondition like ensures 0 == 1; is not detected.
But replacing Valid(s) by the content of the predicate, which is 
requires \valid(s);     
requires \valid_range(s->c, 0, s->N-1);
requires 0 <= s->n <= s->N && 0 < s->N; 
results in ensures 0 == 1; being detected.

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 guess this is what caused most of the trouble in our stack and queue
specifications.
 
Thanks a lot,
Kerstin

--
I use:
Frama-C Boron, Why 2.26, Simplify 1.5.4(7), Alt-Ergo 0.91, Z3 2.7 on Mac OS
X.



-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/ms-tnef
Size: 141837 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100817/173712cc/attachment-0001.bin>