From 2968aaf105af5f7cc23c5f003f43e8ba1ca38fc9 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Thu, 12 Oct 2023 10:13:06 +0200 Subject: [PATCH] do not emit permissions for final fields in pvl constructors --- src/rewrite/vct/rewrite/lang/LangPVLToCol.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala b/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala index 6c606ae991..d961345e7d 100644 --- 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)