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