Frama-C-discuss mailing list archives

xavier.kauffmann at gmail.com (xavier kauffmann) · Wed, 16 Mar 2011 16:56:04 +0100

On Wed, Mar 16, 2011 at 12:00 PM, <
frama-c-discuss-request at lists.gforge.inria.fr> wrote:

> Send Frama-c-discuss mailing list submissions to
>        frama-c-discuss at lists.gforge.inria.fr
>
> To subscribe or unsubscribe via the World Wide Web, visit
>
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
> or, via email, send a message with subject or body 'help' to
>        frama-c-discuss-request at lists.gforge.inria.fr
>
> You can reach the person managing the list at
>        frama-c-discuss-owner at lists.gforge.inria.fr
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Frama-c-discuss digest..."
>
>
> Today's Topics:
>
>   1. Re: precision for expression evaluation in a      condition
>      (Pascal Cuoq)
>   2. Re: precision for expression evaluation in        acondition
>      (Pascal Cuoq)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Tue, 15 Mar 2011 21:17:55 +0100
> From: Pascal Cuoq <pascal.cuoq at gmail.com>
> Subject: Re: [Frama-c-discuss] precision for expression evaluation in
>        a       condition
> To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
> Message-ID:
>        <AANLkTinvN4XhDa3GnxL2rSwFN60E4F88wso+T6A_38q- at mail.gmail.com>
> Content-Type: text/plain; charset=UTF-8
>
> On Tue, Mar 15, 2011 at 6:36 PM, xavier kauffmann wrote:
> > when evaluating bar at the toto = 1; line I get:
> > Before statement:
> > bar ? {1234; }
> > At next statement:
> > bar ? [--..--]
> > [...]
> > Even if there is only one line in the else branch?
> > If possible I'm looking for a way to evaluate an expression at the
> > statement, not before or after.
> > If the statement modifies the expression it does not work but if it is
> not
> > related to it, shouldn't the value analysis be able to provide a value or
> > range for this expression?
>
> With Frama-C's representation of the AST, there is really no place you
> might want to observe the values of variables other than before a
> statement or after a statement. This said, note that your version does
> not claim it gives you the values of bar after the statement. It says
> it gives you the value "at next statement" (which should in some cases
> be "at next statements").
>
> After this introduction, please read
> http://blog.frama-c.com/index.php?post/2011/01/11/Seven-errors-game
> and note that it was published before the release of Frama-C Carbon
> 20110201.
>
> Regarding the "if it is not related to it, shouldn't the value
> analysis be able to provide a value or range for this expression?"
> part of your question: of course, it can provide the value of an
> unrelated expression. If your program has a thousand globals, the
> value of each global at each statement is saved just in case you later
> want to inspect the value of that variable at that program point.
>
Would an ocaml script be able to get this information?
If so how much knowledge of ocaml would it require?
Could you please give some hint about which FramaC api should be used?

>
> > when I was hoping for something like
> > bar ? [--..--] - {1234}
> > based on the evaluation of bar at the toto = 1 and toto = 3 lines
> > Is there a way to get these exclusions from the value analysis?
>
> Well, you may have noticed that "[--..--] - {1234}" is not in the
> documented list of formats in which the value analysis can display
> sets of values. However, you may get the sets [-2^31 .. 1233] and
> [1235 .. 2^31-1] programmatically, provided you are willing to insert
> an annotation to guide the value analysis.
>
Could you please provide an example?
Will it require some additional command line options?

>
> Considering the lab's current focus on the verification of syntactic
> coding rules, if I were you, I wouldn't hold too much hope of seeing
> 1/ how to access these sets documented;
> 2/ their computation made entirely automatic (without need for a user
> annotation).
>
> Pascal
>
Thank you

-Xavier

>
>
>
> ------------------------------
>
> Message: 2
> Date: Tue, 15 Mar 2011 21:34:22 +0100
> From: Pascal Cuoq <pascal.cuoq at gmail.com>
> Subject: Re: [Frama-c-discuss] precision for expression evaluation in
>        acondition
> To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
> Message-ID:
>        <AANLkTim63ipSYqeVjAJahQotbWHOSOaotRiU2H02hDWR at mail.gmail.com>
> Content-Type: text/plain; charset=ISO-8859-1
>
> > I don't know the value analysis very well but maybe it is related
> > to the fact that you do not provide an initial value for toto.
> > If I modify your programm like
> >
> > ? int toto;
> > ? printf("%d\n", toto);
> >
> > then I get the value
> >
> > 1606415944
>
> Considering that it's the value of variable bar the discussion is
> about, and that the program is safe from uninitialized access (until
> you modify it with your call to printf), I do not think that this is
> related.
>
> You can learn about the value analysis by typing "frama-c -val test.c"
> on Xavier's example. It will tell you that the original uses toto
> correctly and that your modification accesses toto unsoundly.
> Uninitialized variables passed as arguments to library functions is a
> vexing problem for technical reasons that would take too long to
> describe here, but if you are using patchlevel 1 of Carbon's value
> analysis, you will get:
> t.c:5:[kernel] warning: accessing uninitialized left-value toto:
> assert(Ook)
>
> Link:
> http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2011-February/002527.html
> It's one of the fixes for 2011/02/12.
> It may have been working correctly in previous versions. As I said, it
> is a vexing issue.
>
> Pascal
>
>
>
> ------------------------------
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
> End of Frama-c-discuss Digest, Vol 34, Issue 12
> ***********************************************
>
-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? nettoy?e...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110316/1fe366e0/attachment.htm>

Frama-C-discuss mailing list archives

[Frama-c-discuss] Frama-c-discuss Digest, Vol 34, Issue 12