diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-03 22:27:16 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-03 22:27:16 +0000 |
commit | f780dd882fc343cef668d5cd9eed8f515d0e70ed (patch) | |
tree | 5a3432a90d1f30cdc00f2353c0b43a468da09661 /test/unit/parser | |
parent | 4cd2a432d621d18f7b811caab8935a617b4771c5 (diff) |
Implementing input from stdin (Fixes: #144)
Diffstat (limited to 'test/unit/parser')
-rw-r--r-- | test/unit/parser/parser_black.h | 37 | ||||
-rw-r--r-- | test/unit/parser/parser_builder_black.h | 150 |
2 files changed, 170 insertions, 17 deletions
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 6f09820c5..f6d822265 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -1,5 +1,5 @@ /********************* */ -/** parser_white.h +/** parser_black.h ** Original author: cconway ** Major contributors: none ** Minor contributors (to current version): dejan, mdeters @@ -10,17 +10,18 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** White box testing of CVC4::parser::SmtParser. + ** Black box testing of CVC4::parser::Parser, including CVC, SMT and + ** SMT v2 inputs. **/ #include <cxxtest/TestSuite.h> -//#include <string> #include <sstream> #include "expr/expr.h" #include "expr/expr_manager.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "parser/parser_options.h" #include "parser/smt2/smt2.h" #include "expr/command.h" #include "util/output.h" @@ -29,8 +30,6 @@ using namespace CVC4; using namespace CVC4::parser; using namespace std; - - class ParserBlack { InputLanguage d_lang; ExprManager *d_exprManager; @@ -62,10 +61,10 @@ protected: // Debug.on("parser-extra"); // cerr << "Testing good input: <<" << goodInput << ">>" << endl; // istringstream stream(goodInputs[i]); - ParserBuilder parserBuilder(d_lang,"test"); Parser *parser = - parserBuilder.withStringInput(goodInput) - .withExprManager(*d_exprManager) + ParserBuilder(*d_exprManager,"test") + .withStringInput(goodInput) + .withInputLanguage(d_lang) .build(); TS_ASSERT( !parser->done() ); Command* cmd; @@ -88,10 +87,11 @@ protected: void tryBadInput(const string badInput, bool strictMode = false) { // cerr << "Testing bad input: '" << badInput << "'\n"; // Debug.on("parser"); - ParserBuilder parserBuilder(d_lang,"test"); + Parser *parser = - parserBuilder.withStringInput(badInput) - .withExprManager(*d_exprManager) + ParserBuilder(*d_exprManager,"test") + .withStringInput(badInput) + .withInputLanguage(d_lang) .withStrictMode(strictMode) .build(); TS_ASSERT_THROWS @@ -109,11 +109,13 @@ protected: // cerr << "Testing good expr: '" << goodExpr << "'\n"; // Debug.on("parser"); // istringstream stream(context + goodBooleanExprs[i]); - ParserBuilder parserBuilder(d_lang,"test"); + Parser *parser = - parserBuilder.withStringInput(goodExpr) - .withExprManager(*d_exprManager) + ParserBuilder(*d_exprManager,"test") + .withStringInput(goodExpr) + .withInputLanguage(d_lang) .build(); + TS_ASSERT( !parser->done() ); setupContext(*parser); TS_ASSERT( !parser->done() ); @@ -142,10 +144,11 @@ protected: // Debug.on("parser"); // Debug.on("parser-extra"); // cout << "Testing bad expr: '" << badExpr << "'\n"; - ParserBuilder parserBuilder(d_lang,"test"); + Parser *parser = - parserBuilder.withStringInput(badExpr) - .withExprManager(*d_exprManager) + ParserBuilder(*d_exprManager,"test") + .withStringInput(badExpr) + .withInputLanguage(d_lang) .withStrictMode(strictMode) .build(); setupContext(*parser); diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h new file mode 100644 index 000000000..f254580af --- /dev/null +++ b/test/unit/parser/parser_builder_black.h @@ -0,0 +1,150 @@ +/********************* */ +/** parser_builder_black.h + ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): dejan, mdeters + ** 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. + ** + ** Black box testing of CVC4::parser::ParserBuilder. + **/ + +#include <cxxtest/TestSuite.h> +#include <ext/stdio_filebuf.h> +#include <fstream> +#include <iostream> +#include <stdio.h> +#include <string.h> +#include <sys/stat.h> +#include <unistd.h> + +#include "expr/command.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" +#include "parser/parser_options.h" + +typedef __gnu_cxx::stdio_filebuf<char> filebuf_gnu; + +using namespace CVC4; +using namespace CVC4::parser; +using namespace std; + +class ParserBuilderBlack : public CxxTest::TestSuite { + + ExprManager *d_exprManager; + + void checkEmptyInput(ParserBuilder& builder) { + Parser *parser = builder.build(); + TS_ASSERT( parser != NULL ); + + Expr e = parser->nextExpression(); + TS_ASSERT( e.isNull() ); + + delete parser; + } + + void checkTrueInput(ParserBuilder& builder) { + Parser *parser = builder.build(); + TS_ASSERT( parser != NULL ); + + Expr e = parser->nextExpression(); + TS_ASSERT_EQUALS( e, d_exprManager->mkConst(true) ); + + e = parser->nextExpression(); + TS_ASSERT( e.isNull() ); + delete parser; + } + + char* mkTemp() { + char *filename = strdup("/tmp/testinput.XXXXXX"); + int fd = mkstemp(filename); + TS_ASSERT( fd != -1 ); + close(fd); + return filename; + } + +public: + + void setUp() { + d_exprManager = new ExprManager; + } + + void tearDown() { + delete d_exprManager; + } + + void testEmptyFileInput() { + char *filename = mkTemp(); + + /* FILE *fp = tmpfile(); */ + /* filebuf_gnu fs( fd, ios_base::out ); */ + + /* ptr = tmpnam(filename); */ + /* std::fstream fs( ptr, fstream::out ); */ + /* fs.close(); */ + + checkEmptyInput( + ParserBuilder(*d_exprManager,filename) + .withInputLanguage(LANG_CVC4) + ); + + remove(filename); + // mkfifo(ptr, S_IWUSR | s_IRUSR); + } + + void testSimpleFileInput() { + char *filename = mkTemp(); + + std::fstream fs( filename, fstream::out ); + fs << "TRUE" << std::endl; + fs.close(); + + checkTrueInput( + ParserBuilder(*d_exprManager,filename) + .withInputLanguage(LANG_CVC4) + ); + + remove(filename); + } + + void testEmptyStringInput() { + checkEmptyInput( + ParserBuilder(*d_exprManager,"foo") + .withInputLanguage(LANG_CVC4) + .withStringInput("") + ); + } + + void testTrueStringInput() { + checkTrueInput( + ParserBuilder(*d_exprManager,"foo") + .withInputLanguage(LANG_CVC4) + .withStringInput("TRUE") + ); + } + + void testEmptyStreamInput() { + stringstream ss( "", ios_base::in ); + checkEmptyInput( + ParserBuilder(*d_exprManager,"foo") + .withInputLanguage(LANG_CVC4) + .withStreamInput(ss) + ); + } + + void testTrueStreamInput() { + stringstream ss( "TRUE", ios_base::in ); + checkTrueInput( + ParserBuilder(*d_exprManager,"foo") + .withInputLanguage(LANG_CVC4) + .withStreamInput(ss) + ); + } + + + +}; // class ParserBuilderBlack |