diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index f3976a3900..1f1b171c40 100644 --- 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 index 0b2c820222..ba82282e61 100644 --- 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 index 8e2beb23d6..38015a9f7f 100644 --- 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",