Search results

Performance of framing

awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users

Status: Open.

#8503 In diffblue/cbmc;

· hanno-becker opened on Nov 11, 2024

CBMC wavefront does not terminate on simple decreases clause in loop

awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users

blocker

bug

Status: Open.

#8301 In diffblue/cbmc;

· rod-chapman opened on May 21, 2024

Move __CPROVER_uninterpreted_* conversion to C type checker

Status: Open (in progress).

diffblue/cbmcnumber 8280

#8280 In diffblue/cbmc;

· tautschnig opened on May 9, 2024

Undetected pointer representation overflows

awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users

aws-high

soundnessSoundness bug? Review and add "aws" if it is, or remove "soundness" if it isn't.Soundness bug? Review and add "aws" if it is, or remove "soundness" if it isn't.

Version 6Pull requests and issues requiring a major version bumpPull requests and issues requiring a major version bump

Status: Open.

#7972 In diffblue/cbmc;

· remi-delmas-3000 opened on Oct 20, 2023

Issue with pointers

awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users

aws-medium

bug

Status: Open.

#7895 In diffblue/cbmc;

· remi-delmas-3000 opened on Sep 14, 2023

DFCC loop contracts crashes with VS

bug

Code ContractsFunction and loop contractsFunction and loop contracts

Status: Open.

#7807 In diffblue/cbmc;

· qinheping opened on Jul 13, 2023

loop normal form properties

awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users

feature request

Status: Open.

#7518 In diffblue/cbmc;

· remi-delmas-3000 opened on Feb 3, 2023

Add cover checks to CBMC

awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users

feature request

KaniBugs or features of importance to Kani Rust VerifierBugs or features of importance to Kani Rust Verifier

Status: Open.

#7293 In diffblue/cbmc;

· feliperodri opened on Nov 2, 2022

Incorrect encoding of function pointer operations in CBMC

awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users

bug

Code ContractsFunction and loop contractsFunction and loop contracts

Status: Open.

#7213 In diffblue/cbmc;

· feliperodri opened on Oct 5, 2022

New CBMC syntax needed for assigns clause with quantifiers

awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users

Code ContractsFunction and loop contractsFunction and loop contracts

feature request

Status: Open.

#7212 In diffblue/cbmc;

· feliperodri opened on Oct 5, 2022

goto-instrument internal error with function pointers

awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users

bug

Code ContractsFunction and loop contractsFunction and loop contracts

Status: Open.

#7205 In diffblue/cbmc;

· feliperodri opened on Oct 5, 2022

Implement a vacuity check for function contracts

awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC users

Code ContractsFunction and loop contractsFunction and loop contracts

research idea

Status: Open.

#7204 In diffblue/cbmc;

· feliperodri opened on Oct 5, 2022