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] [EXTERNAL] Re: Annotating Ghost Contracts

Hi Loic,
    Thanks for your speedy reply! I failed to be clear. The required ACSL statements were clear to us, our question was where to put them- thus far, our guesses have all provoked syntax errors.  We've tried:

1)
//@ ghost uint8_t injectorfgetCBuffer[256];                                                                                                                                           
 //@ ghost uint8_t injectorfgetCBufferCount;                                                                                                                                          
//@ assigns injectorfgetCBufferCount;                                                                                                                                                 
//@ assigns injectorfgetCBuffer;                                                                                                                                                      
 /*@ ghost //@ requires fgetCArg == fgetC;                                                                                                                                            
  @ uint8_t readfgetC(volatile uint8_t *fgetCArg) {                                                                                                                                   
  . . . . . . . . . . 
2) 
//@ assigns injectorfgetCBufferCount;                                                                                                                                                 
//@ assigns injectorfgetCBuffer;                                                                                                                                                      
//@ ghost uint8_t injectorfgetCBuffer[256];                                                                                                                                           
 //@ ghost uint8_t injectorfgetCBufferCount;                                                                                                                                          
 /*@ ghost //@ requires fgetCArg == fgetC;                                                                                                                                            
  @ uint8_t readfgetC(volatile uint8_t *fgetCArg) {     
. . . . . . . . . .

3) //@ ghost uint8_t injectorfgetCBuffer[256];                                                                                                                                           
 //@ ghost uint8_t injectorfgetCBufferCount;                                                                                                                                          
 /*@ ghost //@ requires fgetCArg == fgetC;                                                                                                                                            
   ghost //@ assigns injectorfgetCBufferCount;                                                                                                                                        
   ghost //@ assigns injectorfgetCBuffer;                                                                                                                                             
  @ uint8_t readfgetC(volatile uint8_t *fgetCArg) {          
.. . . . . . . 

These all provoke responses like:
[kernel] stm.c:15:
  syntax error:
  Location: between lines 15 and 17
  13    volatile uint8_t *fgetC = (uint8_t *)INPUT_ADDRESS;
  14    //@ ghost uint8_t injectorfgetCBuffer[256];

  15     //@ ghost uint8_t injectorfgetCBufferCount;
  16    //@ assigns injectorfgetCBufferCount;
  17    //@ assigns injectorfgetCBuffer;

  18     /*@ ghost //@ requires fgetCArg == fgetC;
  19      @ uint8_t readfgetC(volatile uint8_t *fgetCArg) {
[kernel] Frama-C aborted: invalid user input.


On 1/10/19, 1:54 AM, "Frama-c-discuss on behalf of Loïc Correnson" <frama-c-discuss-bounces at lists.gforge.inria.fr on behalf of loic.correnson at cea.fr> wrote:

    Hi Jon,
    
    You simply shall add assigns like requires, assumes and such, like this:
    « //@ assigns injectorfgetCBufferCount ; »
    
    	L.
    
    
    
    
    > Le 9 janv. 2019 à 19:58, Aytac, Jon M <jmaytac at sandia.gov> a écrit :
    > 
    > 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
    > _______________________________________________
    > Frama-c-discuss mailing list
    > Frama-c-discuss at lists.gforge.inria.fr
    > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
    
    _______________________________________________
    Frama-c-discuss mailing list
    Frama-c-discuss at lists.gforge.inria.fr
    https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss