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