Make sure bip constructor arguments are declared

utwente-fmt · Oct 12, 2023 · 9867f86 · 9867f86
1 parent b7f4212
commit 9867f86
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 3 deletions.
diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala
@@ -1134,7 +1134,7 @@ final class BipTransition[G](val signature: BipTransitionSignature[G],
 final class BipGuard[G](val data: Seq[Ref[G, BipIncomingData[G]]], val body: Statement[G], val pure: Boolean)(val blame: Blame[BipGuardPreconditionUnsatisfiable])(implicit val o: Origin) extends ClassDeclaration[G] with BipGuardImpl[G]
 final case class BipGuardInvocation[G](obj: Expr[G], guard: Ref[G, BipGuard[G]])(implicit val o: Origin) extends Expr[G] with BipGuardInvocationImpl[G]
 final class BipComponent[G](val fqn: Seq[String], val invariant: Expr[G], val initial: Ref[G, BipStatePredicate[G]])(implicit val o: Origin) extends ClassDeclaration[G] with BipComponentImpl[G]
-final class BipConstructor[G](val args: Seq[Variable[G]], val body: Statement[G], val requires: Expr[G])(val blame: Blame[BipConstructorFailure])(implicit val o: Origin) extends ClassDeclaration[G] with BipConstructorImpl[G]
+final class BipConstructor[G](val args: Seq[Variable[G]], val body: Statement[G], val requires: Expr[G])(val blame: Blame[BipConstructorFailure])(implicit val o: Origin) extends ClassDeclaration[G] with Declarator[G] with BipConstructorImpl[G]
 
 final class BipPort[G](val t: BipPortType[G])(implicit val o: Origin) extends ClassDeclaration[G] with BipPortImpl[G]
 sealed trait BipPortType[G] extends NodeFamily[G]

diff --git a/src/col/vct/col/ast/declaration/cls/BipConstructorImpl.scala b/src/col/vct/col/ast/declaration/cls/BipConstructorImpl.scala
@@ -1,7 +1,7 @@
 package vct.col.ast.declaration.cls
 
-import vct.col.ast.{BipConstructor, Type, Variable}
+import vct.col.ast.{BipConstructor, Declaration, Type, Variable}
 
 trait BipConstructorImpl[G] { this: BipConstructor[G] =>
-
+  override def declarations: Seq[Declaration[G]] = args
 }
diff --git a/test/main/vct/test/integration/examples/JavaBipSpec.scala b/test/main/vct/test/integration/examples/JavaBipSpec.scala
@@ -17,6 +17,9 @@ class JavaBipSpec extends JavaBipSpecHelper {
     "concepts/javabip/casinoBroken/Casino.java",
     "concepts/javabip/casinoBroken/Operator.java",
   )
+  /*
+    concepts/javabip/casinoBroken/Main.java concepts/javabip/casinoBroken/Constants.java concepts/javabip/casinoBroken/Player.java concepts/javabip/casinoBroken/Casino.java concepts/javabip/casinoBroken/Operator.java
+  * */
 
   passingTest("concepts/javabip/casinoAdjusted/casinoAdjusted.json",
     "concepts/javabip/casinoAdjusted/Main.java",