replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #2548 from tautschnig/vs-switch-case 

Handle all enum values in switch/case [blocks: #2310]
This commit is contained in:
Michael Tautschnig 2019-05-01 12:33:15 +03:00 committed by GitHub
parent 7293aca231 93b2371ff7
commit 07c5e1da0c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
57 changed files with 1047 additions and 619 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
CMakeLists.txt
View File

@ -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

66
jbmc/src/java_bytecode/java_bytecode_language.cpp
View File

@ -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

5
jbmc/src/miniz/miniz.cpp
View File

@ -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";

24
src/analyses/custom_bitvector_analysis.cpp
View File

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

138
src/analyses/escape_analysis.cpp
View File

@ -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;
}
}
@ -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);
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);
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;
escape_domaint &d = operator[](i_it);
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());
}
break;
case DEAD:
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)
{
const code_deadt &code_dead=to_code_dead(instruction.code);
std::set<irep_idt> cleanup_functions1;
escape_domaint &d=operator[](i_it);
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());
}
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++;
}
for(const auto &c : cleanup_functions2)
{
(void)c;
i_it++;
}
(void)c;
i_it++;
}
break;
default:
for(const auto &c : cleanup_functions2)
{
(void)c;
i_it++;
}
}
}

58
src/analyses/global_may_alias.cpp
View File

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

62
src/analyses/interval_domain.cpp
View File

@ -80,37 +80,59 @@ void interval_domaint::transform(
break;
case GOTO:
{
// Comparing iterators is safe as the target must be within the same list
// of instructions because this is a GOTO.
locationt next = from;
next++;
if(from->get_target() != next) // If equal then a skip
{
// Comparing iterators is safe as the target must be within the same list
// of instructions because this is a GOTO.
locationt next=from;
next++;
if(from->get_target() != next) // If equal then a skip
{
if(next == to)
assume(not_exprt(instruction.get_condition()), ns);
else
assume(instruction.get_condition(), ns);
}
if(next == to)
assume(not_exprt(instruction.get_condition()), ns);
else
assume(instruction.get_condition(), ns);
}
break;
}
case ASSUME:
assume(instruction.get_condition(), ns);
break;
case FUNCTION_CALL:
{
const code_function_callt &code_function_call=
to_code_function_call(instruction.code);
if(code_function_call.lhs().is_not_nil())
havoc_rec(code_function_call.lhs());
}
{
const code_function_callt &code_function_call =
to_code_function_call(instruction.code);
if(code_function_call.lhs().is_not_nil())
havoc_rec(code_function_call.lhs());
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 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 LOCATION: // No action required
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;
}
}

20
src/analyses/invariant_set_domain.cpp
View File

@ -75,9 +75,21 @@ void invariant_set_domaint::transform(
invariant_set.make_threaded();
break;
default:
{
// do nothing
}
case CATCH:
case THROW:
DATA_INVARIANT(false, "Exceptions must be removed before analysis");
break;
case DEAD: // No action required
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 END_THREAD: // Require a concurrent analysis at higher level
case SKIP: // No action required
break;
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
DATA_INVARIANT(false, "Only complete instructions can be analyzed");
break;
}
}

91
src/analyses/local_bitvector_analysis.cpp
View File

@ -269,48 +269,77 @@ void local_bitvector_analysist::build()
switch(instruction.type)
{
case ASSIGN:
{
const code_assignt &code_assign=to_code_assign(instruction.code);
assign_lhs(
code_assign.lhs(), code_assign.rhs(), loc_info_src, loc_info_dest);
}
{
const code_assignt &code_assign = to_code_assign(instruction.code);
assign_lhs(
code_assign.lhs(), code_assign.rhs(), loc_info_src, loc_info_dest);
break;
}
case DECL:
{
const code_declt &code_decl=to_code_decl(instruction.code);
assign_lhs(
code_decl.symbol(),
exprt(ID_uninitialized),
loc_info_src,
loc_info_dest);
}
{
const code_declt &code_decl = to_code_decl(instruction.code);
assign_lhs(
code_decl.symbol(),
exprt(ID_uninitialized),
loc_info_src,
loc_info_dest);
break;
}
case DEAD:
{
const code_deadt &code_dead=to_code_dead(instruction.code);
assign_lhs(
code_dead.symbol(),
exprt(ID_uninitialized),
loc_info_src,
loc_info_dest);
}
{
const code_deadt &code_dead = to_code_dead(instruction.code);
assign_lhs(
code_dead.symbol(),
exprt(ID_uninitialized),
loc_info_src,
loc_info_dest);
break;
}
case FUNCTION_CALL:
{
const code_function_callt &code_function_call=
to_code_function_call(instruction.code);
if(code_function_call.lhs().is_not_nil())
assign_lhs(
code_function_call.lhs(), nil_exprt(), loc_info_src, loc_info_dest);
}
{
const code_function_callt &code_function_call =
to_code_function_call(instruction.code);
if(code_function_call.lhs().is_not_nil())
assign_lhs(
code_function_call.lhs(), nil_exprt(), loc_info_src, loc_info_dest);
break;
}
default:
{
}
case CATCH:
case THROW:
#if 0
DATA_INVARIANT(false, "Exceptions must be removed before analysis");
break;
#endif
case RETURN:
#if 0
DATA_INVARIANT(false, "Returns must be removed before analysis");
break;
#endif
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 SKIP: // No action required
case ASSERT: // No action required
case ASSUME: // Ignoring is a valid over-approximation
case GOTO: // Ignoring the guard is a valid over-approximation
case END_FUNCTION: // 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;
}
for(const auto &succ : node.successors)

22
src/analyses/local_cfg.cpp
View File

@ -73,8 +73,26 @@ void local_cfgt::build(const goto_programt &goto_program)
case END_THREAD:
break; // no successor
default:
node.successors.push_back(loc_nr+1);
case CATCH:
case RETURN:
case ATOMIC_BEGIN:
case ATOMIC_END:
case LOCATION:
case SKIP:
case OTHER:
case ASSERT:
case ASSUME:
case FUNCTION_CALL:
case DECL:
case DEAD:
case ASSIGN:
node.successors.push_back(loc_nr + 1);
break;
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
DATA_INVARIANT(false, "Only complete instructions can be analyzed");
break;
}
}
}

99
src/analyses/local_may_alias.cpp
View File

@ -368,60 +368,85 @@ void local_may_aliast::build(const goto_functiont &goto_function)
switch(instruction.type)
{
case ASSIGN:
{
const code_assignt &code_assign=to_code_assign(instruction.code);
assign_lhs(
code_assign.lhs(), code_assign.rhs(), loc_info_src, loc_info_dest);
}
{
const code_assignt &code_assign = to_code_assign(instruction.code);
assign_lhs(
code_assign.lhs(), code_assign.rhs(), loc_info_src, loc_info_dest);
break;
}
case DECL:
{
const code_declt &code_decl=to_code_decl(instruction.code);
assign_lhs(
code_decl.symbol(), nil_exprt(), loc_info_src, loc_info_dest);
}
{
const code_declt &code_decl = to_code_decl(instruction.code);
assign_lhs(code_decl.symbol(), nil_exprt(), loc_info_src, loc_info_dest);
break;
}
case DEAD:
{
const code_deadt &code_dead=to_code_dead(instruction.code);
assign_lhs(
code_dead.symbol(), nil_exprt(), loc_info_src, loc_info_dest);
}
{
const code_deadt &code_dead = to_code_dead(instruction.code);
assign_lhs(code_dead.symbol(), nil_exprt(), loc_info_src, loc_info_dest);
break;
}
case FUNCTION_CALL:
{
const code_function_callt &code_function_call =
to_code_function_call(instruction.code);
if(code_function_call.lhs().is_not_nil())
assign_lhs(
code_function_call.lhs(), nil_exprt(), loc_info_src, loc_info_dest);
// this might invalidate all pointers that are
// a) local and dirty
// b) global
for(std::size_t i = 0; i < objects.size(); i++)
{
const code_function_callt &code_function_call=
to_code_function_call(instruction.code);
if(code_function_call.lhs().is_not_nil())
assign_lhs(
code_function_call.lhs(), nil_exprt(), loc_info_src, loc_info_dest);
// this might invalidate all pointers that are
// a) local and dirty
// b) global
for(std::size_t i=0; i<objects.size(); i++)
if(objects[i].id() == ID_symbol)
{
if(objects[i].id()==ID_symbol)
{
const irep_idt &identifier=
to_symbol_expr(objects[i]).get_identifier();
const irep_idt &identifier =
to_symbol_expr(objects[i]).get_identifier();
if(dirty(identifier) || !locals.is_local(identifier))
{
loc_info_dest.aliases.isolate(i);
loc_info_dest.aliases.make_union(i, unknown_object);
}
if(dirty(identifier) || !locals.is_local(identifier))
{
loc_info_dest.aliases.isolate(i);
loc_info_dest.aliases.make_union(i, unknown_object);
}
}
}
break;
}
default:
{
}
case CATCH:
case THROW:
DATA_INVARIANT(false, "Exceptions must be removed before analysis");
break;
case RETURN:
#if 0
DATA_INVARIANT(false, "Returns must be removed before analysis");
#endif
break;
case GOTO: // Ignoring the guard is a valid over-approximation
case START_THREAD: // Require a concurrent analysis at higher level
case END_THREAD: // Require a concurrent analysis at higher level
case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
case ATOMIC_END: // Ignoring is a valid over-approximation
case LOCATION: // No action required
case SKIP: // No action required
case END_FUNCTION: // No action required
case ASSERT: // No action required
case ASSUME: // Ignoring is a valid over-approximation
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;
}
for(local_cfgt::successorst::const_iterator

11
src/analyses/local_safe_pointers.cpp
View File

@ -119,6 +119,9 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
case RETURN:
case THROW:
case CATCH:
case END_FUNCTION:
case ATOMIC_BEGIN:
case ATOMIC_END:
break;
// Possible checks:
@ -163,7 +166,13 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
break;
default:
case ASSIGN:
case START_THREAD:
case END_THREAD:
case FUNCTION_CALL:
case OTHER:
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
// Pessimistically assume all other instructions might overwrite any
// pointer with a possibly-null value.
checked_expressions.clear();

31
src/analyses/uncaught_exceptions_analysis.cpp
View File

@ -125,8 +125,35 @@ void uncaught_exceptions_domaint::transform(
join(uea.exceptions_map[function_name]);
break;
}
default:
{}
case DECL: // Safe to ignore in this context
case DEAD: // Safe to ignore in this context
case ASSIGN: // Safe to ignore in this context
break;
case RETURN:
#if 0
DATA_INVARIANT(false, "Returns must be removed before analysis");
#endif
break;
case GOTO: // Ignoring the guard is a valid over-approximation
case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
case ATOMIC_END: // Ignoring is a valid over-approximation
case START_THREAD: // Require a concurrent analysis at higher level
case END_THREAD: // Require a concurrent analysis at higher level
case END_FUNCTION: // No action required
case ASSERT: // No action required
case ASSUME: // Ignoring is a valid over-approximation
case LOCATION: // No action required
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;
}
}

36
src/analyses/uninitialized_domain.cpp
View File

@ -29,31 +29,25 @@ void uninitialized_domaint::transform(
if(has_values.is_false())
return;
switch(from->type)
if(from->is_decl())
{
case DECL:
{
const irep_idt &identifier=
to_code_decl(from->code).get_identifier();
const symbolt &symbol=ns.lookup(identifier);
const irep_idt &identifier = to_code_decl(from->code).get_identifier();
const symbolt &symbol = ns.lookup(identifier);
if(!symbol.is_static_lifetime)
uninitialized.insert(identifier);
}
break;
if(!symbol.is_static_lifetime)
uninitialized.insert(identifier);
}
else
{
std::list<exprt> read = expressions_read(*from);
std::list<exprt> written = expressions_written(*from);
default:
{
std::list<exprt> read=expressions_read(*from);
std::list<exprt> written=expressions_written(*from);
for(const auto &expr : written)
assign(expr);
for(const auto &expr : written)
assign(expr);
// we only care about the *first* uninitalized use
for(const auto &expr : read)
assign(expr);
}
// we only care about the *first* uninitalized use
for(const auto &expr : read)
assign(expr);
}
}

9
src/ansi-c/c_typecast.cpp
View File

@ -417,8 +417,13 @@ void c_typecastt::implicit_typecast_arithmetic(
case RATIONAL: new_type=rational_typet(); break;
case REAL: new_type=real_typet(); break;
case INTEGER: new_type=integer_typet(); break;
case COMPLEX: return; // do nothing
default: return;
case COMPLEX:
case OTHER:
case VOIDPTR:
case FIXEDBV:
case LARGE_UNSIGNED_INT:
case LARGE_SIGNED_INT:
return; // do nothing
}
if(new_type != expr.type())

2
src/config.inc
View File

@ -5,7 +5,7 @@ BUILD_ENV = AUTO
ifeq ($(BUILD_ENV),MSVC)
#CXXFLAGS += /Wall /WX
else
CXXFLAGS += -Wall -pedantic -Werror -Wno-deprecated-declarations
CXXFLAGS += -Wall -pedantic -Werror -Wno-deprecated-declarations -Wswitch-enum
endif
# Select optimisation or debug info

4
src/cpp/cpp_id.cpp
View File

@ -99,6 +99,7 @@ std::ostream &operator<<(std::ostream &out, const cpp_idt &cpp_id)
std::ostream &operator<<(std::ostream &out, const cpp_idt::id_classt &id_class)
{
// clang-format off
switch(id_class)
{
case cpp_idt::id_classt::UNKNOWN: return out<<"UNKNOWN";
@ -111,8 +112,9 @@ std::ostream &operator<<(std::ostream &out, const cpp_idt::id_classt &id_class)
case cpp_idt::id_classt::BLOCK_SCOPE: return out<<"BLOCK_SCOPE";
case cpp_idt::id_classt::TEMPLATE_SCOPE: return out<<"TEMPLATE_SCOPE";
case cpp_idt::id_classt::NAMESPACE: return out<<"NAMESPACE";
default: return out << "(OTHER)";
case cpp_idt::id_classt::ENUM: return out<<"ENUM";
}
// clang-format on
UNREACHABLE;
}

5
src/cpp/cpp_typecheck_resolve.cpp
View File

@ -1680,9 +1680,8 @@ exprt cpp_typecheck_resolvet::resolve(
}
break;
default:
{
}
case wantt::BOTH:
break;
}
return result;

3
src/cpp/parse.cpp
View File

@ -1044,7 +1044,8 @@ bool Parser::rTemplateDecl(cpp_declarationt &decl)
decl.swap(body);
break;
default:
case num_tdks:
case tdk_unknown:
UNREACHABLE;
break;
}

228
src/goto-analyzer/taint_analysis.cpp
View File

@ -71,145 +71,137 @@ void taint_analysist::instrument(
goto_programt insert_before, insert_after;
switch(instruction.type)
if(instruction.is_function_call())
{
case FUNCTION_CALL:
const code_function_callt &function_call =
instruction.get_function_call();
const exprt &function = function_call.function();
if(function.id() == ID_symbol)
{
const code_function_callt &function_call =
instruction.get_function_call();
const exprt &function=function_call.function();
const irep_idt &identifier = to_symbol_expr(function).get_identifier();
if(function.id()==ID_symbol)
std::set<irep_idt> identifiers;
identifiers.insert(identifier);
irep_idt class_id = function.get(ID_C_class);
if(class_id.empty())
{
const irep_idt &identifier=
to_symbol_expr(function).get_identifier();
}
else
{
std::string suffix = std::string(
id2string(identifier), class_id.size(), std::string::npos);
std::set<irep_idt> identifiers;
class_hierarchyt::idst parents =
class_hierarchy.get_parents_trans(class_id);
for(const auto &p : parents)
identifiers.insert(id2string(p) + suffix);
}
identifiers.insert(identifier);
irep_idt class_id=function.get(ID_C_class);
if(class_id.empty())
for(const auto &rule : taint.rules)
{
bool match = false;
for(const auto &i : identifiers)
{
}
else
{
std::string suffix=
std::string(
id2string(identifier), class_id.size(), std::string::npos);
class_hierarchyt::idst parents=
class_hierarchy.get_parents_trans(class_id);
for(const auto &p : parents)
identifiers.insert(id2string(p)+suffix);
}
for(const auto &rule : taint.rules)
{
bool match=false;
for(const auto &i : identifiers)
if(i==rule.function_identifier ||
has_prefix(
id2string(i),
"java::"+id2string(rule.function_identifier)+":"))
{
match=true;
break;
}
if(match)
if(
i == rule.function_identifier ||
has_prefix(
id2string(i),
"java::" + id2string(rule.function_identifier) + ":"))
{
log.debug() << "MATCH " << rule.id << " on " << identifier
<< messaget::eom;
match = true;
break;
}
}
exprt where=nil_exprt();
if(match)
{
log.debug() << "MATCH " << rule.id << " on " << identifier
<< messaget::eom;
const code_typet &code_type=to_code_type(function.type());
exprt where = nil_exprt();
bool have_this=
!code_type.parameters().empty() &&
code_type.parameters().front().get_bool(ID_C_this);
const code_typet &code_type = to_code_type(function.type());
switch(rule.where)
bool have_this = !code_type.parameters().empty() &&
code_type.parameters().front().get_bool(ID_C_this);
switch(rule.where)
{
case taint_parse_treet::rulet::RETURN_VALUE:
{
const symbolt &return_value_symbol =
ns.lookup(id2string(identifier) + "#return_value");
where = return_value_symbol.symbol_expr();
break;
}
case taint_parse_treet::rulet::PARAMETER:
{
unsigned nr =
have_this ? rule.parameter_number : rule.parameter_number - 1;
if(function_call.arguments().size() > nr)
where = function_call.arguments()[nr];
break;
}
case taint_parse_treet::rulet::THIS:
if(have_this)
{
case taint_parse_treet::rulet::RETURN_VALUE:
{
const symbolt &return_value_symbol=
ns.lookup(id2string(identifier)+"#return_value");
where=return_value_symbol.symbol_expr();
}
break;
case taint_parse_treet::rulet::PARAMETER:
{
unsigned nr=
have_this?rule.parameter_number:rule.parameter_number-1;
if(function_call.arguments().size()>nr)
where=function_call.arguments()[nr];
}
break;
case taint_parse_treet::rulet::THIS:
if(have_this)
{
DATA_INVARIANT(
!function_call.arguments().empty(),
"`this` implies at least one argument in function call");
where=function_call.arguments()[0];
}
break;
DATA_INVARIANT(
!function_call.arguments().empty(),
"`this` implies at least one argument in function call");
where = function_call.arguments()[0];
}
break;
}
switch(rule.kind)
{
case taint_parse_treet::rulet::SOURCE:
{
codet code_set_may("set_may");
code_set_may.operands().resize(2);
code_set_may.op0()=where;
code_set_may.op1()=
address_of_exprt(string_constantt(rule.taint));
insert_after.add(goto_programt::make_other(
code_set_may, instruction.source_location));
}
break;
switch(rule.kind)
{
case taint_parse_treet::rulet::SOURCE:
{
codet code_set_may("set_may");
code_set_may.operands().resize(2);
code_set_may.op0() = where;
code_set_may.op1() =
address_of_exprt(string_constantt(rule.taint));
insert_after.add(goto_programt::make_other(
code_set_may, instruction.source_location));
break;
}
case taint_parse_treet::rulet::SINK:
{
binary_predicate_exprt get_may(
where,
"get_may",
address_of_exprt(string_constantt(rule.taint)));
goto_programt::targett t =
insert_before.add(goto_programt::make_assertion(
not_exprt(get_may), instruction.source_location));
t->source_location.set_property_class(
"taint rule "+id2string(rule.id));
t->source_location.set_comment(rule.message);
}
break;
case taint_parse_treet::rulet::SINK:
{
binary_predicate_exprt get_may(
where,
"get_may",
address_of_exprt(string_constantt(rule.taint)));
goto_programt::targett t =
insert_before.add(goto_programt::make_assertion(
not_exprt(get_may), instruction.source_location));
t->source_location.set_property_class(
"taint rule " + id2string(rule.id));
t->source_location.set_comment(rule.message);
break;
}
case taint_parse_treet::rulet::SANITIZER:
{
codet code_clear_may("clear_may");
code_clear_may.operands().resize(2);
code_clear_may.op0()=where;
code_clear_may.op1()=
address_of_exprt(string_constantt(rule.taint));
insert_after.add(goto_programt::make_other(
code_clear_may, instruction.source_location));
}
break;
}
case taint_parse_treet::rulet::SANITIZER:
{
codet code_clear_may("clear_may");
code_clear_may.operands().resize(2);
code_clear_may.op0() = where;
code_clear_may.op1() =
address_of_exprt(string_constantt(rule.taint));
insert_after.add(goto_programt::make_other(
code_clear_may, instruction.source_location));
break;
}
}
}
}
}
break;
default:
{
}
}
if(!insert_before.empty())

6
src/goto-cc/compile.cpp
View File

@ -293,7 +293,11 @@ bool compilet::find_library(const std::string &name)
<< eom;
return warning_is_fatal;
default:
case file_typet::THIN_ARCHIVE:
case file_typet::NORMAL_ARCHIVE:
case file_typet::SOURCE_FILE:
case file_typet::FAILED_TO_OPEN_FILE:
case file_typet::UNKNOWN:
break;
}
}

40
src/goto-instrument/cover_util.cpp
View File

@ -58,9 +58,23 @@ std::set<exprt> collect_conditions(const goto_programt::const_targett t)
case FUNCTION_CALL:
return collect_conditions(t->code);
default:
{
}
case CATCH:
case THROW:
case DEAD:
case DECL:
case RETURN:
case ATOMIC_BEGIN:
case ATOMIC_END:
case START_THREAD:
case END_THREAD:
case END_FUNCTION:
case LOCATION:
case OTHER:
case SKIP:
case ASSUME:
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
break;
}
return std::set<exprt>();
@ -125,9 +139,23 @@ std::set<exprt> collect_decisions(const goto_programt::const_targett t)
case FUNCTION_CALL:
return collect_decisions(t->code);
default:
{
}
case CATCH:
case THROW:
case DEAD:
case DECL:
case RETURN:
case ATOMIC_BEGIN:
case ATOMIC_END:
case START_THREAD:
case END_THREAD:
case END_FUNCTION:
case LOCATION:
case OTHER:
case SKIP:
case ASSUME:
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
break;
}
return std::set<exprt>();

21
src/goto-instrument/points_to.cpp
View File

@ -75,9 +75,24 @@ bool points_tot::transform(const cfgt::nodet &e)
// these are like assignments for the arguments
break;
default:
{
}
case CATCH:
case THROW:
case GOTO:
case DEAD:
case DECL:
case ATOMIC_BEGIN:
case ATOMIC_END:
case START_THREAD:
case END_THREAD:
case END_FUNCTION:
case LOCATION:
case OTHER:
case SKIP:
case ASSERT:
case ASSUME:
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
break;
}
return result;

2
src/goto-instrument/show_locations.cpp
View File

@ -58,7 +58,7 @@ void show_locations(
<< it->source_location << '\n';
break;
default:
case ui_message_handlert::uit::JSON_UI:
UNREACHABLE;
}
}

34
src/goto-programs/format_strings.cpp
View File

@ -257,7 +257,10 @@ optionalt<typet> get_type(const format_tokent &token)
else
return unsigned_long_long_int_type();
default:
case format_tokent::length_modifierst::LEN_t:
case format_tokent::length_modifierst::LEN_j:
case format_tokent::length_modifierst::LEN_L:
case format_tokent::length_modifierst::LEN_undef:
if(token.representation==format_tokent::representationt::SIGNED_DEC)
return signed_int_type();
else
@ -269,14 +272,27 @@ optionalt<typet> get_type(const format_tokent &token)
{
case format_tokent::length_modifierst::LEN_l: return double_type();
case format_tokent::length_modifierst::LEN_L: return long_double_type();
default: return float_type();
case format_tokent::length_modifierst::LEN_h:
case format_tokent::length_modifierst::LEN_hh:
case format_tokent::length_modifierst::LEN_j:
case format_tokent::length_modifierst::LEN_ll:
case format_tokent::length_modifierst::LEN_t:
case format_tokent::length_modifierst::LEN_undef:
return float_type();
}
case format_tokent::token_typet::CHAR:
switch(token.length_modifier)
{
case format_tokent::length_modifierst::LEN_l: return wchar_t_type();
default: return char_type();
case format_tokent::length_modifierst::LEN_h:
case format_tokent::length_modifierst::LEN_hh:
case format_tokent::length_modifierst::LEN_j:
case format_tokent::length_modifierst::LEN_L:
case format_tokent::length_modifierst::LEN_ll:
case format_tokent::length_modifierst::LEN_t:
case format_tokent::length_modifierst::LEN_undef:
return char_type();
}
case format_tokent::token_typet::POINTER:
@ -287,10 +303,18 @@ optionalt<typet> get_type(const format_tokent &token)
{
case format_tokent::length_modifierst::LEN_l:
return array_typet(wchar_t_type(), nil_exprt());
default: return array_typet(char_type(), nil_exprt());
case format_tokent::length_modifierst::LEN_h:
case format_tokent::length_modifierst::LEN_hh:
case format_tokent::length_modifierst::LEN_j:
case format_tokent::length_modifierst::LEN_L:
case format_tokent::length_modifierst::LEN_ll:
case format_tokent::length_modifierst::LEN_t:
case format_tokent::length_modifierst::LEN_undef:
return array_typet(char_type(), nil_exprt());
}
default:
case format_tokent::token_typet::TEXT:
case format_tokent::token_typet::UNKNOWN:
return {};
}

112
src/goto-programs/goto_program.cpp
View File

@ -215,7 +215,7 @@ std::ostream &goto_programt::output_instruction(
out << "END THREAD" << '\n';
break;
default:
case INCOMPLETE_GOTO:
UNREACHABLE;
}
@ -285,27 +285,38 @@ std::list<exprt> expressions_read(
break;
case FUNCTION_CALL:
{
const code_function_callt &function_call =
instruction.get_function_call();
forall_expr(it, function_call.arguments())
dest.push_back(*it);
if(function_call.lhs().is_not_nil())
parse_lhs_read(function_call.lhs(), dest);
}
{
const code_function_callt &function_call = instruction.get_function_call();
forall_expr(it, function_call.arguments())
dest.push_back(*it);
if(function_call.lhs().is_not_nil())
parse_lhs_read(function_call.lhs(), dest);
break;
}
case ASSIGN:
{
const code_assignt &assignment = instruction.get_assign();
dest.push_back(assignment.rhs());
parse_lhs_read(assignment.lhs(), dest);
}
{
const code_assignt &assignment = instruction.get_assign();
dest.push_back(assignment.rhs());
parse_lhs_read(assignment.lhs(), dest);
break;
}
default:
{
}
case CATCH:
case THROW:
case DEAD:
case DECL:
case ATOMIC_BEGIN:
case ATOMIC_END:
case START_THREAD:
case END_THREAD:
case END_FUNCTION:
case LOCATION:
case SKIP:
case OTHER:
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
break;
}
return dest;
@ -331,9 +342,25 @@ std::list<exprt> expressions_written(
dest.push_back(instruction.get_assign().lhs());
break;
default:
{
}
case CATCH:
case THROW:
case GOTO:
case RETURN:
case DEAD:
case DECL:
case ATOMIC_BEGIN:
case ATOMIC_END:
case START_THREAD:
case END_THREAD:
case END_FUNCTION:
case ASSERT:
case ASSUME:
case LOCATION:
case SKIP:
case OTHER:
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
break;
}
return dest;
@ -489,9 +516,11 @@ std::string as_string(
case END_THREAD:
return "END THREAD";
default:
case INCOMPLETE_GOTO:
UNREACHABLE;
}
UNREACHABLE;
}
/// Assign each loop in the goto program a unique index. Every backwards goto is
@ -969,7 +998,20 @@ void goto_programt::instructiont::transform(
}
break;
default:
case GOTO:
case ASSUME:
case ASSERT:
case SKIP:
case START_THREAD:
case END_THREAD:
case LOCATION:
case END_FUNCTION:
case ATOMIC_BEGIN:
case ATOMIC_END:
case THROW:
case CATCH:
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
if(has_condition())
{
auto new_condition = f(get_condition());
@ -1015,7 +1057,20 @@ void goto_programt::instructiont::apply(
}
break;
default:
case GOTO:
case ASSUME:
case ASSERT:
case SKIP:
case START_THREAD:
case END_THREAD:
case LOCATION:
case END_FUNCTION:
case ATOMIC_BEGIN:
case ATOMIC_END:
case THROW:
case CATCH:
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
if(has_condition())
f(get_condition());
}
@ -1108,8 +1163,15 @@ std::ostream &operator<<(std::ostream &out, goto_program_instruction_typet t)
case FUNCTION_CALL:
out << "FUNCTION_CALL";
break;
default:
out << "?";
case THROW:
out << "THROW";
break;
case CATCH:
out << "CATCH";
break;
case INCOMPLETE_GOTO:
out << "INCOMPLETE_GOTO";
break;
}
return out;

16
src/goto-programs/goto_trace.cpp
View File

@ -65,6 +65,7 @@ void goto_trace_stept::output(
{
out << "*** ";
// clang-format off
switch(type)
{
case goto_trace_stept::typet::ASSERT: out << "ASSERT"; break;
@ -85,10 +86,12 @@ void goto_trace_stept::output(
case goto_trace_stept::typet::FUNCTION_CALL: out << "FUNCTION CALL"; break;
case goto_trace_stept::typet::FUNCTION_RETURN:
out << "FUNCTION RETURN"; break;
default:
out << "unknown type: " << static_cast<int>(type) << std::endl;
UNREACHABLE;
case goto_trace_stept::typet::MEMORY_BARRIER: out << "MEMORY_BARRIER"; break;
case goto_trace_stept::typet::SPAWN: out << "SPAWN"; break;
case goto_trace_stept::typet::CONSTRAINT: out << "CONSTRAINT"; break;
case goto_trace_stept::typet::NONE: out << "NONE"; break;
}
// clang-format on
if(is_assert() || is_assume() || is_goto())
out << " (" << cond_value << ')';
@ -479,9 +482,12 @@ void show_compact_goto_trace(
case goto_trace_stept::typet::ATOMIC_BEGIN:
case goto_trace_stept::typet::ATOMIC_END:
case goto_trace_stept::typet::DEAD:
case goto_trace_stept::typet::CONSTRAINT:
case goto_trace_stept::typet::SHARED_READ:
case goto_trace_stept::typet::SHARED_WRITE:
break;
default:
case goto_trace_stept::typet::NONE:
UNREACHABLE;
}
}
@ -678,7 +684,7 @@ void show_full_goto_trace(
case goto_trace_stept::typet::CONSTRAINT:
case goto_trace_stept::typet::SHARED_READ:
case goto_trace_stept::typet::SHARED_WRITE:
default:
case goto_trace_stept::typet::NONE:
UNREACHABLE;
}
}

3
src/goto-programs/interpreter.cpp
View File

@ -359,7 +359,8 @@ void interpretert::step()
break;
case CATCH:
break;
default:
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
throw "encountered instruction with undefined instruction type";
}
pc=next_pc;

13
src/goto-programs/json_goto_trace.h
View File

@ -174,7 +174,18 @@ void convert(
}
break;
default:
case goto_trace_stept::typet::ATOMIC_BEGIN:
case goto_trace_stept::typet::ATOMIC_END:
case goto_trace_stept::typet::DEAD:
case goto_trace_stept::typet::LOCATION:
case goto_trace_stept::typet::GOTO:
case goto_trace_stept::typet::ASSUME:
case goto_trace_stept::typet::MEMORY_BARRIER:
case goto_trace_stept::typet::SPAWN:
case goto_trace_stept::typet::SHARED_READ:
case goto_trace_stept::typet::SHARED_WRITE:
case goto_trace_stept::typet::CONSTRAINT:
case goto_trace_stept::typet::NONE:
if(source_location != previous_source_location)
{
json_objectt &json_location_only = dest_array.push_back().make_object();

4
src/goto-programs/show_symbol_table.cpp
View File

@ -295,8 +295,6 @@ void show_symbol_table(
case ui_message_handlert::uit::JSON_UI:
show_symbol_table_json_ui(symbol_table, ui);
default:
break;
}
}
@ -322,7 +320,7 @@ void show_symbol_table_brief(
show_symbol_table_xml_ui();
break;
default:
case ui_message_handlert::uit::JSON_UI:
show_symbol_table_brief_json_ui(symbol_table, ui);
break;
}

18
src/goto-programs/string_instrumentation.cpp
View File

@ -203,19 +203,8 @@ void string_instrumentationt::instrument(
goto_programt &dest,
goto_programt::targett it)
{
switch(it->type)
{
case ASSIGN:
break;
case FUNCTION_CALL:
if(it->is_function_call())
do_function_call(dest, it);
break;
default:
{
}
}
}
void string_instrumentationt::do_function_call(
@ -549,7 +538,10 @@ void string_instrumentationt::do_format_string_write(
// nothing
break;
}
default: // everything else
case format_tokent::token_typet::POINTER:
case format_tokent::token_typet::CHAR:
case format_tokent::token_typet::FLOAT:
case format_tokent::token_typet::INT:
{
const exprt &argument=arguments[argument_start_inx+args];
const dereference_exprt lhs{argument};

60
src/goto-programs/vcd_goto_trace.cpp
View File

@ -113,44 +113,40 @@ void output_vcd(
for(const auto &step : goto_trace.steps)
{
switch(step.type)
if(step.is_assignment())
{
case goto_trace_stept::typet::ASSIGNMENT:
auto lhs_object = step.get_lhs_object();
if(lhs_object.has_value())
{
auto lhs_object=step.get_lhs_object();
if(lhs_object.has_value())
irep_idt identifier = lhs_object->get_identifier();
const typet &type = lhs_object->type();
out << '#' << timestamp << "\n";
timestamp++;
const auto number = n.number(identifier);
// booleans are special in VCD
if(type.id() == ID_bool)
{
irep_idt identifier=lhs_object->get_identifier();
const typet &type=lhs_object->type();
out << '#' << timestamp << "\n";
timestamp++;
const auto number=n.number(identifier);
// booleans are special in VCD
if(type.id()==ID_bool)
{
if(step.full_lhs_value.is_true())
out << "1" << "V" << number << "\n";
else if(step.full_lhs_value.is_false())
out << "0" << "V" << number << "\n";
else
out << "x" << "V" << number << "\n";
}
if(step.full_lhs_value.is_true())
out << "1"
<< "V" << number << "\n";
else if(step.full_lhs_value.is_false())
out << "0"
<< "V" << number << "\n";
else
{
std::string binary=as_vcd_binary(step.full_lhs_value, ns);
if(!binary.empty())
out << "b" << binary << " V" << number << " " << "\n";
}
out << "x"
<< "V" << number << "\n";
}
}
break;
else
{
std::string binary = as_vcd_binary(step.full_lhs_value, ns);
default:
{
if(!binary.empty())
out << "b" << binary << " V" << number << " "
<< "\n";
}
}
}
}

181
src/goto-programs/xml_goto_trace.cpp
View File

@ -60,15 +60,23 @@ void convert(
case goto_trace_stept::typet::ASSIGNMENT:
case goto_trace_stept::typet::DECL:
{
auto lhs_object = step.get_lhs_object();
irep_idt identifier =
lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt();
xmlt &xml_assignment = dest.new_element("assignment");
if(!xml_location.name.empty())
xml_assignment.new_element().swap(xml_location);
{
auto lhs_object=step.get_lhs_object();
irep_idt identifier=
lhs_object.has_value()?lhs_object->get_identifier():irep_idt();
xmlt &xml_assignment=dest.new_element("assignment");
if(!xml_location.name.empty())
xml_assignment.new_element().swap(xml_location);
const symbolt *symbol;
if(
lhs_object.has_value() &&
!ns.lookup(lhs_object->get_identifier(), symbol))
{
const symbolt *symbol;
@ -84,77 +92,77 @@ void convert(
xml_assignment.new_element("type").data=type_string;
}
}
std::string full_lhs_string, full_lhs_value_string;
if(step.full_lhs.is_not_nil())
full_lhs_string=from_expr(ns, identifier, step.full_lhs);
if(step.full_lhs_value.is_not_nil())
full_lhs_value_string=
from_expr(ns, identifier, step.full_lhs_value);
xml_assignment.new_element("full_lhs").data=full_lhs_string;
xml_assignment.new_element("full_lhs_value").data=full_lhs_value_string;
xml_assignment.set_attribute_bool("hidden", step.hidden);
xml_assignment.set_attribute("thread", std::to_string(step.thread_nr));
xml_assignment.set_attribute("step_nr", std::to_string(step.step_nr));
xml_assignment.set_attribute("assignment_type",
step.assignment_type==
goto_trace_stept::assignment_typet::ACTUAL_PARAMETER?
"actual_parameter":"state");
}
std::string full_lhs_string, full_lhs_value_string;
if(step.full_lhs.is_not_nil())
full_lhs_string = from_expr(ns, identifier, step.full_lhs);
if(step.full_lhs_value.is_not_nil())
full_lhs_value_string = from_expr(ns, identifier, step.full_lhs_value);
xml_assignment.new_element("full_lhs").data = full_lhs_string;
xml_assignment.new_element("full_lhs_value").data = full_lhs_value_string;
xml_assignment.set_attribute_bool("hidden", step.hidden);
xml_assignment.set_attribute("thread", std::to_string(step.thread_nr));
xml_assignment.set_attribute("step_nr", std::to_string(step.step_nr));
xml_assignment.set_attribute(
"assignment_type",
step.assignment_type ==
goto_trace_stept::assignment_typet::ACTUAL_PARAMETER
? "actual_parameter"
: "state");
break;
}
case goto_trace_stept::typet::OUTPUT:
{
printf_formattert printf_formatter(ns);
printf_formatter(id2string(step.format_string), step.io_args);
std::string text = printf_formatter.as_string();
xmlt &xml_output = dest.new_element("output");
xml_output.new_element("text").data = text;
xml_output.set_attribute_bool("hidden", step.hidden);
xml_output.set_attribute("thread", std::to_string(step.thread_nr));
xml_output.set_attribute("step_nr", std::to_string(step.step_nr));
if(!xml_location.name.empty())
xml_output.new_element().swap(xml_location);
for(const auto &arg : step.io_args)
{
printf_formattert printf_formatter(ns);
printf_formatter(id2string(step.format_string), step.io_args);
std::string text=printf_formatter.as_string();
xmlt &xml_output=dest.new_element("output");
xml_output.new_element("text").data=text;
xml_output.set_attribute_bool("hidden", step.hidden);
xml_output.set_attribute("thread", std::to_string(step.thread_nr));
xml_output.set_attribute("step_nr", std::to_string(step.step_nr));
if(!xml_location.name.empty())
xml_output.new_element().swap(xml_location);
for(const auto &arg : step.io_args)
{
xml_output.new_element("value").data =
from_expr(ns, step.function_id, arg);
xml_output.new_element("value_expression").
new_element(xml(arg, ns));
}
xml_output.new_element("value").data =
from_expr(ns, step.function_id, arg);
xml_output.new_element("value_expression").new_element(xml(arg, ns));
}
break;
}
case goto_trace_stept::typet::INPUT:
{
xmlt &xml_input = dest.new_element("input");
xml_input.new_element("input_id").data = id2string(step.io_id);
xml_input.set_attribute_bool("hidden", step.hidden);
xml_input.set_attribute("thread", std::to_string(step.thread_nr));
xml_input.set_attribute("step_nr", std::to_string(step.step_nr));
for(const auto &arg : step.io_args)
{
xmlt &xml_input=dest.new_element("input");
xml_input.new_element("input_id").data=id2string(step.io_id);
xml_input.set_attribute_bool("hidden", step.hidden);
xml_input.set_attribute("thread", std::to_string(step.thread_nr));
xml_input.set_attribute("step_nr", std::to_string(step.step_nr));
for(const auto &arg : step.io_args)
{
xml_input.new_element("value").data =
from_expr(ns, step.function_id, arg);
xml_input.new_element("value_expression").
new_element(xml(arg, ns));
}
if(!xml_location.name.empty())
xml_input.new_element().swap(xml_location);
xml_input.new_element("value").data =
from_expr(ns, step.function_id, arg);
xml_input.new_element("value_expression").new_element(xml(arg, ns));
}
if(!xml_location.name.empty())
xml_input.new_element().swap(xml_location);
break;
}
case goto_trace_stept::typet::FUNCTION_CALL:
{
@ -174,31 +182,42 @@ void convert(
if(!xml_location.name.empty())
xml_call_return.new_element().swap(xml_location);
break;
}
break;
case goto_trace_stept::typet::FUNCTION_RETURN:
{
std::string tag = "function_return";
xmlt &xml_call_return=dest.new_element(tag);
{
std::string tag = "function_return";
xmlt &xml_call_return = dest.new_element(tag);
xml_call_return.set_attribute_bool("hidden", step.hidden);
xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
xml_call_return.set_attribute_bool("hidden", step.hidden);
xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
const symbolt &symbol = ns.lookup(step.called_function);
xmlt &xml_function=xml_call_return.new_element("function");
xml_function.set_attribute(
"display_name", id2string(symbol.display_name()));
xml_function.set_attribute("identifier", id2string(symbol.name));
xml_function.new_element()=xml(symbol.location);
const symbolt &symbol = ns.lookup(step.called_function);
xmlt &xml_function = xml_call_return.new_element("function");
xml_function.set_attribute(
"display_name", id2string(symbol.display_name()));
xml_function.set_attribute("identifier", id2string(symbol.name));
xml_function.new_element() = xml(symbol.location);
if(!xml_location.name.empty())
xml_call_return.new_element().swap(xml_location);
}
if(!xml_location.name.empty())
xml_call_return.new_element().swap(xml_location);
break;
}
default:
case goto_trace_stept::typet::ATOMIC_BEGIN:
case goto_trace_stept::typet::ATOMIC_END:
case goto_trace_stept::typet::MEMORY_BARRIER:
case goto_trace_stept::typet::SPAWN:
case goto_trace_stept::typet::SHARED_WRITE:
case goto_trace_stept::typet::SHARED_READ:
case goto_trace_stept::typet::CONSTRAINT:
case goto_trace_stept::typet::DEAD:
case goto_trace_stept::typet::LOCATION:
case goto_trace_stept::typet::GOTO:
case goto_trace_stept::typet::ASSUME:
case goto_trace_stept::typet::NONE:
if(source_location!=previous_source_location)
{
// just the source location

4
src/goto-symex/slice.cpp
View File

@ -104,7 +104,7 @@ void symex_slicet::slice(SSA_stept &SSA_step)
// ignore for now
break;
default:
case goto_trace_stept::typet::NONE:
UNREACHABLE;
}
}
@ -192,7 +192,7 @@ void symex_slicet::collect_open_variables(
// ignore for now
break;
default:
case goto_trace_stept::typet::GOTO:
UNREACHABLE;
}
}

2
src/goto-symex/ssa_step.cpp
View File

@ -106,7 +106,7 @@ void SSA_stept::output(std::ostream &out) const
out << "IF " << format(cond_expr) << " GOTO\n";
break;
default:
case goto_trace_stept::typet::NONE:
UNREACHABLE;
}

6
src/goto-symex/symex_main.cpp
View File

@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include "goto_symex.h"
#include <cassert>
#include <memory>
#include <pointer-analysis/value_set_dereference.h>
@ -19,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include <util/exception_utils.h>
#include <util/expr_iterator.h>
#include <util/expr_util.h>
#include <util/invariant.h>
#include <util/make_unique.h>
#include <util/mathematical_expr.h>
#include <util/replace_symbol.h>
@ -549,8 +549,8 @@ void goto_symext::symex_step(
case NO_INSTRUCTION_TYPE:
throw unsupported_operation_exceptiont("symex got NO_INSTRUCTION");
default:
UNREACHABLE;
case INCOMPLETE_GOTO:
DATA_INVARIANT(false, "symex got unexpected instruction type");
}
}

11
src/pointer-analysis/show_value_sets.cpp
View File

@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include <goto-programs/goto_model.h>
#include <util/invariant.h>
#include <util/xml.h>
#include <iostream>
@ -37,9 +38,8 @@ void show_value_sets(
value_set_analysis.output(goto_model.goto_functions, std::cout);
break;
default:
{
}
case ui_message_handlert::uit::JSON_UI:
UNIMPLEMENTED;
}
}
@ -62,8 +62,7 @@ void show_value_sets(
value_set_analysis.output(goto_program, std::cout);
break;
default:
{
}
case ui_message_handlert::uit::JSON_UI:
UNIMPLEMENTED;
}
}

12
src/pointer-analysis/value_set_domain.h
View File

@ -103,7 +103,17 @@ void value_set_domain_templatet<VST>::transform(
}
break;
default:
case ASSERT:
case SKIP:
case START_THREAD:
case END_THREAD:
case LOCATION:
case ATOMIC_BEGIN:
case ATOMIC_END:
case THROW:
case CATCH:
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
{
// do nothing
}

28
src/pointer-analysis/value_set_domain_fi.cpp
View File

@ -47,17 +47,29 @@ bool value_set_domain_fit::transform(
break;
case FUNCTION_CALL:
{
const code_function_callt &code = from_l->get_function_call();
{
const code_function_callt &code = from_l->get_function_call();
value_set.do_function_call(function_to, code.arguments(), ns);
}
value_set.do_function_call(function_to, code.arguments(), ns);
break;
}
default:
{
// do nothing
}
case CATCH:
case THROW:
case DECL:
case DEAD:
case ATOMIC_BEGIN:
case ATOMIC_END:
case START_THREAD:
case END_THREAD:
case LOCATION:
case SKIP:
case ASSERT:
case ASSUME:
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
// do nothing
break;
}
return (value_set.changed);

30
src/pointer-analysis/value_set_domain_fivr.cpp
View File

@ -43,17 +43,29 @@ bool value_set_domain_fivrt::transform(
break;
case FUNCTION_CALL:
{
const code_function_callt &code=
to_code_function_call(from_l->code);
{
const code_function_callt &code = to_code_function_call(from_l->code);
value_set.do_function_call(function_to, code.arguments(), ns);
break;
}
value_set.do_function_call(function_to, code.arguments(), ns);
break;
}
default:
{
}
case CATCH:
case THROW:
case GOTO:
case DECL:
case DEAD:
case ATOMIC_BEGIN:
case ATOMIC_END:
case START_THREAD:
case END_THREAD:
case LOCATION:
case SKIP:
case ASSERT:
case ASSUME:
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
break;
}
return value_set.handover();

30
src/pointer-analysis/value_set_domain_fivrns.cpp
View File

@ -43,17 +43,29 @@ bool value_set_domain_fivrnst::transform(
break;
case FUNCTION_CALL:
{
const code_function_callt &code=
to_code_function_call(from_l->code);
{
const code_function_callt &code = to_code_function_call(from_l->code);
value_set.do_function_call(function_to, code.arguments(), ns);
break;
}
value_set.do_function_call(function_to, code.arguments(), ns);
break;
}
default:
{
}
case CATCH:
case THROW:
case GOTO:
case DECL:
case DEAD:
case ATOMIC_BEGIN:
case ATOMIC_END:
case START_THREAD:
case END_THREAD:
case LOCATION:
case SKIP:
case ASSERT:
case ASSUME:
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
break;
}
return value_set.handover();

24
src/solvers/flattening/boolbv_get.cpp
View File

@ -84,12 +84,14 @@ exprt boolbvt::bv_get_rec(
{
if(!unknown[offset])
{
// clang-format off
switch(prop.l_get(bv[offset]).get_value())
{
case tvt::tv_enumt::TV_FALSE: return false_exprt();
case tvt::tv_enumt::TV_TRUE: return true_exprt();
default: return false_exprt(); // default
case tvt::tv_enumt::TV_UNKNOWN: return false_exprt(); // default
}
// clang-format on
}
return false_exprt{}; // default
@ -265,15 +267,23 @@ exprt boolbvt::bv_get_rec(
break;
case bvtypet::IS_RANGE:
{
mp_integer int_value=binary2integer(value, false);
mp_integer from=string2integer(type.get_string(ID_from));
{
mp_integer int_value = binary2integer(value, false);
mp_integer from = string2integer(type.get_string(ID_from));
return constant_exprt(integer2string(int_value + from), type);
}
return constant_exprt(integer2string(int_value + from), type);
break;
}
default:
case bvtypet::IS_C_BIT_FIELD:
case bvtypet::IS_VERILOG_UNSIGNED:
case bvtypet::IS_VERILOG_SIGNED:
case bvtypet::IS_C_BOOL:
case bvtypet::IS_FIXED:
case bvtypet::IS_FLOAT:
case bvtypet::IS_UNSIGNED:
case bvtypet::IS_SIGNED:
case bvtypet::IS_BV:
case bvtypet::IS_C_ENUM:
{
const irep_idt bvrep = make_bvrep(

15
src/solvers/flattening/boolbv_typecast.cpp
View File

@ -191,7 +191,12 @@ bool boolbvt::type_conversion(
dest=src;
return false;
default:
case bvtypet::IS_C_BIT_FIELD:
case bvtypet::IS_UNKNOWN:
case bvtypet::IS_RANGE:
case bvtypet::IS_VERILOG_UNSIGNED:
case bvtypet::IS_VERILOG_SIGNED:
case bvtypet::IS_FIXED:
if(src_type.id()==ID_bool)
{
// bool to float
@ -422,7 +427,9 @@ bool boolbvt::type_conversion(
dest = src;
return false;
default:
case bvtypet::IS_RANGE:
case bvtypet::IS_C_BIT_FIELD:
case bvtypet::IS_UNKNOWN:
if(src_type.id() == ID_bool)
{
// bool to integer
@ -516,7 +523,9 @@ bool boolbvt::type_conversion(
return false;
default:
case bvtypet::IS_C_BIT_FIELD:
case bvtypet::IS_UNKNOWN:
case bvtypet::IS_VERILOG_SIGNED:
if(dest_type.id()==ID_array)
{
if(src_width==dest_width)

3
src/solvers/floatbv/float_utils.h
View File

@ -57,7 +57,8 @@ public:
round_to_zero=const_literal(true);
break;
default:
case ieee_floatt::NONDETERMINISTIC:
case ieee_floatt::UNKNOWN:
UNREACHABLE;
}
}

2
src/solvers/prop/cover_goals.cpp
View File

@ -82,7 +82,7 @@ operator()(message_handlert &message_handler)
mark();
break;
default:
case decision_proceduret::resultt::D_ERROR:
{
messaget log(message_handler);
log.error() << "decision procedure has failed" << messaget::eom;

2
src/solvers/prop/prop_conv_solver.cpp
View File

@ -484,7 +484,7 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve()
return resultt::D_SATISFIABLE;
case propt::resultt::P_UNSATISFIABLE:
return resultt::D_UNSATISFIABLE;
default:
case propt::resultt::P_ERROR:
return resultt::D_ERROR;
}

2
src/solvers/prop/prop_minimize.cpp
View File

@ -131,7 +131,7 @@ void prop_minimizet::operator()()
fix_objectives(); // fix the ones we got
break;
default:
case decision_proceduret::resultt::D_ERROR:
log.error() << "decision procedure failed" << messaget::eom;
last_was_SAT = false;
return;

2
src/solvers/qbf/qdimacs_cnf.cpp
View File

@ -50,7 +50,7 @@ void qdimacs_cnft::write_prefix(std::ostream &out) const
out << "e";
break;
default:
case quantifiert::typet::NONE:
UNREACHABLE;
}

10
src/solvers/refinement/bv_refinement_loop.cpp
View File

@ -78,7 +78,7 @@ decision_proceduret::resultt bv_refinementt::dec_solve()
<< messaget::eom;
break;
default:
case resultt::D_ERROR:
return resultt::D_ERROR;
}
}
@ -105,12 +105,14 @@ decision_proceduret::resultt bv_refinementt::prop_solve()
propt::resultt result=prop.prop_solve();
pop();
// clang-format off
switch(result)
{
case propt::resultt::P_SATISFIABLE: return resultt::D_SATISFIABLE;
case propt::resultt::P_UNSATISFIABLE: return resultt::D_UNSATISFIABLE;
default: return resultt::D_ERROR;
case propt::resultt::P_SATISFIABLE: return resultt::D_SATISFIABLE;
case propt::resultt::P_UNSATISFIABLE: return resultt::D_UNSATISFIABLE;
case propt::resultt::P_ERROR: return resultt::D_ERROR;
}
// clang-format off
UNREACHABLE;
}

2
src/solvers/refinement/refine_arrays.cpp
View File

@ -89,7 +89,7 @@ void bv_refinementt::arrays_overapproximated()
nb_active++;
lazy_array_constraints.erase(it++);
break;
default:
case decision_proceduret::resultt::D_ERROR:
INVARIANT(false, "error in array over approximation check");
}
}

2
src/solvers/smt2/smt2_dec.cpp
View File

@ -113,7 +113,7 @@ decision_proceduret::resultt smt2_dect::dec_solve()
argv = {"z3", "-smt2", temp_file_problem()};
break;
default:
case solvert::GENERIC:
UNREACHABLE;
}

32
src/solvers/smt2/smt2_parser.cpp
View File

@ -72,7 +72,12 @@ void smt2_parsert::command_sequence()
// what we expect
break;
default:
case smt2_tokenizert::OPEN:
case smt2_tokenizert::SYMBOL:
case smt2_tokenizert::NUMERAL:
case smt2_tokenizert::STRING_LITERAL:
case smt2_tokenizert::NONE:
case smt2_tokenizert::KEYWORD:
throw error("expected ')' at end of command");
}
}
@ -101,7 +106,11 @@ void smt2_parsert::ignore_command()
case smt2_tokenizert::END_OF_FILE:
throw error("unexpected EOF in command");
default:
case smt2_tokenizert::SYMBOL:
case smt2_tokenizert::NUMERAL:
case smt2_tokenizert::STRING_LITERAL:
case smt2_tokenizert::NONE:
case smt2_tokenizert::KEYWORD:
next_token();
}
}
@ -965,7 +974,12 @@ exprt smt2_parsert::function_application()
}
break;
default:
case smt2_tokenizert::CLOSE:
case smt2_tokenizert::NUMERAL:
case smt2_tokenizert::STRING_LITERAL:
case smt2_tokenizert::END_OF_FILE:
case smt2_tokenizert::NONE:
case smt2_tokenizert::KEYWORD:
// just parentheses
exprt tmp=expression();
if(next_token() != smt2_tokenizert::CLOSE)
@ -1065,7 +1079,10 @@ exprt smt2_parsert::expression()
case smt2_tokenizert::END_OF_FILE:
throw error("EOF in an expression");
default:
case smt2_tokenizert::CLOSE:
case smt2_tokenizert::STRING_LITERAL:
case smt2_tokenizert::NONE:
case smt2_tokenizert::KEYWORD:
throw error("unexpected token in an expression");
}
@ -1156,7 +1173,12 @@ typet smt2_parsert::sort()
throw error() << "unexpected sort: `" << smt2_tokenizer.get_buffer()
<< '\'';
default:
case smt2_tokenizert::CLOSE:
case smt2_tokenizert::NUMERAL:
case smt2_tokenizert::STRING_LITERAL:
case smt2_tokenizert::END_OF_FILE:
case smt2_tokenizert::NONE:
case smt2_tokenizert::KEYWORD:
throw error() << "unexpected token in a sort: `"
<< smt2_tokenizer.get_buffer() << '\'';
}

3
src/solvers/smt2/smt2irep.cpp
View File

@ -74,7 +74,8 @@ optionalt<irept> smt2irept::operator()()
break;
}
default:
case NONE:
case KEYWORD:
throw error("unexpected token");
}
}

7
src/solvers/strings/string_constraint_generator_format.cpp
View File

@ -384,12 +384,9 @@ add_axioms_for_format_specifier(
message.warning() << "unimplemented format specifier: " << fs.conversion
<< message.eom;
return {array_pool.fresh_string(index_type, char_type), {}};
default:
message.error() << "invalid format specifier: " << fs.conversion
<< message.eom;
INVARIANT(
false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
}
INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
}
/// Deserialize an argument for format from \p string.

4
src/util/byte_operators.cpp
View File

@ -20,7 +20,7 @@ irep_idt byte_extract_id()
case configt::ansi_ct::endiannesst::IS_BIG_ENDIAN:
return ID_byte_extract_big_endian;
default:
case configt::ansi_ct::endiannesst::NO_ENDIANNESS:
UNREACHABLE;
}
@ -37,7 +37,7 @@ irep_idt byte_update_id()
case configt::ansi_ct::endiannesst::IS_BIG_ENDIAN:
return ID_byte_update_big_endian;
default:
case configt::ansi_ct::endiannesst::NO_ENDIANNESS:
UNREACHABLE;
}

4
src/util/config.cpp
View File

@ -1096,13 +1096,15 @@ bool configt::set(const cmdlinet &cmdline)
std::string configt::ansi_ct::os_to_string(ost os)
{
// clang-format off
switch(os)
{
case ost::OS_LINUX: return "linux";
case ost::OS_MACOS: return "macos";
case ost::OS_WIN: return "win";
default: return "none";
case ost::NO_OS: return "none";
}
// clang-format on
UNREACHABLE;
}

3
src/util/ieee_float.cpp
View File

@ -688,7 +688,8 @@ void ieee_floatt::divide_and_round(
++dividend;
break;
default:
case NONDETERMINISTIC:
case UNKNOWN:
UNREACHABLE;
}
}