--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on August 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C/Jessie first steps... problems with pointers



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                    |