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] Frama-c-discuss Digest, Vol 110, Issue 6

Hello Jens,

On Wed, 8/9/2017, 12:23:39 PM, Gerlach, Jens  
<jens.gerlach at fokus.fraunhofer.de> wrote:
> Thank you for your pointers.
> I am not sure what you mean by “smt2 files”.
> When I run Frama-C/WP I do not obtain files with an “.smt2” extension.

Just to be sure, this means that WP is done in Frama-c, and not in Why?

> As far as I understand the proof obligations are contained in files that  
> end in “.why”.

Assuming thes answer to my above question is "yes", then these are  
basically the VCs, but in Why3 syntax and not SMTLib syntax. You can  
transform them using why3 with a commandline like this:

$ why3 -P <prover> -o <output-folder> <whyfile>.why

The <prover> part above is the one you have in your .why3.conf file, for  
example -P cvc4, or -P cvc4-1.5 or something like that. The  
<output-folder> is a folder that must previously exist and that will  
contain, after the above command, the file(s) for the prover. The  
<whyfile>.why is the *.why file that you got from Frama-C. Depending on  
what the .why files contain, several prover files may be generated for a  
single .why file.

You can run the provers on the obtained files to check that the above  
process worked and that the results are as expected (i.e. VC is proved or  
not proved as expected).

Note:

* Frama-C might pass extra command line options to why3 which may change  
the transformation of the VCs. Ideally you would need to pass the same  
options to why3 in your command.
* Same for the prover options.


-- 
Johannes Kanig, PhD
Senior Software Engineer
<kanig at adacore.com>