Very simple verification case where a `Perm` predicate is transformed into a `PointsTo` predicate, after assignment of a value to the reference protected by the predicate.
|Path to example file||permissions/box.pvl|
|Lines of code||16 lines (comments not included)|
|Lines of specification||5 lines (31.25% of the total)|
|Computation time||8522 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.