Age | Commit message (Collapse) | Author |
|
Clone some tests to have their 3.7 version. 'call's, 'load's and
'getelementptr's match the new specification in them.
@andreamattavelli: Fixed test cases: BitCastAlias test cases included
modification to alias specifications that require LLVM 3.8
[v2] added comments what was changed and why
[v3] the new tests are without suffix, the old ones have ".leq36".
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Some compilers are picky, so avoid the warning by additional parentheses:
test/VectorInstructions/integer_ops_unsigned_symbolic.c:85:22: warning: & has lower precedence than <; < will be evaluated first [-Wparentheses]
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
If an external function in KLEE is invoked, it might update errno.
Previously, the errno specific variable in a state was only updated
if it was part of the executed instructions.
That opened up a timeframe that increased the likelihood of errno being
overwritten by another method call.
This patch fixes two issues:
* the errno of the KLEE process state is updated before the external
function call allowing to detect changes to it later on
* after the external call, the memory object of errno is directly
updated
with its new value, reducing the likelihood to be overwritten by
another
call
Additional features:
* Add support for `errno()` for Darwin as well.
* Simplified errno handling in POSIX layer
|
|
options. Make klee_abort() call abort() in replay, and removed trivial test which cannot be easily integrated into the test suite.
|
|
corresponding tests
|
|
|
|
doDumpStates calls stepInstruction and therefore indirectly increases time and
instruction statistics for all dangling (dumped) states. This patch removes the
call, but now the timing stats for the last executed state are lost, as
StatsTracker::stepInstruction isn't called anymore.
|
|
enumeration of possible strings instead of CHECK-SAME (does not work as intended with LLVM >= 3.7)
|
|
|
|
|
|
|
|
|
|
|
|
Fixes #800
|
|
|
|
|
|
|
|
|
|
|
|
configuration, TravisCI scripts and Dockerfile build appropriately.
There are a bunch of clean ups this enables but this commit doesn't
attempt them. We can do that in future commits.
|
|
|
|
Added checks for div/mod by zero and overshifts in constant expressio…
|
|
Such div/mod by zero expressions would previously crash KLEE. Added two test cases, one for div/mod by zero, the other for overshift. This fixes the bug reported in #268.
|
|
|
|
evalConstantExpr which allows us to print the location associated with the constant in any error messages. Added a test case for the unsupported features for taking the address of a label, which exercises the patch.
|
|
|
|
|
|
doesn't seem relevant anymore given that LLVM 3.4 is the minimum version
KLEE supports. Also do minor clean up. This was spotted by @andreamattavelli.
|
|
|
|
This is useful on systems like NixOS, where python3 is not in
/usr/bin/python3 as well as for people using alternative ways to
install python such as virtualenv/pyenv.
Some scripts where already using '/usr/bin/env'. With this pull request
it gets more consistent. For background information see also:
https://github.com/systemd/systemd/pull/5816
|
|
|
|
We use LLVM's Scalarizer pass to remove most vectorized code so that the
Executor only needs to support the InsertElement and ExtractElement
instructions.
This pass was not available in LLVM 3.4 so to support that LLVM version
the pass has been back ported.
To check that the Executor is not receiving vector operand types
that it can't handle assertions have been added.
There are a few limitations to this implementation.
* The InsertElement and ExtractElement index cannot be symbolic.
* There is no support for LLVM < 3.4.
|
|
Removing flaky test Vararg.c from Darwin build until we find a proper…
|
|
|
|
|
|
This fixes #664.
As reported by @jirislaby the `test/Feature/LongDouble.cpp` test
fails to compile with Clang 3.4 due to new changes the libstdc++
headers. This ends up giving errors like
```
In file included from /home/abuild/rpmbuild/BUILD/klee-1.3.0+20170409/test/Feature/LongDouble.cpp:12:
In file included from /usr/bin/../lib64/gcc/x86_64-suse-linux/7/../../../../include/c++/7/cstdlib:77:
/usr/bin/../lib64/gcc/x86_64-suse-linux/7/../../../../include/c++/7/bits/std_abs.h:101:3: error: unknown type name '__float128'
__float128
^
/usr/bin/../lib64/gcc/x86_64-suse-linux/7/../../../../include/c++/7/bits/std_abs.h:102:7: error: unknown type name '__float128'
abs(__float128 __x)
^
2 errors generated.
```
Clang 4.0 seems fine with this source file so the problem has already
been addressed upstream so we don't need to file a bug. We just need
to move to a newer LLVM version to fix this properly!
To work around this the test has been made into a C program rather than
a C++ program to avoid including the C++ headers. The program wasn't
using any important C++ features anyway so this seems like a sensible change.
|
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
indentation and syntax highlighting.
|
|
This is useful for testing ranges. Especially when tests are run on
later LLVM versions.
This code is funny as it uses 2, 3, and 4 spaces for indentation :).
This is extensively used in #605.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|