Refute: bad framing

This example complains about the body of the `frame_error` method being unreachable due to the fact that its contract is mal-formed.

General information

ID134
Articlenone
Back-endSilicon
LanguagePVL
Features
Sources
Path to example filerefute/frame_error_1.pvl
Date2017-06-20

Statistical information

Lines of code6 lines (comments not included)
Lines of specification1 lines (16.67% of the total)
Computation time17853 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.