--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on August 2012 ---
Dear All, I'm learning about Frama-C (Nitrogen) trying to annotate some of my C code. I have the function strprevchr below in an integer-based version and in a pointer-based version. With the integer-based version all POs that are generated by Jessie are discharged, but with the pointer-based version there are two POs that do not get discharged. I have followed Claude March?'s advice and looked at the POs in Coq (which I haven't used before and am picking up as I go). Using Coq on this I haven't really gotten much further. I'm hoping that someone more knowledgeable about Frama-C/Jessie & Coq would take a look and advise on how to proceed. Thanks in advance and best regards, Marko -------------- next part -------------- #ifndef STRINGEXTRA_H #define STRINGEXTRA_H const char *strprevchr(const char *endp, char c, const char *startp); #endif -------------- next part -------------- #include <stddef.h> #include "stringExtra.h" /*@ @ predicate AbsentTail{L1,L2}(char *ep1, char *ep2, char c) = @ \forall char *p; @ ep2+1 <= p <= ep1 @ ==> \at(*p,L1) != c; @*/ /*@ requires endp >= startp && \valid_range(startp, 0, endp-startp) && \base_addr(startp) == \base_addr(endp); @ assigns \nothing; @ behavior absent: @ assumes \forall char *p; startp <= p <= endp ==> *p != c; @ ensures \result == NULL; @ behavior present: @ assumes \exists char *r; startp <= r <= endp && *r == c; @ ensures startp <= \result <= \at(endp, Pre); @*/ const char *strprevchr(const char *endp, char c, const char *startp) { /*@ @ loop invariant \at(endp,Pre) >= endp >= startp-1 && \valid_range(endp, 0, \at(endp,Pre)-endp) @ && AbsentTail{Pre,Here}(\at(endp, Pre), \at(endp, Here), c); @ loop variant endp-startp; @*/ while (endp >= startp && *endp != c) endp--; if (endp >= startp) return endp; else return NULL; } -------------- next part -------------- #ifndef STRINGEXTRA_H #define STRINGEXTRA_H int strprevchr(int endi, char c, const char array[]); #endif -------------- next part -------------- #include <stddef.h> #include "stringExtra.h" /*@ @ predicate AbsentTail{L1,L2}(int e1, int e2, char c, char *array) = @ \forall int i; @ e2+1 <= i <= e1 @ ==> \at(array[i],L1) != c; @*/ /*@ requires endi >= 0 && \valid_range(array, 0, endi); @ assigns \nothing; @ behavior absent: @ assumes \forall int i; 0 <= i <= endi ==> array[i] != c; @ ensures \result == -1; @ behavior present: @ assumes \exists int i; 0 <= i <= endi && array[i] == c; @ ensures 0 <= \result <= \at(endi, Pre); @*/ int strprevchr(int endi, char c, const char array[]) { /*@ @ loop invariant \at(endi,Pre) >= endi >= -1 && AbsentTail{Pre,Here}(\at(endi,Pre), \at(endi,Here), c, array); @ loop variant endi; @*/ while (endi >= 0 && array[endi] != c) endi--; return endi; } -------------- next part -------------- A non-text attachment was scrubbed... Name: not available Type: application/pgp-signature Size: 198 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120830/8e34427d/attachment.pgp>