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

  • Subject: [Frama-c-discuss] proving stack axioms with jessie
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
  • Date: Tue, 17 Aug 2010 12:28:17 +0200
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>