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] questions about value analysis

  • Subject: [Frama-c-discuss] questions about value analysis
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
  • Date: Sat, 24 Oct 2009 23:22:19 +0200
  • References: <4ADDDC4F.2080502@wanadoo.fr>
Sorry for the French questions (resp. English answers);
this is a reply to an e-mail sent privately. Note that
if you do not have a maintenance/evolution contract
or existing collaboration that forces developers to
treat your e-mail as important, your best bet for an answer
is to use this (frama-c-discuss) list. If you would like
to set up such a contract, Benjamin.Monate at cea.fr
will be delighted to hear from you. If you would like to
subscribe to frama-c-discuss, the instructions are here:

http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

> les assertions utilisateur ne semblent pas etre utilisees.
> Est-ce qu'il y a une option pour les utiliser sous forme de contraintes ?

This is supposed to work as documented. Note that the
documentation states that the propagated state may not be
reduced as much as allowed by a user assertion, and in
the worst case, not at all. If it seems not to work for you,
you can report it as a bug:

http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:start#using_the_bts

BTS accounts are not shared with frama-c-discuss ones
(sorry about that), but are shared with Frama-C wiki accounts.

> - quelles sont les erreurs runtime detectees ?
> Je n'ai pas l'impression que ce soit les memes qu'avec PolySpace
> (undefined, unspecified, implementation defined dans la norme).

We do not have access to PolySpace, although we have some
idea of what it does. The value analysis aims at emitting alarms
for any undefined or unspecified behavior from the standard.
HOWEVER, it re-classifies some of these behaviors as
implementation-defined behaviors for which it uses the
target platform's definition of what should happen.

Available target platforms can be listed with the "-machdep help".

We welcome and take into account reports of compilers 
breaking this approach by actually not having
reproducible behavior on these constructions 
that have been "upgraded" to "implementation-defined".
This has happened before for signed arithmetic overflows,
which we would have liked to simply handle in
2's-complement arithmetic, and which gcc insists
on treating as undefined for optimization opportunities that
probably allows them to gain 1% on some speed benchmark.

In fact, emitting alarms for signed arithmetic overflows would
already have become the default if it didn't (rightly) warn
about so many existing, hitherto considered fine, programs,
including some already in our regression tests. Eventually,
this will be an option of the target platform description.

> D'autre part la liste donnee pages 16-18 n'est pas complete.
> J'ai obtenu les messages:
> - accessing out of bounds index

I am pretty sure that this category of alarm is described in
the manual at

http://frama-c.cea.fr/download/value-analysis-Beryllium-20090902.pdf

but I do not have access to it right now for technical reasons.

The manual may not be clear enough
on the fact that out-of-bound accesses may take either
"\valid(p)" or "0 <= i && i < 10" depending on whether
the access is in an array.

> - non termination detected in function main

This message is not an alarm, it is an informative message.
A function may not terminate because of what would be
in PolySpace vocabulary a red alarm, or because of an
infinite loop. In either case, the message above is only
here to help track down the real problem, and is not
considered a problem itself.

> - j'utilise l'option unicode pour que les messages soient plus clairs.
> Mais j'obtiens:
> - dans le log: warning: accessing out of bounds index. assert ((0 ? i) ? 
> (i < 14));
> - dans le print: /*@ assert<((0 ? i) ? (i < 14));
>           // synthesized
> Que puis-je faire pour obtenir un texte plus clair.

The two mutually exclusive options are -unicode and 
-no-unicode. The former is the default (you don't need to
set it). It instructs Frama-C to use the Unicode charset.
If you cannot display all the Unicode characters produced
by Frama-C (mathematical symbols mostly), either switch
to a more complete font (the DejaVu font family is
recommended) or use the -no-unicode option, which
restricts Frama-C messages to the ACSII charset.

Pascal