about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2014-09-12Do not require <sys/capability.h>, which is Linux specific.Daniel Dunbar
2014-09-12Regenerate configure with sanctioned autoconf version.Daniel Dunbar
2014-09-12Revert "Patch by Dan Liew: "Improved AutoRegen script so that it supports ↵Daniel Dunbar
newer versions of autoconf"" The entire point of this version check in this script is so that configure is only generated with one exact version of autotools, so that it doesn't get spurious diffs from people generating it with different versions. This is the approach used by LLVM, and I'd like to stick to it. Most people don't regenerate these files, so it falls on the people who do to install the appropriate versions of the tools. If we want to change this policy, we should just drop the version checks completely.
2014-07-21Merge pull request #113 from antiAgainst/klee-statsCristian Cadar
klee-stats refactoring and improvement by antiAgainst: "this includes changing from OptionParser to ArgumentParser, rewriting not-pythonic code, respecting PEP8, etc; Adding line chart drawing in klee-stats."
2014-07-18Refactor klee-stats and add simple line chart drawing functionality.Lei Zhang
2014-07-10Merge pull request #137 from MartinNowack/fix_cxx_standardCristian Cadar
Fix to avoid warning message taking address of main
2014-07-09Fix to avoid warning message taking address of mainMartin Nowack
2014-07-04Merge pull request #133 from delcypher/fix_empty_error_reportCristian Cadar
Fix regression reported by Michael Esser and Andrew Watson
2014-07-04Fix regression reported by Michael Esser and Andrew WatsonDan Liew
(independently). In our recently switch to llvm::raw_ostream (and friends) (I think this is d934d983692c8952cdb887cbcd59f2df0001b9c0) we forgot to flush the llvm::raw_string_ostream to the underlying string used for error report files (e.g. test000001.overshift.err) so we would end up writing an empty string to error report files. Also added a test case to catch this.
2014-06-06Merge pull request #129 from ahorn/masterCristian Cadar
Add SimplifyExpressions command line option
2014-05-30Merge pull request #117 from MartinNowack/llvm_raw_ostreamMartinNowack
Refactor std::ostreams to llvm::raw_ostream and minor cleanups
2014-05-30Fix ExprTest under LLVM 2.9Martin Nowack
2014-05-29Use LLVM DEBUG macro instead of #if 0 or #if DEBUGMartin Nowack
2014-05-29Fix headerMartin Nowack
2014-05-29Avoid non-explicit use of functions from std namespace in KLEEMartin Nowack
2014-05-29Remove #include <iostream> to avoid static constructorsMartin Nowack
iostream injects static constructor function into every compilation unit. Remove this to avoid it.
2014-05-29Refactoring from std::ostream to llvm::raw_ostreamMartin Nowack
According to LLVM: lightweight and simpler implementation of streams.
2014-05-19Rename command line option for equality substitutionsahorn
2014-05-16Changed StaticDestructor.cpp to use uclibc and disable optimizations explicitly.Cristian Cadar
2014-05-13Merge pull request #131 from haneefmubarak/patch-1Cristian Cadar
Update and rename README.txt to README.md
2014-05-12Update and rename README.txt to README.mdHaneef Mubarak
Make it look nicer! :smile:
2014-05-12Merge pull request #124 from pcc/sortDan Liew
Fix the logic in ExprSMTLIBPrinter::getSort
2014-05-12Add SimplifyExpressions command line optionahorn
Allow users to bypass ConstraintManager::simplifyExpr(ref<Expr>).
2014-05-11Fix the logic in ExprSMTLIBPrinter::getSortPeter Collingbourne
This now corresponds to the sorts of the operations we emit, as far as I can tell. Read is one example of an operation that now works correctly (with 1-bit array ranges). It's also possible (but not very useful, and I don't think KLEE can produce it) for other operations such as Add to operate on 1-bit values, and this patch also fixes those.
2014-04-24Merge pull request #122 from hpalikareva/metasmt-array-orderDan Liew
Fixed order of domain and range in array creation in MetaSMTBuilder.
2014-04-24Fixed order of domain and range in array creation in MetaSMTBuilder.Hristina Palikareva
2014-04-24Merge pull request #121 from hpalikareva/domain-range-metasmtDan Liew
Fixed creation of arrays with variable domains and ranges in STPBuilder ...
2014-04-24Fixed creation of arrays with variable domains and ranges in STPBuilder and ↵Hristina Palikareva
MetaSMTBuilder.
2014-04-24Merge pull request #116 from MartinNowack/fix_mallocDan Liew
Fix handling of memory usage in KLEE.
2014-04-24Merge pull request #120 from hpalikareva/order-link-libsDan Liew
Fixing linking order if metaSMT is used: linking rt after z3 to avoid un...
2014-04-24Removed ununsed Executor field in WeightedRandomSearcher to silenceDan Liew
clang warning.
2014-04-24Remove unused pointer to STPSolver in STPSolverImpl to silence clangDan Liew
warning.
2014-04-24Renamed GetTotalMemoryUsage to GetTotalMallocUsageMartin Nowack
2014-04-24Modify klee::util::GetTotalMemoryUsage() so that if the system isDan Liew
not using glibc the malloc usage if computed differently.
2014-04-24Have configure check for presense of mallinfo for the newly addedDan Liew
klee::util::GetTotalMemoryUsage()
2014-04-24Fix handling of memory usage in KLEE.Martin Nowack
Memory usage API in LLVM since 3.3 is not working the way it is intended by KLEE. This ports the pre 3.3. version to KLEE. Fixes the malloc test case.
2014-04-24Add missing newline at end of file to silence a clang warning.Dan Liew
2014-04-24Merge pull request #112 from hpalikareva/domain-range-extraDan Liew
Removing a few more hard-coded values for domains and ranges of Array ob...
2014-04-24Asserting that update lists have non-NULL roots within ReadExpr objects (updateHristina Palikareva
lists can have NULL roots, e.g. in MemoryObject instances with concrete contents, where root is allocated lazily only when the updates are required). Also checking whether array updates are typed correctly in UpdateList::extend() rather than in the constructor of UpdateNode (only for update lists with non-NULL roots).
2014-04-23Fixing linking order if metaSMT is used: linking rt after z3 to avoid ↵Hristina Palikareva
undefined symbols in the z3 library.
2014-04-16Removing a few more hard-coded values for domains and ranges of Array objectsHristina Palikareva
2014-04-16Merge pull request #111 from s-falke/no_uclibcDan Liew
Fixed compilation error if uClibc is not used.
2014-04-16Merge pull request #110 from pcc/domain-rangeDan Liew
Associate a domain and range with each array
2014-04-16Fixed compilation error if uClibc is not used.Stephan Falke
2014-04-15Associate a domain and range with each arrayPeter Collingbourne
2014-04-15Merge pull request #104 from MartinNowack/llvm_34MartinNowack
Merge support for LLVM 3.4
2014-04-15Fix handling of path name creation.Martin Nowack
If directory has no trailing slash, the slash is not addedd if concatenated
2014-04-14Fix compilation under LLVM2.9. SmallString in this old version doesDan Liew
not have the equals() method.
2014-04-14fix TOCTOU and simplify output directory creationFrank Busse
2014-04-14Fix mistake in StatsTracker. It should be reporting process ID butDan Liew
instead it was reporting real user ID of the process.