Skip to content

Add missing analysis options in verification call in C++/Rust API #7662

Open
@NlightNFotis

Description

@NlightNFotis

Description

Add missing analysis options in C++/Rust API:

  • bounds-check
  • pointer-check
  • div-by-zero-check
  • float-overflow-check
  • nan-check
  • undefined-shift-check
  • unwinding-assertions
  • object-bits
  • unwind
  • slice-formula

The end result should allow an API interaction that has an end outcome similar to the following cbmc binary invocation:

cbmc --bounds-check --pointer-check --div-by-zero-check --float-overflow-check --nan-check --undefined-shift-check --unwinding-assertions --object-bits 16 --unwind 5 --slice-formula b_harness.out --json-ui

Context

[This is to track items outlined in #7042 that are missing to make the C++ and Rust API more useful]

Metadata

Metadata

Assignees

No one assigned

    Labels

    KaniBugs or features of importance to Kani Rust VerifierRust APIIssues pertaining to the CBCM Rust API

    Type

    No type

    Projects

    Status

    No status

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions