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

Hi,
Thanks for this detailed report.

First, may I notice that everything is completely proved by default with the forthcoming new release of Frama-C and Alt-Ergo 1.01.

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

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.

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.

	L.

> Le 7 avr. 2016 à 16:55, Christophe Garion <christophe.garion at isae-supaero.fr> a écrit :
> 
> <msg_minimal.c>