Skip to content

Expose all of the CBMC flags that Kani is using to the C++/Rust API #7500

Open
@NlightNFotis

Description

@NlightNFotis

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 VerifierRust APIIssues pertaining to the CBCM Rust APIawsBugs or features of importance to AWS CBMC usersnew feature

Type

No type

Projects

Status

No status

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions