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

Support crate-type=bin and --tests with dependencies #1260

Merged
merged 6 commits into from
Jun 8, 2022

Conversation

tedinski
Copy link
Contributor

@tedinski tedinski commented Jun 7, 2022

Description of changes:

This causes kani-compiler to emit rlib files. Cargo expects these to exist in certain circumstances, such as for the dependencies of --crate-type=bin (including the binaries built by --tests)

Resolved issues:

Resolves #1216
Resolves #473

Newly opened #1258

Call-outs:

Testing:

  • How is this change tested? new tests

  • Is this a refactor change? no

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.

@tedinski tedinski requested a review from a team as a code owner June 7, 2022 23:10
Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

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

Looks great! Thanks for figuring this out, @tedinski!

Only have a few minor comments.

@@ -11,6 +11,15 @@ pub fn alter_extension(path: &Path, ext: &str) -> PathBuf {
path.with_extension(ext)
}

/// Attempt to guess the rlib name for rust source file
pub fn guess_rlib_name(path: &Path) -> PathBuf {
Copy link
Contributor

Choose a reason for hiding this comment

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

Is there a more reliable way to get the rlib name?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Not as far as I can tell, will at least add a quick ref to rustc sources...

tests/cargo-kani/cargo-tests-dir/src/lib.rs Show resolved Hide resolved
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
kani-compiler/src/codegen_cprover_gotoc/archive.rs Outdated Show resolved Hide resolved
let mut entries = Vec::new();

for (entry_name, entry) in self.entries {
// FIXME only read the symbol table of the object files to avoid having to keep all
Copy link
Contributor

Choose a reason for hiding this comment

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

Do we want a tracking issue for the "FIXMEs" here?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

This is not our fixme, it's from the upstream file. I didn't remove it because I wanted to modify the file as minimally as possible.

@tedinski tedinski merged commit 71de074 into model-checking:main Jun 8, 2022
@tedinski tedinski deleted the crate-type-bin branch June 8, 2022 22:50
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.

cargo kani --tests doesn't work with dependencies Cargo rmc fails with crate-type bin (and tests)
3 participants