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



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?

Thanks very much,

Rafael Bachmann
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181126/6147b021/attachment.html>