about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
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>
2018-10-26llvm5: test, change objectsizeJiri Slaby
@llvm.objectsize has now three aguments, so fix the tests accordingly. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26llvm5: Intrinsic::objectsize has three argumentsJiri Slaby
Modify the IntrinsicCleaner accordingly. We do not do anything with the third argument as we do not handle the first argument in any way. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26llvm5: use MutableArrayRef for APFloat::convertToIntegerJiri Slaby
In llvm 5, since commit 957caa243d9270df37a566aedae3f1244e7b62ef, the first parameter to APFloat::convertToInteger is MutableArrayRef. So handle that. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26llvm5: handle new file_magic's locationJiri Slaby
llvm 5, moved file_magic to BinaryFormat in commit 19ca2b0f9daed883c21730285d7f04424e5f5f88, so adapt to that. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26llvm5: SwitchInst case functions now return pointersJiri Slaby
Starting llvm 5, SwitchInst->findCaseValue() now has to be dereferenced using ->. So do so, otherwise we see: ../lib/Core/Executor.cpp:1598:38: error: no member named 'getCaseSuccessor' in 'llvm::SwitchInst::CaseIteratorImpl<llvm::SwitchInst::CaseHandle>'; did you mean to use '->' instead of '.'? BasicBlock *caseSuccessor = i.getCaseSuccessor(); ^ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26llvm5: handle getOrInsertFunction terminatorJiri Slaby
llvm 5 does not terminate getOrInsertFunction parameters with NULL, take care of that. Since commit 9d54400bba7eb04bca80fce97fa170452d19eaf1. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26llvm5: integerPartWidth is from llvm::APFloatBaseJiri Slaby
Otherwise we see: ../lib/Expr/Expr.cpp:331:14: error: no member named 'integerPartWidth' in namespace 'llvm'; did you mean 'llvm::APFloatBase::integerPartWidth'? Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26llvm5: avoid ++ on function->arg_begin()Jiri Slaby
Starting with llvm 5, arguments of a function are not an iterator, but an array. So they cannot be incremented in-place. Add a local auto variable and increment that. Otherwise we see: ../tools/klee/main.cpp:661:23: error: expression is not assignable Value *oldArgv = &*(++mainFn->arg_begin()); ^ ~~~~~~~~~~~~~~~~~~~ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-24Add testcase for shift checkMartin Nowack
Validate non-optimised and optimised variant of added checks.
2018-10-24ShiftChecker: Instrument shift instructions only onceMartin Nowack
As the shift checker could be executed multiple times, we need to avoid that shift instructions are instrumented multiple times as well. Mark the instrumented instruction using metadata and avoid it in successive runs.
2018-10-24ShiftChecker: Avoid unneeded checksMartin Nowack
Do not instrument shift operations with constant shift operations that are smaller than the type size.
2018-10-24ShiftCheck: Use llvm::Builder instead of Inst::Create*Martin Nowack
Use llvm::Builder instead of Inst::Create* to create instruction. This handles metadata automatically and does instruction folding if possible. Updated to C++11 and clang-formatted.
2018-10-24Add test case for div checkerMartin Nowack
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.
2018-10-24DivCheck do not instrument multiple timesMartin Nowack
DivChecker can be executed multiple times due to the new linking process. Avoid instrumenting div instructions multiple times by annotating checked instructions with marker. Only unmarked div instructions will be instrumented.
2018-10-24DivCheck Skip unneeded checksMartin Nowack
Do not instrument divisions which do have a constant non-zero value.
2018-10-24Use llvm::Builder for DivCheck instrumentationMartin Nowack
Use llvm::Builder instead of raw `*Inst::create()` functions. Builder automatically manages metadata (e.g. debug, TBAA, ..) such that we don't have to take care of this automatically. Updated code to C++11 and clang-formated it.
2018-10-24Introduce KLEEIRMetaData to manipulate LLVM-IR metadataMartin Nowack
Simplify the handling of metadata attached to LLVM IR that is specific to KLEE.
2018-10-24Added lowering passRafael Zaehl
2018-10-23refactor klee_open_output_file to return std::unique_ptrJulian Büning
and introduce klee_open_compressed_output_file with similar behavior along some other minor improvements
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-12 22:19:24 +0000