Supporting mce on demand via annotation

Author: marcoeilers

src/main/scala/rules/ExecutionFlowController.scala

@@ -6,6 +6,7 @@
 
 package viper.silicon.rules
 
+import viper.silver.ast
 import viper.silicon.Config.ExhaleMode
 import viper.silicon.interfaces._
 import viper.silicon.logger.records.data.CommentRecord
@@ -129,7 +130,19 @@ object executionFlowController extends ExecutionFlowRules {
 
         val comLog = new CommentRecord("Retry", s0, v.decider.pcs)
         val sepIdentifier = v.symbExLog.openScope(comLog)
-        val temporaryMCE = Verifier.config.exhaleMode != ExhaleMode.Greedy
+        val temporaryMCE = s0.currentMember.map(_.info.getUniqueInfo[ast.AnnotationInfo]) match {
+          case Some(Some(ai)) if ai.values.contains("exhaleMode") =>
+            ai.values("exhaleMode") match {
+              case Seq("0") | Seq("greedy") =>
+                false
+              case Seq("1") | Seq("mce") | Seq("moreCompleteExhale") | Seq("2") | Seq("mceOnDemand") => true
+              case _ =>
+                // Invalid annotation was already reported when creating the initial state.
+                Verifier.config.exhaleMode != ExhaleMode.Greedy
+            }
+          case _ => Verifier.config.exhaleMode != ExhaleMode.Greedy
+        }
+
         action(s0.copy(retrying = true, retryLevel = s.retryLevel, moreCompleteExhale = temporaryMCE), v, (s1, r, v1) => {
           v1.symbExLog.closeScope(sepIdentifier)
           Q(s1.copy(retrying = false, moreCompleteExhale = s0.moreCompleteExhale), r, v1)

src/main/scala/verifier/DefaultMainVerifier.scala

@@ -306,7 +306,7 @@ class DefaultMainVerifier(config: Config,
     val mce = member.info.getUniqueInfo[ast.AnnotationInfo] match {
       case Some(ai) if ai.values.contains("exhaleMode") =>
         ai.values("exhaleMode") match {
-          case Seq("0") | Seq("greedy") =>
+          case Seq("0") | Seq("greedy") | Seq("2") | Seq("mceOnDemand") =>
             if (Verifier.config.counterexample.isSupplied)
               reporter report AnnotationWarning(s"Member ${member.name} has exhaleMode annotation that may interfere with counterexample generation.")
             false