This is an automated nightly release of ESBMC.

This is the ESBMC version used at the FSE'25 submission

What's Changed

• Feature/build mac by @sshivaji in #2219
• GCSE now only caches overflow inner operands by @rafaelsamenezes in #2221
• Only replace inner expressions for overflow in GCSE by @rafaelsamenezes in #2227
• [python-frontend] Handling chained comparisons by @brcfarias in #2228
• GCSE now resets index2t by @rafaelsamenezes in #2230
• Force update of tags in benchexec action by @rafaelsamenezes in #2234
• Added new catch exception for GCSE by @rafaelsamenezes in #2233
• [C++ verification] Improve the adjustment of capture variables by @XLiZHI in #2222

Full Changelog: v7.8...nightly-0f9f34afdc1ef89589437e04f88ffc04437358eb

This is an automated nightly release of ESBMC.

This is an automated nightly release of ESBMC.

This is the first version of ESBMC with transcoder patches

Version 7.8

This release introduces several significant improvements, feature enhancements, bug fixes, and updates to improve the functionality and usability of ESBMC. Below is a detailed breakdown of the changes:

New Features

Build Support for macOS:

• Added build instructions for macOS M1 and Intel architectures (#2217, #2216, #2213).
• Updated README files to reflect new macOS build compatibility (#2213, #2089).

SMT Solver Enhancements:

• Support for extracting arrays from tuples in SMT (#2215).
• Updated Bitwuzla SMT solver from v0.6.1 to v0.7.0 for improved performance (#2199).
• Fixed pointer typecast issues in SMT backends for byte updates (#2197).

Concurrency Improvements:

• Adjusted concurrency flags for memory leak and overflow checks (#2206).
• Read global variables directly from function calls in concurrency checks (#2192).
• Fixed interleavings and guards for better thread scheduling (#2185).
• Introduced a new thread scheduling policy (#2178).

C and C++ Verification Enhancements:

• Added support for clang built-in float16 types (#2214).
• Support for clang::_builtin_va* operations in C verification (#2207).
• Fixed allocation size calculations in C++ new operations (#2187).
• Enhanced lambda captures for C++14 (#2170).
• Supported std::make_tuple, std::forward, and other C++ standard functions (#2051, #2118).

Python Frontend Updates:

• Improved handling of module aliases during verification (#2196).
• Enhanced error messages and documentation for Python (#2107, #2086).

Fixes and Improvements

Verification Process:

• Improved constant propagation handling (#2128).
• Addressed robustness issues in alloca handling during symbolic execution (#2095).
• Enhanced handling of array initialization loops in C++ verification (#2101).

Build and Compilation:

• Fixed compatibility with newer Clang versions (Clang 18 and Clang 19) (#2189, #2099).
• Updated CI to include static builds with LLVM 16 as the default (#2062).

Coverage and Benchmarks:

• Enabled assertion coverage in function mode (#2106).
• Added benchmarks for SV-COMP 2025 (#2158).
• Improved branch coverage support (#2056).

Miscellaneous:

• Hardened utility functions like binary2integer for reliability (#2132).
• Added JSON generation for test reports and refined HTML reports (#2127).
• Updated concurrency benchmark inclusion in BenchExec runs (#2201).

Acknowledgments

This release would not have been possible without the contributions from the community and team members, including but not limited to @ssshivaji, @intrigus-lgtm, @XLiZHI, @ChenfengWei0, @Anthonysdu, @mikhailramalho, and @brcfarias. Thank you for your continued support and efforts to enhance ESBMC.

Full Changelog: v7.7...v7.8

• Clang C/C++ Frontend
  • Interpret option -Wc,OPT1,OPT2,... as passing OPT1 OPT2 ... to the clang frontend directly (#1840)
  • Fix additional C++ APIs: [sf]stream, valarray, locale C++ OM (#1834)
  • Fix some more C++ APIs: bitset, csignal and string_view C++ OM (#1832)
  • fixed std::move functions call (#1827)
• Solidity Frontend
  • Bug fixing and code refactoring (#1839)
  • Support Solidity built-in variables and functions (#1828)
• General Improvements
  • Added total VCCs column (#1841)
  • Improved build instructions about ESBMC-CHERI (#1833)

• Clang-C/C++ Frontend
  • Support "noexcept" keyword (#1819)
  • Add llvm-16 build to CI, switch from --cppstd to --std + remove default -std=c++03 (#1817)
  • Support compilation against LLVM-17 and -18 (#1816)
  • Support more type of exception var (#1815)
  • Param name in parameter packs (#1813)
  • Fix unnamed parameter (#1812)
  • Support throw decl (#1806)
  • Fix member init ref (#1802)
  • Add exception id for catch (#1799)
  • Add frontend support for some constructs used in the Linux kernel (#1798)
  • Support builtin template (#1789)
  • Fix recursive structs (#1781)
  • Fix the order of params (#1780)
  • Handle recursive conversion in base type C++ (#1777)
  • Support empty list initializer for scalars (#1775)
  • Support CXXThrowExpr node (#1768)
  • Adjust return type for ref type (#1766)
  • Fixed seg fault caused by extern (#1765)
  • fixed wrong enum type (#1759)
  • Simplify if conditions (#1756)
  • Add delegating constructors help wanted (#1754)
  • Add support for anon constructors in anon structs (#1753)
  • Support variable template specialization (#1748)
  • Add support for nullptr_t (#1745)
  • Remove <type_traits> + support C++17 variable template declarations C++ OM (#1739)
  • Avoid the temporary object (#1736)
  • Support sizeof expression (#173)
  • Fix base classes and tmp object (#1715)
  • Add new node for CXXDefaultInitExprClass (#1705)
  • Fix compilation errors for the lib (#1702)
  • Fix compilation errors for set (#1700)
  • Fix cpp if-else typecast (#1692)
  • Fix compilation errors and warning messages in the lib (#1691)
  • Fix assertion failed in string OM (#1686)
  • Fix various warning/compilation errors for and libs (#1685)
  • Enable test case for the Typeinfo lib (#1681)
  • Standardize the cpp new/delete (#1670)
  • Add memory deallocation check (#1671)
  • Add <string_view> model (#1672)
• Python Frontend
  • Support for class methods (#1808)
  • Convert "for v in range(start, end, step)" (#1804)
  • Add type annotation to methods (#1800)
  • Handle longer arithmetic expressions (#1795)
  • Variable initialization via ** operator and uint64() function #1791
  • Replace abort() with warning for undefined functions (#1763)
  • Add support for len() (#1757)
  • Support for "break" and "continue" (#1752)
  • Add support for "bytes" type and array indexing (#1744)
  • Add support for float numbers (#1734)
  • Handling imports (#1714)
• Interval Analysis
  • Optimization of Interval Analysis (#1755)
  • Widening fixes (#1738)
  • Add message for interval analysis duration (#1790)
  • Support for symbolic reconstruction of expression (#1726)
  • Fixed relation >= and > for wrapped intervals (#1712)
  • Fixes for interval bitwise arithmetic (#1711)
  • < and <= fixes for Wrapped Intervals (#1662)
• Concurrency Support
  • Make interleavings unviable after the main thread has ended (#1721)
  • Do not record __ESBMC_pthread_thread (#1733)
  • Do not record __ESBMC_rounding_mode (#1732)
• Solidity Frontend
  • Bug fixed for constructor and struct (#1788)
  • Fix the missing contract name in the symbol id (#1697)
• General Improvements
  • Restore LTL code (#1586)
  • Fix atomic_begin and atomic_end translation (#1821)
  • Fix macOS CI build (#1809)
  • Fixes for CHERI builds cheri (#1786)
  • Add incremental smt support for CVC4 (#1773)
  • Fixed seg fault in error trace (#1764)
  • Add --segfault-handler dumping a stack trace and memory map on SIGSEGV and SIGABRT (#1760)
  • Convert references more consistently C++ (#1696)
  • Fix the wrong usage of equality instead of assignment smt (#1689)
  • Extend regdb.py with categorized flags and allow querying using glob patterns (#1684)
  • Support detecting Clang resource dir for >= v16 (#1682)
  • Add tool regdb.py for regression test management (#1680)

This is an experimental pre-release based on PR #1810 to test suitability of mingw64 cross-compilation for potential future Windows releases. It is built with Clang-14-based frontends, with solvers Z3-4.13.0 and Boolector-3.2.3, and the mingw toolchain uses posix-threads.

Any feedback is welcome, preferrably in issue #1801.

• Clang-C++ Frontend
  • Improved C++ dangling pointer checking (#1648).
  • Improved C++ double delete (#1648).
  • Fixed the cpp new initialization (#1636).
  • Fixed the copy and move constructor (#1614).
  • Support rvalue references C++11 (#1595).
• Solidity Frontend
  • Support Multiple Contract Verification (#1640).
  • Bug fixes for Inheritance (#1624).
  • Scope fix (#1606).
  • Support Error Handling (#1598).
  • Supported struct data structure and fixed bugs (#1563).
  • Fixed nested loop and one-statement block (#1546).
  • Fixed Visibility (#1545).
  • Support pattern-base checking in contract mode (#1543).
  • Continue and Break Keyword Supported (#1529).
• Python Frontend
  • Inheritance and overriding (#1639).
  • Empty class instantiation and built-in functions support (#1608).
  • Support pass statement and var declarations without initialization (#1602).
  • Support for Class attributes (#1587).
  • Class definition and instantiation (#1552).
  • Support for // operator (#1522).
  • Add type inference for dynamic variables (#1515).
  • Python frontend: Add support for recursion (#1481).
  • Adjust types and re-enable tests (#1441).
  • Add support for non-determinism (#1439).
  • Optimize --function handling (#1438).
  • Add support for conditional operator and function flag (#1437).
• Jimple frontend
  • Jimple throws are now shown at --show-claims (#1632).
• Abstract Interpretation
  • Interval analysis now inverts boolean correctly (#1625).
  • VSA is now only computed with GCSE flag (#1607).
  • Instrumentation for interval loop invariants (#1603).
  • Wrapped intervals can now optimize expressions (#1566).
  • Support for context-aware intervals (#1564).
• GOTO contractors
  • Ibex fixpoint was causing crashes; fixed-point is done manually now (#1638).
  • Integers (signed and unsigned) and floats are converted from one to another correctly now (#1638).
• Concurrency
  • Fixed monolithic partial order-reduction (#1633)
  • Optimise the efficiency of data race detection (#1544).
  • Support for "printf" for data races check (#1477).
  • Take cur_state->guard into account for creating a new thread (#1463).
  • Fixing dereference in data-races check (#1460).
  • Optimise index races check (#1456).
• Operational models
  • Add libm musl float OMs used in svcomp24 (#1601).
  • Fix range of rand() and random() to include upper endpoint (#1596).
  • Add Operational Model for semaphore (#1536).
  • Added sscanf OM (#1519).
  • Add OM for pthread_rwlock_rdlock (#1516).
  • Rework of the support for builtins (#1435).
• Memory model
  • Pass alignment attribute constraint through to smt (#1593).
  • Value-set considers alignment of references to symbols (#1629).
  • SMT memspace fixes (#1538).
  • Fixed crash caused by invalid id in value set (#1514).
  • Distinguish between valid-memsafety and valid-memcleanup (#1482).
  • Infinity array bounds are no longer checked (#1432).
• General improvements
  • Added missing unwinding assertion loopid (#1635).
  • Protect make_n_ary() from being called with empty list (#1627).
  • Fixed overflow in ID node from witness generation (#1623).
  • Fixed incorrect assertion coverage (#1619).
  • SV-Comp builds includes all supported solvers (#1613).
  • Remove shared_ptr from being used unnecessarily in API (#1612).
  • Improved build instructions for ESBMC-CHERI (#1611).
  • Performance improvement for multi-property verification (#1605).
  • Update Bitwuzla to v0.3.1 (#1604).
  • Show decision runtime for each claim (#1578).
  • Added ARM64 build into CI (#1575).
  • Fixed overflow- encoding (#1560).
  • Fix the general case for string-literal to array conversion (#1549).
  • Update Boolector to v3.2.3 (#1542).
  • Simplify BigInt power2 API (#1532).
  • Do not overwrite location of first instruction during goto-conversion (#1530).
  • Optimize floats memset for zero initialization (#1509).
  • Intrinsic memset claim fix (#1506).
  • Interpret non-adorned fptrs in function argument list (#1503).
  • Add __ESBMC_unreachable() and --enable-unreachability-intrinsic (#1502).
  • Interpret __builtin_unreachable() as no-op for sv-comp (#1500).
  • Fixed wrong line number in if-then-else (#1491).
  • Put some effort into representing array_of terms to the user (#1488).
  • symex_input: use source location of intrinsic for assignments (#1472).
  • Added short circuit for one byte types in optimized memset (#1467).
  • strerror: fix integer overflow (#1457).