Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Make assume impure
Browse files Browse the repository at this point in the history
bruggerl committed Jul 23, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
1 parent c67e18f commit d8ca29f
Showing 2 changed files with 23 additions and 1 deletion.
Original file line number Diff line number Diff line change
@@ -19,7 +19,7 @@ trait GhostStmtTyping extends BaseTyping { this: TypeInfoImpl =>
case PAssert(exp) => assignableToSpec(exp)
case PRefute(exp) => assignableToSpec(exp)
case PExhale(exp) => assignableToSpec(exp)
case PAssume(exp) => assignableToSpec(exp) ++ isPureExpr(exp)
case PAssume(exp) => assignableToSpec(exp)
case PInhale(exp) => assignableToSpec(exp)
case PFold(acc) => wellDefFoldable(acc)
case PUnfold(acc) => wellDefFoldable(acc)
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/

package assumption

type person struct {
name string
age int
}

func f() {
p := &person{name: "Pereira", age: 12}
assume acc(p) // impure assume does not lead to contradiction
//:: ExpectedOutput(assert_error:assertion_error)
assert false
}

func g() {
p := &person{name: "Pereira", age: 12}
inhale acc(p) // inhale leads to contradiction
assert false
}

0 comments on commit d8ca29f

Please sign in to comment.