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

Fix issue 2589 #2787

Merged
merged 5 commits into from
Sep 25, 2023
Merged

Fix issue 2589 #2787

merged 5 commits into from
Sep 25, 2023

Conversation

JustusAdam
Copy link
Contributor

@JustusAdam JustusAdam commented Sep 22, 2023

Description of changes:

This addresses #2589 by providing a better error message that contains both the trait that failed to resolve and the type which does not implement it.

Before:

error: internal compiler error: kani-compiler/src/kani_middle/reachability.rs:471:29: Unexpected polymorphic constant: Unevaluated(UnevaluatedConst { def: DefId(0:6 ~ issue_2589[1b49]::Dummy::TRUE), args: [Adt(std::string::String, [])], promoted: None }, bool) Unevaluated(UnevaluatedConst { def: DefId(0:6 ~ issue_2589[1b49]::Dummy::TRUE), args: [T/#0], promoted: None }, bool)

thread 'rustc' panicked at /rustc/65ea825f4021eaf77f1b25139969712d65b435a4/compiler/rustc_errors/src/lib.rs:995:33:
Box<dyn Any>
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] no current codegen item.
[Kani] no current codegen location.
error: aborting due to previous error; 1 warning emitted

After:

error: Type `std::string::String` does not implement trait `Dummy`. This is likely because `original` is used as a stub but its generic bounds are not being met.

error: aborting due to previous error; 1 warning emitted

Resolved issues:

Resolves #2589

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

Testing:

  • How is this change tested?

  • Is this a refactor change?

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@JustusAdam JustusAdam marked this pull request as ready for review September 23, 2023 17:40
@JustusAdam JustusAdam requested a review from a team as a code owner September 23, 2023 17:40
Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
Copy link
Contributor

@feliperodri feliperodri left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM.

@JustusAdam JustusAdam merged commit e95a7bb into model-checking:main Sep 25, 2023
12 checks passed
@JustusAdam JustusAdam deleted the issue-2589 branch September 25, 2023 17:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Invalid stub cause different ICE while monomorphizing the code
2 participants