about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2015-11-13Moving to version 1.1.0Cristian Cadar
2015-11-08Merge pull request #269 from MartinNowack/fix_sremMartinNowack
[STPBuilder] Generate SRrem expressions correctly
2015-10-31Merge pull request #296 from delcypher/specify_klee_uclibc_versionDan Liew
Specify klee uclibc version
2015-10-30Make sure TravisCI does a few builds where it uses the developmentDan Liew
branch for klee-uclibc.
2015-10-30Teach TravisCI and the Docker build to use the taggedDan Liew
"klee_uclibc_v1.0.0" release of uclibc.
2015-10-08Fix accidently hardcoding of LLVM version in DockerfileDan Liew
2015-09-26Merge pull request #281 from andrewchi/futimesat-fixMartinNowack
Don't use /tmp for futimesat unit test
2015-09-25Don't use /tmp for futimesat unit testAndrew Chi
This causes problems on a shared machine where multiple users are running the KLEE unit tests.
2015-09-22[STPBuilder] Generate SRrem expressions correctlyMartin Nowack
The '%' operater in C is not Gauss Modulo but remainder operations. Using a negative number as right operand can result in a negative number. Fix appropriate SRem building Note: MetaSMTlib implementation doesn't have that bug.
2015-09-21Merge pull request #274 from MartinNowack/fix_sdiv_1Cristian Cadar
Fix signed division by constant 1/ -1
2015-09-18Merge pull request #275 from MartinNowack/fix_empty_constraints_indep_solverCristian Cadar
Allow to generate initial values for queries with empty constraint set.
2015-09-05Allow to generate initial values with empty constraint setMartin Nowack
2015-09-04Merge pull request #276 from MartinNowack/travis_updateCristian Cadar
Travis: Support KLEE with different STP versions, in particular 2.1.0; Disable r940
2015-08-31Delete old patches.Martin Nowack
Say farewell to r940.
2015-08-30Support KLEE with different STP versions; Disable r940Martin Nowack
Build STP version based on provided branch. Build current STP version 2.1.0 by default and test with master branch as well
2015-08-30Fix signed division by constant 1/ -1Martin Nowack
Division by constant divisor get optimized using shift and multiplication operations in STP builder. The used method cannot be applied for divisor 1 and -1. In that case use slow path.
2015-08-21Merge pull request #251 from ret2libc/entryFnParamCristian Cadar
Added option to specify a different entry point from main(). Remove some whitespaces.
2015-08-17Merge pull request #239 from yotann/masterCristian Cadar
Fix assertion failure in getDirectCallTarget
2015-08-14test: add Feature test for EntryPoint optionRiccardo Schirone
2015-08-14tools/klee: pass the entry function name as argumentRiccardo Schirone
2015-08-14tools/klee/main: remove whitespacesRiccardo Schirone
2015-08-13Merge pull request #271 from kren1/coverageInfoCristian Cadar
Added link in README.md to coverage information for KLEE's codebase
2015-08-10Added link to coverage informationunknown
2015-08-10Changed version to 1.0.0 v1.0.0 1.0.xCristian Cadar
2015-08-10Merge pull request #267 from ccadar/masterCristian Cadar
Enabling assertions by default for KLEE. While the instructions for …
2015-08-05Enabling assertions by default for KLEE. While the instructions for 2.9 ↵Cristian Cadar
explicitely requir assertions to be enabled, in 3.4 we ask users to use LLVM packages, which are built in Release mode. This was prompted by issue #246, where the bug would have resulted in an easier-to-debug assert failure.
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-29Fix assertion failure in getDirectCallTargetSean Bartell
It failed when the function being called is a bitcasted alias.
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