diff options
| author |  stefanheule <unknown> | 2012-02-25 03:09:50 -0800 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-02-25 03:09:50 -0800 |
| commit | a52b43105b87605b70ee7d03a59d3f573a54fe6e (patch) | |
| tree | ecb0e0312094b8c558c5102237b2661a962220be /Chalice/src/main/scala/Translator.scala | |
| parent | 86f1f083c81dc9c2d90b60a80422310880fe5d26 (diff) | |
Chalice: (comment about translatePrecondition)
Diffstat (limited to 'Chalice/src/main/scala/Translator.scala')
| -rw-r--r-- | Chalice/src/main/scala/Translator.scala | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala index a2cb2d00..ca319019 100644 --- a/Chalice/src/main/scala/Translator.scala +++ b/Chalice/src/main/scala/Translator.scala @@ -302,6 +302,10 @@ class Translator { }
}
+ /** Get the definition of a precondition with the pure assertions only (i.e.
+ * only functional specifications such as heap properties, assertsions about
+ * variables, etc).
+ */
def translatePrecondition(pre: Expression): Expression = {
desugar(pre) transform {
case _:PermissionExpr => Some(BoolLiteral(true))
|