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