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

Print Kani version #2619

Merged
merged 10 commits into from
Jul 26, 2023
Merged

Print Kani version #2619

merged 10 commits into from
Jul 26, 2023

Conversation

adpaco-aws
Copy link
Contributor

@adpaco-aws adpaco-aws commented Jul 23, 2023

Description of changes:

Dusting this off since it'd be great to have for next release.

This PR changes Kani so it prints its version and the invocation type/mode as
Kani Rust Verifier <version> (<invocation>) where <invocation> is either standalone or cargo plugin.

Please note that I'm leaving development version information for later in #2617. We can continue the discussion we started in #2571 here.

Resolved issues:

Resolves #2570

Testing:

  • How is this change tested? Two 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.

@adpaco-aws adpaco-aws requested a review from a team as a code owner July 23, 2023 22:35
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

Shouldn't we print the same blob for all sub-commands as well?

kani-driver/build.rs Outdated Show resolved Hide resolved
kani-driver/src/main.rs Outdated Show resolved Hide resolved
kani-driver/src/version.rs Show resolved Hide resolved
kani-driver/src/version.rs Outdated Show resolved Hide resolved
@adpaco-aws
Copy link
Contributor Author

Addressed all comments.

Shouldn't we print the same blob for all sub-commands as well?

To be honest, this wasn't clear to me. Guessing it's because I'd really like assess to be a tool rather than a sub-command...

Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

Thanks

@adpaco-aws adpaco-aws enabled auto-merge (squash) July 26, 2023 11:50
@adpaco-aws adpaco-aws merged commit bbffc45 into model-checking:main Jul 26, 2023
adpaco-aws added a commit to zhassan-aws/kani that referenced this pull request Jul 26, 2023
@adpaco-aws adpaco-aws mentioned this pull request Jul 26, 2023
4 tasks
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.

Output - Kani version
2 participants