--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on October 2008 ---
This is of course translated to standard ACSL (http://frama-c.cea.fr/download/acsl_1.3.pdf) so that all existing plug-ins can take advantage of user annotations without having to parse the idiosyncratic syntax invented here or there (?) Pascal -----Original Message----- From: frama-c-discuss-bounces@lists.gforge.inria.fr on behalf of Yannick Moy Sent: Thu 10/9/2008 1:41 PM To: frama-c-discuss Subject: [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 >