Merge pull request #772 from viperproject/meilers_allow_pure_inexhale

Remove warnings for pure in- or exhales
viperproject · Feb 14, 2024 · dc2616a · dc2616a
2 parents eec8dd0 + 7fce62b
commit dc2616a
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/src/main/scala/viper/silver/parser/Resolver.scala b/src/main/scala/viper/silver/parser/Resolver.scala
@@ -226,14 +226,10 @@ case class TypeChecker(names: NameAnalyser) {
         checkMagicWand(e)
       case PExhale(_, e) =>
         check(e, Impure)
-        if (e.typ == Bool)
-          messages ++= FastMessaging.message(stmt, "found `exhale` of pure boolean expression, use `assert` instead", error = false)
       case PAssert(_, e) =>
         check(e, Impure)
       case PInhale(_, e) =>
         check(e, Impure)
-        if (e.typ == Bool)
-          messages ++= FastMessaging.message(stmt, "found `inhale` of pure boolean expression, use `assume` instead", error = false)
       case PAssume(_, e) =>
         check(e, Impure)
       case assign: PAssign =>