Add beginning of class type type checking

utwente-fmt · Oct 18, 2023 · 3fad843 · 3fad843
1 parent 9686116
commit 3fad843
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala
@@ -1758,7 +1758,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
             JavaVariableDeclaration(name, dims, Some(coerce(v, FuncTools.repeat[Type[Pre]](TArray(_), dims, declaration.t))))
         })
       case seqProg: SeqProg[Pre] => seqProg
-      case thread: VeyMontThread[Pre] => thread
+      case thread: VeyMontThread[Pre] => new VeyMontThread(cls(thread.threadType), thread.args)
       case bc: BipConstructor[Pre] => new BipConstructor(bc.args, bc.body, bc.requires)(bc.blame)
       case bc: BipComponent[Pre] =>
         new BipComponent(bc.fqn, res(bc.invariant), bc.initial)

diff --git a/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala b/test/main/vct/test/integration/examples/TechnicalVeymontSpec.scala
@@ -40,6 +40,13 @@ class TechnicalVeymontSpec extends VercorsSpec {
   }
   """
 
+  vercors should error withCode "???" in "thread types should also be classlike" pvl
+  """
+  seq_program Example() {
+     int charlie = 3;
+  }
+  """
+
   vercors should error withCode "parseError" in "parameterized sends not yet supported " pvl
   """
     class Storage { int x; }