Skip to content

Handle all enum values in switch/case [blocks: #2310] #2548

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
May 1, 2019
Merged

Handle all enum values in switch/case [blocks: #2310] #2548

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
81cd230
Handle all enum values in switch/case
tautschnig Jun 20, 2018
5e1c7bf
Add -Wswitch-enum to default GCC/Clang build options
tautschnig Jul 9, 2018
87e86bb
Disable clang-format for recently touched switch statements
tautschnig Nov 7, 2018
81fb35f
clang-format switch statements touched in this PR
tautschnig Nov 8, 2018
d28968c
Annotate missed cases in the transform functions of various domains
Mar 4, 2019
93b2371
Disable a number of invariants that currently fail
tautschnig Mar 4, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
set(CMAKE_CXX_FLAGS_RELEASE "-O2")
set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g")
# Enable lots of warnings
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wno-deprecated-declarations")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wno-deprecated-declarations -Wswitch-enum")
elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
# This would be the place to enable warnings for Windows builds, although
# config.inc doesn't seem to do that currently
Expand Down
66 changes: 33 additions & 33 deletions jbmc/src/java_bytecode/java_bytecode_language.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -793,41 +793,41 @@ bool java_bytecode_languaget::typecheck(
// that are reachable from this entry point.
switch(lazy_methods_mode)
{
case LAZY_METHODS_MODE_CONTEXT_INSENSITIVE:
// ci = context-insensitive
if(do_ci_lazy_method_conversion(symbol_table))
return true;
break;
case LAZY_METHODS_MODE_EAGER:
{
symbol_table_buildert symbol_table_builder =
symbol_table_buildert::wrap(symbol_table);
case LAZY_METHODS_MODE_CONTEXT_INSENSITIVE:
// ci = context-insensitive
if(do_ci_lazy_method_conversion(symbol_table))
return true;
break;
case LAZY_METHODS_MODE_EAGER:
{
symbol_table_buildert symbol_table_builder =
symbol_table_buildert::wrap(symbol_table);

journalling_symbol_tablet journalling_symbol_table =
journalling_symbol_tablet::wrap(symbol_table_builder);
journalling_symbol_tablet journalling_symbol_table =
journalling_symbol_tablet::wrap(symbol_table_builder);

// Convert all synthetic methods:
for(const auto &function_id_and_type : synthetic_methods)
{
convert_single_method(
function_id_and_type.first, journalling_symbol_table);
}
// Convert all methods for which we have bytecode now
for(const auto &method_sig : method_bytecode)
{
convert_single_method(method_sig.first, journalling_symbol_table);
}
// Now convert all newly added string methods
for(const auto &fn_name : journalling_symbol_table.get_inserted())
{
if(string_preprocess.implements_function(fn_name))
convert_single_method(fn_name, symbol_table);
}
}
break;
default:
// Our caller is in charge of elaborating methods on demand.
break;
// Convert all synthetic methods:
for(const auto &function_id_and_type : synthetic_methods)
{
convert_single_method(
function_id_and_type.first, journalling_symbol_table);
}
// Convert all methods for which we have bytecode now
for(const auto &method_sig : method_bytecode)
{
convert_single_method(method_sig.first, journalling_symbol_table);
}
// Now convert all newly added string methods
for(const auto &fn_name : journalling_symbol_table.get_inserted())
{
if(string_preprocess.implements_function(fn_name))
convert_single_method(fn_name, symbol_table);
}
}
break;
case LAZY_METHODS_MODE_EXTERNAL_DRIVER:
// Our caller is in charge of elaborating methods on demand.
break;
}

// now instrument runtime exceptions
Expand Down
5 changes: 3 additions & 2 deletions jbmc/src/miniz/miniz.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7105,8 +7105,9 @@ const char *mz_zip_get_error_string(mz_zip_error mz_err)
return "validation failed";
case MZ_ZIP_WRITE_CALLBACK_FAILED:
return "write calledback failed";
default:
break;
case MZ_ZIP_TOTAL_ERRORS:
// not an actual error, just the maximum index
break;
}

return "unknown error";
Expand Down
24 changes: 21 additions & 3 deletions src/analyses/custom_bitvector_analysis.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -536,9 +536,27 @@ void custom_bitvector_domaint::transform(
}
break;

default:
{
}
case CATCH:
case THROW:
DATA_INVARIANT(false, "Exceptions must be removed before analysis");
break;
case RETURN:
DATA_INVARIANT(false, "Returns must be removed before analysis");
break;
case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
case ATOMIC_END: // Ignoring is a valid over-approximation
case END_FUNCTION: // No action required
case LOCATION: // No action required
case START_THREAD: // Require a concurrent analysis at higher level
case END_THREAD: // Require a concurrent analysis at higher level
case SKIP: // No action required
case ASSERT: // No action required
case ASSUME: // Ignoring is a valid over-approximation
break;
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
DATA_INVARIANT(false, "Only complete instructions can be analyzed");
break;
}
}

Expand Down
132 changes: 68 additions & 64 deletions src/analyses/escape_analysis.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -253,9 +253,33 @@ void escape_domaint::transform(
// This is the edge to the call site.
break;

default:
{
}
case GOTO: // Ignoring the guard is a valid over-approximation
break;
case CATCH:
case THROW:
DATA_INVARIANT(false, "Exceptions must be removed before analysis");
break;
case RETURN:
DATA_INVARIANT(false, "Returns must be removed before analysis");
break;
case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
case ATOMIC_END: // Ignoring is a valid over-approximation
case LOCATION: // No action required
case START_THREAD: // Require a concurrent analysis at higher level
case END_THREAD: // Require a concurrent analysis at higher level
case ASSERT: // No action required
case ASSUME: // Ignoring is a valid over-approximation
case SKIP: // No action required
break;
case OTHER:
#if 0
DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
#endif
break;
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
DATA_INVARIANT(false, "Only complete instructions can be analyzed");
break;
}
}

Expand Down Expand Up @@ -444,78 +468,58 @@ void escape_analysist::instrument(

const goto_programt::instructiont &instruction=*i_it;

switch(instruction.type)
if(instruction.type == ASSIGN)
{
case ASSIGN:
{
const code_assignt &code_assign=to_code_assign(instruction.code);

std::set<irep_idt> cleanup_functions;
operator[](i_it).check_lhs(code_assign.lhs(), cleanup_functions);
insert_cleanup(
f_it->second,
i_it,
code_assign.lhs(),
cleanup_functions,
false,
ns);
}
break;
const code_assignt &code_assign = to_code_assign(instruction.code);

case DEAD:
{
const code_deadt &code_dead=to_code_dead(instruction.code);
std::set<irep_idt> cleanup_functions;
operator[](i_it).check_lhs(code_assign.lhs(), cleanup_functions);
insert_cleanup(
f_it->second, i_it, code_assign.lhs(), cleanup_functions, false, ns);
}
else if(instruction.type == DEAD)
{
const code_deadt &code_dead = to_code_dead(instruction.code);

std::set<irep_idt> cleanup_functions1;
std::set<irep_idt> cleanup_functions1;

escape_domaint &d=operator[](i_it);
escape_domaint &d = operator[](i_it);

const escape_domaint::cleanup_mapt::const_iterator m_it=
d.cleanup_map.find("&"+id2string(code_dead.get_identifier()));
const escape_domaint::cleanup_mapt::const_iterator m_it =
d.cleanup_map.find("&" + id2string(code_dead.get_identifier()));

// does it have a cleanup function for the object?
if(m_it!=d.cleanup_map.end())
{
cleanup_functions1.insert(
m_it->second.cleanup_functions.begin(),
m_it->second.cleanup_functions.end());
}
// does it have a cleanup function for the object?
if(m_it != d.cleanup_map.end())
{
cleanup_functions1.insert(
m_it->second.cleanup_functions.begin(),
m_it->second.cleanup_functions.end());
}

std::set<irep_idt> cleanup_functions2;

d.check_lhs(code_dead.symbol(), cleanup_functions2);

insert_cleanup(
f_it->second,
i_it,
code_dead.symbol(),
cleanup_functions1,
true,
ns);
insert_cleanup(
f_it->second,
i_it,
code_dead.symbol(),
cleanup_functions2,
false,
ns);

for(const auto &c : cleanup_functions1)
{
(void)c;
i_it++;
}
std::set<irep_idt> cleanup_functions2;

for(const auto &c : cleanup_functions2)
{
(void)c;
i_it++;
}
d.check_lhs(code_dead.symbol(), cleanup_functions2);

insert_cleanup(
f_it->second, i_it, code_dead.symbol(), cleanup_functions1, true, ns);
insert_cleanup(
f_it->second,
i_it,
code_dead.symbol(),
cleanup_functions2,
false,
ns);

for(const auto &c : cleanup_functions1)
{
(void)c;
i_it++;
}
break;

default:
for(const auto &c : cleanup_functions2)
{
(void)c;
i_it++;
}
}
}
Expand Down
58 changes: 41 additions & 17 deletions src/analyses/global_may_alias.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,32 +106,56 @@ void global_may_alias_domaint::transform(
switch(instruction.type)
{
case ASSIGN:
{
const code_assignt &code_assign=to_code_assign(instruction.code);
{
const code_assignt &code_assign = to_code_assign(instruction.code);

std::set<irep_idt> rhs_aliases;
get_rhs_aliases(code_assign.rhs(), rhs_aliases);
assign_lhs_aliases(code_assign.lhs(), rhs_aliases);
}
std::set<irep_idt> rhs_aliases;
get_rhs_aliases(code_assign.rhs(), rhs_aliases);
assign_lhs_aliases(code_assign.lhs(), rhs_aliases);
break;
}

case DECL:
{
const code_declt &code_decl=to_code_decl(instruction.code);
aliases.isolate(code_decl.get_identifier());
}
{
const code_declt &code_decl = to_code_decl(instruction.code);
aliases.isolate(code_decl.get_identifier());
break;
}

case DEAD:
{
const code_deadt &code_dead=to_code_dead(instruction.code);
aliases.isolate(code_dead.get_identifier());
}
{
const code_deadt &code_dead = to_code_dead(instruction.code);
aliases.isolate(code_dead.get_identifier());
break;
}

default:
{
}
case FUNCTION_CALL: // Probably safe
case GOTO: // Ignoring the guard is a valid over-approximation
break;
case CATCH:
case THROW:
DATA_INVARIANT(false, "Exceptions must be removed before analysis");
break;
case RETURN:
DATA_INVARIANT(false, "Returns must be removed before analysis");
break;
case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
case ATOMIC_END: // Ignoring is a valid over-approximation
case LOCATION: // No action required
case START_THREAD: // Require a concurrent analysis at higher level
case END_THREAD: // Require a concurrent analysis at higher level
case ASSERT: // No action required
case ASSUME: // Ignoring is a valid over-approximation
case SKIP: // No action required
case END_FUNCTION: // No action required
break;
case OTHER:
DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
break;
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
DATA_INVARIANT(false, "Only complete instructions can be analyzed");
break;
}
}

Expand Down
Loading