--- layout: fc_discuss_archives title: Message 27 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 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
-------------- 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/20120821/ece34100/attachment.pgp>