Verifying goto (succeeding)

Verifying example with goto's and labels. We verify a program with goto's to skip certain code fragments, and show that these fragments do not update the code in some way.

General information

ID69
Articlenone
Back-endSilicon
LanguagePVL
FeaturesGoto
Sources
Path to example filegoto/goto2.pvl
Date2017-06-19

Statistical information

Lines of code16 lines (comments not included)
Lines of specification2 lines (12.5% of the total)
Computation time17038 milliseconds

Example code

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