Merge pull request #748 from viperproject/meilers_old_trigger_inference_proper

Cleaner implementation of fix for issue #740

Author: marcoeilers

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

@@ -195,10 +195,19 @@ abstract class GenericTriggerGenerator[Node <: AnyRef,
         else
           results.flatten
 
+      case e if modifyPossibleTriggers.isDefinedAt(e) => modifyPossibleTriggers.apply(e)(results)
+
       case _ => results.flatten
     })
   }
 
+  /*
+   * Hook for clients to add more cases to getFunctionAppsContaining to modify the found possible triggers.
+   * Used e.g. to wrap trigger expressions inferred from inside old-expression into old()
+   */
+  def modifyPossibleTriggers: PartialFunction[Node, Seq[Seq[(PossibleTrigger, Seq[Var], Seq[Var])]] =>
+    Seq[(PossibleTrigger, Seq[Var], Seq[Var])]] = PartialFunction.empty
+
   /* Precondition: if vars is non-empty then every (f,vs) pair in functs
    * satisfies the property that vars and vs are not disjoint.
    *

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

@@ -57,6 +57,19 @@ object Triggers {
       case LabelledOld(pt: PossibleTrigger, _) => pt.getArgs
       case _ => sys.error(s"Unexpected expression $e")
     }
+
+    override def modifyPossibleTriggers = {
+      case ast.Old(_) => results =>
+        results.flatten.map(t => {
+          val exp = t._1
+          (ast.Old(exp)(exp.pos, exp.info, exp.errT), t._2, t._3)
+        })
+      case ast.LabelledOld(_, l) => results =>
+        results.flatten.map(t => {
+          val exp = t._1
+          (ast.LabelledOld(exp, l)(exp.pos, exp.info, exp.errT), t._2, t._3)
+        })
+    }
   }
 
   /**