summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2018-11-05 09:01:03 -0800
committerAina Niemetz <aina.niemetz@gmail.com>2018-11-05 09:01:03 -0800
commit52ee910c128e6bbcf7299a0660511deacadb14f1 (patch)
tree89a05c005d82e660cdd626441740c719536ea9d6 /test
parent4d65e4b5efecc631bfda19900327cd5da2d740f7 (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.txt1
-rw-r--r--test/unit/api/term_black.h37
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;
+};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback