summaryrefslogtreecommitdiff
path: root/Source/BoogieDriver
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2014-05-19 10:09:57 +0200
committerGravatar wuestholz <unknown>2014-05-19 10:09:57 +0200
commitb71dd16a15ac5e01fe8c04954d05deedd49b5d24 (patch)
tree80ac8e1e7b6eed01d6fd87b47b0674652c730ef7 /Source/BoogieDriver
parent0cad072b686387cc6e5eba233f3e17d08a328d07 (diff)
Made the Boogie driver return an exit code.
Diffstat (limited to 'Source/BoogieDriver')
-rw-r--r--Source/BoogieDriver/BoogieDriver.cs4
1 files changed, 3 insertions, 1 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 12a6084f..cba74bc5 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -24,7 +24,7 @@ namespace Microsoft.Boogie {
public class OnlyBoogie
{
- public static void Main(string[] args)
+ public static int Main(string[] args)
{
Contract.Requires(cce.NonNullElements(args));
@@ -90,6 +90,7 @@ namespace Microsoft.Boogie {
}
}
ExecutionEngine.ProcessFiles(fileList);
+ return 0;
END:
if (CommandLineOptions.Clo.XmlSink != null) {
@@ -99,6 +100,7 @@ namespace Microsoft.Boogie {
Console.WriteLine("Press Enter to exit.");
Console.ReadLine();
}
+ return 1;
}
}
}