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 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