# 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...

*Subject*: [Frama-c-discuss] A few (newbye) questions...*From*: virgile.prevosto at cea.fr (Virgile Prevosto)*Date*: Wed, 13 May 2009 11:25:40 +0200*In-reply-to*: <4A07F01D.8030109@fr.thalesgroup.com>*References*: <4A07F01D.8030109@fr.thalesgroup.com>

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

**Follow-Ups**:**[Frama-c-discuss] A few (newbye) questions...***From:*eric.jenn at fr.thalesgroup.com (JENN Eric)

**References**:**[Frama-c-discuss] A few (newbye) questions...***From:*eric.jenn at fr.thalesgroup.com (JENN Eric)

- Prev by Date:
**[Frama-c-discuss] usage of why-dp** - Next by Date:
**[Frama-c-discuss] String results in logical specifications** - Previous by thread:
**[Frama-c-discuss] A few (newbye) questions...** - Next by thread:
**[Frama-c-discuss] A few (newbye) questions...** - Index(es):