MPS: specs for most of instrumentation component #61
Conversation
| @@ -147,6 +204,8 @@ int instrumentation_step(uint8_t div, struct instrumentation_state *state) { | |||
|
|
|||
There was a problem hiding this comment.
instrumentation_step takes a really long time to verify. I have this file pulled out and am reducing it.
|
I'll fix the frama-c failure |
There was a problem hiding this comment.
Very nice, thanks for the good work!
I have only one request: please turn (or reference) every comment you mentioned in this PR into a VERSE-Toolchain issue, such that your experience is highlighted to the TA1 team and they can appropriately prioritize.
Apparently we cannot share OpenSUT code yet, hence the VERSE-Toolchain issue, vs. a CN issue.
| #define NMODES 3 | ||
| /*$ function (u8) NMODES() $*/ | ||
| static | ||
| uint8_t c_NMODES() /*$ cn_function NMODES; $*/ { return NMODES; } |
There was a problem hiding this comment.
Does this syntax cn_function NMODES; literally say *this is an implementation of function (u8) NMODES()?
There was a problem hiding this comment.
Yes. We need this to move the NMODES definition from the preprocessor into CN for now.
|
@peterohanley looks like the CN proofs are failing on the |
peterohanley
force-pushed
the
11-implement-mps
branch
from
3a69f86 to
c70b1e2
Compare
|
Notes about CN experience added to #98 |
There is still one function in instrumentation.c that has a construct that cn is not yet happy with.
instrumentation_steptakes a very long time to verify. The well-formed constraint for state.modes has to be passed around explicitly in too many places, some of which could be removed.Describe your changes
Specs for instrumentation_common.c and most of instrumentation.c
Issue ticket number and link
#11
Checklist before requesting a review