Repository navigation

test/cbmc: expand CBMC coverage (RFC 0025) - #263

Draft

gburd wants to merge 15 commits into

test/cbmc-expand

Draft

test/cbmc: expand CBMC coverage (RFC 0025)#263
gburd wants to merge 15 commits into
masterfrom
test/cbmc-expand

Commits on Nov 4, 2026
- rfc: 0025 expand CBMC coverage
  gburd
  committed
  61b4f95
- test/cbmc: enable the CBMC workflow, check copies against src/ (RFC 0025 C0)
  gburd
  committed
  f03dc3f
- test/cbmc: H1 __rep_cmp_vote election-winner comparator (RFC 0025 C1)
  libdb agent
  committed
  220d36d
- test/cbmc: H2 __rep_tally vote-tally array (RFC 0025 C1)
  libdb agent
  committed
  23a0321
- test/cbmc: H3 election-quorum arithmetic (RFC 0025 C1)
  libdb agent
  committed
  76823bf
- test/cbmc: H4 repmgr ack-policy durability decision (RFC 0025 C1)
  libdb agent
  committed
  5f95aab
- test/cbmc: B1 __bam_defdecompress bounds -- finds a real over-read (RFC 0025 C2)
  gburd
  committed
  64d8257
- test/cbmc: align B1_FIXED non-dup path with the engine fix (RFC 0025 C2)
  gburd
  committed
  010b177
- test/cbmc: Q1 queue record arithmetic (RFC 0025 C2)
  gburd
  committed
  20327b5
- test/cbmc: L1 log header check + E1 region size classes (RFC 0025 C3)
  gburd
  committed
  b824344
- test/cbmc: B2 compress/decompress round trip (RFC 0025 C2)
  gburd
  committed
  bd95750
- test/cbmc: refresh the workflow runtime note (RFC 0025 C2/C3)
  gburd
  committed
  391d1a2
- test/cbmc: B1 models the decoded varint value as any u32, add the wrap arm
  gburd
  committed
  a431dc7
- test/cbmc: Q1 and E1 bounds widened to the real input range
  gburd
  committed
  7345eb8
- test/cbmc: preprocessor lines at column 0 in harness_bt_decompress.c (s_chk_defines)
  gburd
  committed
  0e20b93