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