VS 2010 mode for Chalice: some errors didn't show up in the window because positions were negative

4 files changed, 67 insertions, 53 deletions

diff --git a/Chalice/src/Boogie.scala b/Chalice/src/Boogie.scala
index 4fa21be0..afaff452 100644
--- a/Chalice/src/Boogie.scala
+++ b/Chalice/src/Boogie.scala
@@ -208,8 +208,8 @@ object Boogie {
    case Comment(msg) => indent +  "// " +  msg + nl

    case assert@Assert(e) =>

      val pos = if (Chalice.vsMode) {

-       val r = assert.pos.line - 1;

-       val c = assert.pos.column - 1;

+       val r = assert.pos.line;

+       val c = assert.pos.column;

        r + "," + c + "," + r + "," + (c+5) + ":"

      } else {

        "  " + assert.pos + ": "

diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
index 43b3a330..0b2d43c5 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -9,6 +9,7 @@ import java.io.InputStreamReader
 import java.io.File

 import java.io.FileWriter

 import scala.util.parsing.input.Position

+import scala.util.parsing.input.NoPosition

 import collection.mutable.ListBuffer

 

 object Chalice {

@@ -36,16 +37,6 @@ object Chalice {
     var boogiePath = "C:\\boogie\\Binaries\\Boogie.exe"

     val inputs = new ListBuffer[String]()

     var printProgram = false

-

-    def ReportError(pos: Position, msg: String) = {

-     if (vsMode) {

-       val r = pos.line - 1;

-       val c = pos.column - 1;

-       Console.out.println(r + "," + c + "," + r + "," + (c+5) + ":" + msg);

-     } else {

-       Console.err.println(pos + ": " + msg)

-     }

-    }

     var doTypecheck = true

     var doTranslate = true

     var boogieArgs = " ";

@@ -196,6 +187,14 @@ object Chalice {
 

   def CommandLineError(msg: String, help: String) = {

    Console.err.println("Error: " + msg)

-   Console.err.println(help);

   }

+

+  def ReportError(pos: Position, msg: String) = {

+    if (vsMode) {

+     val (r,c) = (pos.line, pos.column)     

+     Console.out.println(r + "," + c + "," + r + "," + (c+5) + ":" + msg);

+    } else {

+     Console.err.println(pos + ": " + msg)

+    }

+  }  

 }

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 1ae56ca2..75d23e53 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -1015,8 +1015,8 @@ class Translator {
       isDefined(guard) ::: List(bassume(guard)) :::

       translateStatement(body) ::: 

       // check invariant

-      Exhale(w.oldInvs map { inv => (inv, ErrorMessage(w.pos, "The loop invariant at " + inv.pos + " might not be preserved by the loop."))}, "loop invariant, maintained") :::

-      tag(Exhale(w.newInvs map { inv => (inv, ErrorMessage(w.pos, "The loop invariant at " + inv.pos + " might not be preserved by the loop."))}, "loop invariant, maintained"), keepTag) :::

+      Exhale(w.oldInvs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant at " + inv.pos + " might not be preserved by the loop."))}, "loop invariant, maintained") :::

+      tag(Exhale(w.newInvs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant at " + inv.pos + " might not be preserved by the loop."))}, "loop invariant, maintained"), keepTag) :::

       isLeaking(w.pos, "The loop might leak refereces.") :::

       // check lockchange after loop iteration

       Comment("check lockchange after loop iteration") ::

@@ -1622,6 +1622,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
   **********************************************************************/

 

   def Inhale(predicates: List[Expression], occasion: String, check: Boolean): List[Boogie.Stmt] = {

+    if (predicates.size == 0) return Nil;

+    

     val (ihV, ih) = Boogie.NewBVar("inhaleHeap", theap, true)

     Comment("inhale (" + occasion + ")") ::

     BLocal(ihV) :: Boogie.Havoc(ih) ::

@@ -1633,6 +1635,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
   }

 

   def InhaleFrom(predicates: List[Expression], occasion: String, check: Boolean, useHeap: Boogie.Expr): List[Boogie.Stmt] = {

+    if (predicates.size == 0) return Nil;

+    

     val (ihV, ih) = Boogie.NewBVar("inhaleHeap", theap, true)

     Comment("inhale (" + occasion + ")") ::

     BLocal(ihV) :: Boogie.Assign(ih, useHeap) ::

@@ -1773,6 +1777,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
   }

 

   def Exhale(predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean): List[Boogie.Stmt] = {

+    if (predicates.size == 0) return Nil;

+    

     val (emV, em) = NewBVar("exhaleMask", tmask, true)

     Comment("begin exhale (" + occasion + ")") ::

     BLocal(emV) :: (em := Mask) ::

diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyLanguageService.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyLanguageService.cs
index 4791df00..281040ca 100644
--- a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyLanguageService.cs
+++ b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyLanguageService.cs
@@ -9,6 +9,7 @@ using Irony.Parsing;
 using Irony.Ast;

 

 using System.IO;

+using System.Text.RegularExpressions;

 

 namespace Demo

 {

@@ -108,26 +109,26 @@ namespace Demo
                 }

 

                     // Used for brace matching.

-                    TokenStack braces = parser.Context.OpenBraces;

-                    foreach (Token brace in braces) {

-                      if (brace.OtherBrace == null) continue;

-                      TextSpan openBrace = new TextSpan();

-                      openBrace.iStartLine = brace.Location.Line;

-                      openBrace.iStartIndex = brace.Location.Column;

-                      openBrace.iEndLine = brace.Location.Line;

-                      openBrace.iEndIndex = openBrace.iStartIndex + brace.Length;

-

-                      TextSpan closeBrace = new TextSpan();

-                      closeBrace.iStartLine = brace.OtherBrace.Location.Line;

-                      closeBrace.iStartIndex = brace.OtherBrace.Location.Column;

-                      closeBrace.iEndLine = brace.OtherBrace.Location.Line;

-                      closeBrace.iEndIndex = closeBrace.iStartIndex + brace.OtherBrace.Length;

-

-                      if (source.Braces == null) {

-                        source.Braces = new List<TextSpan[]>();

-                      }

-                      source.Braces.Add(new TextSpan[2] { openBrace, closeBrace });

-                    }

+                    //TokenStack braces = parser.Context.OpenBraces;

+                    //foreach (Token brace in braces) {

+                    //  if (brace.OtherBrace == null) continue;

+                    //  TextSpan openBrace = new TextSpan();

+                    //  openBrace.iStartLine = brace.Location.Line;

+                    //  openBrace.iStartIndex = brace.Location.Column;

+                    //  openBrace.iEndLine = brace.Location.Line;

+                    //  openBrace.iEndIndex = openBrace.iStartIndex + brace.Length;

+

+                    //  TextSpan closeBrace = new TextSpan();

+                    //  closeBrace.iStartLine = brace.OtherBrace.Location.Line;

+                    //  closeBrace.iStartIndex = brace.OtherBrace.Location.Column;

+                    //  closeBrace.iEndLine = brace.OtherBrace.Location.Line;

+                    //  closeBrace.iEndIndex = closeBrace.iStartIndex + brace.OtherBrace.Length;

+

+                    //  if (source.Braces == null) {

+                    //    source.Braces = new List<TextSpan[]>();

+                    //  }

+                    //  source.Braces.Add(new TextSpan[2] { openBrace, closeBrace });

+                    //}

 

                     if (parser.Context.CurrentParseTree.ParserMessages.Count > 0) {

                       foreach (ParserMessage error in parser.Context.CurrentParseTree.ParserMessages) {

@@ -172,7 +173,15 @@ namespace Demo
                             //string result = reader.ReadToEnd();

                             //Console.Write(result);

 

-                            for (string line = reader.ReadLine(); !String.IsNullOrEmpty(line); line = reader.ReadLine()) {

+                            for (string line = reader.ReadLine(); line != null; line = reader.ReadLine()) {

+                              if (line == "") 

+                                continue;

+                              if (line.StartsWith("Boogie program verifier")) {

+                                if (!Regex.IsMatch(line, "Boogie program verifier finished with [0-9]* verified, 0 errors"))

+                                  AddErrorBecauseOfToolProblems(req, line);

+                                continue;

+                              }

+

                               // each line is of the form: "x,y,w,z:arbitrary text"                              

                               string[] numbersAndText = line.Split(':');

                               if (numbersAndText.Length != 2) {

@@ -188,10 +197,10 @@ namespace Demo
                               }

                               try {

                                 TextSpan span = new TextSpan();

-                                span.iStartLine = span.iEndLine = Int32.Parse(positions[0]);

-                                span.iStartIndex = Int32.Parse(positions[1]);

-                                span.iEndLine = Int32.Parse(positions[2]);

-                                span.iEndIndex = Int32.Parse(positions[3]);

+                                span.iStartLine = span.iEndLine = Math.Max(0, Int32.Parse(positions[0]) - 1);

+                                span.iStartIndex = Math.Max(0, Int32.Parse(positions[1]) - 1);

+                                span.iEndLine = Math.Max(0, Int32.Parse(positions[2]) - 1);

+                                span.iEndIndex = Math.Max(0, Int32.Parse(positions[3]) - 1);

                                 req.Sink.AddError(req.FileName, message, span, Severity.Error);

                               } catch (System.ArgumentNullException) {

                                 AddErrorBecauseOfToolProblems(req, "Couldn't parse numbers: '" + numbers + "'");

@@ -230,16 +239,16 @@ namespace Demo
 

                 case ParseReason.HighlightBraces:

                 case ParseReason.MemberSelectAndHighlightBraces:

-                    if (source.Braces != null)

-                    {

-                        foreach (TextSpan[] brace in source.Braces)

-                        {

-                            if (brace.Length == 2)

-                                req.Sink.MatchPair(brace[0], brace[1], 1);

-                            else if (brace.Length >= 3)

-                                req.Sink.MatchTriple(brace[0], brace[1], brace[2], 1);

-                        }

-                    }

+                    //if (source.Braces != null)

+                    //{

+                    //    foreach (TextSpan[] brace in source.Braces)

+                    //    {

+                    //        if (brace.Length == 2)

+                    //            req.Sink.MatchPair(brace[0], brace[1], 1);

+                    //        else if (brace.Length >= 3)

+                    //            req.Sink.MatchTriple(brace[0], brace[1], brace[2], 1);

+                    //    }

+                    //}

                     break;

             }

 

@@ -248,9 +257,9 @@ namespace Demo
 

         private static void AddErrorBecauseOfToolProblems(ParseRequest req, string msg) {

           TextSpan span = new TextSpan();

-          span.iStartLine = span.iEndLine = 1;

-          span.iStartIndex = 1;

-          span.iEndIndex = 2;

+          span.iStartLine = span.iEndLine = 0;

+          span.iStartIndex = 0;

+          span.iEndIndex = 5;

           req.Sink.AddError(req.FileName, msg, span, Severity.Error);

         }