Robustness of code (Identify properties to be verified during code verification)

[MarcBehrens]

Identify properties to be verified during code verification see #53

Possible properties for fomal verification

• [ ] Robustness of code (for later sprints)

[ghost]

As explained for #58, we use case distinctions in the formal function contracts of Bitwalker's Peek and Poke functions. There are cases

• for the out of range behavior for both functions and
• for the behavior if the value to write is too big (Poke only).

In addition, we use WP's rte-option to insert assertions about the absence of run time errors.

[MarcBehrens]

Static analysis on the bitwalker code with

• [x] RSM (e.g. MISRA rules) planned by @idelatorre
• [x] Frama-C planned by @vprevosto

[BerndHekele]

RSM has been performed by SQS and can be found here: c56505e3f5a45291e2fcc9de3867c40fb505d273

[MarcBehrens]

@vprevosto any updates here?

[jensgerlach]

Peek and Poke have been (mostly) verified w.r.t. robustness.