--- layout: fc_discuss_archives title: Message 30 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



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>