Commit 351e958
Carolyn Zech
Fix check_cast harness (#86)
Modifies the `check_cast` harness to:
- Be a proof instead of a proof for contract
- Remove the generic type parameter
Currently, Kani doesn't run this harness. (See the
[log](https://github.com/model-checking/verify-rust-std/actions/runs/10887990165/job/30211482361?pr=85)
from a recent PR). It doesn't run the harness because it has a generic
type parameter, and Kani's error handling for contract proofs doesn't
check for this condition. (PR to fix is
[here](model-checking/kani#3522)). Once we
remove the generic type parameter so that the harness runs, Kani
complains that we can't run it as a proof for contract because there are
no contracts, so we make it a regular proof instead.
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.1 parent 149f6dd commit 351e958
1 file changed
+2
-2
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
284 | 284 | | |
285 | 285 | | |
286 | 286 | | |
287 | | - | |
288 | | - | |
| 287 | + | |
| 288 | + | |
289 | 289 | | |
290 | 290 | | |
291 | 291 | | |
| |||
0 commit comments