diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-11-05 09:01:03 -0800 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-11-05 09:01:03 -0800 |
commit | 52ee910c128e6bbcf7299a0660511deacadb14f1 (patch) | |
tree | 89a05c005d82e660cdd626441740c719536ea9d6 /test | |
parent | 4d65e4b5efecc631bfda19900327cd5da2d740f7 (diff) |
API: Fix assignment operators (#2680)
The assignment operators of `Term`, `OpTerm`, and `Sort` currently have
an issue. The operators dereference their `shared_ptr` member and assign
the corresponding member of the other object. This is problematic
because if we have for example two `Term`s pointing to the same `Expr`,
then the assignment changes both `Term`s even though we only assign to
one, which is not what we want (see the unit test in this commit for a
concrete example of the desired behavior). To fix the issue, the
assignment operator should just copy the pointer of the other object.
This happens to be the behavior of the default assignment operator, so
this commit simply removes the overloaded assignment operators.
Testing: I did `make check` with an ASAN build and no errors other than
the one fixed in #2607 were reported.
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/api/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/unit/api/term_black.h | 37 |
2 files changed, 38 insertions, 0 deletions
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index 90d34f7c6..025575e41 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -2,3 +2,4 @@ # Add unit tests cvc4_add_unit_test_black(api_guards_black api) +cvc4_add_unit_test_black(term_black api) diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h new file mode 100644 index 000000000..c2ca1cb08 --- /dev/null +++ b/test/unit/api/term_black.h @@ -0,0 +1,37 @@ +/********************* */ +/*! \file term_black.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Black box testing of the Term class + **/ + +#include <cxxtest/TestSuite.h> + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +class TermBlack : public CxxTest::TestSuite +{ + public: + void setUp() override {} + void tearDown() override {} + + void testTermAssignment() + { + Term t1 = d_solver.mkReal(1); + Term t2 = t1; + t2 = d_solver.mkReal(2); + TS_ASSERT_EQUALS(t1, d_solver.mkReal(1)); + } + + private: + Solver d_solver; +}; |