about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2015-08-03Merge pull request #198 from holycrap872/IndependentSolverGetInitialValuesCristian Cadar
New version of the get initial values functionality which makes use of the independent solver.
2015-08-03Merge pull request #243 from ccadar/masterCristian Cadar
Option --readable-posix-inputs used to turn on/off POSIX-related CEX preferences
2015-07-06Merge pull request #250 from holycrap872/DefaultOffCexSuperSetCristian Cadar
Added an option for the super-set check in CexCachingSolver -- off by default
2015-07-06Make the super-set check in CexCachingSolver default offEric Rizzi
The super-set check in the CexCachingSolver takes MUCH longer than the sub-set check. Upon closer inspection, the super-set check gets slower and slower as more counterexamples fill the UBTree. Pretty quickly, the cost of the super-set check becomes larger than the time required to simply bypass it and go to the Solver.
2015-06-17Merge pull request #245 from kren1/masterCristian Cadar
Added coverage of the KLEE codebase to Travis CI
2015-06-16added COVERAGE=0 to dockerfile, factored out coverage build flags to be only ↵Timotej Kapus
set when COVERAGE is, added the python server script to scripts
2015-06-15encrypted secrets with main klee repo keyTimotej
2015-06-15added zcov integration to travis CITimotej
2015-06-08Merge pull request #241 from holycrap872/NoPreferCexCristian Cadar
Make creation of human readable test cases optional rather than default
2015-06-03Merge branch 'holycrap872-NoPreferCex'Cristian Cadar
2015-06-03Added an option --readable-posix-inputs which is used to turn on/off the CEX ↵Cristian Cadar
preferences added in the POSIX model. Removed option --prefer-cex which controlled all CEX preferences.
2015-05-31Make use of prefer-cex optional rather than defaultEric Rizzi
Previously, default Klee would go through every byte in a test case and attempt to bound it to be between 0 and 127, making it human readable. While this may be useful when attempting to understand Klee, it also means that the time required to create large test suites was greatly increased. By making this behavior default off, unsuspecting users won't incur these additional costs.
2015-04-25Rename macroDan Liew
s/KLEE_INSTALL_LIB_DIR/KLEE_INSTALL_RUNTIME_DIR/ The new name is more accurrate.
2015-04-25During install, install the klee intrinsic header file which isDan Liew
intended for public use.
2015-04-25Do not install gen-random-bout.Dan Liew
2015-04-25Change install location of KLEE's bytecode runtime librariesDan Liew
to ``${PREFIX}/lib/klee/runtime``. This addresses issue #233
2015-04-25Clean up the installation/building of the runtime libraries.Dan Liew
* We don't need to build the native versions so that is now disabled * We don't need to install (and hence build) the bytecode archive library versions of klee-libc or kleeRuntimeIntrinsic for new versions of LLVM right now (this is kind of messy).
2015-04-25Report the git tag if exists in the output of --version from kleeDan Liew
and kleaver.
2015-04-25Give KLEE release version information in the output of klee and kleaverDan Liew
when they are given the --version command line option. Unfortunately to make the build type and git revision available we need to check this for every build which means KLEE's support library will be rebuilt for every build which will slow down incremental builds. This addresses issue #231
2015-04-25Remove some dead makefile variables left over from the old testingDan Liew
system.
2015-04-25Remove dead STP logging code.Dan Liew
2015-04-25Make sure TravisCI tests at least one Debug+Asserts build.Dan Liew
2015-04-25Remove boost requirements from TravisCI build.Dan Liew
2015-04-19Fixed RewriteEqualities input to be more resilient to differences in ↵Cristian Cadar
compilation.
2015-04-19Temportily marking RewriteEqualities test as XFAIL.Cristian Cadar
2015-04-19Added a new test case that checks the --rewrite-equalities optimisation. ↵Cristian Cadar
The test contains the program proposed by Eric Rizzi in https://github.com/klee/klee/issues/227, and shows a case in which a constant constraint results after the optimisation.
2015-04-18Merge pull request #213 from MartinNowack/klee-clangCristian Cadar
Add klee-clang as alternative to klee-gcc
2015-04-15Add clang-format style. We just use LLVM's style.Dan Liew
2015-04-15Fix the handling of AShrExpr in ExprSMTLIBPrinter so that an overshiftDan Liew
always goes to zero (matches LLVM's APInt::ashr(...)). This is meant to partially address issue #218. There are a few problems with this commit * It is possible for AShrExpr to not be abbreviated because the scan methods will not see that we print the 0th child of the AShrExpr twice * The added test case should really be run through an SMT solver ( i.e. STP) but that requires infrastructure changes.
2015-04-10The Docker image had python2 and python3 which is a waste of spaceDan Liew
(I'm not sure where python3 came from. I didn't explicitly install it). Just ship python3.
2015-04-10Don't upgrade pip or setuptools. Upgrading pip breaks the build becauseDan Liew
/usr/local/bin/ isn't in PATH so using pip after upgrading it fails.
2015-04-10Add missing slash in last commit.Dan Liew
2015-04-10Update DockerfileDavid Leon Gil
klee-stats requires tabulate to be installed.
2015-04-09Add initial Dockerfile for building a KLEE Docker image (uses LLVM3.4).Dan Liew
This is is tightly coupled with the TravisCI scripts. There are some really nasty hacks in here that we should get rid of at some point.
2015-04-09Try to fix using the compiler KLEE's configure script detected again!Dan Liew
My first attempt in b41cf33b6b726fd97e502c5c4818f5feeea0284b was wrong because setting the CC and CXX Makefile variables in Makefile.config.in did not work because LLVM's Makefile.config would override them. Also detecting the C compiler is unnecessary because we already do this (bitcode compiler detection)
2015-04-09Normalised line endingsCristian Cadar
2015-04-09Added .gitattribute file that takes care of line endings.Cristian Cadar
2015-04-09Fix mistake if TravisCI scripts where configure flag for enabling POSIXDan Liew
runtime was incorrect.
2015-04-09Added a new option, --rewrite-equalities, which makes it possible to disable ↵Cristian Cadar
the optimisation that rewrites existing constraints when an equality with a constant is added
2015-04-09Switch to using STP's fork of minisat for TravisCI. It contains fixesDan Liew
needed by Clang.
2015-04-08Fix very annoying issue where KLEE's configure would completlyDan Liew
ignore the C++ compiler detected and just use the compiler detected during the LLVM configure.
2015-04-03Upstream STP now depends on an external build of minisat. Attempt toDan Liew
fix travis build of upstream STP and also how KLEE links against STP.
2015-04-03Fixed issue introduce during a previous refactoring, related to field ordering.Cristian Cadar
2015-04-02Use C instead of C++ comments in C files to silence compiler warnings.Cristian Cadar
2015-04-02Silenced some compilation warnings.Cristian Cadar
2015-04-02Merge pull request #209 from erakadjiev/timestamp_optimizeCristian Cadar
Cleaner, more efficient timestamps
2015-04-02Revert "[include] Added documentation" to avoid a conflict with a pending ↵Cristian Cadar
pull request. This reverts commit badffc570e1be6b675dcab7e21829bd029c46287.
2015-04-02Fixed some doxygen issues.Cristian Cadar
2015-04-02Removed unused fakeState field from ExecutionStateCristian Cadar
2015-04-02Pass over the comments in ExecutionState.hCristian Cadar