From 81cd230198370b3ee9c5b66bdea051b72f3f05a1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 20 Jun 2018 20:18:21 +0100 Subject: [PATCH 1/6] Handle all enum values in switch/case --- .../java_bytecode/java_bytecode_language.cpp | 2 +- jbmc/src/miniz/miniz.cpp | 5 +- src/analyses/custom_bitvector_analysis.cpp | 18 +++- src/analyses/escape_analysis.cpp | 33 +++---- src/analyses/global_may_alias.cpp | 21 ++++- src/analyses/interval_domain.cpp | 18 +++- src/analyses/invariant_set_domain.cpp | 17 +++- src/analyses/local_bitvector_analysis.cpp | 20 ++++- src/analyses/local_cfg.cpp | 17 +++- src/analyses/local_may_alias.cpp | 20 ++++- src/analyses/local_safe_pointers.cpp | 11 ++- src/analyses/uncaught_exceptions_analysis.cpp | 20 ++++- src/analyses/uninitialized_domain.cpp | 9 +- src/ansi-c/c_typecast.cpp | 9 +- src/cpp/cpp_id.cpp | 2 +- src/cpp/cpp_typecheck_resolve.cpp | 5 +- src/cpp/parse.cpp | 3 +- src/goto-analyzer/taint_analysis.cpp | 10 +-- src/goto-cc/compile.cpp | 6 +- src/goto-instrument/cover_util.cpp | 40 +++++++-- src/goto-instrument/points_to.cpp | 21 ++++- src/goto-instrument/show_locations.cpp | 2 +- src/goto-programs/format_strings.cpp | 34 ++++++-- src/goto-programs/goto_program.cpp | 87 ++++++++++++++++--- src/goto-programs/goto_trace.cpp | 14 +-- src/goto-programs/interpreter.cpp | 3 +- src/goto-programs/json_goto_trace.h | 13 ++- src/goto-programs/show_symbol_table.cpp | 4 +- src/goto-programs/string_instrumentation.cpp | 18 ++-- src/goto-programs/vcd_goto_trace.cpp | 10 +-- src/goto-programs/xml_goto_trace.cpp | 13 ++- src/goto-symex/slice.cpp | 4 +- src/goto-symex/ssa_step.cpp | 2 +- src/goto-symex/symex_main.cpp | 6 +- src/pointer-analysis/show_value_sets.cpp | 11 ++- src/pointer-analysis/value_set_domain.h | 12 ++- src/pointer-analysis/value_set_domain_fi.cpp | 20 ++++- .../value_set_domain_fivr.cpp | 19 +++- .../value_set_domain_fivrns.cpp | 19 +++- src/solvers/flattening/boolbv_get.cpp | 12 ++- src/solvers/flattening/boolbv_typecast.cpp | 15 +++- src/solvers/floatbv/float_utils.h | 3 +- src/solvers/prop/cover_goals.cpp | 2 +- src/solvers/prop/prop_conv_solver.cpp | 2 +- src/solvers/prop/prop_minimize.cpp | 2 +- src/solvers/qbf/qdimacs_cnf.cpp | 2 +- src/solvers/refinement/bv_refinement_loop.cpp | 4 +- src/solvers/refinement/refine_arrays.cpp | 2 +- src/solvers/smt2/smt2_dec.cpp | 2 +- src/solvers/smt2/smt2_parser.cpp | 32 +++++-- src/solvers/smt2/smt2irep.cpp | 3 +- .../string_constraint_generator_format.cpp | 7 +- src/util/byte_operators.cpp | 4 +- src/util/config.cpp | 2 +- src/util/ieee_float.cpp | 3 +- 55 files changed, 518 insertions(+), 177 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 6f7a69bf3f..c3d7dfe696 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -825,7 +825,7 @@ bool java_bytecode_languaget::typecheck( } } break; - default: + case LAZY_METHODS_MODE_EXTERNAL_DRIVER: // Our caller is in charge of elaborating methods on demand. break; } diff --git a/jbmc/src/miniz/miniz.cpp b/jbmc/src/miniz/miniz.cpp index 7b511560fe..4377ca4018 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 372a24452b..cd7ddfcaf3 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -536,9 +536,21 @@ void custom_bitvector_domaint::transform( } break; - default: - { - } + case CATCH: + case THROW: + case RETURN: + case ATOMIC_BEGIN: + case ATOMIC_END: + case END_FUNCTION: + case LOCATION: + case START_THREAD: + case END_THREAD: + case SKIP: + case ASSERT: + case ASSUME: + case INCOMPLETE_GOTO: + case NO_INSTRUCTION_TYPE: + break; } } diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp index 0cf3aca8b5..7416a2b471 100644 --- a/src/analyses/escape_analysis.cpp +++ b/src/analyses/escape_analysis.cpp @@ -253,9 +253,22 @@ void escape_domaint::transform( // This is the edge to the call site. break; - default: - { - } + case GOTO: + case CATCH: + case THROW: + case RETURN: + case ATOMIC_BEGIN: + case ATOMIC_END: + case LOCATION: + case START_THREAD: + case END_THREAD: + case ASSERT: + case ASSUME: + case SKIP: + case OTHER: + case INCOMPLETE_GOTO: + case NO_INSTRUCTION_TYPE: + break; } } @@ -444,9 +457,7 @@ void escape_analysist::instrument( const goto_programt::instructiont &instruction=*i_it; - switch(instruction.type) - { - case ASSIGN: + if(instruction.type == ASSIGN) { const code_assignt &code_assign=to_code_assign(instruction.code); @@ -460,9 +471,7 @@ void escape_analysist::instrument( false, ns); } - break; - - case DEAD: + else if(instruction.type == DEAD) { const code_deadt &code_dead=to_code_dead(instruction.code); @@ -512,12 +521,6 @@ void escape_analysist::instrument( i_it++; } } - break; - - default: - { - } - } } Forall_goto_program_instructions(i_it, f_it->second.body) diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp index 45b68fa41d..985bd992b3 100644 --- a/src/analyses/global_may_alias.cpp +++ b/src/analyses/global_may_alias.cpp @@ -129,9 +129,24 @@ void global_may_alias_domaint::transform( } break; - default: - { - } + case FUNCTION_CALL: + case GOTO: + case CATCH: + case THROW: + case RETURN: + case ATOMIC_BEGIN: + case ATOMIC_END: + case LOCATION: + case START_THREAD: + case END_THREAD: + case ASSERT: + case ASSUME: + case SKIP: + case END_FUNCTION: + case OTHER: + case INCOMPLETE_GOTO: + case NO_INSTRUCTION_TYPE: + break; } } diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index cafeb03cf3..c64458edba 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -108,9 +108,21 @@ void interval_domaint::transform( } break; - default: - { - } + case CATCH: + case THROW: + case RETURN: + case ATOMIC_BEGIN: + case ATOMIC_END: + case END_FUNCTION: + case START_THREAD: + case END_THREAD: + case ASSERT: + case LOCATION: + case SKIP: + case OTHER: + case INCOMPLETE_GOTO: + case NO_INSTRUCTION_TYPE: + break; } } diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp index b5d3c70d71..b1cfd2ee42 100644 --- a/src/analyses/invariant_set_domain.cpp +++ b/src/analyses/invariant_set_domain.cpp @@ -75,9 +75,18 @@ void invariant_set_domaint::transform( invariant_set.make_threaded(); break; - default: - { - // do nothing - } + case CATCH: + case THROW: + case DEAD: + case ATOMIC_BEGIN: + case ATOMIC_END: + case END_FUNCTION: + case LOCATION: + case END_THREAD: + case SKIP: + case INCOMPLETE_GOTO: + case NO_INSTRUCTION_TYPE: + // do nothing + break; } } diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp index bddd6cd438..77e0b491c1 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/src/analyses/local_bitvector_analysis.cpp @@ -308,9 +308,23 @@ void local_bitvector_analysist::build() } break; - default: - { - } + case CATCH: + case THROW: + case RETURN: + case ATOMIC_BEGIN: + case ATOMIC_END: + case LOCATION: + case START_THREAD: + case END_THREAD: + case SKIP: + case OTHER: + case ASSERT: + case ASSUME: + case GOTO: + case END_FUNCTION: + case INCOMPLETE_GOTO: + case NO_INSTRUCTION_TYPE: + break; } for(const auto &succ : node.successors) diff --git a/src/analyses/local_cfg.cpp b/src/analyses/local_cfg.cpp index 6617d0b89b..78d4079ccd 100644 --- a/src/analyses/local_cfg.cpp +++ b/src/analyses/local_cfg.cpp @@ -73,8 +73,23 @@ void local_cfgt::build(const goto_programt &goto_program) case END_THREAD: break; // no successor - default: + 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: + case INCOMPLETE_GOTO: + case NO_INSTRUCTION_TYPE: node.successors.push_back(loc_nr+1); + break; } } } diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp index 4b4266f65d..fdaa19f607 100644 --- a/src/analyses/local_may_alias.cpp +++ b/src/analyses/local_may_alias.cpp @@ -419,9 +419,23 @@ void local_may_aliast::build(const goto_functiont &goto_function) } break; - default: - { - } + case CATCH: + case THROW: + case RETURN: + case GOTO: + case START_THREAD: + case END_THREAD: + case ATOMIC_BEGIN: + case ATOMIC_END: + case LOCATION: + case SKIP: + case END_FUNCTION: + case OTHER: + case ASSERT: + case ASSUME: + case INCOMPLETE_GOTO: + case NO_INSTRUCTION_TYPE: + break; } for(local_cfgt::successorst::const_iterator diff --git a/src/analyses/local_safe_pointers.cpp b/src/analyses/local_safe_pointers.cpp index 491d1a3d16..7719325649 100644 --- a/src/analyses/local_safe_pointers.cpp +++ b/src/analyses/local_safe_pointers.cpp @@ -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(); diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp index be9485fcbc..af3e4e89b9 100644 --- a/src/analyses/uncaught_exceptions_analysis.cpp +++ b/src/analyses/uncaught_exceptions_analysis.cpp @@ -125,8 +125,24 @@ void uncaught_exceptions_domaint::transform( join(uea.exceptions_map[function_name]); break; } - default: - {} + case DECL: + case DEAD: + case ASSIGN: + case RETURN: + case GOTO: + 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; } } diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp index 76ad23d67b..ffb85c4e82 100644 --- a/src/analyses/uninitialized_domain.cpp +++ b/src/analyses/uninitialized_domain.cpp @@ -29,9 +29,7 @@ void uninitialized_domaint::transform( if(has_values.is_false()) return; - switch(from->type) - { - case DECL: + if(from->is_decl()) { const irep_idt &identifier= to_code_decl(from->code).get_identifier(); @@ -40,9 +38,7 @@ void uninitialized_domaint::transform( if(!symbol.is_static_lifetime) uninitialized.insert(identifier); } - break; - - default: + else { std::list read=expressions_read(*from); std::list written=expressions_written(*from); @@ -54,7 +50,6 @@ void uninitialized_domaint::transform( for(const auto &expr : read) assign(expr); } - } } void uninitialized_domaint::assign(const exprt &lhs) diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp index 85541711fa..96b7ae52ba 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/cpp/cpp_id.cpp b/src/cpp/cpp_id.cpp index bf15f50f02..d6f53a29f6 100644 --- a/src/cpp/cpp_id.cpp +++ b/src/cpp/cpp_id.cpp @@ -111,7 +111,7 @@ 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"; } UNREACHABLE; diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index eb2d5d6940..89c2034394 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 e1c5da7b7c..351d7a82ee 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 20d6e66078..a0848a8f68 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/src/goto-analyzer/taint_analysis.cpp @@ -71,9 +71,7 @@ void taint_analysist::instrument( goto_programt insert_before, insert_after; - switch(instruction.type) - { - case FUNCTION_CALL: + if(instruction.is_function_call()) { const code_function_callt &function_call = instruction.get_function_call(); @@ -205,12 +203,6 @@ void taint_analysist::instrument( } } } - break; - - default: - { - } - } if(!insert_before.empty()) { diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 0513d1c1f8..be6342b83f 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 b43bc31e05..7202d002b8 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 843d5755ae..5b79d8382b 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 530ad487d7..862a19467d 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 44fbad6930..97a5778060 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 df335b3af0..ef31542380 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; } @@ -303,9 +303,21 @@ std::list expressions_read( } 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 +343,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 +517,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 +999,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 +1058,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 +1164,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 44eaa6f81a..cc81414b2b 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -85,9 +85,10 @@ 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; } if(is_assert() || is_assume() || is_goto()) @@ -479,9 +480,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 +682,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 de9b5ad11c..3d76854b1c 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 302ed969d8..3bdc67c6f7 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 5ec68cd10d..01191824f0 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 26d4a74cd1..bad8162a73 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 1a076fbab4..67ae3fc7e3 100644 --- a/src/goto-programs/vcd_goto_trace.cpp +++ b/src/goto-programs/vcd_goto_trace.cpp @@ -113,9 +113,7 @@ void output_vcd( for(const auto &step : goto_trace.steps) { - switch(step.type) - { - case goto_trace_stept::typet::ASSIGNMENT: + if(step.is_assignment()) { auto lhs_object=step.get_lhs_object(); if(lhs_object.has_value()) @@ -147,11 +145,5 @@ void output_vcd( } } } - break; - - default: - { - } - } } } diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index c6c88f2ad4..74587a6066 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -198,7 +198,18 @@ void convert( } 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 54efd9c979..bd2d0562f2 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 496d5a438a..24f2994212 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 b018c4a20f..2a5834fdc0 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 e1dc0bb938..06297f0b37 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 dd1cc40fae..71b2a39f21 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 f22acab380..0b2b68fcf8 100644 --- a/src/pointer-analysis/value_set_domain_fi.cpp +++ b/src/pointer-analysis/value_set_domain_fi.cpp @@ -54,10 +54,22 @@ bool value_set_domain_fit::transform( } 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 7e45ce424a..d98ad625e7 100644 --- a/src/pointer-analysis/value_set_domain_fivr.cpp +++ b/src/pointer-analysis/value_set_domain_fivr.cpp @@ -51,9 +51,22 @@ bool value_set_domain_fivrt::transform( 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 6baf68a059..411a72b8ca 100644 --- a/src/pointer-analysis/value_set_domain_fivrns.cpp +++ b/src/pointer-analysis/value_set_domain_fivrns.cpp @@ -51,9 +51,22 @@ bool value_set_domain_fivrnst::transform( 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 94996d45e2..816930fef1 100644 --- a/src/solvers/flattening/boolbv_get.cpp +++ b/src/solvers/flattening/boolbv_get.cpp @@ -88,7 +88,7 @@ exprt boolbvt::bv_get_rec( { 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 } } @@ -273,7 +273,15 @@ exprt boolbvt::bv_get_rec( } 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 7352faf151..f3cd29865b 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 93229a3911..989c8d5337 100644 --- a/src/solvers/floatbv/float_utils.h +++ b/src/solvers/floatbv/float_utils.h @@ -57,7 +57,8 @@ public: 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 7f5c7ea2c6..f8f1347e6f 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 09d038a0f8..68cfdb1e90 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 93a1d52186..8777b63aa0 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 ac4897e1c7..3972b3ef5f 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 c1ce82b9a8..ba36225660 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; } } @@ -109,7 +109,7 @@ decision_proceduret::resultt bv_refinementt::prop_solve() { 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_ERROR: return resultt::D_ERROR; } UNREACHABLE; diff --git a/src/solvers/refinement/refine_arrays.cpp b/src/solvers/refinement/refine_arrays.cpp index 11eeb7785d..a233fc2c9a 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 487dc686fa..2aa18cbc04 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 2ac73696f7..674c3afcd9 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 a380c94cd5..14e75e1686 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 ca49485ee6..0b976006ee 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 9a2cfb6949..25895e872e 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 e5ebffbeed..f41f903106 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1101,7 +1101,7 @@ std::string configt::ansi_ct::os_to_string(ost 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"; } UNREACHABLE; diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp index e9280263aa..78be7e46b1 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; } } From 5e1c7bf0cc1efc5a5cc195af5e1f96f5755b3967 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 9 Jul 2018 17:00:13 +0100 Subject: [PATCH 2/6] Add -Wswitch-enum to default GCC/Clang build options This is now consistent with the warnings that Visual Studio would generate, which warns about missing enum cases in switch/case even when a default: is present. --- CMakeLists.txt | 2 +- src/config.inc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 4d46ac1b05..73a43ba806 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/src/config.inc b/src/config.inc index 7d1523a35b..c8114488f1 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 From 87e86bbf437967407a02ecb9e31b11d031c68d7a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Nov 2018 18:40:36 +0000 Subject: [PATCH 3/6] Disable clang-format for recently touched switch statements We should not re-indent a large number of lines of code just because some case statements were added. Silence clang-format for these instead. --- jbmc/src/java_bytecode/java_bytecode_language.cpp | 2 ++ src/analyses/escape_analysis.cpp | 2 ++ src/analyses/global_may_alias.cpp | 2 ++ src/analyses/interval_domain.cpp | 2 ++ src/analyses/local_bitvector_analysis.cpp | 2 ++ src/analyses/local_may_alias.cpp | 2 ++ src/analyses/uninitialized_domain.cpp | 2 ++ src/cpp/cpp_id.cpp | 2 ++ src/goto-analyzer/taint_analysis.cpp | 2 ++ src/goto-programs/goto_program.cpp | 2 ++ src/goto-programs/goto_trace.cpp | 2 ++ src/goto-programs/vcd_goto_trace.cpp | 2 ++ src/goto-programs/xml_goto_trace.cpp | 2 ++ src/pointer-analysis/value_set_domain_fi.cpp | 2 ++ src/pointer-analysis/value_set_domain_fivr.cpp | 2 ++ src/pointer-analysis/value_set_domain_fivrns.cpp | 2 ++ src/solvers/flattening/boolbv_get.cpp | 4 ++++ src/solvers/flattening/boolbv_typecast.cpp | 2 ++ src/solvers/refinement/bv_refinement_loop.cpp | 2 ++ src/util/config.cpp | 2 ++ 20 files changed, 42 insertions(+) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index c3d7dfe696..9776cd8b01 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -791,6 +791,7 @@ bool java_bytecode_languaget::typecheck( // Now incrementally elaborate methods // that are reachable from this entry point. + // clang-format off switch(lazy_methods_mode) { case LAZY_METHODS_MODE_CONTEXT_INSENSITIVE: @@ -829,6 +830,7 @@ bool java_bytecode_languaget::typecheck( // Our caller is in charge of elaborating methods on demand. break; } + // clang-format on // now instrument runtime exceptions java_bytecode_instrument( diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp index 7416a2b471..dde3d31c82 100644 --- a/src/analyses/escape_analysis.cpp +++ b/src/analyses/escape_analysis.cpp @@ -457,6 +457,7 @@ void escape_analysist::instrument( const goto_programt::instructiont &instruction=*i_it; + // clang-format off if(instruction.type == ASSIGN) { const code_assignt &code_assign=to_code_assign(instruction.code); @@ -521,6 +522,7 @@ void escape_analysist::instrument( i_it++; } } + // clang-format on } Forall_goto_program_instructions(i_it, f_it->second.body) diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp index 985bd992b3..e15a6ecee4 100644 --- a/src/analyses/global_may_alias.cpp +++ b/src/analyses/global_may_alias.cpp @@ -103,6 +103,7 @@ void global_may_alias_domaint::transform( const goto_programt::instructiont &instruction=*from; + // clang-format off switch(instruction.type) { case ASSIGN: @@ -148,6 +149,7 @@ void global_may_alias_domaint::transform( case NO_INSTRUCTION_TYPE: break; } + // clang-format on } void global_may_alias_domaint::output( diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index c64458edba..fcc5a11c3b 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -64,6 +64,7 @@ void interval_domaint::transform( ai_baset &, const namespacet &ns) { + // clang-format off const goto_programt::instructiont &instruction=*from; switch(instruction.type) { @@ -124,6 +125,7 @@ void interval_domaint::transform( case NO_INSTRUCTION_TYPE: break; } + // clang-format on } /// Sets *this to the mathematical join between the two domains. This can be diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp index 77e0b491c1..3a9a2a7c99 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/src/analyses/local_bitvector_analysis.cpp @@ -266,6 +266,7 @@ void local_bitvector_analysist::build() auto &loc_info_src=loc_infos[loc_nr]; auto loc_info_dest=loc_infos[loc_nr]; + // clang-format off switch(instruction.type) { case ASSIGN: @@ -326,6 +327,7 @@ void local_bitvector_analysist::build() case NO_INSTRUCTION_TYPE: break; } + // clang-format on for(const auto &succ : node.successors) { diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp index fdaa19f607..73db6c9e2d 100644 --- a/src/analyses/local_may_alias.cpp +++ b/src/analyses/local_may_alias.cpp @@ -365,6 +365,7 @@ void local_may_aliast::build(const goto_functiont &goto_function) const loc_infot &loc_info_src=loc_infos[loc_nr]; loc_infot loc_info_dest=loc_infos[loc_nr]; + // clang-format off switch(instruction.type) { case ASSIGN: @@ -437,6 +438,7 @@ void local_may_aliast::build(const goto_functiont &goto_function) case NO_INSTRUCTION_TYPE: break; } + // clang-format on for(local_cfgt::successorst::const_iterator it=node.successors.begin(); diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp index ffb85c4e82..eb8a6eed06 100644 --- a/src/analyses/uninitialized_domain.cpp +++ b/src/analyses/uninitialized_domain.cpp @@ -29,6 +29,7 @@ void uninitialized_domaint::transform( if(has_values.is_false()) return; + // clang-format off if(from->is_decl()) { const irep_idt &identifier= @@ -50,6 +51,7 @@ void uninitialized_domaint::transform( for(const auto &expr : read) assign(expr); } + // clang-format on } void uninitialized_domaint::assign(const exprt &lhs) diff --git a/src/cpp/cpp_id.cpp b/src/cpp/cpp_id.cpp index d6f53a29f6..9b8d7f8fc9 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"; @@ -113,6 +114,7 @@ std::ostream &operator<<(std::ostream &out, const cpp_idt::id_classt &id_class) case cpp_idt::id_classt::NAMESPACE: return out<<"NAMESPACE"; case cpp_idt::id_classt::ENUM: return out<<"ENUM"; } + // clang-format on UNREACHABLE; } diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp index a0848a8f68..709a11292d 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/src/goto-analyzer/taint_analysis.cpp @@ -71,6 +71,7 @@ void taint_analysist::instrument( goto_programt insert_before, insert_after; + // clang-format off if(instruction.is_function_call()) { const code_function_callt &function_call = @@ -203,6 +204,7 @@ void taint_analysist::instrument( } } } + // clang-format off if(!insert_before.empty()) { diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index ef31542380..8103691e12 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -271,6 +271,7 @@ std::list expressions_read( { std::list dest; + // clang-format off switch(instruction.type) { case ASSUME: @@ -319,6 +320,7 @@ std::list expressions_read( case NO_INSTRUCTION_TYPE: break; } + // clang-format on return dest; } diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index cc81414b2b..49dc4a6eda 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; @@ -90,6 +91,7 @@ void goto_trace_stept::output( 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 << ')'; diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp index 67ae3fc7e3..1113e82d28 100644 --- a/src/goto-programs/vcd_goto_trace.cpp +++ b/src/goto-programs/vcd_goto_trace.cpp @@ -113,6 +113,7 @@ void output_vcd( for(const auto &step : goto_trace.steps) { + // clang-format off if(step.is_assignment()) { auto lhs_object=step.get_lhs_object(); @@ -145,5 +146,6 @@ void output_vcd( } } } + // clang-format on } } diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index 74587a6066..f2dfbfd652 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -40,6 +40,7 @@ void convert( if(source_location.is_not_nil() && !source_location.get_file().empty()) xml_location=xml(source_location); + // clang-format off switch(step.type) { case goto_trace_stept::typet::ASSERT: @@ -227,6 +228,7 @@ void convert( } } } + // clang-format on if(source_location.is_not_nil() && !source_location.get_file().empty()) previous_source_location=source_location; diff --git a/src/pointer-analysis/value_set_domain_fi.cpp b/src/pointer-analysis/value_set_domain_fi.cpp index 0b2b68fcf8..c56b17355d 100644 --- a/src/pointer-analysis/value_set_domain_fi.cpp +++ b/src/pointer-analysis/value_set_domain_fi.cpp @@ -30,6 +30,7 @@ bool value_set_domain_fit::transform( // from_l->function << " " << from_l->location_number << " to " << // to_l->function << " " << to_l->location_number << '\n'; + // clang-format off switch(from_l->type) { case GOTO: @@ -71,6 +72,7 @@ bool value_set_domain_fit::transform( // do nothing break; } + // clang-format on 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 d98ad625e7..d2d5d0101b 100644 --- a/src/pointer-analysis/value_set_domain_fivr.cpp +++ b/src/pointer-analysis/value_set_domain_fivr.cpp @@ -30,6 +30,7 @@ bool value_set_domain_fivrt::transform( to_l->function << " " << to_l->location_number << '\n'; #endif + // clang-format off switch(from_l->type) { case END_FUNCTION: @@ -68,6 +69,7 @@ bool value_set_domain_fivrt::transform( case NO_INSTRUCTION_TYPE: break; } + // clang-format on 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 411a72b8ca..87ea310514 100644 --- a/src/pointer-analysis/value_set_domain_fivrns.cpp +++ b/src/pointer-analysis/value_set_domain_fivrns.cpp @@ -30,6 +30,7 @@ bool value_set_domain_fivrnst::transform( to_l->function << " " << to_l->location_number << '\n'; #endif + // clang-format off switch(from_l->type) { case END_FUNCTION: @@ -68,6 +69,7 @@ bool value_set_domain_fivrnst::transform( case NO_INSTRUCTION_TYPE: break; } + // clang-format on return value_set.handover(); } diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp index 816930fef1..2049232e99 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(); case tvt::tv_enumt::TV_UNKNOWN: return false_exprt(); // default } + // clang-format on } return false_exprt{}; // default @@ -243,6 +245,7 @@ exprt boolbvt::bv_get_rec( value=ch+value; } + // clang-format off switch(bvtype) { case bvtypet::IS_UNKNOWN: @@ -289,6 +292,7 @@ exprt boolbvt::bv_get_rec( return constant_exprt(bvrep, type); } } + // clang-format on UNREACHABLE; } diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp index f3cd29865b..1a236f0cae 100644 --- a/src/solvers/flattening/boolbv_typecast.cpp +++ b/src/solvers/flattening/boolbv_typecast.cpp @@ -325,6 +325,7 @@ bool boolbvt::type_conversion( case bvtypet::IS_UNSIGNED: case bvtypet::IS_SIGNED: case bvtypet::IS_C_ENUM: + // clang-format off switch(src_bvtype) { case bvtypet::IS_FLOAT: // float to integer @@ -448,6 +449,7 @@ bool boolbvt::type_conversion( return false; } } + // clang-format on break; case bvtypet::IS_VERILOG_UNSIGNED: diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp index ba36225660..fe9d547258 100644 --- a/src/solvers/refinement/bv_refinement_loop.cpp +++ b/src/solvers/refinement/bv_refinement_loop.cpp @@ -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; case propt::resultt::P_ERROR: return resultt::D_ERROR; } + // clang-format on UNREACHABLE; } diff --git a/src/util/config.cpp b/src/util/config.cpp index f41f903106..4ff19d6c7c 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1096,6 +1096,7 @@ 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"; @@ -1103,6 +1104,7 @@ std::string configt::ansi_ct::os_to_string(ost os) case ost::OS_WIN: return "win"; case ost::NO_OS: return "none"; } + // clang-format on UNREACHABLE; } From 81fb35fdfd768dbe5defd40f68936d2e5a9c0344 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 8 Nov 2018 21:51:50 +0000 Subject: [PATCH 4/6] clang-format switch statements touched in this PR --- .../java_bytecode/java_bytecode_language.cpp | 68 +++--- src/analyses/escape_analysis.cpp | 110 ++++----- src/analyses/global_may_alias.cpp | 30 ++- src/analyses/interval_domain.cpp | 36 ++- src/analyses/local_bitvector_analysis.cpp | 58 +++-- src/analyses/local_may_alias.cpp | 68 +++--- src/analyses/uninitialized_domain.cpp | 33 ++- src/goto-analyzer/taint_analysis.cpp | 224 +++++++++--------- src/goto-programs/goto_program.cpp | 27 +-- src/goto-programs/vcd_goto_trace.cpp | 56 ++--- src/goto-programs/xml_goto_trace.cpp | 170 ++++++------- src/pointer-analysis/value_set_domain_fi.cpp | 10 +- .../value_set_domain_fivr.cpp | 13 +- .../value_set_domain_fivrns.cpp | 13 +- src/solvers/flattening/boolbv_get.cpp | 12 +- src/solvers/flattening/boolbv_typecast.cpp | 2 - src/solvers/refinement/bv_refinement_loop.cpp | 8 +- 17 files changed, 451 insertions(+), 487 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 9776cd8b01..1e5a42cb97 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -791,46 +791,44 @@ bool java_bytecode_languaget::typecheck( // Now incrementally elaborate methods // that are reachable from this entry point. - // clang-format off 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; - case LAZY_METHODS_MODE_EXTERNAL_DRIVER: - // 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; } - // clang-format on // now instrument runtime exceptions java_bytecode_instrument( diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp index dde3d31c82..f0a4a3b7e8 100644 --- a/src/analyses/escape_analysis.cpp +++ b/src/analyses/escape_analysis.cpp @@ -457,72 +457,60 @@ void escape_analysist::instrument( const goto_programt::instructiont &instruction=*i_it; - // clang-format off if(instruction.type == ASSIGN) - { - const code_assignt &code_assign=to_code_assign(instruction.code); + { + 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); - } + 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; + + 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()) { - const code_deadt &code_dead=to_code_dead(instruction.code); - - std::set 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 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++; - } + cleanup_functions1.insert( + m_it->second.cleanup_functions.begin(), + m_it->second.cleanup_functions.end()); } - // clang-format on + + 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++; + } + + for(const auto &c : cleanup_functions2) + { + (void)c; + i_it++; + } + } } Forall_goto_program_instructions(i_it, f_it->second.body) diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp index e15a6ecee4..1c6c390cfd 100644 --- a/src/analyses/global_may_alias.cpp +++ b/src/analyses/global_may_alias.cpp @@ -103,32 +103,31 @@ void global_may_alias_domaint::transform( const goto_programt::instructiont &instruction=*from; - // clang-format off 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; + } case FUNCTION_CALL: case GOTO: @@ -149,7 +148,6 @@ void global_may_alias_domaint::transform( case NO_INSTRUCTION_TYPE: break; } - // clang-format on } void global_may_alias_domaint::output( diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index fcc5a11c3b..77f570a492 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -64,7 +64,6 @@ void interval_domaint::transform( ai_baset &, const namespacet &ns) { - // clang-format off const goto_programt::instructiont &instruction=*from; switch(instruction.type) { @@ -81,33 +80,33 @@ 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; + } case CATCH: case THROW: @@ -125,7 +124,6 @@ void interval_domaint::transform( case NO_INSTRUCTION_TYPE: break; } - // clang-format on } /// Sets *this to the mathematical join between the two domains. This can be diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp index 3a9a2a7c99..77c7519e6c 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/src/analyses/local_bitvector_analysis.cpp @@ -266,48 +266,47 @@ void local_bitvector_analysist::build() auto &loc_info_src=loc_infos[loc_nr]; auto loc_info_dest=loc_infos[loc_nr]; - // clang-format off 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; + } case CATCH: case THROW: @@ -327,7 +326,6 @@ void local_bitvector_analysist::build() case NO_INSTRUCTION_TYPE: break; } - // clang-format on for(const auto &succ : node.successors) { diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp index 73db6c9e2d..282245421e 100644 --- a/src/analyses/local_may_alias.cpp +++ b/src/analyses/local_may_alias.cpp @@ -365,60 +365,57 @@ void local_may_aliast::build(const goto_functiont &goto_function) const loc_infot &loc_info_src=loc_infos[loc_nr]; loc_infot loc_info_dest=loc_infos[loc_nr]; - // clang-format off 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; iis_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); - } + if(!symbol.is_static_lifetime) + uninitialized.insert(identifier); + } else - { - std::list read=expressions_read(*from); - std::list written=expressions_written(*from); + { + std::list read = expressions_read(*from); + std::list 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); - } - // clang-format on + // we only care about the *first* uninitalized use + for(const auto &expr : read) + assign(expr); + } } void uninitialized_domaint::assign(const exprt &lhs) diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp index 709a11292d..770c771364 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/src/goto-analyzer/taint_analysis.cpp @@ -71,140 +71,138 @@ void taint_analysist::instrument( goto_programt insert_before, insert_after; - // clang-format off if(instruction.is_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 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 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; + } } } } } - // clang-format off + } if(!insert_before.empty()) { diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 8103691e12..9c3f7f3470 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -271,7 +271,6 @@ std::list expressions_read( { std::list dest; - // clang-format off switch(instruction.type) { case ASSUME: @@ -286,23 +285,22 @@ 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; + } case CATCH: case THROW: @@ -320,7 +318,6 @@ std::list expressions_read( case NO_INSTRUCTION_TYPE: break; } - // clang-format on return dest; } diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp index 1113e82d28..f14749c243 100644 --- a/src/goto-programs/vcd_goto_trace.cpp +++ b/src/goto-programs/vcd_goto_trace.cpp @@ -113,39 +113,41 @@ void output_vcd( for(const auto &step : goto_trace.steps) { - // clang-format off if(step.is_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); + out << "x" + << "V" << number << "\n"; + } + else + { + std::string binary = as_vcd_binary(step.full_lhs_value, ns); - if(!binary.empty()) - out << "b" << binary << " V" << number << " " << "\n"; - } + if(!binary.empty()) + out << "b" << binary << " V" << number << " " + << "\n"; } } - // clang-format on + } } } diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index f2dfbfd652..b7f8fc43b1 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -40,7 +40,6 @@ void convert( if(source_location.is_not_nil() && !source_location.get_file().empty()) xml_location=xml(source_location); - // clang-format off switch(step.type) { case goto_trace_stept::typet::ASSERT: @@ -61,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; @@ -85,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: { @@ -175,29 +182,29 @@ 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; + } case goto_trace_stept::typet::ATOMIC_BEGIN: case goto_trace_stept::typet::ATOMIC_END: @@ -228,7 +235,6 @@ void convert( } } } - // clang-format on if(source_location.is_not_nil() && !source_location.get_file().empty()) previous_source_location=source_location; diff --git a/src/pointer-analysis/value_set_domain_fi.cpp b/src/pointer-analysis/value_set_domain_fi.cpp index c56b17355d..e8c5917003 100644 --- a/src/pointer-analysis/value_set_domain_fi.cpp +++ b/src/pointer-analysis/value_set_domain_fi.cpp @@ -30,7 +30,6 @@ bool value_set_domain_fit::transform( // from_l->function << " " << from_l->location_number << " to " << // to_l->function << " " << to_l->location_number << '\n'; - // clang-format off switch(from_l->type) { case GOTO: @@ -48,12 +47,12 @@ 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; + } case CATCH: case THROW: @@ -72,7 +71,6 @@ bool value_set_domain_fit::transform( // do nothing break; } - // clang-format on 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 d2d5d0101b..5491616640 100644 --- a/src/pointer-analysis/value_set_domain_fivr.cpp +++ b/src/pointer-analysis/value_set_domain_fivr.cpp @@ -30,7 +30,6 @@ bool value_set_domain_fivrt::transform( to_l->function << " " << to_l->location_number << '\n'; #endif - // clang-format off switch(from_l->type) { case END_FUNCTION: @@ -44,13 +43,12 @@ 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; + } case CATCH: case THROW: @@ -69,7 +67,6 @@ bool value_set_domain_fivrt::transform( case NO_INSTRUCTION_TYPE: break; } - // clang-format on 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 87ea310514..43a0594ca6 100644 --- a/src/pointer-analysis/value_set_domain_fivrns.cpp +++ b/src/pointer-analysis/value_set_domain_fivrns.cpp @@ -30,7 +30,6 @@ bool value_set_domain_fivrnst::transform( to_l->function << " " << to_l->location_number << '\n'; #endif - // clang-format off switch(from_l->type) { case END_FUNCTION: @@ -44,13 +43,12 @@ 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; + } case CATCH: case THROW: @@ -69,7 +67,6 @@ bool value_set_domain_fivrnst::transform( case NO_INSTRUCTION_TYPE: break; } - // clang-format on return value_set.handover(); } diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp index 2049232e99..3f559cfb61 100644 --- a/src/solvers/flattening/boolbv_get.cpp +++ b/src/solvers/flattening/boolbv_get.cpp @@ -245,7 +245,6 @@ exprt boolbvt::bv_get_rec( value=ch+value; } - // clang-format off switch(bvtype) { case bvtypet::IS_UNKNOWN: @@ -268,13 +267,13 @@ 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; + } case bvtypet::IS_C_BIT_FIELD: case bvtypet::IS_VERILOG_UNSIGNED: @@ -292,7 +291,6 @@ exprt boolbvt::bv_get_rec( return constant_exprt(bvrep, type); } } - // clang-format on UNREACHABLE; } diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp index 1a236f0cae..f3cd29865b 100644 --- a/src/solvers/flattening/boolbv_typecast.cpp +++ b/src/solvers/flattening/boolbv_typecast.cpp @@ -325,7 +325,6 @@ bool boolbvt::type_conversion( case bvtypet::IS_UNSIGNED: case bvtypet::IS_SIGNED: case bvtypet::IS_C_ENUM: - // clang-format off switch(src_bvtype) { case bvtypet::IS_FLOAT: // float to integer @@ -449,7 +448,6 @@ bool boolbvt::type_conversion( return false; } } - // clang-format on break; case bvtypet::IS_VERILOG_UNSIGNED: diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp index fe9d547258..0f192f78de 100644 --- a/src/solvers/refinement/bv_refinement_loop.cpp +++ b/src/solvers/refinement/bv_refinement_loop.cpp @@ -108,11 +108,11 @@ decision_proceduret::resultt bv_refinementt::prop_solve() // clang-format off switch(result) { - 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; + 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 on + // clang-format off UNREACHABLE; } From d28968c29eca0d493ab81cc3baeb95db3d387238 Mon Sep 17 00:00:00 2001 From: martin Date: Mon, 4 Mar 2019 11:46:08 +0000 Subject: [PATCH 5/6] Annotate missed cases in the transform functions of various domains There are a number of reasons why instruction types were left out of these case statements : 1. Ignoring this instruction is generally a valid overapproximation. 2. Ignoring this instruction is a valid overapproximation for this domain. 3. The instruction is assumed to not be present due to preceding passes. 4. The instruction should never appear in any valid goto program. 5. The instruction is newer than the analysis code and was forgotten. This patch tries to correctly document which of these apply. --- src/analyses/custom_bitvector_analysis.cpp | 24 +++++++++----- src/analyses/escape_analysis.cpp | 27 ++++++++++----- src/analyses/global_may_alias.cpp | 31 ++++++++++------- src/analyses/interval_domain.cpp | 24 +++++++++----- src/analyses/invariant_set_domain.cpp | 19 ++++++----- src/analyses/local_bitvector_analysis.cpp | 29 ++++++++++------ src/analyses/local_cfg.cpp | 5 ++- src/analyses/local_may_alias.cpp | 29 ++++++++++------ src/analyses/uncaught_exceptions_analysis.cpp | 33 +++++++++++-------- 9 files changed, 142 insertions(+), 79 deletions(-) diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index cd7ddfcaf3..ef97471298 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -538,18 +538,24 @@ void custom_bitvector_domaint::transform( case CATCH: case THROW: + DATA_INVARIANT(false, "Exceptions must be removed before analysis"); + break; case RETURN: - case ATOMIC_BEGIN: - case ATOMIC_END: - case END_FUNCTION: - case LOCATION: - case START_THREAD: - case END_THREAD: - case SKIP: - case ASSERT: - case ASSUME: + 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 f0a4a3b7e8..a052c8b5d7 100644 --- a/src/analyses/escape_analysis.cpp +++ b/src/analyses/escape_analysis.cpp @@ -253,21 +253,30 @@ void escape_domaint::transform( // This is the edge to the call site. break; - case GOTO: + 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: - case ATOMIC_BEGIN: - case ATOMIC_END: - case LOCATION: - case START_THREAD: - case END_THREAD: - case ASSERT: - case ASSUME: - case SKIP: + 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: + 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/global_may_alias.cpp b/src/analyses/global_may_alias.cpp index 1c6c390cfd..1d74895983 100644 --- a/src/analyses/global_may_alias.cpp +++ b/src/analyses/global_may_alias.cpp @@ -129,23 +129,32 @@ void global_may_alias_domaint::transform( break; } - case FUNCTION_CALL: - case GOTO: + 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: - case ATOMIC_BEGIN: - case ATOMIC_END: - case LOCATION: - case START_THREAD: - case END_THREAD: - case ASSERT: - case ASSUME: - case SKIP: - case END_FUNCTION: + 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 77f570a492..07a7034fc8 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -110,18 +110,26 @@ void interval_domaint::transform( case CATCH: case THROW: + DATA_INVARIANT(false, "Exceptions must be removed before analysis"); + break; case RETURN: - case ATOMIC_BEGIN: - case ATOMIC_END: - case END_FUNCTION: - case START_THREAD: - case END_THREAD: - case ASSERT: - case LOCATION: - case SKIP: + 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: + 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/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp index b1cfd2ee42..0133120cb6 100644 --- a/src/analyses/invariant_set_domain.cpp +++ b/src/analyses/invariant_set_domain.cpp @@ -77,16 +77,19 @@ void invariant_set_domaint::transform( case CATCH: case THROW: - case DEAD: - case ATOMIC_BEGIN: - case ATOMIC_END: - case END_FUNCTION: - case LOCATION: - case END_THREAD: - case SKIP: + 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: - // do nothing + 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 77c7519e6c..4314f74e7d 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/src/analyses/local_bitvector_analysis.cpp @@ -310,20 +310,29 @@ void local_bitvector_analysist::build() case CATCH: case THROW: + DATA_INVARIANT(false, "Exceptions must be removed before analysis"); + break; case RETURN: - case ATOMIC_BEGIN: - case ATOMIC_END: - case LOCATION: - case START_THREAD: - case END_THREAD: - case SKIP: + 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 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: - case ASSERT: - case ASSUME: - case GOTO: - case END_FUNCTION: + 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/local_cfg.cpp b/src/analyses/local_cfg.cpp index 78d4079ccd..3ac29f020d 100644 --- a/src/analyses/local_cfg.cpp +++ b/src/analyses/local_cfg.cpp @@ -86,9 +86,12 @@ void local_cfgt::build(const goto_programt &goto_program) case DECL: case DEAD: case ASSIGN: + node.successors.push_back(loc_nr + 1); + break; + case INCOMPLETE_GOTO: case NO_INSTRUCTION_TYPE: - node.successors.push_back(loc_nr+1); + 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 282245421e..9ea7e7009f 100644 --- a/src/analyses/local_may_alias.cpp +++ b/src/analyses/local_may_alias.cpp @@ -419,20 +419,29 @@ void local_may_aliast::build(const goto_functiont &goto_function) case CATCH: case THROW: + DATA_INVARIANT(false, "Exceptions must be removed before analysis"); + break; case RETURN: - case GOTO: - case START_THREAD: - case END_THREAD: - case ATOMIC_BEGIN: - case ATOMIC_END: - case LOCATION: - case SKIP: - case END_FUNCTION: + DATA_INVARIANT(false, "Returns must be removed before analysis"); + 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: - case ASSERT: - case ASSUME: + 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/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp index af3e4e89b9..2ba9c97053 100644 --- a/src/analyses/uncaught_exceptions_analysis.cpp +++ b/src/analyses/uncaught_exceptions_analysis.cpp @@ -125,23 +125,30 @@ void uncaught_exceptions_domaint::transform( join(uea.exceptions_map[function_name]); break; } - case DECL: - case DEAD: - case ASSIGN: + 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: - case GOTO: - case ATOMIC_BEGIN: - case ATOMIC_END: - case START_THREAD: - case END_THREAD: - case END_FUNCTION: - case ASSERT: - case ASSUME: - case LOCATION: - case SKIP: + DATA_INVARIANT(false, "Returns must be removed before analysis"); + 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: + 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; } } From 93b2371ff7dfbd7530bc281e869eea78036b861e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 Mar 2019 16:03:58 +0000 Subject: [PATCH 6/6] Disable a number of invariants that currently fail This takes us back to the behaviour prior to this series of commits, and effectively is a to-do list to be addressed. We should either handle the cases, or get rid of the instruction type. --- src/analyses/escape_analysis.cpp | 2 ++ src/analyses/interval_domain.cpp | 2 ++ src/analyses/local_bitvector_analysis.cpp | 6 ++++++ src/analyses/local_may_alias.cpp | 4 ++++ src/analyses/uncaught_exceptions_analysis.cpp | 4 ++++ 5 files changed, 18 insertions(+) diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp index a052c8b5d7..b206100224 100644 --- a/src/analyses/escape_analysis.cpp +++ b/src/analyses/escape_analysis.cpp @@ -272,7 +272,9 @@ void escape_domaint::transform( 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: diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 07a7034fc8..b857a74dd8 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -125,7 +125,9 @@ void interval_domaint::transform( 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: diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp index 4314f74e7d..13b41001cc 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/src/analyses/local_bitvector_analysis.cpp @@ -310,11 +310,15 @@ void local_bitvector_analysist::build() 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 @@ -327,8 +331,10 @@ void local_bitvector_analysist::build() 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: diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp index 9ea7e7009f..b762c97b71 100644 --- a/src/analyses/local_may_alias.cpp +++ b/src/analyses/local_may_alias.cpp @@ -422,7 +422,9 @@ void local_may_aliast::build(const goto_functiont &goto_function) 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 @@ -436,8 +438,10 @@ void local_may_aliast::build(const goto_functiont &goto_function) 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: diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp index 2ba9c97053..1b8d1fa0e7 100644 --- a/src/analyses/uncaught_exceptions_analysis.cpp +++ b/src/analyses/uncaught_exceptions_analysis.cpp @@ -130,7 +130,9 @@ void uncaught_exceptions_domaint::transform( 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 @@ -144,7 +146,9 @@ void uncaught_exceptions_domaint::transform( 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: