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] Annotating Ghost Contracts

  • Subject: [Frama-c-discuss] Annotating Ghost Contracts
  • From: jmaytac at sandia.gov (Aytac, Jon M)
  • Date: Wed, 9 Jan 2019 18:58:15 +0000
Hi,
    I have an example where a state machine reads packets from memory mapped I/O. The contract for the function which reads the packet into the state machine is then written in terms of ghost state modeling the stream of values written by the I/O to a volatile memory location which the function then reads:

/*@
  behavior theMacReadPacketBehavior:
    assumes theMac == &TheMac;
    ensures theMac->input == (char)injectorfgetCBuffer[injectorfgetCBufferCount-1];
*/
int read_packet(struct machine *theMac) {
  uint8_t c = *fgetC;
  theMac->input = (char)c;
  return ('a' <= c && c <= 'z');
}

The modeling of the stream of values is through the usual ghost functions:

volatile uint8_t *fgetC = (uint8_t *)INPUT_ADDRESS;
//@ ghost uint8_t injectorfgetCBuffer[256];
//@ ghost uint8_t injectorfgetCBufferCount;
/*@ ghost //@ requires fgetCArg == fgetC;
  @ uint8_t readfgetC(volatile uint8_t *fgetCArg) {
  @ for (int i=0; i<256; i++){
  @   injectorfgetCBuffer[i]=i;
  @ }
  @ if (fgetC == fgetCArg)
  @    return injectorfgetCBuffer[(injectorfgetCBufferCount++)%256];
  @ else
  @   return 0;
  @  }
  @ */
  //@ ghost uint8_t injectorfgetCCollector[256];
  //@ ghost uint8_t fgetCCollectorCount = 0;
  /*@ ghost //@ requires fgetCArg == fgetC;
  @ uint8_t writefgetC(volatile uint8_t *fgetCArg, uint8_t v) {
  @    if (fgetCArg == fgetC)
  @       return injectorfgetCCollector[(fgetCCollectorCount++)%256] = v;
  @    else
  @       return 0;
  @  }
  @*/
//@ volatile *fgetC reads readfgetC writes writefgetC;

Frama-C, of course, complains that this ghost function is missing an assigns, and so assumes this function assigns everything. None of the memory safety proof obligations may be proved.

All my guesses, based on the description in the ACSL-Manual of the syntax for comments within a ghost function, for the syntax for annotating the ghost contract fail to compile, and there are no examples. Any help would be invaluable!
Best wishes and regards,
Jon
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190109/96e34191/attachment.html>