2025-05-05

ci: Fix docker release workflow (#203)

* ci: Fix `freebsd` image version on cirrus

* ci: Pin Ubuntu version to set Z3 as a default solver for macOS

* chore: Update gtest version

* ci: Update llvm version in Dockerfile

* fix(scripts): Fix ShellCheck warning

* feat(build): Add `ENABLE_FP_RUNTIME` option

* style: Use a vector instead of an array as a variable-length container

* chore(docker): Update Dockerfile

* test: Require `not-ubsan` for a couple of tests with 32-bit binaries

KLEEF Test-Comp 2025

What's Changed

• Enable differential shellcheck by @misonijnik in #160
• [feat] KValue base class by @S1eGa in #161
• Move the dependencies from the submodules to build.sh by @misonijnik in #163
• Entry point multiplex, no nonstd::optional, no interactive mode by @ocelaiwo in #164
• Fix cirrus-ci by @misonijnik in #165
• Fix concretized DSU by @misonijnik in #166
• Remove unnecessary field from the ImmutableList by @ladisgin in #168
• [fix] fix bitwuzla build version fix by @ocelaiwo in #169
• Annotations by @ladisgin in #109
• SARIF reports by @S1eGa in #167
• Pre-commit clang-format hook by @S1eGa in #171
• Clang-format hook: removed auto-fixing of PRs. by @S1eGa in #174
• Rework TargetManager by @misonijnik in #172
• [feat] ObjectManager by @ocelaiwo in #173
• Hotfix msan by @misonijnik in #177
• Fully symbolic memory, multiplex entry points, fair searcher by @misonijnik in #176
• Migrate to our ghcr.io repository by @misonijnik in #180
• fix: Fix macOS CI failures by @misonijnik in #185
• fix: Fix naming for coverage related files by @misonijnik in #186
• fix: Get rid of the testcases spamming mode by @misonijnik in #187
• Pointers fixes by @S1eGa in #188
• Compile warnings fixes by @S1eGa in #178
• feat: Take commits from KLEE 3.1 by @misonijnik in #196
• Fix stp build by @ocelaiwo in #200
• Fix macos ci by @misonijnik in #201
• feat: Reintroduce concrete store by @ocelaiwo in #197

Full Changelog: testcomp24...testcomp25

KLEEF Test-Comp 2024

Please find an exact binary participated in the competition here.

What's Changed

• clang-format CI check by @S1eGa in #60
• Fix unsat core tracking for duplicating constrains. by @S1eGa in #76
• Rework CexCacheSolver and add validity core cache by @dim8art in #58
• Don't fail klee on alias with uclibc by @ladisgin in #74
• Fixes for arm arch by @ladisgin in #70
• Print LL only if needed and generate it once by @ladisgin in #79
• Fix linking by @ladisgin in #77
• Fix createLibcWrapper by @Lana243 in #82
• Add error-guided search by @misonijnik in #83
• Filter cases when the pointer base is not resolved to the beginning of the object by @misonijnik in #86
• Improve stability of confidence rate by @Columpio in #87
• Update SarifReport by @misonijnik in #88
• Change to more suitable line calculations by @ladisgin in #90
• Stabilize engine and add some new features by @misonijnik in #91
• Add DistanceCalculator and fix performance bugs by @misonijnik in #94
• Add Cooddy report parser by @misonijnik in #93
• Target progress report by @Columpio in #95
• Reach fork optimization by @Columpio in #96
• SelectExpr simplifying and constant size lazy initialization by @misonijnik in #98
• Small fixes by @Columpio in #99
• Cherry pick KLEE 3.0 commits by @misonijnik in #100
• Add TargetManager and rework TargetedSearcher and GuidedSearcher by @misonijnik in #101
• [fix] Added difference_type for ImmutableTree::iterator by @S1eGa in #113
• [fix] Fixed building of expressions with floats by @S1eGa in #119
• Independent solver rework by @dim8art in #85
• Approximation of tree incrementality for Z3 solver by @Columpio in #104
• Consider function coverage for blocks with calls by @misonijnik in #121
• Make isReachedTarget consistent with reportTruePositive by @misonijnik in #122
• uClibc 32bit by @S1eGa in #115
• tc by @Columpio in #123
• Fixed take from incremental vector with no frames by @Columpio in #125
• Improve IndependentConstraintSetUnion by @misonijnik in #124
• Small fixes by @Columpio in #127
• Mem optimize by @ladisgin in #118
• Small fixes by @Columpio in #128
• Small fixes by @Columpio in #129
• Fix a few bugs by @misonijnik in #130
• Small fix by @misonijnik in #132
• Improved Iterative Deepening Searcher by @Columpio in #133
• [fix] Fixed inner types for unnamed structs. by @S1eGa in #134
• Separate branch and block coverage by @misonijnik in #136
• Optimizations by @Columpio in #137
• Compare expressions by height in simplifier by @ocelaiwo in #138
• Sizeless ObjectState + uninitialized memory support by @ocelaiwo in #131
• Create alpha-equvalency format solver by @dim8art in #135
• Small fixes by @Columpio in #139
• Fix test generation by @misonijnik in #142
• Small fixes by @Columpio in #141
• Fix AlphaEquivalenceSolver by @misonijnik in #143
• Fix several bugs by @misonijnik in #144
• Halt when LLVM passes already proved unreachability by @Columpio in #145
• Set new version by @misonijnik in #147
• Small improvement of call remover by @Columpio in #148
• Fixes pack by @misonijnik in #149
• Enable coverOnTheFly after approaching memory cup by @misonijnik in #150
• Fix several bugs by @misonijnik in #151
• Chore fixes and convenient run script by @Columpio in #152
• Improve coverage branches tests by @misonijnik in #153
• Small fix by @misonijnik in #154
• Several fixes by @misonijnik in #155
• [feat] Added Bitwuzla solver in list of available solvers. by @S1eGa in #158
• Add lazy calculation of constraint dsu by @dim8art in #156
• Several fixes by @misonijnik in #157

New Contributors

• @Columpio made their first contribution in #87
• @ocelaiwo made their first contribution in #138

Full Changelog: https://github.com/UnitTestBot/klee/commits/testcomp24

KLEE before massive reengineering

v2.3-utbot

Fix stdin-read variable

KLEE before rebase to 2.3

Add support stdin/stdout with interactive mode

Implement getc, fgetc, fread, fgets, getchar, gets, putc, fputc, fwrite, fputs, putchar, puts