--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on November 2018 ---
[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>