diff options
| author |  wuestholz <unknown> | 2013-06-03 14:45:41 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-06-03 14:45:41 -0700 |
| commit | bdbe3bc2795a0a6b77f41d7065bebdc9820f0983 (patch) | |
| tree | f50d98d250de1b2b91b7f85f38f2ba601011dd63 /Source/Core | |
| parent | 4a20bc3e87017d90f1ec76f43787964897c3fe90 (diff) | |
Did some refactoring in the Boogie driver.
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/Core.csproj | 1 | ||||
| -rw-r--r-- | Source/Core/ExecutionEngine.cs | 134 |
2 files changed, 135 insertions, 0 deletions
diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index d41fb40b..2010f504 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -152,6 +152,7 @@ <Compile Include="AbsyQuant.cs" />
<Compile Include="AbsyType.cs" />
<Compile Include="BitvectorAnalysis.cs" />
+ <Compile Include="ExecutionEngine.cs" />
<Compile Include="InterProceduralReachabilityGraph.cs" />
<Compile Include="CommandLineOptions.cs" />
<Compile Include="DeadVarElim.cs" />
diff --git a/Source/Core/ExecutionEngine.cs b/Source/Core/ExecutionEngine.cs new file mode 100644 index 00000000..84549892 --- /dev/null +++ b/Source/Core/ExecutionEngine.cs @@ -0,0 +1,134 @@ +using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+
+namespace Core
+{
+ public interface OutputPrinter
+ {
+ void ErrorWriteLine(string s);
+ void ErrorWriteLine(string format, params object[] args);
+ void AdvisoryWriteLine(string format, params object[] args);
+ void Inform(string s);
+ void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories);
+ }
+
+
+ public class ConsolePrinter : OutputPrinter
+ {
+ public void ErrorWriteLine(string s)
+ {
+ Contract.Requires(s != null);
+ if (!s.Contains("Error: ") && !s.Contains("Error BP"))
+ {
+ Console.WriteLine(s);
+ return;
+ }
+
+ // split the string up into its first line and the remaining lines
+ string remaining = null;
+ int i = s.IndexOf('\r');
+ if (0 <= i)
+ {
+ remaining = s.Substring(i + 1);
+ if (remaining.StartsWith("\n"))
+ {
+ remaining = remaining.Substring(1);
+ }
+ s = s.Substring(0, i);
+ }
+
+ ConsoleColor col = Console.ForegroundColor;
+ Console.ForegroundColor = ConsoleColor.Red;
+ Console.WriteLine(s);
+ Console.ForegroundColor = col;
+
+ if (remaining != null)
+ {
+ Console.WriteLine(remaining);
+ }
+ }
+
+
+ public void ErrorWriteLine(string format, params object[] args)
+ {
+ Contract.Requires(format != null);
+ string s = string.Format(format, args);
+ ErrorWriteLine(s);
+ }
+
+
+ public void AdvisoryWriteLine(string format, params object[] args)
+ {
+ Contract.Requires(format != null);
+ ConsoleColor col = Console.ForegroundColor;
+ Console.ForegroundColor = ConsoleColor.Yellow;
+ Console.WriteLine(format, args);
+ Console.ForegroundColor = col;
+ }
+
+
+ /// <summary>
+ /// Inform the user about something and proceed with translation normally.
+ /// Print newline after the message.
+ /// </summary>
+ public void Inform(string s)
+ {
+ if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations)
+ {
+ Console.WriteLine(s);
+ }
+ }
+
+
+ public void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories)
+ {
+ Contract.Requires(0 <= errors && 0 <= inconclusives && 0 <= timeOuts && 0 <= outOfMemories);
+ Console.WriteLine();
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)
+ {
+ Console.Write("{0} finished with {1} credible, {2} doomed{3}", CommandLineOptions.Clo.DescriptiveToolName, verified, errors, errors == 1 ? "" : "s");
+ }
+ else
+ {
+ Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.DescriptiveToolName, verified, errors, errors == 1 ? "" : "s");
+ }
+ if (inconclusives != 0)
+ {
+ Console.Write(", {0} inconclusive{1}", inconclusives, inconclusives == 1 ? "" : "s");
+ }
+ if (timeOuts != 0)
+ {
+ Console.Write(", {0} time out{1}", timeOuts, timeOuts == 1 ? "" : "s");
+ }
+ if (outOfMemories != 0)
+ {
+ Console.Write(", {0} out of memory", outOfMemories);
+ }
+ Console.WriteLine();
+ Console.Out.Flush();
+ }
+ }
+
+
+ public enum PipelineOutcome
+ {
+ Done,
+ ResolutionError,
+ TypeCheckingError,
+ ResolvedAndTypeChecked,
+ FatalError,
+ VerificationCompleted
+ }
+
+
+ class ExecutionEngine
+ {
+
+
+
+ }
+}
|