From 168d8c1508b77e7285c8f78ae195bd7efbef7dcb Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 3 Jan 2019 11:33:39 +0000 Subject: [PATCH 1/8] Do not shadow "operands" Remove unnecessary re-declaration. --- src/solvers/flattening/boolbv_array.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/solvers/flattening/boolbv_array.cpp b/src/solvers/flattening/boolbv_array.cpp index c6a62419738..983cfae9e0a 100644 --- a/src/solvers/flattening/boolbv_array.cpp +++ b/src/solvers/flattening/boolbv_array.cpp @@ -27,7 +27,6 @@ bvt boolbvt::convert_array(const exprt &expr) expr.has_operands(), "the bit width being nonzero implies that the array has a nonzero size " "in which case the array shall have operands"); - const exprt::operandst &operands=expr.operands(); const std::size_t op_width = width / operands.size(); bvt bv; From 91c7be51c4000b730910656b2e76103097443933 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 3 Jan 2019 11:57:56 +0000 Subject: [PATCH 2/8] Avoid shadowing "offset" Just use "expr.offset()" in those places where it is genuinely used. --- src/solvers/flattening/boolbv_byte_extract.cpp | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index ec455047d70..f9e7749d928 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -103,7 +103,6 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) } const exprt &op=expr.op(); - const exprt &offset=expr.offset(); PRECONDITION( expr.id() == ID_byte_extract_little_endian || expr.id() == ID_byte_extract_big_endian); @@ -145,9 +144,10 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) // add implications equal_exprt equality; - equality.lhs()=offset; // index operand + equality.lhs() = expr.offset(); // index operand - typet constant_type=offset.type(); // type of index operand + // type of index operand + const typet &constant_type = expr.offset().type(); bvt equal_bv; equal_bv.resize(width); @@ -171,9 +171,10 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) else { equal_exprt equality; - equality.lhs()=offset; // index operand + equality.lhs() = expr.offset(); // index operand - typet constant_type(offset.type()); // type of index operand + // type of index operand + const typet &constant_type = expr.offset().type(); for(std::size_t i=0; i Date: Thu, 3 Jan 2019 12:36:07 +0000 Subject: [PATCH 3/8] Do not shadow "i" Use "j" for the inner loop instead of re-using the loop counter of the outer loop. --- src/solvers/flattening/boolbv_cond.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/solvers/flattening/boolbv_cond.cpp b/src/solvers/flattening/boolbv_cond.cpp index 29a36f72588..8798abbece1 100644 --- a/src/solvers/flattening/boolbv_cond.cpp +++ b/src/solvers/flattening/boolbv_cond.cpp @@ -74,8 +74,8 @@ bvt boolbvt::convert_cond(const cond_exprt &expr) const bvt &op = convert_bv(value, bv.size()); - for(std::size_t i=0; i Date: Thu, 3 Jan 2019 14:42:39 +0000 Subject: [PATCH 4/8] Do not shadow "filename" The value is necessarily the same as the class member, just remove the parameter. --- src/solvers/flattening/bv_dimacs.cpp | 2 +- src/solvers/flattening/bv_dimacs.h | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/solvers/flattening/bv_dimacs.cpp b/src/solvers/flattening/bv_dimacs.cpp index 60079185227..d0d627f6a35 100644 --- a/src/solvers/flattening/bv_dimacs.cpp +++ b/src/solvers/flattening/bv_dimacs.cpp @@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -bool bv_dimacst::write_dimacs(const std::string &filename) +bool bv_dimacst::write_dimacs() { if(filename.empty() || filename == "-") return write_dimacs(std::cout); diff --git a/src/solvers/flattening/bv_dimacs.h b/src/solvers/flattening/bv_dimacs.h index c6fded199aa..c7dbedb8a0d 100644 --- a/src/solvers/flattening/bv_dimacs.h +++ b/src/solvers/flattening/bv_dimacs.h @@ -24,12 +24,12 @@ class bv_dimacst : public bv_pointerst virtual ~bv_dimacst() { - write_dimacs(filename); + write_dimacs(); } protected: - std::string filename; - bool write_dimacs(const std::string &filename); + const std::string filename; + bool write_dimacs(); bool write_dimacs(std::ostream &); }; From f10d34adcd13517fff4148b3624de8cf9e898f41 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 3 Jan 2019 15:06:29 +0000 Subject: [PATCH 5/8] Remove shadowing "tmp" The name carries no added value, just get rid of the named temporary. --- src/solvers/lowering/byte_operators.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp index 00883e1e427..7da44f745c5 100644 --- a/src/solvers/lowering/byte_operators.cpp +++ b/src/solvers/lowering/byte_operators.cpp @@ -648,8 +648,7 @@ exprt lower_byte_operators(const exprt &src, const namespacet &ns) // destroys any sharing, should use hash table Forall_operands(it, tmp) { - exprt tmp=lower_byte_operators(*it, ns); - it->swap(tmp); + *it = lower_byte_operators(*it, ns); } if(src.id()==ID_byte_update_little_endian || From ede263ba4b01d5deb87bbb96d2405c7909c317b6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 3 Jan 2019 15:11:01 +0000 Subject: [PATCH 6/8] Do not shadow "i" Just get rid of the first loop counter altogether. --- src/solvers/prop/prop_conv.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index a11bf4b04db..0c9f20884f4 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -238,11 +238,10 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr) "constraint_select_one should have at least two operands"); std::vector op_bv; - op_bv.resize(op.size()); + op_bv.reserve(op.size()); - unsigned i=0; forall_operands(it, expr) - op_bv[i++]=convert(*it); + op_bv.push_back(convert(*it)); // add constraints From 1d7c5626bf9dccb9bfb21363a163845ce48b6785 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 3 Jan 2019 16:29:13 +0000 Subject: [PATCH 7/8] Resolve shadowing in smt2_conv Remove duplicate definitions of boolbv_width, do not shadow "it" or "out". --- src/solvers/smt2/smt2_conv.cpp | 48 ++++++++++++++-------------------- src/solvers/smt2/smt2_conv.h | 2 +- 2 files changed, 21 insertions(+), 29 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index f75b8dbd1ec..c47986a21b1 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -40,12 +40,12 @@ Author: Daniel Kroening, kroening@kroening.com // General todos #define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S) -void smt2_convt::print_assignment(std::ostream &out) const +void smt2_convt::print_assignment(std::ostream &os) const { // Boolean stuff for(std::size_t v=0; v &let_order) { - seen_expressionst::iterator it = map.find(expr); + seen_expressionst::iterator entry = map.find(expr); - if(it!=map.end()) + if(entry != map.end()) { - let_count_idt &count_id=it->second; + let_count_idt &count_id = entry->second; ++(count_id.count); return; } diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index f8758d04bcc..30a35babee9 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -118,7 +118,7 @@ class smt2_convt:public prop_convt virtual void set_to(const exprt &expr, bool value); virtual exprt get(const exprt &expr) const; virtual std::string decision_procedure_text() const { return "SMT2"; } - virtual void print_assignment(std::ostream &out) const; + virtual void print_assignment(std::ostream &) const; virtual tvt l_get(literalt l) const; virtual void set_assumptions(const bvt &bv) { assumptions=bv; } From 1883da9b60b21c563a2dc01fc2f1cd7ed81ad3da Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 3 Jan 2019 16:39:42 +0000 Subject: [PATCH 8/8] Do not shadow "value" Rename the mp_integer-typed variant to "int_value." --- src/solvers/smt2/smt2_format.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/solvers/smt2/smt2_format.cpp b/src/solvers/smt2/smt2_format.cpp index 1efab965720..a8a3f5ea78d 100644 --- a/src/solvers/smt2/smt2_format.cpp +++ b/src/solvers/smt2/smt2_format.cpp @@ -54,9 +54,9 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr) { const std::size_t width = to_unsignedbv_type(expr_type).get_width(); - const auto value = numeric_cast_v(expr); + const auto int_value = numeric_cast_v(expr); - out << "(_ bv" << value << " " << width << ")"; + out << "(_ bv" << int_value << " " << width << ")"; } else if(expr_type.id() == ID_bool) {