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