do not emit permissions for final fields in pvl constructors

utwente-fmt · Oct 12, 2023 · 2968aaf · 2968aaf
1 parent cc36ff9
commit 2968aaf
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala b/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala
@@ -63,7 +63,7 @@ case class LangPVLToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
         ApplicableContract(
           UnitAccountedPredicate(tt),
           UnitAccountedPredicate(AstBuildHelpers.foldStar(cls.declarations.collect {
-            case field: InstanceField[Pre] =>
+            case field: InstanceField[Pre] if field.flags.collectFirst { case _: Final[Pre] => () }.isEmpty =>
               fieldPerm[Post](result, rw.succ(field), WritePerm())
           }) &* (if (checkRunnable) IdleToken(result) else tt)), tt, Nil, Nil, Nil, None,
         )(TrueSatisfiable)