Skip to content

Commit e0fc29e

Browse files
tautschnigtautschnig
committed
Handle all enum values in switch/case
1 parent 7c4b5aa commit e0fc29e

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

57 files changed

+646
-280
lines changed

‎src/analyses/custom_bitvector_analysis.cpp

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -536,7 +536,20 @@ void custom_bitvector_domaint::transform(
536536
}
537537
break;
538538

539-
default:
539+
case CATCH:
540+
case THROW:
541+
case RETURN:
542+
case ATOMIC_BEGIN:
543+
case ATOMIC_END:
544+
case END_FUNCTION:
545+
case LOCATION:
546+
case START_THREAD:
547+
case END_THREAD:
548+
case SKIP:
549+
case ASSERT:
550+
case ASSUME:
551+
case INCOMPLETE_GOTO:
552+
case NO_INSTRUCTION_TYPE:
540553
{
541554
}
542555
}

‎src/analyses/escape_analysis.cpp

Lines changed: 33 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -247,7 +247,21 @@ void escape_domaint::transform(
247247
// This is the edge to the call site.
248248
break;
249249

250-
default:
250+
case GOTO:
251+
case CATCH:
252+
case THROW:
253+
case RETURN:
254+
case ATOMIC_BEGIN:
255+
case ATOMIC_END:
256+
case LOCATION:
257+
case START_THREAD:
258+
case END_THREAD:
259+
case ASSERT:
260+
case ASSUME:
261+
case SKIP:
262+
case OTHER:
263+
case INCOMPLETE_GOTO:
264+
case NO_INSTRUCTION_TYPE:
251265
{
252266
}
253267
}
@@ -510,7 +524,24 @@ void escape_analysist::instrument(
510524
}
511525
break;
512526

513-
default:
527+
case FUNCTION_CALL:
528+
case DECL:
529+
case GOTO:
530+
case CATCH:
531+
case THROW:
532+
case RETURN:
533+
case ATOMIC_BEGIN:
534+
case ATOMIC_END:
535+
case LOCATION:
536+
case START_THREAD:
537+
case END_THREAD:
538+
case ASSERT:
539+
case ASSUME:
540+
case SKIP:
541+
case END_FUNCTION:
542+
case OTHER:
543+
case INCOMPLETE_GOTO:
544+
case NO_INSTRUCTION_TYPE:
514545
{
515546
}
516547
}

‎src/analyses/global_may_alias.cpp

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,23 @@ void global_may_alias_domaint::transform(
112112
}
113113
break;
114114

115-
default:
115+
case FUNCTION_CALL:
116+
case GOTO:
117+
case CATCH:
118+
case THROW:
119+
case RETURN:
120+
case ATOMIC_BEGIN:
121+
case ATOMIC_END:
122+
case LOCATION:
123+
case START_THREAD:
124+
case END_THREAD:
125+
case ASSERT:
126+
case ASSUME:
127+
case SKIP:
128+
case END_FUNCTION:
129+
case OTHER:
130+
case INCOMPLETE_GOTO:
131+
case NO_INSTRUCTION_TYPE:
116132
{
117133
}
118134
}

‎src/analyses/interval_domain.cpp

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,20 @@ void interval_domaint::transform(
106106
}
107107
break;
108108

109-
default:
109+
case CATCH:
110+
case THROW:
111+
case RETURN:
112+
case ATOMIC_BEGIN:
113+
case ATOMIC_END:
114+
case END_FUNCTION:
115+
case START_THREAD:
116+
case END_THREAD:
117+
case ASSERT:
118+
case LOCATION:
119+
case SKIP:
120+
case OTHER:
121+
case INCOMPLETE_GOTO:
122+
case NO_INSTRUCTION_TYPE:
110123
{
111124
}
112125
}

‎src/analyses/invariant_set_domain.cpp

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,17 @@ void invariant_set_domaint::transform(
7474
invariant_set.make_threaded();
7575
break;
7676

77-
default:
77+
case CATCH:
78+
case THROW:
79+
case DEAD:
80+
case ATOMIC_BEGIN:
81+
case ATOMIC_END:
82+
case END_FUNCTION:
83+
case LOCATION:
84+
case END_THREAD:
85+
case SKIP:
86+
case INCOMPLETE_GOTO:
87+
case NO_INSTRUCTION_TYPE:
7888
{
7989
// do nothing
8090
}

‎src/analyses/local_bitvector_analysis.cpp

Lines changed: 16 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -310,7 +310,22 @@ void local_bitvector_analysist::build()
310310
}
311311
break;
312312

313-
default:
313+
case CATCH:
314+
case THROW:
315+
case RETURN:
316+
case ATOMIC_BEGIN:
317+
case ATOMIC_END:
318+
case LOCATION:
319+
case START_THREAD:
320+
case END_THREAD:
321+
case SKIP:
322+
case OTHER:
323+
case ASSERT:
324+
case ASSUME:
325+
case GOTO:
326+
case END_FUNCTION:
327+
case INCOMPLETE_GOTO:
328+
case NO_INSTRUCTION_TYPE:
314329
{
315330
}
316331
}

‎src/analyses/local_cfg.cpp

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,21 @@ void local_cfgt::build(const goto_programt &goto_program)
7373
case END_THREAD:
7474
break; // no successor
7575

76-
default:
76+
case CATCH:
77+
case RETURN:
78+
case ATOMIC_BEGIN:
79+
case ATOMIC_END:
80+
case LOCATION:
81+
case SKIP:
82+
case OTHER:
83+
case ASSERT:
84+
case ASSUME:
85+
case FUNCTION_CALL:
86+
case DECL:
87+
case DEAD:
88+
case ASSIGN:
89+
case INCOMPLETE_GOTO:
90+
case NO_INSTRUCTION_TYPE:
7791
node.successors.push_back(loc_nr+1);
7892
}
7993
}

‎src/analyses/local_may_alias.cpp

Lines changed: 16 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -418,7 +418,22 @@ void local_may_aliast::build(const goto_functiont &goto_function)
418418
}
419419
break;
420420

421-
default:
421+
case CATCH:
422+
case THROW:
423+
case RETURN:
424+
case GOTO:
425+
case START_THREAD:
426+
case END_THREAD:
427+
case ATOMIC_BEGIN:
428+
case ATOMIC_END:
429+
case LOCATION:
430+
case SKIP:
431+
case END_FUNCTION:
432+
case OTHER:
433+
case ASSERT:
434+
case ASSUME:
435+
case INCOMPLETE_GOTO:
436+
case NO_INSTRUCTION_TYPE:
422437
{
423438
}
424439
}

‎src/analyses/local_safe_pointers.cpp

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -109,6 +109,9 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
109109
case RETURN:
110110
case THROW:
111111
case CATCH:
112+
case END_FUNCTION:
113+
case ATOMIC_BEGIN:
114+
case ATOMIC_END:
112115
break;
113116

114117
// Possible checks:
@@ -142,7 +145,13 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
142145
// Otherwise fall through to...
143146
}
144147

145-
default:
148+
case ASSIGN:
149+
case START_THREAD:
150+
case END_THREAD:
151+
case FUNCTION_CALL:
152+
case OTHER:
153+
case INCOMPLETE_GOTO:
154+
case NO_INSTRUCTION_TYPE:
146155
// Pessimistically assume all other instructions might overwrite any
147156
// pointer with a possibly-null value.
148157
checked_expressions.clear();

‎src/analyses/uncaught_exceptions_analysis.cpp

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -126,7 +126,23 @@ void uncaught_exceptions_domaint::transform(
126126
join(uea.exceptions_map[function_name]);
127127
break;
128128
}
129-
default:
129+
case DECL:
130+
case DEAD:
131+
case ASSIGN:
132+
case RETURN:
133+
case GOTO:
134+
case ATOMIC_BEGIN:
135+
case ATOMIC_END:
136+
case START_THREAD:
137+
case END_THREAD:
138+
case END_FUNCTION:
139+
case ASSERT:
140+
case ASSUME:
141+
case LOCATION:
142+
case SKIP:
143+
case OTHER:
144+
case INCOMPLETE_GOTO:
145+
case NO_INSTRUCTION_TYPE:
130146
{}
131147
}
132148
}

‎src/analyses/uninitialized_domain.cpp

Lines changed: 19 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -27,31 +27,26 @@ void uninitialized_domaint::transform(
2727
if(has_values.is_false())
2828
return;
2929

30-
switch(from->type)
30+
if(from->is_decl())
3131
{
32-
case DECL:
33-
{
34-
const irep_idt &identifier=
35-
to_code_decl(from->code).get_identifier();
36-
const symbolt &symbol=ns.lookup(identifier);
37-
38-
if(!symbol.is_static_lifetime)
39-
uninitialized.insert(identifier);
40-
}
41-
break;
42-
43-
default:
44-
{
45-
std::list<exprt> read=expressions_read(*from);
46-
std::list<exprt> written=expressions_written(*from);
47-
48-
for(const auto &expr : written)
49-
assign(expr);
50-
51-
// we only care about the *first* uninitalized use
52-
for(const auto &expr : read)
53-
assign(expr);
54-
}
32+
const irep_idt &identifier=
33+
to_code_decl(from->code).get_identifier();
34+
const symbolt &symbol=ns.lookup(identifier);
35+
36+
if(!symbol.is_static_lifetime)
37+
uninitialized.insert(identifier);
38+
}
39+
else
40+
{
41+
std::list<exprt> read=expressions_read(*from);
42+
std::list<exprt> written=expressions_written(*from);
43+
44+
for(const auto &expr : written)
45+
assign(expr);
46+
47+
// we only care about the *first* uninitalized use
48+
for(const auto &expr : read)
49+
assign(expr);
5550
}
5651
}
5752

‎src/ansi-c/c_typecast.cpp

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -396,8 +396,13 @@ void c_typecastt::implicit_typecast_arithmetic(
396396
case RATIONAL: new_type=rational_typet(); break;
397397
case REAL: new_type=real_typet(); break;
398398
case INTEGER: new_type=integer_typet(); break;
399-
case COMPLEX: return; // do nothing
400-
default: return;
399+
case COMPLEX:
400+
case OTHER:
401+
case VOIDPTR:
402+
case FIXEDBV:
403+
case LARGE_UNSIGNED_INT:
404+
case LARGE_SIGNED_INT:
405+
return; // do nothing
401406
}
402407

403408
if(new_type!=expr_type)

‎src/cbmc/bmc.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -534,7 +534,7 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)
534534
report_failure();
535535
return resultt::UNSAFE;
536536

537-
default:
537+
case decision_proceduret::resultt::D_ERROR:
538538
if(options.get_bool_option("dimacs") ||
539539
options.get_option("outfile")!="")
540540
return resultt::SAFE;

‎src/cbmc/fault_localization.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -312,7 +312,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail()
312312
bmc.report_failure();
313313
return safety_checkert::resultt::UNSAFE;
314314

315-
default:
315+
case decision_proceduret::resultt::D_ERROR:
316316
error() << "decision procedure failed" << eom;
317317

318318
return safety_checkert::resultt::ERROR;

0 commit comments

Comments
 (0)