summaryrefslogtreecommitdiff
path: root/Source/DafnyDriver
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2013-06-03 11:00:27 -0700
committerGravatar wuestholz <unknown>2013-06-03 11:00:27 -0700
commit2927e2cc553a6d82ca7c7afeb9cb5d96fed7aa6d (patch)
tree6de5aa87a53b1896e2528a6133131a4c9cfc1f37 /Source/DafnyDriver
parent7a4ffae70254686db3532b748b025c1f8621bef5 (diff)
Did some refactoring of the Dafny drivers.
Diffstat (limited to 'Source/DafnyDriver')
-rw-r--r--Source/DafnyDriver/DafnyDriver.cs21
1 files changed, 5 insertions, 16 deletions
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 25741332..f3da0ec2 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -95,7 +95,7 @@ namespace Microsoft.Dafny
return (int)exitValue;
}
- public static void ErrorWriteLine(string s) {Contract.Requires(s != null);
+ static void ErrorWriteLine(string s) {Contract.Requires(s != null);
if (!s.Contains("Error: ") && !s.Contains("Error BP")) {
Console.WriteLine(s);
return;
@@ -122,14 +122,14 @@ namespace Microsoft.Dafny
}
}
- public static void ErrorWriteLine(string format, params object[] args) {
+ static void ErrorWriteLine(string format, params object[] args) {
Contract.Requires(format != null);
Contract.Requires(args != null);
string s = string.Format(format, args);
ErrorWriteLine(s);
}
- public static void AdvisoryWriteLine(string format, params object[] args) {
+ static void AdvisoryWriteLine(string format, params object[] args) {
Contract.Requires(format != null);
ConsoleColor col = Console.ForegroundColor;
Console.ForegroundColor = ConsoleColor.Yellow;
@@ -137,8 +137,6 @@ namespace Microsoft.Dafny
Console.ForegroundColor = col;
}
- enum FileType { Unknown, Cil, Bpl, Dafny };
-
static ExitValue ProcessFiles (List<string/*!*/>/*!*/ fileNames)
{
Contract.Requires(cce.NonNullElements(fileNames));
@@ -267,20 +265,11 @@ namespace Microsoft.Dafny
}
- static bool ProgramHasDebugInfo (Bpl.Program program)
- {
- Contract.Requires(program != null);
- // We inspect the last declaration because the first comes from the prelude and therefore always has source context.
- return program.TopLevelDeclarations.Count > 0 &&
- cce.NonNull(program.TopLevelDeclarations[program.TopLevelDeclarations.Count - 1]).tok.IsValid;
- }
-
-
/// <summary>
/// Inform the user about something and proceed with translation normally.
/// Print newline after the message.
/// </summary>
- public static void Inform(string s) {
+ static void Inform(string s) {
if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations) {
Console.WriteLine(s);
}
@@ -800,7 +789,7 @@ namespace Microsoft.Dafny
return PipelineOutcome.VerificationCompleted;
}
- private static void ReportAllBplErrors(QKeyValue attr) {
+ static void ReportAllBplErrors(QKeyValue attr) {
while (attr != null) {
if (attr.Key == "msg" && attr.Params.Count == 1) {
var str = attr.Params[0] as string;