--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on January 2019 ---
Hello, Le sam. 12 janv. 2019 à 04:06, Aytac, Jon M <jmaytac at sandia.gov> a écrit : > 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: > > [...] > 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. > > > The main issue is that //@ is a one-line annotation meaning that Frama-C will see the two assigns and the requires as three separate contracts, two of them missing a function to be attached to. Since Frama-C 17 Chlorine, it is possible to write multi-line annotations within ghost code, through /@ ... @/, as described in the ACSL manual. Your function contract could thus be written as such: /*@ ghost /@ requires fgetCArg == fgetC; assigns injectorfgetCBufferCount; assigns injectorfgetCBuffer[0 .. 255]; @/ uint8_t writefgetC(volatile uint8_t *fgetCArg, uint8_t v) { .... } */ Best regards, -- E tutto per oggi, a la prossima volta Virgile -------------- section suivante -------------- Une pièce jointe HTML a été nettoyée... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190114/9ef1be22/attachment.html>