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] 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