about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
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
2017-07-16Added caching of Homebrew downloadsAndrea Mattavelli
2017-07-08Corrected comment of Z3Solver classAndrew Santosa
2017-06-16move module loading into external functionJörg Thalheim
- having an explicit function which is defined for multiple llvm versions separately increases readability. - also: error handling was simplified - Personal motivation: being able to use this functionality in unit tests fixes #561 related to #656
2017-06-16llvm37: introduce type for PassManagerJiri Slaby
In LLVM 3.7, PassManager was moved to the legacy:: namespace. Introduce a type for it and use it in the code. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-06-16Added location info for external calls and improved a message.Cristian Cadar
2017-06-15Merge pull request #680 from jirislaby/llvm37_dilocCristian Cadar
llvm37: do not copy DILocation to getDSPIPath
2017-06-15llvm37: do not copy DILocation to getDSPIPathJiri Slaby
DILocation is not copyable in LLVM 3.7. So, pass it as reference and make it const given we do not write to it. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-06-15llvm: get rid of static_casts from iteratorsJiri Slaby
In commit b7a6aec4eeb4 (convert iterators using static_cast), I switched all implicit casts to static_cast. It turned out that llvm 4.0 banned casting via static_cast. See e.g. 1e2bc42eb988 in the llvm repo what they do. So similarly to the above commit, change all the casts of iterators to "&*" which is what they do in LLVM. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-06-12llvm: don't use clEnumValEnd for LLVM 4.0Jiri Slaby
It became unnecessary when defining options and mainly undefined. So introduce KLEE_LLVM_CL_VAL_END as suggested by @delcypher. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-06-08Merge pull request #675 from ccadar/varargsAndrea Mattavelli
Fixed typos in comments related to vararg support.
2017-06-08Merge pull request #667 from andreamattavelli/fix_macos_varargCristian Cadar
Removing flaky test Vararg.c from Darwin build until we find a proper…
2017-06-08Fixed typos in comments related to vararg support.Cristian Cadar
2017-06-07Prevent test failure when realloc fails in test/Feature/Realloc.cAndrew Santosa