Lets wait with full parameterized syntax for now

utwente-fmt · Oct 13, 2023 · 477a6dd · 477a6dd
1 parent 2af1f53
commit 477a6dd
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 7 deletions.
diff --git a/src/parsers/vct/parsers/transform/PVLToCol.scala b/src/parsers/vct/parsers/transform/PVLToCol.scala
@@ -387,8 +387,8 @@ case class PVLToCol[G](override val originProvider: OriginProvider, override val
 
   def convert(implicit subject: SubjectContext): PVLCommunicateSubject[G] = subject match {
     case Subject0(name) => PVLThreadName(convert(name))
-    case Subject1(family, _, expr, _) => PVLIndexedFamilyName(convert(family), convert(expr))
-    case Subject2(family, _, binder, _, start, _, end, _) => PVLFamilyRange(convert(family), convert(binder), convert(start), convert(end))
+    case Subject1(family, _, expr, _) => ??(subject)
+    case Subject2(family, _, binder, _, start, _, end, _) => ??(subject)
   }
 
   def convert(implicit region: ParRegionContext): ParRegion[G] = region match {

diff --git a/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala b/src/rewrite/vct/rewrite/lang/LangPVLToCol.scala
@@ -10,11 +10,13 @@ import vct.col.rewrite.lang.LangSpecificToCol.{NotAValue, ThisVar}
 import vct.col.ref.Ref
 import vct.col.resolve.ctx.{BuiltinField, BuiltinInstanceMethod, ImplicitDefaultPVLConstructor, PVLBuiltinInstanceMethod, RefADTFunction, RefAxiomaticDataType, RefClass, RefEnum, RefEnumConstant, RefField, RefFunction, RefInstanceFunction, RefInstanceMethod, RefInstancePredicate, RefModel, RefModelAction, RefModelField, RefModelProcess, RefPVLConstructor, RefPredicate, RefProcedure, RefProverFunction, RefVariable, RefVeyMontThread}
 import vct.col.util.{AstBuildHelpers, SuccessionMap}
-import vct.result.VerificationError.SystemError
+import vct.result.VerificationError.{SystemError, UserError}
+import LangPVLToCol.CommunicateNotSupported
 
 case object LangPVLToCol {
-  case object CommunicateNotSupported extends SystemError {
+  case object CommunicateNotSupported extends UserError {
     override def text: String = "The `communicate` statement is not yet supported"
+    override def code: String = "communicateNotSupported"
   }
 }
 
@@ -166,6 +168,6 @@ case class LangPVLToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
   }
 
   def communicate(comm: PVLCommunicate[Pre]): VeyMontCommExpression[Post] = {
-    throw LangPVLToCol.CommunicateNotSupported
+    throw CommunicateNotSupported
   }
 }
diff --git a/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala b/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala
@@ -3,7 +3,7 @@ package vct.test.integration.examples
 import vct.test.integration.helper.VercorsSpec
 
 class TechnicalVeymontSpec extends VercorsSpec {
-  vercors should verify using silicon in "example using communicate" pvl
+  vercors should error withCode "communicateNotSupported" in "example using communicate" pvl
   """
      class Storage {
         int x;
@@ -20,7 +20,7 @@ class TechnicalVeymontSpec extends VercorsSpec {
      }
   """
 
-  vercors should verify using silicon in "parameterized sends not yet supported " pvl
+  vercors should error withCode "parseError" in "parameterized sends not yet supported " pvl
   """
     seq_program Example() {
       thread alice[10] = Storage();