| Age | Commit message (Collapse) | Author |
|---|
|
--external-calls, updated tests accordingly, and improved documentation on external calls
|
|
|
|
|
|
Otherwise optimizations done in klee won't have any effect.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Validate non-optimised and optimised variant of added checks.
|
|
Check that only important div instructions are annotated.
Check the optimized case as well: the call to the validating function
might not be part of the code anymore but already inlined - make sure
the instruction still has the metadata attached.
|
|
|
|
|
|
As we do not support LLVM 2.9 anymore, we can use FileCheck LINE instead of hard coding line numbers.
|
|
Vararg test can fail if KLEE is able to resolve the
intended out-of-bound memory address to a memory object.
To avoid this, allocate memory explicitly deterministic with
sufficient space between the allocations.
Enables support for Mac OSX again
|
|
|
|
|
|
|
|
|
|
* handle BlockAddress (which is not a valid function pointer)
* there is no instruction with opcode 0
* add test for functionality
|
|
alias in LLVM 3.8 has a new format, it adds an AliaseeTy parameter. So
handle this in the tests.
[v2] add comments about what was changed and why
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
deprecated for many years now and causes problems during replay. Changed and simplified affected test case.
|
|
Shifting negative values is implementation-defined.
Shifting by equal number of the bits as is the size of the type is
undefined.
So fix both of these.
This fixes #911.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
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>
|
|
|
|
|
|
|
|
|
|
enumeration of possible strings instead of CHECK-SAME (does not work as intended with LLVM >= 3.7)
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
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.
|
|
Rewritten tests by replacing 'XFAIL: darwin' with 'REQUIRES: not-darwin'
|
|
|
|
ReadExpr::create() was missing an opportunity to constant fold
|
|
constant arrays.
|
|
The helper function had int return type, while no value was being
returned.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
Brings llvm-ar into line with llvm-as and lli, removing the assumption that
llvm-ar is installed system wide
|
|
|
|
For performance reasons, if KLEE branches, one state is reused
and it is progressed by adding new constraints.
Make sure both new states end up at the end of the BFS searcher queue.
|
|
Improved support for assembler handling.
Providing additional triple information
to raise assembler for supported architectures
only.
Implemented support for raising full assembly
memory fence.
Added initial support for memory fences in Executor.
|
|
It allows stopping the execution on some conditions like assertions.
The use is like:
klee -exit-on-error-type=Assert -exit-on-error-type=External file.llvm
This is especially useful in the SV-COMP.
A test to cover the new parameter was added too.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
Sometimes, globals are not sized and ->getTypeStoreSize on such type
crashes inside the LLVM. Check whether type is sized prior to calling
the function above.
A minimalistic example of Y being unsized with no effect on the actual
code is put to tests.
[v2]
Use klee_warning for printing. And use %.*s formatting string given
StringRef.data() need not be null terminated.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
