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

  • Subject: [Frama-c-discuss] Assigns-clauses in preconditions and ghost variable assignment
  • From: rafael.bachmann.93 at gmail.com (Rafael Bachmann)
  • Date: Mon, 26 Nov 2018 17:49:09 +0100
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>