Skip to content

Commit e32eb8c

Browse files
tautschnigtautschnig
committed
Replace assert(...) by macros from invariant.h
While new/modified code shouldn't use assert(...) anyway, we had several existing uses of assert. Once we remove nonstd/optional.h, we will no longer implicitly include cassert, implying that a lot of #include <cassert> changes will be necessary. Instead of adding these, go all the way and fix the undesired uses of assert.
1 parent 31f1b59 commit e32eb8c

File tree

118 files changed

+659
-579
lines changed

Some content is hidden

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

118 files changed

+659
-579
lines changed

‎jbmc/src/java_bytecode/character_refine_preprocess.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ codet character_refine_preprocesst::convert_char_function(
2727
conversion_inputt &target)
2828
{
2929
const code_function_callt &function_call=target;
30-
assert(function_call.arguments().size()==1);
30+
PRECONDITION(function_call.arguments().size() == 1);
3131
const exprt &arg=function_call.arguments()[0];
3232
const exprt &result=function_call.lhs();
3333
const typet &type=result.type();
@@ -111,7 +111,7 @@ codet character_refine_preprocesst::convert_char_value(
111111
codet character_refine_preprocesst::convert_compare(conversion_inputt &target)
112112
{
113113
const code_function_callt &function_call=target;
114-
assert(function_call.arguments().size()==2);
114+
PRECONDITION(function_call.arguments().size() == 2);
115115
const exprt &char1=function_call.arguments()[0];
116116
const exprt &char2=function_call.arguments()[1];
117117
const exprt &result=function_call.lhs();
@@ -223,7 +223,7 @@ codet character_refine_preprocesst::convert_digit_int(conversion_inputt &target)
223223
codet character_refine_preprocesst::convert_for_digit(conversion_inputt &target)
224224
{
225225
const code_function_callt &function_call=target;
226-
assert(function_call.arguments().size()==2);
226+
PRECONDITION(function_call.arguments().size() == 2);
227227
const exprt &digit=function_call.arguments()[0];
228228
const exprt &result=function_call.lhs();
229229
const typet &type=result.type();
@@ -586,7 +586,7 @@ codet character_refine_preprocesst::convert_is_ideographic(
586586
conversion_inputt &target)
587587
{
588588
const code_function_callt &function_call=target;
589-
assert(function_call.arguments().size()==1);
589+
PRECONDITION(function_call.arguments().size() == 1);
590590
const exprt &arg=function_call.arguments()[0];
591591
const exprt &result=function_call.lhs();
592592
exprt is_ideograph=in_interval_expr(arg, 0x4E00, 0x9FFF);
@@ -600,7 +600,7 @@ codet character_refine_preprocesst::convert_is_ISO_control_char(
600600
conversion_inputt &target)
601601
{
602602
const code_function_callt &function_call=target;
603-
assert(function_call.arguments().size()==1);
603+
PRECONDITION(function_call.arguments().size() == 1);
604604
const exprt &arg=function_call.arguments()[0];
605605
const exprt &result=function_call.lhs();
606606
or_exprt iso(
@@ -758,7 +758,7 @@ codet character_refine_preprocesst::convert_is_low_surrogate(
758758
conversion_inputt &target)
759759
{
760760
const code_function_callt &function_call=target;
761-
assert(function_call.arguments().size()==1);
761+
PRECONDITION(function_call.arguments().size() == 1);
762762
const exprt &arg=function_call.arguments()[0];
763763
const exprt &result=function_call.lhs();
764764
exprt is_low_surrogate=in_interval_expr(arg, 0xDC00, 0xDFFF);
@@ -895,7 +895,7 @@ codet character_refine_preprocesst::convert_is_surrogate_pair(
895895
conversion_inputt &target)
896896
{
897897
const code_function_callt &function_call=target;
898-
assert(function_call.arguments().size()==2);
898+
PRECONDITION(function_call.arguments().size() == 2);
899899
const exprt &arg0=function_call.arguments()[0];
900900
const exprt &arg1=function_call.arguments()[1];
901901
const exprt &result=function_call.lhs();

‎jbmc/src/java_bytecode/expr2java.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -117,7 +117,9 @@ std::string expr2javat::convert_struct(
117117
const struct_typet::componentst &components=
118118
struct_type.components();
119119

120-
assert(components.size()==src.operands().size());
120+
DATA_INVARIANT(
121+
components.size() == src.operands().size(),
122+
"inconsistent number of components");
121123

122124
exprt::operandst::const_iterator o_it=src.operands().begin();
123125

‎jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -765,8 +765,8 @@ void java_bytecode_convert_classt::convert(
765765
if(s_it!=symbol_table.symbols.end())
766766
symbol_table.erase(s_it); // erase, we stubbed it
767767

768-
if(symbol_table.add(new_symbol))
769-
assert(false && "failed to add static field symbol");
768+
const bool failed = symbol_table.add(new_symbol);
769+
INVARIANT(!failed, "failed to add static field symbol");
770770
}
771771
else
772772
{

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 28 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -778,20 +778,20 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
778778
bool allow_merge)
779779
{
780780
// Check the tree shape invariant:
781-
assert(tree.branch.size()==tree.branch_addresses.size());
781+
PRECONDITION(tree.branch.size() == tree.branch_addresses.size());
782782

783783
// If there are no child blocks, return this.
784784
if(tree.leaf)
785785
return this_block;
786-
assert(!tree.branch.empty());
786+
PRECONDITION(!tree.branch.empty());
787787

788788
// Find child block starting > address_start:
789789
const auto afterstart=
790790
std::upper_bound(
791791
tree.branch_addresses.begin(),
792792
tree.branch_addresses.end(),
793793
address_start);
794-
assert(afterstart!=tree.branch_addresses.begin());
794+
CHECK_RETURN(afterstart != tree.branch_addresses.begin());
795795
auto findstart=afterstart;
796796
--findstart;
797797
auto child_offset=
@@ -819,9 +819,9 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
819819
while(child_iter != this_block.statements().end() &&
820820
child_iter->get_statement() == ID_decl)
821821
++child_iter;
822-
assert(child_iter != this_block.statements().end());
822+
CHECK_RETURN(child_iter != this_block.statements().end());
823823
std::advance(child_iter, child_offset);
824-
assert(child_iter != this_block.statements().end());
824+
CHECK_RETURN(child_iter != this_block.statements().end());
825825
auto &child_label=to_code_label(*child_iter);
826826
auto &child_block=to_code_block(child_label.code());
827827

@@ -853,7 +853,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
853853
// Check for incoming control-flow edges targeting non-header
854854
// blocks of the new proposed block range:
855855
auto checkit=amap.find(*findstart);
856-
assert(checkit!=amap.end());
856+
CHECK_RETURN(checkit != amap.end());
857857
++checkit; // Skip the header, which can have incoming edges from outside.
858858
for(;
859859
checkit!=amap.end() && (checkit->first)<(findlim_block_start_address);
@@ -885,15 +885,15 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
885885
code_labelt newlabel(child_label_name, code_blockt());
886886
code_blockt &newblock=to_code_block(newlabel.code());
887887
auto nblocks=std::distance(findstart, findlim);
888-
assert(nblocks>=2);
888+
CHECK_RETURN(nblocks >= 2);
889889
log.debug() << "Generating codet: combining "
890890
<< std::distance(findstart, findlim) << " blocks for addresses "
891891
<< (*findstart) << "-" << findlim_block_start_address
892892
<< messaget::eom;
893893

894894
// Make a new block containing every child of interest:
895895
auto &this_block_children = this_block.statements();
896-
assert(tree.branch.size()==this_block_children.size());
896+
CHECK_RETURN(tree.branch.size() == this_block_children.size());
897897
for(auto blockidx=child_offset, blocklim=child_offset+nblocks;
898898
blockidx!=blocklim;
899899
++blockidx)
@@ -923,7 +923,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
923923
++branchstart;
924924
tree.branch.erase(branchstart, branchlim);
925925

926-
assert(tree.branch.size()==this_block_children.size());
926+
CHECK_RETURN(tree.branch.size() == this_block_children.size());
927927

928928
auto branchaddriter=tree.branch_addresses.begin();
929929
std::advance(branchaddriter, child_offset);
@@ -939,7 +939,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
939939

940940
tree.branch[child_offset]=std::move(newnode);
941941

942-
assert(tree.branch.size()==tree.branch_addresses.size());
942+
CHECK_RETURN(tree.branch.size() == tree.branch_addresses.size());
943943

944944
return
945945
to_code_block(
@@ -1079,10 +1079,10 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
10791079
converted_instructiont ins=converted_instructiont(i_it, code_skipt());
10801080
std::pair<address_mapt::iterator, bool> a_entry=
10811081
address_map.insert(std::make_pair(i_it->address, ins));
1082-
assert(a_entry.second);
1082+
CHECK_RETURN(a_entry.second);
10831083
// addresses are strictly increasing, hence we must have inserted
10841084
// a new maximal key
1085-
assert(a_entry.first==--address_map.end());
1085+
CHECK_RETURN(a_entry.first == --address_map.end());
10861086

10871087
const auto bytecode = i_it->bytecode;
10881088
const std::string statement = bytecode_info[i_it->bytecode].mnemonic;
@@ -1222,9 +1222,10 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
12221222
instruction.stack.clear();
12231223
codet &c = instruction.code;
12241224

1225-
assert(
1225+
INVARIANT(
12261226
stack.empty() || instruction.predecessors.size() <= 1 ||
1227-
has_prefix(stack.front().get_string(ID_C_base_name), "$stack"));
1227+
has_prefix(stack.front().get_string(ID_C_base_name), "$stack"),
1228+
"inconsistent stack");
12281229

12291230
exprt arg0=i_it->args.size()>=1?i_it->args[0]:nil_exprt();
12301231
exprt arg1=i_it->args.size()>=2?i_it->args[1]:nil_exprt();
@@ -1293,7 +1294,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
12931294

12941295
if(bytecode == BC_aconst_null)
12951296
{
1296-
assert(results.size()==1);
1297+
PRECONDITION(results.size() == 1);
12971298
results[0] = null_pointer_exprt(java_reference_type(java_void_type()));
12981299
}
12991300
else if(bytecode == BC_athrow)
@@ -1433,18 +1434,18 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
14331434
// and write something like:
14341435
// if(retaddr==5) goto 5; else if(retaddr==10) goto 10; ...
14351436
PRECONDITION(op.empty() && results.empty());
1436-
assert(!jsr_ret_targets.empty());
1437+
PRECONDITION(!jsr_ret_targets.empty());
14371438
c = convert_ret(
14381439
jsr_ret_targets, arg0, i_it->source_location, i_it->address);
14391440
}
14401441
else if(bytecode == BC_iconst_m1)
14411442
{
1442-
assert(results.size()==1);
1443+
PRECONDITION(results.size() == 1);
14431444
results[0]=from_integer(-1, java_int_type());
14441445
}
14451446
else if(bytecode == patternt("?const_?"))
14461447
{
1447-
assert(results.size()==1);
1448+
PRECONDITION(results.size() == 1);
14481449
results = convert_const(statement, to_constant_expr(arg0), results);
14491450
}
14501451
else if(bytecode == patternt("?ipush"))
@@ -1742,7 +1743,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
17421743
numeric_cast_v<std::size_t>(to_constant_expr(arg1));
17431744

17441745
op=pop(dimension);
1745-
assert(results.size()==1);
1746+
PRECONDITION(results.size() == 1);
17461747
c = convert_multianewarray(i_it->source_location, arg0, op, results);
17471748
}
17481749
else if(bytecode == BC_arraylength)
@@ -1853,7 +1854,9 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
18531854
stackt::const_iterator os_it=a_it2->second.stack.begin();
18541855
for(auto &expr : stack)
18551856
{
1856-
assert(has_prefix(os_it->get_string(ID_C_base_name), "$stack"));
1857+
INVARIANT(
1858+
has_prefix(os_it->get_string(ID_C_base_name), "$stack"),
1859+
"invalid base name");
18571860
symbol_exprt lhs=to_symbol_expr(*os_it);
18581861
code_assignt a(lhs, expr);
18591862
more_code.add(a);
@@ -1926,7 +1929,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
19261929
for(const auto &address_pair : address_map)
19271930
{
19281931
const method_offsett address = address_pair.first;
1929-
assert(address_pair.first==address_pair.second.source->address);
1932+
CHECK_RETURN(address_pair.first == address_pair.second.source->address);
19301933
const codet &c=address_pair.second.code;
19311934

19321935
// Start a new lexical block if this is a branch target:
@@ -1955,9 +1958,10 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
19551958
root_block.add(
19561959
code_labelt{label(std::to_string(address)), code_blockt{}});
19571960
root.branch.push_back(block_tree_nodet::get_leaf());
1958-
assert((root.branch_addresses.empty() ||
1959-
root.branch_addresses.back()<address) &&
1960-
"Block addresses should be unique and increasing");
1961+
INVARIANT(
1962+
(root.branch_addresses.empty() ||
1963+
root.branch_addresses.back() < address),
1964+
"Block addresses should be unique and increasing");
19611965
root.branch_addresses.push_back(address);
19621966
}
19631967

‎jbmc/src/java_bytecode/java_bytecode_typecheck.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ std::string java_bytecode_typecheckt::to_string(const typet &type)
2525

2626
void java_bytecode_typecheckt::typecheck_non_type_symbol(symbolt &symbol)
2727
{
28-
assert(!symbol.is_type);
28+
PRECONDITION(!symbol.is_type);
2929
typecheck_type(symbol.type);
3030
typecheck_expr(symbol.value);
3131
}

‎jbmc/src/java_bytecode/java_class_loader_limit.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ void java_class_loader_limitt::setup_class_load_limit(
6262
}
6363
else
6464
{
65-
assert(java_cp_include_files.length()>1);
65+
PRECONDITION(java_cp_include_files.length() > 1);
6666
jsont json_cp_config;
6767
if(parse_json(
6868
java_cp_include_files.substr(1),
@@ -76,7 +76,7 @@ void java_class_loader_limitt::setup_class_load_limit(
7676
throw "the JSON file has a wrong format";
7777
for(const jsont &file_entry : to_json_array(include_files))
7878
{
79-
assert(file_entry.is_string());
79+
PRECONDITION(file_entry.is_string());
8080
set_matcher.insert(file_entry.value);
8181
}
8282
}

‎jbmc/src/java_bytecode/java_entry_point.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -623,7 +623,7 @@ bool java_entry_point(
623623
return true;
624624
symbolt symbol=res.main_function;
625625

626-
assert(symbol.type.id()==ID_code);
626+
DATA_INVARIANT(symbol.type.id() == ID_code, "expected code-typed symbol");
627627

628628
return generate_java_start_function(
629629
symbol,

‎jbmc/src/java_bytecode/java_local_variable_table.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -488,7 +488,7 @@ static java_bytecode_convert_methodt::method_offsett get_common_dominator(
488488
++domit;
489489
++repeats;
490490
}
491-
assert(repeats<=merge_vars.size());
491+
INVARIANT(repeats <= merge_vars.size(), "out of bounds");
492492
if(repeats==merge_vars.size())
493493
return dom;
494494
}

‎jbmc/src/java_bytecode/java_pointer_casts.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ bool find_superclass_with_type(
3434
const typet &target_type,
3535
const namespacet &ns)
3636
{
37-
assert(ptr.type().id()==ID_pointer);
37+
PRECONDITION(ptr.type().id() == ID_pointer);
3838
while(true)
3939
{
4040
const typet ptr_base=ns.follow(ptr.type().subtype());
@@ -93,15 +93,15 @@ exprt make_clean_pointer_cast(
9393
exprt bare_ptr=ptr;
9494
while(bare_ptr.id()==ID_typecast)
9595
{
96-
assert(
97-
bare_ptr.type().id()==ID_pointer &&
96+
INVARIANT(
97+
bare_ptr.type().id() == ID_pointer,
9898
"Non-pointer in make_clean_pointer_cast?");
9999
if(to_pointer_type(bare_ptr.type()).base_type() == java_void_type())
100100
bare_ptr = to_typecast_expr(bare_ptr).op();
101101
}
102102

103-
assert(
104-
bare_ptr.type().id()==ID_pointer &&
103+
INVARIANT(
104+
bare_ptr.type().id() == ID_pointer,
105105
"Non-pointer in make_clean_pointer_cast?");
106106

107107
if(bare_ptr.type()==target_type)

‎jbmc/src/java_bytecode/java_types.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -581,13 +581,13 @@ class java_class_typet:public class_typet
581581

582582
inline const java_class_typet &to_java_class_type(const typet &type)
583583
{
584-
assert(type.id()==ID_struct);
584+
PRECONDITION(type.id() == ID_struct);
585585
return static_cast<const java_class_typet &>(type);
586586
}
587587

588588
inline java_class_typet &to_java_class_type(typet &type)
589589
{
590-
assert(type.id()==ID_struct);
590+
PRECONDITION(type.id() == ID_struct);
591591
return static_cast<java_class_typet &>(type);
592592
}
593593

‎src/analyses/custom_bitvector_analysis.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -579,7 +579,7 @@ void custom_bitvector_domaint::output(
579579
for(unsigned i=0; b!=0; i++, b>>=1)
580580
if(b&1)
581581
{
582-
assert(i<cba.bits.size());
582+
INVARIANT(i < cba.bits.size(), "inconsistent bit widths");
583583
out << ' '
584584
<< cba.bits[i];
585585
}
@@ -595,7 +595,7 @@ void custom_bitvector_domaint::output(
595595
for(unsigned i=0; b!=0; i++, b>>=1)
596596
if(b&1)
597597
{
598-
assert(i<cba.bits.size());
598+
INVARIANT(i < cba.bits.size(), "inconsistent bit widths");
599599
out << ' '
600600
<< cba.bits[i];
601601
}

‎src/analyses/dependence_graph.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -220,7 +220,7 @@ void dep_graph_domaint::transform(
220220
locationt to{trace_to->current_location()};
221221

222222
dependence_grapht *dep_graph=dynamic_cast<dependence_grapht*>(&ai);
223-
assert(dep_graph!=nullptr);
223+
CHECK_RETURN(dep_graph != nullptr);
224224

225225
// We do not propagate control dependencies on function calls, i.e., only the
226226
// entry point of a function should have a control dependency on the call
@@ -366,9 +366,9 @@ void dependence_grapht::add_dep(
366366
goto_programt::const_targett to)
367367
{
368368
const node_indext n_from = (*this)[from].get_node_id();
369-
assert(n_from<size());
369+
CHECK_RETURN(n_from < size());
370370
const node_indext n_to = (*this)[to].get_node_id();
371-
assert(n_to<size());
371+
CHECK_RETURN(n_to < size());
372372

373373
// add_edge is redundant as the subsequent operations also insert
374374
// entries into the edge maps (implicitly)

0 commit comments

Comments
 (0)