--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on August 2017 ---
[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>