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