Esbmc Versions Save

This is an automated nightly release of ESBMC.

This is an automated nightly release of ESBMC.

• 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)

This is an automated nightly release of ESBMC.

This is an automated nightly release of ESBMC.

• 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 automated nightly release of ESBMC.

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.

This is an automated nightly release of ESBMC.

This is an automated nightly release of ESBMC.