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] Assigns-clauses in preconditions and ghost variable assignment

Hello,

Le lun. 26 nov. 2018 à 17:49, Rafael Bachmann <rafael.bachmann.93 at gmail.com>
a écrit :

> Hi,
> while verifying the following function, it occurred to me that WP
> considers assignments to ghost variables to be regular assignments, i.e. a
> function which only assigns ghost variables cannot fulfil the property
> "assigns \nothing":
>
>
> //@ ghost int interrupt_status = INTERRUPTS_ON;
>
> /*@ ensures interrupt_status == INTERRUPTS_ON;
>    assigns interrupt_status; */
> void interrupts_on() {
>    //@ ghost interrupt_status = INTERRUPTS_ON;
> }
>
> I would have assumed that assignment of a ghost variable does not have an
> effect on the actual implementation of the function, and hence should not
> count as assignment.
>
> Is this behaviour intentional? If so, is there a workaround or a
> recommended different strategy?
>
>
I'm afraid you won't get an answer that differs much from the one made on
stackoverflow over a very similar topic:
https://stackoverflow.com/a/53378028/1633665

In essence, yes this is the intended behavior. `assigns` clause are meant
to list all locations, be they ghost or not, that might be modified during
a function call. In fact, Example 2.62 of the manual at
https://github.com/acsl-language/acsl/releases/download/v1.13%2BChlorine/acsl_1.13.pdf
shows an example of function with an assigns clause (note however that it
won't compile with current Frama-C releases as ghost variables with a
purely ACSL type are not supported by the implementation yet). What the
discussion in section 2.12 of the document is about concerns the fact that
ghost statements must not interfere with regular statements (although this
is not checked by the current implementation), but if they do modify ghost
memory locations that are globally accessible, this must appear in the
assigns clause, along with the regular memory locations that are modified
by regular statements.

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/20181126/7bb27953/attachment.html>