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

Add expanded harness name to cargo kani arguments #103

Merged

Conversation

jaisnan
Copy link
Contributor

@jaisnan jaisnan commented Jun 1, 2023

Description of changes:

Kani's --harness returns a fuzzy output, which cause issues for the extension when there's multiple harnesses under the same name. With this patch, the extension passes the fully qualified name to kani as an argument, preventing more than one harness from being run.

Changes from PR

  1. Adds fully qualified name to the harness command
  2. Adds fully qualified name to concrete playback button and command
  3. Adds unit tests for the module name
  4. Refactors paths invoking the harness name to be more modular, like the cargo kani --test pathway.

Tackles #39

Testing:

  • How is this change tested? Manual and Unit tests

  • Is this a refactor change? Yes

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.

@jaisnan jaisnan marked this pull request as ready for review June 2, 2023 20:40
@jaisnan jaisnan changed the title Add fully qualified harness name to kani arguments Add fully qualified harness name to cargo kani arguments Jun 2, 2023
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.

src/model/kaniCommandCreate.ts Outdated Show resolved Hide resolved
src/test-tree/createTests.ts Outdated Show resolved Hide resolved
src/test/suite/sourceCodeParser.test.ts Outdated Show resolved Hide resolved
src/test/suite/sourceCodeParser.test.ts Outdated Show resolved Hide resolved
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.

This is a heuristic at this point, which is probably better than what we have.

I do recommend that you read: https://doc.rust-lang.org/book/ch07-01-packages-and-crates.html and https://doc.rust-lang.org/book/ch07-02-defining-modules-to-control-scope-and-privacy.html to understand the rules of how qualified names are built.

src/model/kaniCommandCreate.ts Outdated Show resolved Hide resolved
src/model/kaniCommandCreate.ts Show resolved Hide resolved
src/model/kaniCommandCreate.ts Show resolved Hide resolved
src/model/kaniCommandCreate.ts Show resolved Hide resolved
src/test-tree/createTests.ts Outdated Show resolved Hide resolved
@jaisnan jaisnan changed the title Add fully qualified harness name to cargo kani arguments Add expanded harness name to cargo kani arguments Jun 6, 2023
@jaisnan jaisnan merged commit 78e92c4 into model-checking:main Jun 6, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
No open projects
Status: Done
Development

Successfully merging this pull request may close these issues.

4 participants