Add an option to allow automatically generated requirements to be printed

to a file, making them easier to inspect and manipulate.

1 files changed, 6 insertions, 0 deletions

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 6921522c..56e28047 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -759,6 +759,12 @@ namespace Microsoft.Dafny
 

       if (!tip.Equals("")) {

         resolver.ReportAdditionalInformation(f.tok, tip, f.tok.val.Length);

+        if (DafnyOptions.O.AutoReqPrintFile != null) {

+          using (System.IO.TextWriter writer = new System.IO.StreamWriter(DafnyOptions.O.AutoReqPrintFile, true)) {

+            writer.WriteLine(f.Name);

+            writer.WriteLine("\t" + tip);

+          }

+        }

       }

     }