about summary refs log tree commit diff homepage
path: root/unittests
AgeCommit message (Collapse)Author
2015-12-18Fix memory leaks of ``Array`` objects detected by ASan.Dan Liew
Some of these leaks were introduced by the factory constructor for Array objects (f049ff3bc04daead8c3bb9f06e89e71e2054c82a) but a few others have been around for far longer. This leak was fixed by introducing a ``ArrayCache`` object which has two purposes * Retains ownership of all created ``Array`` objects and destroys them when the ``ArrayCache`` destructor is called. * Mimic the caching behaviour for symbolic arrays that was introduced by f049ff3bc04daead8c3bb9f06e89e71e2054c82a where arrays with the same name and size get "uniqued". The Executor now maintains a ``arrayCache`` member that it uses and passes by pointer to objects that need to construct ``Array`` objects (i.e. ``ObjectState``). This way when the Executor is destroyed all the ``Array`` objects get freed which seems like the right time to do this. For Kleaver the ``ParserImpl`` has a ``TheArrayCache`` member that is used for building ``Array`` objects. This means that the Parser must live as long as the built expressions will be used otherwise we will have a use after free. I'm not sure this is the right design choice. It might be better to transfer ownership of the ``Array`` objects to the root ``Decl`` returned by the parser.
2015-04-03Upstream STP now depends on an external build of minisat. Attempt toDan Liew
fix travis build of upstream STP and also how KLEE links against STP.
2015-02-22Added factory method for Arrays + hid constructors from outside callsEric Rizzi
The way that Arrays were handled in the past led to the possibility of aliasing issues. This occured whenever a new branch discovered an array for the first time. Each branch would create a new instance of the same array without seeing if it had been created before. Therefore, should a new branch encounter the same state as some previous branch, the previous branch's solution wouldn't satisfy the new state since they didn't recognize they were referencing the same array. By creating an array factory that creates a single symbolic array, that problem is handled. Note: Concrete arrays should not be created by the factory method since their values are never shared between branches. The factory works by seeing if an array with a similar hash has been created before (the hash is based on the name and size of array). If there has been it then searches through all of the arrays with the same hash (stored in a vector) to see if there is one with an exact match. If there is one, the address of this previously created equivalent array is returned. Otherwise, the newly created array is unique, it is added to the map, and it's address is returned. This aliasing issue can be seen by comparing the output of the Dogfood/ImmutableSet.cpp test cases with and with out this commit. Both act correctly, but the number of queries making it to the solver in the previous version is much greater 244 vs 211. This is because the UBTree in the CexCachingSolver and the cache in the CachingSolver do not recognize queries whose solutions were previously calculated because it doesn't think the arrays in the two queries are the same. While this does not cause an error, it does mean that extra calls are made.
2014-11-01Upstream libstp is no longer dependent on Boost so remove theDan Liew
configure/Makefile code that adds Boost as a depdendency because We don't need to support old versions of STP that needed Boost.
2014-05-30Fix ExprTest under LLVM 2.9Martin Nowack
2014-02-12Fixed compilation of unittests with upstream STP (Boost dependency).Dan Liew
2013-12-21Fixed mistake in commit c5510caa2a0ce6ad9a153fee094fe50855313450Dan Liew
( Fix compilation of unittests under Clang )
2013-12-20Fix compilation of unittests under Clang.Dan Liew
It seems the GTest header file in LLVM 3.3 (and possibly other versions) makes use of typeid() but the build system passes -fno-rtti. These are incompatible and if building with Clang then compilation will fail. GCC doesn't seem to care!
2013-08-21Remove unnecessary loop from SolverTest unit test.Dan Liew
2013-07-23BFS searcher.Lei Zhang
2013-03-11Small patch by Dan Liew removing unnecessary line from a Makefile.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@176816 91177308-0d34-0410-b5e6-96231b3b80d8
2012-07-31Patch by Dan Liew that removes our internal copy of STP, and makes the ↵Cristian Cadar
--with-stp option mandatory: "1. At configure time the --with-stp= option is now mandatory. 2. The HAVE_EXT_STP macro has been removed. 3. The ENABLE_EXT_STP autoconf replacement variable has been removed and consequently the Makefile variable of the same name has been removed." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@161055 91177308-0d34-0410-b5e6-96231b3b80d8
2012-04-07Patch by Seungbeom that fixes a memory management issue with Refs, andCristian Cadar
associated unit test. More details at http://keeda.stanford.edu/pipermail/klee-commits/2012-February/000904.html git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154256 91177308-0d34-0410-b5e6-96231b3b80d8
2012-04-07Fix unittests build when using external STP.Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154236 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-29Fixed compilation of unit tests.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102611 91177308-0d34-0410-b5e6-96231b3b80d8
2009-09-01Update for LLVM ostream changes.Daniel Dunbar
- Includes patch by Michael Stone! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@80665 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Remove Array::object.Daniel Dunbar
- The sole remaining client was IVC, which is currently disabled for other correctness issues. I patched it to compile and left a FIXME that we will have to resolve this before we can reenable IVC. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73129 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Remove Array::id.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73128 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Switch Array* print-outs to use name instead of ID, and update a fewDaniel Dunbar
constructors I missed. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73127 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Change ConstantExpr::{alloc,create} to return a ref<ConstantExpr>Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72853 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Use dyn_cast<> instead of dyn_ref_cast.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72847 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-03Kill off specialized ref<> forwarding methods, in the interest of making it aDaniel Dunbar
more standard reference counting wrapper. - The only interesting changes here are in Ref.h, everything else is just updating foo.method to use foo->method instead. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72777 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-02Use ConstantExpr::alloc instead of ref<Expr> directlyDaniel Dunbar
- The "constant optimization" embedded inside ref<Expr> is going away. - No functionality change. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72730 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-21Initial KLEE checkin.Daniel Dunbar
- Lots more tweaks, documentation, and web page content is needed, but this should compile & work on OS X & Linux. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8