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

-- "Gerlach, Jens" (2017-08-09)
> Hello Yannick and Johannes.
> 
> Thank you for your pointers.
> I am not sure what you mean by “smt2 files”.

These are the input files for CVC4, in SMT-LIB2 syntax. 

> When I run Frama-C/WP I do not obtain files with an “.smt2” extension.

The extension does not matter. In SPARK, we generate files with an extension .smt2 for CVC4, since we're using the SMT-LIB2 syntax for these. But maybe Frama-C/WP uses another extension. Or maybe you don't get the intermediate file in SMT-LIB2 syntax unless you use an option to keep intermediate files?

> As far as I understand the proof obligations are contained in files that end in “.why”.
> Do you think that they might be sufficient for the cvc4 people?


CVC4 people will need files in SMT-LIB2 syntax, not files in Why3 syntax.

--
Yannick Moy, Senior Software Engineer, AdaCore




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170809/48684137/attachment.html>