Boogie: add /printCFG command line option, which prints each implementation's CFG in Graphviz format

1 files changed, 11 insertions, 0 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index c28d8c8a..7d55e177 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -450,6 +450,7 @@ namespace Microsoft.Boogie {
     public string PrintErrorModelFile = null;

     public string/*?*/ ModelViewFile = null;

     public int EnhancedErrorMessages = 0;

+    public string PrintCFGPrefix = null;

     public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present

     public bool UseArrayTheory = false;

     public bool UseLabels = true;

@@ -834,6 +835,12 @@ namespace Microsoft.Boogie {
           ps.GetNumericArgument(ref EnhancedErrorMessages, 2);

           return true;

 

+        case "printCFG":

+          if (ps.ConfirmArgumentCount(1)) {

+            PrintCFGPrefix = args[ps.i];

+          }

+          return true;

+

         case "inlineDepth":

           ps.GetNumericArgument(ref InlineDepth);

           return true;

@@ -1449,6 +1456,10 @@ namespace Microsoft.Boogie {
                 0 (default) - no enhanced error messages

                 1 - Z3 error model enhanced error messages

 

+  /printCFG:<prefix> : print control flow graph of each implementation in

+                       Graphviz format to files named:

+                         <prefix>.<procedure name>.dot

+

   ---- Inference options -----------------------------------------------------

 

   /infer:<flags>