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] trouble discharging some proof obligations related to strings

  • Subject: [Frama-c-discuss] trouble discharging some proof obligations related to strings
  • From: MarkoSchuetz at web.de (Marko Schütz Schmuck)
  • Date: Thu, 30 Aug 2012 13:24:14 -0400
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>