--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on April 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] VC not the same when verifying function in isolation or in complete compilation unit



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