GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/util/array_store_all_white.cpp Lines: 31 31 100.0 %
Date: 2021-03-22 Branches: 108 264 40.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file array_store_all_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Black box testing of CVC4::ArrayStoreAll
13
 **
14
 ** Black box testing of CVC4::ArrayStoreAll.
15
 **/
16
17
#include "expr/array_store_all.h"
18
#include "test_smt.h"
19
20
namespace CVC4 {
21
namespace test {
22
23
12
class TestUtilWhiteArrayStoreAll : public TestSmt
24
{
25
};
26
27
12
TEST_F(TestUtilWhiteArrayStoreAll, store_all)
28
{
29
4
  TypeNode usort = d_nodeManager->mkSort("U");
30
4
  ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(),
31
4
                                           d_nodeManager->realType()),
32
4
                d_nodeManager->mkConst(Rational(9, 2)));
33
2
  ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkSort("U"), usort),
34
4
                d_nodeManager->mkConst(UninterpretedConstant(usort, 0)));
35
4
  ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8),
36
4
                                           d_nodeManager->realType()),
37
4
                d_nodeManager->mkConst(Rational(0)));
38
4
  ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8),
39
4
                                           d_nodeManager->integerType()),
40
4
                d_nodeManager->mkConst(Rational(0)));
41
2
}
42
43
12
TEST_F(TestUtilWhiteArrayStoreAll, type_errors)
44
{
45
4
  ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(),
46
                             d_nodeManager->mkConst(UninterpretedConstant(
47
                                 d_nodeManager->mkSort("U"), 0))),
48
2
               IllegalArgumentException);
49
4
  ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(),
50
                             d_nodeManager->mkConst(Rational(9, 2))),
51
2
               IllegalArgumentException);
52
4
  ASSERT_THROW(
53
      ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(),
54
                                               d_nodeManager->mkSort("U")),
55
                    d_nodeManager->mkConst(Rational(9, 2))),
56
2
      IllegalArgumentException);
57
}
58
59
12
TEST_F(TestUtilWhiteArrayStoreAll, const_error)
60
{
61
4
  TypeNode usort = d_nodeManager->mkSort("U");
62
4
  ASSERT_THROW(ArrayStoreAll(d_nodeManager->mkArrayType(
63
                                 d_nodeManager->mkSort("U"), usort),
64
                             d_nodeManager->mkVar(usort)),
65
2
               IllegalArgumentException);
66
4
  ASSERT_THROW(
67
      ArrayStoreAll(d_nodeManager->integerType(),
68
                    d_nodeManager->mkVar("x", d_nodeManager->integerType())),
69
2
      IllegalArgumentException);
70
4
  ASSERT_THROW(
71
      ArrayStoreAll(d_nodeManager->integerType(),
72
                    d_nodeManager->mkNode(kind::PLUS,
73
                                          d_nodeManager->mkConst(Rational(1)),
74
                                          d_nodeManager->mkConst(Rational(0)))),
75
2
      IllegalArgumentException);
76
}
77
}  // namespace test
78
40814
}  // namespace CVC4