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] Z3 and CVC3 issue in GWhy 2.26

  • Subject: [Frama-c-discuss] Z3 and CVC3 issue in GWhy 2.26
  • From: barbaraisabelvieira at gmail.com (Barbara Vieira)
  • Date: Thu, 27 Jan 2011 15:04:14 +0000
Dear all,

I have Frama-C Boron and Why 2.26 installed (Mac OSX binaries ) on Mac OSX and everything seems to work very well.

However it appears that I have an issue with GWhy because it does not detect some provers. There are few different things that happen:

	1. I have a translator for a small language called CAO, which translates CAO programs into Jessie input language. Running jessie tool on the output of my CAO2Jessie translator and using the makefile that Jessie generates to run GWhy, the CVC3 (version 2.1) prover works very well and it seems to be detected by Gwhy.

	2. On the other hand, running the Jessie plugin (using Frama-C > frama-c -jessie ex.c)  on a C file, seems that the CVC3 is not detected by Gwhy.

	3. I also have Z3 installed and it seems that Gwhy does not detect it in any case. However, when running why-config, both CVC3 and Z3 are detected.

	4. Both provers work very well when they are called directly, e.g.: make -f ex.makefile z3 

Does anyone has any idea of what is going wrong? Should I change some configuration file?!

It is very helpful to have all the provers working properly on GWhy.


Thanks in advance.
Best regards,
B?rbara Vieira