Skip to content

Change Default UI to New Display and Add UI Test Suite#828

Merged
jaisnan merged 8 commits intomodel-checking:mainfrom
jaisnan:main
Feb 15, 2022
Merged

Change Default UI to New Display and Add UI Test Suite#828
jaisnan merged 8 commits intomodel-checking:mainfrom
jaisnan:main

Conversation

@jaisnan
Copy link
Copy Markdown
Contributor

@jaisnan jaisnan commented Feb 15, 2022

Description of changes:

  1. Change Default Value to the new display.
  2. Add test suite for the output formats.
  3. Change expected test suite to use old format as a temporary fix.
  4. Fix issue that dry-run didn't run well with expected

This is what calling kani on a file looks like by default -

Screen Shot 2022-02-15 at 1 13 29 AM

Call-outs:

To get the old output display, pass the flag --output-format old.

The new output display has an issue where --visualize doesn't act well with the --output-format flag. A fix is in the works.

Testing:

  • How is this change tested? Added a new test suite

  • 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.

@jaisnan jaisnan requested a review from a team as a code owner February 15, 2022 05:38
Copy link
Copy Markdown
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.

Sweet! Thanks

@zhassan-aws
Copy link
Copy Markdown
Contributor

Does it make sense to add --output-format old in compiletest itself to avoid having to modify that many files and updated the line numbers in the "expected" files?

@jaisnan
Copy link
Copy Markdown
Contributor Author

jaisnan commented Feb 15, 2022

Yes, that change makes sense, this is a temporary fix for now.

@tedinski
Copy link
Copy Markdown
Contributor

Does it make sense to add --output-format old in compiletest itself

This might make it difficult to write tests against other output formats. We'd have to see if multiple --output-format would mean last one wins on my new code, or if it'd just error.

@jaisnan jaisnan changed the title Change Default UI to New Display and Add Test Suite Change Default UI to New Display and Add UI Test Suite Feb 15, 2022
@jaisnan jaisnan merged commit 9360263 into model-checking:main Feb 15, 2022
tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 26, 2022
…g#828)

* Change expected files and add flags to explicitly demand old output

* Fix issues with dry run and change default output to regular style

* Add UI test suite
tedinski pushed a commit that referenced this pull request Apr 27, 2022
* Change expected files and add flags to explicitly demand old output

* Fix issues with dry run and change default output to regular style

* Add UI test suite
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.

4 participants