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] lightweight annotations for Jessie

  • Subject: [Frama-c-discuss] lightweight annotations for Jessie
  • From: yannick.moy at gmail.com (Yannick Moy)
  • Date: Mon Oct 6 19:10:46 2008
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