diff --git a/CMakeLists.txt b/CMakeLists.txt index 4d46ac1b056..73a43ba8068 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -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 diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 6f7a69bf3fe..1e5a42cb970 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -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 diff --git a/jbmc/src/miniz/miniz.cpp b/jbmc/src/miniz/miniz.cpp index 7b511560fec..4377ca40183 100644 --- a/jbmc/src/miniz/miniz.cpp +++ b/jbmc/src/miniz/miniz.cpp @@ -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"; diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index 372a24452b1..ef97471298f 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -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; } } diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp index 0cf3aca8b53..b2061002246 100644 --- a/src/analyses/escape_analysis.cpp +++ b/src/analyses/escape_analysis.cpp @@ -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); - - std::set 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 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 cleanup_functions1; + std::set 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 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 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++; } } } diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp index 45b68fa41d0..1d74895983b 100644 --- a/src/analyses/global_may_alias.cpp +++ b/src/analyses/global_may_alias.cpp @@ -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 rhs_aliases; - get_rhs_aliases(code_assign.rhs(), rhs_aliases); - assign_lhs_aliases(code_assign.lhs(), rhs_aliases); - } + std::set 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; } } diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index cafeb03cf3a..b857a74dd8f 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -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; } } diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp index b5d3c70d71f..0133120cb66 100644 --- a/src/analyses/invariant_set_domain.cpp +++ b/src/analyses/invariant_set_domain.cpp @@ -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; } } diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp index bddd6cd4384..13b41001cc6 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/src/analyses/local_bitvector_analysis.cpp @@ -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) diff --git a/src/analyses/local_cfg.cpp b/src/analyses/local_cfg.cpp index 6617d0b89b6..3ac29f020d9 100644 --- a/src/analyses/local_cfg.cpp +++ b/src/analyses/local_cfg.cpp @@ -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; } } } diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp index 4b4266f65dc..b762c97b714 100644 --- a/src/analyses/local_may_alias.cpp +++ b/src/analyses/local_may_alias.cpp @@ -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; itype) + if(from->is_decl()) { - case DECL: - { - 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; - - default: - { - std::list read=expressions_read(*from); - std::list written=expressions_written(*from); - - for(const auto &expr : written) - assign(expr); - - // we only care about the *first* uninitalized use - for(const auto &expr : read) - assign(expr); - } + 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); + } + else + { + std::list read = expressions_read(*from); + std::list written = expressions_written(*from); + + for(const auto &expr : written) + assign(expr); + + // we only care about the *first* uninitalized use + for(const auto &expr : read) + assign(expr); } } diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp index 85541711fab..96b7ae52bad 100644 --- a/src/ansi-c/c_typecast.cpp +++ b/src/ansi-c/c_typecast.cpp @@ -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()) diff --git a/src/config.inc b/src/config.inc index 7d1523a35b0..c8114488f18 100644 --- a/src/config.inc +++ b/src/config.inc @@ -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 diff --git a/src/cpp/cpp_id.cpp b/src/cpp/cpp_id.cpp index bf15f50f024..9b8d7f8fc96 100644 --- a/src/cpp/cpp_id.cpp +++ b/src/cpp/cpp_id.cpp @@ -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; } diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index eb2d5d69409..89c2034394a 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -1680,9 +1680,8 @@ exprt cpp_typecheck_resolvet::resolve( } break; - default: - { - } + case wantt::BOTH: + break; } return result; diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index e1c5da7b7ce..351d7a82ee9 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -1044,7 +1044,8 @@ bool Parser::rTemplateDecl(cpp_declarationt &decl) decl.swap(body); break; - default: + case num_tdks: + case tdk_unknown: UNREACHABLE; break; } diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp index 20d6e660786..770c771364c 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/src/goto-analyzer/taint_analysis.cpp @@ -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) - { - const irep_idt &identifier= - to_symbol_expr(function).get_identifier(); + std::set identifiers; + + identifiers.insert(identifier); - std::set identifiers; + irep_idt class_id = function.get(ID_C_class); + if(class_id.empty()) + { + } + else + { + std::string suffix = std::string( + id2string(identifier), class_id.size(), std::string::npos); - identifiers.insert(identifier); + class_hierarchyt::idst parents = + class_hierarchy.get_parents_trans(class_id); + for(const auto &p : parents) + identifiers.insert(id2string(p) + suffix); + } - irep_idt class_id=function.get(ID_C_class); - if(class_id.empty()) - { - } - else + for(const auto &rule : taint.rules) + { + bool match = false; + for(const auto &i : identifiers) { - 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); + if( + i == rule.function_identifier || + has_prefix( + id2string(i), + "java::" + id2string(rule.function_identifier) + ":")) + { + match = true; + break; + } } - for(const auto &rule : taint.rules) + if(match) { - 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; - } + log.debug() << "MATCH " << rule.id << " on " << identifier + << messaget::eom; - if(match) - { - log.debug() << "MATCH " << rule.id << " on " << identifier - << messaget::eom; + exprt where = nil_exprt(); - exprt where=nil_exprt(); + const code_typet &code_type = to_code_type(function.type()); - const code_typet &code_type=to_code_type(function.type()); + bool have_this = !code_type.parameters().empty() && + code_type.parameters().front().get_bool(ID_C_this); - 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; + } - 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) - { - DATA_INVARIANT( - !function_call.arguments().empty(), - "`this` implies at least one argument in function call"); - where=function_call.arguments()[0]; - } - 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; + } - switch(rule.kind) + case taint_parse_treet::rulet::THIS: + if(have_this) { - 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::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; + 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; + } + + 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; + } } } } } - break; - - default: - { - } } if(!insert_before.empty()) diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 0513d1c1f8f..be6342b83f5 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -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; } } diff --git a/src/goto-instrument/cover_util.cpp b/src/goto-instrument/cover_util.cpp index b43bc31e052..7202d002b81 100644 --- a/src/goto-instrument/cover_util.cpp +++ b/src/goto-instrument/cover_util.cpp @@ -58,9 +58,23 @@ std::set 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(); @@ -125,9 +139,23 @@ std::set 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(); diff --git a/src/goto-instrument/points_to.cpp b/src/goto-instrument/points_to.cpp index 843d5755aee..5b79d8382b8 100644 --- a/src/goto-instrument/points_to.cpp +++ b/src/goto-instrument/points_to.cpp @@ -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; diff --git a/src/goto-instrument/show_locations.cpp b/src/goto-instrument/show_locations.cpp index 530ad487d7a..862a19467da 100644 --- a/src/goto-instrument/show_locations.cpp +++ b/src/goto-instrument/show_locations.cpp @@ -58,7 +58,7 @@ void show_locations( << it->source_location << '\n'; break; - default: + case ui_message_handlert::uit::JSON_UI: UNREACHABLE; } } diff --git a/src/goto-programs/format_strings.cpp b/src/goto-programs/format_strings.cpp index 44fbad69308..97a57780604 100644 --- a/src/goto-programs/format_strings.cpp +++ b/src/goto-programs/format_strings.cpp @@ -257,7 +257,10 @@ optionalt 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 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 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 {}; } diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index df335b3af0f..9c3f7f34707 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -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 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 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; diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 44eaa6f81ae..49dc4a6eda3 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -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(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; } } diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index de9b5ad11c4..3d76854b1cc 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -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; diff --git a/src/goto-programs/json_goto_trace.h b/src/goto-programs/json_goto_trace.h index 302ed969d8d..3bdc67c6f77 100644 --- a/src/goto-programs/json_goto_trace.h +++ b/src/goto-programs/json_goto_trace.h @@ -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(); diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp index 5ec68cd10d3..01191824f0d 100644 --- a/src/goto-programs/show_symbol_table.cpp +++ b/src/goto-programs/show_symbol_table.cpp @@ -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; } diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp index 26d4a74cd18..bad8162a73d 100644 --- a/src/goto-programs/string_instrumentation.cpp +++ b/src/goto-programs/string_instrumentation.cpp @@ -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}; diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp index 1a076fbab41..f14749c2433 100644 --- a/src/goto-programs/vcd_goto_trace.cpp +++ b/src/goto-programs/vcd_goto_trace.cpp @@ -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"; + } } } } diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index c6c88f2ad41..b7f8fc43b1c 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -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; + 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.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); + 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.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_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"); - } + 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"); + { + 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.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)); + 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); + 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)); - } + 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)); } 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); + { + 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)); + 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); + 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); 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 diff --git a/src/goto-symex/slice.cpp b/src/goto-symex/slice.cpp index 54efd9c9793..bd2d0562f23 100644 --- a/src/goto-symex/slice.cpp +++ b/src/goto-symex/slice.cpp @@ -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; } } diff --git a/src/goto-symex/ssa_step.cpp b/src/goto-symex/ssa_step.cpp index 496d5a438a2..24f29942125 100644 --- a/src/goto-symex/ssa_step.cpp +++ b/src/goto-symex/ssa_step.cpp @@ -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; } diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index b018c4a20f2..2a5834fdc04 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_symex.h" -#include #include #include @@ -19,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -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"); } } diff --git a/src/pointer-analysis/show_value_sets.cpp b/src/pointer-analysis/show_value_sets.cpp index e1dc0bb938e..06297f0b376 100644 --- a/src/pointer-analysis/show_value_sets.cpp +++ b/src/pointer-analysis/show_value_sets.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include @@ -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; } } diff --git a/src/pointer-analysis/value_set_domain.h b/src/pointer-analysis/value_set_domain.h index dd1cc40fae8..71b2a39f212 100644 --- a/src/pointer-analysis/value_set_domain.h +++ b/src/pointer-analysis/value_set_domain.h @@ -103,7 +103,17 @@ void value_set_domain_templatet::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 } diff --git a/src/pointer-analysis/value_set_domain_fi.cpp b/src/pointer-analysis/value_set_domain_fi.cpp index f22acab380f..e8c5917003c 100644 --- a/src/pointer-analysis/value_set_domain_fi.cpp +++ b/src/pointer-analysis/value_set_domain_fi.cpp @@ -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); diff --git a/src/pointer-analysis/value_set_domain_fivr.cpp b/src/pointer-analysis/value_set_domain_fivr.cpp index 7e45ce424a6..5491616640d 100644 --- a/src/pointer-analysis/value_set_domain_fivr.cpp +++ b/src/pointer-analysis/value_set_domain_fivr.cpp @@ -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(); diff --git a/src/pointer-analysis/value_set_domain_fivrns.cpp b/src/pointer-analysis/value_set_domain_fivrns.cpp index 6baf68a059a..43a0594ca69 100644 --- a/src/pointer-analysis/value_set_domain_fivrns.cpp +++ b/src/pointer-analysis/value_set_domain_fivrns.cpp @@ -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(); diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp index 94996d45e2d..3f559cfb61c 100644 --- a/src/solvers/flattening/boolbv_get.cpp +++ b/src/solvers/flattening/boolbv_get.cpp @@ -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( diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp index 7352faf151c..f3cd29865b6 100644 --- a/src/solvers/flattening/boolbv_typecast.cpp +++ b/src/solvers/flattening/boolbv_typecast.cpp @@ -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) diff --git a/src/solvers/floatbv/float_utils.h b/src/solvers/floatbv/float_utils.h index 93229a39112..989c8d53377 100644 --- a/src/solvers/floatbv/float_utils.h +++ b/src/solvers/floatbv/float_utils.h @@ -57,7 +57,8 @@ class float_utilst round_to_zero=const_literal(true); break; - default: + case ieee_floatt::NONDETERMINISTIC: + case ieee_floatt::UNKNOWN: UNREACHABLE; } } diff --git a/src/solvers/prop/cover_goals.cpp b/src/solvers/prop/cover_goals.cpp index 7f5c7ea2c6d..f8f1347e6f9 100644 --- a/src/solvers/prop/cover_goals.cpp +++ b/src/solvers/prop/cover_goals.cpp @@ -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; diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp index 09d038a0f88..68cfdb1e903 100644 --- a/src/solvers/prop/prop_conv_solver.cpp +++ b/src/solvers/prop/prop_conv_solver.cpp @@ -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; } diff --git a/src/solvers/prop/prop_minimize.cpp b/src/solvers/prop/prop_minimize.cpp index 93a1d521861..8777b63aa01 100644 --- a/src/solvers/prop/prop_minimize.cpp +++ b/src/solvers/prop/prop_minimize.cpp @@ -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; diff --git a/src/solvers/qbf/qdimacs_cnf.cpp b/src/solvers/qbf/qdimacs_cnf.cpp index ac4897e1c76..3972b3ef5f7 100644 --- a/src/solvers/qbf/qdimacs_cnf.cpp +++ b/src/solvers/qbf/qdimacs_cnf.cpp @@ -50,7 +50,7 @@ void qdimacs_cnft::write_prefix(std::ostream &out) const out << "e"; break; - default: + case quantifiert::typet::NONE: UNREACHABLE; } diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp index c1ce82b9a82..0f192f78de5 100644 --- a/src/solvers/refinement/bv_refinement_loop.cpp +++ b/src/solvers/refinement/bv_refinement_loop.cpp @@ -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; } diff --git a/src/solvers/refinement/refine_arrays.cpp b/src/solvers/refinement/refine_arrays.cpp index 11eeb7785db..a233fc2c9a6 100644 --- a/src/solvers/refinement/refine_arrays.cpp +++ b/src/solvers/refinement/refine_arrays.cpp @@ -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"); } } diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index 487dc686fad..2aa18cbc042 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -113,7 +113,7 @@ decision_proceduret::resultt smt2_dect::dec_solve() argv = {"z3", "-smt2", temp_file_problem()}; break; - default: + case solvert::GENERIC: UNREACHABLE; } diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index 2ac73696f7e..674c3afcd98 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -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() << '\''; } diff --git a/src/solvers/smt2/smt2irep.cpp b/src/solvers/smt2/smt2irep.cpp index a380c94cd50..14e75e16863 100644 --- a/src/solvers/smt2/smt2irep.cpp +++ b/src/solvers/smt2/smt2irep.cpp @@ -74,7 +74,8 @@ optionalt smt2irept::operator()() break; } - default: + case NONE: + case KEYWORD: throw error("unexpected token"); } } diff --git a/src/solvers/strings/string_constraint_generator_format.cpp b/src/solvers/strings/string_constraint_generator_format.cpp index ca49485ee6e..0b976006eea 100644 --- a/src/solvers/strings/string_constraint_generator_format.cpp +++ b/src/solvers/strings/string_constraint_generator_format.cpp @@ -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. diff --git a/src/util/byte_operators.cpp b/src/util/byte_operators.cpp index 9a2cfb69491..25895e872e6 100644 --- a/src/util/byte_operators.cpp +++ b/src/util/byte_operators.cpp @@ -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; } diff --git a/src/util/config.cpp b/src/util/config.cpp index e5ebffbeed9..4ff19d6c7c6 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -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; } diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp index e9280263aaf..78be7e46b12 100644 --- a/src/util/ieee_float.cpp +++ b/src/util/ieee_float.cpp @@ -688,7 +688,8 @@ void ieee_floatt::divide_and_round( ++dividend; break; - default: + case NONDETERMINISTIC: + case UNKNOWN: UNREACHABLE; } }