* [Lit] Add system information (linux/darwim) to LIT configuration. Added 'not-*' features that exist if target operating system does not match a list of know operating systems.
* Fix test case for OSX: only weak aliases are supported on darwin Rewritten tests by replacing 'XFAIL: darwin' with 'REQUIRES: not-darwin'
* [travis] use a proper version of metaSMT via environment variable METASMT_VERSION
* [travis] build metaSMT without C++11
* remove special handling of metaSMT_CXXFLAGS (unnecessary now as we use a fixed version of metaSMT with this flag being properly set)
* [WIP] Fix bug where stats would not be updated on early exit caused by finding a bug with the `-exit-on-error` option enabled.
* Replace `llvm:errs()` with `klee_error()` as suggested by @andreamattavelli
* Add test case to check that on early exits stats are flushed
* Add `AssignmentValidatingSolver`. It's purpose is to check any computed assignments against the corresponding `Query` object and check the assignment evaluates correctly.
* [CMake] Unbreak build due to not adding AssignmentValidatingSolver.cpp to list of source files.
* Fix `Feature/MemoryLimit.c` test when building KLEE with ASan.
* [TravisCI] Modify TravisCI/Docker build scripts to support doing ASan/UBSan builds of KLEE.
* Fix the Autoconf/Makefile build system when building with coverage flags.
* Teach both build systems to pass the user provided CXXFLAGS and CFLAGS when using the native compiler in system tests.
* In legacy build system fix building libkleeRuntest when building with ASan.
* Increased the type size for the stop-after-n-instructions option to avoid too strict limitations
* Revert "Increased the type size for the stop-after-n-instructions option to a…"
* Silenced two "control may reach end of non-void function [-Wreturn-type]" compiler warnings, one by adding an assert, and the other by refactoring the choose() function.
* Removing unused lib/SMT directory
* Added error message when STP fails to fork.
* ReadExpr::create() was missing an opportunity to constant fold when handling constant arrays.
* Added unit tests for ReadExpr::create() to check that constant folding is correctly applied
* Added pre/post conditions as assertions
* Fixed assertion invocation: We were invoking bits64::truncateToNBits with a width greater than 64
* Refactoring code to improve readability by using UINT32/64_C macros
* Fix linker compatibility under macOS
* Increased the type size for the stop-after-n-instructions option to avoid too strict limitations (LLVM >= 3.0)
* Silenced warning: comparison of integers of different signs ('const int' and 'const unsigned long long')
* Add test case that causes an assertion failure in `klee::getDirectCallTarget(llvm::CallSite)`.
* Teach `klee::getDirectCallTarget()` to resolve weak aliases. This is 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.
* [TravisCI] Fix bug where TravisCI build scripts would carry on executing even though configure/build failed. This due to using the `&&` operator which means failure of commands to execute in this compound statement will not trigger the script to exit as requested by `set -e`.
* [TravisCI] Remove `set +e` commands so that when running tests we fail fast rather than continuing to run the tests (due to `set -e` at the beginning of the script).
* [TravisCI] When building with the old build system move back to the root of the build tree after doing the hack the generate the lit configuration files.
* CMake: Fixed the LLVM version regex
* [CMake] Fix linker warning about mixed linking modes when LLVM was built with `-fvisibility-inlines-hidden`.
* Fix -Wformat warnings emitted by Apple Clang (800.0.42.1).
* rerun lit tests for non-default metaSMT backends
* Changed preferred permissions from 0622 to the more standard 0644.
* Fix two issues with AC_LINK_IFELSE for metaSMT:
* tests: Added substitution for llvm-ar
* Write tests to test `libkleeRuntest`. The `replay_posix_runtime.c` test is marked XFAIL because there is a bug in the implementation of `libkleeRuntest`.
* Fix bug reported privately by @danielschemmel .
* Change how error handling is done in libkleeRuntest.
* [CMake] Rename "integrationtests" to "systemtests".
* Rename old build system targets so that
* Remove undocumented and unused `check-local`, `check-dg` and `check-lit` targets from Autoconf/Makefile build system. Having these around just confuses things.
* [CMake] Only add dependencies to `check` if the target is enabled.
* [CMake] If CMP0037 policy is available set it to NEW so that we disallow using reserved target names.
* Fixing current version of STP in Dockerfile (see #505) to 2.1.2
* Switched to STP 2.1.2 on Travis CI builds
* Increasing version to 1.3.0
* Release notes for 1.3.0
* Remove support for reporting the approximate git tag.
* Added among the external calls that we model
* CMake: support LLVMCC.ExtraFlags
* Fixed the issue of klee-stats not being copied to bin/
* [TravisCI] Fix the list of available configuration environment variables.
* [TravisCI] Clean up the configuration matrix.
* [CMake] Fix bug in the Makefile bitcode build system where the runtime would not recompile if the LLVM C compiler flags changed. This could happen if the user did something like
* [CMake] Fix bug in the Makefile bitcode build system where the runtime would not recompile if the `Makefile.cmake.bitcode.rules` file changed.
* [CMake] Fix bug where if KLEE was built with `ENABLE_TCMALLOC` and then re-configured with `ENABLE_TCMALLOC` set to OFF then `klee/Config/config.h` was not correctly re-generated.
* [CMake] Add missing dependencies reported in #507.
* [CMake] Fix link order of LLVM libraries and required system libraries.
* [CMake] Add another missing LLVM component dependency for `kleeModule`.
* [CMake] Fix determining the system libraries needed by LLVM from `llvm-config` when using LLVM 3.5 and newer.
* [CMake] Fix bug where the wrong path is checked for when checking to see if we can find klee-uclibc's C library.
* [CMake] Fix some indentation issues.
* Renamed .pc to .kquery (kleaver query)
* Fix bug in implementation of `NotExpr`. It should not implement `compareContents()`.
* Remove default implementation of `Expr::compareContents(const Expr&)` and make it a pure virtual method. Also make it protected rather than public because it is an implementation detail of `Expr::compare()`.
* add nicer error messages for --use-merge and add explanation why it currently cannot be used with random-path
* Fix BFS searcher
* [CMake] Re-express LLVM and KLEE library dependencies as transitive dependencies on KLEE's libraries rather than on the final binaries. This is better because it means we can build other tools that use KLEE's libraries and not need to express the needed LLVM dependencies.
* [CMake] Remove use of tabs in `CMakeLists.txt` files.
* [CMake] Document implicit `STP_DIR` and `metaSMT_DIR` options.
* Documented the level at which BFS operates in KLEE, as part of --help
* Remove option --randomize-fork. If someone needs this, the right way is to implement it in the solver.
* [CMake] Remove unneeded dependency declarations for the unit tests. These were changes that I forgot to make in dda296e09ee53ed85ccf1c3f08e7e809adce612e .
* [CMake] Fix the old Autoconf/Makefile build system files in source tree interfering with CMake build.
* remove mimic_stp option and the associated ITE chain construction for shift operators
* When building KLEE with the sanitizers make sure the runtime is not built with them because KLEE can't handle this.
* Use newer trusty-based Travis CI (#452)
* Fix `-Wmisleading-indentation` warning and also correctly set the `dirty` flag if we remove `llvm.trap` from the module.
* remove outdated FIXME (metaSMT-Z3 implements assumption via push/pop)
* change signature of runAndGetCex() to match runAndGetCexForked()
* move the query creation part into runAndGetCex() (to be consistent with runAndGetCexForked())
* upgrade to boolector-2.2.0 & remove the no longer needed aux array vector
* update comments
* apply clang-format
* Adds support for Darwin platform in RaiseAsm pass
* Implement a CMake based build system for KLEE.
* Add the Dockerfile to `.dockerignore` so that changes the Dockerfile don't trigger unnecessary rebuilds. Also make the Dockerfile ignore Vim source files anywhere in the tree.
* [CMake] Report git revision information if available.
* Check the existence of the entry point during the initialization of the POSIX runtime. If the check fails, exit with an error. (#457)
* Clang-format ``ConstructSolverChain.cpp``
* Add ``-debug-cross-check-core-solver`` option to allow cross-checking with another solver. For example the core solver can be STP and the cross checking solver can be Z3.
* Correct out of date comments for some of the klee error handling functions.
* Rename `-debug-cross-check-core-solver` option to `-debug-crosscheck-core-solver` as requested by Cristian
* Avoid internalization of non-standard entry point (i.e. not the main function) (#455)
* Modified logging information to steer the usage of klee_message, klee_warning, and klee_error
