--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on October 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