about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2014-09-12Update .gitignore.Daniel Dunbar
2014-09-12[tests] Rewrite MemoryLimit test to use larger allocations for "little" test ↵Daniel Dunbar
path. - Otherwise this test takes a long time just hammering on the allocator trying to get to the memory limit.
2014-09-12[tests] Dramatically scale back the forks limit for our ImmutableSet test.Daniel Dunbar
- This one test was taking about half the test time, and it definitely isn't worth that much value as a test. We probably should have some kind of long running tests infrastructure for things where we actually want to test KLEE on real programs.
2014-09-12[tests] Set --output-dir on all test runs, in support of running tests in ↵Daniel Dunbar
parallel. - It would be nice if there was an easier way to do this that didn't involve editing all of the tests (like running each test in its own directory), but this approach fixes #146 and doesn't involve changing 'lit' or writing a wrapper harness. My assumption is a lot of tests start are derived from another one, so hopefully following this convention won't be burdensome, and I updated 'make check' so that it will produce an error if any test runs klee without --output-dir (by checking for the existing of klee-last files). - This also helps with #147 but I still can't fully run tests in parallel (I start hitting STP errors).
2014-09-12[tests] Update ConcreteTest to use --output-dir.Daniel Dunbar
2014-09-12Add a README for the Concrete tests.Daniel Dunbar
2014-09-12Fix up ConstantExpr to be deterministic with 64-bit addresses.Daniel Dunbar
2014-09-12Add support for testing Concrete tests via lit.Daniel Dunbar
Fixes #96.
2014-09-12Fix up Concrete Makefile to not remove outputs, so tests can run in parallel.Daniel Dunbar
2014-09-12Rewrite ConcreteTest.py to only run one test at a time.Daniel Dunbar
2014-09-12Update Concrete test Makefile for LLVM changes.Daniel Dunbar
2014-09-12Update testingUtils to use printf(), putchar() isn't a known external ↵Daniel Dunbar
function anymore.
2014-09-12Update FloatingPointOps concrete test case for LLVM changes.Daniel Dunbar
2014-09-12XFAIL LargeReturnTypes.cpp on Darwin, it depends indirectly on using libstdcxx.Daniel Dunbar
2014-09-12When building against libc++ (vs libstdcxx), use standard ↵Daniel Dunbar
unordered_{map,set} includes. - I'm not sure what the status of libstdcxx's c++11 support is. It may be we can just move over to <unordered_map> everywhere, but I don't have a Linux test machine handy at the moment.
2014-09-12Regenerate configure.Daniel Dunbar
2014-09-12Tweak the workarounds for multiple definition of PACKAGE_* macros from ↵Daniel Dunbar
config.h files. - There seems to be a better solution for this by defining a macro prefix, per: http://www.gnu.org/software/autoconf-archive/ax_prefix_config_h.html but I have no experience with that and it looks like it might involve rewriting a bunch of our macro checks.
2014-09-12Add support for getting memory usage on Darwin.Daniel Dunbar
2014-09-12Do not require mallinfo(), which is Linux specific.Daniel Dunbar
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.