diff options
| author |  wuestholz <unknown> | 2013-06-03 15:32:05 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-06-03 15:32:05 -0700 |
| commit | c0578efe1ff17e30eb33e60e279a9a14a7a836a5 (patch) | |
| tree | d36da3614ff95c215987938f4eaa9cfc31ee54c3 /Source/Core | |
| parent | bdbe3bc2795a0a6b77f41d7065bebdc9820f0983 (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, 0 insertions, 135 deletions
diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index 2010f504..d41fb40b 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -152,7 +152,6 @@ <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 deleted file mode 100644 index 84549892..00000000 --- a/Source/Core/ExecutionEngine.cs +++ /dev/null @@ -1,134 +0,0 @@ -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
- {
-
-
-
- }
-}
|