GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/main/interactive_shell_black.cpp Lines: 58 58 100.0 %
Date: 2021-03-23 Branches: 56 124 45.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file interactive_shell_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Christopher L. Conway, Andrew Reynolds
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::InteractiveShell.
13
 **
14
 ** Black box testing of CVC4::InteractiveShell.
15
 **/
16
17
#include <sstream>
18
#include <vector>
19
20
#include "api/cvc4cpp.h"
21
#include "expr/symbol_manager.h"
22
#include "main/interactive_shell.h"
23
#include "options/base_options.h"
24
#include "options/language.h"
25
#include "options/options.h"
26
#include "parser/parser_builder.h"
27
#include "smt/command.h"
28
#include "test.h"
29
30
namespace CVC4 {
31
namespace test {
32
33
24
class TestMainBlackInteractiveShell : public TestInternal
34
{
35
 protected:
36
12
  void SetUp() override
37
  {
38
12
    TestInternal::SetUp();
39
24
    d_sin.reset(new std::stringstream);
40
24
    d_sout.reset(new std::stringstream);
41
24
    d_options.set(options::in, d_sin.get());
42
24
    d_options.set(options::out, d_sout.get());
43
24
    d_options.set(options::inputLanguage, language::input::LANG_CVC4);
44
12
    d_solver.reset(new CVC4::api::Solver(&d_options));
45
12
    d_symman.reset(new SymbolManager(d_solver.get()));
46
12
  }
47
48
12
  void TearDown() override
49
  {
50
12
    d_sin.reset(nullptr);
51
12
    d_sout.reset(nullptr);
52
    // ensure that symbol manager is destroyed before solver
53
12
    d_symman.reset(nullptr);
54
12
    d_solver.reset(nullptr);
55
12
  }
56
57
  /**
58
   * Read up to maxCommands+1 from the shell and throw an assertion error if
59
   * it's fewer than minCommands and more than maxCommands.  Note that an
60
   * empty string followed by EOF may be returned as an empty command, and
61
   * not NULL (subsequent calls to readCommand() should return NULL). E.g.,
62
   * "CHECKSAT;\n" may return two commands: the CHECKSAT, followed by an
63
   * empty command, followed by NULL.
64
   */
65
12
  void countCommands(InteractiveShell& shell,
66
                     uint32_t minCommands,
67
                     uint32_t maxCommands)
68
  {
69
    Command* cmd;
70
12
    uint32_t n = 0;
71
40
    while (n <= maxCommands && (cmd = shell.readCommand()) != NULL)
72
    {
73
14
      ++n;
74
14
      delete cmd;
75
    }
76
12
    ASSERT_LE(n, maxCommands);
77
12
    ASSERT_GE(n, minCommands);
78
  }
79
80
  std::unique_ptr<std::stringstream> d_sin;
81
  std::unique_ptr<std::stringstream> d_sout;
82
  std::unique_ptr<SymbolManager> d_symman;
83
  std::unique_ptr<CVC4::api::Solver> d_solver;
84
  Options d_options;
85
};
86
87
15
TEST_F(TestMainBlackInteractiveShell, assert_true)
88
{
89
2
  *d_sin << "ASSERT TRUE;\n" << std::flush;
90
4
  InteractiveShell shell(d_solver.get(), d_symman.get());
91
2
  countCommands(shell, 1, 1);
92
2
}
93
94
15
TEST_F(TestMainBlackInteractiveShell, query_false)
95
{
96
2
  *d_sin << "QUERY FALSE;\n" << std::flush;
97
4
  InteractiveShell shell(d_solver.get(), d_symman.get());
98
2
  countCommands(shell, 1, 1);
99
2
}
100
101
15
TEST_F(TestMainBlackInteractiveShell, def_use1)
102
{
103
4
  InteractiveShell shell(d_solver.get(), d_symman.get());
104
2
  *d_sin << "x : REAL; ASSERT x > 0;\n" << std::flush;
105
  /* readCommand may return a sequence, so we can't say for sure
106
     whether it will return 1 or 2... */
107
2
  countCommands(shell, 1, 2);
108
2
}
109
110
15
TEST_F(TestMainBlackInteractiveShell, def_use2)
111
{
112
4
  InteractiveShell shell(d_solver.get(), d_symman.get());
113
  /* readCommand may return a sequence, see above. */
114
2
  *d_sin << "x : REAL;\n" << std::flush;
115
2
  Command* tmp = shell.readCommand();
116
2
  *d_sin << "ASSERT x > 0;\n" << std::flush;
117
2
  countCommands(shell, 1, 1);
118
2
  delete tmp;
119
2
}
120
121
15
TEST_F(TestMainBlackInteractiveShell, empty_line)
122
{
123
4
  InteractiveShell shell(d_solver.get(), d_symman.get());
124
2
  *d_sin << std::flush;
125
2
  countCommands(shell, 0, 0);
126
2
}
127
128
15
TEST_F(TestMainBlackInteractiveShell, repeated_empty_lines)
129
{
130
2
  *d_sin << "\n\n\n";
131
4
  InteractiveShell shell(d_solver.get(), d_symman.get());
132
  /* Might return up to four empties, might return nothing */
133
2
  countCommands(shell, 0, 3);
134
2
}
135
}  // namespace test
136
57
}  // namespace CVC4