--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on May 2010 ---
[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"?