Salvage early resolve stuff and tests

utwente-fmt · Oct 18, 2023 · f2551d6 · f2551d6
1 parent 794cd4c
commit f2551d6
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 0 deletions.
diff --git a/src/col/vct/col/resolve/Resolve.scala b/src/col/vct/col/resolve/Resolve.scala
@@ -277,6 +277,11 @@ case object ResolveReferences extends LazyLogging {
     case cls: Class[G] => ctx
       .copy(currentThis=Some(RefClass(cls)))
       .declare(cls.declarations)
+    case seqProg: VeyMontSeqProg[G] => ctx
+      .copy(currentThis = Some(RefSeqProg(seqProg)))
+      .declare(seqProg.methods)
+      .declare(seqProg.threads)
+      .declare(seqProg.progArgs)
     case method: JavaMethod[G] => ctx
       .copy(currentResult=Some(RefJavaMethod(method)))
       .copy(inStaticJavaContext=method.modifiers.collectFirst { case _: JavaStatic[_] => () }.nonEmpty)
@@ -376,6 +381,8 @@ case object ResolveReferences extends LazyLogging {
       local.ref = Some(PVL.findName(name, ctx).getOrElse(throw NoSuchNameError("local", name, local)))
     case local@Local(ref) =>
       ref.tryResolve(name => Spec.findLocal(name, ctx).getOrElse(throw NoSuchNameError("local", name, local)))
+    case local@PVLThreadName(name) =>
+      local.ref = Some(PVL.findName(name, ctx).getOrElse(throw NoSuchNameError("VeyMont thread", name, local)))
     case local@TVar(ref) =>
       ref.tryResolve(name => Spec.findLocal(name, ctx).getOrElse(throw NoSuchNameError("type variable", name, local)))
     case funcOf@FunctionOf(v, vars) =>

diff --git a/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala b/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala
@@ -20,8 +20,29 @@ class TechnicalVeymontSpec extends VercorsSpec {
      }
   """
 
+  vercors should error withCode "noSuchName" in "non-existent thread name in communicate fails" pvl
+  """
+  seq_program Example() {
+     run {
+       communicate charlie.x <- charlie.x;
+     }
+  }
+  """
+
+  vercors should error withCode "???" in "non-existent field in communicate fails" pvl
+  """
+  class Storage { int x; }
+  seq_program Example() {
+     thread charlie = Storage();
+     run {
+       communicate charlie.nonExistent <- charlie.nonExistent;
+     }
+  }
+  """
+
   vercors should error withCode "parseError" in "parameterized sends not yet supported " pvl
   """
+    class Storage { int x; }
     seq_program Example() {
       thread alice[10] = Storage();
       thread bob[10] = Storage();