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

[Frama-c-discuss] Re: lightweight annotations for Jessie



Hi,

A quick follow-up on the same subject. I added support for declspec that
express properties of function parameters and returns with additional
arguments. E.g. one can express that integer parameters and returns fit in a
specific range like that:

//@ predicate range(integer i, integer lb, integer rb) = lb <= i <= rb;

#define RANGE(a,b) __declspec(range(a,b))

int RANGE(-5,15) f (int RANGE(0,5) x, int RANGE(-5,10) y) {
  //@ assert 0 <= x <= 5;
  //@ assert -5 <= y <= 10;
  return x + y;
}

For those constructs that are not predicates, Jessie prolog defines specific
declspec:

#define FRAMA_C_PTR __declspec(valid)
#define FRAMA_C_ARRAY(n) __declspec(valid_range(0,n))

and an annotation for strings that could be defined in user code but is
better defined in the prolog because it is useful for everybody:

#define FRAMA_C_STRING __declspec(valid_string)

So that one can specify a function like this:

char *
FRAMA_C_ARRAY(n-1)
FRAMA_C_STRING
my_string_copy (char *FRAMA_C_ARRAY(n-1) dest,
        const char *FRAMA_C_STRING src,
        unsigned n)
{
  // ...
  return dest;
}

I personally like this way of annotating functions. Please let me know if
you have ideas to improve on this.
Thanks,

-- Yannick


On Mon, Oct 6, 2008 at 7:10 PM, Yannick Moy <yannick.moy@gmail.com> wrote:

> 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/20081009/556f211b/attachment.html