--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on January 2019 ---
[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