Age | Commit message (Collapse) | Author |
|
-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
|
|
heuristics in KLEE. The new options are documented at
http://klee.llvm.org/klee-options.html.
Cleaned a bit the code in UserSearcher.cpp, and fixed some test cases
to use the new options.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@163711 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
heuristics.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@163631 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@160547 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154367 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
also used. Thanks to Paul Marinescu for reporting and debugging this.
The patch also disables the STP timeout by default.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154300 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
direct function call logic.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@136605 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
For example, clang creates these for ++ and -- operations on pointers
on 64-bit platforms.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@136474 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@131586 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@131583 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@117118 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
is run a second time without running 'make clean' in-between.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@110321 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@107912 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
http://llvm.org/bugs/show_bug.cgi?id=6690.
The patch adds specialized versions of klee_get_value for different
types, fixing the previous klee_get_value function that sometimes
truncated 64bit parameters to 32bit.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@107006 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100421 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100397 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- Based on a patch by Vladimir Kuznetsov!
- x86_64 has a complicated calling convention for va_args; instead of dealing
with this, this patch uses a clever workaround by initializing the va_list
structure so that the callee believes all arguments were passed in the stack
save area.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77819 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- Incomplete, still have to move some conversion operations.
- Also, there isn't support yet for copying long double values to native
memory.
- Still, should be a monotonic improvement and we are no longer faking long
double support.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74363 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74144 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
creation).
- Not used yet.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74142 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- There are two optional lists following the constraints and the
query expression. The first is a list of expressions to give values
for and the second is a list of arrays to provide values for.
- Update ExprPPrinter to accept extra arguments to print these
arguments.
- Add Parser support.
- Add more ArrayDecl support.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72938 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72920 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
backward compatibility. Also changed KLEE_RUNTEST to KTEST_FILE. Updated tutorial-1.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72312 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- For compatibility we still accept 2 argument form of klee_make_symbolic, but
this will go away eventually.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72265 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
- Lots more tweaks, documentation, and web page content is needed,
but this should compile & work on OS X & Linux.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8
|