From 931b5641dfffcd3779239e014406aa057e21e0f7 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 7 Jun 2013 15:23:36 -0400 Subject: Allow disabling include-file feature --- src/parser/smt2/Smt2.g | 5 ++++- src/parser/smt2/smt2.cpp | 5 +++++ 2 files changed, 9 insertions(+), 1 deletion(-) (limited to 'src/parser/smt2') diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 29bc8d40f..5abaa0163 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -197,7 +197,10 @@ parseCommand returns [CVC4::Command* cmd = NULL] * the RPAREN_TOK is properly eaten and we are in a good state to read * the included file's tokens. */ | LPAREN_TOK INCLUDE_TOK str[name] RPAREN_TOK - { if(PARSER_STATE->strictModeEnabled()) { + { if(!PARSER_STATE->canIncludeFile()) { + PARSER_STATE->parseError("include-file feature was disabled for this run."); + } + if(PARSER_STATE->strictModeEnabled()) { PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode."); } PARSER_STATE->includeFile(name); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index be4907e8e..42324fe1e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -242,6 +242,11 @@ static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) { } void Smt2::includeFile(const std::string& filename) { + // security for online version + if(!canIncludeFile()) { + parseError("include-file feature was disabled for this run."); + } + // Get the lexer AntlrInput* ai = static_cast(getInput()); pANTLR3_LEXER lexer = ai->getAntlr3Lexer(); -- cgit v1.2.3