All pull requests

Pull requests

• DFCC: Add opt-in to force call by contract

  #9465·hanno-becker opened Nov 13, 2026·

  ·

• SMT2: declare datatypes of pointed-to structs after the pointing struct

  #9464·tautschnig opened Nov 12, 2026Collaborator·3 tasks done·

  ·
  2

• Library linking: a callee only a model declares is in the goto program

  #9463·tautschnig opened Nov 12, 2026Collaborator·3 tasks done·

  ·
  2

• Goto conversion: the floating-point comparison macros are relations

  #9462·tautschnig opened Nov 12, 2026Collaborator·3 tasks done·

  ·
  3

• va_start: the variadic arguments follow the last named parameter

  #9460·tautschnig opened Nov 12, 2026Collaborator·3 tasks done·

  ·
  2

• CodeQL: build with JDK 21

  #9459·tautschnig opened Nov 12, 2026Collaborator·3 tasks done·

  ·
  2

• Slicer: ignore GOTO steps over sliced assignments

  #9458·albertwujj opened Nov 12, 2026·6 tasks done·

  ·

• C front-end: decreases clause types and pointer comparisons

  #9457·tautschnig opened Nov 12, 2026Collaborator·2 of 3 tasks·

  ·
  2

• generate-function-body: reuse free-suffix hints when havocking

  #9456·tautschnig opened Nov 12, 2026Collaborator·3 tasks done·

  ·
  2

• Loop contracts file: report bad clauses and loop identifiers instead of crashing

  #9455·tautschnig opened Nov 12, 2026Collaborator·3 tasks done·

  ·
  13

• Symex: warn when arrays of structs or pointers exceed the field-sensitivity limit

  #9454·tautschnig opened Nov 12, 2026Collaborator·3 of 4 tasks·

  ·
  2

• goto_inline: handle arguments of a type that differs from the parameter's

  dependent - do not merge
  #9453·tautschnig opened Nov 12, 2026Collaborator·3 tasks done·

  ·
  2

• DFCC: pass the write set where the write set parameter is

  Code Contracts
  #9452·tautschnig opened Nov 12, 2026Collaborator·4 tasks done·

  ·
  9

• DFCC: test that checks inside uncontracted loops are not all suppressed

  #9451·tautschnig opened Nov 12, 2026Collaborator·3 tasks done·

  ·
  2

• Flattening: build byte_update endianness maps once, not once per offset

  #9450·tautschnig opened Nov 12, 2026Collaborator·3 of 4 tasks·

  ·
  2

• Config: wchar_t is unsigned on Arm, except on Apple platforms

  #9449·tautschnig opened Nov 11, 2026Collaborator·3 tasks done·

  ·
  2

• Linking: keep anonymous tag types anonymous when renaming them

  #9448·tautschnig opened Nov 11, 2026Collaborator·3 tasks done·

  ·
  2

• Field sensitivity: keep typecasts outside the SSA expression of a union read

  #9447·tautschnig opened Nov 11, 2026Collaborator·3 tasks done·

  ·
  2

• C front-end: keep side effects of integer zeros converted to pointers

  #9446·tautschnig opened Nov 11, 2026Collaborator·3 tasks done·

  ·
  2

• C library: models of strtol_l, strtoul_l, strtoll_l and strtoull_l

  #9444·tautschnig opened Nov 10, 2026Collaborator·4 tasks done·

  ·
  2

• library_check: exclude tests.log from regression/cbmc-library scan

  #9443·tautschnig opened Nov 10, 2026Collaborator·2 of 3 tasks·

  ·
  2

• C library: link the model of _InterlockedIncrement

  #9442·tautschnig opened Nov 10, 2026Collaborator·4 tasks done·

  ·
  2

• C library: model of uselocale

  #9441·tautschnig opened Nov 10, 2026Collaborator·3 tasks done·

  ·
  2

• C library: localeconv returns the "C" locale's values

  #9440·tautschnig opened Nov 10, 2026Collaborator·3 tasks done·

  ·
  2

• ansi-c library: model strtoll, strtoul and strtoull

  #9439·tautschnig opened Nov 10, 2026Collaborator·4 tasks done·

  ·
  2