Only allow precondition on javabip constructors

utwente-fmt · Oct 10, 2023 · 7092c6e · 7092c6e
1 parent 38f0bb4
commit 7092c6e
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/src/rewrite/vct/rewrite/lang/LangBipToCol.scala b/src/rewrite/vct/rewrite/lang/LangBipToCol.scala
@@ -176,7 +176,8 @@ case class LangBipToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
 
   def rewriteConstructor(constructor: JavaConstructor[Pre], annotation: JavaAnnotation[Pre], data: jad.BipComponent[Pre]): Unit = {
     implicit val o: Origin = constructor.o
-    val contractWithoutRequires = constructor.contract.copy(requires = UnitAccountedPredicate(tt))()
+    val contractWithoutRequires = constructor.contract.copy(requires = UnitAccountedPredicate[Pre](tt))(
+      blame = constructor.contract.blame)(o = constructor.o)
     if (contractWithoutRequires.nonEmpty) {
       throw ImproperConstructor(constructor, "Only precondition is allowed on JavaBIP component constructors")
     }

diff --git a/src/rewrite/vct/rewrite/lang/LangJavaToCol.scala b/src/rewrite/vct/rewrite/lang/LangJavaToCol.scala
@@ -4,7 +4,7 @@ import com.typesafe.scalalogging.LazyLogging
 import hre.util.{FuncTools, ScopedStack}
 import vct.col.ast._
 import vct.col.rewrite.lang.LangSpecificToCol.{NotAValue, ThisVar}
-import vct.col.origin.{AbstractApplicable, Blame, CallableFailure, ContextEverywhereFailedInPost, ContractedFailure, DerefPerm, ExceptionNotInSignals, JavaArrayInitializerBlame, JavaConstructorPostconditionFailed, Origin, PanicBlame, PostBlameSplit, SignalsFailed, SourceNameOrigin, TerminationMeasureFailed, TrueSatisfiable}
+import vct.col.origin.{AbstractApplicable, Blame, CallableFailure, ContextEverywhereFailedInPost, ContractedFailure, DerefPerm, ExceptionNotInSignals, JavaArrayInitializerBlame, JavaConstructorPostconditionFailed, Origin, PanicBlame, PostBlameSplit, PostconditionFailed, SignalsFailed, SourceNameOrigin, TerminationMeasureFailed, TrueSatisfiable}
 import vct.col.ref.{LazyRef, Ref}
 import vct.col.resolve.ctx._
 import vct.col.rewrite.{Generation, Rewritten}
@@ -268,7 +268,7 @@ case class LangJavaToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends
       case method: JavaMethod[Pre] =>
         // For each javabip annotation that we encounter, execute a rewrite
         val results = method.modifiers.collect {
-          case annotation @ JavaAnnotationEx(_, _, guard @ JavaAnnotationData.BipGuard(_)) =>
+          case annotation @ JavaAnnotationEx(_, _, guard: JavaAnnotationData.BipGuard[Pre]) =>
             rw.bip.rewriteGuard(method, annotation, guard)
           case annotation @ JavaAnnotationEx(_, _, transition : JavaAnnotationData.BipTransition[Pre]) =>
             rw.bip.rewriteTransition(method, annotation, transition)