Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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                    |