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>

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);
         }
       }
     )