quantified permissions on the right of a magic wand cause stack trace

[alexanderjsummers]

Using quantified permissions on the left of a wand seems OK, but on the RHS I get a stack trace. For example, for the program:

field val : Int

method foo(x:Set[Ref]) {
    package true --* forall r:Ref :: r != null ==> acc(r.val)
}

I get the following (slightly abridged):

Exception in thread "main" java.lang.RuntimeException: impure expression not caught in exhaleExt at scala.sys.package$.error(package.scala:27) at viper.carbon.modules.impls.DefaultWandModule.exhaleExtExp(DefaultWandModule.scala:339) at viper.carbon.modules.impls.DefaultWandModule.exhaleExt(DefaultWandModule.scala:329) at viper.carbon.modules.impls.DefaultWandModule.exhaleExt(DefaultWandModule.scala:320) at viper.carbon.modules.impls.DefaultWandModule.exhaleExt(DefaultWandModule.scala:320) at viper.carbon.modules.impls.DefaultWandModule.exec(DefaultWandModule.scala:309) at viper.carbon.modules.impls.DefaultWandModule.translatePackageBody(DefaultWandModule.scala:259) at viper.carbon.modules.impls.DefaultWandModule.translatePackage(DefaultWandModule.scala:238) at viper.carbon.modules.impls.DefaultStmtModule.simpleHandleStmt(DefaultStmtModule.scala:223) at viper.carbon.modules.impls.DefaultStmtModule.handleStmt(DefaultStmtModule.scala:94) at viper.carbon.modules.impls.DefaultStmtModule.$anonfun$translateStmt$5(DefaultStmtModule.scala:267) at viper.carbon.modules.impls.DefaultStmtModule.$anonfun$translateStmt$5$adapted(DefaultStmtModule.scala:264) at scala.collection.immutable.List.foreach(List.scala:333) at viper.carbon.modules.impls.DefaultStmtModule.translateStmt(DefaultStmtModule.scala:264) at viper.carbon.modules.impls.DefaultStmtModule.$anonfun$translateStmt$3(DefaultStmtModule.scala:252) at scala.collection.immutable.List.map(List.scala:246) at scala.collection.immutable.List.map(List.scala:79) at viper.carbon.modules.impls.DefaultStmtModule.translateStmt(DefaultStmtModule.scala:252) at viper.carbon.modules.impls.DefaultStmtModule.$anonfun$translateStmt$3(DefaultStmtModule.scala:252) at scala.collection.immutable.List.map(List.scala:246) at scala.collection.immutable.List.map(List.scala:79) at viper.carbon.modules.impls.DefaultStmtModule.translateStmt(DefaultStmtModule.scala:252) at viper.carbon.modules.impls.DefaultMainModule.translateMethodDecl(DefaultMainModule.scala:148) at viper.carbon.modules.impls.DefaultMainModule.$anonfun$translate$9(DefaultMainModule.scala:100) at scala.collection.immutable.List.flatMap(List.scala:293) at scala.collection.immutable.List.flatMap(List.scala:79) at viper.carbon.modules.impls.DefaultMainModule.translate(DefaultMainModule.scala:100) ....