From: Christopher L. Conway Date: Sun, 24 Oct 2010 16:37:00 +0000 (+0000) Subject: Adding unit test for InteractiveShell X-Git-Tag: cvc5-1.0.0~8781 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ade732181ad2eabfb3a6eef46bdc9ea42d27246e;p=cvc5.git Adding unit test for InteractiveShell --- 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 + +//Used in some of the tests +#include +#include + +#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 ); + } + +};