diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2020-03-05 11:42:54 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-05 11:42:54 -0800 |
commit | 04039407e6308070c148de0d5e93640ec1b0a341 (patch) | |
tree | b66f63d49df0713b1ca2a440bec89f1d60af32a4 /src/parser | |
parent | 18fe192c29a9a2c37d1925730af01e906b9888c5 (diff) |
Enable -Wshadow and fix warnings. (#3909)
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally.
Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 47 | ||||
-rw-r--r-- | src/parser/line_buffer.cpp | 6 | ||||
-rw-r--r-- | src/parser/parser.cpp | 1 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 72 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 16 | ||||
-rw-r--r-- | src/parser/tptp/Tptp.g | 12 |
6 files changed, 77 insertions, 77 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 94904f6d9..637603997 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1483,7 +1483,6 @@ prefixFormula[CVC4::Expr& f] boundVarDeclsReturn[terms,types] RPAREN COLON formula[f] { PARSER_STATE->popScope(); - Type t = EXPR_MANAGER->mkFunctionType(types, f.getType()); Expr bvl = EXPR_MANAGER->mkExpr( kind::BOUND_VAR_LIST, terms ); f = EXPR_MANAGER->mkExpr( kind::LAMBDA, bvl, f ); } @@ -1770,9 +1769,9 @@ postfixTerm[CVC4::Expr& f] if(left) { f = MK_EXPR(kind::BITVECTOR_CONCAT, f, MK_CONST(BitVector(k))); } else { - unsigned n = BitVectorType(f.getType()).getSize(); + unsigned bv_size = BitVectorType(f.getType()).getSize(); f = MK_EXPR(kind::BITVECTOR_CONCAT, MK_CONST(BitVector(k)), - MK_EXPR(MK_CONST(BitVectorExtract(n - 1, k)), f)); + MK_EXPR(MK_CONST(BitVectorExtract(bv_size - 1, k)), f)); } } @@ -1782,41 +1781,41 @@ postfixTerm[CVC4::Expr& f] ( COMMA formula[f] { args.push_back(f); } )* RPAREN { PARSER_STATE->checkFunctionLike(args.front()); - Kind k = PARSER_STATE->getKindForFunction(args.front()); + Kind kind = PARSER_STATE->getKindForFunction(args.front()); Debug("parser") << "expr is " << args.front() << std::endl; - Debug("parser") << "kind is " << k << std::endl; - f = MK_EXPR(k, args); + Debug("parser") << "kind is " << kind << std::endl; + f = MK_EXPR(kind, args); } /* record / tuple select */ | DOT ( identifier[id,CHECK_NONE,SYM_VARIABLE] - { Type t = f.getType(); - if(! t.isRecord()) { + { Type type = f.getType(); + if(! type.isRecord()) { PARSER_STATE->parseError("record-select applied to non-record"); } - const Record& rec = ((DatatypeType)t).getRecord(); + const Record& rec = ((DatatypeType)type).getRecord(); if(!rec.contains(id)){ PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); } - const Datatype & dt = ((DatatypeType)t).getDatatype(); + const Datatype & dt = ((DatatypeType)type).getDatatype(); std::vector<Expr> sargs; sargs.push_back( dt[0][id].getSelector() ); sargs.push_back( f ); f = MK_EXPR(CVC4::kind::APPLY_SELECTOR,sargs); } | k=numeral - { Type t = f.getType(); - if(! t.isTuple()) { + { Type type = f.getType(); + if(! type.isTuple()) { PARSER_STATE->parseError("tuple-select applied to non-tuple"); } - size_t length = ((DatatypeType)t).getTupleLength(); + size_t length = ((DatatypeType)type).getTupleLength(); if(k >= length) { std::stringstream ss; ss << "tuple is of length " << length << "; cannot access index " << k; PARSER_STATE->parseError(ss.str()); } - const Datatype & dt = ((DatatypeType)t).getDatatype(); + const Datatype & dt = ((DatatypeType)type).getDatatype(); std::vector<Expr> sargs; sargs.push_back( dt[0][k].getSelector() ); sargs.push_back( f ); @@ -2095,8 +2094,8 @@ simpleTerm[CVC4::Expr& f] for(std::vector<Expr>::const_iterator i = args.begin(); i != args.end(); ++i) { types.push_back((*i).getType()); } - DatatypeType t = EXPR_MANAGER->mkTupleType(types); - const Datatype& dt = t.getDatatype(); + DatatypeType dtype = EXPR_MANAGER->mkTupleType(types); + const Datatype& dt = dtype.getDatatype(); args.insert( args.begin(), dt[0].getConstructor() ); f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); } @@ -2105,14 +2104,14 @@ simpleTerm[CVC4::Expr& f] /* empty tuple literal */ | LPAREN RPAREN { std::vector<Type> types; - DatatypeType t = EXPR_MANAGER->mkTupleType(types); - const Datatype& dt = t.getDatatype(); + DatatypeType dtype = EXPR_MANAGER->mkTupleType(types); + const Datatype& dt = dtype.getDatatype(); f = MK_EXPR(kind::APPLY_CONSTRUCTOR, dt[0].getConstructor()); } /* empty record literal */ | PARENHASH HASHPAREN - { DatatypeType t = EXPR_MANAGER->mkRecordType(std::vector< std::pair<std::string, Type> >()); - const Datatype& dt = t.getDatatype(); + { DatatypeType dtype = EXPR_MANAGER->mkRecordType(std::vector< std::pair<std::string, Type> >()); + const Datatype& dt = dtype.getDatatype(); f = MK_EXPR(kind::APPLY_CONSTRUCTOR, dt[0].getConstructor()); } /* empty set literal */ @@ -2197,8 +2196,8 @@ simpleTerm[CVC4::Expr& f] for(unsigned i = 0; i < names.size(); ++i) { typeIds.push_back(std::make_pair(names[i], args[i].getType())); } - DatatypeType t = EXPR_MANAGER->mkRecordType(typeIds); - const Datatype& dt = t.getDatatype(); + DatatypeType dtype = EXPR_MANAGER->mkRecordType(typeIds); + const Datatype& dt = dtype.getDatatype(); args.insert( args.begin(), dt[0].getConstructor() ); f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); } @@ -2208,8 +2207,8 @@ simpleTerm[CVC4::Expr& f] /* ascriptions will be required for parameterized zero-ary constructors */ { f = PARSER_STATE->getVariable(name); // datatypes: zero-ary constructors - Type t2 = f.getType(); - if(t2.isConstructor() && ConstructorType(t2).getArity() == 0) { + Type dtype = f.getType(); + if(dtype.isConstructor() && ConstructorType(dtype).getArity() == 0) { // don't require parentheses, immediately turn it into an apply f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, f); } diff --git a/src/parser/line_buffer.cpp b/src/parser/line_buffer.cpp index 35263f3ac..6e7614d88 100644 --- a/src/parser/line_buffer.cpp +++ b/src/parser/line_buffer.cpp @@ -69,8 +69,10 @@ bool LineBuffer::isPtrBefore(uint8_t* ptr, size_t line, size_t pos_in_line) { return false; } -bool LineBuffer::readToLine(size_t line) { - while (line >= d_lines.size()) { +bool LineBuffer::readToLine(size_t line_size) +{ + while (line_size >= d_lines.size()) + { if (!(*d_stream)) { return false; } diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 5beec6565..eae9636a2 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -536,7 +536,6 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) api::Sort etype = t.getSort(); if (etype.isConstructor()) { - api::Sort etype = t.getSort(); // get the datatype that t belongs to api::Sort etyped = etype.getConstructorCodomainSort(); api::Datatype d = etyped.getDatatype(); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a47d58944..9ae9f7261 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -441,10 +441,10 @@ command [std::unique_ptr<CVC4::Command>* cmd] } } ( k=INTEGER_LITERAL - { unsigned n = AntlrInput::tokenToUnsigned(k); - if(n == 0) { + { unsigned num = AntlrInput::tokenToUnsigned(k); + if(num == 0) { cmd->reset(new EmptyCommand()); - } else if(n == 1) { + } else if(num == 1) { PARSER_STATE->pushScope(); cmd->reset(new PushCommand()); } else { @@ -452,10 +452,10 @@ command [std::unique_ptr<CVC4::Command>* cmd] do { PARSER_STATE->pushScope(); Command* push_cmd = new PushCommand(); - push_cmd->setMuted(n > 1); + push_cmd->setMuted(num > 1); seq->addCommand(push_cmd); - --n; - } while(n > 0); + --num; + } while(num > 0); cmd->reset(seq.release()); } } @@ -474,14 +474,14 @@ command [std::unique_ptr<CVC4::Command>* cmd] } } ( k=INTEGER_LITERAL - { unsigned n = AntlrInput::tokenToUnsigned(k); - if(n > PARSER_STATE->scopeLevel()) { + { unsigned num = AntlrInput::tokenToUnsigned(k); + if(num > PARSER_STATE->scopeLevel()) { PARSER_STATE->parseError("Attempted to pop above the top stack " "frame."); } - if(n == 0) { + if(num == 0) { cmd->reset(new EmptyCommand()); - } else if(n == 1) { + } else if(num == 1) { PARSER_STATE->popScope(); cmd->reset(new PopCommand()); } else { @@ -489,10 +489,10 @@ command [std::unique_ptr<CVC4::Command>* cmd] do { PARSER_STATE->popScope(); Command* pop_command = new PopCommand(); - pop_command->setMuted(n > 1); + pop_command->setMuted(num > 1); seq->addCommand(pop_command); - --n; - } while(n > 0); + --num; + } while(num > 0); cmd->reset(seq.release()); } } @@ -1263,7 +1263,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } nonemptySortList[sorts] RPAREN_TOK - { Type t; + { Type tt; if(sorts.size() > 1) { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { PARSER_STATE->parseError( @@ -1275,13 +1275,13 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] // must flatten Type range = sorts.back(); sorts.pop_back(); - t = PARSER_STATE->mkFlatFunctionType(sorts, range); + tt = PARSER_STATE->mkFlatFunctionType(sorts, range); } else { - t = sorts[0]; + tt = sorts[0]; } // allow overloading - Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true); - seq->addCommand(new DeclareFunctionCommand(name, func, t)); + Expr func = PARSER_STATE->mkVar(name, tt, ExprManager::VAR_FLAG_NONE, true); + seq->addCommand(new DeclareFunctionCommand(name, func, tt)); sorts.clear(); } )+ @@ -1293,7 +1293,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } sortList[sorts] RPAREN_TOK - { Type t = EXPR_MANAGER->booleanType(); + { Type boolType = EXPR_MANAGER->booleanType(); if(sorts.size() > 0) { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { PARSER_STATE->parseError( @@ -1302,11 +1302,11 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] + PARSER_STATE->getLogic().getLogicString() + " unless option --uf-ho is used"); } - t = EXPR_MANAGER->mkFunctionType(sorts, t); + boolType = EXPR_MANAGER->mkFunctionType(sorts, boolType); } // allow overloading - Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true); - seq->addCommand(new DeclareFunctionCommand(name, func, t)); + Expr func = PARSER_STATE->mkVar(name, boolType, ExprManager::VAR_FLAG_NONE, true); + seq->addCommand(new DeclareFunctionCommand(name, func, boolType)); sorts.clear(); } )+ @@ -1335,18 +1335,18 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] // declare the name down here (while parsing term, signature // must not be extended with the name itself; no recursion // permitted) - Type t = e.getType(); + Type tt = e.getType(); if( sortedVarNames.size() > 0 ) { - std::vector<CVC4::Type> sorts; - sorts.reserve(sortedVarNames.size()); + std::vector<CVC4::Type> types; + types.reserve(sortedVarNames.size()); for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; ++i) { - sorts.push_back((*i).second); + types.push_back((*i).second); } - t = EXPR_MANAGER->mkFunctionType(sorts, t); + tt = EXPR_MANAGER->mkFunctionType(types, tt); } - Expr func = PARSER_STATE->mkVar(name, t, + Expr func = PARSER_STATE->mkVar(name, tt, ExprManager::VAR_FLAG_DEFINED); cmd->reset(new DefineFunctionCommand(name, func, terms, e)); } @@ -1750,8 +1750,8 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] cargs.push_back(f); cargs.insert(cargs.end(),args.begin(),args.end()); Expr c = MK_EXPR(kind::APPLY_CONSTRUCTOR,cargs); - Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST,args); - Expr mc = MK_EXPR(kind::MATCH_BIND_CASE, bvl, c, f3); + Expr bvla = MK_EXPR(kind::BOUND_VAR_LIST,args); + Expr mc = MK_EXPR(kind::MATCH_BIND_CASE, bvla, c, f3); matchcases.push_back(mc); // now, pop the scope PARSER_STATE->popScope(); @@ -1781,8 +1781,8 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] Expr mc; if (f.getKind() == kind::BOUND_VARIABLE) { - Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, f); - mc = MK_EXPR(kind::MATCH_BIND_CASE, bvl, f, f3); + Expr bvlf = MK_EXPR(kind::BOUND_VAR_LIST, f); + mc = MK_EXPR(kind::MATCH_BIND_CASE, bvlf, f, f3); } else { @@ -2116,8 +2116,8 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr] avar = expr[0]; } }else{ - Type t = EXPR_MANAGER->booleanType(); - avar = PARSER_STATE->mkVar(attr_name, t); + Type boolType = EXPR_MANAGER->booleanType(); + avar = PARSER_STATE->mkVar(attr_name, boolType); } if( success ){ //Will set the attribute on auxiliary var (preserves attribute on @@ -2151,8 +2151,8 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr] values.push_back( n ); std::string attr_name(AntlrInput::tokenText($tok)); attr_name.erase( attr_name.begin() ); - Type t = EXPR_MANAGER->booleanType(); - Expr avar = PARSER_STATE->mkVar(attr_name, t); + Type boolType = EXPR_MANAGER->booleanType(); + Expr avar = PARSER_STATE->mkVar(attr_name, boolType); retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar); Command* c = new SetUserAttributeCommand( attr_name, avar, values ); c->setMuted(true); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 94a273193..15fdd8461 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1376,9 +1376,9 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt, } else { - std::stringstream ss; - ss << "unexpected parse operator for sygus constructor" << ops[i]; - parseError(ss.str()); + std::stringstream ess; + ess << "unexpected parse operator for sygus constructor" << ops[i]; + parseError(ess.str()); } Debug("parser-sygus") << " finished constructing the datatype" << std::endl; @@ -1696,12 +1696,12 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) { argTypes.push_back((*i).getType()); } - Expr op = getOverloadedFunctionForTypes(p.d_name, argTypes); - if (!op.isNull()) + Expr fop = getOverloadedFunctionForTypes(p.d_name, argTypes); + if (!fop.isNull()) { - checkFunctionLike(op); - kind = getKindForFunction(op); - args.insert(args.begin(), op); + checkFunctionLike(fop); + kind = getKindForFunction(fop); + args.insert(args.begin(), fop); } else { diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 873fde25c..afa072e6d 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -965,8 +965,8 @@ thfAtomTyping[CVC4::Command*& cmd] else { // as yet, it's undeclared - Type type = PARSER_STATE->mkSort(name); - cmd = new DeclareTypeCommand(name, 0, type); + Type atype = PARSER_STATE->mkSort(name); + cmd = new DeclareTypeCommand(name, 0, atype); } } | parseThfType[type] @@ -1317,8 +1317,8 @@ tffTypedAtom[CVC4::Command*& cmd] PARSER_STATE->parseError("Symbol `" + name + "' previously declared as a constant; cannot also be a sort"); } else { // as yet, it's undeclared - Type type = PARSER_STATE->mkSort(name); - cmd = new DeclareTypeCommand(name, 0, type); + Type atype = PARSER_STATE->mkSort(name); + cmd = new DeclareTypeCommand(name, 0, atype); } } | parseType[type] @@ -1336,8 +1336,8 @@ tffTypedAtom[CVC4::Command*& cmd] } } else { // as yet, it's undeclared - CVC4::Expr expr = PARSER_STATE->mkVar(name, type); - cmd = new DeclareFunctionCommand(name, expr, type); + CVC4::Expr aexpr = PARSER_STATE->mkVar(name, type); + cmd = new DeclareFunctionCommand(name, aexpr, type); } } ) |