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

Errors caused by refute statement inside of loop with goto #773

Closed
bruggerl opened this issue Nov 10, 2023 · 2 comments
Closed

Errors caused by refute statement inside of loop with goto #773

bruggerl opened this issue Nov 10, 2023 · 2 comments
Assignees
Labels
bug Something isn't working unsoundness

Comments

@bruggerl
Copy link
Contributor

When verifying the following method, Silicon throws an exception (leading to a "Verification aborted exceptionally" error) and also falsely reports that the refute statement does not hold:

method test()
{
    label l0
    refute false
    goto l0
}
@bruggerl bruggerl added bug Something isn't working unsoundness labels Nov 10, 2023
@marcoeilers
Copy link
Contributor

The refute plugin generates this code, which looks fine to me but makes Silicon crash:

method test()
{
  {
    label l0
    {
      var __plugin_refute_nondet1: Bool
      if (__plugin_refute_nondet1) {
        assert false
        inhale false
      }
    }
    goto l0
  }
}

@marcoeilers
Copy link
Contributor

Fixed in #774.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working unsoundness
Projects
None yet
Development

No branches or pull requests

2 participants