7 Pull requests merged by 1 person

• C front-end: tolerate type differences with asm renaming

  #7584 merged Jul 30, 2025

• Extend cbmc-incr-oneloop timeout with CMake

  #8701 merged Jul 29, 2025

• Contracts instrumentation: cleanup unnecessary includes

  #8696 merged Jul 28, 2025

• C library: remove explicit zero initialisers

  #8698 merged Jul 26, 2025

• Simplifier: do not create extractbits with pointer type

  #8678 merged Jul 24, 2025

• SMT2 back-end: flatten with_exprt operands

  #8670 merged Jul 23, 2025

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

  #8684 merged Jul 16, 2025

5 Pull requests opened by 1 person

• DFCC: do not surface confusing warning

  #8694 opened Jul 25, 2025

• Contracts instrumentation: hide unhelpful "no body" warnings

  #8697 opened Jul 25, 2025

• Work around Z3 not producing models for some quantified expressions

  #8703 opened Jul 31, 2025

• Value-set supported simplifier: add object_size, is_invalid_pointer

  #8704 opened Aug 6, 2025

• Rewrite byte_extract from multi-dimensional array

  #8705 opened Aug 6, 2025

3 Issues closed by 2 people

• Wrong result using __va_list_tag_type with multiple arguments

  #7706 closed Jul 29, 2025

• CBMC proof complexity/time in mldsa-native top-level signature generation

  #8680 closed Jul 19, 2025

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

  #8681 closed Jul 16, 2025

14 Issues opened by 5 people

• `goto-instrument --enforce-contract-rec` does nothing

  #8702 opened Jul 30, 2025

• Invariant violation in pointer validity check

  #8700 opened Jul 28, 2025

• `goto-instrument` invariant violation with generated harness with fn pointer when contract with same signature exists

  #8699 opened Jul 25, 2025

• `--enum-range-check` has false positives after harness or dfcc instrumentation

  #8693 opened Jul 22, 2025

• Custom memory predicates don't work for non-pointer args

  #8692 opened Jul 22, 2025

• Feature request: goto-instrument flag for listing functions in goto in machine readable format

  #8691 opened Jul 22, 2025

• CBMC fails to match _Generic arms for pointers to arrays

  #8690 opened Jul 22, 2025

• Question: How to specify errno in a function contract's write set

  #8689 opened Jul 22, 2025

• CBMC fails to parse constructor attribute with argument

  #8688 opened Jul 21, 2025

• No body for 'free' during inlining when using `goto-instrument` with dfcc

  #8687 opened Jul 21, 2025

• SMT generated for Bitwuzla is mal-formed and rejected

  #8686 opened Jul 20, 2025

• goto-cc fails to parse declaration with attributes before contract clauses

  #8685 opened Jul 17, 2025

• Improving compilation instructions in COMPILING.md on mac

  #8683 opened Jul 15, 2025

• feature request: Support getting compile flags from compile_commands.json

  #8682 opened Jul 15, 2025

35 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

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

  #8640 commented on Jul 15, 2025 • 0 new comments

• goto-instrument -dfcc spurious "no body" warnings

  #8639 commented on Jul 25, 2025 • 0 new comments

• goto-instrument -dfcc spurious warnings

  #8638 commented on Jul 26, 2025 • 0 new comments

• CBMC cannot understand Z3 generating a quantified expression in a counter-example

  #8679 commented on Jul 30, 2025 • 0 new comments

• Consistently use unsigned/size_t in big-int [blocks: #2310]

  #2452 commented on Jul 28, 2025 • 0 new comments

• Message handler: add quote_begin, quote_end commands

  #5696 commented on Jul 28, 2025 • 0 new comments

• Value set dereferencing: do not treat struct prefixes as equal

  #5876 commented on Jul 29, 2025 • 0 new comments

• Add support for MergeSat

  #6439 commented on Jul 29, 2025 • 0 new comments

• Move rounding_mode_identifier() to configt

  #6555 commented on Jul 29, 2025 • 0 new comments

• goto-symex: apply_condition should not change L2 index

  #6993 commented on Jul 29, 2025 • 0 new comments

• Fix goto-symex' auto-objects feature

  #7177 commented on Jul 28, 2025 • 0 new comments

• Introduce bitst and bytest to avoid bit/byte mix-up

  #7413 commented on Jul 29, 2025 • 0 new comments

• Linking: fix up all types before handling functions or objects

  #7579 commented on Jul 29, 2025 • 0 new comments

• C front-end: ensure array type updates are consistent

  #7610 commented on Jul 28, 2025 • 0 new comments

• Reading/writing goto binaries: consistently use return values

  #7643 commented on Jul 28, 2025 • 0 new comments

• Mimic GCC/Clang simplification behaviour when type checking ?:

  #7959 commented on Jul 29, 2025 • 0 new comments

• Perform simplification of not_exprt as preorder step

  #7996 commented on Jul 28, 2025 • 0 new comments

• Symex guards: avoid unnecessary duplicate negation

  #8041 commented on Jul 29, 2025 • 0 new comments

• Conditionally simplify use of if-then-else conditions

  #8042 commented on Jul 28, 2025 • 0 new comments

• C library: Refine and improve stdio models

  #8043 commented on Jul 28, 2025 • 0 new comments

• Move __CPROVER_uninterpreted_* conversion to C type checker

  #8280 commented on Jul 28, 2025 • 0 new comments

• C++ front-end: support explicit type conversion with braced-init-list

  #8385 commented on Jul 28, 2025 • 0 new comments

• C++ front-end: support constexpr

  #8386 commented on Jul 28, 2025 • 0 new comments

• Promote set_all_frozen to decision_proceduret to remove a dynamic_cast

  #8404 commented on Jul 28, 2025 • 0 new comments

• Remove dynamic_cast from hardness collection code paths

  #8423 commented on Jul 28, 2025 • 0 new comments

• Automatically create release tags via GitHub actions

  #8424 commented on Jul 28, 2025 • 0 new comments

• Automatically produce a CBMC release twice per month

  #8425 commented on Jul 28, 2025 • 0 new comments

• Remove renamedt from symex_targett interface

  #8447 commented on Jul 28, 2025 • 0 new comments

• Cleanup exprt and expr_util [depends-on: 8675, 8455]

  #8451 commented on Jul 28, 2025 • 0 new comments

• Mark constant_exprt::value_is_zero_string protected [depends-on: 8675]

  #8455 commented on Jul 28, 2025 • 0 new comments

• Clarify usage of history variables in error messages

  #8456 commented on Aug 6, 2025 • 0 new comments

• goto-symex: assumed pointer equalities must update value set

  #8494 commented on Jul 28, 2025 • 0 new comments

• Make goto_symext::language_mode protected [depends-on: 8643]

  #8646 commented on Jul 28, 2025 • 0 new comments

• Value set: remove array-of-array special case

  #8653 commented on Jul 28, 2025 • 0 new comments

• operator== for exprt and bool, int, nullptr_t

  #8675 commented on Jul 28, 2025 • 0 new comments