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.

Sign up for GitHub

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

Jump to bottom

Kani driver crashes with cdylib and rlib #3569

Closed
zhassan-aws opened this issue Oct 4, 2024 · 1 comment · Fixed by #3576
Closed

Kani driver crashes with cdylib and rlib #3569

zhassan-aws opened this issue Oct 4, 2024 · 1 comment · Fixed by #3576
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed

Comments

@zhassan-aws
Copy link
Contributor

Steps to reproduce:

  1. cargo new --lib newbug
  2. cd newbug
  3. printf '\n[lib]\ncrate-type = ["cdylib", "rlib"]\n' >> Cargo.toml
  4. cargo kani

Output:

$ cargo kani
Kani Rust Verifier 0.55.0 (cargo plugin)
   Compiling newbug v0.1.0 (/home/ubuntu/examples/newbug)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.15s
thread 'main' panicked at kani-driver/src/call_cargo.rs:461:82:
called `Result::unwrap()` on an `Err` value: Error("expected value", line: 1, column: 1)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

with Kani version: f3ed5e8
@zhassan-aws zhassan-aws added [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed labels Oct 4, 2024
@zhassan-aws
Copy link
Contributor Author

Bisecting revealed 4f75199 as the culprit commit. The crash does not occur with the previous commit (9dc09e7).

@celinval celinval mentioned this issue Oct 7, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue Oct 7, 2024
@celinval
Fix issue when linking rlib + another library type (#3576)
21f4af9 
Invoking the native linker was overriding the `json` we create in Kani's
compiler. Thus, invoke the native linker first, then create the `json`
files.

Resolves #3569

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix issue when linking rlib + another library type celinval/kani-dev
1 participant
@zhassan-aws