Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-09-12 | Update .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-12 | Add a README for the Concrete tests. | Daniel Dunbar | |
2014-09-12 | Fix up ConstantExpr to be deterministic with 64-bit addresses. | Daniel Dunbar | |
2014-09-12 | Add support for testing Concrete tests via lit. | Daniel Dunbar | |
Fixes #96. | |||
2014-09-12 | Fix up Concrete Makefile to not remove outputs, so tests can run in parallel. | Daniel Dunbar | |
2014-09-12 | Rewrite ConcreteTest.py to only run one test at a time. | Daniel Dunbar | |
2014-09-12 | Update Concrete test Makefile for LLVM changes. | Daniel Dunbar | |
2014-09-12 | Update testingUtils to use printf(), putchar() isn't a known external ↵ | Daniel Dunbar | |
function anymore. | |||
2014-09-12 | Update FloatingPointOps concrete test case for LLVM changes. | Daniel Dunbar | |
2014-09-12 | XFAIL LargeReturnTypes.cpp on Darwin, it depends indirectly on using libstdcxx. | Daniel Dunbar | |
2014-09-12 | When 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-12 | Regenerate configure. | Daniel Dunbar | |
2014-09-12 | Tweak 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-12 | Add support for getting memory usage on Darwin. | Daniel Dunbar | |
2014-09-12 | Do not require mallinfo(), which is Linux specific. | Daniel Dunbar | |
2014-09-12 | Do not require <sys/capability.h>, which is Linux specific. | Daniel Dunbar | |
2014-09-12 | Regenerate configure with sanctioned autoconf version. | Daniel Dunbar | |
2014-09-12 | Revert "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-21 | Merge pull request #113 from antiAgainst/klee-stats | Cristian 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-18 | Refactor klee-stats and add simple line chart drawing functionality. | Lei Zhang | |
2014-07-10 | Merge pull request #137 from MartinNowack/fix_cxx_standard | Cristian Cadar | |
Fix to avoid warning message taking address of main | |||
2014-07-09 | Fix to avoid warning message taking address of main | Martin Nowack | |
2014-07-04 | Merge pull request #133 from delcypher/fix_empty_error_report | Cristian Cadar | |
Fix regression reported by Michael Esser and Andrew Watson | |||
2014-07-04 | Fix regression reported by Michael Esser and Andrew Watson | Dan 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-06 | Merge pull request #129 from ahorn/master | Cristian Cadar | |
Add SimplifyExpressions command line option | |||
2014-05-30 | Merge pull request #117 from MartinNowack/llvm_raw_ostream | MartinNowack | |
Refactor std::ostreams to llvm::raw_ostream and minor cleanups | |||
2014-05-30 | Fix ExprTest under LLVM 2.9 | Martin Nowack | |
2014-05-29 | Use LLVM DEBUG macro instead of #if 0 or #if DEBUG | Martin Nowack | |
2014-05-29 | Fix header | Martin Nowack | |
2014-05-29 | Avoid non-explicit use of functions from std namespace in KLEE | Martin Nowack | |
2014-05-29 | Remove #include <iostream> to avoid static constructors | Martin Nowack | |
iostream injects static constructor function into every compilation unit. Remove this to avoid it. | |||
2014-05-29 | Refactoring from std::ostream to llvm::raw_ostream | Martin Nowack | |
According to LLVM: lightweight and simpler implementation of streams. | |||
2014-05-19 | Rename command line option for equality substitutions | ahorn | |
2014-05-16 | Changed StaticDestructor.cpp to use uclibc and disable optimizations explicitly. | Cristian Cadar | |
2014-05-13 | Merge pull request #131 from haneefmubarak/patch-1 | Cristian Cadar | |
Update and rename README.txt to README.md | |||
2014-05-12 | Update and rename README.txt to README.md | Haneef Mubarak | |
Make it look nicer! :smile: | |||
2014-05-12 | Merge pull request #124 from pcc/sort | Dan Liew | |
Fix the logic in ExprSMTLIBPrinter::getSort | |||
2014-05-12 | Add SimplifyExpressions command line option | ahorn | |
Allow users to bypass ConstraintManager::simplifyExpr(ref<Expr>). | |||
2014-05-11 | Fix the logic in ExprSMTLIBPrinter::getSort | Peter 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-24 | Merge pull request #122 from hpalikareva/metasmt-array-order | Dan Liew | |
Fixed order of domain and range in array creation in MetaSMTBuilder. | |||
2014-04-24 | Fixed order of domain and range in array creation in MetaSMTBuilder. | Hristina Palikareva | |
2014-04-24 | Merge pull request #121 from hpalikareva/domain-range-metasmt | Dan Liew | |
Fixed creation of arrays with variable domains and ranges in STPBuilder ... | |||
2014-04-24 | Fixed creation of arrays with variable domains and ranges in STPBuilder and ↵ | Hristina Palikareva | |
MetaSMTBuilder. | |||
2014-04-24 | Merge pull request #116 from MartinNowack/fix_malloc | Dan Liew | |
Fix handling of memory usage in KLEE. | |||
2014-04-24 | Merge pull request #120 from hpalikareva/order-link-libs | Dan Liew | |
Fixing linking order if metaSMT is used: linking rt after z3 to avoid un... | |||
2014-04-24 | Removed ununsed Executor field in WeightedRandomSearcher to silence | Dan Liew | |
clang warning. |