--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on August 2010 ---
[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>