--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] lightweight annotations for Jessie



Hello,

I just coded some lightweight annotations for those who use Frama-C with the
Jessie plugin to perform deductive verification. Say you want to express
that some function parameters and returns are non-null.

First define a non-null predicate:

//@ predicate non_null(void *p) = p != 0;

Then, define a declspec of the same name, usually through a macro:

#define NON_NULL __declspec(non_null)

Finally, decorate function parameters and returns with the appropriate
declspec! The corresponding proposition gets added to the function
precondition for parameters, and to the function postcondition for returns:

char*NON_NULL f(char *NON_NULL x, char *y) {
  //@ assert x != 0;
  //@ assert y != 0;
  return x;
}

In the example above, 2 of 3 VC are automatically proved. The last one is
not provable of course (y != 0).

-- 
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081006/b931084d/attachment.html