about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2017-07-29Added an optional KInstruction* argument to evalConstant and ↵Cristian Cadar
evalConstantExpr which allows us to print the location associated with the constant in any error messages. Added a test case for the unsupported features for taking the address of a label, which exercises the patch.
2017-07-29Added another variant of printFileLine in KInstruction that returns the ↵Cristian Cadar
location as a string. Also added const qualifier to the printFileLine functions
2017-07-28Merge pull request #728 from delcypher/cmake_change_defaultAndrea Mattavelli
[CMake] Change some defaults
2017-07-28Merge pull request #735 from andreamattavelli/fixes_travis_0717MartinNowack
[TravisCI] Some fixes for STP scripts
2017-07-28Fixed script for STP in Travis-CI: Build now exits on errorsAndrea Mattavelli
2017-07-28Modified Travis-CI script to compile STP with BOOST supportAndrea Mattavelli
2017-07-28[TravisCI] Make sure when building with CMake that only the solversDan Liew
requested get used.
2017-07-28[CMake] Change the default value of `ENABLE_SOLVER_METASMT` to be setDan Liew
dynamically based on whether MetaSMT is available. Previously the default was always off.
2017-07-28[CMake] Add `ENABLE_ZLIB` option to control whether KLEE usesDan Liew
zlib. The default is `ON` if zlib is found on first configure and `OFF` if zlib is not found on first configure.
2017-07-28[CMake] Refactor Z3 detection and change the default value ofDan Liew
`ENABLE_SOLVER_Z3` to be set dynamically based on whether Z3 is available. Previously the default was always off.
2017-07-28[CMake] Refactor STP detection and change the default value ofDan Liew
`ENABLE_SOLVER_STP` to be set dynamically based on whether STP is available. Previously the default was always off.
2017-07-27Merge pull request #734 from ccadar/miscCristian Cadar
Now that LLVM 2.9 is gone, we can use cl::bits when needed
2017-07-26Now that LLVM 2.9 is gone, we can use cl::bits instead of cl::listCristian Cadar
2017-07-26Merge pull request #733 from ccadar/miscAndrea Mattavelli
This reverts incorrect patch https://github.com/klee/klee/commit/db29…
2017-07-26This reverts incorrect patch ↵Cristian Cadar
https://github.com/klee/klee/commit/db29a0bba74b672cdf4b8fef4d94ffa6ab845e6d __fprintf_chk has a different prototype than fprintf
2017-07-25Added regression test for bug reported by @kren1 in #262Cristian Cadar
2017-07-25Merge pull request #726 from delcypher/cmake_fix_llvm_built_with_no_assertsMartinNowack
[CMake] Handle building against LLVM built without assertions
2017-07-25Cleanup tests for last LLVM 2.9 referencesAndrea Mattavelli
2017-07-25[CMake] Emit warning when mixing assert and non assert builds.Dan Liew
This could lead to lots of problems. If we discover that these configurations don't work at all we should make this an error.
2017-07-25Merge pull request #725 from ccadar/foldCristian Cadar
Refactored some code related to constant evaluation
2017-07-25[CMake] Fix bug where we would inherit LLVM's `-DNDEBUG` defineDan Liew
when LLVM was built without assertions. This prevented `ENABLE_KLEE_ASSERTS` from working correctly. Reported by @MartinNowack .
2017-07-25Merge pull request #724 from delcypher/floating_point_ops_clean_upAndrea Mattavelli
Re-enable parts of `FloatingPointOps.ll`
2017-07-25This commit simply moves evalConstant to ExecutorUtil (where ↵Cristian Cadar
evalConstantExpr also resides), as suggested by an old comment.
2017-07-25Added the const qualifier to the keys in the constantMapCristian Cadar
2017-07-25Re-enable parts of `FloatingPointOps.ll`. The message about failuresDan Liew
doesn't seem relevant anymore given that LLVM 3.4 is the minimum version KLEE supports. Also do minor clean up. This was spotted by @andreamattavelli.
2017-07-24Moved klee_choose from klee-libc to KLEE intrinsics.Cristian Cadar
2017-07-24more portable shebangsJörg Thalheim
This is useful on systems like NixOS, where python3 is not in /usr/bin/python3 as well as for people using alternative ways to install python such as virtualenv/pyenv. Some scripts where already using '/usr/bin/env'. With this pull request it gets more consistent. For background information see also: https://github.com/systemd/systemd/pull/5816
2017-07-24llvm: get rid of static_casts from iterators (take 2)Jörg Thalheim
follow up of c9c90a0ecdce10172fd5318aea60a9ff4057679f
2017-07-24Merge pull request #721 from delcypher/cmake_runtime_dependency_fixesAndrea Mattavelli
A few runtime build system fixes
2017-07-24Merge pull request #713 from MartinNowack/remove_llvm_29_33Andrea Mattavelli
Remove support for LLVM < 3.4
2017-07-24[CMake] Add a sanity check to the runtime build system so that weDan Liew
provide a better error message (and stop earlier) when no C source files are found.
2017-07-24[CMake] Fix bug where the runtime build system would not rebuild bitcodeDan Liew
archive/modules when the list of source files that constitute it changes. To fix this a file is written in the build directory that contains the list of `.bc` files. This file is updated whenever the list of `.bc` files for a module changes and then the rule that builds the module/archive depends on that file. This fixes a bug reported by @ccadar in #718.
2017-07-23Remove LLVM 2.9 from MakefilesMartin Nowack
2017-07-23Remove klee-gccMartin Nowack
2017-07-23Cleanup Travis builderMartin Nowack
2017-07-23Updated test cases to reflect removal of LLVM 2.9Martin Nowack
2017-07-23Remove support for LLVM < 3.4Martin Nowack
Request LLVM 3.4 as minimal requirement for KLEE
2017-07-21Release notes for 1.4.0 v1.4.0 1.4.xCristian Cadar
2017-07-20Switching version to 1.4.0Cristian Cadar
2017-07-20Merge pull request #657 from delcypher/vectorized_instructionsCristian Cadar
Implement basic support for vectorized instructions.
2017-07-20Replace assertions of types on LLVM instructions in the Executor with aDan Liew
pass that checks these assertions. This improves several things. * This pass provides more friendly messages than assertions in that it just emits a warning and carries on checking the rest of the instructions. * The takes the checks outside of the Executor's hot path and so avoids checking the same instruction multiple times. Now each instruction is only checked once just before execution starts. The disadvantage of this approach is the check for invariants we expect to hold have been pulled far away from where we expect them to hold. After discussion with @ccadar and @MartinNowack it was decided we will take this hit to readability for better performance and simpler code in the Executor.
2017-07-20Merge pull request #673 from jirislaby/llvm40_WallTimerMartinNowack
Core: TimingSolver, use WallTimer
2017-07-20Core: TimingSolver, use TimerStatIncrementerJiri Slaby
Do not opencode what we already have in TimerStatIncrementer. This simplifies the code a lot and makes transition to LLVM 4.0 a lot easier. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-07-20Merge pull request #704 from ccadar/TreeStreamAndrea Mattavelli
Fixes bug in TreeStreamWriter::write reported by @gladtbx in #562. A…
2017-07-19Added some unit tests for TreeStream: one testing some basic behaviour, the ↵Cristian Cadar
other a regression test for #562
2017-07-19Implement basic support for vectorized instructions.Dan Liew
We use LLVM's Scalarizer pass to remove most vectorized code so that the Executor only needs to support the InsertElement and ExtractElement instructions. This pass was not available in LLVM 3.4 so to support that LLVM version the pass has been back ported. To check that the Executor is not receiving vector operand types that it can't handle assertions have been added. There are a few limitations to this implementation. * The InsertElement and ExtractElement index cannot be symbolic. * There is no support for LLVM < 3.4.
2017-07-19Fixes bug in TreeStreamWriter::write reported by @gladtbx in #562. Also ↵Cristian Cadar
removes commented out code from that function.
2017-07-18Use assembly line for printing debug informationMartin Nowack
Instead of using an id, use the assembly line number executed
2017-07-18Merge pull request #672 from jirislaby/llvm40_static_castsAndrea Mattavelli
llvm: get rid of static_casts from iterators
2017-07-17Merge pull request #700 from andreamattavelli/fix_travis_macosCristian Cadar
Added caching of Homebrew downloads
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-07-14 20:47:26 +0000