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

  • Subject: [Frama-c-discuss] Frama-C/Jessie first steps... problems with pointers
  • From: MarkoSchuetz at web.de (Marko Schütz Schmuck)
  • Date: Tue, 21 Aug 2012 17:25:35 -0400
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>