From d2c1d40625f02837167df7a7a3a3ceca4a9196a6 Mon Sep 17 00:00:00 2001
From: Wander Nauta <info@wandernauta.nl>
Date: Mon, 7 Oct 2024 14:00:15 +0200
Subject: [PATCH] Disallow empty PVL enums in PVLToCol transform

An enum that does not define any enumeration constants is now a parse error.
---
 src/parsers/vct/parsers/transform/PVLToCol.scala          | 8 ++++----
 .../vct/test/integration/examples/TechnicalEnumSpec.scala | 8 ++++++++
 2 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/parsers/vct/parsers/transform/PVLToCol.scala b/src/parsers/vct/parsers/transform/PVLToCol.scala
index a4ecf4d03b..d3ebfc22dc 100644
--- a/src/parsers/vct/parsers/transform/PVLToCol.scala
+++ b/src/parsers/vct/parsers/transform/PVLToCol.scala
@@ -37,10 +37,10 @@ case class PVLToCol[G](
 
   def convert(implicit enum: EnumDeclContext): Enum[G] =
     enum match {
-      case EnumDecl0(_, name, _, constants, _, _) =>
-        new vct.col.ast.Enum[G](constants.map(convertConstants(_)).getOrElse(
-          Nil
-        ))(origin(enum).sourceName(convert(name)))
+      case EnumDecl0(_, name, _, Some(constants), _, _) =>
+        new vct.col.ast.Enum[G](convertConstants(constants))(origin(enum).sourceName(convert(name)))
+      case _ =>
+        fail(enum, "This enumeration must specify at least one constant")
     }
 
   def convertConstants(
diff --git a/test/main/vct/test/integration/examples/TechnicalEnumSpec.scala b/test/main/vct/test/integration/examples/TechnicalEnumSpec.scala
index af3ea60660..91518c1bbe 100644
--- a/test/main/vct/test/integration/examples/TechnicalEnumSpec.scala
+++ b/test/main/vct/test/integration/examples/TechnicalEnumSpec.scala
@@ -45,6 +45,14 @@ class Test {
     enum AB { A, B }
   """
 
+  vercors should error withCode "parseError" in "pvl/empty enum" pvl """
+    enum E { }
+  """
+
+  vercors should error withCode "parseError" in "pvl/empty enum with added comma" pvl """
+    enum E { , }
+  """
+
   vercors should verify using silicon in "pvl/enum return" pvl """
     enum AB { A, B }