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] A few (newbye) questions...

Hello ?ric,

Le lun. 11 mai 2009 11:30:05 CEST,
JENN Eric <eric.jenn at fr.thalesgroup.com> a ?crit :

> 
> + First, I guess I definitively need some good introductory book before asking dumb questions... any advice?

The Why lecture at the TYPES summer school (available on
http://why.lri.fr/) might be a good start.

> + Is is possible to use ATP to discharge proof obligations using modulo arithmetic?

In theory yes. In practice, modulo arithmetic is much more difficult
to handle than "normal" integer arithmetic. However, your example does
not really deal with modulo, but rather with bitvector operations. Some
of the provers supported by why can deal with that natively, but the
model used by why itself does not take advantage of that, and the
axiomatisation of these operations in why is very weak.

> + If not, shall I use Coq?

This won't really help here. The issue is to provide an adequate
axiomatisation for bitwise operations. A set of 'lemmas'
which allow to prove (at least with Z3) the proof obligations generated
by your example is the following

/*@ lemma shift_left_bw_distributes:
  \forall integer x, y, n; ((x&y)<<n) == ((x<<n)&(y<<n));
  lemma shift_left_right :
  \forall integer x, y, n;
  ((x>>n)&y) ==  ((x&(y<<n))>>n);
  lemma shift_zero :
    \forall integer n; 0>>n == 0;
  lemma one_bit_mask :
  \forall integer x,n; (x & (1<<n)) == (1<<n) || (x & (1<<n)) == 0;
*/

Again, note that none of these lemmas can be proved with the current
axiomatization of bitwise operations: they have to be assumed.

> + What kind of "post installation" tweaking shall I do to be able to use Coq with Why?

If for some reason (Coq was not installed or its standard library was
installed in a place which was not writable) Why is not able to put the
Coq files containing its own prelude in a place where Coq can find them
by default, it installs them with the other Frama-C files. Adding the
option -I `frama-c -print-path`/why/coq to the
coqc/coqide/coqtop command line should help.

> + Is there any Frequently Asked Questions on Jessie / Why?

Not really. The Frama-C wiki
(http://bts.frama-c.com/dokuwiki/doku.php?id=mantis%3AFrama-C%3Astart)
contains very few questions (and answers), but this needs to be
extended.

> + Is there any document explaining / giving hints on how ACSL specifications shall be preferably written in order to facilitate the proof ? (or, at least, the type of things one shall never write in order to have any change to discharge POs)?

No. In fact, this depends not only on the specification, but also on
the code, and on the underlying memory model and axiomatisation of
built-in operations. Moreover, given enough admitted auxiliary lemmas,
any PO can be discharged (of course, usage of
//@ lemma admit_everything: \false;
is not exactly recommended for any serious verification activity).

Best regards, 
-- 
Virgile Prevosto
Ing?nieur-Chercheur, CEA, LIST
Laboratoire de S?ret? des Logiciels
+33/0 1 69 08 71 83