Merge

5 files changed, 53 insertions, 50 deletions

diff --git a/Source/Dafny/Makefile b/Source/Dafny/Makefile
index e8c0f5e0..68ab7a2d 100644
--- a/Source/Dafny/Makefile
+++ b/Source/Dafny/Makefile
@@ -4,7 +4,7 @@
 # from http://boogiepartners.codeplex.com/. Update the FRAME_DIR variable to

 # point to whatever directory you install that into.

 # ###############################################################################

-COCO_EXE_DIR = ..\..\..\boogie-partners\CocoRdownload

+COCO_EXE_DIR = ..\..\..\boogie-partners\CocoR\bin

 FRAME_DIR = ..\..\..\boogie-partners\CocoR\Modified

 COCO = $(COCO_EXE_DIR)\Coco.exe

 

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index dae1b95e..fd6fb026 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -78,11 +78,11 @@ public class Parser {
 	const bool _x = false;

 	const int minErrDist = 2;

 

-	public Scanner/*!*/ scanner;

-	public Errors/*!*/  errors;

+	public Scanner scanner;

+	public Errors  errors;

 

-	public Token/*!*/ t;    // last recognized token

-	public Token/*!*/ la;   // lookahead token

+	public Token t;    // last recognized token

+	public Token la;   // lookahead token

 	int errDist = minErrDist;

 

 readonly Expression/*!*/ dummyExpr;

@@ -454,10 +454,10 @@ bool IsType(ref IToken pt) {
 /*--------------------------------------------------------------------------*/

 

 

-	public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors) {

+	public Parser(Scanner scanner, Errors errors) {

 		this.scanner = scanner;

 		this.errors = errors;

-		Token/*!*/ tok = new Token();

+		Token tok = new Token();

 		tok.val = "";

 		this.la = tok;

 		this.t = new Token(); // just to satisfy its non-null constraint

@@ -468,13 +468,13 @@ bool IsType(ref IToken pt) {
 		errDist = 0;

 	}

 

-	public void SemErr (string/*!*/ msg) {

+	public void SemErr (string msg) {

 		Contract.Requires(msg != null);

 		if (errDist >= minErrDist) errors.SemErr(t, msg);

 		errDist = 0;

 	}

 

-	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {

+	public void SemErr(IToken tok, string msg) {

 	  Contract.Requires(tok != null);

 	  Contract.Requires(msg != null);

 	  errors.SemErr(tok, msg);

@@ -4385,10 +4385,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Dafny();

 		Expect(0);

 

-		Expect(0);

 	}

 

-	static readonly bool[,]/*!*/ set = {

+	static readonly bool[,] set = {

 		{_T,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_T, _x,_x,_T,_T, _T,_x,_x,_T, _T,_x,_x,_T, _T,_x,_T,_T, _T,_T,_T,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_T, _T,_x,_x,_T, _T,_T,_x,_x, _T,_x,_x,_T, _T,_T,_T,_T, _T,_T,_x,_T, _T,_x,_x,_T, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_x,_x,_x},

 		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _T,_x,_x,_x, _x,_T,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x},

 		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_x, _x,_T,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x},

@@ -4428,17 +4427,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 public class Errors {

 	public int count = 0;                                    // number of errors detected

-	public System.IO.TextWriter/*!*/ errorStream = Console.Out;   // error messages go to this stream

-	public string errMsgFormat = "{0}({1},{2}): Error: {3}"; // 0=filename, 1=line, 2=column, 3=text

-	public string warningMsgFormat = "{0}({1},{2}): Warning: {3}"; // 0=filename, 1=line, 2=column, 3=text

 

 	public void SynErr(string filename, int line, int col, int n) {

 		SynErr(filename, line, col, GetSyntaxErrorString(n));

 	}

 

-	public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {

+	public virtual void SynErr(string filename, int line, int col, string msg) {

 		Contract.Requires(msg != null);

-		errorStream.WriteLine(errMsgFormat, filename, line, col - 1, msg);

+		Dafny.Util.ReportIssue("Error", filename, line, col, msg);

 		count++;

 	}

 

@@ -4693,27 +4689,23 @@ public class Errors {
 		return s;

 	}

 

-	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors

+	public void SemErr(IToken tok, string msg) {  // semantic errors

 		Contract.Requires(tok != null);

 		Contract.Requires(msg != null);

-		SemErr(tok.filename, tok.line, tok.col, msg);

+		Dafny.Util.ReportIssue("Error", tok, msg);

+		count++;

 	}

 

-	public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {

+	public virtual void SemErr(string filename, int line, int col, string msg) {

 		Contract.Requires(msg != null);

-		errorStream.WriteLine(errMsgFormat, filename, line, col - 1, msg);

+		Dafny.Util.ReportIssue("Error", filename, line, col, msg);

 		count++;

 	}

 

-	public void Warning(IToken/*!*/ tok, string/*!*/ msg) {  // warnings

+	public virtual void Warning(IToken tok, string msg) {  // warnings

 		Contract.Requires(tok != null);

 		Contract.Requires(msg != null);

-		Warning(tok.filename, tok.line, tok.col, msg);

-	}

-

-	public virtual void Warning(string filename, int line, int col, string msg) {

-		Contract.Requires(msg != null);

-		errorStream.WriteLine(warningMsgFormat, filename, line, col - 1, msg);

+		Dafny.Util.ReportIssue("Warning", tok, msg);

 	}

 } // Errors

 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 44990d7d..e977dbd5 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -24,9 +24,7 @@ namespace Microsoft.Dafny
       Contract.Requires(msg != null);

       ConsoleColor col = Console.ForegroundColor;

       Console.ForegroundColor = ConsoleColor.Red;

-      Console.WriteLine("{0}({1},{2}): Error: {3}",

-          DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(tok.filename) : tok.filename, tok.line, tok.col - 1,

-          string.Format(msg, args));

+      Dafny.Util.ReportIssue("Error", tok, msg, args);

       Console.ForegroundColor = col;

       ErrorCount++;

     }

@@ -66,9 +64,7 @@ namespace Microsoft.Dafny
       if (reportWarnings) {

         ConsoleColor col = Console.ForegroundColor;

         Console.ForegroundColor = ConsoleColor.Yellow;

-        Console.WriteLine("{0}({1},{2}): Warning: {3}",

-            DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(tok.filename) : tok.filename, tok.line, tok.col - 1,

-            string.Format(msg, args));

+        Dafny.Util.ReportIssue("Warning", tok, msg, args);

         Console.ForegroundColor = col;

       }

     }

@@ -281,9 +277,7 @@ namespace Microsoft.Dafny
     }

 

     public static void DefaultInformationReporter(AdditionalInformation info) {

-      Console.WriteLine("{0}({1},{2}): Info: {3}",

-                        DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(info.Token.filename) : info.Token.filename,

-                        info.Token.line, info.Token.col - 1, info.Text);

+      Dafny.Util.ReportIssue("Info", info.Token, info.Text);

     }

 

     public void ResolveProgram(Program prog) {

@@ -4497,6 +4491,10 @@ namespace Microsoft.Dafny
           // something is wrong; either aa or bb wasn't properly resolved, or they don't unify

           return false;

         }

+      } else if (a is Resolver_IdentifierExpr.ResolverType_Type) {

+        return b is Resolver_IdentifierExpr.ResolverType_Type;

+      } else if (a is Resolver_IdentifierExpr.ResolverType_Module) {

+        return b is Resolver_IdentifierExpr.ResolverType_Module;

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type

       }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 3821e5df..b8c4b8ec 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3609,7 +3609,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(tok != null);

       Contract.Ensures(Contract.Result<Bpl.Cmd>() != null);

       var col = tok.col + (isEndToken ? tok.val.Length : 0);

-      string description = string.Format("{0}({1},{2}){3}{4}", tok.filename, tok.line, col, additionalInfo == null ? "" : ": ", additionalInfo ?? "");

+      string description = Util.ReportIssueToString_Bare(additionalInfo == null ? "" : ": ", tok.filename, tok.line, tok.col, additionalInfo ?? "");

       QKeyValue kv = new QKeyValue(tok, "captureState", new List<object>() { description }, null);

       return new Bpl.AssumeCmd(tok, Bpl.Expr.True, kv);

     }

@@ -12956,12 +12956,8 @@ namespace Microsoft.Dafny {
           } else {

             // Skip inlining, as it would cause arbitrary expressions to pop up in the trigger

             // CLEMENT: Report inlining issue in a VS plugin friendly way

-            var info = new AdditionalInformation {

-              Token = fexp.tok,

-              Length = fexp.tok.val.Length,

-              Text = "This call cannot be safely inlined.",

-            };

-            Resolver.DefaultInformationReporter(info);

+            //CLEMENT this should appear at the outmost call site, not at the innermost. See SnapshotableTrees.dfy

+            Dafny.Util.ReportIssue("Info", fexp.tok, "Some instances of this call cannot safely be inlined.");

           }

         }

 

diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs
index 63659696..508d23c6 100644
--- a/Source/Dafny/Util.cs
+++ b/Source/Dafny/Util.cs
@@ -67,18 +67,35 @@ namespace Microsoft.Dafny {
       return res;

     }

 

+    public static void ReportIssue(string header, IToken tok, string msg, params object[] args) {

+      ReportIssue(header, tok, String.Format(msg, args));

+    }

+

+    public static void ReportIssue(string header, IToken tok, string msg) {

+      ReportIssue(header, tok.filename, tok.line, tok.col, msg);

+    }

+

+    public static void ReportIssue(string header, string filename, int line, int column, string msg) {

+      Console.WriteLine(ReportIssueToString(header, filename, line, column, msg));

+    }

+

+    public static string ReportIssueToString(string header, string filename, int line, int column, string msg) {

+      Contract.Requires(header != null);

+      Contract.Requires(filename != null);

+      Contract.Requires(msg != null);

+      return ReportIssueToString_Bare(": " + header, filename, line, column, ": " + msg);

+    }

+

+    public static string ReportIssueToString_Bare(string header, string filename, int line, int column, string msg) {

+      return String.Format("{0}({1},{2}){3}{4}", filename, line, column - 1, header, msg ?? "");

+    }

+

     /// <summary>

     /// Returns s but with all occurrences of '_' removed.

     /// </summary>

     public static string RemoveUnderscores(string s) {

       Contract.Requires(s != null);

-      while (true) {

-        var j = s.IndexOf('_');

-        if (j == -1) {

-          return s;

-        }

-        s = s.Substring(0, j) + s.Substring(j + 1);

-      }

+      return s.Replace("_", "");

     }

 

     /// <summary>