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

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>