about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2019-03-05add regression test for LLVM PR39177Julian Büning
2019-03-05workaround for LLVM PR39177Julian Büning
provides a workaround for LLVM bug PR39177, which affects LLVM versions 3.9 - 7.0.0: https://bugs.llvm.org/show_bug.cgi?id=39177 This commit is intended to be reverted once support for LLVM versions <= 7 is dropped from KLEE.
2019-03-05ktest-tool: add --extract optionFrank Busse
2019-03-05Renamed "Starting options" to "Startup options" and added a missing space in ↵Cristian Cadar
a help message.
2019-03-05remove klee-clang, use wllvm/gllvm insteadFrank Busse
2019-03-05fix Executor::initializeGlobals for aliases pointing to another aliasJulian Büning
2019-01-15make AssignmentLessThan::operator() const-invocableJulian Büning
2019-01-07fix a bug in a function callTipwheal
the function name is "getTreeStream" but here's a spelling error
2018-12-19ktest-tool: move from optparse to argparse, add ouput/example sections to helpFrank Busse
2018-12-19Travis OSX: install Python 3.xFrank Busse
2018-12-19regression/2014-09-13-debug-info.c: use 'int: ' instead of 'data:'Frank Busse
2018-12-19Various fixes for ktest-toolFrank Busse
* switch to Python 3 * add file encoding * some PEP8 reformatting * fix TOCTOU for open * replace trimZeros() with rstrip * remove unused pos/args variables * remove --write-ints (print by default) * remove progname section (unused) * added/modified output rows - "data:" now shows the Python representation (for use in scripts) - "hex :" shows the hex representation - "text:" shows ASCII, all out-of-range/non-printable characters are replaced by a dot - "int :"/"uint:" print (unsigned) 8/16/32/64 bit integers * reduce width for object counter to needed minimum instead of 4 * refactor printing into function
2018-12-19Added default values to option commentsMartinNowack
Co-Authored-By: ccadar <c.cadar@imperial.ac.uk>
2018-12-19Renamed --environ to --env-fileCristian Cadar
2018-12-19Renamed --stop-after-n-tests to --max-testsCristian Cadar
2018-12-19Added a replaying option categoryCristian Cadar
2018-12-19Added checks option category, moved --optimize to starting category, renamed ↵Cristian Cadar
original --run-in option to --running-dir
2018-12-19Added linking option categoryCristian Cadar
2018-12-19Added starting option categoryCristian Cadar
2018-12-19Added test case option categoryCristian Cadar
2018-12-19Added debugging categoryCristian Cadar
2018-12-19Renamed --stop-after-n-instructions to --max-instructions, as suggested by @251Cristian Cadar
2018-12-19Added some descriptions suggested by @MartinNowack and placed ↵Cristian Cadar
--max-static-... options under the termination category of options
2018-12-19Added option categories for external call policy and termination criteriaCristian Cadar
2018-12-19Created two more option categories: test generation and seeding.Cristian Cadar
2018-12-14Enable C++14 supportMartin Nowack
2018-11-23Implemented memalign with alignmentLukas Wölfer
2018-11-11Use LLVM 4 for Mac BuildMartin Nowack
2018-11-07Fix bug which resulted in an incorrect warning to be printed.Cristian Cadar
2018-11-06fix: actually set -O0 in test/concrete/CMakeLists.txtJulian Büning
`-O0` has to be used in conjunction with, not instead of `-Xclang -disable-O0-optnone`
2018-11-05Fixed crash on zero size arraysLukas Wölfer
2018-11-05Check for stack overflow in a tested programMartin Nowack
Check if a state reaches the maximum number of stack frames allowed. To be performant, the number of stack frames are checked. In comparison, native execution checks the size of the stack. Still, this is good enough to find possible stack overflows. The limit can be changed with `-max-stack-frames`. The current default is 8192 frames.
2018-11-02Added test for the case where external calls are encountered but disallowedCristian Cadar
2018-11-02Replaced --no-externals and --allow-external-sym-calls with ↵Cristian Cadar
--external-calls, updated tests accordingly, and improved documentation on external calls
2018-11-02The test DeterministicSwitch.c does not need to allow external symbolic callsCristian Cadar
2018-11-02Introduced a constraint solving option category to which all the options in ↵Cristian Cadar
CmdLineOptions.cpp are currently added.
2018-10-30Base time API upon std::chronoFrank Busse
This should not change the behaviour of KLEE and mimics the old API. - functions moved from util into time namespace - uses time points and time spans instead of double - CLI arguments now have the form "3h5min8us" Changed command line parameters: - batch-time (double to string) - istats-write-interval (double to string) - max-instruction-time (double to string) - max-solver-time (double to string) - max-time (double to string) - min-query-time-to-log (double to string) - seed-time (double to string) - stats-write-interval (double to string) - uncovered-update-interval (double to string) - added: log-timed-out-queries (replaces negative max-solver-time)
2018-10-29add %OOopt to recently added tests and ConcreteJulian Büning
2018-10-26travis: enable LLVM 7 testingJiri Slaby
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26llvm7: handle new header filesJiri Slaby
createLowerSwitchPass moved in llvm commit 49ca55e3813c to Utils.h. createInstructionCombiningPass moved in llvm commitb5b7fce64c1d to InstCombine.h. So add the includes where needed. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26llvm7: adapt to new openFileForWriteJiri Slaby
In llvm commit 03bcb2143b5c, OpenFlags were split and openFileForWrite accepts one more parameter. Fortunately, openFileForWrite now defaults to F_None, so we remove the parameter completely from llvm 3.7 and later. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26llvm7: WriteBitcodeToFile takes Module &Jiri Slaby
Since llvm commit 06d6207c1c63, WriteBitcodeToFile accepts Module &, not Module *. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26Added gen-bout tool to generate ktest file (file.bout) using specified ↵Andrew Santosa
concrete arguments and files. * Sample use cases: * Using an interesting input as a seed, such as a crashing input. * Analyzing the path condition of a crashing input. * Also added the test: test/Runtime/POSIX/GenBout.c
2018-10-26travis: enable LLVM 6 testingJiri Slaby
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26llvm6: handle headers renamingJiri Slaby
Some headers were moved from llvm/Target/ to llvm/CodeGen/. Handle that. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26llvm6: SetVersionPrinter now passes down a streamJiri Slaby
I.e. klee::printVersion should now have a parameter -- the output stream. Change both the prototype and the implementation to handle this properly. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26travis: enable LLVM 5 testingJiri Slaby
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26llvm5: APInt->getSignBit -> getSignMaskJiri Slaby
This was renamed in LLVM commit 54f0462d2b7f, so handle the rename. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26llvm5: CallSite.paramHasAttr is indexed from 0Jiri Slaby
Since LLVM 5 commit 1f8f0490690b, CallSite.paramHasAttr is indexed from 0, so make sure we use correct indexing in klee. And use CallSite.hasRetAttr for return attributes. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26llvm5: test, add -disable-O0-optnone to -O0Jiri Slaby
Otherwise optimizations done in klee won't have any effect. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-12-03 10:18:49 +0000