--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on August 2012 ---
Dear All, I am adding ACSL annotations to some C code: #include <stddef.h> #include "stringExtra.h" /*@ @ predicate AbsentTail{L1,L2}(char *ep, char c) = @ \forall char *p; @ \at(ep,L2)+1 <= p <= \at(ep,L1) @ ==> \at(*p,L1) != c; @*/ /*@ requires endp >= startp && \valid_range(startp, 0, endp-startp); @ 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 @ ==> \forall char *p; r+1 <= p <= endp ==> *p != c && *r == c; @ ensures startp <= \result <= \at(endp, Pre) && *\result == c; @*/ const char *strprevchr(const char *endp, char c, const char *startp) { /*@ @ loop invariant \at(endp,Pre) >= endp >= startp-1 && AbsentTail{Pre,Here}(endp, c); @ loop variant endp-startp; @*/ while (endp >= startp && *endp != c) endp--; if (endp >= startp) return endp; else return NULL; } To my surprise none of the ATPs (z3,cvc3, alt-ergo, yices, simplify) discharges the proof obligation that the pre-condition implies the loop invariant. For an integer-based version with similar functionality all ATPs discharge this specific PO. #include <stddef.h> #include "stringExtra.h" /*@ @ predicate AbsentTail{L1,L2}(int e, char c, char *array) = @ \forall int i; @ \at(e,L2)+1 <= i <= \at(e,L1) @ ==> \at(array[\at(i,L1)],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 r; 0 <= r <= endi @ ==> \forall int p; r+1 <= p <= endi ==> array[p] != c && array[r] == 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}(endi, c, array); @ loop variant endi; @*/ while (endi >= 0 && array[endi] != c) endi--; return endi; } 1. What is it that I am missing here? 2. For the future: what would be a good resource to help me answer questions similar to this one? Thanks a lot in advance and best regards, Marko -------------- 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/20120821/ece34100/attachment.pgp>