Skip to content

Commit ca49d2e

Browse files
tautschnigtautschnig
authored
Merge pull request #3414 from tautschnig/add-return-value
Avoid warning about not returning a value [blocks: #2548]
2 parents 223e3a6 + c805422 commit ca49d2e

15 files changed

+43
-24
lines changed

‎src/cbmc/bmc.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -485,6 +485,8 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)
485485

486486
return resultt::ERROR;
487487
}
488+
489+
UNREACHABLE;
488490
}
489491

490492
/// Perform core BMC, using an abstract model to supply GOTO function bodies

‎src/cbmc/fault_localization.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -315,6 +315,8 @@ safety_checkert::resultt fault_localizationt::stop_on_fail()
315315

316316
return safety_checkert::resultt::ERROR;
317317
}
318+
319+
UNREACHABLE;
318320
}
319321

320322
void fault_localizationt::goal_covered(

‎src/cpp/cpp_id.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <ostream>
1515

16+
#include <util/invariant.h>
17+
1618
#include "cpp_scope.h"
1719

1820
cpp_idt::cpp_idt():
@@ -111,4 +113,6 @@ std::ostream &operator<<(std::ostream &out, const cpp_idt::id_classt &id_class)
111113
case cpp_idt::id_classt::NAMESPACE: return out<<"NAMESPACE";
112114
default: return out << "(OTHER)";
113115
}
116+
117+
UNREACHABLE;
114118
}

‎src/goto-programs/format_strings.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,11 +11,11 @@ Author: CM Wintersteiger
1111

1212
#include "format_strings.h"
1313

14+
#include <util/c_types.h>
1415
#include <util/exception_utils.h>
15-
#include <util/std_types.h>
16+
#include <util/invariant.h>
1617
#include <util/std_expr.h>
17-
18-
#include <util/c_types.h>
18+
#include <util/std_types.h>
1919

2020
#include <cctype>
2121

@@ -293,4 +293,6 @@ typet get_type(const format_tokent &token)
293293
default:
294294
return nil_typet();
295295
}
296+
297+
UNREACHABLE;
296298
}

‎src/goto-programs/goto_program.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
1616

1717
#include <util/expr_iterator.h>
1818
#include <util/find_symbols.h>
19+
#include <util/invariant.h>
1920
#include <util/std_expr.h>
2021
#include <util/validate.h>
2122

‎src/goto-programs/remove_function_pointers.cpp

Lines changed: 5 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -138,21 +138,15 @@ bool remove_function_pointerst::arg_is_type_compatible(
138138
call_type.id()==ID_c_enum ||
139139
call_type.id()==ID_c_enum_tag)
140140
{
141-
if(function_type.id()==ID_signedbv ||
142-
function_type.id()==ID_unsigned ||
143-
function_type.id()==ID_bool ||
144-
function_type.id()==ID_pointer ||
145-
function_type.id()==ID_c_enum ||
146-
function_type.id()==ID_c_enum_tag)
147-
return true;
148-
149-
return false;
141+
return function_type.id() == ID_signedbv ||
142+
function_type.id() == ID_unsigned || function_type.id() == ID_bool ||
143+
function_type.id() == ID_pointer ||
144+
function_type.id() == ID_c_enum ||
145+
function_type.id() == ID_c_enum_tag;
150146
}
151147

152148
return pointer_offset_bits(call_type, ns) ==
153149
pointer_offset_bits(function_type, ns);
154-
155-
return false;
156150
}
157151

158152
bool remove_function_pointerst::is_type_compatible(

‎src/solvers/flattening/boolbv_extractbit.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,4 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
8585
return literal;
8686
}
8787
}
88-
89-
return SUB::convert_rest(expr);
9088
}

‎src/solvers/flattening/bv_utils.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -818,8 +818,9 @@ bvt bv_utilst::multiplier(
818818
{
819819
case representationt::SIGNED: return signed_multiplier(op0, op1);
820820
case representationt::UNSIGNED: return unsigned_multiplier(op0, op1);
821-
default: UNREACHABLE;
822821
}
822+
823+
UNREACHABLE;
823824
}
824825

825826
bvt bv_utilst::multiplier_no_overflow(
@@ -833,8 +834,9 @@ bvt bv_utilst::multiplier_no_overflow(
833834
return signed_multiplier_no_overflow(op0, op1);
834835
case representationt::UNSIGNED:
835836
return unsigned_multiplier_no_overflow(op0, op1);
836-
default: UNREACHABLE;
837837
}
838+
839+
UNREACHABLE;
838840
}
839841

840842
void bv_utilst::signed_divider(
@@ -887,8 +889,6 @@ void bv_utilst::divider(
887889
signed_divider(op0, op1, result, remainer); break;
888890
case representationt::UNSIGNED:
889891
unsigned_divider(op0, op1, result, remainer); break;
890-
default:
891-
UNREACHABLE;
892892
}
893893
}
894894

‎src/solvers/prop/prop_conv.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -480,6 +480,8 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve()
480480
case propt::resultt::P_UNSATISFIABLE: return resultt::D_UNSATISFIABLE;
481481
default: return resultt::D_ERROR;
482482
}
483+
484+
UNREACHABLE;
483485
}
484486

485487
exprt prop_conv_solvert::get(const exprt &expr) const

‎src/solvers/refinement/bv_refinement_loop.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -108,6 +108,8 @@ decision_proceduret::resultt bv_refinementt::prop_solve()
108108
case propt::resultt::P_UNSATISFIABLE: return resultt::D_UNSATISFIABLE;
109109
default: return resultt::D_ERROR;
110110
}
111+
112+
UNREACHABLE;
111113
}
112114

113115
void bv_refinementt::check_SAT()

‎src/solvers/smt2/smt2_parser.cpp

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
1212

1313
#include <util/arith_tools.h>
1414
#include <util/ieee_float.h>
15+
#include <util/invariant.h>
1516
#include <util/range.h>
1617

1718
#include <numeric>
@@ -906,6 +907,8 @@ exprt smt2_parsert::function_application()
906907

907908
return tmp;
908909
}
910+
911+
UNREACHABLE;
909912
}
910913

911914
exprt smt2_parsert::expression()
@@ -997,6 +1000,8 @@ exprt smt2_parsert::expression()
9971000
default:
9981001
throw error("unexpected token in an expression");
9991002
}
1003+
1004+
UNREACHABLE;
10001005
}
10011006

10021007
typet smt2_parsert::sort()
@@ -1080,6 +1085,8 @@ typet smt2_parsert::sort()
10801085
default:
10811086
throw error() << "unexpected token in a sort: `" << buffer << '\'';
10821087
}
1088+
1089+
UNREACHABLE;
10831090
}
10841091

10851092
smt2_parsert::signature_with_parameter_idst

‎src/util/byte_operators.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,8 @@ irep_idt byte_extract_id()
2323
default:
2424
UNREACHABLE;
2525
}
26+
27+
UNREACHABLE;
2628
}
2729

2830
irep_idt byte_update_id()
@@ -38,4 +40,6 @@ irep_idt byte_update_id()
3840
default:
3941
UNREACHABLE;
4042
}
43+
44+
UNREACHABLE;
4145
}

‎src/util/config.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1102,6 +1102,8 @@ std::string configt::ansi_ct::os_to_string(ost os)
11021102
case ost::OS_WIN: return "win";
11031103
default: return "none";
11041104
}
1105+
1106+
UNREACHABLE;
11051107
}
11061108

11071109
configt::ansi_ct::ost configt::ansi_ct::string_to_os(const std::string &os)

‎src/util/invariant.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -149,7 +149,7 @@ class invariant_with_diagnostics_failedt : public invariant_failedt
149149

150150
#ifdef __GNUC__
151151
#define CBMC_NORETURN __attribute((noreturn))
152-
#elif defined(_MSV_VER)
152+
#elif defined(_MSC_VER)
153153
#define CBMC_NORETURN __declspec(noreturn)
154154
#elif __cplusplus >= 201703L
155155
#define CBMC_NORETURN [[noreturn]]
@@ -391,8 +391,6 @@ CBMC_NORETURN void report_invariant_failure(
391391
__VA_ARGS__); /* NOLINT */ \
392392
} while(false)
393393

394-
#endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block
395-
396394
// Short hand macros. The variants *_STRUCTURED below allow to specify a custom
397395
// exception, and are equivalent to INVARIANT_STRUCTURED.
398396

@@ -426,6 +424,8 @@ CBMC_NORETURN void report_invariant_failure(
426424
} \
427425
} while(false)
428426

427+
#endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block
428+
429429
// The condition should only contain (unmodified) inputs to the method. Inputs
430430
// include arguments passed to the function, as well as member variables that
431431
// the function may read.

‎src/util/std_types.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,6 @@ std::size_t struct_union_typet::component_number(
4646
}
4747

4848
UNREACHABLE;
49-
return 0;
5049
}
5150

5251
/// Get the reference to a component with given name.

0 commit comments

Comments
 (0)