--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on August 2012 ---
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 - 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 |