From b84033b52e0c7f8d26deb08a5d46ed83c68cbad1 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Fri, 23 Jan 2026 23:44:40 +0800 Subject: [PATCH] adds a hook to print the SIF-encoded AST --- .../viper/silver/plugin/sif/SIFExtendedTransformer.scala | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/plugin/sif/SIFExtendedTransformer.scala b/src/main/scala/viper/silver/plugin/sif/SIFExtendedTransformer.scala index 804ce7158..b2d37ed94 100644 --- a/src/main/scala/viper/silver/plugin/sif/SIFExtendedTransformer.scala +++ b/src/main/scala/viper/silver/plugin/sif/SIFExtendedTransformer.scala @@ -51,6 +51,11 @@ trait SIFExtendedTransformer { var enableNaginiSpecificFeatures: Boolean = false /** Function to be called when errors are encountered. Prints to stdout by default. */ var reportError: AbstractError => Unit = defaultReportError + /** + * Optional callback that is invoked after applying the SIF transformation, which can be used to print the AST for + * debugging purposes + */ + var transformedProgramCallback: Option[Program => Unit] = None } def optimizeControlFlow(v: Boolean): Unit = { Config.optimizeControlFlow = v @@ -234,8 +239,10 @@ trait SIFExtendedTransformer { p.methods.map(m => translateMethod(m)) } - p.copy(domains = newDomains, fields = productFields, functions = newFunctions, predicates = newPredicates, + val res = p.copy(domains = newDomains, fields = productFields, functions = newFunctions, predicates = newPredicates, methods = newMethods)(p.pos, p.info, p.errT) + Config.transformedProgramCallback.foreach(fn => fn(res)) + res } // TODO REM: depends on the results of relationalPredicates