Allow non-ghost axioms in order to model trusted external calls,

e.g., Ironclad's calls to assembly instructions.
Also fixed what appeared to be a bug in the Makefile for invoking Coco

1 files changed, 4 insertions, 8 deletions

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 06493434..ca72e221 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -299,7 +299,7 @@ public class Scanner {
 	}

 

 //	[NotDelayed]

-	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler, bool useBaseName = false) : base() {

+	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {

 	  Contract.Requires(fileName != null);

 	  Contract.Requires(errorHandler != null);

 		this.errorHandler = errorHandler;

@@ -308,7 +308,7 @@ public class Scanner {
 		try {

 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);

 			buffer = new Buffer(stream, false);

-			Filename = useBaseName? GetBaseName(fileName): fileName;

+			Filename = fileName;

 			Init();

 		} catch (IOException) {

 			throw new FatalError("Cannot open file " + fileName);

@@ -316,7 +316,7 @@ public class Scanner {
 	}

 

 //	[NotDelayed]

-	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName, bool useBaseName = false) : base() {

+	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {

 	  Contract.Requires(s != null);

 	  Contract.Requires(errorHandler != null);

 	  Contract.Requires(fileName != null);

@@ -324,14 +324,10 @@ public class Scanner {
 		t = new Token(); // dummy because t is a non-null field

 		buffer = new Buffer(s, true);

 		this.errorHandler = errorHandler;

-		this.Filename = useBaseName? GetBaseName(fileName) : fileName;

+		this.Filename = fileName;

 		Init();

 	}

 

-    string GetBaseName(string fileName) {

-        return System.IO.Path.GetFileName(fileName); // Return basename

-    }

-

 	void Init() {

 		pos = -1; line = 1; col = 0;

 		oldEols = 0;