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