Review changes

Author: JonasAlaif

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

@@ -367,48 +367,48 @@ trait Info {
 
 /** A default `Info` that is empty. */
 case object NoInfo extends Info {
-  override def comment = Nil
-  override def isCached = false
+  override val comment = Nil
+  override val isCached = false
 }
 
 /** A simple `Info` that contains a list of comments. */
 case class SimpleInfo(comment: Seq[String]) extends Info {
-  override def isCached = false
+  override val isCached = false
 }
 
 /** An `Info` instance for labelling a quantifier as auto-triggered. */
 case object AutoTriggered extends Info {
-  override def comment = Nil
-  override def isCached = false
+  override val comment = Nil
+  override val isCached = false
 }
 
 /** An `Info` instance for labelling a pre-verified AST node (e.g., via caching). */
 case object Cached extends Info {
-  override def comment = Nil
-  override def isCached = true
+  override val comment = Nil
+  override val isCached = true
 }
 
 /** An `Info` instance for labelling a node as synthesized. A synthesized node is one that
   * was not present in the original program that was passed to a Viper backend, such as nodes that
   * originate from an AST transformation.
   */
 case object Synthesized extends Info {
-  override def comment = Nil
-  override def isCached = false
+  override val comment = Nil
+  override val isCached = false
 }
 
 /** An `Info` instance for labelling an AST node which is expected to fail verification.
  * This is used by Silicon to avoid stopping verification.
 */
 abstract class FailureExpectedInfo extends Info {
-  override def comment = Nil
-  override def isCached = false
+  override val comment = Nil
+  override val isCached = false
 }
 
 /** An `Info` instance for composing multiple `Info`s together */
 case class ConsInfo(head: Info, tail: Info) extends Info {
-  override def comment = head.comment ++ tail.comment
-  override def isCached = head.isCached || tail.isCached
+  override val comment = head.comment ++ tail.comment
+  override val isCached = head.isCached || tail.isCached
 }
 
 /** Build a `ConsInfo` instance out of two `Info`s, unless the latter is `NoInfo` (which can be dropped) */

src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala

@@ -18,18 +18,18 @@ import viper.silver.verifier.errors.AssertFailed
 class RefutePlugin extends SilverPlugin with ParserPluginTemplate {
 
   /** Keyword used to define refute statements. */
-  private val RefuteKeyword: String = "refute"
+  private val refuteKeyword: String = "refute"
 
-  private var RefuteAsserts: Map[Position, Refute] = Map()
+  private var refuteAsserts: Map[Position, Refute] = Map()
 
   /** Parser for refute statements. */
   def refute[_: P]: P[PRefute] =
-    FP(keyword(RefuteKeyword) ~/ exp).map{ case (pos, e) => PRefute(e)(pos) }
+    FP(keyword(refuteKeyword) ~/ exp).map{ case (pos, e) => PRefute(e)(pos) }
 
   /** Add refute to the parser. */
   override def beforeParse(input: String, isImported: Boolean): String = {
     // Add new keyword
-    ParserExtension.addNewKeywords(Set[String](RefuteKeyword))
+    ParserExtension.addNewKeywords(Set[String](refuteKeyword))
     // Add new parser to the precondition
     ParserExtension.addNewStmtAtEnd(refute(_))
     input
@@ -42,36 +42,36 @@ class RefutePlugin extends SilverPlugin with ParserPluginTemplate {
   override def beforeVerify(input: Program): Program =
     ViperStrategy.Slim({
       case r@Refute(exp) => {
-        this.RefuteAsserts += (r.pos -> r)
+        this.refuteAsserts += (r.pos -> r)
         Seqn(Seq(
-          If(LocalVar(s"__plugin_refute_nondet${this.RefuteAsserts.size}", Bool)(r.pos),
+          If(LocalVar(s"__plugin_refute_nondet${this.refuteAsserts.size}", Bool)(r.pos),
             Seqn(Seq(
               Assert(exp)(r.pos, RefuteInfo),
               Inhale(BoolLit(false)(r.pos))(r.pos)
             ), Seq())(r.pos),
             Seqn(Seq(), Seq())(r.pos))(r.pos)
           ),
-          Seq(LocalVarDecl(s"__plugin_refute_nondet${this.RefuteAsserts.size}", Bool)(r.pos))
+          Seq(LocalVarDecl(s"__plugin_refute_nondet${this.refuteAsserts.size}", Bool)(r.pos))
         )(r.pos)
       }
     }).recurseFunc({
       case Method(_, _, _, _, _, body) => Seq(body)
     }).execute(input)
 
-  /** Remove refutation related errors and add RefuteAsserts that didn't report an error. */
+  /** Remove refutation related errors and add refuteAsserts that didn't report an error. */
   override def mapVerificationResult(input: VerificationResult): VerificationResult = {
     val errors: Seq[AbstractError] = (input match {
       case Success => Seq()
       case Failure(errors) => {
         errors.filter {
           case AssertFailed(a, _, _) if a.info == RefuteInfo => {
-            this.RefuteAsserts -= a.pos
+            this.refuteAsserts -= a.pos
             false
           }
           case _ => true
         }
       }
-    }) ++ this.RefuteAsserts.map(r => RefuteFailed(r._2, RefutationTrue(r._2.exp)))
+    }) ++ this.refuteAsserts.map(r => RefuteFailed(r._2, RefutationTrue(r._2.exp)))
     if (errors.length == 0) Success
     else Failure(errors)
   }

src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala

@@ -28,7 +28,7 @@ class TerminationPlugin(reporter: viper.silver.reporter.Reporter,
   /**
    * Keyword used to define decreases clauses
    */
-  private val DecreasesKeyword: String = "decreases"
+  private val decreasesKeyword: String = "decreases"
 
   /**
    * Parser for decreases clauses with following possibilities.
@@ -40,7 +40,7 @@ class TerminationPlugin(reporter: viper.silver.reporter.Reporter,
    * decreases *
    */
   def decreases[_: P]: P[PDecreasesClause] =
-    P(keyword(DecreasesKeyword) ~/ (decreasesWildcard | decreasesStar | decreasesTuple) ~ ";".?)
+    P(keyword(decreasesKeyword) ~/ (decreasesWildcard | decreasesStar | decreasesTuple) ~ ";".?)
   def decreasesTuple[_: P]: P[PDecreasesTuple] =
     FP(exp.rep(sep = ",") ~/ condition.?).map { case (pos, (a, c)) => PDecreasesTuple(a, c)(pos) }
   def decreasesWildcard[_: P]: P[PDecreasesWildcard] = FP("_" ~/ condition.?).map{ case (pos, c) => PDecreasesWildcard(c)(pos) }
@@ -53,7 +53,7 @@ class TerminationPlugin(reporter: viper.silver.reporter.Reporter,
    */
   override def beforeParse(input: String, isImported: Boolean): String = {
     // Add new keyword
-    ParserExtension.addNewKeywords(Set[String](DecreasesKeyword))
+    ParserExtension.addNewKeywords(Set[String](decreasesKeyword))
     // Add new parser to the precondition
     ParserExtension.addNewPreCondition(decreases(_))
     // Add new parser to the postcondition

src/main/scala/viper/silver/verifier/VerificationError.scala

@@ -155,8 +155,8 @@ trait ErrorMessage {
   def withNode(offendingNode: errors.ErrorNode = this.offendingNode) : ErrorMessage
 
   // Check if the offendingNode contains any `FailureExpectedInfo` info tags
-  def isExpected: Boolean = if (!offendingNode.isInstanceOf[Infoed]) false
-    else offendingNode.asInstanceOf[Infoed].info.getUniqueInfo[FailureExpectedInfo].isDefined
+  def isExpected: Boolean = offendingNode.isInstanceOf[Infoed] &&
+    offendingNode.asInstanceOf[Infoed].info.getUniqueInfo[FailureExpectedInfo].isDefined
 }
 
 trait VerificationError extends AbstractError with ErrorMessage {