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] Uncaught exception

On Fri, May 7, 2010 at 7:27 AM, Pascal Cuoq <pascal.cuoq at gmail.com> wrote:
> On Thu, May 6, 2010 at 11:42 PM, Tom Hawkins <tomahawkins at gmail.com> wrote:
>> And a third question. ?What could be causing this exception? ?(I got a
>> little too ambitious and threw Frama-C our entire embedded design.)
>
> Again not quite the answer to your question,
> but in my opinion the single biggest advantage of
> Jessie and of the Weakest Precondition approach to
> verification is that it is compositional : when verifying a
> function, you only ever need to look at the code
> of the function you are verifying, the specs of the
> function you are verifying, and the specs of the callees.

Yes, I started to better appreciate this last night.  So what are the
recommended practices for annotating function declarations (i.e. in
header files) versus definitions, such that Jessie has enough
information when processing one file, or one function at a time?

One thing I noticed when experimenting with definition and declaration
annotations is that "assign \nothing;" does not mean "no side
effects".  For example, I had a function that assigned a static
top-level variable, which I specified in the definition annotation.
But in the header file, where the variable is hidden from view, I
placed "assign \nothing;".  None of the solvers complained.  So am I
correct is saying that "assign \nothing;" means "does not assign
anything in scope"?