-
Notifications
You must be signed in to change notification settings - Fork 277
Open
Labels
KaniBugs or features of importance to Kani Rust VerifierBugs or features of importance to Kani Rust VerifierRust APIIssues pertaining to the CBCM Rust APIIssues pertaining to the CBCM Rust APIawsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC usersnew feature
Description
To enable Kani to be able to depend on the CBMC Rust API for a full verification run, without any need for interaction with the binary-based version of CBMC.
To do that, we would need to export the following flags to the C++ (and subsequently the Rust API):
-
--validate-goto-equation
-
--trace
-
--object-bits
-
--unwind
-
--bounds-check
-
--pointer-check
-
--div-by-zero-check
-
--float-overflow-check
-
--unwinding-assertions
-
--pointer-overflow-check
-
--pointer-primitive-check
Metadata
Metadata
Assignees
Labels
KaniBugs or features of importance to Kani Rust VerifierBugs or features of importance to Kani Rust VerifierRust APIIssues pertaining to the CBCM Rust APIIssues pertaining to the CBCM Rust APIawsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC usersnew feature
Type
Projects
Status
No status