diff --git a/examples/technical/javabip/BipGuardUnsatisfiablePrecondition.java b/examples/technical/javabip/BipGuardPreconditionUnsatisfiable.java similarity index 100% rename from examples/technical/javabip/BipGuardUnsatisfiablePrecondition.java rename to examples/technical/javabip/BipGuardPreconditionUnsatisfiable.java index 34b91ccfba..a93dfc8f29 100644 --- a/examples/technical/javabip/BipGuardUnsatisfiablePrecondition.java +++ b/examples/technical/javabip/BipGuardPreconditionUnsatisfiable.java @@ -20,11 +20,11 @@ public class GuardIsUsed { } @Pure - @Guard(name = GEQ_Y) /*[/expect bipGuardPreconditionUnsatisfiable]*/ + @Guard(name = GEQ_Y) + /*[/end]*/ public boolean geqZero() { return true; } - /*[/end]*/ } /*[/end]*/ diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index 7c47dfe00d..7e55d166d9 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -1131,7 +1131,7 @@ final class BipTransition[G](val signature: BipTransitionSignature[G], val data: Seq[Ref[G, BipIncomingData[G]]], val guard: Expr[G], val requires: Expr[G], val ensures: Expr[G], val body: Statement[G] )(val blame: Blame[BipTransitionFailure])(implicit val o: Origin) extends ClassDeclaration[G] with BipTransitionImpl[G] -final class BipGuard[G](val data: Seq[Ref[G, BipIncomingData[G]]], val body: Statement[G], val pure: Boolean)(val blame: Blame[BipGuardNontrivialUnsatisfiable])(implicit val o: Origin) extends ClassDeclaration[G] with BipGuardImpl[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 constructors: Seq[Ref[G, Procedure[G]]], val invariant: Expr[G], val initial: Ref[G, BipStatePredicate[G]])(implicit val o: Origin) extends ClassDeclaration[G] with BipComponentImpl[G] diff --git a/src/col/vct/col/origin/Blame.scala b/src/col/vct/col/origin/Blame.scala index a13b27692e..303c30f1c3 100644 --- a/src/col/vct/col/origin/Blame.scala +++ b/src/col/vct/col/origin/Blame.scala @@ -682,8 +682,8 @@ case class BipOutgoingDataPreconditionUnsatisfiable(node: BipOutgoingData[_]) ex override def inlineDescWithSource(source: String): String = s"Precondition unsatisfiable for outgoing data `$source`" } -case class BipGuardNontrivialUnsatisfiable(node: BipGuard[_]) extends NodeVerificationFailure { - override def code: String = "bipGuardNontrivialUnsatisfiable" +case class BipGuardPreconditionUnsatisfiable(node: BipGuard[_]) extends JavaAnnotationFailure with NodeVerificationFailure { + override def code: String = "bipGuardPreconditionUnsatisfiable" override def descInContext: String = "The precondition of this guard (consisting of only the component invariant) is unsatisfiable" override def inlineDescWithSource(source: String): String = s"Precondition unsatisfiable for guard `$source`" } diff --git a/src/col/vct/col/resolve/lang/Java.scala b/src/col/vct/col/resolve/lang/Java.scala index b60168d399..b81a8cbdc6 100644 --- a/src/col/vct/col/resolve/lang/Java.scala +++ b/src/col/vct/col/resolve/lang/Java.scala @@ -521,10 +521,10 @@ case object JavaAnnotationData { final case class BipData[G](name: String)(implicit val o: Origin) extends JavaAnnotationData[G] case object BipGuard { - def get[G](m: JavaMethod[G]): Option[BipGuard[G]] = + def get[G](m: JavaMethod[G]): Option[JavaAnnotation[G]] = m.modifiers - .collect { case ja @ JavaAnnotation(_, _) if ja.data.isDefined => ja.data.get } - .collectFirst { case b: BipGuard[G] => b } + .collect { case ja @ JavaAnnotation(_, _) => (ja, ja.data) } + .collectFirst { case (ja, Some(_: BipGuard[G])) => ja } def getName[G](method: JavaMethod[G]): Option[Expr[G]] = method.modifiers.collectFirst { diff --git a/src/rewrite/vct/rewrite/bip/EncodeBip.scala b/src/rewrite/vct/rewrite/bip/EncodeBip.scala index 59c8a6b8f3..c2be9d9c18 100644 --- a/src/rewrite/vct/rewrite/bip/EncodeBip.scala +++ b/src/rewrite/vct/rewrite/bip/EncodeBip.scala @@ -46,7 +46,7 @@ case object EncodeBip extends RewriterBuilderArg[VerificationResults] { } case ctx: SignalsFailed => PanicBlame("BIP transition does not have signals").blame(ctx) case ctx: ExceptionNotInSignals => PanicBlame("BIP transition does not have signals").blame(ctx) - case _: BipConstructorFailure | _: BipTransitionFailure | _: BipGuardFailure => PanicBlame("This error never occurs in the encoding, so why is it under CallableFailure?").blame(error) + case _: BipConstructorFailure | _: BipTransitionFailure => PanicBlame("This error never occurs in the encoding, so why is it under CallableFailure?").blame(error) } } @@ -69,7 +69,7 @@ case object EncodeBip extends RewriterBuilderArg[VerificationResults] { } case ctx: SignalsFailed => proc.blame.blame(ctx) case ctx: ExceptionNotInSignals => proc.blame.blame(ctx) - case _: BipConstructorFailure | _: BipTransitionFailure | _: BipGuardFailure => PanicBlame("This error never occurs in the encoding, so why is it under CallableFailure?").blame(error) + case _: BipConstructorFailure | _: BipTransitionFailure =>PanicBlame("This error never occurs in the encoding, so why is it under CallableFailure?").blame(error) } } diff --git a/src/rewrite/vct/rewrite/lang/LangBipToCol.scala b/src/rewrite/vct/rewrite/lang/LangBipToCol.scala index 3809fc1d66..80204fbb21 100644 --- a/src/rewrite/vct/rewrite/lang/LangBipToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangBipToCol.scala @@ -164,7 +164,8 @@ case class LangBipToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L } def rewriteGuard(m: JavaMethod[Pre]): Unit = { - val jad.BipGuard(_) = jad.BipGuard.get(m).get + val annotation = jad.BipGuard.get(m).get + val Some(jad.BipGuard(_)) = annotation.data if (m.returnType != TBool[Pre]()) { throw LangBipToCol.WrongGuardReturnType(m) } @@ -172,7 +173,7 @@ case class LangBipToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L m.parameters.map(rewriteParameter), rw.dispatch(m.body.get), true - )(m.blame)(SourceNameOrigin(m.name, m.o))) + )(annotation.blame)(SourceNameOrigin(m.name, m.o))) } def rewriteOutgoingData(m: JavaMethod[Pre]): Unit = { diff --git a/test/main/vct/test/integration/examples/TechnicalJavaBipSpec.scala b/test/main/vct/test/integration/examples/TechnicalJavaBipSpec.scala index 97869a8841..43bdfb6b52 100644 --- a/test/main/vct/test/integration/examples/TechnicalJavaBipSpec.scala +++ b/test/main/vct/test/integration/examples/TechnicalJavaBipSpec.scala @@ -37,7 +37,7 @@ class TechnicalJavaBipSpec extends JavaBipSpecHelper { "technical/javabip/TransitionPostconditionFailed.java", ) - vercors should verify using silicon example "technical/javabip/BipGuardUnsatisfiablePrecondition.java" + vercors should verify using silicon example "technical/javabip/BipGuardPreconditionUnsatisfiable.java" vercors should verify using silicon example "technical/javabip/BipGuardUsed.java" vercors should verify using silicon example "technical/javabip/BipGuardDataUsed.java" }