about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2017-03-01Added new option --warnings-only-to-file which causes warnings to be written ↵Cristian Cadar
to warnings.txt only. Disabled by default.
2017-03-01Merge pull request #604 from jirislaby/add_castsAndrea Mattavelli
convert iterators using static_cast
2017-02-28convert iterators using static_castJiri Slaby
Newer versions of LLVM do not allow to implicitly cast iterators to pointers where they point. So convert all such uses to explicit static_cast, the same as LLVM code does. Otherwise we see errors like: lib/Core/Executor.cpp:548:15: error: no viable conversion from 'Module::iterator' (aka 'ilist_iterator<llvm::Function>') to 'llvm::Function *' Function *f = i; ^ ~ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-02-28Merge pull request #547 from delcypher/fix_alignment_of_alloc_memoryCristian Cadar
Teach KLEE to respect the requested memory alignment of allocated memory
2017-02-27Merge pull request #600 from jirislaby/no_global_contextCristian Cadar
llvm: stop using global context
2017-02-25llvm: stop using global contextJiri Slaby
It was marked as deprecated long time ago and finally removed in LLVM 3.9. Remove all uses of getGlobalContext and create our own context. Propagate it all over the code then. [v2] use ctx, not C as name Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-02-24Teach KLEE to respect the requested memory alignment of globals and stackDan Liew
variables when possible. Previously an alignment 8 was always used which did not faithfully emulate what was either explicitly requested in the LLVM IR or what the default alignment was for the target.
2017-02-24Merge pull request #603 from jirislaby/no_list_copyAndrea Mattavelli
CommandLine: do not copy list in optionIsSet
2017-02-23CommandLine: do not copy list in optionIsSetJiri Slaby
Pass the list as reference. Otherwise we can get errors with newer LLVM like: lib/Basic/ConstructSolverChain.cpp:26:19: error: call to deleted constructor of 'llvm::cl::list<QueryLoggingSolverType>' if (optionIsSet(queryLoggingOptions, SOLVER_KQUERY)) { ^~~~~~~~~~~~~~~~~~~ llvm/Support/CommandLine.h:1466:3: note: 'list' has been explicitly marked deleted here list(const list &) = delete; ^ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-02-22Merge pull request #599 from jirislaby/de_registerAndrea Mattavelli
klee: remove use of deprecated 'register'
2017-02-22Makefile: change -std-compile-opts to -O3Richard Trembecký
As per: http://llvm.org/releases/3.6.0/docs/ReleaseNotes.html#the-opt-option-std-compile-opts-was-removed the -std-compile-opts was effectively an alias of -O3. And since it was removed in later LLVM versions, stop relying on that. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-02-22klee: remove use of deprecated 'register'Jiri Slaby
New compilers warn about using 'register' as follows: ConstantDivision.cpp:66:3: warning: 'register' storage class specifier is deprecated and incompatible with C++1z [-Wdeprecated-register] Remove the register specifier -- the compilers are clever enough to know what to do. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-02-21Merge pull request #514 from ↵Andrea Mattavelli
delcypher/fix_klee_get_direct_call_bitcast_weak_alias Fix assertion failure when klee::getDirectCallTarget() is used on call to bitcasted weak alias
2017-02-21fix metaSMT versionHoang M. Le
2017-02-21Teach `klee::getDirectCallTarget()` to resolve weak aliases. This isDan Liew
controlled by a new parameter `moduleIsFullyLinked`. When true the linkage type of a weak alias is ignored. It is legal to do this when the module is fully linked because there won't be another function that could override the weak alias. This fixes a previous assertion failure in `klee::getDirectCallTarget()` triggered by the `test/regression/2016-11-24-bitcast-weak-alias.c` test case.
2017-02-21Add test case that causes an assertion failure in ↵Dan Liew
`klee::getDirectCallTarget(llvm::CallSite)`. The problem is that it doesn't handle bitcasted functions that call a weak alias.
2017-02-20Merge pull request #596 from andreamattavelli/fix_readexpr_testsCristian Cadar
Silenced warning: comparison of integers of different signs ('const i…
2017-02-16Silenced warning: comparison of integers of different signs ('const int' and ↵Andrea Mattavelli
'const unsigned long long')
2017-02-14Increased the type size for the stop-after-n-instructions option to avoid ↵Andrea Mattavelli
too strict limitations (LLVM >= 3.0)
2017-02-14Fix linker compatibility under macOSAndrea Mattavelli
2017-02-14Merge pull request #574 from delcypher/read_expr_missed_constaint_foldAndrea Mattavelli
ReadExpr::create() was missing an opportunity to constant fold
2017-02-14Refactoring code to improve readability by using UINT32/64_C macrosAndrea Mattavelli
2017-02-14Fixed assertion invocation: We were invoking bits64::truncateToNBits with a ↵Andrea Mattavelli
width greater than 64
2017-02-14Added pre/post conditions as assertionsAndrea Mattavelli
2017-02-14Added unit tests for ReadExpr::create() to check that constant folding is ↵Andrea Mattavelli
correctly applied
2017-02-14ReadExpr::create() was missing an opportunity to constant fold when handling ↵Dan Liew
constant arrays.
2017-02-14Merge pull request #590 from ccadar/stp-fork-errorAndrea Mattavelli
Added error message when STP fails to fork.
2017-02-14Added error message when STP fails to fork.Cristian Cadar
2017-02-14Merge pull request #592 from ccadar/remove-SMTAndrea Mattavelli
Removing unused lib/SMT directory
2017-02-13Removing unused lib/SMT directoryCristian Cadar
2017-02-13Merge pull request #506 from delcypher/travis_asan_ubsanCristian Cadar
Modify scripts and a test to allow ASan/UBSan builds.
2017-02-13Silenced two "control may reach end of non-void function [-Wreturn-type]" ↵Cristian Cadar
compiler warnings, one by adding an assert, and the other by refactoring the choose() function.
2017-02-13Merge pull request #588 from klee/revert-587-fix_stop_instructionsAndrea Mattavelli
Revert "Increased the type size for the stop-after-n-instructions option to a…"
2017-02-13Revert "Increased the type size for the stop-after-n-instructions option to ↵Cristian Cadar
a…"
2017-02-13Merge pull request #587 from andreamattavelli/fix_stop_instructionsCristian Cadar
Increased the type size for the stop-after-n-instructions option to a…
2017-02-13Increased the type size for the stop-after-n-instructions option to avoid ↵Andrea Mattavelli
too strict limitations
2017-02-11[CMake] More widely available rebuilding for runtimesLevente Kurusa
Signed-off-by: Levente Kurusa <levex@linux.com>
2017-02-10Merge pull request #582 from jirislaby/varargCristian Cadar
Fix Vararg test
2017-02-10test: fix broken Vararg testMartijn Thé
The helper function had int return type, while no value was being returned. Signed-off-by: Jiri Slaby <jslaby@suse.cz>
2017-01-28[cmake] add PATH_SUFFIXES needed to find z3 on FedoraKevin Laeufer
2017-01-19In legacy build system fix building libkleeRuntest when buildingDan Liew
with ASan.
2017-01-19Teach both build systems to pass the user provided CXXFLAGS and CFLAGSDan Liew
when using the native compiler in system tests. This fixes the `libkleeruntest` tests when building with ASan.
2017-01-19Fix the Autoconf/Makefile build system when building with coverageDan Liew
flags. The old build system stupidly propagates flags for the host C compiler into the flags for the C bitcode compiler leading to unwanted instrumentation being added to KLEE's runtime.
2017-01-19[TravisCI] Modify TravisCI/Docker build scripts to support doing ASan/UBSan ↵Dan Liew
builds of KLEE. Two configurations (one for each build system) have been added to TravisCI to do an ASan build.
2017-01-19Fix `Feature/MemoryLimit.c` test when building KLEE with ASan.Dan Liew
When building with ASan the `mallinfo()` function is intercepted. However the currently implementation is just a stub that always returns 0. So instead use the public API of the sanitizer runtime to get the amount of currently allocated memory when KLEE is built with ASan. Unfortunately it appears that the way to detect building with ASan differs between Clang and GCC. There was also a sanitizer runtime API change too. This was tested with * Clang 3.4, 3.5, and 3.9.0 * GCC 4.8, 4.9, 5.2, 5.4 and, 6.2.1.
2017-01-18Merge pull request #569 from delcypher/cmake_remove_enable_tests_optionAndrea Mattavelli
[CMake] Remove `ENABLE_TESTS` CMake cache option.
2017-01-18[CMake] Remove `ENABLE_TESTS` CMake cache option.Dan Liew
The intention of this option was to provide a switch that can be used to globally enable/disable tests. This option ended up causing a lot of confusion as can be seen on the discussion on writing documention for the new build system. https://github.com/klee/klee.github.io/pull/53 So it was decided to remove this option. This fixes #568 .
2017-01-18Merge pull request #546 from delcypher/cmake_rename_test_targetsCristian Cadar
[CMake] Rename "integrationtests" to "systemtests", removed some undocumented targets and other build changes
2017-01-16[CMake] If CMP0037 policy is available set it to NEW so that weDan Liew
disallow using reserved target names.
2017-01-16[CMake] Only add dependencies to `check` if the target is enabled.Dan Liew
Surprisingly the old code still worked even when the target didn't exist.