Skip to content

Commit c82b28d

Browse files
authored
adds a hook to print the SIF-encoded AST (#900)
1 parent 80e4de2 commit c82b28d

1 file changed

Lines changed: 8 additions & 1 deletion

File tree

src/main/scala/viper/silver/plugin/sif/SIFExtendedTransformer.scala

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,11 @@ trait SIFExtendedTransformer {
5151
var enableNaginiSpecificFeatures: Boolean = false
5252
/** Function to be called when errors are encountered. Prints to stdout by default. */
5353
var reportError: AbstractError => Unit = defaultReportError
54+
/**
55+
* Optional callback that is invoked after applying the SIF transformation, which can be used to print the AST for
56+
* debugging purposes
57+
*/
58+
var transformedProgramCallback: Option[Program => Unit] = None
5459
}
5560
def optimizeControlFlow(v: Boolean): Unit = {
5661
Config.optimizeControlFlow = v
@@ -234,8 +239,10 @@ trait SIFExtendedTransformer {
234239
p.methods.map(m => translateMethod(m))
235240
}
236241

237-
p.copy(domains = newDomains, fields = productFields, functions = newFunctions, predicates = newPredicates,
242+
val res = p.copy(domains = newDomains, fields = productFields, functions = newFunctions, predicates = newPredicates,
238243
methods = newMethods)(p.pos, p.info, p.errT)
244+
Config.transformedProgramCallback.foreach(fn => fn(res))
245+
res
239246
}
240247

241248
// TODO REM: depends on the results of relationalPredicates

0 commit comments

Comments
 (0)