diffblue/cbmc issues and pull requests

#8684 - goto-harness: use __CPROVER_(de)?allocate, not malloc/free

Pull Request - State: closed - Opened by tautschnig 15 days ago - 1 comment

#8683 - Improving compilation instructions in COMPILING.md on mac

Issue - State: open - Opened by HuStmpHrrr 15 days ago

#8681 - goto-harness results in `no body for function 'free'`

Issue - State: closed - Opened by archigup 16 days ago - 2 comments
Labels: pending merge

#8669 - Stop using GNU parallel on windows-2022 runner

Pull Request - State: open - Opened by tautschnig about 1 month ago - 1 comment

#8668 - Fix support for `with_exprt` with more than 3 operands

Pull Request - State: open - Opened by tautschnig about 1 month ago - 2 comments
Labels: bugfix, soundness

#8667 - Release CBMC 6.7.0

Pull Request - State: closed - Opened by tautschnig about 1 month ago - 1 comment

#8666 - Remove deprecated make_with_expr

Pull Request - State: closed - Opened by tautschnig about 1 month ago - 1 comment
Labels: cleanup

#8665 - Remove deprecated is_null_pointer

Pull Request - State: closed - Opened by tautschnig about 1 month ago - 1 comment
Labels: cleanup

#8664 - Move is_{true,false,zero,one} from `exprt` to `constant_exprt`

Pull Request - State: open - Opened by tautschnig about 1 month ago - 5 comments
Labels: blocker

#8663 - [Question] C++ standard library and language version support

Issue - State: open - Opened by bob-boberman about 1 month ago - 2 comments

#8662 - [Question] Using incremental SAT solving

Issue - State: closed - Opened by mroximut about 1 month ago - 2 comments

#8661 - Fix loop assign clause for Kani

Pull Request - State: closed - Opened by thanhnguyen-aws about 1 month ago - 1 comment

#8660 - CI: use Visual Studio 2025 runners instead of 2019

Pull Request - State: closed - Opened by tautschnig about 1 month ago - 3 comments

#8659 - goto-analyzer: support typecasts as left-hand sides

Pull Request - State: closed - Opened by tautschnig about 1 month ago - 1 comment

#8658 - Avoid need for preprocessor calls with -m64

Pull Request - State: closed - Opened by tautschnig about 1 month ago - 1 comment

#8657 - fixup! fix exprt::opX accesses in linker_script_merge

Pull Request - State: closed - Opened by tautschnig about 1 month ago - 1 comment

#8656 - CBMC gives spurious warning for unwind bound > 1

Issue - State: open - Opened by Costandre97 about 1 month ago - 1 comment
Labels: bug

#8655 - Change the "no assigns..." and "no decreases..." warnings to higher verbosity

Pull Request - State: closed - Opened by rod-chapman about 2 months ago - 2 comments
Labels: aws, Code Contracts

#8654 - Can the "no decreases clause" and "no assigns clause" warnings be at a higher verbosity?

Issue - State: closed - Opened by rod-chapman about 2 months ago
Labels: aws, Code Contracts, trivial

#8653 - Value set: remove array-of-array special case

Pull Request - State: open - Opened by tautschnig about 2 months ago - 1 comment

#8652 - [Question] Problems verifying simple linear search using contracts

Issue - State: closed - Opened by Gaareth about 2 months ago - 2 comments

#8651 - Flow-insensitive value set: don't create index expressions over non-array objects

Pull Request - State: open - Opened by tautschnig about 2 months ago - 1 comment
Labels: bugfix

#8650 - `run(..., std::ostream &, ...)` with pipe

Pull Request - State: closed - Opened by kroening about 2 months ago - 1 comment

#8649 - Fix statement-expression expansion for Kani-provided quantifiers

Pull Request - State: closed - Opened by tautschnig about 2 months ago - 4 comments
Labels: bugfix, Kani

#8648 - Use `std::size_t`

Pull Request - State: closed - Opened by kroening about 2 months ago - 1 comment
Labels: cleanup

#8647 - Value set: lift offset from numeric constants to expressions

Pull Request - State: closed - Opened by tautschnig 2 months ago - 2 comments

#8646 - Make goto_symext::language_mode protected

Pull Request - State: open - Opened by tautschnig 2 months ago - 1 comment
Labels: dependent - do not merge

#8645 - Move unwindset.{h,cpp} to goto-programs

Pull Request - State: closed - Opened by tautschnig 2 months ago - 1 comment

#8644 - goto-checker no longer depends on cbmc

Pull Request - State: closed - Opened by tautschnig 2 months ago - 1 comment

#8643 - unwindsett: goto_model is only needed for options processing

Pull Request - State: open - Opened by tautschnig 2 months ago - 1 comment
Labels: blocker

#8642 - Introduce value-set supported simplifier for goto-symex

Pull Request - State: closed - Opened by tautschnig 2 months ago - 1 comment

#8641 - fix shell quoting

Pull Request - State: closed - Opened by kroening 2 months ago - 1 comment
Labels: bugfix

#8640 - [Question] Can goto-cc be used with an ESP-IDF project easily

Issue - State: open - Opened by jdbaptista 2 months ago

#8639 - goto-instrument -dfcc spurious "no body" warnings

Issue - State: open - Opened by rod-chapman 3 months ago
Labels: aws, Code Contracts

#8638 - goto-instrument -dfcc spurious warnings

Issue - State: open - Opened by rod-chapman 3 months ago
Labels: aws

#8637 - Printing SMT file with Z3 backend crashes CBMC

Issue - State: open - Opened by rod-chapman 3 months ago - 4 comments
Labels: bug, Solvers, aws

#8636 - DRAFT: Control Flow Retrace feature

Pull Request - State: open - Opened by lks9 3 months ago - 2 comments

#8635 - [Question] Mismatch Between pthread_create Declarations Causes Type Error

Issue - State: open - Opened by bob-boberman 3 months ago - 4 comments
Labels: Concurrency

#8634 - Divide by +INFINITY raises NaN failure with --nan-check even when numerator is a finite number

Issue - State: open - Opened by sree314 3 months ago

#8633 - __CPROVER_assume behaviour different --float-overflow-check in CBMC 5.48 and CBMC 6.4

Issue - State: open - Opened by sree314 3 months ago - 4 comments
Labels: bug, Symbolic Execution

#8632 - Release CBMC 6.6.0

Pull Request - State: closed - Opened by tautschnig 3 months ago - 1 comment

#8631 - Use GitHub mirror to download GNU parallel

Pull Request - State: closed - Opened by tautschnig 3 months ago - 1 comment

#8630 - JBMC and verification of URL encoding

Issue - State: open - Opened by Etienne13 3 months ago - 2 comments

#8629 - prophecy_r_or_w_ok_exprt lowering: adjust for dynamic/static objects

Pull Request - State: closed - Opened by tautschnig 3 months ago - 6 comments

#8628 - DFCC instrumentation: skip unused functions

Pull Request - State: closed - Opened by tautschnig 3 months ago - 1 comment

#8627 - Simplify multiple-of-element size access to arrays

Pull Request - State: closed - Opened by tautschnig 4 months ago - 4 comments

#8626 - ansi-c: remove duplicate `loc()` invocations from scanner

Pull Request - State: closed - Opened by kroening 4 months ago - 1 comment
Labels: C++ Front End, C Front End, cleanup

#8625 - ansi-c: more use of `conditional_keyword`

Pull Request - State: closed - Opened by kroening 4 months ago - 1 comment
Labels: C++ Front End, C Front End, cleanup

#8624 - Visual Studio recognises `__nullptr` in C++ mode

Pull Request - State: closed - Opened by kroening 4 months ago - 1 comment
Labels: C++ Front End, bugfix

#8623 - C23 keywords

Pull Request - State: closed - Opened by kroening 4 months ago - 7 comments
Labels: enhancement, C Front End

#8622 - ansi-c: add `""` around C++ keywords

Pull Request - State: closed - Opened by kroening 4 months ago - 1 comment
Labels: C++ Front End, C Front End, cleanup

#8621 - ansi-c: introduce `conditional_keyword(c, t)`

Pull Request - State: closed - Opened by kroening 4 months ago - 1 comment
Labels: C++ Front End, C Front End, cleanup

#8620 - C17 and C23 support

Pull Request - State: closed - Opened by kroening 4 months ago - 1 comment
Labels: enhancement, C Front End

#8619 - Refine-arithmetic supports simplifier

Pull Request - State: closed - Opened by peterschrammel 4 months ago - 1 comment

#8618 - Replace conditions in quantified statement expressions

Pull Request - State: closed - Opened by qinheping 4 months ago - 1 comment

#8617 - Huge SMT file and slow proof for simple array function

Issue - State: closed - Opened by rod-chapman 4 months ago - 45 comments
Labels: pending merge, blocker, aws, aws-high, Code Contracts

#8616 - Fix quantifiers with nested statement-expressions

Pull Request - State: closed - Opened by qinheping 4 months ago - 1 comment

#8615 - CBMC getting stuck when post-processing functions with memmove and non-deterministic sizes

Issue - State: open - Opened by AmPaschal 4 months ago

#8614 - Soundness with __CPROVER_r_ok

Issue - State: closed - Opened by lks9 4 months ago - 4 comments

#8613 - CI: Remove use of Ubuntu 20.04

Pull Request - State: closed - Opened by tautschnig 4 months ago - 3 comments

#8612 - Dump-C appears incompatible with --dfcc

Issue - State: open - Opened by tautschnig 4 months ago - 1 comment

#8611 - Use same CMake minimum version in DownloadProject configuration

Pull Request - State: closed - Opened by tautschnig 4 months ago - 4 comments

#8610 - Buggy handling of assignments involving pointer dereference

Issue - State: open - Opened by nianzelee 4 months ago - 5 comments
Labels: bug

#8609 - Fix display of code changes in clang-format CI action

Pull Request - State: closed - Opened by tautschnig 4 months ago - 1 comment

#8608 - Simplify quantified expressions over constants

Pull Request - State: closed - Opened by tautschnig 4 months ago - 5 comments

#8607 - Release CBMC 6.5.0

Pull Request - State: closed - Opened by tautschnig 5 months ago - 1 comment

#8606 - [Question] Running CBMC on a C file with dynamic linking and/or shared libraries

Issue - State: open - Opened by a-shokri 5 months ago - 1 comment
Labels: question

#8605 - Handle quantifiers with statement expressions

Pull Request - State: closed - Opened by qinheping 5 months ago - 6 comments

#8604 - [Question] Syntax Error with `__CPROVER_loop_invariant` in CBMC 6.4.1 Docker

Issue - State: open - Opened by zhoulaifu 5 months ago - 4 comments

#8603 - CONTRACTS: is_fresh now tracks separation at the byte level instead of whole objects

Pull Request - State: closed - Opened by remi-delmas-3000 5 months ago - 6 comments

#8602 - CBMC May Struggle with `sscanf` and `strcmp` Handling in Symbolic Execution?

Issue - State: open - Opened by zhoulaifu 5 months ago - 8 comments

#8601 - [QUESTION] How to log all SAT literals

Issue - State: open - Opened by cvick32 5 months ago

#8600 - Performance Cliff and Excessive Memory Usage at --unwind 6

Issue - State: open - Opened by zhoulaifu 5 months ago - 8 comments

#8599 - __CPROVER_is_cstring() Ignored in CBMC Verification

Issue - State: open - Opened by zhoulaifu 5 months ago

#8598 - Extracting Concrete Input Strings from CBMC Counterexamples

Issue - State: open - Opened by zhoulaifu 5 months ago - 2 comments

#8597 - fixup #8538 -- correct rounding modes for `floor`, `trunc`

Pull Request - State: closed - Opened by kroening 5 months ago - 4 comments
Labels: bugfix

#8596 - Regression in floating-point floor

Issue - State: closed - Opened by zhassan-aws 5 months ago
Labels: Kani

#8595 - Remove set but not used variables

Pull Request - State: closed - Opened by mgudemann 5 months ago - 2 comments

#8594 - simplify: rewrite `bitxnor` on booleans to equal

Pull Request - State: closed - Opened by kroening 5 months ago - 1 comment

#8593 - CBMC does not recognize pointer initializations outside functions

Issue - State: open - Opened by AmPaschal 5 months ago - 1 comment

#8592 - CBMC misbehaves in functions with pointer arithmetic computation

Issue - State: open - Opened by AmPaschal 5 months ago - 4 comments

#8591 - Pointer subtraction underflows and leads to faulty verification result

Issue - State: open - Opened by AmPaschal 5 months ago - 5 comments

#8590 - Remove `namespace_baset::follow(typet)`

Pull Request - State: closed - Opened by kroening 6 months ago - 1 comment
Labels: cleanup

#8589 - implement boolbvt::get for enumeration types

Pull Request - State: closed - Opened by kroening 6 months ago - 1 comment
Labels: Solvers

#8588 - No pointer check or bounds check failure and incorrect program equation for access of array in struct with negative index

Issue - State: open - Opened by andreast271 6 months ago

GitHub / diffblue/cbmc issues and pull requests