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] Making frama-c-gui a read-only tool?

Hi,

> Have you tried the -save and -load options? Are there WP specific things
> that are missing from the loaded session?

Indeed, WP does not keep much data through -save/-load kernel options.
This is a design choice : WP calculus is fast, and the resulting proof obligations can be recomputed on demand.
On the contrary, discharging proof obligations with SMT solvers can be long, and interactive proof sessions (eg. with Coq) have inherent value to be saved and reused across different sessions.

For the SMT part, we have on ongoing task in VESSEDIA project for caching at a large scale proof obligation results, but we are just at the beginning of the project.

For the interactive proofs part, the -load/-save options are not enough : the binary OCaml values saved by the kernel generally do not survive to (even small) C/ACSL source changes, or to a Frama-C upgrade.
We can not impose to users to rewrite all their proofs at each source change ! Instead, we save text-based data into user sessions via `-wp-script` option.
In the next coming Frama-C release, featuring a new interactive prover for WP, this concept of user-sessions is much more evolved. Moreover, we have design algorithms to recover as much as possible from small C/ACSL source changes.

For this new interactive prover, a complete journal of what have been proved (and how) is kept. We have actually distinguish between two interactive modes : one mode for upgrading, editing or tuning proofs or SMT parameters, and a replay-mode which is read-only. Both modes are available from the command line and the GUI — although we do not have a « lock » option in the GUI : if you save a new proof, it would be written on disk !

	L.