| Age | Commit message (Collapse) | Author |
|---|
|
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>
|
|
|
|
test: POSIX, stop FD_Fail to fail
|
|
In our build environments, /etc/fstab is an empty file. Use /etc/mtab,
which should be non-empty anywhere, hopefully.
For the reference, the test fails as follows:
FAIL: KLEE :: Runtime/POSIX/FD_Fail.c (188 of 212)
************ TEST 'KLEE :: Runtime/POSIX/FD_Fail.c' FAILED ************
Script:
--
clang-3.8 -Iinclude test/Runtime/POSIX/FD_Fail.c -emit-llvm -O0 -c -o build/test/Runtime/POSIX/Output/FD_Fail.c.tmp1.bc
rm -rf build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.klee-out
build/bin/klee --output-dir=build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.klee-out --libc=uclibc --posix-runtime build/test/Runtime/POSIX/Output/FD_Fail.c.tmp1.bc --sym-files 0 0 --max-fail 1 > build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.log
grep -q "fread(): ok" build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.log
grep -q "fread(): fail" build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.log
grep -q "fclose(): ok" build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.log
grep -q "fclose(): fail" build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.log
--
Exit Code: 1
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
There was a typo and 'not' utility was tried to be built with
FileCheck's libraries. But those can be undefined. Fix this by using the
correct variable.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Rewritten tests by replacing 'XFAIL: darwin' with 'REQUIRES: not-darwin'
|
|
'not-*' features that exist if target operating system does not match a list of know operating systems.
|
|
test: ConstantExpr, kill bogus test
|
|
There is a test that thinks this should hold:
((&gInt >> 8) << 8) != ((&gInt << 8) >> 8)
For example, if the address is 0x00123400, this means:
0x00123400 != 0x00123400
which is obviously not true. Kill the bogus assumption as it causes
occasional failures in the tests. This is done by ORing the address with
1 so that we can have:
0x00123400 != 0x00123401
Convert also the respective truncated 32bit pointers to 64bit.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
* remove unused stat variable
* use %ld for long int
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Added new option --warnings-only-to-file which causes warnings to be written to warnings.txt only.
|
|
|
|
|
|
variables when possible.
Previously an alignment 8 was always used which did not faithfully
emulate what was either explicitly requested in the LLVM IR or what
the default alignment was for the target.
|
|
`klee::getDirectCallTarget(llvm::CallSite)`.
The problem is that it doesn't handle bitcasted functions that call a
weak alias.
|
|
|
|
ReadExpr::create() was missing an opportunity to constant fold
|
|
constant arrays.
|
