--- layout: fc_discuss_archives title: Message 5 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



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>