Last bit to support predicates as well

utwente-fmt · Sep 24, 2024 · 7becf37 · 7becf37
1 parent 6bdcd89
commit 7becf37
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala b/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala
@@ -331,7 +331,9 @@ case class EncodePermissionStratification[Pre <: Generation](
         }
 
       case cp: ChorPerm[Pre] =>
-        ??? // Unexpected chorperm with something else than a FieldLocation
+        specializing.having(EndpointName[Post](succ(cp.endpoint.decl))(cp.o)) {
+          Perm(dispatch(cp.loc), dispatch(cp.perm))(expr.o)
+        }
 
       case Perm(loc: FieldLocation[Pre], perm) if specializing.nonEmpty =>
         makeWrappedPerm(loc, perm, specializing.top)(expr.o)