1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
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
{
}
}
|
