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

Failure on cargo-ui/unstable-attr/invalid regression #2530

Closed
karkhaz opened this issue Jun 15, 2023 · 0 comments · Fixed by #2536
Closed

Failure on cargo-ui/unstable-attr/invalid regression #2530

karkhaz opened this issue Jun 15, 2023 · 0 comments · Fixed by #2536
Labels
[C] Bug This is a bug. Something isn't working.

Comments

@karkhaz
Copy link
Contributor

karkhaz commented Jun 15, 2023

I tried running the regression suite just before releasing on an M1 macOS host:

RUST_BACKTRACE=1 ./scripts/kani-regression.sh

using tag 0.30.0, i.e. tip of this PR.

One test failed:

---- [cargo-kani] cargo-ui/unstable-attr/invalid/expected stdout ----

error: test failed: expected output to contain the line(s):
error: failed to parse `#[kani::unstable]`: missing `feature` field
src/lib.rs
|
| #[kani::unstable(
| ^^^^^^^^^^^^^^^^^^
|
= note: expected format: #[kani::unstable(feature="<IDENTIFIER>", issue="<ISSUE>", reason="<DESCRIPTION>")]
= note: this error originates in the attribute macro `kani::unstable` (in Nightly builds, run with -Z macro-backtrace for more info)
status: exit status: 1
command: cd "/private/tmp/kani-0.30.0/tests/cargo-ui/unstable-attr/invalid" && "cargo" "kani" "--target-dir" "/private/tmp/kani-0.30.0/build/tests/cargo-ui/unstable-attr/invalid/expected/target"
stdout:
------------------------------------------
error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `feature`
  --> src/lib.rs:17:1
   |
17 | #[kani::unstable(feature, issue)]
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: expected format: #[kani::unstable(feature="<IDENTIFIER>", issue="<ISSUE>", reason="<DESCRIPTION>")]
   = note: this error originates in the attribute macro `kani::unstable` (in Nightly builds, run with -Z macro-backtrace for more info)

error: internal compiler error: Kani unexpectedly panicked at panicked at 'expected well formed unstable attribute, but found: UnstableAttrParseError { reason: "expected \"key = value\" pair, but found `feature`", attr: Attribute { kind: Normal(NormalAttr { item: AttrItem { path: Path { span: src/lib.rs:17:1: 17:34 (#13), segments: [PathSegment { ident: kanitool#13, id: NodeId(26), args: None }, PathSegment { ident: unstable#13, id: NodeId(27), args: None }], tokens: None }, args: Delimited(DelimArgs { dspan: DelimSpan { open: src/lib.rs:17:1: 17:34 (#13), close: src/lib.rs:17:1: 17:34 (#13) }, delim: Parenthesis, tokens: TokenStream([Token(Token { kind: Ident("feature", false), span: src/lib.rs:17:18: 17:25 (#0) }, Joint), Token(Token { kind: Comma, span: src/lib.rs:17:25: 17:26 (#0) }, Alone), Token(Token { kind: Ident("issue", false), span: src/lib.rs:17:27: 17:32 (#0) }, Alone)]) }), tokens: None }, tokens: None }), id: AttrId(102), style: Outer, span: src/lib.rs:17:1: 17:34 (#13) } }', kani-compiler/src/kani_middle/attributes.rs:154:21.

error: Failed to compile `invalid` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at 'expected well formed unstable attribute, but found: UnstableAttrParseError { reason: "expected \"key = value\" pair, but found `feature`", attr: Attribute { kind: Normal(NormalAttr { item: AttrItem { path: Path { span: src/lib.rs:17:1: 17:34 (#13), segments: [PathSegment { ident: kanitool#13, id: NodeId(26), args: None }, PathSegment { ident: unstable#13, id: NodeId(27), args: None }], tokens: None }, args: Delimited(DelimArgs { dspan: DelimSpan { open: src/lib.rs:17:1: 17:34 (#13), close: src/lib.rs:17:1: 17:34 (#13) }, delim: Parenthesis, tokens: TokenStream([Token(Token { kind: Ident("feature", false), span: src/lib.rs:17:18: 17:25 (#0) }, Joint), Token(Token { kind: Comma, span: src/lib.rs:17:25: 17:26 (#0) }, Alone), Token(Token { kind: Ident("issue", false), span: src/lib.rs:17:27: 17:32 (#0) }, Alone)]) }), tokens: None }, tokens: None }), id: AttrId(102), style: Outer, span: src/lib.rs:17:1: 17:34 (#13) } }', kani-compiler/src/kani_middle/attributes.rs:154:21.



------------------------------------------
stderr:
------------------------------------------
   Compiling invalid v0.1.0 (/private/tmp/kani-0.30.0/tests/cargo-ui/unstable-attr/invalid)
thread 'rustc' panicked at 'expected well formed unstable attribute, but found: UnstableAttrParseError { reason: "expected \"key = value\" pair, but found `feature`", attr: Attribute { kind: Normal(NormalAttr { item: AttrItem { path: Path { span: src/lib.rs:17:1: 17:34 (#13), segments: [PathSegment { ident: kanitool#13, id: NodeId(26), args: None }, PathSegment { ident: unstable#13, id: NodeId(27), args: None }], tokens: None }, args: Delimited(DelimArgs { dspan: DelimSpan { open: src/lib.rs:17:1: 17:34 (#13), close: src/lib.rs:17:1: 17:34 (#13) }, delim: Parenthesis, tokens: TokenStream([Token(Token { kind: Ident("feature", false), span: src/lib.rs:17:18: 17:25 (#0) }, Joint), Token(Token { kind: Comma, span: src/lib.rs:17:25: 17:26 (#0) }, Alone), Token(Token { kind: Ident("issue", false), span: src/lib.rs:17:27: 17:32 (#0) }, Alone)]) }), tokens: None }, tokens: None }), id: AttrId(102), style: Outer, span: src/lib.rs:17:1: 17:34 (#13) } }', kani-compiler/src/kani_middle/attributes.rs:154:21
stack backtrace:
   0: _rust_begin_unwind
   1: core::panicking::panic_fmt
   2: kani_compiler::kani_middle::attributes::check_unstable_features
             at /private/tmp/kani-0.30.0/kani-compiler/src/kani_middle/attributes.rs:154:21
   3: kani_compiler::kani_middle::check_reachable_items
             at /private/tmp/kani-0.30.0/kani-compiler/src/kani_middle/mod.rs:74:13
   4: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items
             at /private/tmp/kani-0.30.0/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:94:9
   5: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
             at /private/tmp/kani-0.30.0/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:243:25
   6: rustc_interface::passes::start_codegen
   7: <rustc_middle::ty::context::GlobalCtxt>::enter::<<rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_span::ErrorGuaranteed>>
   8: <rustc_interface::queries::Queries>::ongoing_codegen
   9: <rustc_interface::interface::Compiler>::enter::<rustc_driver_impl::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_span::ErrorGuaranteed>>
  10: <scoped_tls::ScopedKey<rustc_span::SessionGlobals>>::set::<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_driver_impl::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_span::ErrorGuaranteed>>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose 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: could not compile `invalid` (lib) due to 2 previous errors

------------------------------------------



failures:
    [cargo-kani] cargo-ui/unstable-attr/invalid/expected

test result: FAILED. 0 passed; 1 failed; 28 ignored; 0 measured; 0 filtered out; finished in 1.60s

Some tests failed in compiletest suite=cargo-ui mode=cargo-kani host=(none) target=(none
@karkhaz karkhaz added the [C] Bug This is a bug. Something isn't working. label Jun 15, 2023
@celinval celinval linked a pull request Jun 17, 2023 that will close this issue
4 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working.
Projects
No open projects
Status: No status
Development

Successfully merging a pull request may close this issue.

1 participant