--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on April 2016 ---
On Fri, Apr 08 2016 at 09:28:29 AM, Loïc Correnson <loic.correnson at cea.fr> wrote: > Hi, Hi, Loic. > Thanks for this detailed report. Thanks for the detailed answer! > First, may I notice that everything is completely proved by default with the forthcoming new release of Frama-C and Alt-Ergo 1.01. OK, I have forgotten to precise I am currently using Frama-C Magnesium with Alt-Ergo 1.01 and Why3 0.87. > However, there are interesting points in your experience report, that I shall comment on. > - files with *.txt suffix are only « human readable » printing of the VCs, without any formally defined syntax > - the two wp-print-*.txt in your submitted report are identical :-( > - the VC sent to alt-ergo with the native wp driver are *.ergo files (for the goal only) and *.mlw files (including the libraries) > - it should be interesting to see if the VCs sent to alt-ergo are really different and eventually send a bug report I have written something wrong in my previous mail: all my proof attempts have been done through Why3 (I have upgraded my installation of Alt-Ergo to version 1.01 and Frama-C Magnesium cannot parse Alt-Ergo 1.01 outputs). VC generated in both cases with -wp-prover alt-ergo are valid (despite the parsing problem with Magnesium) and generated ergo files are perfectly identical. The VC are different only when using Why3 as a frontend to Alt-Ergo. Sorry for the mistake. > There is actually a difference when running wp in isolation on one > function or several ones, or on a single property and on a bunch of > properties ; on the logical point of view, all the generated VCs shall > be equivalent ; however, due to free variable generators, incremental > and cached compilation, library inclusion, we can have small > differences (variable renaming, non-filtered hypotheses, > etc.). Unfortunately, SMT solvers *are* sensitive to such > differences. > Although, we are continuously working on reducing such disturbing > differences, but sometimes, it requires deep refactoring of WP > internals. > > The extreme illustration of such differences arise when comparing Why3 > output for Alt-Ergo and WP output for Alt-Ergo. The two platforms > (Why3 and WP) rely on the same Alt-Ergo theories, but we are using > slightly different encoding for some constructs. For instance, you may > have a look at <frama-c-share>/wp/default.driver and compare how a > given theory is implemented for native alt-ergo and why3. Thanks for the suggestion, I will look at the driver. > It is interesting to notice that, to prepare a Frama-C distribution, > we build the shared WP resources for native alt-ergo and why3 provers > from a unique, separate Why3 development, with dedicated realization > plugins. These common Why3 theories are partially realized in Coq to > ensure consistency. This methodology shows to be reliable and > productive and we are working on making it available for Frama-C/WP > users, as a step forward in the integration of Why3 and Frama-C. That would be great. Thanks again for your answer and sorry for my previous mistake. Christophe -- Christophe Garion ISAE-SUPAERO/DISC garion at isae-supaero.fr 10 avenue Edouard Belin Tél : +33 5 61 33 80 57 BP 54032 Fax : +33 5 61 33 83 45 31055 Toulouse Cedex 4