--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on August 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] trouble discharging some proof obligations related to strings



Dear All,

I'm learning about Frama-C (Nitrogen) trying to annotate some of my C
code. I have the function strprevchr below in an integer-based version
and in a pointer-based version.

With the integer-based version all POs that are generated by Jessie
are discharged, but with the pointer-based version there are two POs
that do not get discharged. I have followed Claude March?'s advice and
looked at the POs in Coq (which I haven't used before and am picking
up as I go). Using Coq on this I haven't really gotten much further.

I'm hoping that someone more knowledgeable about Frama-C/Jessie & Coq
would take a look and advise on how to proceed.

Thanks in advance and best regards,

Marko
-------------- next part --------------
#ifndef STRINGEXTRA_H
#define STRINGEXTRA_H

const char *strprevchr(const char *endp, char c, const char *startp);

#endif

-------------- next part --------------
#include <stddef.h>
#include "stringExtra.h"
/*@
  @ predicate AbsentTail{L1,L2}(char *ep1, char *ep2, char c) =
  @    \forall char *p;
  @       ep2+1 <= p <= ep1
  @         ==> \at(*p,L1) != c;
  @*/

/*@ requires endp >= startp && \valid_range(startp, 0, endp-startp) && \base_addr(startp) == \base_addr(endp);
  @ 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 && *r == c;
  @   ensures startp <= \result <= \at(endp, Pre);
  @*/
const char *strprevchr(const char *endp, char c, const char *startp) {
  /*@
    @ loop invariant \at(endp,Pre) >= endp >= startp-1 && \valid_range(endp, 0, \at(endp,Pre)-endp)
    @ && AbsentTail{Pre,Here}(\at(endp, Pre), \at(endp, Here), c);
    @ loop variant endp-startp;
    @*/
  while (endp >= startp && *endp != c)
    endp--;
  if (endp >= startp)
    return endp;
  else
    return NULL;
}

-------------- next part --------------
#ifndef STRINGEXTRA_H
#define STRINGEXTRA_H

int strprevchr(int endi, char c, const char array[]);

#endif

-------------- next part --------------
#include <stddef.h>
#include "stringExtra.h"
/*@
  @ predicate AbsentTail{L1,L2}(int e1, int e2, char c, char *array) =
  @    \forall int i;
  @       e2+1 <= i <= e1
  @         ==> \at(array[i],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 i; 0 <= i <= endi && array[i] == 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}(\at(endi,Pre), \at(endi,Here), c, array);
    @ loop variant endi;
    @*/
  while (endi >= 0 && array[endi] != c)
    endi--;
  return endi;
}

-------------- 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/20120830/8e34427d/attachment.pgp>