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] Jessie Plugin Tutorial

  • Subject: [Frama-c-discuss] Jessie Plugin Tutorial
  • From: lc at adelard.com (Lukasz Cyra)
  • Date: Fri, 19 Jun 2009 16:52:33 +0100
Hi,

I tried to repeat some of the exercieses, which are contained in the Jessie Plugin Tutorial, however, I was not able to obtain the same results. In many cases, for which the tutorial claims that certain SMT solvers can provide a possitive answer I was only obtaining a qustion mark. In particular non of the SMT solvers I used was able to demonstrate the lemma about mean value:
/*@ lemma mean : \forall integer x, y; x <= y ==> x <= (x+y)/2 <= y; */

My question is what is the reason of such a situation. If it depends on the version of solvers what versions should I use to obtain similar results:

My configuration is:

- Linux

- Frama C Lithium Dec 2008

- Alt-Ergo 0.8

- Simplify 1.5.5 (also tried 1.5.4)

- Yices 1.0.21 (also tried 1.0.17) <--- this was the solver which in the tutarial is claimed to be very powerful, but in my case did not seem so

- CVC3 1.5

- Z3 1.3
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090619/6e6d945d/attachment.htm