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

4 files changed, 5 insertions, 17 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 84f09ee0..46ed1b76 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -740,10 +740,6 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
   [ BlockStmt<out body, out bodyStart, out bodyEnd>

   ]

   (.

-     if (Attributes.Contains(attrs, "axiom") && !mmod.IsGhost && !isLemma) {

-        SemErr(t, "only ghost methods can have the :axiom attribute");

-     }

-

      if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom")) {

         SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");

      }

diff --git a/Source/Dafny/Makefile b/Source/Dafny/Makefile
index 95cd7748..4c01c780 100644
--- a/Source/Dafny/Makefile
+++ b/Source/Dafny/Makefile
@@ -6,7 +6,7 @@
 # ###############################################################################

 COCO_EXE_DIR = ..\..\..\boogiepartners\CocoRdownload

 FRAME_DIR = ..\..\..\boogiepartners\CocoR\Modified

-COCO = COCO = $(COCO_EXE_DIR)\Coco.exe

+COCO = $(COCO_EXE_DIR)\Coco.exe

 

 # "all" depends on 2 files, really (Parser.cs and Scanner.cs), but they

 # are both generated in one go and I don't know a better way to tell

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 2358fc79..ca13a01e 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1089,10 +1089,6 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		if (la.kind == 15) {

 			BlockStmt(out body, out bodyStart, out bodyEnd);

 		}

-		if (Attributes.Contains(attrs, "axiom") && !mmod.IsGhost && !isLemma) {

-		  SemErr(t, "only ghost methods can have the :axiom attribute");

-		}

-		

 		if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom")) {

 		  SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");

 		}

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;