summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/main/Makefile.am7
-rw-r--r--src/main/interactive_shell.cpp41
-rw-r--r--test/unit/Makefile.am10
-rw-r--r--test/unit/main/interactive_shell_black.h115
4 files changed, 152 insertions, 21 deletions
diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 05a451d52..52a659322 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -4,8 +4,9 @@ AM_CPPFLAGS = \
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas
bin_PROGRAMS = cvc4
+noinst_LIBRARIES = libmain.a
-cvc4_SOURCES = \
+libmain_a_SOURCES = \
interactive_shell.h \
interactive_shell.cpp \
main.h \
@@ -13,10 +14,12 @@ cvc4_SOURCES = \
usage.h \
util.cpp
+cvc4_SOURCES =
cvc4_LDADD = \
../parser/libcvc4parser.la \
../libcvc4.la \
- ../lib/libreplacements.la
+ ../lib/libreplacements.la \
+ libmain.a
if STATIC_BINARY
cvc4_LINK = $(CXXLINK) -all-static
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 587c07495..8437d61b2 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -52,25 +52,15 @@ Command* InteractiveShell::readCommand() {
line = sb.str();
// cout << "Input was '" << input << "'" << endl << flush;
- /* If we hit EOF, we're done. */
- if( d_in.eof() ) {
- input += line;
- break;
- }
+ Assert( !(d_in.fail() && !d_in.eof()) || line.empty() );
- /* Check for failure */
- if( d_in.fail() ) {
+ /* Check for failure. */
+ if( d_in.fail() && !d_in.eof() ) {
/* This should only happen if the input line was empty. */
Assert( line.empty() );
d_in.clear();
}
- /* Extract the newline delimiter from the stream too */
- int c = d_in.get();
- Assert( c == '\n' );
-
- // cout << "Next char is '" << (char)c << "'" << endl << flush;
-
/* Strip trailing whitespace. */
int n = line.length() - 1;
while( !line.empty() && isspace(line[n]) ) {
@@ -78,12 +68,31 @@ Command* InteractiveShell::readCommand() {
n--;
}
+ /* If we hit EOF, we're done. */
+ if( d_in.eof() ) {
+ input += line;
+
+ if( input.empty() ) {
+ /* Nothing left to parse. */
+ return NULL;
+ }
+
+ /* Some input left to parse, but nothing left to read.
+ Jump out of input loop. */
+ break;
+ }
+
+ /* Extract the newline delimiter from the stream too */
+ int c = d_in.get();
+ Assert( c == '\n' );
+
+ // cout << "Next char is '" << (char)c << "'" << endl << flush;
+
input += line;
/* If the last char was a backslash, continue on the next line. */
- if( !line.empty() && line[n] == '\\' ) {
- n = input.length() - 1;
- Assert( input[n] == '\\' );
+ n = input.length() - 1;
+ if( !line.empty() && input[n] == '\\' ) {
input[n] = '\n';
d_out << "... > " << flush;
} else {
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index af9e447ed..d511e48e7 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -39,7 +39,8 @@ UNIT_TESTS = \
util/integer_white \
util/rational_black \
util/rational_white \
- util/stats_black
+ util/stats_black \
+ main/interactive_shell_black
export VERBOSE = 1
@@ -74,11 +75,14 @@ AM_LDFLAGS_BLACK =
AM_LDFLAGS_PUBLIC =
AM_LIBADD_WHITE = \
@abs_top_builddir@/src/parser/libcvc4parser_noinst.la \
- @abs_top_builddir@/src/libcvc4_noinst.la
+ @abs_top_builddir@/src/libcvc4_noinst.la \
+ @abs_top_builddir@/src/main/libmain.a
AM_LIBADD_BLACK = \
@abs_top_builddir@/src/parser/libcvc4parser_noinst.la \
- @abs_top_builddir@/src/libcvc4_noinst.la
+ @abs_top_builddir@/src/libcvc4_noinst.la \
+ @abs_top_builddir@/src/main/libmain.a
AM_LIBADD_PUBLIC = \
+ @abs_top_builddir@/src/parser/libcvc4parser.la \
@abs_top_builddir@/src/libcvc4.la
EXTRA_DIST = \
diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
new file mode 100644
index 000000000..e56e8de8a
--- /dev/null
+++ b/test/unit/main/interactive_shell_black.h
@@ -0,0 +1,115 @@
+/********************* */
+/*! \file interactive_shell_black.h
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::InteractiveShell.
+ **
+ ** Black box testing of CVC4::InteractiveShell.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+//Used in some of the tests
+#include <vector>
+#include <sstream>
+
+#include "expr/expr_manager.h"
+#include "main/interactive_shell.h"
+#include "parser/parser_builder.h"
+#include "util/language.h"
+#include "util/options.h"
+
+using namespace CVC4;
+using namespace std;
+
+class InteractiveShellBlack : public CxxTest::TestSuite {
+private:
+ ExprManager* d_exprManager;
+ Options d_options;
+ stringstream* d_sin;
+ stringstream* d_sout;
+
+ /** Read up to maxCommands+1 from the shell and throw an assertion
+ error if it's fewer than minCommands and more than maxCommands.
+ Note that an empty string followed by EOF may be returned as an
+ empty command, and not NULL (subsequent calls to readCommand()
+ should return NULL). E.g., "CHECKSAT;\n" may return two
+ commands: the CHECKSAT, followed by an empty command, followed
+ by NULL. */
+ void countCommands(InteractiveShell& shell,
+ int minCommands,
+ int maxCommands) {
+ int n = 0;
+ while( n <= maxCommands && shell.readCommand() != NULL ) { ++n; }
+ TS_ASSERT( n <= maxCommands );
+ TS_ASSERT( n >= minCommands );
+ }
+
+ public:
+ void setUp() {
+ d_exprManager = new ExprManager;
+ d_sin = new stringstream;
+ d_sout = new stringstream;
+ d_options.in = d_sin;
+ d_options.out = d_sout;
+ d_options.inputLanguage = language::input::LANG_CVC4;
+ }
+
+ void tearDown() {
+ delete d_exprManager;
+ delete d_sin;
+ delete d_sout;
+ }
+
+ void testAssertTrue() {
+ *d_sin << "ASSERT TRUE;" << flush;
+ InteractiveShell shell(*d_exprManager, d_options);
+ countCommands( shell, 1, 1 );
+ }
+
+ void testQueryFalse() {
+ *d_sin << "QUERY FALSE;" << flush;
+ InteractiveShell shell(*d_exprManager, d_options);
+ countCommands( shell, 1, 1 );
+ }
+
+ void testDefUse() {
+ InteractiveShell shell(*d_exprManager, d_options);
+ *d_sin << "x : REAL; ASSERT x > 0;\n" << flush;
+ /* readCommand may return a sequence, so we can't say for sure
+ whether it will return 1 or 2... */
+ countCommands( shell, 1, 2 );
+ }
+
+ void testDefUse2() {
+ InteractiveShell shell(*d_exprManager, d_options);
+ /* readCommand may return a sequence, see above. */
+ *d_sin << "x : REAL;\n" << flush;
+ shell.readCommand();
+ *d_sin << "ASSERT x > 0;\n" << flush;
+ countCommands( shell, 1, 1 );
+ }
+
+ void testEmptyLine() {
+ InteractiveShell shell(*d_exprManager, d_options);
+ *d_sin << flush;
+ countCommands(shell,0,0);
+ }
+
+ void testRepeatedEmptyLines() {
+ *d_sin << "\n\n\n";
+ InteractiveShell shell(*d_exprManager, d_options);
+ /* Might return up to four empties, might return nothing */
+ countCommands( shell, 0, 3 );
+ }
+
+};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback