Merge pull request #728 from viperproject/meilers_term_plugin_deactiv…

…e_flag

Do not perform new checks and imports if the termination plugin is deactivated...

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

@@ -153,6 +153,9 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
   }
 
   override def beforeTranslate(input: PProgram): PProgram = {
+    if (deactivated)
+      return input
+
     val allClauseTypes: Set[Any] = decreasesClauses.flatMap{
       case PDecreasesTuple(Seq(), _) => Seq(())
       case PDecreasesTuple(exps, _) => exps.map(e => e.typ match {
@@ -240,27 +243,29 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
   override def beforeVerify(input: Program): Program = {
     // Prevent potentially unsafe (mutually) recursive function calls in function postcondtions
     // for all functions that don't have a decreases clause
-    lazy val cycles = Functions.findFunctionCyclesViaOptimized(input, func => func.body.toSeq)
-    for (f <- input.functions) {
-      val hasDecreasesClause = (f.pres ++ f.posts).exists(p => p.shallowCollect {
-        case dc: DecreasesClause => dc
-      }.nonEmpty)
-      if (!hasDecreasesClause) {
-        val funcCycles = cycles.get(f)
-        val problematicFuncApps = f.posts.flatMap(p => p.shallowCollect {
-          case fa: FuncApp if fa.func(input) == f => fa
-          case fa: FuncApp if funcCycles.isDefined && funcCycles.get.contains(fa.func(input)) => fa
-        }).toSet
-        for (fa <- problematicFuncApps) {
-          val calledFunc = fa.func(input)
-          if (calledFunc == f) {
-            if (fa.args == f.formalArgs.map(_.localVar)) {
-              reportError(ConsistencyError(s"Function ${f.name} has a self-reference in its postcondition and must be proven to be well-founded. Use \"result\" instead to refer to the result of the function.", fa.pos))
+    if (!deactivated) {
+      lazy val cycles = Functions.findFunctionCyclesViaOptimized(input, func => func.body.toSeq)
+      for (f <- input.functions) {
+        val hasDecreasesClause = (f.pres ++ f.posts).exists(p => p.shallowCollect {
+          case dc: DecreasesClause => dc
+        }.nonEmpty)
+        if (!hasDecreasesClause) {
+          val funcCycles = cycles.get(f)
+          val problematicFuncApps = f.posts.flatMap(p => p.shallowCollect {
+            case fa: FuncApp if fa.func(input) == f => fa
+            case fa: FuncApp if funcCycles.isDefined && funcCycles.get.contains(fa.func(input)) => fa
+          }).toSet
+          for (fa <- problematicFuncApps) {
+            val calledFunc = fa.func(input)
+            if (calledFunc == f) {
+              if (fa.args == f.formalArgs.map(_.localVar)) {
+                reportError(ConsistencyError(s"Function ${f.name} has a self-reference in its postcondition and must be proven to be well-founded. Use \"result\" instead to refer to the result of the function.", fa.pos))
+              } else {
+                reportError(ConsistencyError(s"Function ${f.name} has a self-reference in its postcondition and must be proven to be well-founded. Add a \"decreases\" clause to prove well-foundedness.", fa.pos))
+              }
             } else {
-              reportError(ConsistencyError(s"Function ${f.name} has a self-reference in its postcondition and must be proven to be well-founded. Add a \"decreases\" clause to prove well-foundedness.", fa.pos))
+              reportError(ConsistencyError(s"Function ${f.name} has a call to mutually-recursive function ${calledFunc.name} in its postcondition and must be proven to be well-founded. Add a \"decreases\" clause to prove well-foundedness.", fa.pos))
             }
-          } else {
-            reportError(ConsistencyError(s"Function ${f.name} has a call to mutually-recursive function ${calledFunc.name} in its postcondition and must be proven to be well-founded. Add a \"decreases\" clause to prove well-foundedness.", fa.pos))
           }
         }
       }