Skip to content

Consistency checks to forbid inhale-exhale-assertions in function preconditions and predicate bodies #828

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
marcoeilers wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

Consistency checks to forbid inhale-exhale-assertions in function preconditions and predicate bodies #828

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions src/main/scala/viper/silver/ast/Program.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -362,6 +362,7 @@ case class Field(name: String, typ: Type)(val pos: Position = NoPosition, val in
case class Predicate(name: String, formalArgs: Seq[LocalVarDecl], body: Option[Exp])(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends Location {
override lazy val check : Seq[ConsistencyError] =
(if (body.isDefined) Consistency.checkNonPostContract(body.get) ++ Consistency.checkWildcardUsage(body.get, false) else Seq()) ++
(if (body.isDefined) Consistency.checkNoInhaleExhale(body.get, "predicates") else Seq()) ++
(if (body.isDefined && !Consistency.noOld(body.get))
Seq(ConsistencyError("Predicates must not contain old expressions.",body.get.pos))
else Seq()) ++
Expand Down Expand Up @@ -455,6 +456,7 @@ case class Function(name: String, formalArgs: Seq[LocalVarDecl], typ: Type, pres
posts.flatMap(p=>{ if(!Consistency.noOld(p))
Seq(ConsistencyError("Function post-conditions must not have old expressions.", p.pos)) else Seq()}) ++
(pres ++ posts).flatMap(Consistency.checkNoPermForpermExceptInhaleExhale) ++
(pres flatMap (pre => Consistency.checkNoInhaleExhale(pre, "function preconditions"))) ++
(pres ++ posts ++ body.toSeq).flatMap(Consistency.checkWildcardUsage(_, true)) ++
(if(!(body forall (_ isSubtype typ))) Seq(ConsistencyError("Type of function body must match function type.", pos)) else Seq() ) ++
(posts flatMap (p => if (!Consistency.noPerm(p) || !Consistency.noForPerm(p)) Seq(ConsistencyError("perm and forperm expressions are not allowed in function postconditions", p.pos)) else Seq() )) ++
Expand Down
8 changes: 8 additions & 0 deletions src/main/scala/viper/silver/ast/utility/Consistency.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -161,6 +161,14 @@ object Consistency {
})
}

/** Checks that no inhale/exhale assertions occur in the given node. */
def checkNoInhaleExhale(e: Exp, locationDescription: String) : Seq[ConsistencyError] = {
e.deepCollect({
case ie: InhaleExhaleExp =>
ConsistencyError(s"Inhale-exhale expressions are not allowed in ${locationDescription}.", ie.pos)
})
}

/** Check all properties required for a function body. */
def checkFunctionBody(e: Exp) : Seq[ConsistencyError] = {
var s = Seq.empty[ConsistencyError]
Expand Down
Loading