Verifying goto (failing)

Failing verification example in which a program is verified that uses goto's and labels.

General information

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

Statistical information

Lines of code14 lines (comments not included)
Lines of specification2 lines (14.29% of the total)
Computation time18043 milliseconds

Example code

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