Skip to content
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.

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

non ghost assignment in ghost if-else block #420

Closed
LinoTelschow opened this issue Mar 6, 2022 · 0 comments · Fixed by #755 or #771
Closed

non ghost assignment in ghost if-else block #420

LinoTelschow opened this issue Mar 6, 2022 · 0 comments · Fixed by #755 or #771
Assignees

Comments

@LinoTelschow
Copy link
Contributor

Gobra verifies ghost if-else blocks that assign to non-ghost variables.
An example that verifies:

func foo() int {
    ghost bar := true
    var baz int
    ghost if bar {
        baz = 1
    } else {
        baz = 0
    }
    return baz
}

Configuration:
Gobra: 63ea747
silver: 7228e7144d41c91f02a70a68a93b6b3efae57d14
silicon: 22551b40509c381991a493da0108ea4c97fd602d
carbon: 4393d154a5ae24d994a0c2c578374bdd49c3a3b3
viperserver: 5907ce1744501b7949d25cc0d5356145431ab6f7

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
3 participants