Merge branch 'master' into fix-adt-postconditions

src/main/scala/viper/silver/ast/Position.scala

@@ -89,10 +89,10 @@ class IdentifierPosition(val file: Path, val start: HasLineColumn, val end: Opti
     file :: start :: end :: id :: Nil
 }
 
-object LineCol {
-  def apply(index: Int): (Int, Int) = {
+class LineCol(fp: FastParser) {
+  def getPos(index: Int): (Int, Int) = {
     // val Array(line, col) = ctx.input.prettyIndex(index).split(":").map(_.toInt)
-    val line_offset = FastParser._line_offset
+    val line_offset = fp._line_offset
     val result = java.util.Arrays.binarySearch(line_offset, index)
     if (result >= 0) {
       // Exact match

src/main/scala/viper/silver/ast/utility/Consistency.scala

@@ -8,7 +8,7 @@ package viper.silver.ast.utility
 
 import viper.silver.ast._
 import viper.silver.ast.utility.rewriter.Traverse
-import viper.silver.parser.FastParser
+import viper.silver.parser.{FastParser, FastParserCompanion}
 import viper.silver.verifier.ConsistencyError
 import viper.silver.{FastMessage, FastMessaging}
 
@@ -29,7 +29,7 @@ object Consistency {
     recordIfNot(suspect, !property, message)
 
   /** Names that are not allowed for use in programs. */
-  def reservedNames: Seq[String] = FastParser.keywords.toSeq
+  def reservedNames: Set[String] = FastParserCompanion.basicKeywords
 
   /** Returns true iff the string `name` is a valid identifier. */
   val identFirstLetter = "[a-zA-Z$_]"

src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala

@@ -53,39 +53,33 @@ object QuantifiedPermissions {
    *       e.g. someMethod.quantifiedFields.
    */
 
-  def quantifiedFields(root: Node, program: Program): collection.Set[Field] = {
+  def quantifiedFields(root: Member, program: Program): collection.Set[Field] = {
     val collected = mutable.LinkedHashSet[Field]()
     val visited = mutable.Set[Member]()
     val toVisit = mutable.Queue[Member]()
 
-    root match {
-      case m: Member => toVisit += m
-      case _ =>
-    }
+    toVisit += root
 
     toVisit ++= Nodes.referencedMembers(root, program)
 
-    quantifiedFields(toVisit, collected, visited, program)
+    quantifiedFields(toVisit, root, collected, visited, program)
 
     collected
   }
 
   /* TODO: See comment above about caching
    * TODO: Unify with corresponding code for fields
    */
-  def quantifiedPredicates(root: Node, program: Program): collection.Set[Predicate] = {
+  def quantifiedPredicates(root: Member, program: Program): collection.Set[Predicate] = {
     val collected = mutable.LinkedHashSet[Predicate]()
     val visited = mutable.Set[Member]()
     val toVisit = mutable.Queue[Member]()
 
-    root match {
-      case m: Member => toVisit += m
-      case _ =>
-    }
+    toVisit += root
 
     toVisit ++= Nodes.referencedMembers(root, program)
 
-    quantifiedPredicates(toVisit, collected, visited, program)
+    quantifiedPredicates(toVisit, root, collected, visited, program)
 
     collected
   }
@@ -98,44 +92,69 @@ object QuantifiedPermissions {
   }
 
   private def quantifiedFields(toVisit: mutable.Queue[Member],
+                               root: Member,
                                collected: mutable.LinkedHashSet[Field],
                                visited: mutable.Set[Member],
                                program: Program): Unit = {
 
     while (toVisit.nonEmpty) {
-      val root = toVisit.dequeue()
-
-      root visit {
-        case QuantifiedPermissionAssertion(_, _, acc: FieldAccessPredicate) =>
-          collected += acc.loc.field
-        case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case fa: FieldAccess => fa.field}
+      val currentRoot = toVisit.dequeue()
+
+      val relevantNodes: Seq[Node] = currentRoot match {
+        case m@Method(_, _, _, pres, posts, _) if m != root =>
+          // use only specification of called methods
+          pres ++ posts
+        case f@Function(_, _, _, pres, posts, _) if f != root=>
+          // use only specification of called functions
+          pres ++ posts
+        case _ => Seq(currentRoot)
       }
 
-      visited += root
+      visited += currentRoot
 
-      utility.Nodes.referencedMembers(root, program) foreach (m =>
-        if (!visited.contains(m)) toVisit += m)
+      for (n <- relevantNodes){
+        n visit {
+          case QuantifiedPermissionAssertion(_, _, acc: FieldAccessPredicate) =>
+            collected += acc.loc.field
+          case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case fa: FieldAccess => fa.field}
+        }
+        utility.Nodes.referencedMembers(n, program) foreach (m =>
+          if (!visited.contains(m)) toVisit += m)
+      }
     }
   }
 
   private def quantifiedPredicates(toVisit: mutable.Queue[Member],
+                                   root: Member,
                                    collected: mutable.LinkedHashSet[Predicate],
                                    visited: mutable.Set[Member],
                                    program: Program): Unit = {
 
     while (toVisit.nonEmpty) {
-      val root = toVisit.dequeue()
-
-      root visit {
-        case QuantifiedPermissionAssertion(_, _, acc: PredicateAccessPredicate) =>
-          collected += program.findPredicate(acc.loc.predicateName)
-        case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case pa: PredicateAccess => pa.loc(program)}
+      val currentRoot = toVisit.dequeue()
+
+      val relevantNodes: Seq[Node] = currentRoot match {
+        case m@Method(_, _, _, pres, posts, _) if m != root =>
+          // use only specification of called methods
+          pres ++ posts
+        case f@Function(_, _, _, pres, posts, _) if f != root =>
+          // use only specification of called functions
+          pres ++ posts
+        case _ => Seq(currentRoot)
       }
 
-      visited += root
+      visited += currentRoot
 
-      utility.Nodes.referencedMembers(root, program) foreach (m =>
-        if (!visited.contains(m)) toVisit += m)
+      for (n <- relevantNodes){
+        n visit {
+          case QuantifiedPermissionAssertion(_, _, acc: PredicateAccessPredicate) =>
+            collected += program.findPredicate(acc.loc.predicateName)
+          case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case pa: PredicateAccess => pa.loc(program)}
+        }
+        utility.Nodes.referencedMembers(n, program) foreach (m =>
+          if (!visited.contains(m)) toVisit += m)
+
+      }
     }
   }
 

src/main/scala/viper/silver/cfg/CfgTest.scala

@@ -36,7 +36,7 @@ object CfgTest {
   }
 
   private def parse[_: P](input: String, file: Path): Option[PProgram] = {
-    val result = FastParser.parse(input, file)
+    val result = new FastParser().parse(input, file)
     result match {
       case Parsed.Success(program@PProgram(_, _, _, _, _, _, _,_, errors), _) =>
         if (errors.isEmpty || errors.forall(_.isInstanceOf[ParseWarning])) Some(program)

src/main/scala/viper/silver/frontend/SilFrontend.scala

@@ -89,11 +89,12 @@ trait SilFrontend extends DefaultFrontend {
   /** For testing of plugin import feature */
   def defaultPluginCount: Int = defaultPlugins.size
 
+  protected val fp = new FastParser()
 
   protected var _plugins: SilverPluginManager = SilverPluginManager(defaultPlugins match {
     case Seq() => None
     case s => Some(s.mkString(":"))
-  })(reporter, logger, _config)
+  })(reporter, logger, _config, fp)
 
   def plugins: SilverPluginManager = _plugins
 
@@ -187,7 +188,7 @@ trait SilFrontend extends DefaultFrontend {
         val list = _config.plugin.toOption ++ defaultPlugins
         if (list.isEmpty) { None } else { Some(list.mkString(":")) }
       }
-      _plugins = SilverPluginManager(plugins)(reporter, logger, _config)
+      _plugins = SilverPluginManager(plugins)(reporter, logger, _config, fp)
     }
   }
 
@@ -233,7 +234,7 @@ trait SilFrontend extends DefaultFrontend {
     val file = _inputFile.get
     _plugins.beforeParse(input, isImported = false) match {
       case Some(inputPlugin) =>
-        val result = FastParser.parse(inputPlugin, file, Some(_plugins))
+        val result = fp.parse(inputPlugin, file, Some(_plugins))
           result match {
             case Parsed.Success(e@ PProgram(_, _, _, _, _, _, _, _, err_list), _) =>
               if (err_list.isEmpty || err_list.forall(p => p.isInstanceOf[ParseWarning])) {
@@ -243,7 +244,7 @@ trait SilFrontend extends DefaultFrontend {
               else Fail(err_list)
             case fail @ Parsed.Failure(_, index, extra) =>
               val msg = fail.trace().longAggregateMsg
-              val (line, col) = LineCol(index)
+              val (line, col) = fp.lineCol.getPos(index)
               Fail(List(ParseError(s"Expected $msg", SourcePosition(file, line, col))))
             //? val pos = extra.input.prettyIndex(index).split(":").map(_.toInt)
               //? Fail(List(ParseError(s"Expected $msg", SourcePosition(file, pos(0), pos(1)))))