David Trabish
David Trabish
### Summary of the problem Analysis fails in *pure-symbolic* mode. The input program: ``` #include #include #include int y = 3; int main() { read(0, &y, 1); char a[10] =...
1. The _kleaver_ tool fails to parse the attached query. [query.tar.gz](https://github.com/klee/klee/files/7513956/query.tar.gz) 2. Reproduce using: ``` kleaver ``` 3. The output: ``` issue.kq:28:32: error: cannot infer type of number. (Concat w64...
The ExprReplaceVisitor/ExprReplaceVisitor2 visitors ignore array updates (index/value pairs). This means that the outcome of replacement algorithm will be incorrect if the expression to be replaced appears in an array update...
When we merge two states where one state comes from basic block _bb1_ and the other one comes from _bb2_, then it might create issues with PHI instructions such as:...
Is there a way to fast-forward a given symbolic state (for example, executing the next K instructions) in a synchronous way?
When I try to install the package with ``` pip install enum34 pyxlsb2 ``` It fails: ``` Collecting enum34==1.1.10 Downloading enum34-1.1.10-py2-none-any.whl (11 kB) Collecting pyxlsb2==0.0.2 Downloading pyxlsb2-0.0.2.tar.gz (31 kB) ERROR:...
There is a crash in `png_do_write_transformations` which is reachable from the `png_write_png` API. This happens because of an invalid pointer increment (_sp_) in `png_do_strip_channel` without checking the width, for exmaple:...
## Summary: This is a PR for the following issue: https://github.com/klee/klee/issues/1721. The main goal is to add support for symbolic size allocations. Here, a memory object has a (concrete or...
**Problem:** Currently, when the allocation size is symbolic, KLEE concretizes it. This may lead to coverage loss and missed bugs. **Solution:** To address this, we may use the bounded symbolic...
1. Some of the tests related to `ubsan` runtime fail when running: `make check` (or `make systemtests`). It seems that debug information is missing and as a result, the log...