Skip to content

Commit

Permalink
Remove comment about kani-driver code.
Browse files Browse the repository at this point in the history
  • Loading branch information
adpaco-aws committed Jun 15, 2023
1 parent a699fd5 commit 27bd4f4
Showing 1 changed file with 1 addition and 4 deletions.
5 changes: 1 addition & 4 deletions rfc/src/rfcs/0007-global-conditions.md
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ However, we may consider adding a new subsection `Global conditions` to the `Ref
## Detailed Design

The only component to be modified is `kani-driver` since that's where verification results are built and determined.
But given the growing complexity of `kani-driver`, we should consider moving the logic related to global conditions onto a new crate.
But we should consider moving this logic into another crate.

We don't need new dependencies.
The corner cases will depend on the specific global conditions to be implemented.
Expand All @@ -78,9 +78,6 @@ As mentioned earlier, we're proposing this change to help users understand globa
In many cases, global conditions empower users to write harnesses which weren't possible to write before.
As an example, the `#[kani::should_panic]` attribute allowed users to write harnesses expecting panic-related failures.

On the other hand, this proposal will add a significant amount of code to `kani-driver`.
It's possible to move some code into another crate, but even then some code will be added in `kani-driver`.

Also, we don't really know if more global conditions will be requested in the future.
We may consider discarding this proposal and waiting for the next feature that can be implemented as a global condition to be requested.

Expand Down

0 comments on commit 27bd4f4

Please sign in to comment.