--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on May 2010 ---
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. Even if some of your functions contain constructs that are temporarily or permanently not supported by Jessie, as long as the effects of these functions can be characterized with an ACSL specification, this does not preclude its use for other functions. There are also -deps and -out options in Frama-C for computing various versions of the footprint of a function. They rely on completely different techniques and are not quite as compositional as Jessie. These work best when analyzing the source code of a complete task, including the source code for the library functions that are called from the task (or a modelization in C of these functions, or a minimal ACSL specification). Pascal