Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>