Skip to content

Conversation

@celinval
Copy link
Contributor

Description of changes:

The per-reachability analysis can cause a big penalty when assessing a project that has lots of tests.

Change that for now.

Despite that improvement, assessing the firecracker still takes a long time, even with --only-codegen, due to the number of calls done to goto-cc. Thus, don't use assess here.

Resolved issues:

N/A

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

Due to #2472, we need a specialized name for each test harness. For now, we just replicate the model for each harness.

Testing:

  • How is this change tested?

  • Is this a refactor change?

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.

The per-reachability analysis can cause a big penalty when assessing a
project that has lots of tests.

Change that for now.

Despite that improvement, assessing the firecracker still takes a long
time, even with --only-codegen, due to the number of calls done to
goto-cc. Thus, don't use assess here.
@celinval celinval requested a review from a team as a code owner May 25, 2023 22:29
@celinval celinval enabled auto-merge (squash) May 26, 2023 17:16
@celinval celinval merged commit 3d9bfe0 into model-checking:main May 26, 2023
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.

2 participants