| Age | Commit message (Collapse) | Author |
|---|
|
Added option to specify a different entry point from main(). Remove some whitespaces.
|
|
|
|
It failed when the function being called is a bitcasted alias.
|
|
compilation.
|
|
|
|
The test contains the program proposed by Eric Rizzi in https://github.com/klee/klee/issues/227, and shows a case in which a constant constraint results after the optimisation.
|
|
also test a negative constant as the lhs.
|
|
between arrays created at the same location but with different sizes
|
|
|
|
Instead of checking for every possible casse which result in overflow,
it is much simpler to perform the operation using integers with bigger
dimension and check if the result overflow
|
|
Previously the check was done as
unsigned int a, b, c;
c = a * b;
if (c < a)
// error
but it is wrong, since it catches only a subset of all the
possible overflows.
This patch improves the check as
unsigned int a, b, c;
if ((a > 1) && (b > 1){
if ((UINT_MAX/a) < b)
// error
}
An additional case has been added to the tests, with two 32-bit
values that cause overflow and are not detected by the old check.
It is also necessary to break the lowering procedure in case the current
BasicBlock is splitted; in this case it was necessary in order not to
trigger the division by 0 error.
|
|
|
|
Will redo the merge to preserve original commits.
This reverts commit a743d7072d9ccf11f96e3df45f25ad07da6ad9d6.
|
|
and mul operations. Refactored tests into two main cases, and
disabled them on LLVM 2.9, which does not support -fsanitized=*signed-integer-overflow.
|
|
Fix va args passing for big types
|
|
unconstrained buf[3]
|
|
Removed XFAIL tag from the Feature/VarArgLongDouble.c test
Fixed Executor to (more) correctly handle the alignment of types larger than 64bit (such as long double) when those are passed in var_args on x86_64.
Specifically:
From http://www.x86-64.org/documentation/abi.pdf
AMD64-ABI 3.5.7p5: Step 7.
Align l->overflow_arg_area upwards to a 16 byte boundary if alignment needed by type exceeds 8 byte boundary.
|
|
varargs on x86_64.
|
|
- KCachegrind appears to expect the first function name to be preceeded by the
name of the file it appears in. Otherwise, it will end up creating two
different records for the function, one of which has no file name and won't
have any statistics.
|
|
- This makes KCachegrind output look nicer, as otherwise it assumes
instructions without debug info were inlined and shows some message to that
effect.
- This does however we might be lying a bit about the source line that an
instruction came from.
- This also adds a test case for our istats output, yay!
|
|
- I suspect no one is using this feature, and I'm not sure it is well conceived
either. Ripping it out for now in lieu of bothering to maintain it.
|
|
|
|
- The change in 6829fb9 caused us to not allocation InstructionInfo objects for
instructions without source-level debug info, however, that means that all
such instructions end up sharing the one dummy InstructionInfo object, which
really breaks statistics tracking.
- This commit basically reverts that change, and also changes the code so we
don't ever use the dummy InstructionInfo object for instructions, so that
this problem can't be hit in other ways (e.g., if someone modifies the module
after the InstructionInfoTable construction). There is a FIXME for checking
the same thing for functions.
- Fixes #144.
|
|
path.
- Otherwise this test takes a long time just hammering on the allocator trying
to get to the memory limit.
|
|
parallel.
- It would be nice if there was an easier way to do this that didn't involve
editing all of the tests (like running each test in its own directory), but
this approach fixes #146 and doesn't involve changing 'lit' or writing a
wrapper harness. My assumption is a lot of tests start are derived from
another one, so hopefully following this convention won't be burdensome, and
I updated 'make check' so that it will produce an error if any test runs klee
without --output-dir (by checking for the existing of klee-last files).
- This also helps with #147 but I still can't fully run tests in parallel (I
start hitting STP errors).
|
|
|
|
instruction in main().
|
|
optimizations are enabled.
|
|
behaviour for arithmetic right shift are identical.
|
|
to zero. Test case is included.
|
|
behaviour for logical right shift are identical.
|
|
behaviour for left shift are identical.
|
|
Say hello to our new friend, llvm-lit :)
|
|
DejaGNU testing used to have this flag in its substitution variable
but for llvm-lit this has not been done.
I could replicate what DejaGNU did but by forcing developers to be
explicit when creating LLVM bitcode
* Remove test suite inconsistentcies. Some tests explictly use
-emit-llvm
* Allows for tests to be written in the future that invoke
the compiler as a native compiler
|
|
seemed to causing problems for llvm-lit's parser.
|
|
{ } quotes. I also add FileCheck lines but I've not added running
FileCheck because only new versions of FileCheck support the CHECK-DAG:
syntax.
|
|
a file created by KLEE exists. A big difference between
DejaGNU and llvm-lit is that in DejaGNU the working directory
is the test output directory (e.g. test/Feature/Output) but
in llvm-lit the working directory is the test directory
(e.g. test/Feature )
To fix this I have used the %T substitution variable for llvm-lit.
I have also improved some tests by using LLVM's FileCheck tool
and removing of hard coded constants for data type size in
some places.
This commit inevitably breaks running the tests under DejaGNU.
Although it is possible to hack by introducing the %T substitution
variable some tests would still be broken because the use of shell
pipes in DejaGNU doesn't seem to work properly. I could work around
this but it's really not worth the effort.
|
|
Fixed bug where divide by zero bugs would only be detected once in a program
|
|
./test/Feature/ExprLogging.c -- using the counterexample cache affects the total number of queries issued to the solver.
|
|
|
|
command line argument).
Overshift is where a Shl, AShr or LShr has a shift width greater
than the bit width of the first operand. This is undefined behaviour
in LLVM so we report this as an error.
|
|
even if there were many divide by zero bugs.
The fix basically inlines all function calls to klee_div_zero_check()
so that each call to klee_report_error() is a unique instruction
for each instrumentation of a divide operation.
It also seems that inlining the call "magically" fixed the debug information
(file and line number) of the instruction so that the debug information on the
inlined instructions matches that of the instrumented division instruction.
Note that the command line option -emit-all-errors could be used to
workaround the bug fixed in this commit.
|
|
Major changes are:
- Switching to llvm-link to build archive files
- Use GetMallocUsage instead of GetTotalMemoryUsage (be aware of bug in
LLVM 3.3 http://llvm.org/bugs/show_bug.cgi?id=16847)
- intrinsic library functions like memcpy/mov/set use weak linkage to be
replaced by e.g. uclibc functions
- rewrote linking with library
- enhanced MemoryLimit test case to check if mallocs were successful
|
|
|
|
STP. More specifically, command-line options max-stp-time, use-forked-stp and stp-optimize-divides renamed to max-solver-time, use-forked-solver and solver-optimize-divides, respectively.
Option of running the SMT solver in a separate process (i.e. forked) set to true by default.
Options of running SMT solver forked and with optimized divides made available to Kleaver as well.
|
|
logging class hierarchy.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171387 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
Addresses the issue raised by Bowen Zhou at http://keeda.stanford.edu/pipermail/klee-dev/2012-November/000972.html.
Fixed test case that depended on the old behavior.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@168797 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
by the compiler (this was failing with clang/llvm 3.1).
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@168795 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
-print-smt option. Improved Feature/ExprLogging.c test:
- Now (primitive) checks the result of -write-smt2s
- Now (primitive) checks the result of -write-pcs
- Now (primitive) checks the result of -write-cvcs"
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166569 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
-use-query-pc-log and -use-stp-query-pc-log and replaced with better
command line option -use-query-log=option. Multiple comma seperated
options can be specified after -use-query-log=. In addition queries
can now be logged in SMT-LIBv2 format as well as KQuery format. The
names of logging files has changed and also KLEE now informs users
which files are being written to.
Because of the changes the test/Feature/ExprLogging.c test broke so it
was necessary to fix it."
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166565 91177308-0d34-0410-b5e6-96231b3b80d8
|
