| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | 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-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-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-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 | Fixed order of domain and range in array creation in MetaSMTBuilder. | Hristina Palikareva | |
| 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 | Removed ununsed Executor field in WeightedRandomSearcher to silence | Dan Liew | |
| clang warning. | |||
| 2014-04-24 | Remove unused pointer to STPSolver in STPSolverImpl to silence clang | Dan Liew | |
| warning. | |||
| 2014-04-24 | Renamed GetTotalMemoryUsage to GetTotalMallocUsage | Martin Nowack | |
| 2014-04-24 | Modify klee::util::GetTotalMemoryUsage() so that if the system is | Dan Liew | |
| not using glibc the malloc usage if computed differently. | |||
| 2014-04-24 | Fix 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-24 | Asserting that update lists have non-NULL roots within ReadExpr objects (update | Hristina 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-16 | Removing a few more hard-coded values for domains and ranges of Array objects | Hristina Palikareva | |
| 2014-04-15 | Associate a domain and range with each array | Peter Collingbourne | |
| 2014-04-14 | Fix mistake in StatsTracker. It should be reporting process ID but | Dan Liew | |
| instead it was reporting real user ID of the process. | |||
| 2014-04-14 | Replace sys::Process::GetCurrentUserId() with getuid() because it | Dan Liew | |
| has been removed in LLVM3.4 | |||
| 2014-04-14 | Do not add SimplifyLibCallsPass for LLVM 3.4 and newer because | Dan Liew | |
| it has been removed. From the LLVM 3.4 release notes: " The library call simplification pass has been removed. Its functionality has been integrated into the instruction combiner and function attribute marking passes. " | |||
| 2014-04-14 | Tidy up code by using LLVM's V2 path API only and removing uses | Dan Liew | |
| of old V1 path API. LLVM2.9 supports LLVM's V2 path API. Because that is the minimum version we support we should just use this API everywhere so we reduce the number of #if LLVM_VERSION_CODE macros and duplicated code. | |||
| 2014-04-14 | Add missing include file for LLVM 3.4 | Martin Nowack | |
| 2014-04-14 | Use SmallString and llvm::sys::path/fs API of LLVM 3.4 because | Martin Nowack | |
| Old Path API was removed | |||
| 2014-04-04 | Add the ability to control whether the pretty printer uses line breaks | Peter Collingbourne | |
| This change makes it possible to more reliably write unit tests which check that an expression is equivalent to an expected pretty printed string. | |||
| 2014-04-02 | Modify the SMT-LIB printer to declare arrays in a deterministic ↵ | Peter Collingbourne | |
| (alphabetical) order. | |||
| 2014-03-09 | Use clang-format to reformat SMT-LIB printer in LLVM style. | Peter Collingbourne | |
| 2014-02-24 | Improved help message for make-concrete-symbolic and fixed some typos. | Cristian Cadar | |
| 2014-02-14 | Explicitly get the width of the "shift" expression rather than assuming | Dan Liew | |
| that is the samw width of the "expr" expression. It probably is the same width (it defintely is in SMT-LIB but I'm not sure about STP) but it is probably better to be explicit. | |||
| 2014-02-14 | Remove STPBuilder::getShiftBits() which is no longer used. | Dan Liew | |
| 2014-02-14 | Fixed overshift of arithmetic right shift by constant so that it | Dan Liew | |
| overshifts to zero. Test case is included. | |||
| 2014-02-14 | Fixed overshift of arithmetic right shift by symbolic so that it overshifts | Dan Liew | |
| to zero. Test case is included. | |||
| 2014-02-14 | Fixed overshift of logical right shift by constant so that it | Dan Liew | |
| overshifts to zero. Test case is included. | |||
| 2014-02-14 | Fixed overshift of logical right shift by symbolic so that it overshifts | Dan Liew | |
| to zero. Test case is included. | |||
| 2014-02-14 | Fixed overshifting an expression by a constant so that we overshift to | Dan Liew | |
| zero. A test case was added for this. In addition the use to vc_bvExtract() was removed for shifting left by an expression because we don't want/need bitmasked behaviour anymore. | |||
| 2014-02-14 | Added a test case for testing overshift behaviour of Shl and fixed | Dan Liew | |
| a bug in the previous commit where 32-bit width was assumed. | |||
| 2014-02-14 | Translate shl overshifts into 0 | Paul Marinescu | |
| The other shift operators still need to be changed | |||
| 2014-02-14 | When running with -debug-only=klee_linker do not report the number | Dan Liew | |
| of modules left because this information is no longer correct (we no longer shrink the vector). | |||
| 2014-02-14 | Refactor cleaning up memory in linkBCA() so that if linking fails | Dan Liew | |
| then clean up is performed. | |||
| 2014-02-14 | Refactor variable name s/RemovedSymbols/SymbolsToRemove/ | Dan Liew | |
| because "RemovedSymbols" implies that the symbols have already been removed which is misleading because we don't remove until the end. | |||
| 2014-02-14 | Correct and tidy up comments. | Dan Liew | |
| 2014-02-06 | Fix access of iterators after they have been invalidated | Martin Nowack | |
| Iterators get invalidated after elements of std::vector/set are deleted. Avoid this by remembering which elements need to be deleted and do it after iterating over the data structure. | |||
| 2014-02-06 | When using KLEE's built-in Bitcode archive linker do not consider | Dan Liew | |
| KLEE intrinsics as undefined symbols | |||
 |
index : ~cnx/klee | |
| KLEE fork for patch differentiation testing |
| about summary refs log tree commit diff homepage |