--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on August 2012 ---
Dear Claude, At Wed, 22 Aug 2012 17:27:23 +0200, Claude Marche wrote: > > > Indeed, the Why3 memory modl sesm to miss an axiom to discharge your > obligations. You can try to edit the file > > lib/why3/jessie.why > > find the section regarding sub_pointer and add the axiom > > axiom sub_pointer_neg: > forall p q:pointer 't. sub_pointer p q = - sub_pointer q p > > It works for me this works for me too. I'm using why2 and changed your suggestion to axiom sub_pointer_neg: forall p:'t pointer. forall q:'t pointer. sub_pointer(p,q) = -sub_pointer(q,p) Thank you very much! Best regards, Marko > - Claude > > Le 21/08/2012 23:25, Marko Sch?tz Schmuck a ?crit : > > 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 > > > > > > > > _______________________________________________ > > Frama-c-discuss mailing list > > Frama-c-discuss at lists.gforge.inria.fr > > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > -- > Claude March? | tel: +33 1 72 92 59 69 > INRIA Saclay - ?le-de-France | > Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ > F-91405 ORSAY Cedex | > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- 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/20120822/29d6f4e4/attachment.pgp>