[cmake] update MathSAT download link #2370
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
ChenfengWei0
pushed a commit
that referenced
this pull request
Apr 4, 2025
The master version fails as: ```` Downloading Mathsat -- Downloading MATHSAT from https://mathsat.fbk.eu/download.php?file=mathsat-5.6.10-linux-x86_64.tar.gz -- Extracting MATHSAT CMake Error at src/solvers/mathsat/CMakeLists.txt:20 (message): Could not find mathsat include headers, please check Mathsat_DIR ```` This PR adds the new download link MathSAT: for https://mathsat.fbk.eu/release/mathsat-5.6.11-linux-x86_64.tar.gz. Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
mihaistate
pushed a commit
that referenced
this pull request
Jun 24, 2025
The master version fails as: ```` Downloading Mathsat -- Downloading MATHSAT from https://mathsat.fbk.eu/download.php?file=mathsat-5.6.10-linux-x86_64.tar.gz -- Extracting MATHSAT CMake Error at src/solvers/mathsat/CMakeLists.txt:20 (message): Could not find mathsat include headers, please check Mathsat_DIR ```` This PR adds the new download link MathSAT: for https://mathsat.fbk.eu/release/mathsat-5.6.11-linux-x86_64.tar.gz. Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com>
mihaistate
pushed a commit
that referenced
this pull request
Jun 27, 2025
[OM] Overlapping memory check Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] Added test case to check for overlapping memory Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] Added test to check for NULL in memcpy Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [OM] Check for src and dest NULL Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] detected NULL source pointer Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [OM] return dst if n=0 (nothing to copy) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] check for memcpy output Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Apply automatic changes [TC] add variant of github_60 test (#2362) Make TC from #1175 compatible with windows (#2361) [TC] add TC from #1290 (#2359) Update README.md Update README.md [Z3] Support bitwise for integer arithmetic (#2354) This PR refactors our bitwise operations handling and enhances our SMT conversion functions to better support integer and boolean types. In particular, it introduces more consistent handling for boolean and integer types and improves compatibility with the Z3 solver's bit-vector operations. - [X] bitnot_id - [X] bitxor_id - [x] bitand_id - [x] bitor_id - [x] bitnand_id - [x] bitnor_id - [x] bitnxor_id This PR (30s): ```` Statistics: 33569 Files correct: 18073 correct true: 10743 correct false: 7330 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15456 Score: 27968 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/13956944037 ```` Master (30s): ```` Statistics: 33569 Files correct: 18075 correct true: 10743 correct false: 7332 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15454 Score: 27970 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/13906715936 ```` --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update README.md Update README.md [C verification] remove nonexistent function (#2358) Fixes #2355. nand() doesn't actually exist in the standard C library; the <math.h> header only defines nan(), nanf(), and nanl(). We introduced a new function : -) Update README.md Update stats-600s.txt [cmake] update MathSAT download link (#2370) The master version fails as: ```` Downloading Mathsat -- Downloading MATHSAT from https://mathsat.fbk.eu/download.php?file=mathsat-5.6.10-linux-x86_64.tar.gz -- Extracting MATHSAT CMake Error at src/solvers/mathsat/CMakeLists.txt:20 (message): Could not find mathsat include headers, please check Mathsat_DIR ```` This PR adds the new download link MathSAT: for https://mathsat.fbk.eu/release/mathsat-5.6.11-linux-x86_64.tar.gz. Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md [Overflow] Added overflow_cast to support integer overflow detection (#2367) Fixes #2357. This PR extends the `overflow_cast` method in ESBMC to handle integer arithmetic typecast overflow detection. Key Changes: - Checks for signed and unsigned typecast overflow in integer arithmetic. - Handles cases where values exceed the target type’s range This PR (30s): ```` Statistics: 33569 Files correct: 18079 correct true: 10747 correct false: 7332 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15450 Score: 27978 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/14016741212 ```` Master (30s): ```` Statistics: 33569 Files correct: 18075 correct true: 10743 correct false: 7332 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15454 Score: 27970 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/13906715936 ```` --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update stats-30s.txt [memory-leak] Track global memory (#2372) This PR fixes #2335. Here, 'g' acts as a guard condition, determining whether 'e' should be considered. 'same_object2tc(obj, e)' checks if 'obj' and 'e' refer to the same object; if 'g' is an AND condition (is_and2t) or already a same-object check (is_same_object2t), then 'g' is combined; otherwise, we directly use 'same_object2tc(obj, e).' This PR (30s): ```` Statistics: 33569 Files correct: 18077 correct true: 10751 correct false: 7326 incorrect: 36 incorrect true: 13 incorrect false: 23 unknown: 15456 Score: 28044 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/14046421617 ```` Master (30s): ```` Statistics: 33569 Files correct: 18079 correct true: 10747 correct false: 7332 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15450 Score: 27978 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/14016741212 ```` --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update stats-30s.txt Update stats-300s.txt [overflow] check typecast overflow for signed and unsigned int only (#2376) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [overflow] use resolved_type instead Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-300s.txt [Solidity] fix address modelling (#2379) [OM] Refactoring our C++ operational models: functional (#2381) [python-frontend] Model for numpy.ceil (#2382) - Add operational model for [numpy.ceil](https://numpy.org/doc/stable/reference/generated/numpy.ceil.html#numpy.ceil). - Fix handling of negative numbers in lists. --------- Co-authored-by: brcfarias <1334363+brcfarias@users.noreply.github.com> [Z3] Fix overflow detection for signed subtraction and unsigned division and modulus (#2383) Update README.md [overflow] removed unused variable Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-30s.txt [sv-comp] increase context-switch to 3 (#2378) This PR (900s): ```` Statistics: 3179 Files correct: 1814 correct true: 1360 correct false: 454 incorrect: 40 incorrect true: 23 incorrect false: 17 unknown: 1325 Score: 2166 (max: 5725) https://github.com/esbmc/esbmc/actions/runs/14191126275 ```` Master (900s): ```` Statistics: 3179 Files correct: 1843 correct true: 1409 correct false: 434 incorrect: 61 incorrect true: 43 incorrect false: 18 unknown: 1275 Score: 1588 (max: 5725) https://github.com/esbmc/esbmc/actions/runs/14191018069 ```` --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [Concurrency] unified data race flag (#2385) This PR (900s): ``` Statistics: 1029 Files correct: 530 correct true: 415 correct false: 115 incorrect: 21 incorrect true: 14 incorrect false: 7 unknown: 478 Score: 385 (max: 1823) https://github.com/esbmc/esbmc/actions/runs/14193032102 ``` Master (900s): ``` Statistics: 1029 Files correct: 565 correct true: 449 correct false: 116 incorrect: 24 incorrect true: 18 incorrect false: 6 unknown: 440 Score: 342 (max: 1823) https://github.com/esbmc/esbmc/actions/runs/14193024857 ``` Update ExternalDependencies.cmake (#2390) This should fix the old dependencies which where asking for minimum cmake of < 3.5 --------- Co-authored-by: XLiZHI <958689657@qq.com> Update stats-30s.txt Update stats-300s.txt Update stats-600s.txt [Cov & Sol] Coverage support for Solidity (#2389) [Solidity] Upgrade the AST merging algorithm for multiple files (#2392) [Coverage] fix the covergae algorithm (#2365) [python-frontend] Reuse C libm models for NumPy math functions (#2395) [solidity] create unique temp file to prevent races (#2396) [Solidity] Support Unit keywords && insufficient balance checks (#2393) [Solidity] function call with options (#2398) Update test.desc [data-races-check] get rid of static analysis (#2399) [Solidity] Fix function order bug in AST merge (#2400) [solidity] fix regression (#2402) Fix windows build (#2403) [build] update ESBMC version Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update Release Notes for ESBMC v7.9 (#2404) [python] Fix unary negation (#2406) Update stats-30s.txt [Solidity] add support for several keywords and update modelling algorithm (#2405) [python] Expand numpy math models (#2407) Reusing C models for floor, fabs, sin and exp. [goto-programs] ESBMC Overflow Intrinsic Support (#2408) Fixes rafaelsamenezes/goto-transcoder#2. This PR implements intrinsic functions in ESBMC that perform arithmetic operations with overflow detection. These intrinsics are designed to return both the result of the operation and a flag indicating whether overflow occurred, similar to `__builtin_*_overflow` in GCC/Clang. --- | Intrinsic | Operation | Description | |-----------|-----------|-------------| | `__ESBMC_overflow_result_plus(a, b)` | `a + b` | Addition with overflow check | | `__ESBMC_overflow_result_minus(a, b)` | `a - b` | Subtraction with overflow check | | `__ESBMC_overflow_result_mult(a, b)` | `a * b` | Multiplication with overflow check | | `__ESBMC_overflow_result_shl(a, b)` | `a << b` | Shift-left with overflow check | | `__ESBMC_overflow_result_unary_minus(a)` | `-a` | Unary negation with overflow check | --- Each intrinsic returns a structure: ```c struct __ESBMC_overflow_result { bool overflow; T result; }; --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update stats-300s.txt Update stats-30s.txt [C++ verification] fix std::find function (#2410) [Solidity] Bug fix (#2409) Update README.md [goto-programs] refactored do_function_call_symbol (#2411) [regression] added test case for casting Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for casting Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] enabled test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] disabled test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update CREDITS Update CREDITS [python-frontend] Handling list slicing (#2414) [python] check for float and str comparisons Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Apply automatic changes [python] improved report about the TypeError location Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Apply automatic changes [regression] added test case for casting Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for casting Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] fixed regular expression Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] fixed regular expression Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [Python] add chr() built-in function support (#2416) This PR introduces support for Python’s built-in chr() function in the ESBMC Python frontend. The chr() function takes an integer and returns a one-character string corresponding to the ASCII code of that integer. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] fixed range check Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] refactor our python frontend and extend chr() and float() built-in functions (#2417) This PR enhances the ESBMC Python frontend by improving support for built-in type-casting functions, particularly `chr()` and `float()`, and refining type handling across expressions. It introduces better error detection, stricter type enforcement, and new regression tests to validate behavior. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Fix default variable implementation (#2418) [python] Add support for hex() built-in function (#2419) [python] Handle string comparison for != operator (#2420) [python] add support for python's oct() built-in function (#2421) This PR extends ESBMC’s Python frontend to support the built-in `oct()` function, which converts integers to their octal string representation (e.g., oct(8) → "0o10", oct(-9) → "-0o11"). It adds implementation and regression tests to ensure correct behavior for successful and failing cases. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [util] removed header Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md Update README.md Update README.md [python] Handle ord(): convert single-character string to integer Unicode code point (#2423) This PR implements the `ord()` built-in function as described in the Python documentation (https://docs.python.org/3/library/functions.html#ord): _"Given a string representing one Unicode character, return an integer representing the Unicode code point of that character. For example, ord('a') returns the integer 97 and ord('€') (Euro sign) returns 8364. This is the inverse of [chr()](https://docs.python.org/3/library/functions.html#chr)."_ --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [C++ verification] update operational models (#2424) [python] Support python true division semantics (/) with float type coercion (#2425) This PR supports the Python frontend for correctly handling Python’s true division operator (/) in mixed-type arithmetic, particularly when the result is assigned to a float-annotated variable. It ensures that integer operands are type-coerced to floatbv (IEEE floating-point type) when necessary. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] Improved inference to handle true division (/) operator (#2426) [python] add support for str(float) conversion (#2427) [python] support for int() and float() conversion for symbols (#2429) This PR enhances our Python frontend by supporting Python-style int() and float() conversions on symbolic variables holding string values. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [cmake] enable precompile headers for gcc (#2428) [symex] Support for CPROVER R_OK (#2431) Fixes #2430 (comment). This PR introduces the `__ESBMC_r_ok` intrinsic to ESBMC's symbolic execution engine. This function enables users to verify that a memory read of a specified length from a given address stays within the bounds of the allocated object, improving ESBMC’s ability to check low-level memory safety. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [CI] add static CHERI llvm17 build (#2432) [regression] added test case for division Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] fixed log warning Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] added test case for true division Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> update test.desc (#2433) [python] Refactor get_binary_operator_expr (#2434) [python] fixed log_warning Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] extended numpy test case for math Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] extended numpy test case for fabs Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for numpy.fabs() (#2435) This PR implements support for `numpy.fabs()` function using a native `fabs` implementation in `libm`. It also improves error handling and diagnostics for unsupported NumPy calls in the Python frontend. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [CI] update llvm-16 for windows (#2436) [python] added test cases for numpy math functions (#2437) [regression] enabled test case for exp numpy function Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for Euler constant Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] enabled test case for exp numpy function Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [libm] fix acos function (#2442) fix #2439  https://en.wikipedia.org/wiki/Inverse_trigonometric_functions Update README.md Update README.md [solidity] fix reentry attack checks (#2422) This PR - fix reentry checks algo - fix inheritance - fix contract address assignment --------- Co-authored-by: hejueyun2 <hejueyun@gmail.com> Update stats-30s.txt [python] add support and error checking for Python abs() builtin function (#2441) This PR evaluates the abs() builtin for constant and symbolic numeric types. It also rejects invalid types (e.g., str, list, etc.) with appropriate TypeError messages. Lastly,, it adds test cases to validate valid and invalid uses of abs(). --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update README.md [regression] add test cases for divison by zero function Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md [numpy] Add support for numpy.arccos() and some fixes (#2444) Update README.md [numpy] enhance numpy math function verification coverage (#2445) This PR expands the regression test suite for various NumPy mathematical functions, improves verification accuracy, and addresses known edge cases. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update README.md [regression] added test case for function call Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for function call Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Fix bounds computation for multi-dimensional arrays (#2446) Fixes #2440 Update stats-300s.txt Update README.md Update README.md Update stats-30s.txt Update README.md [regression] added test case for ethereum bug Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [numpy] added integer_squareroot test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [numpy] added integer_squareroot test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [OM] Fix warning messages for pthread and setjmp models (#2448) [OM] removed unnecessary typecast Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md Update README.md Update README.md Update README.md [Solidity] Add support for the library entity (#2394) The purpose of this pull request is to add support for the "library" in Solidity. Update stats-30s.txt [concurrency] : add support for pthread_cleanup_push and pthread_cleanup_pop (#2450) [regression] added test cases for pthread cleanup Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] Set location for the conditional statement (#2453) Fixes #2452. Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update BUILDING.md (#2454) Update some build instructions [pthread] push/pop must match Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-30s.txt [pthread] improved comment for assertion Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added more test cases for chained comparisons Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [Python] Extend support for compound assignment statements (#2458) This PR extends our Python frontend to parse, type check, and translate compound assignment statements (e.g., x += 1, y /= 2) into GOTO code. It includes frontend code changes and regression test cases to ensure correctness and detect corner-case failures such as division by zero and improper type propagation. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] Handling NumPy dot product (#2460) This PR adds C model infrastructure to compute [dot product](https://numpy.org/doc/stable/reference/generated/numpy.dot.html#numpy.dot) of arrays. --------- Co-authored-by: brcfarias <1334363+brcfarias@users.noreply.github.com> [python] build symbolic multiplication tree for power/pow functions (#2462) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] improved comment for handle_power_operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases in Python for while Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases in Python for function call Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases in Python for function call Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] Handle function calls used as arguments (#2465) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] Improve abs() handling (#2466) This PR enhances the Python frontend's `abs()` function handling to detect and reject non-numeric arguments correctly, and to better infer operand types. It addresses two previously undetected or misclassified errors and adds supporting regression tests. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python-frontend] Handling array literals (#2467) [regression] added test for function call + class Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for pass in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] Allow variables in NumPy math function calls (#2469) [regression] added test cases for ceil in numpy Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update numpy.py Update stats-300s.txt [regression] added test cases for logican and in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for mod in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for range in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [SMT solver] Updated Bitwuzla from v0.7.0 to v0.8.0 (#2472) [python] improve range() handling (#2473) [Solidity] Refactoring Mapping (#2468) [python] Handling numpy functions (#2474) [regression] added test cases for power in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [symex] removed temporary fix for the condition coverage (#2477) [python] improved support for power operator (**) (#2478) Disabled broken solvers for benchexec CI (#2481) Yices and Bitwuzla are not building on benchexec CI runs. The crashes seems to be related to GMP. Lets avoid it for now and enable again when it is working. [C verification] Adjust the behavior of parameter checking for the unknown method (#2479) Update README.md [CHERI] support the verification of CHERI capability bounds (#2464) [python] add support for unary+ operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for unary+ operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for unary+ operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [build] fix solvers gmp library link (#2483) We have multiple solvers that depend on the gmp library at the same time, perhaps putting the gmp lib link at the top level is better. https://github.com/esbmc/esbmc/actions/runs/15322131655/job/43108043486 --------- Co-authored-by: Lucas C. Cordeiro <lucasccordeiro@gmail.com> Update stats-30s.txt [python] add support for bytes literals and indexing (#2484) Revert "[build] fix solvers gmp library link" (#2485) Reverts #2483 Revert "Revert "[build] fix solvers gmp library link"" (#2486) Reverts #2485 [python] Add numpy.matmul (#2487) Handling [numpy.matmul](https://numpy.org/doc/stable/reference/generated/numpy.matmul.html) calls. [python] added tests for numpy det Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] added test cases for numpy dot Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] added test cases for numpy transpose Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for Is and IsNot operators (#2480) Update stats-300s.txt [python] add support for numpy.dot() with 1D and mixed-dimension arrays (#2489) This PR extends our Python frontend to support additional `numpy.dot()` operand combinations, enabling verification of vector and matrix dot products across a wider range of dimensions. - 1D × 1D → scalar - 1D × 2D → 1D array - 2D × 1D → 1D array - 2D × 2D → 2D array (already supported) --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] simplified is operator (#2490) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md [python] added test case for None Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] support for "NoneType" (#2493) This PR introduces support for "NoneType" in the type system, represented by a pointer to void. The Python None value is now internally represented as a null pointer (constant_exprt with pointer_type and value "0"). Enhanced AST type inference to detect various forms of None across Python versions (e.g., Constant, NameConstant, and Name). --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [numpy] disallow 3D or higher-dimensional arrays (#2492) Fixes #2491. This PR introduces validation in the Python frontend to reject 3D or higher-dimensional arrays. It includes a new regression test (dot8) to verify that ESBMC correctly throws an error when such input is provided. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] improved return type inference (#2494) This PR enhances our Python frontend’s ability to infer function return types in ESBMC by improving logic in `python_annotation::get_function_return_type`. It adds support for parsing and handling annotated and inferred return types from Python AST nodes. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Co-authored-by: Bruno Farias <brunocarvalhofarias@gmail.com> [regression] Show warning when KNOWNBUG tests stop failing (#2496) **Before:**  **Now:**  CPROVER migration compatibility (#2443) In this PR I am introducing ireps that were originated from CBMC into the migration. However, I am focusing on implementing them as intrinsic function calls. As we can then test the behavior using C files. This is still a draft as it requires: - [x] ~There is a bug in the transcoder that is making the pop_frame assertion break.~ Applying same hack as coverage. - [X] ~Overflow-result needs to invoke our intrinsic function.~ Can't apply late goto transformations. - [X] ~r_ok intrinsic. ~ Will fix in another PR - [X] .goto testcases need to be constructed from CBMC and then adapted to ESBMC format (using goto-transcoder). - [x] ~Export header of ESBMC. This is a C file including all the intrinsic function signatures, this is meant to be exported as a .goto file.~ Testing utilities will be ported to utils (#2476). --------- Co-authored-by: Rafael Sá Menezes <rafael.sa.menezes40@gmail.com> Co-authored-by: rafaelsamenezes <8601807+rafaelsamenezes@users.noreply.github.com> [built-in] model builtin clzll using constraints (#2501) This is a PR of an attempt to model a builtin function with assumptions The algorithm is as follows: ``` 1. nondet symbol clz_sym（uint64） 2. assert(x != 0) 3. assume(0 ≤ clz_sym ≤ 63) 4. idx = 63 - clz_sym 5. assume(((x >> idx) & 1) != 0) 6. assume((x >> (idx+1)) == 0) 7. return (int)clz_sym ``` [python] enhanced string comparison handling (#2497) This PR introduces a significant enhancement to the Python frontend's handling of string comparisons, specifically improving the accuracy and robustness of equality checks involving string-returning functions. It adds new logic for constant resolution and identity function detection and expands regression test coverage with various string manipulation scenarios. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [smt] don't access vector out of bounds (#2502) `reserve` only changes the capacity, but not the size. After `args.reserve(20)`, `args[10]` would still fail. The loop that initialized all `args` has been changed to use push_back instead of indices. The few cases that later tried to write to e.g. `args[0]` where there was previously no value written to `args[0]` have been changed to now do the write. Alternative to #2498 Co-authored-by: intrigus <abc123zeus@live.de> [python] Handle string annotations like -> int (#2495) Update stats-30s.txt [goto-programs] add validation for invalid member accesses on incomplete or incorrectly typed expressions (Fixes #2236) (#2500) [python] check for sideeffect in is_zero_length_array Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] avoid string comparison with sideeffects Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] added test cases for ternary operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-30s.txt [regression] added test case for overflow/nan Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md Update README.md Update README.md [CHERI] hide compressed/decompressed trace (#2504) The counterexample becomes cleaner [python] enhanced handling of true division (#2505) This PR introduces several enhancements to the ESBMC Python frontend (`python_converter.cpp`) to more accurately model Python semantics for true division (/). --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update README.md [python] implement pow symbolically (#2506) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [regression] removed --incremental-bmc Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-600s.txt [python] add support for python built-in function handling (#2507) [regression] added test case from #1599 Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case from #1599 Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] removed test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for transforming general python for loops over iterables (#2508) [regression] added test case for Python class Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] improved test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] Fix compound assignment on object attributes (#2509) [python] added test case for assert stmt Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for class Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] handles assertions involving function calls and refactor attribute handling (#2510) [python] added test case for class Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for realloc [CI] Integrate cheribsd-riscv64 system root (#2447) The build on GitHub runner using cheribuild took too long and exceeded the runner's hard disk capacity. Currently I have uploaded the cheribsd SDK built locally and hope it works as expected. ;) [regression] added test case for realloc [c++] added test case for vector Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [cpp] resolve mismatch template deduction errors with pointer types (#2517) [cpp] add support for std::is_sorted and improve vector initialization (#2515) [c++] implement missing ostreambuf_iterator methods for STL algorithm support (#2519) [cpp] Fix vector const_reverse_iterator implementation for reverse iteration support (#2520) Implement the `const_reverse_iterator` class with conversion constructors and operators derived from `reverse_iterator`. Add missing `const rbegin()/rend()` method implementations. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] fix map::insert() to accept temporary pair objects (#2521) This PR changes `map::insert(value_type &val)` to `map::insert(const value_type &val)` to allow binding to rvalue references. This fixes compilation errors when inserting temporary pair objects such as `mymap.insert(pair<char,int>('a', 100));`. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] fix multiset constructor ambiguity (#2522) [c++] fix deque iterator increment operators binding to temporary (#2523) [c++] fix npos handling (#2525) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] fix iterator assignment operators (#2526) [goto-symex] use size directly (#2516) [c++] add explicit int overload for list::insert and replace invalid null check in remove_if (#2527) [c++] fix STL operator overload resolution errors in ostream, sstream and string headers (#2528) [c++] add basic unordered_set support (#2529) [solidity] improve overall performance (#2511) ```sh Over 5 mins esbmc --sol example.sol example.solast --incremental-bmc --no-standard-checks 1.90s user 0.19s system 64% cpu 3.255 total Over 5 mins esbmc --sol example.sol example.solast --contract Reproduction 4.13s user 0.20s system 80% cpu 5.384 total ```  now the whole regression test can be finished in 120 second (-j 8) --- This PR also contains some bug fixing, including library API (_max/_min), address binding in trusted mode --------- Co-authored-by: hejueyun2 <hejueyun@gmail.com> [c++] added basic std::unordered_map support (#2530) This PR introduces initial support for `std::unordered_map` in our C++ model, along with corresponding regression tests to validate its correctness and error detection capabilities. The support includes a simplified internal implementation suitable for bounded model checking, and test cases to ensure expected behavior. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] removed esbmc_forward_iterator_tag Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for Python range Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Consider the guard when dealing with sideeffects (#2514) This is one of the known problems: 1. The current guard needs to be taken into account when dealing with memory allocation, especially in if expressions. 2. There is something wrong with our realloc operation that causes out of bound. This is because we only adjust the bound in the track new pointer, while nothing changes in the dynamic object. I tried to modify the symbol directly, but at the SMT level there was a bit width mismatch. Should we rethink the implementation of realloc, perhaps malloc and memcpy would be a good approach instead? [c++] added test case for vector Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [C++ verification] Add a new implementation of typeid (#2534) The type of polymorphism needs to be fetched at runtime, which is not handled by the frontend, so for now we skip it for preliminary support. The TC in this PR reflects all currently supported methods. [c++] fix vector default constructor: remove explicit keyword (#2535) [regression] reduced verification time for insert2_fail Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] reduced verification time for emplace_fail Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for vector Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] add allocator template parameter to std::vector (#2536) Update main.cpp [c++] applied coding style to vector Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] add deterministic hash specializations for std::hash (#2538) [python] added test case for range Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Address incosistent behaviour in dump_smt function across solvers (#2524) Updated the z3_convt::output_smt() and the bitwulza_convt::dump_smt() functions to print to stdout when no output was defined Improved the handling of empty and "-" output paths in the smtlib_conv::dump_smt() function Addressed issue #2167 --------- Signed-off-by: mihaistate05 <mihaita.state@yahoo.com> Signed-off-by: mihaistate <mihai.state03@yahoo.com> Signed-off-by: mihaistate05 <mihai.state03@yahoo.com> Co-authored-by: mihaistate05 <mihaita.state@yahoo.com> [CI] improve auto commit (#2540) Improve the code style check CI: Only branches in the ESBMC repository will trigger the auto commit, because git commit does not have permission to modify other repositories. Otherwise, we show the corresponding code, throw an error. Update stats-300s.txt Update stats-30s.txt
mihaistate
added a commit
that referenced
this pull request
Jun 27, 2025
Created a new memcpy function that copies 8 bytes per iteration The if statement checks that both dst and src pointers are 8-byte aligned. If they are, it copies 8 bytes of memory using uint64_t pointers for efficiency. Remaining bytes are handled in a trailing byte loop. If the pointers are not 8-bytes aligned, the function falls back to a safe byte-by-byte copy. Signed-off-by: mihaistate05 <mihai.state03@yahoo.com> [TC] add variant of github_60 test (#2362) Make TC from #1175 compatible with windows (#2361) [TC] add TC from #1290 (#2359) Update README.md Update README.md [Z3] Support bitwise for integer arithmetic (#2354) This PR refactors our bitwise operations handling and enhances our SMT conversion functions to better support integer and boolean types. In particular, it introduces more consistent handling for boolean and integer types and improves compatibility with the Z3 solver's bit-vector operations. - [X] bitnot_id - [X] bitxor_id - [x] bitand_id - [x] bitor_id - [x] bitnand_id - [x] bitnor_id - [x] bitnxor_id This PR (30s): ```` Statistics: 33569 Files correct: 18073 correct true: 10743 correct false: 7330 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15456 Score: 27968 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/13956944037 ```` Master (30s): ```` Statistics: 33569 Files correct: 18075 correct true: 10743 correct false: 7332 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15454 Score: 27970 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/13906715936 ```` --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update README.md Update README.md [C verification] remove nonexistent function (#2358) Fixes #2355. nand() doesn't actually exist in the standard C library; the <math.h> header only defines nan(), nanf(), and nanl(). We introduced a new function : -) Update README.md Update stats-600s.txt [cmake] update MathSAT download link (#2370) The master version fails as: ```` Downloading Mathsat -- Downloading MATHSAT from https://mathsat.fbk.eu/download.php?file=mathsat-5.6.10-linux-x86_64.tar.gz -- Extracting MATHSAT CMake Error at src/solvers/mathsat/CMakeLists.txt:20 (message): Could not find mathsat include headers, please check Mathsat_DIR ```` This PR adds the new download link MathSAT: for https://mathsat.fbk.eu/release/mathsat-5.6.11-linux-x86_64.tar.gz. Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md [Overflow] Added overflow_cast to support integer overflow detection (#2367) Fixes #2357. This PR extends the `overflow_cast` method in ESBMC to handle integer arithmetic typecast overflow detection. Key Changes: - Checks for signed and unsigned typecast overflow in integer arithmetic. - Handles cases where values exceed the target type’s range This PR (30s): ```` Statistics: 33569 Files correct: 18079 correct true: 10747 correct false: 7332 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15450 Score: 27978 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/14016741212 ```` Master (30s): ```` Statistics: 33569 Files correct: 18075 correct true: 10743 correct false: 7332 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15454 Score: 27970 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/13906715936 ```` --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update stats-30s.txt [memory-leak] Track global memory (#2372) This PR fixes #2335. Here, 'g' acts as a guard condition, determining whether 'e' should be considered. 'same_object2tc(obj, e)' checks if 'obj' and 'e' refer to the same object; if 'g' is an AND condition (is_and2t) or already a same-object check (is_same_object2t), then 'g' is combined; otherwise, we directly use 'same_object2tc(obj, e).' This PR (30s): ```` Statistics: 33569 Files correct: 18077 correct true: 10751 correct false: 7326 incorrect: 36 incorrect true: 13 incorrect false: 23 unknown: 15456 Score: 28044 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/14046421617 ```` Master (30s): ```` Statistics: 33569 Files correct: 18079 correct true: 10747 correct false: 7332 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15450 Score: 27978 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/14016741212 ```` --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update stats-30s.txt Update stats-300s.txt [overflow] check typecast overflow for signed and unsigned int only (#2376) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [overflow] use resolved_type instead Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-300s.txt [Solidity] fix address modelling (#2379) [OM] Refactoring our C++ operational models: functional (#2381) [python-frontend] Model for numpy.ceil (#2382) - Add operational model for [numpy.ceil](https://numpy.org/doc/stable/reference/generated/numpy.ceil.html#numpy.ceil). - Fix handling of negative numbers in lists. --------- Co-authored-by: brcfarias <1334363+brcfarias@users.noreply.github.com> [Z3] Fix overflow detection for signed subtraction and unsigned division and modulus (#2383) Update README.md [overflow] removed unused variable Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-30s.txt [sv-comp] increase context-switch to 3 (#2378) This PR (900s): ```` Statistics: 3179 Files correct: 1814 correct true: 1360 correct false: 454 incorrect: 40 incorrect true: 23 incorrect false: 17 unknown: 1325 Score: 2166 (max: 5725) https://github.com/esbmc/esbmc/actions/runs/14191126275 ```` Master (900s): ```` Statistics: 3179 Files correct: 1843 correct true: 1409 correct false: 434 incorrect: 61 incorrect true: 43 incorrect false: 18 unknown: 1275 Score: 1588 (max: 5725) https://github.com/esbmc/esbmc/actions/runs/14191018069 ```` --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [Concurrency] unified data race flag (#2385) This PR (900s): ``` Statistics: 1029 Files correct: 530 correct true: 415 correct false: 115 incorrect: 21 incorrect true: 14 incorrect false: 7 unknown: 478 Score: 385 (max: 1823) https://github.com/esbmc/esbmc/actions/runs/14193032102 ``` Master (900s): ``` Statistics: 1029 Files correct: 565 correct true: 449 correct false: 116 incorrect: 24 incorrect true: 18 incorrect false: 6 unknown: 440 Score: 342 (max: 1823) https://github.com/esbmc/esbmc/actions/runs/14193024857 ``` Update ExternalDependencies.cmake (#2390) This should fix the old dependencies which where asking for minimum cmake of < 3.5 --------- Co-authored-by: XLiZHI <958689657@qq.com> Update stats-30s.txt Update stats-300s.txt Update stats-600s.txt [Cov & Sol] Coverage support for Solidity (#2389) [Solidity] Upgrade the AST merging algorithm for multiple files (#2392) [Coverage] fix the covergae algorithm (#2365) [python-frontend] Reuse C libm models for NumPy math functions (#2395) [solidity] create unique temp file to prevent races (#2396) [Solidity] Support Unit keywords && insufficient balance checks (#2393) [Solidity] function call with options (#2398) Update test.desc [data-races-check] get rid of static analysis (#2399) [Solidity] Fix function order bug in AST merge (#2400) [solidity] fix regression (#2402) Fix windows build (#2403) [build] update ESBMC version Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update Release Notes for ESBMC v7.9 (#2404) [python] Fix unary negation (#2406) Update stats-30s.txt [Solidity] add support for several keywords and update modelling algorithm (#2405) [python] Expand numpy math models (#2407) Reusing C models for floor, fabs, sin and exp. [goto-programs] ESBMC Overflow Intrinsic Support (#2408) Fixes rafaelsamenezes/goto-transcoder#2. This PR implements intrinsic functions in ESBMC that perform arithmetic operations with overflow detection. These intrinsics are designed to return both the result of the operation and a flag indicating whether overflow occurred, similar to `__builtin_*_overflow` in GCC/Clang. --- | Intrinsic | Operation | Description | |-----------|-----------|-------------| | `__ESBMC_overflow_result_plus(a, b)` | `a + b` | Addition with overflow check | | `__ESBMC_overflow_result_minus(a, b)` | `a - b` | Subtraction with overflow check | | `__ESBMC_overflow_result_mult(a, b)` | `a * b` | Multiplication with overflow check | | `__ESBMC_overflow_result_shl(a, b)` | `a << b` | Shift-left with overflow check | | `__ESBMC_overflow_result_unary_minus(a)` | `-a` | Unary negation with overflow check | --- Each intrinsic returns a structure: ```c struct __ESBMC_overflow_result { bool overflow; T result; }; --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update stats-300s.txt Update stats-30s.txt [C++ verification] fix std::find function (#2410) [Solidity] Bug fix (#2409) Update README.md [goto-programs] refactored do_function_call_symbol (#2411) [regression] added test case for casting Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for casting Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] enabled test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] disabled test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update CREDITS Update CREDITS [python-frontend] Handling list slicing (#2414) [python] check for float and str comparisons Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Apply automatic changes [python] improved report about the TypeError location Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Apply automatic changes [regression] added test case for casting Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for casting Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] fixed regular expression Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] fixed regular expression Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [Python] add chr() built-in function support (#2416) This PR introduces support for Python’s built-in chr() function in the ESBMC Python frontend. The chr() function takes an integer and returns a one-character string corresponding to the ASCII code of that integer. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] fixed range check Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] refactor our python frontend and extend chr() and float() built-in functions (#2417) This PR enhances the ESBMC Python frontend by improving support for built-in type-casting functions, particularly `chr()` and `float()`, and refining type handling across expressions. It introduces better error detection, stricter type enforcement, and new regression tests to validate behavior. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Fix default variable implementation (#2418) [python] Add support for hex() built-in function (#2419) [python] Handle string comparison for != operator (#2420) [python] add support for python's oct() built-in function (#2421) This PR extends ESBMC’s Python frontend to support the built-in `oct()` function, which converts integers to their octal string representation (e.g., oct(8) → "0o10", oct(-9) → "-0o11"). It adds implementation and regression tests to ensure correct behavior for successful and failing cases. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [util] removed header Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md Update README.md Update README.md [python] Handle ord(): convert single-character string to integer Unicode code point (#2423) This PR implements the `ord()` built-in function as described in the Python documentation (https://docs.python.org/3/library/functions.html#ord): _"Given a string representing one Unicode character, return an integer representing the Unicode code point of that character. For example, ord('a') returns the integer 97 and ord('€') (Euro sign) returns 8364. This is the inverse of [chr()](https://docs.python.org/3/library/functions.html#chr)."_ --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [C++ verification] update operational models (#2424) [python] Support python true division semantics (/) with float type coercion (#2425) This PR supports the Python frontend for correctly handling Python’s true division operator (/) in mixed-type arithmetic, particularly when the result is assigned to a float-annotated variable. It ensures that integer operands are type-coerced to floatbv (IEEE floating-point type) when necessary. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] Improved inference to handle true division (/) operator (#2426) [python] add support for str(float) conversion (#2427) [python] support for int() and float() conversion for symbols (#2429) This PR enhances our Python frontend by supporting Python-style int() and float() conversions on symbolic variables holding string values. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [cmake] enable precompile headers for gcc (#2428) [symex] Support for CPROVER R_OK (#2431) Fixes #2430 (comment). This PR introduces the `__ESBMC_r_ok` intrinsic to ESBMC's symbolic execution engine. This function enables users to verify that a memory read of a specified length from a given address stays within the bounds of the allocated object, improving ESBMC’s ability to check low-level memory safety. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [CI] add static CHERI llvm17 build (#2432) [regression] added test case for division Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] fixed log warning Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] added test case for true division Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> update test.desc (#2433) [python] Refactor get_binary_operator_expr (#2434) [python] fixed log_warning Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] extended numpy test case for math Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] extended numpy test case for fabs Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for numpy.fabs() (#2435) This PR implements support for `numpy.fabs()` function using a native `fabs` implementation in `libm`. It also improves error handling and diagnostics for unsupported NumPy calls in the Python frontend. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [CI] update llvm-16 for windows (#2436) [python] added test cases for numpy math functions (#2437) [regression] enabled test case for exp numpy function Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for Euler constant Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] enabled test case for exp numpy function Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [libm] fix acos function (#2442) fix #2439  https://en.wikipedia.org/wiki/Inverse_trigonometric_functions Update README.md Update README.md [solidity] fix reentry attack checks (#2422) This PR - fix reentry checks algo - fix inheritance - fix contract address assignment --------- Co-authored-by: hejueyun2 <hejueyun@gmail.com> Update stats-30s.txt [python] add support and error checking for Python abs() builtin function (#2441) This PR evaluates the abs() builtin for constant and symbolic numeric types. It also rejects invalid types (e.g., str, list, etc.) with appropriate TypeError messages. Lastly,, it adds test cases to validate valid and invalid uses of abs(). --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update README.md [regression] add test cases for divison by zero function Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md [numpy] Add support for numpy.arccos() and some fixes (#2444) Update README.md [numpy] enhance numpy math function verification coverage (#2445) This PR expands the regression test suite for various NumPy mathematical functions, improves verification accuracy, and addresses known edge cases. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update README.md [regression] added test case for function call Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for function call Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Fix bounds computation for multi-dimensional arrays (#2446) Fixes #2440 Update stats-300s.txt Update README.md Update README.md Update stats-30s.txt Update README.md [regression] added test case for ethereum bug Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [numpy] added integer_squareroot test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [numpy] added integer_squareroot test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [OM] Fix warning messages for pthread and setjmp models (#2448) [OM] removed unnecessary typecast Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md Update README.md Update README.md Update README.md [Solidity] Add support for the library entity (#2394) The purpose of this pull request is to add support for the "library" in Solidity. Update stats-30s.txt [concurrency] : add support for pthread_cleanup_push and pthread_cleanup_pop (#2450) [regression] added test cases for pthread cleanup Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] Set location for the conditional statement (#2453) Fixes #2452. Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update BUILDING.md (#2454) Update some build instructions [pthread] push/pop must match Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-30s.txt [pthread] improved comment for assertion Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added more test cases for chained comparisons Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [Python] Extend support for compound assignment statements (#2458) This PR extends our Python frontend to parse, type check, and translate compound assignment statements (e.g., x += 1, y /= 2) into GOTO code. It includes frontend code changes and regression test cases to ensure correctness and detect corner-case failures such as division by zero and improper type propagation. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] Handling NumPy dot product (#2460) This PR adds C model infrastructure to compute [dot product](https://numpy.org/doc/stable/reference/generated/numpy.dot.html#numpy.dot) of arrays. --------- Co-authored-by: brcfarias <1334363+brcfarias@users.noreply.github.com> [python] build symbolic multiplication tree for power/pow functions (#2462) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] improved comment for handle_power_operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases in Python for while Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases in Python for function call Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases in Python for function call Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] Handle function calls used as arguments (#2465) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] Improve abs() handling (#2466) This PR enhances the Python frontend's `abs()` function handling to detect and reject non-numeric arguments correctly, and to better infer operand types. It addresses two previously undetected or misclassified errors and adds supporting regression tests. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python-frontend] Handling array literals (#2467) [regression] added test for function call + class Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for pass in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] Allow variables in NumPy math function calls (#2469) [regression] added test cases for ceil in numpy Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update numpy.py Update stats-300s.txt [regression] added test cases for logican and in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for mod in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for range in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [SMT solver] Updated Bitwuzla from v0.7.0 to v0.8.0 (#2472) [python] improve range() handling (#2473) [Solidity] Refactoring Mapping (#2468) [python] Handling numpy functions (#2474) [regression] added test cases for power in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [symex] removed temporary fix for the condition coverage (#2477) [python] improved support for power operator (**) (#2478) Disabled broken solvers for benchexec CI (#2481) Yices and Bitwuzla are not building on benchexec CI runs. The crashes seems to be related to GMP. Lets avoid it for now and enable again when it is working. [C verification] Adjust the behavior of parameter checking for the unknown method (#2479) Update README.md [CHERI] support the verification of CHERI capability bounds (#2464) [python] add support for unary+ operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for unary+ operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for unary+ operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [build] fix solvers gmp library link (#2483) We have multiple solvers that depend on the gmp library at the same time, perhaps putting the gmp lib link at the top level is better. https://github.com/esbmc/esbmc/actions/runs/15322131655/job/43108043486 --------- Co-authored-by: Lucas C. Cordeiro <lucasccordeiro@gmail.com> Update stats-30s.txt [python] add support for bytes literals and indexing (#2484) Revert "[build] fix solvers gmp library link" (#2485) Reverts #2483 Revert "Revert "[build] fix solvers gmp library link"" (#2486) Reverts #2485 [python] Add numpy.matmul (#2487) Handling [numpy.matmul](https://numpy.org/doc/stable/reference/generated/numpy.matmul.html) calls. [python] added tests for numpy det Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] added test cases for numpy dot Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] added test cases for numpy transpose Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for Is and IsNot operators (#2480) Update stats-300s.txt [python] add support for numpy.dot() with 1D and mixed-dimension arrays (#2489) This PR extends our Python frontend to support additional `numpy.dot()` operand combinations, enabling verification of vector and matrix dot products across a wider range of dimensions. - 1D × 1D → scalar - 1D × 2D → 1D array - 2D × 1D → 1D array - 2D × 2D → 2D array (already supported) --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] simplified is operator (#2490) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md [python] added test case for None Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] support for "NoneType" (#2493) This PR introduces support for "NoneType" in the type system, represented by a pointer to void. The Python None value is now internally represented as a null pointer (constant_exprt with pointer_type and value "0"). Enhanced AST type inference to detect various forms of None across Python versions (e.g., Constant, NameConstant, and Name). --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [numpy] disallow 3D or higher-dimensional arrays (#2492) Fixes #2491. This PR introduces validation in the Python frontend to reject 3D or higher-dimensional arrays. It includes a new regression test (dot8) to verify that ESBMC correctly throws an error when such input is provided. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] improved return type inference (#2494) This PR enhances our Python frontend’s ability to infer function return types in ESBMC by improving logic in `python_annotation::get_function_return_type`. It adds support for parsing and handling annotated and inferred return types from Python AST nodes. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Co-authored-by: Bruno Farias <brunocarvalhofarias@gmail.com> [regression] Show warning when KNOWNBUG tests stop failing (#2496) **Before:**  **Now:**  CPROVER migration compatibility (#2443) In this PR I am introducing ireps that were originated from CBMC into the migration. However, I am focusing on implementing them as intrinsic function calls. As we can then test the behavior using C files. This is still a draft as it requires: - [x] ~There is a bug in the transcoder that is making the pop_frame assertion break.~ Applying same hack as coverage. - [X] ~Overflow-result needs to invoke our intrinsic function.~ Can't apply late goto transformations. - [X] ~r_ok intrinsic. ~ Will fix in another PR - [X] .goto testcases need to be constructed from CBMC and then adapted to ESBMC format (using goto-transcoder). - [x] ~Export header of ESBMC. This is a C file including all the intrinsic function signatures, this is meant to be exported as a .goto file.~ Testing utilities will be ported to utils (#2476). --------- Co-authored-by: Rafael Sá Menezes <rafael.sa.menezes40@gmail.com> Co-authored-by: rafaelsamenezes <8601807+rafaelsamenezes@users.noreply.github.com> [built-in] model builtin clzll using constraints (#2501) This is a PR of an attempt to model a builtin function with assumptions The algorithm is as follows: ``` 1. nondet symbol clz_sym（uint64） 2. assert(x != 0) 3. assume(0 ≤ clz_sym ≤ 63) 4. idx = 63 - clz_sym 5. assume(((x >> idx) & 1) != 0) 6. assume((x >> (idx+1)) == 0) 7. return (int)clz_sym ``` [python] enhanced string comparison handling (#2497) This PR introduces a significant enhancement to the Python frontend's handling of string comparisons, specifically improving the accuracy and robustness of equality checks involving string-returning functions. It adds new logic for constant resolution and identity function detection and expands regression test coverage with various string manipulation scenarios. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [smt] don't access vector out of bounds (#2502) `reserve` only changes the capacity, but not the size. After `args.reserve(20)`, `args[10]` would still fail. The loop that initialized all `args` has been changed to use push_back instead of indices. The few cases that later tried to write to e.g. `args[0]` where there was previously no value written to `args[0]` have been changed to now do the write. Alternative to #2498 Co-authored-by: intrigus <abc123zeus@live.de> [python] Handle string annotations like -> int (#2495) Update stats-30s.txt [goto-programs] add validation for invalid member accesses on incomplete or incorrectly typed expressions (Fixes #2236) (#2500) [python] check for sideeffect in is_zero_length_array Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] avoid string comparison with sideeffects Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] added test cases for ternary operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-30s.txt [regression] added test case for overflow/nan Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md Update README.md Update README.md [CHERI] hide compressed/decompressed trace (#2504) The counterexample becomes cleaner [python] enhanced handling of true division (#2505) This PR introduces several enhancements to the ESBMC Python frontend (`python_converter.cpp`) to more accurately model Python semantics for true division (/). --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update README.md [python] implement pow symbolically (#2506) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [regression] removed --incremental-bmc Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-600s.txt [python] add support for python built-in function handling (#2507) [regression] added test case from #1599 Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case from #1599 Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] removed test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for transforming general python for loops over iterables (#2508) [regression] added test case for Python class Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] improved test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] Fix compound assignment on object attributes (#2509) [python] added test case for assert stmt Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for class Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] handles assertions involving function calls and refactor attribute handling (#2510) [python] added test case for class Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for realloc [CI] Integrate cheribsd-riscv64 system root (#2447) The build on GitHub runner using cheribuild took too long and exceeded the runner's hard disk capacity. Currently I have uploaded the cheribsd SDK built locally and hope it works as expected. ;) [regression] added test case for realloc [c++] added test case for vector Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [cpp] resolve mismatch template deduction errors with pointer types (#2517) [cpp] add support for std::is_sorted and improve vector initialization (#2515) [c++] implement missing ostreambuf_iterator methods for STL algorithm support (#2519) [cpp] Fix vector const_reverse_iterator implementation for reverse iteration support (#2520) Implement the `const_reverse_iterator` class with conversion constructors and operators derived from `reverse_iterator`. Add missing `const rbegin()/rend()` method implementations. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] fix map::insert() to accept temporary pair objects (#2521) This PR changes `map::insert(value_type &val)` to `map::insert(const value_type &val)` to allow binding to rvalue references. This fixes compilation errors when inserting temporary pair objects such as `mymap.insert(pair<char,int>('a', 100));`. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] fix multiset constructor ambiguity (#2522) [c++] fix deque iterator increment operators binding to temporary (#2523) [c++] fix npos handling (#2525) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] fix iterator assignment operators (#2526) [goto-symex] use size directly (#2516) [c++] add explicit int overload for list::insert and replace invalid null check in remove_if (#2527) [c++] fix STL operator overload resolution errors in ostream, sstream and string headers (#2528) [c++] add basic unordered_set support (#2529) [solidity] improve overall performance (#2511) ```sh Over 5 mins esbmc --sol example.sol example.solast --incremental-bmc --no-standard-checks 1.90s user 0.19s system 64% cpu 3.255 total Over 5 mins esbmc --sol example.sol example.solast --contract Reproduction 4.13s user 0.20s system 80% cpu 5.384 total ```  now the whole regression test can be finished in 120 second (-j 8) --- This PR also contains some bug fixing, including library API (_max/_min), address binding in trusted mode --------- Co-authored-by: hejueyun2 <hejueyun@gmail.com> [c++] added basic std::unordered_map support (#2530) This PR introduces initial support for `std::unordered_map` in our C++ model, along with corresponding regression tests to validate its correctness and error detection capabilities. The support includes a simplified internal implementation suitable for bounded model checking, and test cases to ensure expected behavior. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] removed esbmc_forward_iterator_tag Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for Python range Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Consider the guard when dealing with sideeffects (#2514) This is one of the known problems: 1. The current guard needs to be taken into account when dealing with memory allocation, especially in if expressions. 2. There is something wrong with our realloc operation that causes out of bound. This is because we only adjust the bound in the track new pointer, while nothing changes in the dynamic object. I tried to modify the symbol directly, but at the SMT level there was a bit width mismatch. Should we rethink the implementation of realloc, perhaps malloc and memcpy would be a good approach instead? [c++] added test case for vector Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [C++ verification] Add a new implementation of typeid (#2534) The type of polymorphism needs to be fetched at runtime, which is not handled by the frontend, so for now we skip it for preliminary support. The TC in this PR reflects all currently supported methods. [c++] fix vector default constructor: remove explicit keyword (#2535) [regression] reduced verification time for insert2_fail Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] reduced verification time for emplace_fail Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for vector Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] add allocator template parameter to std::vector (#2536) Update main.cpp [c++] applied coding style to vector Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] add deterministic hash specializations for std::hash (#2538) [python] added test case for range Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Address incosistent behaviour in dump_smt function across solvers (#2524) Updated the z3_convt::output_smt() and the bitwulza_convt::dump_smt() functions to print to stdout when no output was defined Improved the handling of empty and "-" output paths in the smtlib_conv::dump_smt() function Addressed issue #2167 --------- Signed-off-by: mihaistate05 <mihaita.state@yahoo.com> Signed-off-by: mihaistate <mihai.state03@yahoo.com> Signed-off-by: mihaistate05 <mihai.state03@yahoo.com> Co-authored-by: mihaistate05 <mihaita.state@yahoo.com> [CI] improve auto commit (#2540) Improve the code style check CI: Only branches in the ESBMC repository will trigger the auto commit, because git commit does not have permission to modify other repositories. Otherwise, we show the corresponding code, throw an error. Update stats-300s.txt Update stats-30s.txt [c++] fixed typos in string Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] fix namespace collision in functional header (#2541) This PR replaces unqualified `std::` references with `::std::` to resolve parsing errors where ESBMC incorrectly looks up standard library features in `__shedskin__::std` (https://github.com/shedskin/shedskin/blob/master/shedskin/lib/builtin/hash.hpp) instead of the `global ::std` namespace. ```` ESBMC version 7.9.0 64-bit x86_64 linux Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc Parsing main.cpp In file included from main.cpp:1: In file included from ./builtin.hpp:223: In file included from ./builtin/hash.hpp:5: /tmp/esbmc-cpp-headers-ba1b-0202-35ea/functional:50:50: error: no template named 'forward' in namespace '__shedskin__::std'; did you mean '::std::forward'? explicit callable_wrapper(Callable &&f) : func(std::forward<Callable>(f)) ^~~~~ /../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/move.h:77:5: note: '::std::forward' declared here forward(typename std::remove_reference<_Tp>::type& __t) noexcept ^ In file included from main.cpp:1: In file included from ./builtin.hpp:223: In file included from ./builtin/hash.hpp:5: /tmp/esbmc-cpp-headers-ba1b-0202-35ea/functional:50:50: error: no template named 'forward' in namespace '__shedskin__::std'; did you mean '::std::forward'? explicit callable_wrapper(Callable &&f) : func(std::forward<Callable>(f)) ```` Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] added basic bitset operational model (#2543) [python-frontend] Handling string attributes (#2546) - Handle string attributes as char pointers; - Append `'\0'` to char arrays to enable use of `strcmp` for string comparisons. --------- Co-authored-by: brcfarias <1334363+brcfarias@users.noreply.github.com>
mihaistate
added a commit
that referenced
this pull request
Jun 27, 2025
Update stats-300s.txt [OM] Overlapping memory check Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] Added test case to check for overlapping memory Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] Added test to check for NULL in memcpy Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [OM] Check for src and dest NULL Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] detected NULL source pointer Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [OM] return dst if n=0 (nothing to copy) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] check for memcpy output Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Apply automatic changes [TC] add variant of github_60 test (#2362) Make TC from #1175 compatible with windows (#2361) [TC] add TC from #1290 (#2359) Update README.md Update README.md [Z3] Support bitwise for integer arithmetic (#2354) This PR refactors our bitwise operations handling and enhances our SMT conversion functions to better support integer and boolean types. In particular, it introduces more consistent handling for boolean and integer types and improves compatibility with the Z3 solver's bit-vector operations. - [X] bitnot_id - [X] bitxor_id - [x] bitand_id - [x] bitor_id - [x] bitnand_id - [x] bitnor_id - [x] bitnxor_id This PR (30s): ```` Statistics: 33569 Files correct: 18073 correct true: 10743 correct false: 7330 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15456 Score: 27968 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/13956944037 ```` Master (30s): ```` Statistics: 33569 Files correct: 18075 correct true: 10743 correct false: 7332 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15454 Score: 27970 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/13906715936 ```` --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update README.md Update README.md [C verification] remove nonexistent function (#2358) Fixes #2355. nand() doesn't actually exist in the standard C library; the <math.h> header only defines nan(), nanf(), and nanl(). We introduced a new function : -) Update README.md Update stats-600s.txt [cmake] update MathSAT download link (#2370) The master version fails as: ```` Downloading Mathsat -- Downloading MATHSAT from https://mathsat.fbk.eu/download.php?file=mathsat-5.6.10-linux-x86_64.tar.gz -- Extracting MATHSAT CMake Error at src/solvers/mathsat/CMakeLists.txt:20 (message): Could not find mathsat include headers, please check Mathsat_DIR ```` This PR adds the new download link MathSAT: for https://mathsat.fbk.eu/release/mathsat-5.6.11-linux-x86_64.tar.gz. Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md [Overflow] Added overflow_cast to support integer overflow detection (#2367) Fixes #2357. This PR extends the `overflow_cast` method in ESBMC to handle integer arithmetic typecast overflow detection. Key Changes: - Checks for signed and unsigned typecast overflow in integer arithmetic. - Handles cases where values exceed the target type’s range This PR (30s): ```` Statistics: 33569 Files correct: 18079 correct true: 10747 correct false: 7332 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15450 Score: 27978 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/14016741212 ```` Master (30s): ```` Statistics: 33569 Files correct: 18075 correct true: 10743 correct false: 7332 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15454 Score: 27970 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/13906715936 ```` --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update stats-30s.txt [memory-leak] Track global memory (#2372) This PR fixes #2335. Here, 'g' acts as a guard condition, determining whether 'e' should be considered. 'same_object2tc(obj, e)' checks if 'obj' and 'e' refer to the same object; if 'g' is an AND condition (is_and2t) or already a same-object check (is_same_object2t), then 'g' is combined; otherwise, we directly use 'same_object2tc(obj, e).' This PR (30s): ```` Statistics: 33569 Files correct: 18077 correct true: 10751 correct false: 7326 incorrect: 36 incorrect true: 13 incorrect false: 23 unknown: 15456 Score: 28044 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/14046421617 ```` Master (30s): ```` Statistics: 33569 Files correct: 18079 correct true: 10747 correct false: 7332 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15450 Score: 27978 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/14016741212 ```` --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update stats-30s.txt Update stats-300s.txt [overflow] check typecast overflow for signed and unsigned int only (#2376) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [overflow] use resolved_type instead Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-300s.txt [Solidity] fix address modelling (#2379) [OM] Refactoring our C++ operational models: functional (#2381) [python-frontend] Model for numpy.ceil (#2382) - Add operational model for [numpy.ceil](https://numpy.org/doc/stable/reference/generated/numpy.ceil.html#numpy.ceil). - Fix handling of negative numbers in lists. --------- Co-authored-by: brcfarias <1334363+brcfarias@users.noreply.github.com> [Z3] Fix overflow detection for signed subtraction and unsigned division and modulus (#2383) Update README.md [overflow] removed unused variable Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-30s.txt [sv-comp] increase context-switch to 3 (#2378) This PR (900s): ```` Statistics: 3179 Files correct: 1814 correct true: 1360 correct false: 454 incorrect: 40 incorrect true: 23 incorrect false: 17 unknown: 1325 Score: 2166 (max: 5725) https://github.com/esbmc/esbmc/actions/runs/14191126275 ```` Master (900s): ```` Statistics: 3179 Files correct: 1843 correct true: 1409 correct false: 434 incorrect: 61 incorrect true: 43 incorrect false: 18 unknown: 1275 Score: 1588 (max: 5725) https://github.com/esbmc/esbmc/actions/runs/14191018069 ```` --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [Concurrency] unified data race flag (#2385) This PR (900s): ``` Statistics: 1029 Files correct: 530 correct true: 415 correct false: 115 incorrect: 21 incorrect true: 14 incorrect false: 7 unknown: 478 Score: 385 (max: 1823) https://github.com/esbmc/esbmc/actions/runs/14193032102 ``` Master (900s): ``` Statistics: 1029 Files correct: 565 correct true: 449 correct false: 116 incorrect: 24 incorrect true: 18 incorrect false: 6 unknown: 440 Score: 342 (max: 1823) https://github.com/esbmc/esbmc/actions/runs/14193024857 ``` Update ExternalDependencies.cmake (#2390) This should fix the old dependencies which where asking for minimum cmake of < 3.5 --------- Co-authored-by: XLiZHI <958689657@qq.com> Update stats-30s.txt Update stats-300s.txt Update stats-600s.txt [Cov & Sol] Coverage support for Solidity (#2389) [Solidity] Upgrade the AST merging algorithm for multiple files (#2392) [Coverage] fix the covergae algorithm (#2365) [python-frontend] Reuse C libm models for NumPy math functions (#2395) [solidity] create unique temp file to prevent races (#2396) [Solidity] Support Unit keywords && insufficient balance checks (#2393) [Solidity] function call with options (#2398) Update test.desc [data-races-check] get rid of static analysis (#2399) [Solidity] Fix function order bug in AST merge (#2400) [solidity] fix regression (#2402) Fix windows build (#2403) [build] update ESBMC version Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update Release Notes for ESBMC v7.9 (#2404) [python] Fix unary negation (#2406) Update stats-30s.txt [Solidity] add support for several keywords and update modelling algorithm (#2405) [python] Expand numpy math models (#2407) Reusing C models for floor, fabs, sin and exp. [goto-programs] ESBMC Overflow Intrinsic Support (#2408) Fixes rafaelsamenezes/goto-transcoder#2. This PR implements intrinsic functions in ESBMC that perform arithmetic operations with overflow detection. These intrinsics are designed to return both the result of the operation and a flag indicating whether overflow occurred, similar to `__builtin_*_overflow` in GCC/Clang. --- | Intrinsic | Operation | Description | |-----------|-----------|-------------| | `__ESBMC_overflow_result_plus(a, b)` | `a + b` | Addition with overflow check | | `__ESBMC_overflow_result_minus(a, b)` | `a - b` | Subtraction with overflow check | | `__ESBMC_overflow_result_mult(a, b)` | `a * b` | Multiplication with overflow check | | `__ESBMC_overflow_result_shl(a, b)` | `a << b` | Shift-left with overflow check | | `__ESBMC_overflow_result_unary_minus(a)` | `-a` | Unary negation with overflow check | --- Each intrinsic returns a structure: ```c struct __ESBMC_overflow_result { bool overflow; T result; }; --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update stats-300s.txt Update stats-30s.txt [C++ verification] fix std::find function (#2410) [Solidity] Bug fix (#2409) Update README.md [goto-programs] refactored do_function_call_symbol (#2411) [regression] added test case for casting Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for casting Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] enabled test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] disabled test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update CREDITS Update CREDITS [python-frontend] Handling list slicing (#2414) [python] check for float and str comparisons Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Apply automatic changes [python] improved report about the TypeError location Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Apply automatic changes [regression] added test case for casting Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for casting Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] fixed regular expression Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] fixed regular expression Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [Python] add chr() built-in function support (#2416) This PR introduces support for Python’s built-in chr() function in the ESBMC Python frontend. The chr() function takes an integer and returns a one-character string corresponding to the ASCII code of that integer. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] fixed range check Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] refactor our python frontend and extend chr() and float() built-in functions (#2417) This PR enhances the ESBMC Python frontend by improving support for built-in type-casting functions, particularly `chr()` and `float()`, and refining type handling across expressions. It introduces better error detection, stricter type enforcement, and new regression tests to validate behavior. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Fix default variable implementation (#2418) [python] Add support for hex() built-in function (#2419) [python] Handle string comparison for != operator (#2420) [python] add support for python's oct() built-in function (#2421) This PR extends ESBMC’s Python frontend to support the built-in `oct()` function, which converts integers to their octal string representation (e.g., oct(8) → "0o10", oct(-9) → "-0o11"). It adds implementation and regression tests to ensure correct behavior for successful and failing cases. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [util] removed header Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md Update README.md Update README.md [python] Handle ord(): convert single-character string to integer Unicode code point (#2423) This PR implements the `ord()` built-in function as described in the Python documentation (https://docs.python.org/3/library/functions.html#ord): _"Given a string representing one Unicode character, return an integer representing the Unicode code point of that character. For example, ord('a') returns the integer 97 and ord('€') (Euro sign) returns 8364. This is the inverse of [chr()](https://docs.python.org/3/library/functions.html#chr)."_ --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [C++ verification] update operational models (#2424) [python] Support python true division semantics (/) with float type coercion (#2425) This PR supports the Python frontend for correctly handling Python’s true division operator (/) in mixed-type arithmetic, particularly when the result is assigned to a float-annotated variable. It ensures that integer operands are type-coerced to floatbv (IEEE floating-point type) when necessary. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] Improved inference to handle true division (/) operator (#2426) [python] add support for str(float) conversion (#2427) [python] support for int() and float() conversion for symbols (#2429) This PR enhances our Python frontend by supporting Python-style int() and float() conversions on symbolic variables holding string values. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [cmake] enable precompile headers for gcc (#2428) [symex] Support for CPROVER R_OK (#2431) Fixes #2430 (comment). This PR introduces the `__ESBMC_r_ok` intrinsic to ESBMC's symbolic execution engine. This function enables users to verify that a memory read of a specified length from a given address stays within the bounds of the allocated object, improving ESBMC’s ability to check low-level memory safety. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [CI] add static CHERI llvm17 build (#2432) [regression] added test case for division Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] fixed log warning Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] added test case for true division Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> update test.desc (#2433) [python] Refactor get_binary_operator_expr (#2434) [python] fixed log_warning Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] extended numpy test case for math Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] extended numpy test case for fabs Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for numpy.fabs() (#2435) This PR implements support for `numpy.fabs()` function using a native `fabs` implementation in `libm`. It also improves error handling and diagnostics for unsupported NumPy calls in the Python frontend. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [CI] update llvm-16 for windows (#2436) [python] added test cases for numpy math functions (#2437) [regression] enabled test case for exp numpy function Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for Euler constant Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] enabled test case for exp numpy function Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [libm] fix acos function (#2442) fix #2439  https://en.wikipedia.org/wiki/Inverse_trigonometric_functions Update README.md Update README.md [solidity] fix reentry attack checks (#2422) This PR - fix reentry checks algo - fix inheritance - fix contract address assignment --------- Co-authored-by: hejueyun2 <hejueyun@gmail.com> Update stats-30s.txt [python] add support and error checking for Python abs() builtin function (#2441) This PR evaluates the abs() builtin for constant and symbolic numeric types. It also rejects invalid types (e.g., str, list, etc.) with appropriate TypeError messages. Lastly,, it adds test cases to validate valid and invalid uses of abs(). --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update README.md [regression] add test cases for divison by zero function Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md [numpy] Add support for numpy.arccos() and some fixes (#2444) Update README.md [numpy] enhance numpy math function verification coverage (#2445) This PR expands the regression test suite for various NumPy mathematical functions, improves verification accuracy, and addresses known edge cases. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update README.md [regression] added test case for function call Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for function call Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Fix bounds computation for multi-dimensional arrays (#2446) Fixes #2440 Update stats-300s.txt Update README.md Update README.md Update stats-30s.txt Update README.md [regression] added test case for ethereum bug Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [numpy] added integer_squareroot test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [numpy] added integer_squareroot test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [OM] Fix warning messages for pthread and setjmp models (#2448) [OM] removed unnecessary typecast Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md Update README.md Update README.md Update README.md [Solidity] Add support for the library entity (#2394) The purpose of this pull request is to add support for the "library" in Solidity. Update stats-30s.txt [concurrency] : add support for pthread_cleanup_push and pthread_cleanup_pop (#2450) [regression] added test cases for pthread cleanup Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] Set location for the conditional statement (#2453) Fixes #2452. Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update BUILDING.md (#2454) Update some build instructions [pthread] push/pop must match Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-30s.txt [pthread] improved comment for assertion Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added more test cases for chained comparisons Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [Python] Extend support for compound assignment statements (#2458) This PR extends our Python frontend to parse, type check, and translate compound assignment statements (e.g., x += 1, y /= 2) into GOTO code. It includes frontend code changes and regression test cases to ensure correctness and detect corner-case failures such as division by zero and improper type propagation. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] Handling NumPy dot product (#2460) This PR adds C model infrastructure to compute [dot product](https://numpy.org/doc/stable/reference/generated/numpy.dot.html#numpy.dot) of arrays. --------- Co-authored-by: brcfarias <1334363+brcfarias@users.noreply.github.com> [python] build symbolic multiplication tree for power/pow functions (#2462) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] improved comment for handle_power_operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases in Python for while Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases in Python for function call Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases in Python for function call Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] Handle function calls used as arguments (#2465) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] Improve abs() handling (#2466) This PR enhances the Python frontend's `abs()` function handling to detect and reject non-numeric arguments correctly, and to better infer operand types. It addresses two previously undetected or misclassified errors and adds supporting regression tests. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python-frontend] Handling array literals (#2467) [regression] added test for function call + class Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for pass in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] Allow variables in NumPy math function calls (#2469) [regression] added test cases for ceil in numpy Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update numpy.py Update stats-300s.txt [regression] added test cases for logican and in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for mod in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for range in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [SMT solver] Updated Bitwuzla from v0.7.0 to v0.8.0 (#2472) [python] improve range() handling (#2473) [Solidity] Refactoring Mapping (#2468) [python] Handling numpy functions (#2474) [regression] added test cases for power in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [symex] removed temporary fix for the condition coverage (#2477) [python] improved support for power operator (**) (#2478) Disabled broken solvers for benchexec CI (#2481) Yices and Bitwuzla are not building on benchexec CI runs. The crashes seems to be related to GMP. Lets avoid it for now and enable again when it is working. [C verification] Adjust the behavior of parameter checking for the unknown method (#2479) Update README.md [CHERI] support the verification of CHERI capability bounds (#2464) [python] add support for unary+ operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for unary+ operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for unary+ operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [build] fix solvers gmp library link (#2483) We have multiple solvers that depend on the gmp library at the same time, perhaps putting the gmp lib link at the top level is better. https://github.com/esbmc/esbmc/actions/runs/15322131655/job/43108043486 --------- Co-authored-by: Lucas C. Cordeiro <lucasccordeiro@gmail.com> Update stats-30s.txt [python] add support for bytes literals and indexing (#2484) Revert "[build] fix solvers gmp library link" (#2485) Reverts #2483 Revert "Revert "[build] fix solvers gmp library link"" (#2486) Reverts #2485 [python] Add numpy.matmul (#2487) Handling [numpy.matmul](https://numpy.org/doc/stable/reference/generated/numpy.matmul.html) calls. [python] added tests for numpy det Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] added test cases for numpy dot Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] added test cases for numpy transpose Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for Is and IsNot operators (#2480) Update stats-300s.txt [python] add support for numpy.dot() with 1D and mixed-dimension arrays (#2489) This PR extends our Python frontend to support additional `numpy.dot()` operand combinations, enabling verification of vector and matrix dot products across a wider range of dimensions. - 1D × 1D → scalar - 1D × 2D → 1D array - 2D × 1D → 1D array - 2D × 2D → 2D array (already supported) --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] simplified is operator (#2490) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md [python] added test case for None Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] support for "NoneType" (#2493) This PR introduces support for "NoneType" in the type system, represented by a pointer to void. The Python None value is now internally represented as a null pointer (constant_exprt with pointer_type and value "0"). Enhanced AST type inference to detect various forms of None across Python versions (e.g., Constant, NameConstant, and Name). --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [numpy] disallow 3D or higher-dimensional arrays (#2492) Fixes #2491. This PR introduces validation in the Python frontend to reject 3D or higher-dimensional arrays. It includes a new regression test (dot8) to verify that ESBMC correctly throws an error when such input is provided. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] improved return type inference (#2494) This PR enhances our Python frontend’s ability to infer function return types in ESBMC by improving logic in `python_annotation::get_function_return_type`. It adds support for parsing and handling annotated and inferred return types from Python AST nodes. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Co-authored-by: Bruno Farias <brunocarvalhofarias@gmail.com> [regression] Show warning when KNOWNBUG tests stop failing (#2496) **Before:**  **Now:**  CPROVER migration compatibility (#2443) In this PR I am introducing ireps that were originated from CBMC into the migration. However, I am focusing on implementing them as intrinsic function calls. As we can then test the behavior using C files. This is still a draft as it requires: - [x] ~There is a bug in the transcoder that is making the pop_frame assertion break.~ Applying same hack as coverage. - [X] ~Overflow-result needs to invoke our intrinsic function.~ Can't apply late goto transformations. - [X] ~r_ok intrinsic. ~ Will fix in another PR - [X] .goto testcases need to be constructed from CBMC and then adapted to ESBMC format (using goto-transcoder). - [x] ~Export header of ESBMC. This is a C file including all the intrinsic function signatures, this is meant to be exported as a .goto file.~ Testing utilities will be ported to utils (#2476). --------- Co-authored-by: Rafael Sá Menezes <rafael.sa.menezes40@gmail.com> Co-authored-by: rafaelsamenezes <8601807+rafaelsamenezes@users.noreply.github.com> [built-in] model builtin clzll using constraints (#2501) This is a PR of an attempt to model a builtin function with assumptions The algorithm is as follows: ``` 1. nondet symbol clz_sym（uint64） 2. assert(x != 0) 3. assume(0 ≤ clz_sym ≤ 63) 4. idx = 63 - clz_sym 5. assume(((x >> idx) & 1) != 0) 6. assume((x >> (idx+1)) == 0) 7. return (int)clz_sym ``` [python] enhanced string comparison handling (#2497) This PR introduces a significant enhancement to the Python frontend's handling of string comparisons, specifically improving the accuracy and robustness of equality checks involving string-returning functions. It adds new logic for constant resolution and identity function detection and expands regression test coverage with various string manipulation scenarios. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [smt] don't access vector out of bounds (#2502) `reserve` only changes the capacity, but not the size. After `args.reserve(20)`, `args[10]` would still fail. The loop that initialized all `args` has been changed to use push_back instead of indices. The few cases that later tried to write to e.g. `args[0]` where there was previously no value written to `args[0]` have been changed to now do the write. Alternative to #2498 Co-authored-by: intrigus <abc123zeus@live.de> [python] Handle string annotations like -> int (#2495) Update stats-30s.txt [goto-programs] add validation for invalid member accesses on incomplete or incorrectly typed expressions (Fixes #2236) (#2500) [python] check for sideeffect in is_zero_length_array Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] avoid string comparison with sideeffects Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] added test cases for ternary operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-30s.txt [regression] added test case for overflow/nan Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md Update README.md Update README.md [CHERI] hide compressed/decompressed trace (#2504) The counterexample becomes cleaner [python] enhanced handling of true division (#2505) This PR introduces several enhancements to the ESBMC Python frontend (`python_converter.cpp`) to more accurately model Python semantics for true division (/). --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update README.md [python] implement pow symbolically (#2506) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [regression] removed --incremental-bmc Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-600s.txt [python] add support for python built-in function handling (#2507) [regression] added test case from #1599 Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case from #1599 Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] removed test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for transforming general python for loops over iterables (#2508) [regression] added test case for Python class Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] improved test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] Fix compound assignment on object attributes (#2509) [python] added test case for assert stmt Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for class Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] handles assertions involving function calls and refactor attribute handling (#2510) [python] added test case for class Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for realloc [CI] Integrate cheribsd-riscv64 system root (#2447) The build on GitHub runner using cheribuild took too long and exceeded the runner's hard disk capacity. Currently I have uploaded the cheribsd SDK built locally and hope it works as expected. ;) [regression] added test case for realloc [c++] added test case for vector Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [cpp] resolve mismatch template deduction errors with pointer types (#2517) [cpp] add support for std::is_sorted and improve vector initialization (#2515) [c++] implement missing ostreambuf_iterator methods for STL algorithm support (#2519) [cpp] Fix vector const_reverse_iterator implementation for reverse iteration support (#2520) Implement the `const_reverse_iterator` class with conversion constructors and operators derived from `reverse_iterator`. Add missing `const rbegin()/rend()` method implementations. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] fix map::insert() to accept temporary pair objects (#2521) This PR changes `map::insert(value_type &val)` to `map::insert(const value_type &val)` to allow binding to rvalue references. This fixes compilation errors when inserting temporary pair objects such as `mymap.insert(pair<char,int>('a', 100));`. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] fix multiset constructor ambiguity (#2522) [c++] fix deque iterator increment operators binding to temporary (#2523) [c++] fix npos handling (#2525) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] fix iterator assignment operators (#2526) [goto-symex] use size directly (#2516) [c++] add explicit int overload for list::insert and replace invalid null check in remove_if (#2527) [c++] fix STL operator overload resolution errors in ostream, sstream and string headers (#2528) [c++] add basic unordered_set support (#2529) [solidity] improve overall performance (#2511) ```sh Over 5 mins esbmc --sol example.sol example.solast --incremental-bmc --no-standard-checks 1.90s user 0.19s system 64% cpu 3.255 total Over 5 mins esbmc --sol example.sol example.solast --contract Reproduction 4.13s user 0.20s system 80% cpu 5.384 total ```  now the whole regression test can be finished in 120 second (-j 8) --- This PR also contains some bug fixing, including library API (_max/_min), address binding in trusted mode --------- Co-authored-by: hejueyun2 <hejueyun@gmail.com> [c++] added basic std::unordered_map support (#2530) This PR introduces initial support for `std::unordered_map` in our C++ model, along with corresponding regression tests to validate its correctness and error detection capabilities. The support includes a simplified internal implementation suitable for bounded model checking, and test cases to ensure expected behavior. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] removed esbmc_forward_iterator_tag Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for Python range Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Consider the guard when dealing with sideeffects (#2514) This is one of the known problems: 1. The current guard needs to be taken into account when dealing with memory allocation, especially in if expressions. 2. There is something wrong with our realloc operation that causes out of bound. This is because we only adjust the bound in the track new pointer, while nothing changes in the dynamic object. I tried to modify the symbol directly, but at the SMT level there was a bit width mismatch. Should we rethink the implementation of realloc, perhaps malloc and memcpy would be a good approach instead? [c++] added test case for vector Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [C++ verification] Add a new implementation of typeid (#2534) The type of polymorphism needs to be fetched at runtime, which is not handled by the frontend, so for now we skip it for preliminary support. The TC in this PR reflects all currently supported methods. [c++] fix vector default constructor: remove explicit keyword (#2535) [regression] reduced verification time for insert2_fail Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] reduced verification time for emplace_fail Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for vector Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] add allocator template parameter to std::vector (#2536) Update main.cpp [c++] applied coding style to vector Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] add deterministic hash specializations for std::hash (#2538) [python] added test case for range Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Address incosistent behaviour in dump_smt function across solvers (#2524) Updated the z3_convt::output_smt() and the bitwulza_convt::dump_smt() functions to print to stdout when no output was defined Improved the handling of empty and "-" output paths in the smtlib_conv::dump_smt() function Addressed issue #2167 --------- Signed-off-by: mihaistate05 <mihaita.state@yahoo.com> Signed-off-by: mihaistate <mihai.state03@yahoo.com> Signed-off-by: mihaistate05 <mihai.state03@yahoo.com> Co-authored-by: mihaistate05 <mihaita.state@yahoo.com> [CI] improve auto commit (#2540) Improve the code style check CI: Only branches in the ESBMC repository will trigger the auto commit, because git commit does not have permission to modify other repositories. Otherwise, we show the corresponding code, throw an error. Update stats-300s.txt Update stats-30s.txt
mihaistate
added a commit
that referenced
this pull request
Jun 27, 2025
Created a new memcpy function that copies 8 bytes per iteration The if statement checks that both dst and src pointers are 8-byte aligned. If they are, it copies 8 bytes of memory using uint64_t pointers for efficiency. Remaining bytes are handled in a trailing byte loop. If the pointers are not 8-bytes aligned, the function falls back to a safe byte-by-byte copy. Signed-off-by: mihaistate05 <mihai.state03@yahoo.com> [TC] add variant of github_60 test (#2362) Make TC from #1175 compatible with windows (#2361) [TC] add TC from #1290 (#2359) Update README.md Update README.md [Z3] Support bitwise for integer arithmetic (#2354) This PR refactors our bitwise operations handling and enhances our SMT conversion functions to better support integer and boolean types. In particular, it introduces more consistent handling for boolean and integer types and improves compatibility with the Z3 solver's bit-vector operations. - [X] bitnot_id - [X] bitxor_id - [x] bitand_id - [x] bitor_id - [x] bitnand_id - [x] bitnor_id - [x] bitnxor_id This PR (30s): ```` Statistics: 33569 Files correct: 18073 correct true: 10743 correct false: 7330 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15456 Score: 27968 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/13956944037 ```` Master (30s): ```` Statistics: 33569 Files correct: 18075 correct true: 10743 correct false: 7332 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15454 Score: 27970 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/13906715936 ```` --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update README.md Update README.md [C verification] remove nonexistent function (#2358) Fixes #2355. nand() doesn't actually exist in the standard C library; the <math.h> header only defines nan(), nanf(), and nanl(). We introduced a new function : -) Update README.md Update stats-600s.txt [cmake] update MathSAT download link (#2370) The master version fails as: ```` Downloading Mathsat -- Downloading MATHSAT from https://mathsat.fbk.eu/download.php?file=mathsat-5.6.10-linux-x86_64.tar.gz -- Extracting MATHSAT CMake Error at src/solvers/mathsat/CMakeLists.txt:20 (message): Could not find mathsat include headers, please check Mathsat_DIR ```` This PR adds the new download link MathSAT: for https://mathsat.fbk.eu/release/mathsat-5.6.11-linux-x86_64.tar.gz. Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md [Overflow] Added overflow_cast to support integer overflow detection (#2367) Fixes #2357. This PR extends the `overflow_cast` method in ESBMC to handle integer arithmetic typecast overflow detection. Key Changes: - Checks for signed and unsigned typecast overflow in integer arithmetic. - Handles cases where values exceed the target type’s range This PR (30s): ```` Statistics: 33569 Files correct: 18079 correct true: 10747 correct false: 7332 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15450 Score: 27978 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/14016741212 ```` Master (30s): ```` Statistics: 33569 Files correct: 18075 correct true: 10743 correct false: 7332 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15454 Score: 27970 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/13906715936 ```` --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update stats-30s.txt [memory-leak] Track global memory (#2372) This PR fixes #2335. Here, 'g' acts as a guard condition, determining whether 'e' should be considered. 'same_object2tc(obj, e)' checks if 'obj' and 'e' refer to the same object; if 'g' is an AND condition (is_and2t) or already a same-object check (is_same_object2t), then 'g' is combined; otherwise, we directly use 'same_object2tc(obj, e).' This PR (30s): ```` Statistics: 33569 Files correct: 18077 correct true: 10751 correct false: 7326 incorrect: 36 incorrect true: 13 incorrect false: 23 unknown: 15456 Score: 28044 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/14046421617 ```` Master (30s): ```` Statistics: 33569 Files correct: 18079 correct true: 10747 correct false: 7332 incorrect: 40 incorrect true: 13 incorrect false: 27 unknown: 15450 Score: 27978 (max: 55885) https://github.com/esbmc/esbmc/actions/runs/14016741212 ```` --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update stats-30s.txt Update stats-300s.txt [overflow] check typecast overflow for signed and unsigned int only (#2376) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [overflow] use resolved_type instead Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-300s.txt [Solidity] fix address modelling (#2379) [OM] Refactoring our C++ operational models: functional (#2381) [python-frontend] Model for numpy.ceil (#2382) - Add operational model for [numpy.ceil](https://numpy.org/doc/stable/reference/generated/numpy.ceil.html#numpy.ceil). - Fix handling of negative numbers in lists. --------- Co-authored-by: brcfarias <1334363+brcfarias@users.noreply.github.com> [Z3] Fix overflow detection for signed subtraction and unsigned division and modulus (#2383) Update README.md [overflow] removed unused variable Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-30s.txt [sv-comp] increase context-switch to 3 (#2378) This PR (900s): ```` Statistics: 3179 Files correct: 1814 correct true: 1360 correct false: 454 incorrect: 40 incorrect true: 23 incorrect false: 17 unknown: 1325 Score: 2166 (max: 5725) https://github.com/esbmc/esbmc/actions/runs/14191126275 ```` Master (900s): ```` Statistics: 3179 Files correct: 1843 correct true: 1409 correct false: 434 incorrect: 61 incorrect true: 43 incorrect false: 18 unknown: 1275 Score: 1588 (max: 5725) https://github.com/esbmc/esbmc/actions/runs/14191018069 ```` --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [Concurrency] unified data race flag (#2385) This PR (900s): ``` Statistics: 1029 Files correct: 530 correct true: 415 correct false: 115 incorrect: 21 incorrect true: 14 incorrect false: 7 unknown: 478 Score: 385 (max: 1823) https://github.com/esbmc/esbmc/actions/runs/14193032102 ``` Master (900s): ``` Statistics: 1029 Files correct: 565 correct true: 449 correct false: 116 incorrect: 24 incorrect true: 18 incorrect false: 6 unknown: 440 Score: 342 (max: 1823) https://github.com/esbmc/esbmc/actions/runs/14193024857 ``` Update ExternalDependencies.cmake (#2390) This should fix the old dependencies which where asking for minimum cmake of < 3.5 --------- Co-authored-by: XLiZHI <958689657@qq.com> Update stats-30s.txt Update stats-300s.txt Update stats-600s.txt [Cov & Sol] Coverage support for Solidity (#2389) [Solidity] Upgrade the AST merging algorithm for multiple files (#2392) [Coverage] fix the covergae algorithm (#2365) [python-frontend] Reuse C libm models for NumPy math functions (#2395) [solidity] create unique temp file to prevent races (#2396) [Solidity] Support Unit keywords && insufficient balance checks (#2393) [Solidity] function call with options (#2398) Update test.desc [data-races-check] get rid of static analysis (#2399) [Solidity] Fix function order bug in AST merge (#2400) [solidity] fix regression (#2402) Fix windows build (#2403) [build] update ESBMC version Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update Release Notes for ESBMC v7.9 (#2404) [python] Fix unary negation (#2406) Update stats-30s.txt [Solidity] add support for several keywords and update modelling algorithm (#2405) [python] Expand numpy math models (#2407) Reusing C models for floor, fabs, sin and exp. [goto-programs] ESBMC Overflow Intrinsic Support (#2408) Fixes rafaelsamenezes/goto-transcoder#2. This PR implements intrinsic functions in ESBMC that perform arithmetic operations with overflow detection. These intrinsics are designed to return both the result of the operation and a flag indicating whether overflow occurred, similar to `__builtin_*_overflow` in GCC/Clang. --- | Intrinsic | Operation | Description | |-----------|-----------|-------------| | `__ESBMC_overflow_result_plus(a, b)` | `a + b` | Addition with overflow check | | `__ESBMC_overflow_result_minus(a, b)` | `a - b` | Subtraction with overflow check | | `__ESBMC_overflow_result_mult(a, b)` | `a * b` | Multiplication with overflow check | | `__ESBMC_overflow_result_shl(a, b)` | `a << b` | Shift-left with overflow check | | `__ESBMC_overflow_result_unary_minus(a)` | `-a` | Unary negation with overflow check | --- Each intrinsic returns a structure: ```c struct __ESBMC_overflow_result { bool overflow; T result; }; --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update stats-300s.txt Update stats-30s.txt [C++ verification] fix std::find function (#2410) [Solidity] Bug fix (#2409) Update README.md [goto-programs] refactored do_function_call_symbol (#2411) [regression] added test case for casting Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for casting Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] enabled test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] disabled test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update CREDITS Update CREDITS [python-frontend] Handling list slicing (#2414) [python] check for float and str comparisons Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Apply automatic changes [python] improved report about the TypeError location Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Apply automatic changes [regression] added test case for casting Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for casting Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] fixed regular expression Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] fixed regular expression Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [Python] add chr() built-in function support (#2416) This PR introduces support for Python’s built-in chr() function in the ESBMC Python frontend. The chr() function takes an integer and returns a one-character string corresponding to the ASCII code of that integer. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] fixed range check Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] refactor our python frontend and extend chr() and float() built-in functions (#2417) This PR enhances the ESBMC Python frontend by improving support for built-in type-casting functions, particularly `chr()` and `float()`, and refining type handling across expressions. It introduces better error detection, stricter type enforcement, and new regression tests to validate behavior. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Fix default variable implementation (#2418) [python] Add support for hex() built-in function (#2419) [python] Handle string comparison for != operator (#2420) [python] add support for python's oct() built-in function (#2421) This PR extends ESBMC’s Python frontend to support the built-in `oct()` function, which converts integers to their octal string representation (e.g., oct(8) → "0o10", oct(-9) → "-0o11"). It adds implementation and regression tests to ensure correct behavior for successful and failing cases. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [util] removed header Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md Update README.md Update README.md [python] Handle ord(): convert single-character string to integer Unicode code point (#2423) This PR implements the `ord()` built-in function as described in the Python documentation (https://docs.python.org/3/library/functions.html#ord): _"Given a string representing one Unicode character, return an integer representing the Unicode code point of that character. For example, ord('a') returns the integer 97 and ord('€') (Euro sign) returns 8364. This is the inverse of [chr()](https://docs.python.org/3/library/functions.html#chr)."_ --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [C++ verification] update operational models (#2424) [python] Support python true division semantics (/) with float type coercion (#2425) This PR supports the Python frontend for correctly handling Python’s true division operator (/) in mixed-type arithmetic, particularly when the result is assigned to a float-annotated variable. It ensures that integer operands are type-coerced to floatbv (IEEE floating-point type) when necessary. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] Improved inference to handle true division (/) operator (#2426) [python] add support for str(float) conversion (#2427) [python] support for int() and float() conversion for symbols (#2429) This PR enhances our Python frontend by supporting Python-style int() and float() conversions on symbolic variables holding string values. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [cmake] enable precompile headers for gcc (#2428) [symex] Support for CPROVER R_OK (#2431) Fixes #2430 (comment). This PR introduces the `__ESBMC_r_ok` intrinsic to ESBMC's symbolic execution engine. This function enables users to verify that a memory read of a specified length from a given address stays within the bounds of the allocated object, improving ESBMC’s ability to check low-level memory safety. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [CI] add static CHERI llvm17 build (#2432) [regression] added test case for division Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] fixed log warning Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] added test case for true division Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> update test.desc (#2433) [python] Refactor get_binary_operator_expr (#2434) [python] fixed log_warning Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] extended numpy test case for math Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] extended numpy test case for fabs Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for numpy.fabs() (#2435) This PR implements support for `numpy.fabs()` function using a native `fabs` implementation in `libm`. It also improves error handling and diagnostics for unsupported NumPy calls in the Python frontend. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [CI] update llvm-16 for windows (#2436) [python] added test cases for numpy math functions (#2437) [regression] enabled test case for exp numpy function Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for Euler constant Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] enabled test case for exp numpy function Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [libm] fix acos function (#2442) fix #2439  https://en.wikipedia.org/wiki/Inverse_trigonometric_functions Update README.md Update README.md [solidity] fix reentry attack checks (#2422) This PR - fix reentry checks algo - fix inheritance - fix contract address assignment --------- Co-authored-by: hejueyun2 <hejueyun@gmail.com> Update stats-30s.txt [python] add support and error checking for Python abs() builtin function (#2441) This PR evaluates the abs() builtin for constant and symbolic numeric types. It also rejects invalid types (e.g., str, list, etc.) with appropriate TypeError messages. Lastly,, it adds test cases to validate valid and invalid uses of abs(). --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update README.md [regression] add test cases for divison by zero function Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md [numpy] Add support for numpy.arccos() and some fixes (#2444) Update README.md [numpy] enhance numpy math function verification coverage (#2445) This PR expands the regression test suite for various NumPy mathematical functions, improves verification accuracy, and addresses known edge cases. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update README.md [regression] added test case for function call Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for function call Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Fix bounds computation for multi-dimensional arrays (#2446) Fixes #2440 Update stats-300s.txt Update README.md Update README.md Update stats-30s.txt Update README.md [regression] added test case for ethereum bug Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [numpy] added integer_squareroot test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [numpy] added integer_squareroot test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [OM] Fix warning messages for pthread and setjmp models (#2448) [OM] removed unnecessary typecast Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md Update README.md Update README.md Update README.md [Solidity] Add support for the library entity (#2394) The purpose of this pull request is to add support for the "library" in Solidity. Update stats-30s.txt [concurrency] : add support for pthread_cleanup_push and pthread_cleanup_pop (#2450) [regression] added test cases for pthread cleanup Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] Set location for the conditional statement (#2453) Fixes #2452. Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update BUILDING.md (#2454) Update some build instructions [pthread] push/pop must match Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-30s.txt [pthread] improved comment for assertion Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added more test cases for chained comparisons Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [Python] Extend support for compound assignment statements (#2458) This PR extends our Python frontend to parse, type check, and translate compound assignment statements (e.g., x += 1, y /= 2) into GOTO code. It includes frontend code changes and regression test cases to ensure correctness and detect corner-case failures such as division by zero and improper type propagation. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] Handling NumPy dot product (#2460) This PR adds C model infrastructure to compute [dot product](https://numpy.org/doc/stable/reference/generated/numpy.dot.html#numpy.dot) of arrays. --------- Co-authored-by: brcfarias <1334363+brcfarias@users.noreply.github.com> [python] build symbolic multiplication tree for power/pow functions (#2462) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] improved comment for handle_power_operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases in Python for while Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases in Python for function call Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases in Python for function call Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] Handle function calls used as arguments (#2465) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] Improve abs() handling (#2466) This PR enhances the Python frontend's `abs()` function handling to detect and reject non-numeric arguments correctly, and to better infer operand types. It addresses two previously undetected or misclassified errors and adds supporting regression tests. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python-frontend] Handling array literals (#2467) [regression] added test for function call + class Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for pass in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] Allow variables in NumPy math function calls (#2469) [regression] added test cases for ceil in numpy Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update numpy.py Update stats-300s.txt [regression] added test cases for logican and in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for mod in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for range in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [SMT solver] Updated Bitwuzla from v0.7.0 to v0.8.0 (#2472) [python] improve range() handling (#2473) [Solidity] Refactoring Mapping (#2468) [python] Handling numpy functions (#2474) [regression] added test cases for power in Python Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [symex] removed temporary fix for the condition coverage (#2477) [python] improved support for power operator (**) (#2478) Disabled broken solvers for benchexec CI (#2481) Yices and Bitwuzla are not building on benchexec CI runs. The crashes seems to be related to GMP. Lets avoid it for now and enable again when it is working. [C verification] Adjust the behavior of parameter checking for the unknown method (#2479) Update README.md [CHERI] support the verification of CHERI capability bounds (#2464) [python] add support for unary+ operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for unary+ operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for unary+ operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [build] fix solvers gmp library link (#2483) We have multiple solvers that depend on the gmp library at the same time, perhaps putting the gmp lib link at the top level is better. https://github.com/esbmc/esbmc/actions/runs/15322131655/job/43108043486 --------- Co-authored-by: Lucas C. Cordeiro <lucasccordeiro@gmail.com> Update stats-30s.txt [python] add support for bytes literals and indexing (#2484) Revert "[build] fix solvers gmp library link" (#2485) Reverts #2483 Revert "Revert "[build] fix solvers gmp library link"" (#2486) Reverts #2485 [python] Add numpy.matmul (#2487) Handling [numpy.matmul](https://numpy.org/doc/stable/reference/generated/numpy.matmul.html) calls. [python] added tests for numpy det Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] added test cases for numpy dot Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] added test cases for numpy transpose Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for Is and IsNot operators (#2480) Update stats-300s.txt [python] add support for numpy.dot() with 1D and mixed-dimension arrays (#2489) This PR extends our Python frontend to support additional `numpy.dot()` operand combinations, enabling verification of vector and matrix dot products across a wider range of dimensions. - 1D × 1D → scalar - 1D × 2D → 1D array - 2D × 1D → 1D array - 2D × 2D → 2D array (already supported) --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] simplified is operator (#2490) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md [python] added test case for None Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] support for "NoneType" (#2493) This PR introduces support for "NoneType" in the type system, represented by a pointer to void. The Python None value is now internally represented as a null pointer (constant_exprt with pointer_type and value "0"). Enhanced AST type inference to detect various forms of None across Python versions (e.g., Constant, NameConstant, and Name). --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [numpy] disallow 3D or higher-dimensional arrays (#2492) Fixes #2491. This PR introduces validation in the Python frontend to reject 3D or higher-dimensional arrays. It includes a new regression test (dot8) to verify that ESBMC correctly throws an error when such input is provided. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [python] improved return type inference (#2494) This PR enhances our Python frontend’s ability to infer function return types in ESBMC by improving logic in `python_annotation::get_function_return_type`. It adds support for parsing and handling annotated and inferred return types from Python AST nodes. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Co-authored-by: Bruno Farias <brunocarvalhofarias@gmail.com> [regression] Show warning when KNOWNBUG tests stop failing (#2496) **Before:**  **Now:**  CPROVER migration compatibility (#2443) In this PR I am introducing ireps that were originated from CBMC into the migration. However, I am focusing on implementing them as intrinsic function calls. As we can then test the behavior using C files. This is still a draft as it requires: - [x] ~There is a bug in the transcoder that is making the pop_frame assertion break.~ Applying same hack as coverage. - [X] ~Overflow-result needs to invoke our intrinsic function.~ Can't apply late goto transformations. - [X] ~r_ok intrinsic. ~ Will fix in another PR - [X] .goto testcases need to be constructed from CBMC and then adapted to ESBMC format (using goto-transcoder). - [x] ~Export header of ESBMC. This is a C file including all the intrinsic function signatures, this is meant to be exported as a .goto file.~ Testing utilities will be ported to utils (#2476). --------- Co-authored-by: Rafael Sá Menezes <rafael.sa.menezes40@gmail.com> Co-authored-by: rafaelsamenezes <8601807+rafaelsamenezes@users.noreply.github.com> [built-in] model builtin clzll using constraints (#2501) This is a PR of an attempt to model a builtin function with assumptions The algorithm is as follows: ``` 1. nondet symbol clz_sym（uint64） 2. assert(x != 0) 3. assume(0 ≤ clz_sym ≤ 63) 4. idx = 63 - clz_sym 5. assume(((x >> idx) & 1) != 0) 6. assume((x >> (idx+1)) == 0) 7. return (int)clz_sym ``` [python] enhanced string comparison handling (#2497) This PR introduces a significant enhancement to the Python frontend's handling of string comparisons, specifically improving the accuracy and robustness of equality checks involving string-returning functions. It adds new logic for constant resolution and identity function detection and expands regression test coverage with various string manipulation scenarios. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [smt] don't access vector out of bounds (#2502) `reserve` only changes the capacity, but not the size. After `args.reserve(20)`, `args[10]` would still fail. The loop that initialized all `args` has been changed to use push_back instead of indices. The few cases that later tried to write to e.g. `args[0]` where there was previously no value written to `args[0]` have been changed to now do the write. Alternative to #2498 Co-authored-by: intrigus <abc123zeus@live.de> [python] Handle string annotations like -> int (#2495) Update stats-30s.txt [goto-programs] add validation for invalid member accesses on incomplete or incorrectly typed expressions (Fixes #2236) (#2500) [python] check for sideeffect in is_zero_length_array Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] avoid string comparison with sideeffects Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] added test cases for ternary operator Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-30s.txt [regression] added test case for overflow/nan Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update README.md Update README.md Update README.md [CHERI] hide compressed/decompressed trace (#2504) The counterexample becomes cleaner [python] enhanced handling of true division (#2505) This PR introduces several enhancements to the ESBMC Python frontend (`python_converter.cpp`) to more accurately model Python semantics for true division (/). --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> Update README.md [python] implement pow symbolically (#2506) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Co-authored-by: lucasccordeiro <3694109+lucasccordeiro@users.noreply.github.com> [regression] removed --incremental-bmc Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Update stats-600s.txt [python] add support for python built-in function handling (#2507) [regression] added test case from #1599 Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case from #1599 Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] removed test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] add support for transforming general python for loops over iterables (#2508) [regression] added test case for Python class Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] improved test case Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] Fix compound assignment on object attributes (#2509) [python] added test case for assert stmt Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for class Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [python] handles assertions involving function calls and refactor attribute handling (#2510) [python] added test case for class Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test case for realloc [CI] Integrate cheribsd-riscv64 system root (#2447) The build on GitHub runner using cheribuild took too long and exceeded the runner's hard disk capacity. Currently I have uploaded the cheribsd SDK built locally and hope it works as expected. ;) [regression] added test case for realloc [c++] added test case for vector Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [cpp] resolve mismatch template deduction errors with pointer types (#2517) [cpp] add support for std::is_sorted and improve vector initialization (#2515) [c++] implement missing ostreambuf_iterator methods for STL algorithm support (#2519) [cpp] Fix vector const_reverse_iterator implementation for reverse iteration support (#2520) Implement the `const_reverse_iterator` class with conversion constructors and operators derived from `reverse_iterator`. Add missing `const rbegin()/rend()` method implementations. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] fix map::insert() to accept temporary pair objects (#2521) This PR changes `map::insert(value_type &val)` to `map::insert(const value_type &val)` to allow binding to rvalue references. This fixes compilation errors when inserting temporary pair objects such as `mymap.insert(pair<char,int>('a', 100));`. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] fix multiset constructor ambiguity (#2522) [c++] fix deque iterator increment operators binding to temporary (#2523) [c++] fix npos handling (#2525) Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] fix iterator assignment operators (#2526) [goto-symex] use size directly (#2516) [c++] add explicit int overload for list::insert and replace invalid null check in remove_if (#2527) [c++] fix STL operator overload resolution errors in ostream, sstream and string headers (#2528) [c++] add basic unordered_set support (#2529) [solidity] improve overall performance (#2511) ```sh Over 5 mins esbmc --sol example.sol example.solast --incremental-bmc --no-standard-checks 1.90s user 0.19s system 64% cpu 3.255 total Over 5 mins esbmc --sol example.sol example.solast --contract Reproduction 4.13s user 0.20s system 80% cpu 5.384 total ```  now the whole regression test can be finished in 120 second (-j 8) --- This PR also contains some bug fixing, including library API (_max/_min), address binding in trusted mode --------- Co-authored-by: hejueyun2 <hejueyun@gmail.com> [c++] added basic std::unordered_map support (#2530) This PR introduces initial support for `std::unordered_map` in our C++ model, along with corresponding regression tests to validate its correctness and error detection capabilities. The support includes a simplified internal implementation suitable for bounded model checking, and test cases to ensure expected behavior. --------- Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] removed esbmc_forward_iterator_tag Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for Python range Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Consider the guard when dealing with sideeffects (#2514) This is one of the known problems: 1. The current guard needs to be taken into account when dealing with memory allocation, especially in if expressions. 2. There is something wrong with our realloc operation that causes out of bound. This is because we only adjust the bound in the track new pointer, while nothing changes in the dynamic object. I tried to modify the symbol directly, but at the SMT level there was a bit width mismatch. Should we rethink the implementation of realloc, perhaps malloc and memcpy would be a good approach instead? [c++] added test case for vector Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [C++ verification] Add a new implementation of typeid (#2534) The type of polymorphism needs to be fetched at runtime, which is not handled by the frontend, so for now we skip it for preliminary support. The TC in this PR reflects all currently supported methods. [c++] fix vector default constructor: remove explicit keyword (#2535) [regression] reduced verification time for insert2_fail Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] reduced verification time for emplace_fail Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [regression] added test cases for vector Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] add allocator template parameter to std::vector (#2536) Update main.cpp [c++] applied coding style to vector Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] add deterministic hash specializations for std::hash (#2538) [python] added test case for range Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> Address incosistent behaviour in dump_smt function across solvers (#2524) Updated the z3_convt::output_smt() and the bitwulza_convt::dump_smt() functions to print to stdout when no output was defined Improved the handling of empty and "-" output paths in the smtlib_conv::dump_smt() function Addressed issue #2167 --------- Signed-off-by: mihaistate05 <mihaita.state@yahoo.com> Signed-off-by: mihaistate <mihai.state03@yahoo.com> Signed-off-by: mihaistate05 <mihai.state03@yahoo.com> Co-authored-by: mihaistate05 <mihaita.state@yahoo.com> [CI] improve auto commit (#2540) Improve the code style check CI: Only branches in the ESBMC repository will trigger the auto commit, because git commit does not have permission to modify other repositories. Otherwise, we show the corresponding code, throw an error. Update stats-300s.txt Update stats-30s.txt [c++] fixed typos in string Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] fix namespace collision in functional header (#2541) This PR replaces unqualified `std::` references with `::std::` to resolve parsing errors where ESBMC incorrectly looks up standard library features in `__shedskin__::std` (https://github.com/shedskin/shedskin/blob/master/shedskin/lib/builtin/hash.hpp) instead of the `global ::std` namespace. ```` ESBMC version 7.9.0 64-bit x86_64 linux Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc Parsing main.cpp In file included from main.cpp:1: In file included from ./builtin.hpp:223: In file included from ./builtin/hash.hpp:5: /tmp/esbmc-cpp-headers-ba1b-0202-35ea/functional:50:50: error: no template named 'forward' in namespace '__shedskin__::std'; did you mean '::std::forward'? explicit callable_wrapper(Callable &&f) : func(std::forward<Callable>(f)) ^~~~~ /../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/move.h:77:5: note: '::std::forward' declared here forward(typename std::remove_reference<_Tp>::type& __t) noexcept ^ In file included from main.cpp:1: In file included from ./builtin.hpp:223: In file included from ./builtin/hash.hpp:5: /tmp/esbmc-cpp-headers-ba1b-0202-35ea/functional:50:50: error: no template named 'forward' in namespace '__shedskin__::std'; did you mean '::std::forward'? explicit callable_wrapper(Callable &&f) : func(std::forward<Callable>(f)) ```` Signed-off-by: Lucas Cordeiro <lucasccordeiro@gmail.com> [c++] added basic bitset operational model (#2543) [python-frontend] Handling string attributes (#2546) - Handle string attributes as char pointers; - Append `'\0'` to char arrays to enable use of `strcmp` for string comparisons. --------- Co-authored-by: brcfarias <1334363+brcfarias@users.noreply.github.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The master version fails as:
This PR adds the new download link MathSAT: for https://mathsat.fbk.eu/release/mathsat-5.6.11-linux-x86_64.tar.gz.