Skip to content

Commit 5a04db9

Browse files
author
Daniel Kroening
committed
replace assert(false) by UNREACHABLE
1 parent 90b1ed6 commit 5a04db9

File tree

90 files changed

+214
-202
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

90 files changed

+214
-202
lines changed

‎src/analyses/constant_propagator.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -79,7 +79,7 @@ void constant_propagator_domaint::assign_rec(
7979
cond = simplify_expr(cond,ns);
8080
}
8181
else
82-
assert(0);
82+
UNREACHABLE;
8383

8484
assign(values, to_symbol_expr(lhs), cond, ns);
8585
}

‎src/analyses/custom_bitvector_analysis.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -296,7 +296,7 @@ void custom_bitvector_domaint::transform(
296296
else if(identifier=="__CPROVER_clear_may")
297297
mode=modet::CLEAR_MAY;
298298
else
299-
assert(false);
299+
UNREACHABLE;
300300

301301
exprt lhs=code_function_call.arguments()[0];
302302

@@ -411,7 +411,7 @@ void custom_bitvector_domaint::transform(
411411
else if(statement=="clear_may")
412412
mode=modet::CLEAR_MAY;
413413
else
414-
assert(false);
414+
UNREACHABLE;
415415

416416
exprt lhs=instruction.code.op0();
417417

‎src/analyses/goto_check.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -833,7 +833,7 @@ void goto_checkt::nan_check(
833833
equal_exprt(expr.op1(), minus_inf)));
834834
}
835835
else
836-
assert(false);
836+
UNREACHABLE;
837837

838838
isnan.make_not();
839839

‎src/analyses/goto_rw.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -713,7 +713,7 @@ void goto_rw(goto_programt::const_targett target,
713713
switch(target->type)
714714
{
715715
case NO_INSTRUCTION_TYPE:
716-
assert(false);
716+
UNREACHABLE;
717717
break;
718718

719719
case GOTO:

‎src/analyses/invariant_set.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -474,7 +474,7 @@ void invariant_sett::strengthen_rec(const exprt &expr)
474474
}
475475
}
476476
else
477-
assert(false);
477+
UNREACHABLE;
478478
}
479479
else if(expr.id()==ID_equal)
480480
{
@@ -673,7 +673,7 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
673673
else if(expr.id()==ID_notequal)
674674
return is_ne(p);
675675
else
676-
assert(false);
676+
UNREACHABLE;
677677
}
678678

679679
return tvt::unknown();

‎src/ansi-c/ansi_c_convert_type.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -460,7 +460,7 @@ void ansi_c_convert_typet::write(typet &type)
460460
else
461461
type=unsigned_long_long_int_type();
462462
else
463-
assert(false);
463+
UNREACHABLE;
464464
}
465465
else if(gcc_int128_cnt)
466466
{

‎src/ansi-c/ansi_c_declaration.cpp

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

1717
#include <util/config.h>
1818
#include <util/std_types.h>
19+
#include <util/invariant.h>
1920

2021
void ansi_c_declaratort::build(irept &src)
2122
{
@@ -36,7 +37,7 @@ void ansi_c_declaratort::build(irept &src)
3637
else if(t.id().empty() ||
3738
t.is_nil())
3839
{
39-
assert(0);
40+
UNREACHABLE;
4041
}
4142
else if(t.id()==ID_abstract)
4243
{
@@ -108,7 +109,7 @@ typet ansi_c_declarationt::full_type(
108109
p=&(p->subtypes().back());
109110
}
110111
else
111-
assert(false);
112+
UNREACHABLE;
112113
}
113114

114115
*p=type();

‎src/ansi-c/ansi_c_entry_point.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -305,7 +305,7 @@ bool ansi_c_entry_point(
305305
max=to_unsignedbv_type(envp_size_symbol.type).largest();
306306
}
307307
else
308-
assert(false);
308+
UNREACHABLE;
309309

310310
exprt max_minus_one=from_integer(max-1, envp_size_symbol.type);
311311

@@ -431,7 +431,7 @@ bool ansi_c_entry_point(
431431
}
432432
}
433433
else
434-
assert(false);
434+
UNREACHABLE;
435435
}
436436
else
437437
{

‎src/ansi-c/c_preprocess.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,7 @@ static std::string type_max(const typet &src)
106106
return integer2string(
107107
power(2, to_unsignedbv_type(src).get_width()-1)-1);
108108
else
109-
assert(false);
109+
UNREACHABLE;
110110
}
111111

112112
/// quote a string for bash and CMD
@@ -766,7 +766,7 @@ bool c_preprocess_gcc_clang(
766766
else if(config.ansi_c.wchar_t_width==config.ansi_c.char_width)
767767
command+=" -D__WCHAR_TYPE__=\""+sig+" char\"";
768768
else
769-
assert(false);
769+
UNREACHABLE;
770770
}
771771

772772
if(config.ansi_c.char_is_unsigned)
@@ -804,7 +804,7 @@ bool c_preprocess_gcc_clang(
804804
break;
805805

806806
default:
807-
assert(false);
807+
UNREACHABLE;
808808
}
809809

810810
// Standard Defines, ANSI9899 6.10.8

‎src/ansi-c/c_typecast.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -378,11 +378,11 @@ void c_typecastt::implicit_typecast_arithmetic(
378378
}
379379
return;
380380

381-
case BOOL: assert(false); // should always be promoted to int
382-
case CHAR: assert(false); // should always be promoted to int
383-
case UCHAR: assert(false); // should always be promoted to int
384-
case SHORT: assert(false); // should always be promoted to int
385-
case USHORT: assert(false); // should always be promoted to int
381+
case BOOL: UNREACHABLE; // should always be promoted to int
382+
case CHAR: UNREACHABLE; // should always be promoted to int
383+
case UCHAR: UNREACHABLE; // should always be promoted to int
384+
case SHORT: UNREACHABLE; // should always be promoted to int
385+
case USHORT: UNREACHABLE; // should always be promoted to int
386386
case INT: new_type=signed_int_type(); break;
387387
case UINT: new_type=unsigned_int_type(); break;
388388
case LONG: new_type=signed_long_int_type(); break;

0 commit comments

Comments
 (0)