--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on August 2010 ---
Hello, we have tried to prove the algebraic axioms for a stack. Doing this some problems occured. We were able to prove something, but unfortunately we could also prove that 0 == 1, which means something must be wrong. You can find a small example attached to this mail. pop.c finds the false postcondition, but equal_pop.c, which runs pop twice does not. Kind Regards, Kerstin -------------- next part -------------- A non-text attachment was scrubbed... Name: stack.zip Type: application/zip Size: 2158 bytes Desc: stack.zip URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100817/d0101061/attachment.zip>