Email Gateway (Aug 22 2022 at 09:00): Email Gateway (Aug 22 2022 at 09:00):From: scott constable <sdconsta@syr.edu>
Hi All,
When importing a function containing static variable(s), AutoCorres
instantiates each static variable to "unknown", making it very difficult to
reason about functions whose correctness depends on those static variables.
For instance, I have a function, out_char(), which uses a static variable
"col" to track which column on the screen will be printed to next. Once
"col" reaches 80, it wraps around by resetting to 0. So it would be nice to
be able to prove, among other things, that "col" will never leave the
interval [0..80].
Many thanks in advance,
~Scott Constable
Email Gateway (Aug 22 2022 at 09:05):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Hi Scott,
the problem is less with AutoCorres, more with the C-to-Isabelle parser underneath: it currently doesn’t properly handle function static variables.
As a quick workaround, you might want to put that variable into a global instead, while we’re looking at this more deeply.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 09:06):From: scott constable <sdconsta@syr.edu>
Thank you Gerwin. Using a global variable instead was the fallback plan
anyway. I don't believe that this limitation is mentioned in the current C
parser documentation, i.e. the document titled "Translation of the StrictC
dialect."
~Scott
Email Gateway (Aug 22 2022 at 09:06):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Yes. I hope we can just support it and don’t have to fix the manual ;-)
Cheers,
Gerwin
Last updated: Apr 20 2024 at 12:26 UTC