summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/Dafny/DafnyOptions.cs37
-rw-r--r--Source/Dafny/Reporting.cs2
-rw-r--r--Source/DafnyDriver/DafnyDriver.cs14
-rw-r--r--Source/DafnyServer/DafnyHelper.cs5
-rw-r--r--Source/DafnyServer/Utilities.cs4
-rw-r--r--Source/DafnyServer/VerificationTask.cs3
6 files changed, 47 insertions, 18 deletions
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 1986ea6d..08e53d5c 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -9,8 +9,11 @@ namespace Microsoft.Dafny
{
public class DafnyOptions : Bpl.CommandLineOptions
{
- public DafnyOptions()
+ private ErrorReporter errorReporter;
+
+ public DafnyOptions(ErrorReporter errorReporter = null)
: base("Dafny", "Dafny program verifier") {
+ this.errorReporter = errorReporter;
SetZ3ExecutableName();
}
@@ -257,13 +260,37 @@ namespace Microsoft.Dafny
// TODO: provide attribute help here
}
+
+ /// <summary>
+ /// Dafny comes with it's own copy of z3, to save new users the trouble of having to install extra dependency.
+ /// For this to work, Dafny makes the Z3ExecutablePath point to the path were Z3 is put by our release script.
+ /// For developers though (and people getting this from source), it's convenient to be able to run right away,
+ /// so we vendor a Windows version.
+ /// </summary>
private void SetZ3ExecutableName() {
var platform = (int)System.Environment.OSVersion.Platform;
- var isLinux = platform == 4 || platform == 128; // http://www.mono-project.com/docs/faq/technical/
- //TODO should we also vendor an OSX build?
- var binDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location);
- Z3ExecutablePath = System.IO.Path.Combine(binDir, isLinux ? "z3" : "z3.exe");
+ // http://www.mono-project.com/docs/faq/technical/
+ var isUnix = platform == 4 || platform == 128;
+
+ var z3binName = isUnix ? "z3" : "z3.exe";
+ var dafnyBinDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location);
+ var z3BinDir = System.IO.Path.Combine(dafnyBinDir, "z3", "bin");
+ var z3BinPath = System.IO.Path.Combine(z3BinDir, z3binName);
+
+ if (!System.IO.File.Exists(z3BinPath) && !isUnix) {
+ // This is most likely a Windows user running from source without downloading z3
+ // separately; this is ok, since we vendor z3.exe.
+ z3BinPath = System.IO.Path.Combine(dafnyBinDir, z3binName);
+ }
+
+ if (!System.IO.File.Exists(z3BinPath) && errorReporter != null) {
+ var tok = new Bpl.Token(1, 1) { filename = "*** " };
+ errorReporter.Warning(MessageSource.Other, tok, "Could not find '{0}' in '{1}'.{2}Downloading and extracting a Z3 distribution to Dafny's 'Binaries' folder would solve this issue; for now, we'll rely on Boogie to find Z3.",
+ z3binName, z3BinDir, System.Environment.NewLine);
+ } else {
+ Z3ExecutablePath = z3BinPath;
+ }
}
public override void Usage() {
diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs
index 4cfbf20e..760392ca 100644
--- a/Source/Dafny/Reporting.cs
+++ b/Source/Dafny/Reporting.cs
@@ -143,7 +143,7 @@ namespace Microsoft.Dafny {
}
public override bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) {
- if (base.Message(source, level, tok, msg) && (DafnyOptions.O.PrintTooltips || level != ErrorLevel.Info)) {
+ if (base.Message(source, level, tok, msg) && ((DafnyOptions.O != null && DafnyOptions.O.PrintTooltips) || level != ErrorLevel.Info)) {
// Extra indent added to make it easier to distinguish multiline error messages for clients that rely on the CLI
msg = msg.Replace(Environment.NewLine, Environment.NewLine + " ");
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 4b5ae8d8..c45d66fc 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -40,10 +40,11 @@ namespace Microsoft.Dafny
public static int ThreadMain(string[] args)
{
Contract.Requires(cce.NonNullElements(args));
-
+
+ ErrorReporter reporter = new ConsoleErrorReporter();
ExecutionEngine.printer = new DafnyConsolePrinter(); // For boogie errors
- DafnyOptions.Install(new DafnyOptions());
+ DafnyOptions.Install(new DafnyOptions(reporter));
ExitValue exitValue = ExitValue.VERIFIED;
CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;
@@ -92,7 +93,7 @@ namespace Microsoft.Dafny
goto END;
}
}
- exitValue = ProcessFiles(CommandLineOptions.Clo.Files);
+ exitValue = ProcessFiles(CommandLineOptions.Clo.Files, reporter);
END:
if (CommandLineOptions.Clo.XmlSink != null) {
@@ -112,7 +113,7 @@ namespace Microsoft.Dafny
}
- static ExitValue ProcessFiles(IList<string/*!*/>/*!*/ fileNames, bool lookForSnapshots = true, string programId = null)
+ static ExitValue ProcessFiles(IList<string/*!*/>/*!*/ fileNames, ErrorReporter reporter, bool lookForSnapshots = true, string programId = null)
{
Contract.Requires(cce.NonNullElements(fileNames));
@@ -128,7 +129,7 @@ namespace Microsoft.Dafny
{
Console.WriteLine();
Console.WriteLine("-------------------- {0} --------------------", f);
- var ev = ProcessFiles(new List<string> { f }, lookForSnapshots, f);
+ var ev = ProcessFiles(new List<string> { f }, reporter, lookForSnapshots, f);
if (exitValue != ev && ev != ExitValue.VERIFIED)
{
exitValue = ev;
@@ -142,7 +143,7 @@ namespace Microsoft.Dafny
var snapshotsByVersion = ExecutionEngine.LookForSnapshots(fileNames);
foreach (var s in snapshotsByVersion)
{
- var ev = ProcessFiles(new List<string>(s), false, programId);
+ var ev = ProcessFiles(new List<string>(s), reporter, false, programId);
if (exitValue != ev && ev != ExitValue.VERIFIED)
{
exitValue = ev;
@@ -153,7 +154,6 @@ namespace Microsoft.Dafny
using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count-1])) {
Dafny.Program dafnyProgram;
- ErrorReporter reporter = new ConsoleErrorReporter();
string programName = fileNames.Count == 1 ? fileNames[0] : "the program";
string err = Dafny.Main.ParseCheck(fileNames, programName, reporter, out dafnyProgram);
if (err != null) {
diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs
index 3204fdb3..e54e2b48 100644
--- a/Source/DafnyServer/DafnyHelper.cs
+++ b/Source/DafnyServer/DafnyHelper.cs
@@ -29,18 +29,21 @@ namespace Microsoft.Dafny {
class DafnyHelper {
private string fname;
private string source;
+ private string[] args;
private readonly Dafny.ErrorReporter reporter;
private Dafny.Program dafnyProgram;
private Bpl.Program boogieProgram;
- public DafnyHelper(string fname, string source) {
+ public DafnyHelper(string[] args, string fname, string source) {
+ this.args = args;
this.fname = fname;
this.source = source;
this.reporter = new Dafny.ConsoleErrorReporter();
}
public bool Verify() {
+ ServerUtils.ApplyArgs(args, reporter);
return Parse() && Resolve() && Translate() && Boogie();
}
diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs
index 59b3abb9..5e2c6f96 100644
--- a/Source/DafnyServer/Utilities.cs
+++ b/Source/DafnyServer/Utilities.cs
@@ -43,8 +43,8 @@ namespace Microsoft.Dafny {
}
}
- internal static void ApplyArgs(string[] args) {
- Dafny.DafnyOptions.Install(new Dafny.DafnyOptions());
+ internal static void ApplyArgs(string[] args, ErrorReporter reporter) {
+ Dafny.DafnyOptions.Install(new Dafny.DafnyOptions(reporter));
Dafny.DafnyOptions.O.ProverKillTime = 15; //This is just a default; it can be overriden
if (CommandLineOptions.Clo.Parse(args)) {
diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs
index a00688b1..eb740e70 100644
--- a/Source/DafnyServer/VerificationTask.cs
+++ b/Source/DafnyServer/VerificationTask.cs
@@ -52,8 +52,7 @@ namespace Microsoft.Dafny {
}
internal void Run() {
- ServerUtils.ApplyArgs(args);
- new DafnyHelper(filename, ProgramSource).Verify();
+ new DafnyHelper(args, filename, ProgramSource).Verify();
}
}
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 16:04:44 +0000