Age | Commit message (Collapse) | Author | |
---|---|---|---|
2020-06-29 | Implement fshr/fshl intrinsics | Alastair Reid | |
Changes: - IntrinsicCleaner accepts fshr/fshl as accepted intrinsics - Executor::executeCall converts fshr/fshl to urem/zext/concat/shift/extract - Klee/main suppresses warnings about externals that are LLVM reserved (i.e., begin with "llvm.") - New test exercises 32 and 7 bit versions including oversize shift values Test values are based on LLVM's test for fshl/fshr - Changes that depend on existence of fshr/fshl are guarded by #if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0) or ; REQUIRES: geq-llvm-7.0 | |||
2020-06-25 | Enforce fork/branch limits in branch() and fix double termination | Frank Busse | |
* extend help messages for -max-memory and -max-memory-inhibit * introduces branchingPermitted() * enforces fork/branch limits in branch() (vector version) * changes main loop * calls updateStates() before checkMemoryUsage() * calls updateStates() again in case we early terminate states This should prevent double termination for now. Other solutions are imho more expensive as we would have to compare possibly large vectors of states (either states(arr) in checkMemoryUsage() or removedStates in terminateState()). | |||
2020-06-25 | fix Executor: initializeGlobalAliases | Julian Büning | |
2020-06-25 | add simple unknown bitcast alias test from the original issue | Julian Büning | |
2020-06-25 | add known bitcast test for comparison | Julian Büning | |
2020-06-25 | regression test for unknown bitcast alias | Julian Büning | |
2020-06-19 | Added test reported in https://github.com/klee/klee/issues/189 for byval ↵ | Cristian Cadar | |
variadic arguments | |||
2020-06-19 | Renamed Vararg.c to VarArg.c for consistency with the other var arg tests ↵ | Cristian Cadar | |
and reformatted comments. | |||
2020-06-19 | Added test checking for correct alignment of variadic arguments | Cristian Cadar | |
2020-06-19 | Added test checking that KLEE correctly handles variadic arguments with the ↵ | Cristian Cadar | |
byval attribute | |||
2020-06-06 | [Module] Add testcase for inline asm lifting | Martin Nowack | |
2020-05-01 | Add test case from #1257 to reproduce behaviour | Martin Nowack | |
2020-04-30 | Removed the Internal directory from include/klee | Cristian Cadar | |
2020-04-09 | [posix-runtime] Improve model to handle full-path symbolic files | Timotej Kapus | |
2020-04-09 | [posix-runtime] Add test for full path consistency for symbolic files | Timotej Kapus | |
2020-04-08 | test: add a new test for readStringAtAddress | Marek Chalupa | |
Read strings from different parts of objects. | |||
2020-03-22 | [posix-runtime] Simple GET/SET_LK model | Timotej Kapus | |
2020-03-19 | Additional test for dealing with vector instructions | Cristian Cadar | |
2020-03-02 | fix lit.cfg: numerical comparison of LLVM version numbers | Julian Büning | |
2020-03-02 | test/lit.cfg: add LLVM 10.0 | Julian Büning | |
2020-01-18 | Fix handling of debug information for functions | Martin Nowack | |
Tracking function locations separately correctly without prefixing it with a directory. | |||
2020-01-13 | Assume assembly.ll is local to the run.istats file | Martin Nowack | |
Assuming a `klee-out-*` directory is moved to a different path location, subsequent analysis of the run.istats with KCachegrind focusing on assembly is impossible as the `assembly.ll` cannot be found. The reason is that the absolute path of the object file (assembly.ll) is hard-coded as part of the generated run.istats. To fix this, assume that the file is local to the `run.istats`. | |||
2020-01-10 | Fix update_list_order.c | Martin Nowack | |
2019-12-12 | [optimize-array] Fix value transformation | Timotej Kapus | |
Value transformation operates on word instead of byte arrays. That means the Read indicies need to be adjusted to reflect that. Previously IndexCleanerVisitor tried to remove the multiplications in the index to covert byte indicies to word indicies. However as the two added test cases show this is not sufficent. Therefore we remove the IndexCleanerVisistor and just divide the index with word size which should always be correct. | |||
2019-12-12 | [optimize-array] Fix hole index in buildMixedSelectExpr | Timotej Kapus | |
buildMixedSelectExpr was using the byte index for holes in the select condition instead of the word based one. This only occured if there was more than 1 hole. | |||
2019-12-12 | [optimize-array] Fix update list read order | Timotej Kapus | |
ArrayExprOptimizer read the UpdateList in the wrong order, which meant that it used least recent update instead of the most recent one. This patch fixes this as well as adds a test to illustrate the issue. | |||
2019-11-15 | Implement @llvm.is.constant() intrinsic handling and add a test for it. | Gleb Popov | |
2019-11-07 | Handle llvm.objectsize explicitly | Martin Nowack | |
llvm.objectsize is used in several optimisation during compile time. Lowering these intrinsics took a conservative approach returning always the value for unknown. Instead, lower to the object's real size, if possible. Otherwise, a conservative value is used. Since LLVM 4.0, the function `llvm::lowerObjectSizeCall()` does exactly this. Use this function or preserve the old behaviour for older LLVM versions. | |||
2019-11-07 | Added test for 3-argument main. | Cristian Cadar | |
2019-11-05 | Most libc++ tests require uclibc; add missing REQUIRES statements or remove ↵ | Cristian Cadar | |
dependency. | |||
2019-11-05 | Mark all constant global memory objects as constant | Martin Nowack | |
Fixes #264. We first aggregate all constant memory objects initialise them and initialise their counter parts in the concrete memory. After that, we mark memory objects as constant such that they can't be modified (i.e. this includes marking them symbolic). | |||
2019-11-05 | [test] Fix missing includes | Martin Nowack | |
Fix multiple missing includes | |||
2019-10-31 | Executor: fix missing default case in switch instruction | Frank Busse | |
2019-10-31 | enable testing for LLVM 9.0 | Julian Büning | |
2019-10-31 | LLVM 9.0: fourth parameter for @llvm.objectsize() | Julian Büning | |
2019-10-31 | klee-libc: add bcmp | Julian Büning | |
2019-10-07 | test/Expr/Evaluate2.kquery: add link to issue | Julian Büning | |
2019-10-07 | fix: make llvm 7.1 known | Julian Büning | |
2019-10-07 | test/Feature/SolverTimeout.c: re-enable for Z3 | Julian Büning | |
2019-10-07 | test/lit.cfg: test if current version is known | Julian Büning | |
2019-10-07 | test/lit.cfg: use lit_config instead of lit | Julian Büning | |
Since LLVM version 3.6.0 or lit version 0.5.0, `lit_config` is the name of the global object, not `lit`. | |||
2019-10-07 | Do not use klee_range() in regression/2014-09-13-debug-info.c test, as it is | Gleb Popov | |
incompatible with klee_prefer_cex. Fixes https://github.com/klee/klee/issues/1161 While there, remove dependence on `sort` utility, which might help porting KLEE Windows eventually. | |||
2019-09-20 | Move intrinsics tests to the proper directory | Mateusz Naściszewski | |
2019-09-20 | Add tests for saturating arithmetic | Mateusz Naściszewski | |
2019-09-05 | test/CMakeLists.txt: error handling for download | Julian Büning | |
2019-09-05 | test/CMakeLists.txt: use official llvm monorepo for download | Julian Büning | |
2019-08-14 | Update basic block iterator after deleting instruction; add test case | Martin Nowack | |
2019-08-14 | Rewrote the checks in GenRandomBout.c to remove dependency on bash and use ↵ | Cristian Cadar | |
FileCheck instead (FreeBSD tests on Travis CI fail otherwise) | |||
2019-08-14 | Moved Gen*Bout.c tests outside the test/Runtime/POSIX directory, as they ↵ | Cristian Cadar | |
don't need POSIX support to run. | |||
2019-08-14 | Replace sprintf with snprintf throughout codebase | Cristian Cadar | |