Merge pull request #1248 from wandernauta/pvl-nil-enum

Prevent empty enums from being declared in PVL.
utwente-fmt · Oct 9, 2024 · 5f8de42 · 5f8de42
2 parents dc107f0 + d2c1d40
commit 5f8de42
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 4 deletions.
diff --git 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
@@ -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 }