about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2015-12-17Add LeakSanitizer (component of AddressSanitizer) suppression fileDan Liew
which is required to suppress all the leaks I'm currently seeing in KLEE when running ``make unittests`` and ``make check``. Ideally there should be no leaks but we aren't there yet. Hopefully at some point we won't need to suppress any leaks and then we can have a TravisCI build that builds with ASan. The leak of the expression objects when running the executor is worrying and I will investigate this next.
2015-12-16Propagate AddressSanitizer, LeakSanitizer (part of AddressSanitizer),Dan Liew
MemorySanitzer and ThreadSanitizer environment variables when running lit tests. This makes it easy suppress errors in sanitized versions of KLEE
2015-12-13Ignore some generated files that will be visible if doing an in sourceDan Liew
build. Spotted by @domainexpert
2015-12-13Ignore some autoconf generated files.Dan Liew
2015-12-13Set C++ standard in Clang format settings file to C++03. OtherwiseDan Liew
template braces get reformatted the C++11 way and that breaks compilation.
2015-12-11Reword help description for ``--silent-klee-assume`` command lineDan Liew
flag as suggested by @ccadar
2015-12-11Change SilentKleeAssume.c test slightly so thatDan Liew
``--silent-klee-assume=0`` is no longer passed. This ensures that we also check that ``--silent-klee-assume`` is off by default.
2015-12-11Add command line flag ``--silent-klee-assume``to suppress errors due toValentin Wüstholz
infeasible assumptions.
2015-12-04Remove dead ifdef in STPBuilder header file. There is noDan Liew
``stp/stplog.h`` header file in the current version of STP and no support in the build system for setting this define so this code is completly dead.
2015-12-04Remove dead ``tempVars`` and ``getTempVar()`` method in STPBuilderDan Liew
2015-12-04Merge pull request #310 from msoos/fix-klee-clang-script2MartinNowack
Fixing klee-clang to strip all flags not understood by llvm-link
2015-12-04Fixing klee-clang to strip all flags not understood by llvm-linkMate Soos
2015-12-02Merge pull request #309 from msoos/fixstrong3MartinNowack
Removing -fstack-protector-strong for clang <= 3.4
2015-12-02Removing -fstack-protector-strong for clang <= 3.4Mate Soos
It's not supported and breaks compilation. This affects in particular Debian Jessie and probably all derived distros, too
2015-11-13Added NEWS fileCristian Cadar
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