Getting Started
Installation Guide
Tutorial
Issue Tracker
Tools
Verifier
Alpinist
VeSUV
VeyMont
Showcases
Publications
About
VerCors Team
News
Contact
Credits
License
Verifying goto (failing)
Failing verification example in which a program is verified that uses goto's and labels.
General Information
Backend
: Silicon
Language
: PVL
Features
: Goto
Path to Example File
: goto/goto1.pvl
Should Verify
: No
Date
: 2017-06-19
Lines of Code
: 14 (comments not included)
Lines of Specification
: 2 (14.3% of total)
Computation Time
: 18.0 seconds
// -*- tab-width:2 ; indent-tabs-mode:nil -*- //:: cases Goto1 //:: tools silicon carbon //:: verdict Fail class Ref { requires n > 0; ensures \result > 0; int t1(int n){ int r; goto lbl; r = n; label lbl; return r; } }
Language:
PVL
Java
Cuda
C / OpenMP / OpenCL
Viper