about summary refs log tree commit diff homepage
path: root/lib
AgeCommit message (Collapse)Author
2014-01-17Fix error message for failing linking of librariesMartin Nowack
In case linking of external libraries failed, user would only be informed if KLEE is compiled with assertions enabled. This fix lets KLEE always fail.
2014-01-17Make KLEE fail in case main function is missingMartin Nowack
Existence of main() function is checked with assertion. This check fails if KLEE is compiled in Release mode.
2014-01-12Merge pull request #68 from MartinNowack/feature_kleeInternalFunctionsDan Liew
Feature klee internal functions
2013-12-21Do not install KLEE's internal libraries.Dan Liew
2013-12-19Added a few comments to Executor::getLastNonKleeInternalInstruction()Dan Liew
emphasising that the function cannot be returned from early.
2013-12-19When writing stack traces for bugs write the location in the assembly.llDan Liew
file as well.
2013-12-19If error location information is missing be explicit about it. ThisDan Liew
is more helpful because often the next message is "Now ignoring error at this location". Which is slightly confusing when no location is shown.
2013-12-19Only record debug info into InstructionInfoTable if debug informationDan Liew
is actually available. In addition if doing a DEBUG build then the command line flag -debug-only=klee_missing_debug shows the instructions missing debug information and -debug-only=klee_obtained_debug show the instructions with debug information.
2013-12-19Remove old algorithm for acquiring debug info. Since LLVM 2.7,Dan Liew
debug information is attached directly to most instructions so the simpler algorithm added in 5ecfd6e2fd5becc10be355b3a20d014e76e40518 can be used. Since support for LLVM version < 2.9 has been removed the old algorithm should be removed. This has been tested with LLVM 2.9 and LLVM 3.3
2013-12-19Optimize inlineChecks functionMartin Nowack
* Just iterate over the instructions which use the function to be inlined * Handle each callsite (e.g. CallInst and InvokeInst)
2013-12-19Replicate debug information from checked instructions to checker call.Martin Nowack
2013-12-19Allow to specify KLEE-internal functionsMartin Nowack
KLEE provides runtime library functions to do detection of bugs (e.g. overflow). This runtime functions are not the location of the bugs but it is the next non-runtime library function from the stack. Use the caller inside that function to indicate where the bug is.
2013-12-19Simplify acquisition of debug informtion for instruction info with newer ↵Martin Nowack
LLVM versions With newer LLVM versions (starting with LLVM 2.7) debug information are directly associated as meta data with each instruction. Therefore, debug information can be acquired directly from each instruction.
2013-12-06Remove stoppoint referencesMartin Nowack
2013-12-06Deprecate LLVM 2.8 and lowerMartin Nowack
2013-12-05Fix unitialized valueMartin Nowack
2013-12-05Free used constants if not used anymoreMartin Nowack
Fixes memleak
2013-12-05Fix timer leakMartin Nowack
2013-11-13Fix using assembler addresses for global variablesMartin Nowack
Format of assembler address strings are different with newer LLVM version (They don't have a prefix anymore). This fix takes care of newer LLVM versions (>=3.3) as well.
2013-10-29Merge pull request #26 from delcypher/fix_divide_by_zeroPaul
Fixed bug where divide by zero bugs would only be detected once in a program
2013-10-15command-line option --use-metasmt declared and defined inside #ifdef ↵Hristina Palikareva
SUPPORT_METASMT ... #endif macros
2013-10-11getConstraintLog() of MetaSMTSolver explicitly states that this feature is ↵Hristina Palikareva
not supported; a test case modified to not fail because of this.
2013-10-11Bug fix in MetaSMTBuilderHristina Palikareva
2013-10-11MetaSMT builder, solver and command-line options.Hristina Palikareva
2013-10-11Merge pull request #40 from antiAgainst/intrinsic-trapCristian Cadar
Bugfix: Remove llvm.trap declaration after cleaning all uses.
2013-10-08Remove llvm.trap declaration after cleaning all uses.Lei Zhang
2013-10-08Merge pull request #34 from ddcc/masterCristian Cadar
Replace current implementation of linkWithLibrary()
2013-09-25Merge pull request #25 from paulmar/masterCristian Cadar
Added some of the common *at functions & others to the model. Obey --max-forks in switch statements.
2013-09-25Obey --max-forks in switch statementsPaul Marinescu
2013-09-24Add missing header file and linker parameterDominic Chen
2013-09-24Replace implementation of linkWithLibrary()Dominic Chen
2013-09-23Lower intrinsic instruction "llvm.trap" to a call of the abort() function.Lei Zhang
2013-09-21Merge pull request #17 from MartinNowack/LLVM33Cristian Cadar
Make KLEE compile with LLVM 2.3.
2013-09-17Merge pull request #21 from delcypher/fix_query_loggingCristian Cadar
Fix queries not being logged correctly if an assertion failure is hit.
2013-09-02Implemented runtime check for overshift (controllable with --check-overshiftDan Liew
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.
2013-09-02Fixed bug where divide by zero bugs would only be detected once in a programDan Liew
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.
2013-09-02Fixed unused static function warning for forceImportMartin Nowack
2013-08-30Merge branch 'CompilerWarnings' of https://github.com/MartinNowack/klee into ↵Cristian Cadar
MartinNowack-CompilerWarnings
2013-08-29Revert "Use new PathV2 interface for LLVM 2.9 and higher"Martin Nowack
This reverts commit 5c059018c02a7c7db252a3cb636a39c89c430a06.
2013-08-29Merge branch 'CompilerWarnings' of https://github.com/MartinNowack/klee into ↵Cristian Cadar
MartinNowack-CompilerWarnings
2013-08-29Use new PathV2 interface for LLVM 2.9 and higherMartin Nowack
Enable PathV2 interface starting from LLVM 2.9 and do some minor include cleanup.
2013-08-28Merge branch 'CompilerWarnings' of https://github.com/MartinNowack/klee into ↵Cristian Cadar
MartinNowack-CompilerWarnings
2013-08-28Fixed warning about unused variableMartin Nowack
2013-08-28Fix constness warnings issued by gcc 4.7Martin Nowack
2013-08-28Silence warning of deprecated PathV1 usageMartin Nowack
2013-08-27Handle constant arrays as wellMartin Nowack
2013-08-27Port to LLVM 3.3Martin Nowack
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
2013-08-23In QueryLoggingSolver call flush() on std::ofstream so that queriesDan Liew
get correctly logged if an assertion failure is hit later on.
2013-08-16Merge pull request #9 from delcypher/refactor-arg-initCristian Cadar
Slight refactor of code initialising memory for argments/environment c-strings
2013-08-15Merge pull request #18 from MartinNowack/FeatureUMulOverflowCristian Cadar
Patch Set III (update) Implemented llvm.umul.with.overflow
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-11 12:04:54 +0000