Search results

Invariant violation with bitwuzla backend due to ID_infinity

Status: Open.

#8571 In diffblue/cbmc;

· remi-delmas-3000 opened on Jan 17, 2025

__CPROVER_forall fails when dealing with flattening of nested structure

Status: Open.

#8570 In diffblue/cbmc;

· hanno-becker opened on Jan 16, 2025

Program instrumentation options not working

Status: Open.

#8569 In diffblue/cbmc;

· junchun opened on Jan 15, 2025

Question: CBMC loop unwinding behaviours--programs fully unwound with just --unwind 2 takes forever if no parameter given

Status: Open.

#8568 In diffblue/cbmc;

· hellotommmy opened on Jan 15, 2025

[question] is a list of C11 UB up to date?

Status: Open.

#8567 In diffblue/cbmc;

· ligurio opened on Jan 15, 2025

Race check in CBMC

Status: Open.

#8566 In diffblue/cbmc;

· Misasasa opened on Jan 14, 2025

Using __CPROVER_is_fresh in disjunctions

Code ContractsFunction and loop contractsFunction and loop contracts

aws-high

bug

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.

Status: Open.

#8560 In diffblue/cbmc;

· hanno-becker opened on Jan 10, 2025

--no-standard-checks is included in goto-instrument help, but can only be parsed by cbmc and goto-analyzer

Status: Open.

#8557 In diffblue/cbmc;

· polgreen opened on Jan 5, 2025

Compiling code generated by dump-c (removing cprover_TYPE, etc)

Status: Open.

#8535 In diffblue/cbmc;

· metamaterialsuit opened on Dec 19, 2024

How to debug dump-c invariant violation?

Status: Open.

#8534 In diffblue/cbmc;

· metamaterialsuit opened on Dec 18, 2024

invariant violation report using loop contracts

Status: Open.

#8528 In diffblue/cbmc;

· polgreen opened on Dec 15, 2024

Adding CPROVER_assigns statement changes result

Status: Open.

#8527 In diffblue/cbmc;

· polgreen opened on Dec 15, 2024