Improve error reporting for some parsing and typechecking errors

src/main/scala/viper/silver/parser/ParseAst.scala

@@ -795,6 +795,7 @@ class PBinExp(val left: PExp, val opName: String, val right: PExp)(val pos: (Pos
   }
 
   override def hashCode(): Int = viper.silver.utility.Common.generateHashCode(left, opName, right)
+  override def toString(): String = s"PBinExp($left,$opName,$right)"
 }
 
 object PBinExp {
@@ -1319,7 +1320,7 @@ case class PGoto(targets: PIdnUse)(val pos: (Position, Position)) extends PStmt
 
 case class PTypeVarDecl(idndef: PIdnDef)(val pos: (Position, Position)) extends PLocalDeclaration
 
-case class PDefine(idndef: PIdnDef, parameters: Option[Seq[PIdnDef]], body: PNode)(val pos: (Position, Position)) extends PStmt with PLocalDeclaration
+case class PDefine(idndef: PIdnDef, parameters: Option[Seq[PIdnDef]], body: PNode)(val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PStmt with PLocalDeclaration
 
 case class PSkip()(val pos: (Position, Position)) extends PStmt
 
@@ -1410,9 +1411,9 @@ case class PProgram(imports: Seq[PImport], macros: Seq[PDefine], domains: Seq[PD
 
 abstract class PImport() extends PNode
 
-case class PLocalImport(file: String)(val pos: (Position, Position)) extends PImport()
+case class PLocalImport(file: String)(val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PImport()
 
-case class PStandardImport(file: String)(val pos: (Position, Position)) extends PImport()
+case class PStandardImport(file: String)(val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PImport()
 
 case class PMethod(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl], formalReturns: Seq[PFormalReturnDecl], pres: Seq[PExp], posts: Seq[PExp], body: Option[PStmt])
                   (val pos: (Position, Position), val annotations: Seq[(String, Seq[String])]) extends PSingleMember {

src/main/scala/viper/silver/parser/Transformer.scala

@@ -141,14 +141,14 @@ object Transformer {
         case p@PVars(vars, init) => PVars(vars map go, init map go)(p.pos)
         case p@PLabel(idndef, invs) => PLabel(go(idndef), invs map go)(p.pos)
         case p@PGoto(target) => PGoto(go(target))(p.pos)
-        case p@PDefine(idndef, optArgs, exp) => PDefine(go(idndef), optArgs map (_ map go) , go(exp))(p.pos)
+        case p@PDefine(idndef, optArgs, exp) => PDefine(go(idndef), optArgs map (_ map go) , go(exp))(p.pos, p.annotations)
         case p@PLet(exp, nestedScope) => PLet(go(exp), go(nestedScope))(p.pos)
         case p@PLetNestedScope(idndef, body) => PLetNestedScope(go(idndef), go(body))(p.pos)
         case _: PSkip => parent
 
         case p@PProgram(files, macros, domains, fields, functions, predicates, methods, extensions, errors) => PProgram(files, macros map go, domains map go, fields map go, functions map go, predicates map go, methods map go, extensions map go, errors)(p.pos)
-        case p@PLocalImport(file) => PLocalImport(file)(p.pos)
-        case p@PStandardImport(file) => PStandardImport(file)(p.pos)
+        case p@PLocalImport(file) => PLocalImport(file)(p.pos, p.annotations)
+        case p@PStandardImport(file) => PStandardImport(file)(p.pos, p.annotations)
         case p@PMethod(idndef, formalArgs, formalReturns, pres, posts, body) => PMethod(go(idndef), formalArgs map go, formalReturns map go, pres map go, posts map go, body map go)(p.pos, p.annotations)
         case p@PDomain(idndef, typVars, funcs, axioms, interp) => PDomain(go(idndef), typVars map go, funcs map go, axioms map go, interp)(p.pos, p.annotations)
         case p@PFields(fields) => PFields(fields map go)(p.pos, p.annotations)

src/test/resources/all/issues/silver/0105-1.vpr

@@ -7,8 +7,8 @@ domain Process {
   function p_ping(): Process
   function p_ping_omega(): Process
 
-  //:: ExpectedOutput(parser.error)
   axiom ping_axiom_2_post_TWO {
+    //:: ExpectedOutput(parser.error)
     (exists  :: p_ping_omega() == p_seq(p_ping_omega(), p_ping()))
   }
 }

src/test/resources/all/issues/silver/0105.vpr

@@ -7,8 +7,8 @@ domain Process {
   function p_ping(): Process
   function p_ping_omega(): Process
 
-   //:: ExpectedOutput(parser.error)
    axiom ping_axiom_2_post {
+     //:: ExpectedOutput(parser.error)
      (forall  :: p_ping_omega() == p_seq(p_ping_omega(), p_ping()))
    }05
 }

src/test/resources/all/parsing/assign_ambig.vpr

@@ -0,0 +1,7 @@
+field f: Bool
+method bar(a: Bool, b: Seq[Ref])
+    requires |b| > 0 && acc(b[0].f)
+{
+  assume a
+  (b[..1][0]).f := a
+}

src/test/resources/all/parsing/typed_call_ambig.vpr

@@ -0,0 +1,8 @@
+domain huh {
+    function myfun(b: Bool): Bool
+}
+
+method m()
+{
+  assert (myfun(forall i: Int :: i > 0 || i <= 0)) || true
+}

src/test/resources/all/parsing/typed_call_ambig2.vpr

@@ -0,0 +1,14 @@
+//:: IgnoreFile(/Carbon/issue/488/)
+
+domain huh {
+    function myfun(b: Bool): Bool
+}
+
+field f: Int
+
+method m()
+{
+  var x: Ref, y: Ref
+  inhale acc(x.f) && (acc(x.f) --* acc(y.f))
+  assert (myfun(applying (acc(x.f) --* acc(y.f)) in y.f == 0)) || true
+}