Skip to content

Commit 0b3f43b

Browse files
tautschnigtautschnig
authored
Merge pull request #3685 from tautschnig/vs-shadow-jbmc-unit
Avoid shadowing in directory jbmc/unit [blocks: #3607]
2 parents 493d3c3 + 7c33e43 commit 0b3f43b

File tree

3 files changed

+36
-51
lines changed

3 files changed

+36
-51
lines changed

‎jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -21,10 +21,6 @@ SCENARIO(
2121
std::string class_prefix = "java::BoundedGenericInnerClasses";
2222
REQUIRE(new_symbol_table.has_symbol(class_prefix));
2323

24-
const symbolt &class_symbol = new_symbol_table.lookup_ref(class_prefix);
25-
const java_class_typet &java_class_type =
26-
require_type::require_complete_java_non_generic_class(class_symbol.type);
27-
2824
WHEN("Parsing an inner class with type variable")
2925
{
3026
std::string inner_name = class_prefix + "$Inner";
@@ -90,6 +86,8 @@ SCENARIO(
9086

9187
WHEN("There is a generic field with a concrete type")
9288
{
89+
const symbolt &class_symbol = new_symbol_table.lookup_ref(class_prefix);
90+
require_type::require_complete_java_non_generic_class(class_symbol.type);
9391
const struct_union_typet::componentt &belem_type =
9492
require_type::require_component(
9593
to_struct_type(class_symbol.type), "belem");

‎jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -600,14 +600,14 @@ SCENARIO(
600600

601601
GIVEN("A method that may or may not throw exceptions")
602602
{
603-
const symbol_tablet &new_symbol_table = load_java_class(
603+
const symbol_tablet &new_symbol_table2 = load_java_class(
604604
"ThrowsExceptions", "./java_bytecode/java_bytecode_parser");
605605
WHEN("Parsing the exceptions attribute for a method that throws exceptions")
606606
{
607607
THEN("We should be able to get the list of exceptions it throws")
608608
{
609609
const symbolt &method_symbol =
610-
new_symbol_table.lookup_ref("java::ThrowsExceptions.test:()V");
610+
new_symbol_table2.lookup_ref("java::ThrowsExceptions.test:()V");
611611
const java_method_typet method =
612612
to_java_method_type(method_symbol.type);
613613
const std::vector<irep_idt> exceptions = method.throws_exceptions();
@@ -629,7 +629,7 @@ SCENARIO(
629629
{
630630
THEN("We should be able to get the list of exceptions it throws")
631631
{
632-
const symbolt &method_symbol = new_symbol_table.lookup_ref(
632+
const symbolt &method_symbol = new_symbol_table2.lookup_ref(
633633
"java::ThrowsExceptions.testNoExceptions:()V");
634634
const java_method_typet method =
635635
to_java_method_type(method_symbol.type);

‎jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp‎

Lines changed: 31 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -164,7 +164,7 @@ SCENARIO("instantiate_not_contains",
164164
register_language(new_java_bytecode_language);
165165
std::unique_ptr<languaget> java_lang = get_language_from_mode(ID_java);
166166
symbol_tablet symtbl;
167-
const namespacet ns(symtbl);
167+
const namespacet empty_ns(symtbl);
168168

169169
// initialize architecture with sensible default values
170170
config.set_arch("none");
@@ -190,9 +190,7 @@ SCENARIO("instantiate_not_contains",
190190
t.length_type());
191191

192192
// Generating the corresponding axioms and simplifying, recording info
193-
symbol_tablet symtab;
194-
const namespacet empty_ns(symtab);
195-
string_constraint_generatort generator(ns);
193+
string_constraint_generatort generator(empty_ns);
196194
const auto pair = generator.add_axioms_for_function_application(
197195
generator.fresh_symbol, func);
198196
const string_constraintst &constraints = pair.second;
@@ -206,7 +204,7 @@ SCENARIO("instantiate_not_contains",
206204
constraints.universal.end(),
207205
axioms,
208206
[&](const std::string &accu, string_constraintt sc) {
209-
simplify(sc.body, ns);
207+
simplify(sc.body, empty_ns);
210208
return accu + to_string(sc) + "\n\n";
211209
});
212210

@@ -215,9 +213,9 @@ SCENARIO("instantiate_not_contains",
215213
constraints.not_contains.end(),
216214
axioms,
217215
[&](const std::string &accu, string_not_contains_constraintt sc) {
218-
simplify(sc.premise, ns);
219-
simplify(sc.s0, ns);
220-
simplify(sc.s1, ns);
216+
simplify(sc.premise, empty_ns);
217+
simplify(sc.s0, empty_ns);
218+
simplify(sc.s1, empty_ns);
221219
witnesses[sc] = generator.fresh_symbol("w", t.witness_type());
222220
nc_axioms.push_back(sc);
223221
return accu + to_string(sc) + "\n\n";
@@ -228,9 +226,9 @@ SCENARIO("instantiate_not_contains",
228226
constraints.existential.end(),
229227
axioms,
230228
[&](const std::string &accu, exprt axiom) {
231-
simplify(axiom, ns);
229+
simplify(axiom, empty_ns);
232230
std::string s;
233-
java_lang->from_expr(axiom, s, ns);
231+
java_lang->from_expr(axiom, s, empty_ns);
234232
return accu + s + "\n\n";
235233
});
236234

@@ -254,14 +252,14 @@ SCENARIO("instantiate_not_contains",
254252
lemmas.insert(lemmas.end(), l.begin(), l.end());
255253
}
256254

257-
const exprt conj=combine_lemmas(lemmas, ns);
258-
const std::string info=create_info(lemmas, ns);
255+
const exprt conj = combine_lemmas(lemmas, empty_ns);
256+
const std::string info = create_info(lemmas, empty_ns);
259257
INFO(info);
260258

261259
THEN("the conjunction of instantiations is SAT")
262260
{
263261
// Check if SAT
264-
decision_proceduret::resultt result=check_sat(conj, ns);
262+
decision_proceduret::resultt result = check_sat(conj, empty_ns);
265263

266264
// Require SAT
267265
if(result==decision_proceduret::resultt::D_ERROR)
@@ -288,9 +286,7 @@ SCENARIO("instantiate_not_contains",
288286
a_array};
289287

290288
// Create witness for axiom
291-
symbol_tablet symtab;
292-
const namespacet empty_ns(symtab);
293-
string_constraint_generatort generator(ns);
289+
string_constraint_generatort generator(empty_ns);
294290
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
295291
witnesses[vacuous] = generator.fresh_symbol("w", t.witness_type());
296292

@@ -306,14 +302,14 @@ SCENARIO("instantiate_not_contains",
306302
std::vector<exprt> lemmas = instantiate_not_contains(
307303
vacuous, product(index_set_a, index_set_a), witnesses);
308304

309-
const exprt conj=combine_lemmas(lemmas, ns);
310-
const std::string info=create_info(lemmas, ns);
305+
const exprt conj = combine_lemmas(lemmas, empty_ns);
306+
const std::string info = create_info(lemmas, empty_ns);
311307
INFO(info);
312308

313309
THEN("the conjunction of instantiations is SAT")
314310
{
315311
// Check if SAT
316-
decision_proceduret::resultt result=check_sat(conj, ns);
312+
decision_proceduret::resultt result = check_sat(conj, empty_ns);
317313

318314
// Require SAT
319315
if(result==decision_proceduret::resultt::D_ERROR)
@@ -340,9 +336,7 @@ SCENARIO("instantiate_not_contains",
340336
b_array};
341337

342338
// Create witness for axiom
343-
symbol_tablet symtab;
344-
const namespacet ns(symtab);
345-
string_constraint_generatort generator(ns);
339+
string_constraint_generatort generator(empty_ns);
346340
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
347341
witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
348342

@@ -359,14 +353,14 @@ SCENARIO("instantiate_not_contains",
359353
std::vector<exprt> lemmas = instantiate_not_contains(
360354
trivial, product(index_set_a, index_set_b), witnesses);
361355

362-
const exprt conj=combine_lemmas(lemmas, ns);
363-
const std::string info=create_info(lemmas, ns);
356+
const exprt conj = combine_lemmas(lemmas, empty_ns);
357+
const std::string info = create_info(lemmas, empty_ns);
364358
INFO(info);
365359

366360
THEN("the conjunction of instantiations is UNSAT")
367361
{
368362
// Check if SAT
369-
decision_proceduret::resultt result=check_sat(conj, ns);
363+
decision_proceduret::resultt result = check_sat(conj, empty_ns);
370364

371365
// Require UNSAT
372366
if(result==decision_proceduret::resultt::D_ERROR)
@@ -393,9 +387,7 @@ SCENARIO("instantiate_not_contains",
393387
empty_array};
394388

395389
// Create witness for axiom
396-
symbol_tablet symtab;
397-
const namespacet empty_ns(symtab);
398-
string_constraint_generatort generator(ns);
390+
string_constraint_generatort generator(empty_ns);
399391
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
400392
witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
401393

@@ -413,14 +405,14 @@ SCENARIO("instantiate_not_contains",
413405
std::vector<exprt> lemmas = instantiate_not_contains(
414406
trivial, product(index_set_a, index_set_empty), witnesses);
415407

416-
const exprt conj=combine_lemmas(lemmas, ns);
417-
const std::string info=create_info(lemmas, ns);
408+
const exprt conj = combine_lemmas(lemmas, empty_ns);
409+
const std::string info = create_info(lemmas, empty_ns);
418410
INFO(info);
419411

420412
THEN("the conjunction of instantiations is UNSAT")
421413
{
422414
// Check if SAT
423-
decision_proceduret::resultt result=check_sat(conj, ns);
415+
decision_proceduret::resultt result = check_sat(conj, empty_ns);
424416

425417
// Require UNSAT
426418
if(result==decision_proceduret::resultt::D_ERROR)
@@ -448,10 +440,7 @@ SCENARIO("instantiate_not_contains",
448440
ab_array};
449441

450442
// Create witness for axiom
451-
symbol_tablet symtab;
452-
const namespacet empty_ns(symtab);
453-
454-
string_constraint_generatort generator(ns);
443+
string_constraint_generatort generator(empty_ns);
455444
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
456445
witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
457446

@@ -467,14 +456,14 @@ SCENARIO("instantiate_not_contains",
467456
std::vector<exprt> lemmas = instantiate_not_contains(
468457
trivial, product(index_set_ab, index_set_ab), witnesses);
469458

470-
const exprt conj=combine_lemmas(lemmas, ns);
471-
const std::string info=create_info(lemmas, ns);
459+
const exprt conj = combine_lemmas(lemmas, empty_ns);
460+
const std::string info = create_info(lemmas, empty_ns);
472461
INFO(info);
473462

474463
THEN("the conjunction of instantiations is UNSAT")
475464
{
476465
// Check if SAT
477-
decision_proceduret::resultt result=check_sat(conj, ns);
466+
decision_proceduret::resultt result = check_sat(conj, empty_ns);
478467

479468
// Require UNSAT
480469
if(result==decision_proceduret::resultt::D_ERROR)
@@ -502,9 +491,7 @@ SCENARIO("instantiate_not_contains",
502491
cd_array};
503492

504493
// Create witness for axiom
505-
symbol_tablet symtab;
506-
const namespacet empty_ns(symtab);
507-
string_constraint_generatort generator(ns);
494+
string_constraint_generatort generator(empty_ns);
508495
std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
509496
witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
510497

@@ -521,14 +508,14 @@ SCENARIO("instantiate_not_contains",
521508
std::vector<exprt> lemmas = instantiate_not_contains(
522509
trivial, product(index_set_ab, index_set_cd), witnesses);
523510

524-
const exprt conj=combine_lemmas(lemmas, ns);
525-
const std::string info=create_info(lemmas, ns);
511+
const exprt conj = combine_lemmas(lemmas, empty_ns);
512+
const std::string info = create_info(lemmas, empty_ns);
526513
INFO(info);
527514

528515
THEN("the conjunction of instantiations is SAT")
529516
{
530517
// Check if SAT
531-
decision_proceduret::resultt result=check_sat(conj, ns);
518+
decision_proceduret::resultt result = check_sat(conj, empty_ns);
532519

533520
// Require UNSAT
534521
if(result==decision_proceduret::resultt::D_ERROR)

0 commit comments

Comments
 (0)