generateSingleOwnerPermissions fails with classes containing final fields

[wandernauta]

With the --generate-permissions flag enabled, the following Java program causes VerCors to crash with a transformation check error:

class Numbers {
    int big() {
        return Integer.MAX_VALUE;
    }
}

The generateSingleOwnerPermissions rewrite seems to generate a write permission for the constructor of the Integer class to write to its final static int fields, which is not allowed (and I think not needed).

vct.main.stages.Transformation$TransformationCheckError: The generateSingleOwnerPermissions rewrite caused the AST to no longer typecheck:
======================================
43     final int max_value;
   44     
                      [--------------
   45     ensures Perm(this.min_value, write);
                       --------------]
   46     ensures Perm(this.max_value, write);
   47     constructor() {
--------------------------------------
[1/1] Specifying permission over final fields is not allowed, since they are treated as constants.
======================================
======================================
44     
   45     ensures Perm(this.min_value, write);
                      [--------------
   46     ensures Perm(this.max_value, write);
                       --------------]
   47     constructor() {
   48
--------------------------------------
[1/1] Specifying permission over final fields is not allowed, since they are treated as constants.
======================================
	at vct.main.stages.Transformation.$anonfun$run$4(Transformation.scala:263)
	at vct.main.stages.Transformation.$anonfun$run$4$adapted(Transformation.scala:238)
	at hre.progress.Progress$.$anonfun$foreach$2(Progress.scala:25)
	at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
	at hre.progress.task.AbstractTask.frame(AbstractTask.scala:166)
	at hre.progress.Progress$.$anonfun$foreach$1(Progress.scala:25)
	at hre.progress.Progress$.$anonfun$foreach$1$adapted(Progress.scala:24)
	at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
	at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
	at scala.collection.AbstractIterator.foreach(Iterator.scala:1300)
	at hre.progress.Progress$.foreach(Progress.scala:24)
	at vct.main.stages.Transformation.$anonfun$run$2(Transformation.scala:238)
	at hre.debug.TimeTravel$.safelyRepeatable(TimeTravel.scala:32)
	at vct.main.stages.Transformation.run(Transformation.scala:232)
	at vct.main.stages.Transformation.run(Transformation.scala:205)
	at hre.stages.Stages.$anonfun$run$3(Stages.scala:104)
	at hre.stages.Stages.$anonfun$run$3$adapted(Stages.scala:101)
	at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
	at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
	at scala.collection.AbstractIterable.foreach(Iterable.scala:933)
	at scala.collection.IterableOps$WithFilter.foreach(Iterable.scala:903)
	at hre.stages.Stages.$anonfun$run$1(Stages.scala:101)
	at hre.progress.task.NameSequenceTask.scope(NameSequenceTask.scala:16)
	at hre.progress.Progress$.stages(Progress.scala:47)
	at hre.stages.Stages.run(Stages.scala:98)
	at hre.stages.Stages.run$(Stages.scala:95)
	at hre.stages.StagesPair.run(Stages.scala:145)
	at vct.main.modes.Verify$.verifyWithOptions(Verify.scala:64)
	at vct.main.modes.Verify$.$anonfun$runOptions$3(Verify.scala:99)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.util.Time$.logTime(Time.scala:23)
	at vct.main.modes.Verify$.runOptions(Verify.scala:99)
	at vct.main.Main$.runMode(Main.scala:107)
	at vct.main.Main$.$anonfun$runOptions$3(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.middleware.Middleware$.using(Middleware.scala:78)
	at vct.main.Main$.$anonfun$runOptions$2(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.io.Watch$.booleanWithWatch(Watch.scala:58)
	at vct.main.Main$.$anonfun$runOptions$1(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.middleware.Middleware$.using(Middleware.scala:78)
	at vct.main.Main$.runOptions(Main.scala:95)
	at vct.main.Main$.main(Main.scala:50)
	at vct.main.Main.main(Main.scala)
[ERROR] !*!*!*!*!*!*!*!*!*!*!*!
[ERROR] ! VerCors has crashed !
[ERROR] !*!*!*!*!*!*!*!*!*!*!*!

[bobismijnnaam]

You are correct, that pass should not generate any permissions for static final fields, those are managed by the static final encoder itself. It would be fine to throw a regular not supported error, though actually implementing proper behaviour here shouldn't be too much work either.