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

@extern functions preconditions wiped out in presence of unsupported constructs #1274

Closed
mario-bucev opened this issue May 27, 2022 · 0 comments · Fixed by #1277
Closed

@extern functions preconditions wiped out in presence of unsupported constructs #1274

mario-bucev opened this issue May 27, 2022 · 0 comments · Fixed by #1277
Labels

Comments

@mario-bucev
Copy link
Collaborator

In the following snippet, the call to ext2 (in test2) does not generate a VC for the precondition of ext2:

import stainless.annotation._

object ExternRequires {

  @extern
  def ext1(x: Int): Unit = {
    require(x >= 10)
    ()
  }

  @extern
  def ext2(x: Int): Unit = {
    require(x >= 10)
    val s = x.toString // Unsupported construct
    ()
  }

  def test1: Unit = ext1(0) // Invalid (as expected)

  def test2: Unit = ext2(0) // Should fail, but no VC gets generated
}

It seems that having constructs that Stainless does not support leads to having the require clauses being dropped (the postconditions are unaffected, though)

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

Successfully merging a pull request may close this issue.

1 participant