From 05e516fab34be85c8071971fb791dae05fe4daae Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 30 Sep 2024 18:49:52 +0200 Subject: [PATCH 1/2] add source tracking in VCGenerator --- .../scala/at/forsyte/apalache/tla/bmcmt/VCGenerator.scala | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/VCGenerator.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/VCGenerator.scala index 62945021c0..22ebc0c79f 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/VCGenerator.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/VCGenerator.scala @@ -67,6 +67,9 @@ class VCGenerator(tracker: TransformationTracker) extends LazyLogging { val notBody = tla.not(tla.fromTlaEx(copy.deepCopyEx(body))).typed(BoolT1) val negative = TlaOperDecl(NormalizedNames.VC_NOT_TRACE_INV_PREFIX + "0", params, notBody)(traceInv.typeTag) + // track the changes + tracker.hold(body, positive.body) + tracker.hold(body, negative.body) TlaModule(module.name, module.declarations :+ positive :+ negative) case Some(decl: TlaOperDecl) => @@ -166,7 +169,10 @@ class VCGenerator(tracker: TransformationTracker) extends LazyLogging { expr case (nameEx, set) :: tail => - decorateWithUniversals(tail, tla.forall(nameEx, set, expr).typed(BoolT1)) + val withForall = tla.forall(nameEx, set, expr).typed(BoolT1) + // remember the source of the change + tracker.hold(expr, withForall) + decorateWithUniversals(tail, withForall) } } } From 35b826bfe5d33d24eb45b1af7a9dd992b66e83c9 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 30 Sep 2024 21:07:32 +0200 Subject: [PATCH 2/2] add release notes --- .unreleased/bug-fixes/source-tracking-in-vcgen.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 .unreleased/bug-fixes/source-tracking-in-vcgen.md diff --git a/.unreleased/bug-fixes/source-tracking-in-vcgen.md b/.unreleased/bug-fixes/source-tracking-in-vcgen.md new file mode 100644 index 0000000000..04e361c2de --- /dev/null +++ b/.unreleased/bug-fixes/source-tracking-in-vcgen.md @@ -0,0 +1 @@ +Fix source tracking in `VCGenerator` to avoid spurious diagnostic messages, see #3010