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