--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on January 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Annotating Ghost Contracts



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