diff --git a/jbmc/src/java_bytecode/character_refine_preprocess.cpp b/jbmc/src/java_bytecode/character_refine_preprocess.cpp index 6387c743fa3..956840aa505 100644 --- a/jbmc/src/java_bytecode/character_refine_preprocess.cpp +++ b/jbmc/src/java_bytecode/character_refine_preprocess.cpp @@ -29,7 +29,7 @@ codet character_refine_preprocesst::convert_char_function( conversion_inputt &target) { const code_function_callt &function_call=target; - assert(function_call.arguments().size()==1); + PRECONDITION(function_call.arguments().size() == 1); const exprt &arg=function_call.arguments()[0]; const exprt &result=function_call.lhs(); const typet &type=result.type(); @@ -113,7 +113,7 @@ codet character_refine_preprocesst::convert_char_value( codet character_refine_preprocesst::convert_compare(conversion_inputt &target) { const code_function_callt &function_call=target; - assert(function_call.arguments().size()==2); + PRECONDITION(function_call.arguments().size() == 2); const exprt &char1=function_call.arguments()[0]; const exprt &char2=function_call.arguments()[1]; const exprt &result=function_call.lhs(); @@ -225,7 +225,7 @@ codet character_refine_preprocesst::convert_digit_int(conversion_inputt &target) codet character_refine_preprocesst::convert_for_digit(conversion_inputt &target) { const code_function_callt &function_call=target; - assert(function_call.arguments().size()==2); + PRECONDITION(function_call.arguments().size() == 2); const exprt &digit=function_call.arguments()[0]; const exprt &result=function_call.lhs(); const typet &type=result.type(); @@ -588,7 +588,7 @@ codet character_refine_preprocesst::convert_is_ideographic( conversion_inputt &target) { const code_function_callt &function_call=target; - assert(function_call.arguments().size()==1); + PRECONDITION(function_call.arguments().size() == 1); const exprt &arg=function_call.arguments()[0]; const exprt &result=function_call.lhs(); exprt is_ideograph=in_interval_expr(arg, 0x4E00, 0x9FFF); @@ -602,7 +602,7 @@ codet character_refine_preprocesst::convert_is_ISO_control_char( conversion_inputt &target) { const code_function_callt &function_call=target; - assert(function_call.arguments().size()==1); + PRECONDITION(function_call.arguments().size() == 1); const exprt &arg=function_call.arguments()[0]; const exprt &result=function_call.lhs(); or_exprt iso( @@ -760,7 +760,7 @@ codet character_refine_preprocesst::convert_is_low_surrogate( conversion_inputt &target) { const code_function_callt &function_call=target; - assert(function_call.arguments().size()==1); + PRECONDITION(function_call.arguments().size() == 1); const exprt &arg=function_call.arguments()[0]; const exprt &result=function_call.lhs(); exprt is_low_surrogate=in_interval_expr(arg, 0xDC00, 0xDFFF); @@ -897,7 +897,7 @@ codet character_refine_preprocesst::convert_is_surrogate_pair( conversion_inputt &target) { const code_function_callt &function_call=target; - assert(function_call.arguments().size()==2); + PRECONDITION(function_call.arguments().size() == 2); const exprt &arg0=function_call.arguments()[0]; const exprt &arg1=function_call.arguments()[1]; const exprt &result=function_call.lhs(); diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp index 7c5414bf402..7342ccf2fda 100644 --- a/jbmc/src/java_bytecode/expr2java.cpp +++ b/jbmc/src/java_bytecode/expr2java.cpp @@ -117,7 +117,9 @@ std::string expr2javat::convert_struct( const struct_typet::componentst &components= struct_type.components(); - assert(components.size()==src.operands().size()); + DATA_INVARIANT( + components.size() == src.operands().size(), + "inconsistent number of components"); exprt::operandst::const_iterator o_it=src.operands().begin(); diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 3efd1c6e667..d14a070e506 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -763,8 +763,8 @@ void java_bytecode_convert_classt::convert( if(s_it!=symbol_table.symbols.end()) symbol_table.erase(s_it); // erase, we stubbed it - if(symbol_table.add(new_symbol)) - assert(false && "failed to add static field symbol"); + const bool failed = symbol_table.add(new_symbol); + CHECK_RETURN_WITH_DIAGNOSTICS(!failed, "failed to add static field symbol"); } else { diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index be1b0d61aa6..45325cbae67 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -773,12 +773,12 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange( bool allow_merge) { // Check the tree shape invariant: - assert(tree.branch.size()==tree.branch_addresses.size()); + PRECONDITION(tree.branch.size() == tree.branch_addresses.size()); // If there are no child blocks, return this. if(tree.leaf) return this_block; - assert(!tree.branch.empty()); + PRECONDITION(!tree.branch.empty()); // Find child block starting > address_start: const auto afterstart= @@ -786,7 +786,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange( tree.branch_addresses.begin(), tree.branch_addresses.end(), address_start); - assert(afterstart!=tree.branch_addresses.begin()); + CHECK_RETURN(afterstart != tree.branch_addresses.begin()); auto findstart=afterstart; --findstart; auto child_offset= @@ -814,9 +814,9 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange( while(child_iter != this_block.statements().end() && child_iter->get_statement() == ID_decl) ++child_iter; - assert(child_iter != this_block.statements().end()); + CHECK_RETURN(child_iter != this_block.statements().end()); std::advance(child_iter, child_offset); - assert(child_iter != this_block.statements().end()); + CHECK_RETURN(child_iter != this_block.statements().end()); auto &child_label=to_code_label(*child_iter); auto &child_block=to_code_block(child_label.code()); @@ -848,7 +848,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange( // Check for incoming control-flow edges targeting non-header // blocks of the new proposed block range: auto checkit=amap.find(*findstart); - assert(checkit!=amap.end()); + CHECK_RETURN(checkit != amap.end()); ++checkit; // Skip the header, which can have incoming edges from outside. for(; checkit!=amap.end() && (checkit->first)<(findlim_block_start_address); @@ -880,7 +880,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange( code_labelt newlabel(child_label_name, code_blockt()); code_blockt &newblock=to_code_block(newlabel.code()); auto nblocks=std::distance(findstart, findlim); - assert(nblocks>=2); + CHECK_RETURN(nblocks >= 2); log.debug() << "Generating codet: combining " << std::distance(findstart, findlim) << " blocks for addresses " << (*findstart) << "-" << findlim_block_start_address @@ -888,7 +888,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange( // Make a new block containing every child of interest: auto &this_block_children = this_block.statements(); - assert(tree.branch.size()==this_block_children.size()); + CHECK_RETURN(tree.branch.size() == this_block_children.size()); for(auto blockidx=child_offset, blocklim=child_offset+nblocks; blockidx!=blocklim; ++blockidx) @@ -918,7 +918,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange( ++branchstart; tree.branch.erase(branchstart, branchlim); - assert(tree.branch.size()==this_block_children.size()); + CHECK_RETURN(tree.branch.size() == this_block_children.size()); auto branchaddriter=tree.branch_addresses.begin(); std::advance(branchaddriter, child_offset); @@ -934,7 +934,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange( tree.branch[child_offset]=std::move(newnode); - assert(tree.branch.size()==tree.branch_addresses.size()); + CHECK_RETURN(tree.branch.size() == tree.branch_addresses.size()); return to_code_block( @@ -1074,10 +1074,10 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) converted_instructiont ins=converted_instructiont(i_it, code_skipt()); std::pair a_entry= address_map.insert(std::make_pair(i_it->address, ins)); - assert(a_entry.second); + CHECK_RETURN(a_entry.second); // addresses are strictly increasing, hence we must have inserted // a new maximal key - assert(a_entry.first==--address_map.end()); + CHECK_RETURN(a_entry.first == --address_map.end()); const auto bytecode = i_it->bytecode; const std::string statement = bytecode_info[i_it->bytecode].mnemonic; @@ -1217,9 +1217,10 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) instruction.stack.clear(); codet &c = instruction.code; - assert( + INVARIANT( stack.empty() || instruction.predecessors.size() <= 1 || - has_prefix(stack.front().get_string(ID_C_base_name), "$stack")); + has_prefix(stack.front().get_string(ID_C_base_name), "$stack"), + "inconsistent stack"); exprt arg0=i_it->args.size()>=1?i_it->args[0]:nil_exprt(); exprt arg1=i_it->args.size()>=2?i_it->args[1]:nil_exprt(); @@ -1288,7 +1289,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) if(bytecode == BC_aconst_null) { - assert(results.size()==1); + PRECONDITION(results.size() == 1); results[0] = null_pointer_exprt(java_reference_type(java_void_type())); } else if(bytecode == BC_athrow) @@ -1428,23 +1429,23 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) // and write something like: // if(retaddr==5) goto 5; else if(retaddr==10) goto 10; ... PRECONDITION(op.empty() && results.empty()); - assert(!jsr_ret_targets.empty()); + PRECONDITION(!jsr_ret_targets.empty()); c = convert_ret( jsr_ret_targets, arg0, i_it->source_location, i_it->address); } else if(bytecode == BC_iconst_m1) { - assert(results.size()==1); + CHECK_RETURN(results.size() == 1); results[0]=from_integer(-1, java_int_type()); } else if(bytecode == patternt("?const_?")) { - assert(results.size()==1); + CHECK_RETURN(results.size() == 1); results = convert_const(statement, to_constant_expr(arg0), results); } else if(bytecode == patternt("?ipush")) { - PRECONDITION(results.size()==1); + CHECK_RETURN(results.size() == 1); DATA_INVARIANT( arg0.id()==ID_constant, "ipush argument expected to be constant"); @@ -1737,7 +1738,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) numeric_cast_v(to_constant_expr(arg1)); op=pop(dimension); - assert(results.size()==1); + CHECK_RETURN(results.size() == 1); c = convert_multianewarray(i_it->source_location, arg0, op, results); } else if(bytecode == BC_arraylength) @@ -1848,7 +1849,9 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) stackt::const_iterator os_it=a_it2->second.stack.begin(); for(auto &expr : stack) { - assert(has_prefix(os_it->get_string(ID_C_base_name), "$stack")); + INVARIANT( + has_prefix(os_it->get_string(ID_C_base_name), "$stack"), + "invalid base name"); symbol_exprt lhs=to_symbol_expr(*os_it); code_assignt a(lhs, expr); more_code.add(a); @@ -1917,7 +1920,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) for(const auto &address_pair : address_map) { const method_offsett address = address_pair.first; - assert(address_pair.first==address_pair.second.source->address); + CHECK_RETURN(address_pair.first == address_pair.second.source->address); const codet &c=address_pair.second.code; // Start a new lexical block if this is a branch target: @@ -1946,9 +1949,10 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) root_block.add( code_labelt{label(std::to_string(address)), code_blockt{}}); root.branch.push_back(block_tree_nodet::get_leaf()); - assert((root.branch_addresses.empty() || - root.branch_addresses.back()1); + PRECONDITION(java_cp_include_files.length() > 1); jsont json_cp_config; if(parse_json( java_cp_include_files.substr(1), @@ -76,7 +76,7 @@ void java_class_loader_limitt::setup_class_load_limit( throw "the JSON file has a wrong format"; for(const jsont &file_entry : to_json_array(include_files)) { - assert(file_entry.is_string()); + PRECONDITION(file_entry.is_string()); set_matcher.insert(file_entry.value); } } diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 1f8bc5e3349..0477fb383d0 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -621,7 +621,7 @@ bool java_entry_point( return true; symbolt symbol=res.main_function; - assert(symbol.type.id()==ID_code); + DATA_INVARIANT(symbol.type.id() == ID_code, "expected code-typed symbol"); return generate_java_start_function( symbol, diff --git a/jbmc/src/java_bytecode/java_local_variable_table.cpp b/jbmc/src/java_bytecode/java_local_variable_table.cpp index 977a336ae22..7327d423586 100644 --- a/jbmc/src/java_bytecode/java_local_variable_table.cpp +++ b/jbmc/src/java_bytecode/java_local_variable_table.cpp @@ -488,7 +488,7 @@ static java_bytecode_convert_methodt::method_offsett get_common_dominator( ++domit; ++repeats; } - assert(repeats<=merge_vars.size()); + INVARIANT(repeats <= merge_vars.size(), "out of bounds"); if(repeats==merge_vars.size()) return dom; } diff --git a/jbmc/src/java_bytecode/java_pointer_casts.cpp b/jbmc/src/java_bytecode/java_pointer_casts.cpp index ecd913fdf0d..e5fd1d399cf 100644 --- a/jbmc/src/java_bytecode/java_pointer_casts.cpp +++ b/jbmc/src/java_bytecode/java_pointer_casts.cpp @@ -34,7 +34,7 @@ bool find_superclass_with_type( const typet &target_type, const namespacet &ns) { - assert(ptr.type().id()==ID_pointer); + PRECONDITION(ptr.type().id() == ID_pointer); while(true) { const typet ptr_base = ns.follow(to_pointer_type(ptr.type()).base_type()); @@ -93,15 +93,15 @@ exprt make_clean_pointer_cast( exprt bare_ptr=ptr; while(bare_ptr.id()==ID_typecast) { - assert( - bare_ptr.type().id()==ID_pointer && + INVARIANT( + bare_ptr.type().id() == ID_pointer, "Non-pointer in make_clean_pointer_cast?"); if(to_pointer_type(bare_ptr.type()).base_type() == java_void_type()) bare_ptr = to_typecast_expr(bare_ptr).op(); } - assert( - bare_ptr.type().id()==ID_pointer && + INVARIANT( + bare_ptr.type().id() == ID_pointer, "Non-pointer in make_clean_pointer_cast?"); if(bare_ptr.type()==target_type) diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 2db1df9f1af..5c38043c701 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -581,13 +581,13 @@ class java_class_typet:public class_typet inline const java_class_typet &to_java_class_type(const typet &type) { - assert(type.id()==ID_struct); + PRECONDITION(type.id() == ID_struct); return static_cast(type); } inline java_class_typet &to_java_class_type(typet &type) { - assert(type.id()==ID_struct); + PRECONDITION(type.id() == ID_struct); return static_cast(type); } diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index 66630c51d7b..5263efad2e8 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -579,7 +579,7 @@ void custom_bitvector_domaint::output( for(unsigned i=0; b!=0; i++, b>>=1) if(b&1) { - assert(i>=1) if(b&1) { - assert(icurrent_location()}; dependence_grapht *dep_graph=dynamic_cast(&ai); - assert(dep_graph!=nullptr); + CHECK_RETURN(dep_graph != nullptr); // We do not propagate control dependencies on function calls, i.e., only the // entry point of a function should have a control dependency on the call @@ -372,9 +372,9 @@ void dependence_grapht::add_dep( goto_programt::const_targett to) { const node_indext n_from = (*this)[from].get_node_id(); - assert(n_from::max()); + PRECONDITION(node_id != std::numeric_limits::max()); return node_id; } diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp index c4dbe21d51a..2aa7f41bb88 100644 --- a/src/analyses/flow_insensitive_analysis.cpp +++ b/src/analyses/flow_insensitive_analysis.cpp @@ -80,13 +80,13 @@ flow_insensitive_analysis_baset::locationt flow_insensitive_analysis_baset::get_next( working_sett &working_set) { - assert(!working_set.empty()); + PRECONDITION(!working_set.empty()); -// working_sett::iterator i=working_set.begin(); -// locationt l=i->second; -// working_set.erase(i); + // working_sett::iterator i=working_set.begin(); + // locationt l=i->second; + // working_set.erase(i); -// pop_heap(working_set.begin(), working_set.end()); + // pop_heap(working_set.begin(), working_set.end()); locationt l=working_set.top(); working_set.pop(); @@ -223,7 +223,8 @@ bool flow_insensitive_analysis_baset::do_function_call( return new_data; } - assert(!goto_function.body.instructions.empty()); + DATA_INVARIANT( + !goto_function.body.instructions.empty(), "body must be present"); bool new_data=false; @@ -256,7 +257,7 @@ bool flow_insensitive_analysis_baset::do_function_call( // get location at end of procedure locationt l_end=--goto_function.body.instructions.end(); - assert(l_end->is_end_function()); + DATA_INVARIANT(l_end->is_end_function(), "must be end of function"); // do edge from end of function to instruction after call locationt l_next=l_call; diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 05090caaa4a..5ed73b221b9 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -264,9 +264,9 @@ void interval_domaint::assume_rec( // we now have lhs < rhs or // lhs <= rhs - assert(id==ID_lt || id==ID_le); + DATA_INVARIANT(id == ID_lt || id == ID_le, "unexpected comparison operator"); - #ifdef DEBUG +#ifdef DEBUG std::cout << "assume_rec: " << from_expr(lhs) << " " << id << " " << from_expr(rhs) << "\n"; diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp index 44a45f5a1bc..10bc317d34a 100644 --- a/src/analyses/invariant_set.cpp +++ b/src/analyses/invariant_set.cpp @@ -77,7 +77,7 @@ unsigned inv_object_storet::add(const exprt &expr) bool inv_object_storet::is_constant(unsigned n) const { - assert(nsecond]); } @@ -334,7 +333,7 @@ void local_bitvector_analysist::build() for(const auto &succ : node.successors) { - assert(succ local_may_aliast::get( const exprt &rhs) const { local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t); - - assert(loc_it!=cfg.loc_map.end()); + CHECK_RETURN(loc_it != cfg.loc_map.end()); const loc_infot &loc_info_src=loc_infos[loc_it->second]; @@ -143,8 +142,7 @@ bool local_may_aliast::aliases( const exprt &src1, const exprt &src2) const { local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t); - - assert(loc_it!=cfg.loc_map.end()); + CHECK_RETURN(loc_it != cfg.loc_map.end()); const loc_infot &loc_info_src=loc_infos[loc_it->second]; @@ -484,7 +482,7 @@ void local_may_aliast::output( for(std::size_t j=0; jfunction_map.find(fkt); - assert(f_it2!=goto_functions->function_map.end()); + CHECK_RETURN(f_it2 != goto_functions->function_map.end()); return *(fkt_map[fkt]=util_make_unique(f_it2->second)); } @@ -127,7 +127,7 @@ class local_may_alias_factoryt { target_mapt::const_iterator t_it= target_map.find(t); - assert(t_it!=target_map.end()); + CHECK_RETURN(t_it != target_map.end()); return operator()(t_it->second); } diff --git a/src/analyses/natural_loops.h b/src/analyses/natural_loops.h index 7cbf225d269..3323be6d4e3 100644 --- a/src/analyses/natural_loops.h +++ b/src/analyses/natural_loops.h @@ -136,7 +136,7 @@ void natural_loops_templatet::compute(P &program) template void natural_loops_templatet::compute_natural_loop(T m, T n) { - assert(n->location_number<=m->location_number); + PRECONDITION(n->location_number <= m->location_number); std::stack stack; diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index eae78353388..0b2ccf42f68 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -70,7 +70,7 @@ reaching_definitions_analysist::~reaching_definitions_analysist()=default; /// `output` method. void rd_range_domaint::populate_cache(const irep_idt &identifier) const { - assert(bv_container); + PRECONDITION(bv_container); valuest::const_iterator v_entry=values.find(identifier); if(v_entry==values.end() || @@ -106,7 +106,7 @@ void rd_range_domaint::transform( bad_cast_exceptiont, "ai has type reaching_definitions_analysist"); - assert(bv_container); + PRECONDITION(bv_container); // kill values if(from->is_dead()) @@ -351,7 +351,7 @@ void rd_range_domaint::kill( return; } - assert(range_end>range_start); + PRECONDITION(range_end > range_start); valuest::iterator entry=values.find(identifier); if(entry==values.end()) @@ -432,7 +432,7 @@ void rd_range_domaint::kill( } else if(it!=entry->second.end()) { - assert(*it==id); + DATA_INVARIANT(*it == id, "entries must match"); ++it; } } @@ -622,7 +622,7 @@ bool rd_range_domaint::merge_inner( } else if(itr!=dest.end()) { - assert(*itr==id); + DATA_INVARIANT(*itr == id, "entries must match"); ++itr; } } @@ -651,7 +651,7 @@ bool rd_range_domaint::merge( } else if(it!=values.end()) { - assert(it->first==value.first); + DATA_INVARIANT(it->first == value.first, "entries must match"); if(merge_inner(it->second, value.second)) { @@ -701,7 +701,7 @@ bool rd_range_domaint::merge_shared( } else if(it!=values.end()) { - assert(it->first==value.first); + DATA_INVARIANT(it->first == value.first, "entries must match"); if(merge_inner(it->second, value.second)) { diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h index 0987362ef2b..f3fd7a46a75 100644 --- a/src/analyses/reaching_definitions.h +++ b/src/analyses/reaching_definitions.h @@ -44,7 +44,7 @@ class sparse_bitvector_analysist public: const V &get(const std::size_t value_index) const { - assert(value_indexfirst; } @@ -143,7 +143,8 @@ inline bool operator<( // we do not expect comparison of unrelated definitions // as this operator< is only used in sparse_bitvector_analysist - assert(a.identifier==b.identifier); + INVARIANT( + a.identifier == b.identifier, "comparison of unrelated definitions"); return false; } @@ -365,19 +366,19 @@ class reaching_definitions_analysist: value_setst &get_value_sets() const { - assert(value_sets); + PRECONDITION(value_sets); return *value_sets; } const is_threadedt &get_is_threaded() const { - assert(is_threaded); + PRECONDITION(is_threaded); return *is_threaded; } const dirtyt &get_is_dirty() const { - assert(is_dirty); + PRECONDITION(is_dirty); return *is_dirty; } diff --git a/src/analyses/static_analysis.cpp b/src/analyses/static_analysis.cpp index 727cf0ca28a..566f2816782 100644 --- a/src/analyses/static_analysis.cpp +++ b/src/analyses/static_analysis.cpp @@ -40,8 +40,7 @@ exprt static_analysis_baset::get_return_lhs(locationt to) if(to->is_end_function()) return static_cast(get_nil_irep()); - // must be the function call - assert(to->is_function_call()); + DATA_INVARIANT(to->is_function_call(), "must be the function call"); return to->call_lhs(); } @@ -145,7 +144,7 @@ void static_analysis_baset::update( static_analysis_baset::locationt static_analysis_baset::get_next( working_sett &working_set) { - assert(!working_set.empty()); + PRECONDITION(!working_set.empty()); working_sett::iterator i=working_set.begin(); locationt l=i->second; @@ -249,7 +248,7 @@ void static_analysis_baset::do_function_call( if(!goto_function.body_available()) return; // do nothing - assert(!goto_function.body.instructions.empty()); + CHECK_RETURN(!goto_function.body.instructions.empty()); { // get the state at the beginning of the function @@ -287,7 +286,7 @@ void static_analysis_baset::do_function_call( // get location at end of procedure locationt l_end=--goto_function.body.instructions.end(); - assert(l_end->is_end_function()); + DATA_INVARIANT(l_end->is_end_function(), "must be end of function"); statet &end_of_function=get_state(l_end); diff --git a/src/ansi-c/ansi_c_declaration.h b/src/ansi-c/ansi_c_declaration.h index d3d1f87bc29..c3f2fe57829 100644 --- a/src/ansi-c/ansi_c_declaration.h +++ b/src/ansi-c/ansi_c_declaration.h @@ -58,13 +58,13 @@ class ansi_c_declaratort : public nullary_exprt inline ansi_c_declaratort &to_ansi_c_declarator(exprt &expr) { - assert(expr.id()==ID_declarator); + PRECONDITION(expr.id() == ID_declarator); return static_cast(expr); } inline const ansi_c_declaratort &to_ansi_c_declarator(const exprt &expr) { - assert(expr.id()==ID_declarator); + PRECONDITION(expr.id() == ID_declarator); return static_cast(expr); } @@ -226,13 +226,13 @@ class ansi_c_declarationt:public exprt // special case of a declaration with exactly one declarator const ansi_c_declaratort &declarator() const { - assert(declarators().size()==1); + PRECONDITION(declarators().size() == 1); return declarators()[0]; } ansi_c_declaratort &declarator() { - assert(declarators().size()==1); + PRECONDITION(declarators().size() == 1); return declarators()[0]; } @@ -240,20 +240,20 @@ class ansi_c_declarationt:public exprt void add_initializer(exprt &value) { - assert(!declarators().empty()); + PRECONDITION(!declarators().empty()); declarators().back().value().swap(value); } }; inline ansi_c_declarationt &to_ansi_c_declaration(exprt &expr) { - assert(expr.id()==ID_declaration); + PRECONDITION(expr.id() == ID_declaration); return static_cast(expr); } inline const ansi_c_declarationt &to_ansi_c_declaration(const exprt &expr) { - assert(expr.id()==ID_declaration); + PRECONDITION(expr.id() == ID_declaration); return static_cast(expr); } diff --git a/src/ansi-c/ansi_c_parser.cpp b/src/ansi-c/ansi_c_parser.cpp index 5e90ccbf56a..9aa79de4ab4 100644 --- a/src/ansi-c/ansi_c_parser.cpp +++ b/src/ansi-c/ansi_c_parser.cpp @@ -85,7 +85,7 @@ void ansi_c_parsert::add_declarator( exprt &declaration, irept &declarator) { - assert(declarator.is_not_nil()); + PRECONDITION(declarator.is_not_nil()); ansi_c_declarationt &ansi_c_declaration= to_ansi_c_declaration(declaration); diff --git a/src/ansi-c/ansi_c_parser.h b/src/ansi-c/ansi_c_parser.h index 3573380530e..4dde7752afe 100644 --- a/src/ansi-c/ansi_c_parser.h +++ b/src/ansi-c/ansi_c_parser.h @@ -102,7 +102,7 @@ class ansi_c_parsert:public parsert scopet ¤t_scope() { - assert(!scopes.empty()); + PRECONDITION(!scopes.empty()); return scopes.back(); } @@ -116,7 +116,7 @@ class ansi_c_parsert:public parsert void copy_item(const ansi_c_declarationt &declaration) { - assert(declaration.id()==ID_declaration); + PRECONDITION(declaration.id() == ID_declaration); parse_tree.items.push_back(declaration); } diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp index b76ad2ad6af..d4f64ce585f 100644 --- a/src/ansi-c/c_typecast.cpp +++ b/src/ansi-c/c_typecast.cpp @@ -698,13 +698,13 @@ void c_typecastt::implicit_typecast_arithmetic( } else if(c_type1==COMPLEX) { - assert(c_type1==COMPLEX && c_type2!=COMPLEX); + INVARIANT(c_type2 != COMPLEX, "both types were COMPLEX"); do_typecast(expr2, to_complex_type(type1).subtype()); do_typecast(expr2, type1); } else { - assert(c_type1!=COMPLEX && c_type2==COMPLEX); + INVARIANT(c_type2 == COMPLEX, "neither type was COMPLEX"); do_typecast(expr1, to_complex_type(type2).subtype()); do_typecast(expr1, type2); } diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 9c4d97c52d6..fa821e88739 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -671,7 +671,9 @@ void c_typecheck_baset::apply_asm_label( if(!asm_label_map.insert( std::make_pair(p_id, p_new_id)).second) - assert(asm_label_map[p_id]==p_new_id); + { + CHECK_RETURN(asm_label_map[p_id] == p_new_id); + } } } } diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index df68d74adcc..b5354e043c0 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -87,13 +87,13 @@ void c_typecheck_baset::typecheck_code(codet &code) typecheck_gcc_local_label(code); else if(statement==ID_msc_try_finally) { - assert(code.operands().size()==2); + PRECONDITION(code.operands().size() == 2); typecheck_code(to_code(code.op0())); typecheck_code(to_code(code.op1())); } else if(statement==ID_msc_try_except) { - assert(code.operands().size()==3); + PRECONDITION(code.operands().size() == 3); typecheck_code(to_code(code.op0())); typecheck_expr(code.op1()); typecheck_code(to_code(code.op2())); @@ -127,13 +127,13 @@ void c_typecheck_baset::typecheck_code(codet &code) else if(statement==ID_CPROVER_try_catch || statement==ID_CPROVER_try_finally) { - assert(code.operands().size()==2); + PRECONDITION(code.operands().size() == 2); typecheck_code(to_code(code.op0())); typecheck_code(to_code(code.op1())); } else if(statement==ID_CPROVER_throw) { - assert(code.operands().empty()); + PRECONDITION(code.operands().empty()); } else if(statement==ID_assume || statement==ID_assert) @@ -141,7 +141,7 @@ void c_typecheck_baset::typecheck_code(codet &code) // These are not generated by the C/C++ parsers, // but we allow them for the benefit of other users // of the typechecker. - assert(code.operands().size()==1); + PRECONDITION(code.operands().size() == 1); typecheck_expr(code.op0()); } else @@ -181,7 +181,7 @@ void c_typecheck_baset::typecheck_asm(code_asmt &code) } else if(flavor==ID_msc) { - assert(code.operands().size()==1); + PRECONDITION(code.operands().size() == 1); typecheck_expr(code.op0()); } } diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 9a8609d1a48..89a293f5cbc 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -245,7 +245,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr) expr.type()=bool_typet(); auto &subtypes = (static_cast(expr.add(ID_type_arg))).subtypes(); - assert(subtypes.size()==2); + PRECONDITION(subtypes.size() == 2); typecheck_type(subtypes[0]); typecheck_type(subtypes[1]); source_locationt source_location=expr.source_location(); @@ -607,7 +607,7 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr) while(!found) { - assert(type.id()==ID_union || type.id()==ID_struct); + PRECONDITION(type.id() == ID_union || type.id() == ID_struct); const struct_union_typet &struct_union_type= to_struct_union_type(type); @@ -671,7 +671,7 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr) typet tmp = follow(c.type()); type=tmp; - assert(type.id()==ID_union || type.id()==ID_struct); + CHECK_RETURN(type.id() == ID_union || type.id() == ID_struct); found2=true; break; // we run into another iteration of the outer loop } @@ -922,7 +922,7 @@ void c_typecheck_baset::typecheck_side_effect_statement_expression( if(last_statement==ID_expression) { - assert(last.operands().size()==1); + PRECONDITION(last.operands().size() == 1); exprt &op=last.op0(); // arrays here turn into pointers (array decay) @@ -1571,7 +1571,7 @@ void c_typecheck_baset::typecheck_expr_trinary(if_exprt &expr) { exprt::operandst &operands=expr.operands(); - assert(operands.size()==3); + PRECONDITION(operands.size() == 3); // copy (save) original types const typet o_type0=operands[0].type(); @@ -1788,7 +1788,7 @@ void c_typecheck_baset::typecheck_expr_dereference(exprt &expr) expr.id(ID_index); expr.type() = to_array_type(op_type).element_type(); expr.copy_to_operands(from_integer(0, c_index_type())); - assert(expr.operands().size()==2); + CHECK_RETURN(expr.operands().size() == 2); } else if(op_type.id()==ID_pointer) { @@ -4029,7 +4029,7 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr) void c_typecheck_baset::typecheck_expr_shifts(shift_exprt &expr) { - assert(expr.id()==ID_shl || expr.id()==ID_shr); + PRECONDITION(expr.id() == ID_shl || expr.id() == ID_shr); exprt &op0=expr.op0(); exprt &op1=expr.op1(); diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index 732fd11ca73..9bb8da634f4 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -359,18 +359,18 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer( // copy the value, we may need to adjust it exprt value=*init_it; - assert(!designator.empty()); + PRECONDITION(!designator.empty()); if(value.id()==ID_designated_initializer) { - assert(value.operands().size()==1); + PRECONDITION(value.operands().size() == 1); designator= make_designator( designator.front().type, static_cast(value.find(ID_designator))); - assert(!designator.empty()); + CHECK_RETURN(!designator.empty()); // discard the return value do_designated_initializer( @@ -593,7 +593,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer( else *dest=do_initializer_rec(value, type, force_constant); - assert(full_type==follow(dest->type())); + DATA_INVARIANT(full_type == follow(dest->type()), "matching types"); return ++init_it; // done } @@ -661,10 +661,10 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer( } } - assert(full_type.id()==ID_struct || - full_type.id()==ID_union || - full_type.id()==ID_array || - full_type.id()==ID_vector); + DATA_INVARIANT( + full_type.id() == ID_struct || full_type.id() == ID_union || + full_type.id() == ID_array || full_type.id() == ID_vector, + "full type must be composite"); // we are initializing a compound type, and enter it! // this may change the type, full_type might not be valid any more @@ -715,7 +715,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer( void c_typecheck_baset::increment_designator(designatort &designator) { - assert(!designator.empty()); + PRECONDITION(!designator.empty()); while(true) { @@ -736,7 +736,8 @@ void c_typecheck_baset::increment_designator(designatort &designator) to_struct_type(full_type); const struct_typet::componentst &components= struct_type.components(); - assert(components.size()==entry.size); + DATA_INVARIANT( + components.size() == entry.size, "matching component numbers"); // we skip over any padding or code // we also skip over anonymous members @@ -762,7 +763,7 @@ void c_typecheck_baset::increment_designator(designatort &designator) // pop entry designator.pop_entry(); - assert(!designator.empty()); + INVARIANT(!designator.empty(), "designator had more than one entry"); } } @@ -770,7 +771,7 @@ designatort c_typecheck_baset::make_designator( const typet &src_type, const exprt &src) { - assert(!src.operands().empty()); + PRECONDITION(!src.operands().empty()); typet type=src_type; designatort designator; @@ -909,7 +910,7 @@ designatort c_typecheck_baset::make_designator( designator.push_entry(entry); } - assert(!designator.empty()); + INVARIANT(!designator.empty(), "expected an entry to be added"); return designator; } @@ -919,7 +920,7 @@ exprt c_typecheck_baset::do_initializer_list( const typet &type, bool force_constant) { - assert(value.id()==ID_initializer_list); + PRECONDITION(value.id() == ID_initializer_list); const typet &full_type=follow(type); diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index a035ba34117..ba9bc1348b0 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -134,8 +134,10 @@ void c_typecheck_baset::typecheck_type(typet &type) underlying_type = follow_tag(to_c_enum_tag_type(underlying_type)).underlying_type(); - assert(underlying_type.id()==ID_signedbv || - underlying_type.id()==ID_unsignedbv); + DATA_INVARIANT( + underlying_type.id() == ID_signedbv || + underlying_type.id() == ID_unsignedbv, + "underlying type must be bitvector"); } if(underlying_type.id()==ID_signedbv || @@ -198,7 +200,7 @@ void c_typecheck_baset::typecheck_type(typet &type) } else { - assert(config.ansi_c.long_long_int_width==64); + PRECONDITION(config.ansi_c.long_long_int_width == 64); if(is_signed) result=signed_long_long_int_type(); @@ -780,7 +782,7 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type) if(type.find(ID_tag).is_nil()) { // Anonymous? Must come with body. - assert(have_body); + PRECONDITION(have_body); // produce symbol type_symbolt compound_symbol{irep_idt{}, type, mode}; @@ -904,7 +906,7 @@ void c_typecheck_baset::typecheck_compound_body( for(auto &decl : old_components) { // the arguments are member declarations or static assertions - assert(decl.id()==ID_declaration); + PRECONDITION(decl.id() == ID_declaration); ansi_c_declarationt &declaration= to_ansi_c_declaration(static_cast(decl)); @@ -914,8 +916,8 @@ void c_typecheck_baset::typecheck_compound_body( struct_union_typet::componentt new_component; new_component.id(ID_static_assert); new_component.add_source_location()=declaration.source_location(); + PRECONDITION(declaration.operands().size() == 2); new_component.operands().swap(declaration.operands()); - assert(new_component.operands().size()==2); components.push_back(new_component); } else diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 6ab5817b1ea..58f3ef179f0 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -668,7 +668,8 @@ std::string expr2ct::convert_struct_type( // Either we are including the body (in which case it makes sense to include // or exclude the parameters) or there is no body so therefore we definitely // shouldn't be including the parameters - assert(inc_struct_body || !inc_padding_components); + INVARIANT( + inc_struct_body || !inc_padding_components, "inconsistent configuration"); const struct_typet &struct_type=to_struct_type(src); @@ -896,8 +897,7 @@ std::string expr2ct::convert_with( const struct_union_typet::componentt &comp_expr= struct_union_type.get_component(component_name); - - assert(comp_expr.is_not_nil()); + CHECK_RETURN(comp_expr.is_not_nil()); irep_idt display_component_name; @@ -1642,7 +1642,7 @@ std::string expr2ct::convert_symbol(const exprt &src) get_shorthands(src); entry=shorthands.find(id); - assert(entry!=shorthands.end()); + CHECK_RETURN(entry != shorthands.end()); } dest=id2string(entry->second); diff --git a/src/ansi-c/literals/convert_character_literal.cpp b/src/ansi-c/literals/convert_character_literal.cpp index 9a9bfcb0685..1c56ad18ecd 100644 --- a/src/ansi-c/literals/convert_character_literal.cpp +++ b/src/ansi-c/literals/convert_character_literal.cpp @@ -23,14 +23,14 @@ exprt convert_character_literal( bool force_integer_type, const source_locationt &source_location) { - assert(src.size()>=2); + PRECONDITION(src.size() >= 2); exprt result; if(src[0]=='L' || src[0]=='u' || src[0]=='U') { - assert(src[1]=='\''); - assert(src[src.size()-1]=='\''); + PRECONDITION(src[1] == '\''); + PRECONDITION(src[src.size() - 1] == '\''); std::basic_string value= unescape_wide_string(std::string(src, 2, src.size()-3)); @@ -68,8 +68,8 @@ exprt convert_character_literal( } else { - assert(src[0]=='\''); - assert(src[src.size()-1]=='\''); + PRECONDITION(src[0] == '\''); + PRECONDITION(src[src.size() - 1] == '\''); std::string value= unescape_string(std::string(src, 1, src.size()-2)); diff --git a/src/ansi-c/literals/convert_string_literal.cpp b/src/ansi-c/literals/convert_string_literal.cpp index 57d94150cd7..874ed680f29 100644 --- a/src/ansi-c/literals/convert_string_literal.cpp +++ b/src/ansi-c/literals/convert_string_literal.cpp @@ -21,12 +21,12 @@ Author: Daniel Kroening, kroening@kroening.com std::basic_string convert_one_string_literal( const std::string &src) { - assert(src.size()>=2); + PRECONDITION(src.size() >= 2); if(src[0]=='u' && src[1]=='8') { - assert(src[src.size()-1]=='"'); - assert(src[2]=='"'); + PRECONDITION(src[src.size() - 1] == '"'); + PRECONDITION(src[2] == '"'); std::basic_string value= unescape_wide_string(std::string(src, 3, src.size()-4)); @@ -43,15 +43,15 @@ std::basic_string convert_one_string_literal( } else if(src[0]=='L' || src[0]=='u' || src[0]=='U') { - assert(src[src.size()-1]=='"'); - assert(src[1]=='"'); + PRECONDITION(src[src.size() - 1] == '"'); + PRECONDITION(src[1] == '"'); return unescape_wide_string(std::string(src, 2, src.size()-3)); } else { - assert(src[0]=='"'); - assert(src[src.size()-1]=='"'); + PRECONDITION(src[0] == '"'); + PRECONDITION(src[src.size() - 1] == '"'); std::string char_value= unescape_string(std::string(src, 1, src.size()-2)); @@ -120,7 +120,8 @@ exprt convert_string_literal(const std::string &src) case 'L': subtype=wchar_t_type(); break; case 'u': subtype=char16_t_type(); break; case 'U': subtype=char32_t_type(); break; - default: assert(false); + default: + UNREACHABLE; } exprt result=exprt(ID_array); diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index abb8b2246bb..0580819cdbd 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -2919,7 +2919,9 @@ function_definition: ansi_c_declarationt &ansi_c_declaration= to_ansi_c_declaration(parser_stack($$)); - assert(ansi_c_declaration.declarators().size()==1); + INVARIANT( + ansi_c_declaration.declarators().size()==1, + "exactly one declarator"); ansi_c_declaration.add_initializer(parser_stack($2)); // Kill the scope that 'function_head' creates. diff --git a/src/ansi-c/parser_static.inc b/src/ansi-c/parser_static.inc index 1716fa5fd43..b38947b7e92 100644 --- a/src/ansi-c/parser_static.inc +++ b/src/ansi-c/parser_static.inc @@ -185,7 +185,7 @@ static void make_subtype(typet &dest, typet &src) std::cout << "S: " << src.pretty() << '\n'; #endif - assert(src.id()==ID_array || + PRECONDITION(src.id()==ID_array || src.id()==ID_frontend_pointer || src.id()==ID_code || src.id()==ID_merged_type || @@ -221,9 +221,9 @@ static void make_subtype(typet &dest, typet &src) break; } else if(p->is_nil()) - assert(false); + UNREACHABLE; else if(p->id().empty()) - assert(false); + UNREACHABLE; else { // *p is now type or symbol @@ -246,9 +246,9 @@ static void make_subtype(typet &dest, typet &src) p=&merged_type.last_type(); } else if(p->id().empty()) - assert(false); + UNREACHABLE; else if(p->is_nil()) - assert(false); + UNREACHABLE; else p=&p->add_subtype(); } @@ -403,7 +403,7 @@ static void adjust_KnR_parameters( Forall_operands(d_it, declarations) { - assert(d_it->id()==ID_declaration); + DATA_INVARIANT(d_it->id()==ID_declaration, "expected declaration"); ansi_c_declarationt &declaration= to_ansi_c_declaration(static_cast(*d_it)); diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp index 50bfc48b173..87fdfc9624a 100644 --- a/src/ansi-c/type2name.cpp +++ b/src/ansi-c/type2name.cpp @@ -40,7 +40,8 @@ static std::string type2name_tag( if(ns.lookup(identifier, symbol)) return "SYM#"+id2string(identifier)+"#"; - assert(symbol && symbol->is_type); + DATA_INVARIANT(symbol, "symbol not found"); + DATA_INVARIANT(symbol->is_type, "not a type symbol"); if(symbol->type.id()!=ID_struct && symbol->type.id()!=ID_union) diff --git a/src/cpp/cpp_constructor.cpp b/src/cpp/cpp_constructor.cpp index 3ff729cba1d..09e022073cd 100644 --- a/src/cpp/cpp_constructor.cpp +++ b/src/cpp/cpp_constructor.cpp @@ -31,8 +31,7 @@ optionalt cpp_typecheckt::cpp_constructor( elaborate_class_template(object_tc.type()); typet tmp_type(follow(object_tc.type())); - - assert(!is_reference(tmp_type)); + CHECK_RETURN(!is_reference(tmp_type)); if(tmp_type.id()==ID_array) { @@ -50,7 +49,9 @@ optionalt cpp_typecheckt::cpp_constructor( throw 0; } - assert(operands.empty() || operands.size()==1); + DATA_INVARIANT( + operands.empty() || operands.size() == 1, + "array constructor must have at most one operand"); if(operands.empty() && cpp_is_pod(tmp_type)) return {}; @@ -224,13 +225,15 @@ optionalt cpp_typecheckt::cpp_constructor( source_location); typecheck_side_effect_function_call(function_call); - assert(function_call.get(ID_statement)==ID_temporary_object); + CHECK_RETURN(function_call.get(ID_statement) == ID_temporary_object); exprt &initializer = static_cast(function_call.add(ID_initializer)); - assert(initializer.id()==ID_code && - initializer.get(ID_statement)==ID_expression); + DATA_INVARIANT( + initializer.id() == ID_code && + initializer.get(ID_statement) == ID_expression, + "initializer must be expression statement"); auto &statement_expr = to_code_expression(to_code(initializer)); diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp index 1f0454e9d08..d55fd811898 100644 --- a/src/cpp/cpp_convert_type.cpp +++ b/src/cpp/cpp_convert_type.cpp @@ -179,8 +179,9 @@ void cpp_convert_typet::read_function_type(const typet &type) cpp_convert_plain_type(declaration.type(), message_handler); - // there should be only one declarator - assert(declaration.declarators().size()==1); + DATA_INVARIANT( + declaration.declarators().size() == 1, + "there should be only one declarator"); cpp_declaratort &declarator= declaration.declarators().front(); @@ -212,7 +213,7 @@ void cpp_convert_typet::read_function_type(const typet &type) else if(cpp_name.is_simple_name()) { irep_idt base_name=cpp_name.get_base_name(); - assert(!base_name.empty()); + CHECK_RETURN(!base_name.empty()); new_parameter.set_identifier(base_name); new_parameter.set_base_name(base_name); new_parameter.add_source_location()=cpp_name.source_location(); diff --git a/src/cpp/cpp_declaration.h b/src/cpp/cpp_declaration.h index 84d65da88f5..db8088f7222 100644 --- a/src/cpp/cpp_declaration.h +++ b/src/cpp/cpp_declaration.h @@ -145,13 +145,13 @@ class cpp_declarationt:public exprt inline cpp_declarationt &to_cpp_declaration(irept &irep) { - assert(irep.id()==ID_cpp_declaration); + PRECONDITION(irep.id() == ID_cpp_declaration); return static_cast(irep); } inline const cpp_declarationt &to_cpp_declaration(const irept &irep) { - assert(irep.id()==ID_cpp_declaration); + PRECONDITION(irep.id() == ID_cpp_declaration); return static_cast(irep); } diff --git a/src/cpp/cpp_declarator.cpp b/src/cpp/cpp_declarator.cpp index 8d070f3c88f..22d867dafc7 100644 --- a/src/cpp/cpp_declarator.cpp +++ b/src/cpp/cpp_declarator.cpp @@ -50,7 +50,7 @@ typet cpp_declaratort::merge_type(const typet &declaration_type) const } else { - assert(!t.id().empty()); + DATA_INVARIANT(!t.id().empty(), "empty type"); p = &t.add_subtype(); } } diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp index d65fdebf948..7ac12490d40 100644 --- a/src/cpp/cpp_declarator_converter.cpp +++ b/src/cpp/cpp_declarator_converter.cpp @@ -39,7 +39,7 @@ symbolt &cpp_declarator_convertert::convert( const cpp_member_spect &member_spec, cpp_declaratort &declarator) { - assert(declaration_type.is_not_nil()); + PRECONDITION(declaration_type.is_not_nil()); if(declaration_type.id()=="cpp-cast-operator") { @@ -51,9 +51,9 @@ symbolt &cpp_declarator_convertert::convert( declarator.name().get_sub().back().swap(name); } - assert(declarator.id()==ID_cpp_declarator); + PRECONDITION(declarator.id() == ID_cpp_declarator); final_type=declarator.merge_type(declaration_type); - assert(final_type.is_not_nil()); + CHECK_RETURN(final_type.is_not_nil()); cpp_storage_spect final_storage_spec = storage_spec; final_storage_spec |= cpp_storage_spect(final_type); diff --git a/src/cpp/cpp_destructor.cpp b/src/cpp/cpp_destructor.cpp index 2282b5d4186..d7f895f8bd1 100644 --- a/src/cpp/cpp_destructor.cpp +++ b/src/cpp/cpp_destructor.cpp @@ -23,8 +23,7 @@ optionalt cpp_typecheckt::cpp_destructor( elaborate_class_template(object.type()); typet tmp_type(follow(object.type())); - - assert(!is_reference(tmp_type)); + CHECK_RETURN(!is_reference(tmp_type)); // PODs don't need a destructor if(cpp_is_pod(tmp_type)) diff --git a/src/cpp/cpp_enum_type.h b/src/cpp/cpp_enum_type.h index 91976fe4c6c..2f1a40b09d4 100644 --- a/src/cpp/cpp_enum_type.h +++ b/src/cpp/cpp_enum_type.h @@ -61,13 +61,13 @@ class cpp_enum_typet:public typet inline const cpp_enum_typet &to_cpp_enum_type(const irept &irep) { - assert(irep.id()==ID_c_enum); + PRECONDITION(irep.id() == ID_c_enum); return static_cast(irep); } inline cpp_enum_typet &to_cpp_enum_type(irept &irep) { - assert(irep.id()==ID_c_enum); + PRECONDITION(irep.id() == ID_c_enum); return static_cast(irep); } diff --git a/src/cpp/cpp_id.h b/src/cpp/cpp_id.h index 30e8cf6c192..fab3593d052 100644 --- a/src/cpp/cpp_id.h +++ b/src/cpp/cpp_id.h @@ -87,7 +87,7 @@ class cpp_idt void set_parent(cpp_idt &_parent) { - assert(_parent.is_scope); + PRECONDITION(_parent.is_scope); parent=&_parent; } diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp index 837e9b8c8dc..4328428b326 100644 --- a/src/cpp/cpp_instantiate_template.cpp +++ b/src/cpp/cpp_instantiate_template.cpp @@ -150,8 +150,7 @@ const symbolt &cpp_typecheckt::class_template_symbol( const cpp_template_args_tct &specialization_template_args, const cpp_template_args_tct &full_template_args) { - // we should never get 'unassigned' here - assert(!full_template_args.has_unassigned()); + PRECONDITION(!full_template_args.has_unassigned()); // do we have args? if(full_template_args.arguments().empty()) @@ -278,8 +277,11 @@ const symbolt &cpp_typecheckt::instantiate_template( bool specialization_given=specialization.is_not_nil(); // we should never get 'unassigned' here - assert(!specialization_template_args.has_unassigned()); - assert(!full_template_args.has_unassigned()); + DATA_INVARIANT( + !specialization_template_args.has_unassigned(), + "should never get 'unassigned' here"); + DATA_INVARIANT( + !full_template_args.has_unassigned(), "should never get 'unassigned' here"); #ifdef DEBUG std::cout << "A: <"; @@ -363,8 +365,10 @@ const symbolt &cpp_typecheckt::instantiate_template( // It has already been instantiated! const cpp_idt &cpp_id = **id_set.begin(); - assert(cpp_id.id_class == cpp_idt::id_classt::CLASS || - cpp_id.id_class == cpp_idt::id_classt::SYMBOL); + DATA_INVARIANT( + cpp_id.id_class == cpp_idt::id_classt::CLASS || + cpp_id.id_class == cpp_idt::id_classt::SYMBOL, + "id must be class or symbol"); const symbolt &symb=lookup(cpp_id.identifier); @@ -477,7 +481,7 @@ const symbolt &cpp_typecheckt::instantiate_template( { symbolt &symb = symbol_table.get_writeable_ref(class_name); - assert(new_decl.declarators().size() == 1); + PRECONDITION(new_decl.declarators().size() == 1); if(new_decl.member_spec().is_virtual()) { @@ -508,8 +512,8 @@ const symbolt &cpp_typecheckt::instantiate_template( bool is_static=new_decl.storage_spec().is_static(); irep_idt access = new_decl.get(ID_C_access); - assert(!access.empty()); - assert(symb.type.id()==ID_struct); + CHECK_RETURN(!access.empty()); + PRECONDITION(symb.type.id() == ID_struct); typecheck_compound_declarator( symb, @@ -527,7 +531,7 @@ const symbolt &cpp_typecheckt::instantiate_template( // not a class template, not a class template method, // it must be a function template! - assert(new_decl.declarators().size()==1); + PRECONDITION(new_decl.declarators().size() == 1); convert_non_template_declaration(new_decl); diff --git a/src/cpp/cpp_item.h b/src/cpp/cpp_item.h index 6940b8ce911..d8488d17705 100644 --- a/src/cpp/cpp_item.h +++ b/src/cpp/cpp_item.h @@ -31,13 +31,13 @@ class cpp_itemt:public irept cpp_declarationt &get_declaration() { - assert(is_declaration()); + PRECONDITION(is_declaration()); return (cpp_declarationt &)*this; } const cpp_declarationt &get_declaration() const { - assert(is_declaration()); + PRECONDITION(is_declaration()); return (const cpp_declarationt &)*this; } @@ -56,13 +56,13 @@ class cpp_itemt:public irept cpp_linkage_spect &get_linkage_spec() { - assert(is_linkage_spec()); + PRECONDITION(is_linkage_spec()); return (cpp_linkage_spect &)*this; } const cpp_linkage_spect &get_linkage_spec() const { - assert(is_linkage_spec()); + PRECONDITION(is_linkage_spec()); return (const cpp_linkage_spect &)*this; } @@ -81,13 +81,13 @@ class cpp_itemt:public irept cpp_namespace_spect &get_namespace_spec() { - assert(is_namespace_spec()); + PRECONDITION(is_namespace_spec()); return (cpp_namespace_spect &)*this; } const cpp_namespace_spect &get_namespace_spec() const { - assert(is_namespace_spec()); + PRECONDITION(is_namespace_spec()); return (const cpp_namespace_spect &)*this; } @@ -106,13 +106,13 @@ class cpp_itemt:public irept cpp_usingt &get_using() { - assert(is_using()); + PRECONDITION(is_using()); return (cpp_usingt &)*this; } const cpp_usingt &get_using() const { - assert(is_using()); + PRECONDITION(is_using()); return (const cpp_usingt &)*this; } @@ -131,7 +131,7 @@ class cpp_itemt:public irept cpp_static_assertt &get_static_assert() { - assert(is_static_assert()); + PRECONDITION(is_static_assert()); return (cpp_static_assertt &)*this; } diff --git a/src/cpp/cpp_scope.h b/src/cpp/cpp_scope.h index 0e94aa6de60..228734f1c36 100644 --- a/src/cpp/cpp_scope.h +++ b/src/cpp/cpp_scope.h @@ -102,13 +102,13 @@ class cpp_scopet:public cpp_idt void add_secondary_scope(cpp_scopet &other) { - assert(other.is_scope); + PRECONDITION(other.is_scope); secondary_scopes.push_back(&other); } void add_using_scope(cpp_scopet &other) { - assert(other.is_scope); + PRECONDITION(other.is_scope); using_scopes.push_back(&other); } diff --git a/src/cpp/cpp_scopes.cpp b/src/cpp/cpp_scopes.cpp index f03e834bfab..03efd8b970c 100644 --- a/src/cpp/cpp_scopes.cpp +++ b/src/cpp/cpp_scopes.cpp @@ -26,8 +26,8 @@ cpp_idt &cpp_scopest::put_into_scope( cpp_scopet &scope, bool is_friend) { - assert(!symbol.name.empty()); - assert(!symbol.base_name.empty()); + PRECONDITION(!symbol.name.empty()); + PRECONDITION(!symbol.base_name.empty()); // functions are also scopes if(symbol.type.id()==ID_code) diff --git a/src/cpp/cpp_scopes.h b/src/cpp/cpp_scopes.h index 4a4bfde9e2e..dd3830003f3 100644 --- a/src/cpp/cpp_scopes.h +++ b/src/cpp/cpp_scopes.h @@ -38,7 +38,7 @@ class cpp_scopest const irep_idt &new_scope_name, cpp_idt::id_classt id_class) { - assert(!new_scope_name.empty()); + PRECONDITION(!new_scope_name.empty()); cpp_scopet &n=current_scope_ptr->new_scope(new_scope_name); n.id_class=id_class; id_map[n.identifier]=&n; @@ -80,7 +80,7 @@ class cpp_scopest cpp_scopet &get_scope(const irep_idt &identifier) { cpp_idt &n=get_id(identifier); - assert(n.is_scope); + CHECK_RETURN(n.is_scope); return (cpp_scopet &)n; } @@ -102,7 +102,7 @@ class cpp_scopest void go_to(cpp_idt &id) { - assert(id.is_scope); + PRECONDITION(id.is_scope); current_scope_ptr=static_cast(&id); } diff --git a/src/cpp/cpp_token_buffer.cpp b/src/cpp/cpp_token_buffer.cpp index 949a54e8874..df7e918f8a7 100644 --- a/src/cpp/cpp_token_buffer.cpp +++ b/src/cpp/cpp_token_buffer.cpp @@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu int cpp_token_buffert::LookAhead(unsigned offset) { - assert(current_pos<=token_vector.size()); + PRECONDITION(current_pos <= token_vector.size()); offset+=current_pos; @@ -27,7 +27,7 @@ int cpp_token_buffert::LookAhead(unsigned offset) int cpp_token_buffert::get_token(cpp_tokent &token) { - assert(current_pos<=token_vector.size()); + PRECONDITION(current_pos <= token_vector.size()); if(token_vector.size()==current_pos) read_token(); @@ -41,7 +41,7 @@ int cpp_token_buffert::get_token(cpp_tokent &token) int cpp_token_buffert::get_token() { - assert(current_pos<=token_vector.size()); + PRECONDITION(current_pos <= token_vector.size()); if(token_vector.size()==current_pos) read_token(); @@ -55,7 +55,7 @@ int cpp_token_buffert::get_token() int cpp_token_buffert::LookAhead(unsigned offset, cpp_tokent &token) { - assert(current_pos<=token_vector.size()); + PRECONDITION(current_pos <= token_vector.size()); offset+=current_pos; @@ -107,7 +107,7 @@ void cpp_token_buffert::Restore(post pos) void cpp_token_buffert::Replace(const cpp_tokent &token) { - assert(current_pos<=token_vector.size()); + PRECONDITION(current_pos <= token_vector.size()); if(token_vector.size()==current_pos) read_token(); @@ -117,7 +117,7 @@ void cpp_token_buffert::Replace(const cpp_tokent &token) void cpp_token_buffert::Insert(const cpp_tokent &token) { - assert(current_pos<=token_vector.size()); + PRECONDITION(current_pos <= token_vector.size()); tokens.push_back(token); diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index 166d036c1b3..abb002558de 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -64,11 +64,11 @@ const struct_typet &cpp_typecheckt::this_struct_type() const exprt &this_expr= cpp_scopes.current_scope().this_expr; - assert(this_expr.is_not_nil()); - assert(this_expr.type().id()==ID_pointer); + CHECK_RETURN(this_expr.is_not_nil()); + CHECK_RETURN(this_expr.type().id() == ID_pointer); const typet &t = follow(to_pointer_type(this_expr.type()).base_type()); - assert(t.id()==ID_struct); + CHECK_RETURN(t.id() == ID_struct); return to_struct_type(t); } @@ -167,9 +167,9 @@ void cpp_typecheckt::static_and_dynamic_initialization() if(cpp_is_pod(symbol.type)) continue; - assert(symbol.is_static_lifetime); - assert(!symbol.is_type); - assert(symbol.type.id()!=ID_code); + DATA_INVARIANT(symbol.is_static_lifetime, "should be static"); + DATA_INVARIANT(!symbol.is_type, "should not be a type"); + DATA_INVARIANT(symbol.type.id() != ID_code, "should not be code"); exprt symbol_expr=cpp_symbol_expr(symbol); @@ -228,7 +228,7 @@ void cpp_typecheckt::do_not_typechecked() symbol.value.id() == ID_cpp_not_typechecked && symbol.value.get_bool(ID_is_used)) { - assert(symbol.type.id()==ID_code); + DATA_INVARIANT(symbol.type.id() == ID_code, "must be code"); exprt value = symbol.value; if(symbol.base_name=="operator=") diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp index 18c5c9ddf9f..00e0bf5f569 100644 --- a/src/cpp/cpp_typecheck_code.cpp +++ b/src/cpp/cpp_typecheck_code.cpp @@ -124,7 +124,7 @@ void cpp_typecheckt::typecheck_try_catch(codet &code) code_frontend_declt &decl = to_code_frontend_decl(statements.front()); cpp_declarationt &cpp_declaration = to_cpp_declaration(decl.symbol()); - assert(cpp_declaration.declarators().size()==1); + PRECONDITION(cpp_declaration.declarators().size() == 1); cpp_declaratort &declarator=cpp_declaration.declarators().front(); if(is_reference(declarator.type())) @@ -197,8 +197,8 @@ void cpp_typecheckt::typecheck_switch(codet &code) codet decl = to_code(value); typecheck_decl(decl); - assert(decl.get_statement()==ID_decl_block); - assert(decl.operands().size()==1); + CHECK_RETURN(decl.get_statement() == ID_decl_block); + CHECK_RETURN(decl.operands().size() == 1); // replace declaration by its symbol value = to_code_frontend_decl(to_code(to_unary_expr(decl).op())).symbol(); @@ -245,7 +245,8 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code) { const code_typet &code_type=to_code_type(symbol_expr.type()); - assert(code_type.parameters().size()>=1); + DATA_INVARIANT( + code_type.parameters().size() >= 1, "at least one parameter"); // It's a parent. Call the constructor that we got. side_effect_expr_function_callt function_call( @@ -254,7 +255,7 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code) // we have to add 'this' exprt this_expr = cpp_scopes.current_scope().this_expr; - assert(this_expr.is_not_nil()); + PRECONDITION(this_expr.is_not_nil()); make_ptr_typecast( this_expr, @@ -406,7 +407,7 @@ void cpp_typecheckt::typecheck_decl(codet &code) throw 0; } - assert(code.op0().id()==ID_cpp_declaration); + PRECONDITION(code.op0().id() == ID_cpp_declaration); cpp_declarationt &declaration= to_cpp_declaration(code.op0()); @@ -418,7 +419,7 @@ void cpp_typecheckt::typecheck_decl(codet &code) if(declaration.declarators().empty() || !has_auto(type)) typecheck_type(type); - assert(type.is_not_nil()); + CHECK_RETURN(type.is_not_nil()); if(declaration.declarators().empty() && follow(type).get_bool(ID_C_is_anonymous)) diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 603c5de70cf..17b9e15fe49 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -305,8 +305,9 @@ void cpp_typecheckt::typecheck_compound_declarator( if(is_cast_operator) { - assert(declarator.name().get_sub().size()==2 && - declarator.name().get_sub().front().id()==ID_operator); + PRECONDITION( + declarator.name().get_sub().size() == 2 && + declarator.name().get_sub().front().id() == ID_operator); typet type=static_cast(declarator.name().get_sub()[1]); declarator.type().add_subtype() = type; @@ -515,9 +516,11 @@ void cpp_typecheckt::typecheck_compound_declarator( { is_virtual=true; const code_typet &code_type=to_code_type(comp.type()); - assert(!code_type.parameters().empty()); + DATA_INVARIANT( + !code_type.parameters().empty(), "must have parameters"); const typet &pointer_type=code_type.parameters()[0].type(); - assert(pointer_type.id()==ID_pointer); + DATA_INVARIANT( + pointer_type.id() == ID_pointer, "this must be pointer"); virtual_bases.insert( to_pointer_type(pointer_type).base_type().get(ID_identifier)); } @@ -937,8 +940,7 @@ void cpp_typecheckt::typecheck_compound_body(symbolt &symbol) // enter scope of compound cpp_scopes.set_scope(symbol.name); - assert(symbol.type.id()==ID_struct || - symbol.type.id()==ID_union); + PRECONDITION(symbol.type.id() == ID_struct || symbol.type.id() == ID_union); struct_union_typet &type= to_struct_union_type(symbol.type); @@ -1181,7 +1183,7 @@ void cpp_typecheckt::typecheck_compound_body(symbolt &symbol) // build declaration cpp_declarationt cpctor; default_cpctor(symbol, cpctor); - assert(cpctor.declarators().size()==1); + CHECK_RETURN(cpctor.declarators().size() == 1); exprt value(ID_cpp_not_typechecked); value.copy_to_operands(cpctor.declarators()[0].value()); @@ -1199,7 +1201,7 @@ void cpp_typecheckt::typecheck_compound_body(symbolt &symbol) // build declaration cpp_declarationt assignop; default_assignop(symbol, assignop); - assert(assignop.declarators().size()==1); + CHECK_RETURN(assignop.declarators().size() == 1); // The value will be typechecked only if the operator // is actually used @@ -1477,8 +1479,8 @@ bool cpp_typecheckt::get_component( { const typet &followed_type=follow(object.type()); - assert(followed_type.id()==ID_struct || - followed_type.id()==ID_union); + PRECONDITION( + followed_type.id() == ID_struct || followed_type.id() == ID_union); struct_union_typet final_type= to_struct_union_type(followed_type); @@ -1579,8 +1581,7 @@ bool cpp_typecheckt::check_component_access( if(access==ID_public) return false; // ok - assert(access==ID_private || - access==ID_protected); + PRECONDITION(access == ID_private || access == ID_protected); const irep_idt &struct_identifier= struct_union_type.get(ID_name); @@ -1683,8 +1684,8 @@ void cpp_typecheckt::make_ptr_typecast( { typet src_type=expr.type(); - assert(src_type.id()== ID_pointer); - assert(dest_type.id()== ID_pointer); + PRECONDITION(src_type.id() == ID_pointer); + PRECONDITION(dest_type.id() == ID_pointer); const struct_typet &src_struct = to_struct_type( static_cast(follow(to_pointer_type(src_type).base_type()))); diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp index 0c006ef9df7..79709e447a2 100644 --- a/src/cpp/cpp_typecheck_constructor.cpp +++ b/src/cpp/cpp_typecheck_constructor.cpp @@ -232,7 +232,7 @@ void cpp_typecheckt::default_cpctor( exprt var=virtual_table_symbol_var.symbol_expr(); address_of_exprt address(var); - assert(address.type() == mem_c.type()); + CHECK_RETURN(address.type() == mem_c.type()); already_typechecked_exprt::make_already_typechecked(address); @@ -422,11 +422,11 @@ void cpp_typecheckt::check_member_initializers( const struct_typet::componentst &components, const irept &initializers) { - assert(initializers.id()==ID_member_initializers); + PRECONDITION(initializers.id() == ID_member_initializers); for(const auto &initializer : initializers.get_sub()) { - assert(initializer.is_not_nil()); + PRECONDITION(initializer.is_not_nil()); const cpp_namet &member_name= to_cpp_name(initializer.find(ID_member)); @@ -549,7 +549,7 @@ void cpp_typecheckt::full_member_initialization( const struct_union_typet::componentst &components= struct_union_type.components(); - assert(initializers.id()==ID_member_initializers); + PRECONDITION(initializers.id() == ID_member_initializers); irept final_initializers(ID_member_initializers); @@ -687,7 +687,7 @@ void cpp_typecheckt::full_member_initialization( exprt var=virtual_table_symbol_var.symbol_expr(); address_of_exprt address(var); - assert(address.type() == c.type()); + CHECK_RETURN(address.type() == c.type()); already_typechecked_exprt::make_already_typechecked(address); diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp index b69caf0a58b..108b0cc85de 100644 --- a/src/cpp/cpp_typecheck_conversions.cpp +++ b/src/cpp/cpp_typecheck_conversions.cpp @@ -47,7 +47,7 @@ bool cpp_typecheckt::standard_conversion_lvalue_to_rvalue( const exprt &expr, exprt &new_expr) const { - assert(expr.get_bool(ID_C_lvalue)); + PRECONDITION(expr.get_bool(ID_C_lvalue)); if(expr.type().id() == ID_code) return false; @@ -78,7 +78,7 @@ bool cpp_typecheckt::standard_conversion_array_to_pointer( const exprt &expr, exprt &new_expr) const { - assert(expr.type().id()==ID_array); + PRECONDITION(expr.type().id() == ID_array); index_exprt index(expr, from_integer(0, c_index_type())); @@ -575,13 +575,13 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member( to_pointer_type(expr.type()).base_type().id() == ID_code) { code_typet code1 = to_code_type(to_pointer_type(expr.type()).base_type()); - assert(!code1.parameters().empty()); + DATA_INVARIANT(!code1.parameters().empty(), "must have parameters"); code_typet::parametert this1=code1.parameters()[0]; INVARIANT(this1.get_this(), "first parameter should be `this'"); code1.parameters().erase(code1.parameters().begin()); code_typet code2 = to_code_type(to_pointer_type(type).base_type()); - assert(!code2.parameters().empty()); + DATA_INVARIANT(!code2.parameters().empty(), "must have parameters"); code_typet::parametert this2=code2.parameters()[0]; INVARIANT(this2.get_this(), "first parameter should be `this'"); code2.parameters().erase(code2.parameters().begin()); @@ -682,7 +682,7 @@ bool cpp_typecheckt::standard_conversion_sequence( exprt &new_expr, unsigned &rank) { - assert(!is_reference(expr.type()) && !is_reference(type)); + PRECONDITION(!is_reference(expr.type()) && !is_reference(type)); exprt curr_expr=expr; @@ -862,8 +862,8 @@ bool cpp_typecheckt::user_defined_conversion_sequence( exprt &new_expr, unsigned &rank) { - assert(!is_reference(expr.type())); - assert(!is_reference(type)); + PRECONDITION(!is_reference(expr.type())); + PRECONDITION(!is_reference(type)); const typet &from=follow(expr.type()); const typet &to=follow(type); @@ -985,9 +985,9 @@ bool cpp_typecheckt::user_defined_conversion_sequence( uninitialized_typet{}, expr.source_location()); typecheck_side_effect_function_call(ctor_expr); + CHECK_RETURN(ctor_expr.get(ID_statement) == ID_temporary_object); new_expr.swap(ctor_expr); - assert(new_expr.get(ID_statement)==ID_temporary_object); if(to.get_bool(ID_C_constant)) new_expr.type().set(ID_C_constant, true); @@ -1119,8 +1119,8 @@ bool cpp_typecheckt::reference_related( const exprt &expr, const typet &type) const { - assert(is_reference(type)); - assert(!is_reference(expr.type())); + PRECONDITION(is_reference(type)); + PRECONDITION(!is_reference(expr.type())); typet from=follow(expr.type()); typet to = follow(to_reference_type(type).base_type()); @@ -1157,8 +1157,8 @@ bool cpp_typecheckt::reference_compatible( const typet &type, unsigned &rank) const { - assert(is_reference(type)); - assert(!is_reference(expr.type())); + PRECONDITION(is_reference(type)); + PRECONDITION(!is_reference(expr.type())); if(!reference_related(expr, type)) return false; @@ -1221,8 +1221,8 @@ bool cpp_typecheckt::reference_binding( exprt &new_expr, unsigned &rank) { - assert(is_reference(type)); - assert(!is_reference(expr.type())); + PRECONDITION(is_reference(type)); + PRECONDITION(!is_reference(expr.type())); unsigned backup_rank=rank; @@ -1301,7 +1301,8 @@ bool cpp_typecheckt::reference_binding( if(!is_reference(component_type.return_type())) continue; - assert(component_type.parameters().size()==1); + DATA_INVARIANT( + component_type.parameters().size() == 1, "exactly one parameter"); typet this_type = component_type.parameters().front().type(); @@ -1585,7 +1586,7 @@ void cpp_typecheckt::reference_initializer( exprt &expr, const typet &type) { - assert(is_reference(type)); + PRECONDITION(is_reference(type)); add_implicit_dereference(expr); unsigned rank=0; @@ -1605,7 +1606,7 @@ bool cpp_typecheckt::cast_away_constness( const typet &t1, const typet &t2) const { - assert(t1.id()==ID_pointer && t2.id()==ID_pointer); + PRECONDITION(t1.id() == ID_pointer && t2.id() == ID_pointer); typet nt1=t1; typet nt2=t2; diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp index 72a1666231c..4049003a68b 100644 --- a/src/cpp/cpp_typecheck_declaration.cpp +++ b/src/cpp/cpp_typecheck_declaration.cpp @@ -98,7 +98,7 @@ codet cpp_typecheckt::convert_anonymous_union(cpp_declarationt &declaration) void cpp_typecheckt::convert_non_template_declaration( cpp_declarationt &declaration) { - assert(!declaration.is_template()); + PRECONDITION(!declaration.is_template()); // we first check if this is a typedef typet &declaration_type=declaration.type(); diff --git a/src/cpp/cpp_typecheck_destructor.cpp b/src/cpp/cpp_typecheck_destructor.cpp index 18de2413708..6f080c1f55c 100644 --- a/src/cpp/cpp_typecheck_destructor.cpp +++ b/src/cpp/cpp_typecheck_destructor.cpp @@ -29,8 +29,7 @@ void cpp_typecheckt::default_dtor( const symbolt &symbol, cpp_declarationt &dtor) { - assert(symbol.type.id()==ID_struct || - symbol.type.id()==ID_union); + PRECONDITION(symbol.type.id() == ID_struct || symbol.type.id() == ID_union); cpp_declaratort decl; decl.name() = cpp_namet("~" + id2string(symbol.base_name), symbol.location); @@ -49,8 +48,7 @@ void cpp_typecheckt::default_dtor( /// produces destructor code for a class object codet cpp_typecheckt::dtor(const symbolt &symbol, const symbol_exprt &this_expr) { - assert(symbol.type.id()==ID_struct || - symbol.type.id()==ID_union); + PRECONDITION(symbol.type.id() == ID_struct || symbol.type.id() == ID_union); source_locationt source_location=symbol.type.source_location(); @@ -79,7 +77,7 @@ codet cpp_typecheckt::dtor(const symbolt &symbol, const symbol_exprt &this_expr) exprt var=virtual_table_symbol_var.symbol_expr(); address_of_exprt address(var); - assert(address.type() == c.type()); + DATA_INVARIANT(address.type() == c.type(), "type mismatch"); already_typechecked_exprt::make_already_typechecked(address); diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index c725d8bfb16..936510f8c36 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -134,7 +134,7 @@ void cpp_typecheckt::typecheck_expr_main(exprt &expr) void cpp_typecheckt::typecheck_expr_trinary(if_exprt &expr) { - assert(expr.operands().size()==3); + PRECONDITION(expr.operands().size() == 3); implicit_typecast(expr.op0(), bool_typet()); @@ -470,7 +470,7 @@ bool cpp_typecheckt::operator_is_overloaded(exprt &expr) expr.get_bool(ID_C_implicit)) return false; - assert(expr.operands().size()>=1); + PRECONDITION(expr.operands().size() >= 1); if(expr.id()=="explicit-typecast") { @@ -485,7 +485,7 @@ bool cpp_typecheckt::operator_is_overloaded(exprt &expr) // See if the struct declares the cast operator as a member bool found_in_struct=false; - assert(!expr.operands().empty()); + PRECONDITION(!expr.operands().empty()); typet t0(follow(to_unary_expr(expr).op().type())); if(t0.id()==ID_struct) @@ -543,8 +543,9 @@ bool cpp_typecheckt::operator_is_overloaded(exprt &expr) { if(expr.id()==e->id) { - if(expr.id()==ID_dereference) - assert(!expr.get_bool(ID_C_implicit)); + DATA_INVARIANT( + expr.id() != ID_dereference || !expr.get_bool(ID_C_implicit), + "no implicit dereference"); std::string op_name=std::string("operator")+e->op_name; @@ -734,8 +735,7 @@ void cpp_typecheckt::typecheck_expr_throw(exprt &expr) { expr.type() = void_type(); - assert(expr.operands().size()==1 || - expr.operands().empty()); + PRECONDITION(expr.operands().size() == 1 || expr.operands().empty()); if(expr.operands().size()==1) { @@ -840,7 +840,7 @@ static exprt collect_comma_expression(const exprt &src) if(src.id()==ID_comma) { - assert(src.operands().size()==2); + PRECONDITION(src.operands().size() == 2); result = collect_comma_expression(to_binary_expr(src).op0()); result.copy_to_operands(to_binary_expr(src).op1()); } @@ -970,7 +970,7 @@ void cpp_typecheckt::typecheck_expr_explicit_constructor_call(exprt &expr) } else { - assert(expr.type().id()==ID_struct); + CHECK_RETURN(expr.type().id() == ID_struct); struct_tag_typet tag(expr.type().get(ID_name)); tag.add_source_location() = expr.source_location(); @@ -992,8 +992,8 @@ void cpp_typecheckt::typecheck_expr_this(exprt &expr) const exprt &this_expr=cpp_scopes.current_scope().this_expr; const source_locationt source_location=expr.find_source_location(); - assert(this_expr.is_not_nil()); - assert(this_expr.type().id()==ID_pointer); + PRECONDITION(this_expr.is_not_nil()); + PRECONDITION(this_expr.type().id() == ID_pointer); expr=this_expr; expr.add_source_location()=source_location; @@ -1143,14 +1143,15 @@ void cpp_typecheckt::typecheck_expr_member( if(symbol_expr.id()==ID_dereference) { - assert(symbol_expr.get_bool(ID_C_implicit)); + CHECK_RETURN(symbol_expr.get_bool(ID_C_implicit)); exprt tmp = to_dereference_expr(symbol_expr).pointer(); symbol_expr.swap(tmp); } - assert(symbol_expr.id()==ID_symbol || - symbol_expr.id()==ID_member || - symbol_expr.id()==ID_constant); + DATA_INVARIANT( + symbol_expr.id() == ID_symbol || symbol_expr.id() == ID_member || + symbol_expr.id() == ID_constant, + "expression kind unexpected"); // If it is a symbol or a constant, just return it! // Note: the resolver returns a symbol if the member @@ -1232,7 +1233,7 @@ void cpp_typecheckt::typecheck_expr_member( symbol_table_baset::symbolst::const_iterator it = symbol_table.symbols.find(component_name); - assert(it!=symbol_table.symbols.end()); + CHECK_RETURN(it != symbol_table.symbols.end()); if(it->second.value.id() == ID_cpp_not_typechecked) symbol_table.get_writeable_ref(component_name) @@ -1244,7 +1245,7 @@ void cpp_typecheckt::typecheck_expr_ptrmember( exprt &expr, const cpp_typecheck_fargst &fargs) { - assert(expr.id()==ID_ptrmember); + PRECONDITION(expr.id() == ID_ptrmember); if(expr.operands().size()!=1) { @@ -1442,7 +1443,7 @@ void cpp_typecheckt::typecheck_expr_cpp_name( fargs); // we want VAR - assert(symbol_expr.id()!=ID_type); + CHECK_RETURN(symbol_expr.id() != ID_type); if(symbol_expr.id()==ID_member) { @@ -1534,11 +1535,11 @@ void cpp_typecheckt::typecheck_side_effect_function_call( if(expr.function().id() == ID_pod_constructor) { - assert(expr.function().type().id()==ID_code); + PRECONDITION(expr.function().type().id() == ID_code); // This must be a POD. const typet &pod=to_code_type(expr.function().type()).return_type(); - assert(cpp_is_pod(pod)); + PRECONDITION(cpp_is_pod(pod)); // These aren't really function calls, but either conversions or // initializations. @@ -1596,7 +1597,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call( } // add `this' - assert(bound.type().id()==ID_pointer); + DATA_INVARIANT(bound.type().id() == ID_pointer, "should be pointer"); expr.arguments().insert(expr.arguments().begin(), bound); // we don't need the object any more @@ -1612,7 +1613,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call( } else { - assert(expr.function().type().id()==ID_pointer); + PRECONDITION(expr.function().type().id() == ID_pointer); dereference_exprt tmp(expr.function()); tmp.add_source_location() = expr.function().source_location(); expr.function().swap(tmp); @@ -1654,7 +1655,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call( const struct_typet::componentt &vt_compo= vt_struct.get_component(vtable_name); - assert(vt_compo.is_not_nil()); + CHECK_RETURN(vt_compo.is_not_nil()); vtptr_member.set(ID_component_name, vtable_name); @@ -1668,7 +1669,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call( vtentry_member.set(ID_component_name, vtentry_component_name); typecheck_expr(vtentry_member); - assert(vtentry_member.type().id()==ID_pointer); + CHECK_RETURN(vtentry_member.type().id() == ID_pointer); { dereference_exprt tmp(vtentry_member); @@ -1720,12 +1721,12 @@ void cpp_typecheckt::typecheck_side_effect_function_call( if(expr.type().id()==ID_constructor) { - assert(expr.function().id() == ID_symbol); + PRECONDITION(expr.function().id() == ID_symbol); const code_typet::parameterst ¶meters= to_code_type(expr.function().type()).parameters(); - assert(parameters.size()>=1); + DATA_INVARIANT(!parameters.empty(), "parameters expected"); const auto &this_type = to_pointer_type(parameters[0].type()); @@ -1790,7 +1791,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call( return; } - assert(expr.operands().size()==2); + PRECONDITION(expr.operands().size() == 2); if(expr.function().id()==ID_member) typecheck_method_application(expr); @@ -1825,11 +1826,11 @@ void cpp_typecheckt::typecheck_side_effect_function_call( } } - assert(expr.operands().size()==2); + CHECK_RETURN(expr.operands().size() == 2); typecheck_function_call_arguments(expr); - assert(expr.operands().size()==2); + CHECK_RETURN(expr.operands().size() == 2); add_implicit_dereference(expr); @@ -1868,7 +1869,7 @@ void cpp_typecheckt::typecheck_function_call_arguments( { if(parameter.get_bool(ID_C_call_by_value)) { - assert(is_reference(parameter.type())); + DATA_INVARIANT(is_reference(parameter.type()), "reference expected"); if(arg_it->id()!=ID_temporary_object) { @@ -1927,10 +1928,10 @@ void cpp_typecheckt::typecheck_expr_side_effect( void cpp_typecheckt::typecheck_method_application( side_effect_expr_function_callt &expr) { - assert(expr.operands().size()==2); + PRECONDITION(expr.operands().size() == 2); - assert(expr.function().id()==ID_member); - assert(expr.function().operands().size()==1); + PRECONDITION(expr.function().id() == ID_member); + PRECONDITION(expr.function().operands().size() == 1); // turn e.f(...) into xx::f(e, ...) @@ -1971,7 +1972,7 @@ void cpp_typecheckt::typecheck_method_application( typet this_type=func_type.parameters().front().type(); // Special case. Make it a reference. - assert(this_type.id()==ID_pointer); + DATA_INVARIANT(this_type.id() == ID_pointer, "this should be pointer"); this_type.set(ID_C_reference, true); this_type.set(ID_C_this, true); @@ -1983,7 +1984,9 @@ void cpp_typecheckt::typecheck_method_application( func_type.parameters().front().type()) { implicit_typecast(expr.arguments().front(), this_type); - assert(is_reference(expr.arguments().front().type())); + DATA_INVARIANT( + is_reference(expr.arguments().front().type()), + "argument should be reference"); expr.arguments().front().type().remove(ID_C_reference); } } @@ -1991,7 +1994,8 @@ void cpp_typecheckt::typecheck_method_application( { exprt this_arg = to_member_expr(member_expr).compound(); implicit_typecast(this_arg, this_type); - assert(is_reference(this_arg.type())); + DATA_INVARIANT( + is_reference(this_arg.type()), "argument should be reference"); this_arg.type().remove(ID_C_reference); expr.arguments().insert(expr.arguments().begin(), this_arg); } @@ -2252,7 +2256,7 @@ void cpp_typecheckt::typecheck_expr_function_identifier(exprt &expr) symbol_table_baset::symbolst::const_iterator it = symbol_table.symbols.find(expr.get(ID_identifier)); - assert(it != symbol_table.symbols.end()); + CHECK_RETURN(it != symbol_table.symbols.end()); if(it->second.value.id() == ID_cpp_not_typechecked) symbol_table.get_writeable_ref(it->first).value.set(ID_is_used, true); @@ -2295,7 +2299,7 @@ void cpp_typecheckt::explicit_typecast_ambiguity(exprt &expr) if(expr.id()!="explicit-typecast") return; - assert(expr.operands().size()==1); + PRECONDITION(expr.operands().size() == 1); irep_idt op0_id = to_unary_expr(expr).op().id(); diff --git a/src/cpp/cpp_typecheck_fargs.cpp b/src/cpp/cpp_typecheck_fargs.cpp index 3d07e9974e3..ed402e8bffa 100644 --- a/src/cpp/cpp_typecheck_fargs.cpp +++ b/src/cpp/cpp_typecheck_fargs.cpp @@ -79,7 +79,7 @@ bool cpp_typecheck_fargst::match( // * User-defined conversion sequences // * Ellipsis conversion sequences - assert(it!=ops.end()); + DATA_INVARIANT(it != ops.end(), "arguments and parameters must match"); const exprt &operand=*it; typet type=parameter.type(); diff --git a/src/cpp/cpp_typecheck_fargs.h b/src/cpp/cpp_typecheck_fargs.h index 47bad0d8557..88524292737 100644 --- a/src/cpp/cpp_typecheck_fargs.h +++ b/src/cpp/cpp_typecheck_fargs.h @@ -56,7 +56,7 @@ class cpp_typecheck_fargst // for function overloading void remove_object() { - assert(has_object); + PRECONDITION(has_object); operands.erase(operands.begin()); has_object = false; } diff --git a/src/cpp/cpp_typecheck_function.cpp b/src/cpp/cpp_typecheck_function.cpp index 47a311faf22..e7968615198 100644 --- a/src/cpp/cpp_typecheck_function.cpp +++ b/src/cpp/cpp_typecheck_function.cpp @@ -111,7 +111,7 @@ void cpp_typecheckt::convert_function(symbolt &symbol) !function_scope.is_static_member) { code_typet::parameterst ¶meters=function_type.parameters(); - assert(parameters.size()>=1); + DATA_INVARIANT(parameters.size() >= 1, "parameters expected"); code_typet::parametert &this_parameter_expr=parameters.front(); function_scope.this_expr = symbol_exprt{ this_parameter_expr.get_identifier(), this_parameter_expr.type()}; diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index 5fab61517aa..a59f38773d8 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -269,7 +269,7 @@ void cpp_typecheckt::zero_initializer( for(const auto &component : union_type.components()) { - assert(component.type().is_not_nil()); + DATA_INVARIANT(component.type().is_not_nil(), "missing component type"); if(component.type().id()==ID_code) continue; diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index 885791d799e..1ee1f8be33a 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -52,8 +52,7 @@ void cpp_typecheck_resolvet::convert_identifiers( if(e.is_not_nil()) { - if(e.id()==ID_type) - assert(e.type().is_not_nil()); + CHECK_RETURN(e.id() != ID_type || e.type().is_not_nil()); identifiers.push_back(e); } @@ -75,8 +74,7 @@ void cpp_typecheck_resolvet::apply_template_args( if(e.is_not_nil()) { - if(e.id()==ID_type) - assert(e.type().is_not_nil()); + CHECK_RETURN(e.id() != ID_type || e.type().is_not_nil()); identifiers.push_back(e); } @@ -97,7 +95,7 @@ void cpp_typecheck_resolvet::guess_function_template_args( if(e.is_not_nil()) { - assert(e.id()!=ID_type); + CHECK_RETURN(e.id() != ID_type); identifiers.push_back(e); } } @@ -109,7 +107,7 @@ void cpp_typecheck_resolvet::guess_function_template_args( { // instantiate that one exprt e=*identifiers.begin(); - assert(e.id()==ID_template_function_instance); + CHECK_RETURN(e.id() == ID_template_function_instance); const symbolt &template_symbol= cpp_typecheck.lookup(e.type().get(ID_C_template)); @@ -222,8 +220,9 @@ exprt cpp_typecheck_resolvet::convert_identifier( const symbolt &compound_symbol= cpp_typecheck.lookup(identifier.class_identifier); - assert(compound_symbol.type.id()==ID_struct || - compound_symbol.type.id()==ID_union); + CHECK_RETURN( + compound_symbol.type.id() == ID_struct || + compound_symbol.type.id() == ID_union); const struct_union_typet &struct_union_type= to_struct_union_type(compound_symbol.type); @@ -232,7 +231,7 @@ exprt cpp_typecheck_resolvet::convert_identifier( struct_union_type.get_component(identifier.identifier); const typet &type=component.type(); - assert(type.is_not_nil()); + DATA_INVARIANT(type.is_not_nil(), "type must not be nil"); if(identifier.id_class==cpp_scopet::id_classt::TYPEDEF) { @@ -262,13 +261,15 @@ exprt cpp_typecheck_resolvet::convert_identifier( if(fargs.has_object) { // the object is given to us in fargs - assert(!fargs.operands.empty()); + PRECONDITION(!fargs.operands.empty()); object=fargs.operands.front(); } else if(this_expr.is_not_nil()) { // use this->... - assert(this_expr.type().id()==ID_pointer); + DATA_INVARIANT( + this_expr.type().id() == ID_pointer, + "this argument should be pointer"); object = exprt(ID_dereference, to_pointer_type(this_expr.type()).base_type()); object.copy_to_operands(this_expr); @@ -333,7 +334,7 @@ exprt cpp_typecheck_resolvet::convert_identifier( if(symbol.is_macro) // includes typedefs { e = type_exprt(symbol.type); - assert(symbol.type.is_not_nil()); + PRECONDITION(symbol.type.is_not_nil()); } else if(symbol.type.id()==ID_c_enum) { @@ -351,7 +352,7 @@ exprt cpp_typecheck_resolvet::convert_identifier( else if(symbol.is_macro) { e=symbol.value; - assert(e.is_not_nil()); + PRECONDITION(e.is_not_nil()); } else { @@ -506,7 +507,9 @@ void cpp_typecheck_resolvet::disambiguate_functions( const code_typet &f2 = to_code_type(resolve_it->type()); // TODO: may fail when using ellipsis - assert(f1.parameters().size() == f2.parameters().size()); + DATA_INVARIANT( + f1.parameters().size() == f2.parameters().size(), + "parameter numbers should match"); bool f1_better=true; bool f2_better=true; @@ -858,7 +861,7 @@ cpp_scopet &cpp_typecheck_resolvet::resolve_scope( irep_idt &base_name, cpp_template_args_non_tct &template_args) { - assert(!cpp_name.get_sub().empty()); + PRECONDITION(!cpp_name.get_sub().empty()); original_scope=&cpp_typecheck.cpp_scopes.current_scope(); source_location=cpp_name.source_location(); @@ -938,7 +941,7 @@ cpp_scopet &cpp_typecheck_resolvet::resolve_scope( throw 0; } - assert(id_set.size()==1); + CHECK_RETURN(id_set.size() == 1); cpp_typecheck.cpp_scopes.go_to(**id_set.begin()); @@ -959,7 +962,7 @@ cpp_scopet &cpp_typecheck_resolvet::resolve_scope( final_base_name+="operator"; irept::subt::const_iterator next=pos+1; - assert(next != cpp_name.get_sub().end()); + CHECK_RETURN(next != cpp_name.get_sub().end()); if( next->id() == ID_cpp_name || next->id() == ID_pointer || @@ -1019,7 +1022,7 @@ struct_tag_typet cpp_typecheck_resolvet::disambiguate_template_classes( primary_templates.insert(id); } - assert(!primary_templates.empty()); + CHECK_RETURN(!primary_templates.empty()); if(primary_templates.size()>=2) { @@ -1103,8 +1106,10 @@ struct_tag_typet cpp_typecheck_resolvet::disambiguate_template_classes( cpp_declaration.template_type()); // iterate over template instance - assert(full_template_args_tc.arguments().size()== - partial_specialization_args.arguments().size()); + DATA_INVARIANT( + full_template_args_tc.arguments().size() == + partial_specialization_args.arguments().size(), + "number of arguments should match"); // we need to do this in the right scope @@ -1152,8 +1157,10 @@ struct_tag_typet cpp_typecheck_resolvet::disambiguate_template_classes( // if these match the arguments, we have a match - assert(partial_specialization_args_tc.arguments().size()== - full_template_args_tc.arguments().size()); + DATA_INVARIANT( + partial_specialization_args_tc.arguments().size() == + full_template_args_tc.arguments().size(), + "argument numbers must match"); if(partial_specialization_args_tc== full_template_args_tc) @@ -1164,7 +1171,7 @@ struct_tag_typet cpp_typecheck_resolvet::disambiguate_template_classes( } } - assert(!matches.empty()); + CHECK_RETURN(!matches.empty()); std::sort(matches.begin(), matches.end()); @@ -1475,7 +1482,7 @@ exprt cpp_typecheck_resolvet::resolve( { const irep_idt id = id_ptr->identifier; const symbolt &s=cpp_typecheck.lookup(id); - assert(s.type.get_bool(ID_is_template)); + CHECK_RETURN(s.type.get_bool(ID_is_template)); if(to_cpp_declaration(s.type).is_class_template()) have_classes=true; else @@ -1879,7 +1886,7 @@ exprt cpp_typecheck_resolvet::guess_function_template_args( if(!tmp.get_bool(ID_is_template)) return nil_exprt(); // not a template - assert(expr.id()==ID_symbol); + PRECONDITION(expr.id() == ID_symbol); // a template is always a declaration const cpp_declarationt &cpp_declaration= @@ -1910,7 +1917,7 @@ exprt cpp_typecheck_resolvet::guess_function_template_args( cpp_declaration.template_type()); // there should be exactly one declarator - assert(cpp_declaration.declarators().size()==1); + PRECONDITION(cpp_declaration.declarators().size() == 1); const cpp_declaratort &function_declarator= cpp_declaration.declarators().front(); @@ -1961,7 +1968,8 @@ exprt cpp_typecheck_resolvet::guess_function_template_args( to_cpp_declaration(parameter); // again, there should be one declarator - assert(arg_declaration.declarators().size()==1); + DATA_INVARIANT( + arg_declaration.declarators().size() == 1, "exactly one declarator"); // turn into type typet arg_type= @@ -2093,7 +2101,7 @@ void cpp_typecheck_resolvet::apply_template_args( cpp_typecheck.lookup( fargs.operands.begin()->type().get(ID_identifier)); - assert(type_symb.type.id()==ID_struct); + CHECK_RETURN(type_symb.type.id() == ID_struct); const struct_typet &struct_type= to_struct_type(type_symb.type); @@ -2195,7 +2203,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes( if(id.is_class() || id.is_enum() || id.is_namespace()) { // std::cout << "X1\n"; - assert(id.is_scope); + DATA_INVARIANT(id.is_scope, "should be scope"); new_set.insert(&id); } else if(id.is_typedef()) @@ -2209,7 +2217,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes( while(true) { const symbolt &symbol=cpp_typecheck.lookup(identifier); - assert(symbol.is_type); + CHECK_RETURN(symbol.is_type); // todo? maybe do enum here, too? if(symbol.type.id()==ID_struct) @@ -2218,7 +2226,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes( cpp_idt &class_id= cpp_typecheck.cpp_scopes.get_id(identifier); - assert(class_id.is_scope); + DATA_INVARIANT(class_id.is_scope, "should be scope"); new_set.insert(&class_id); break; } @@ -2272,7 +2280,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes( irep_idt identifier=type.get_identifier(); const symbolt &symbol=cpp_typecheck.lookup(identifier); - assert(symbol.is_type); + CHECK_RETURN(symbol.is_type); if(symbol.type.id() == ID_template_parameter_symbol_type) type = to_template_parameter_symbol_type(symbol.type); @@ -2284,7 +2292,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes( cpp_idt &class_id= cpp_typecheck.cpp_scopes.get_id(identifier); - assert(class_id.is_scope); + DATA_INVARIANT(class_id.is_scope, "should be scope"); new_set.insert(&class_id); break; } diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp index 3ade4c59235..d807575b0be 100644 --- a/src/cpp/cpp_typecheck_template.cpp +++ b/src/cpp/cpp_typecheck_template.cpp @@ -204,7 +204,7 @@ void cpp_typecheckt::typecheck_class_template( void cpp_typecheckt::typecheck_function_template( cpp_declarationt &declaration) { - assert(declaration.declarators().size()==1); + PRECONDITION(declaration.declarators().size() == 1); cpp_declaratort &declarator=declaration.declarators()[0]; const cpp_namet &cpp_name = declarator.name(); @@ -304,13 +304,12 @@ void cpp_typecheckt::typecheck_function_template( void cpp_typecheckt::typecheck_class_template_member( cpp_declarationt &declaration) { - assert(declaration.declarators().size()==1); + PRECONDITION(declaration.declarators().size() == 1); cpp_declaratort &declarator=declaration.declarators()[0]; const cpp_namet &cpp_name = declarator.name(); - assert(cpp_name.is_qualified() || - cpp_name.has_template_args()); + PRECONDITION(cpp_name.is_qualified() || cpp_name.has_template_args()); // must be of the form: name1::name2 // or: name1::operator X @@ -495,7 +494,7 @@ void cpp_typecheckt::convert_class_template_specialization( typet &type=declaration.type(); - assert(type.id()==ID_struct); + PRECONDITION(type.id() == ID_struct); cpp_namet &cpp_name= static_cast(type.add(ID_tag)); @@ -565,7 +564,7 @@ void cpp_typecheckt::convert_class_template_specialization( symbol_table_baset::symbolst::const_iterator s_it = symbol_table.symbols.find((*id_set.begin())->identifier); - assert(s_it!=symbol_table.symbols.end()); + CHECK_RETURN(s_it != symbol_table.symbols.end()); const symbolt &template_symbol=s_it->second; @@ -619,14 +618,14 @@ void cpp_typecheckt::convert_template_function_or_member_specialization( throw 0; } - assert(declaration.declarators().size()==1); + PRECONDITION(declaration.declarators().size() == 1); cpp_declaratort declarator=declaration.declarators().front(); cpp_namet &cpp_name=declarator.name(); // There is specialization (instantiation with template arguments) // but also function overloading (no template arguments) - assert(!cpp_name.get_sub().empty()); + PRECONDITION(!cpp_name.get_sub().empty()); if(cpp_name.get_sub().back().id()==ID_template_args) { @@ -702,7 +701,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters( { cpp_save_scopet cpp_saved_scope(cpp_scopes); - assert(type.id()==ID_template); + PRECONDITION(type.id() == ID_template); std::string id_suffix="template::"+std::to_string(template_counter++); @@ -731,7 +730,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters( cpp_declarator_convertert cpp_declarator_converter(*this); // there must be _one_ declarator - assert(declaration.declarators().size()==1); + PRECONDITION(declaration.declarators().size() == 1); cpp_declaratort &declarator=declaration.declarators().front(); @@ -823,7 +822,7 @@ cpp_template_args_tct cpp_typecheckt::typecheck_template_args( // old stuff PRECONDITION(template_args.id() != ID_already_typechecked); - assert(template_symbol.type.get_bool(ID_is_template)); + PRECONDITION(template_symbol.type.get_bool(ID_is_template)); const template_typet &template_type= to_cpp_declaration(template_symbol.type).template_type(); @@ -880,7 +879,7 @@ cpp_template_args_tct cpp_typecheckt::typecheck_template_args( cpp_scopes.go_to(*template_scope); } - assert(i=1); + DATA_INVARIANT( + declaration.declarators().size() >= 1, "declarator required"); cpp_declaratort &declarator=declaration.declarators()[0]; const cpp_namet &cpp_name = declarator.name(); diff --git a/src/cpp/cpp_typecheck_type.cpp b/src/cpp/cpp_typecheck_type.cpp index d55c39f7b10..40e709b670a 100644 --- a/src/cpp/cpp_typecheck_type.cpp +++ b/src/cpp/cpp_typecheck_type.cpp @@ -24,8 +24,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu void cpp_typecheckt::typecheck_type(typet &type) { - assert(!type.id().empty()); - assert(type.is_not_nil()); + PRECONDITION(!type.id().empty()); + PRECONDITION(type.is_not_nil()); try { @@ -66,7 +66,7 @@ void cpp_typecheckt::typecheck_type(typet &type) } type=symbol_expr.type(); - assert(type.is_not_nil()); + PRECONDITION(type.is_not_nil()); if(type.get_bool(ID_C_constant)) qualifiers.is_constant = true; @@ -109,7 +109,8 @@ void cpp_typecheckt::typecheck_type(typet &type) if(class_object.id()==ID_cpp_name) { - assert(class_object.get_sub().back().id()=="::"); + DATA_INVARIANT( + class_object.get_sub().back().id() == "::", "scope suffix expected"); class_object.get_sub().pop_back(); } @@ -309,5 +310,5 @@ void cpp_typecheckt::typecheck_type(typet &type) throw 0; } - assert(type.is_not_nil()); + CHECK_RETURN(type.is_not_nil()); } diff --git a/src/cpp/cpp_typecheck_virtual_table.cpp b/src/cpp/cpp_typecheck_virtual_table.cpp index 7d01484afae..6817eec2761 100644 --- a/src/cpp/cpp_typecheck_virtual_table.cpp +++ b/src/cpp/cpp_typecheck_virtual_table.cpp @@ -18,7 +18,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu void cpp_typecheckt::do_virtual_table(const symbolt &symbol) { - assert(symbol.type.id()==ID_struct); + PRECONDITION(symbol.type.id() == ID_struct); // builds virtual-table value maps: (class x virtual_name x value) std::map > vt_value_maps; @@ -32,7 +32,7 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol) continue; const code_typet &code_type=to_code_type(compo.type()); - assert(code_type.parameters().size() > 0); + DATA_INVARIANT(code_type.parameters().size() > 0, "parameters expected"); const pointer_typet ¶meter_pointer_type= to_pointer_type(code_type.parameters()[0].type()); @@ -88,9 +88,9 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol) { std::map::const_iterator cit2 = value_map.find(compo.get_base_name()); - assert(cit2!=value_map.end()); + CHECK_RETURN(cit2 != value_map.end()); const exprt &value=cit2->second; - assert(value.type()==compo.type()); + DATA_INVARIANT(value.type() == compo.type(), "component type mismatch"); values.operands().push_back(value); } vt_symb_var.value=values; diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp index 34d9fe4fbdb..e63708c6a30 100644 --- a/src/cpp/expr2cpp.cpp +++ b/src/cpp/expr2cpp.cpp @@ -63,7 +63,8 @@ std::string expr2cppt::convert_struct( const struct_typet::componentst &components= struct_type.components(); - assert(components.size()==src.operands().size()); + DATA_INVARIANT( + components.size() == src.operands().size(), "component count mismatch"); exprt::operandst::const_iterator o_it=src.operands().begin(); diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index cc5eff8807b..66442cbace4 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -1714,7 +1714,7 @@ bool Parser::rOtherDeclaration( std::cout << std::string(__indent, ' ') << "Parser::rOtherDeclaration 4\n"; #endif - assert(!type_name.get_sub().empty()); + DATA_INVARIANT(!type_name.get_sub().empty(), "type name details expected"); for(std::size_t i=0; i < type_name.get_sub().size(); i++) { @@ -1752,7 +1752,7 @@ bool Parser::rOtherDeclaration( std::cout << std::string(__indent, ' ') << "Parser::rOtherDeclaration 6\n"; #endif - assert(!type_name.get_sub().empty()); + DATA_INVARIANT(!type_name.get_sub().empty(), "type name details expected"); bool is_destructor=false; for(const auto &irep : type_name.get_sub()) @@ -3363,7 +3363,7 @@ bool Parser::optPtrOperator(typet &ptrs) } else { - assert(it->is_not_nil()); + DATA_INVARIANT(it->is_not_nil(), "must not be nil"); it->add_subtype().swap(ptrs); } @@ -3725,7 +3725,7 @@ bool Parser::rOperatorName(irept &name) return rCastOperatorName(name); } - assert(!operator_id.empty()); + DATA_INVARIANT(!operator_id.empty(), "operator id missing"); lex.get_token(tk); name=irept(operator_id); set_location(name, tk); @@ -4000,8 +4000,8 @@ bool Parser::rTemplateArgs(irept &template_args) tk2.text='>'; lex.Replace(tk2); lex.Insert(tk2); - assert(lex.LookAhead(0)=='>'); - assert(lex.LookAhead(1)=='>'); + DATA_INVARIANT(lex.LookAhead(0) == '>', "should be >"); + DATA_INVARIANT(lex.LookAhead(1) == '>', "should be >"); return true; default: @@ -7787,7 +7787,8 @@ optionalt Parser::rTryStatement() return {}; // No name in the declarator? Make one. - assert(declaration.declarators().size()==1); + DATA_INVARIANT( + declaration.declarators().size() == 1, "exactly one declarator"); if(declaration.declarators().front().name().is_nil()) declaration.declarators().front().name() = cpp_namet("#anon"); diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp index fd97a58806a..6ff7822bed7 100644 --- a/src/goto-analyzer/unreachable_instructions.cpp +++ b/src/goto-analyzer/unreachable_instructions.cpp @@ -140,12 +140,12 @@ static void add_to_json( std::string s=oss.str(); std::string::size_type n=s.find('\n'); - assert(n!=std::string::npos); + CHECK_RETURN(n != std::string::npos); s.erase(0, n+1); n=s.find_first_not_of(' '); - assert(n!=std::string::npos); + CHECK_RETURN(n != std::string::npos); s.erase(0, n); - assert(!s.empty()); + CHECK_RETURN(!s.empty()); s.erase(s.size()-1); // print info for file actually with full path diff --git a/src/goto-diff/change_impact.cpp b/src/goto-diff/change_impact.cpp index dba94cefce6..b974c27e47a 100644 --- a/src/goto-diff/change_impact.cpp +++ b/src/goto-diff/change_impact.cpp @@ -363,17 +363,17 @@ void change_impactt::change_impact( switch(d.second) { case unified_difft::differencet::SAME: - assert(o_it!=old_goto_program.instructions.end()); - assert(n_it!=new_goto_program.instructions.end()); + INVARIANT(o_it != old_goto_program.instructions.end(), "within range"); + INVARIANT(n_it != new_goto_program.instructions.end(), "within range"); old_impact[o_it]|=SAME; ++o_it; - assert(n_it==d.first); + INVARIANT(n_it == d.first, "start of hunk"); new_impact[n_it]|=SAME; ++n_it; break; case unified_difft::differencet::DELETED: - assert(o_it!=old_goto_program.instructions.end()); - assert(o_it==d.first); + INVARIANT(o_it != old_goto_program.instructions.end(), "within range"); + INVARIANT(o_it == d.first, "start of hunk"); { const dependence_grapht::nodet &d_node= old_dep_graph[old_dep_graph[o_it].get_node_id()]; @@ -391,8 +391,8 @@ void change_impactt::change_impact( ++o_it; break; case unified_difft::differencet::NEW: - assert(n_it!=new_goto_program.instructions.end()); - assert(n_it==d.first); + INVARIANT(n_it != new_goto_program.instructions.end(), "within range"); + INVARIANT(n_it == d.first, "start of hunk"); { const dependence_grapht::nodet &d_node= new_dep_graph[new_dep_graph[n_it].get_node_id()]; @@ -548,7 +548,7 @@ void change_impactt::operator()() ns_new); else { - assert(oc_it->first==nc_it->first); + INVARIANT(oc_it->first == nc_it->first, "same instruction"); output_change_impact( nc_it->first, @@ -572,7 +572,7 @@ void change_impactt::output_change_impact( { goto_functionst::function_mapt::const_iterator f_it = goto_functions.function_map.find(function_id); - assert(f_it!=goto_functions.function_map.end()); + CHECK_RETURN(f_it != goto_functions.function_map.end()); const goto_programt &goto_program=f_it->second.body; if(!compact_output) @@ -620,12 +620,12 @@ void change_impactt::output_change_impact( { goto_functionst::function_mapt::const_iterator o_f_it = o_goto_functions.function_map.find(function_id); - assert(o_f_it!=o_goto_functions.function_map.end()); + CHECK_RETURN(o_f_it != o_goto_functions.function_map.end()); const goto_programt &old_goto_program=o_f_it->second.body; goto_functionst::function_mapt::const_iterator f_it = n_goto_functions.function_map.find(function_id); - assert(f_it!=n_goto_functions.function_map.end()); + CHECK_RETURN(f_it != n_goto_functions.function_map.end()); const goto_programt &goto_program=f_it->second.body; if(!compact_output) @@ -678,18 +678,20 @@ void change_impactt::output_change_impact( { prefix='D'; - assert(old_mod_flags==SAME || - old_mod_flags&DEL_DATA_DEP || - old_mod_flags&DEL_CTRL_DEP); + DATA_INVARIANT( + old_mod_flags == SAME || old_mod_flags & DEL_DATA_DEP || + old_mod_flags & DEL_CTRL_DEP, + "expected kind of flag"); ++o_target; } else if(mod_flags&NEW_CTRL_DEP) { prefix='C'; - assert(old_mod_flags==SAME || - old_mod_flags&DEL_DATA_DEP || - old_mod_flags&DEL_CTRL_DEP); + DATA_INVARIANT( + old_mod_flags == SAME || old_mod_flags & DEL_DATA_DEP || + old_mod_flags & DEL_CTRL_DEP, + "expected kind of flag"); ++o_target; } else diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index 95353a09ca8..8431005f169 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -689,7 +689,7 @@ bool acceleration_utilst::do_arrays( } else { - assert(!"ITSALLGONEWRONG"); + UNREACHABLE; } or_exprt unchanged_by_this_one( diff --git a/src/goto-instrument/accelerate/polynomial.cpp b/src/goto-instrument/accelerate/polynomial.cpp index 74582741021..ea9f9194f92 100644 --- a/src/goto-instrument/accelerate/polynomial.cpp +++ b/src/goto-instrument/accelerate/polynomial.cpp @@ -367,7 +367,7 @@ int monomialt::compare(monomialt &other) } else { - assert(it->var==jt->var); + INVARIANT(it->var == jt->var, "must match"); // Variables are equal, compare exponents. if(e1 < e2) { @@ -379,7 +379,7 @@ int monomialt::compare(monomialt &other) } else { - assert(e1==e2); + INVARIANT(e1 == e2, "must match"); // v1==v2 && e1 == e2. Look at the next term in the power product. ++it; ++jt; diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp index 8cc41a0d014..801821b7674 100644 --- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp +++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp @@ -332,7 +332,7 @@ bool polynomial_acceleratort::fit_polynomial_sliced( } std::size_t width=to_bitvector_type(var.type()).get_width(); - assert(width>0); + CHECK_RETURN(width > 0); for(std::vector::iterator it=parameters.begin(); it!=parameters.end(); diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp index d5fca111024..eb645a5a9b1 100644 --- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp +++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp @@ -119,7 +119,7 @@ void sat_path_enumeratort::build_path( // We should have a looping path, so we should never hit a location // with no successors. - assert(succs.size() > 0); + CHECK_RETURN(succs.size() > 0); if(succs.size()==1) { @@ -150,7 +150,7 @@ void sat_path_enumeratort::build_path( } } - assert(found_branch); + INVARIANT(found_branch, "no branch taken"); exprt cond=nil_exprt(); @@ -264,7 +264,7 @@ void sat_path_enumeratort::build_fixed() if(t->is_goto()) { - assert(fixedt->is_goto()); + DATA_INVARIANT(fixedt->is_goto(), "inconsistent programs"); // If this is a forwards jump, it's either jumping inside the loop // (in which case we leave it alone), or it jumps outside the loop. // If it jumps out of the loop, it's on a path we don't care about diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h index d075f605e4c..0fb1e2b3a06 100644 --- a/src/goto-instrument/dump_c_class.h +++ b/src/goto-instrument/dump_c_class.h @@ -204,8 +204,8 @@ class dump_ct code_frontend_declt d(sym); std::string d_str=expr_to_string(d); - assert(!d_str.empty()); - assert(*d_str.rbegin()==';'); + CHECK_RETURN(!d_str.empty()); + CHECK_RETURN(*d_str.rbegin() == ';'); return d_str.substr(0, d_str.size()-1); } diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index 36d6a673d17..a5d54c954f9 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -40,9 +40,9 @@ void full_slicert::add_function_calls( { goto_functionst::function_mapt::const_iterator f_it = goto_functions.function_map.find(node.function_id); - assert(f_it!=goto_functions.function_map.end()); + CHECK_RETURN(f_it != goto_functions.function_map.end()); - assert(!f_it->second.body.instructions.empty()); + CHECK_RETURN(!f_it->second.body.instructions.empty()); goto_programt::const_targett begin_function= f_it->second.body.instructions.begin(); diff --git a/src/goto-instrument/function.cpp b/src/goto-instrument/function.cpp index 575c7a5c3de..066c2e7edc8 100644 --- a/src/goto-instrument/function.cpp +++ b/src/goto-instrument/function.cpp @@ -49,7 +49,7 @@ code_function_callt function_to_call( symbol_table.insert(std::move(new_symbol)); s_it=symbol_table.symbols.find(id); - assert(s_it!=symbol_table.symbols.end()); + DATA_INVARIANT(s_it != symbol_table.symbols.end(), "symbol not found"); #endif } @@ -141,7 +141,7 @@ void function_exit( // exiting without return goto_programt::targett last=body.instructions.end(); last--; - assert(last->is_end_function()); + DATA_INVARIANT(last->is_end_function(), "must be end of function"); // is there already a return? bool has_set_return_value = false; diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 1e579669da8..a39ae1f33f3 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -60,7 +60,7 @@ void goto_program2codet::build_loop_map() l_it!=loops.loop_map.end(); ++l_it) { - assert(!l_it->second.empty()); + PRECONDITION(!l_it->second.empty()); // l_it->first need not be the program-order first instruction in the // natural loop, because a natural loop may have multiple entries. But we @@ -137,7 +137,7 @@ goto_programt::const_targett goto_program2codet::convert_instruction( goto_programt::const_targett upper_bound, code_blockt &dest) { - assert(target!=goto_program.instructions.end()); + PRECONDITION(target != goto_program.instructions.end()); if( target->type() != ASSERT && @@ -346,7 +346,7 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs( // if the return value is used, the next instruction will be assign goto_programt::const_targett next=target; ++next; - assert(next!=goto_program.instructions.end()); + CHECK_RETURN(next != goto_program.instructions.end()); if(next!=upper_bound && next->is_assign()) { @@ -366,7 +366,8 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs( } // assignment not found, still need a proper typeof expression - assert(r.find(ID_C_va_arg_type).is_not_nil()); + DATA_INVARIANT( + r.find(ID_C_va_arg_type).is_not_nil(), "#va_arg_type must be set"); const typet &va_arg_type= static_cast(r.find(ID_C_va_arg_type)); @@ -431,7 +432,7 @@ goto_programt::const_targett goto_program2codet::convert_set_return_value( // all v3 (or later) goto programs have an explicit GOTO after return goto_programt::const_targett next=target; ++next; - assert(next!=goto_program.instructions.end()); + CHECK_RETURN(next != goto_program.instructions.end()); // skip goto (and possibly dead), unless crossing the current boundary while(next!=upper_bound && next->is_dead() && !next->is_target()) @@ -455,7 +456,7 @@ goto_programt::const_targett goto_program2codet::convert_decl( goto_programt::const_targett next=target; ++next; - assert(next!=goto_program.instructions.end()); + CHECK_RETURN(next != goto_program.instructions.end()); // see if decl can go in current dest block dead_mapt::const_iterator entry=dead_map.find(symbol.get_identifier()); @@ -513,7 +514,7 @@ goto_programt::const_targett goto_program2codet::convert_do_while( goto_programt::const_targett loop_end, code_blockt &dest) { - assert(loop_end->is_goto() && loop_end->is_backwards_goto()); + PRECONDITION(loop_end->is_goto() && loop_end->is_backwards_goto()); code_dowhilet d(loop_end->condition(), code_blockt()); simplify(d.cond(), ns); @@ -538,9 +539,9 @@ goto_programt::const_targett goto_program2codet::convert_goto( goto_programt::const_targett upper_bound, code_blockt &dest) { - assert(target->is_goto()); + PRECONDITION(target->is_goto()); // we only do one target for now - assert(target->targets.size()==1); + PRECONDITION(target->targets.size() == 1); loopt::const_iterator loop_entry=loop_map.find(target); @@ -561,7 +562,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_while( goto_programt::const_targett loop_end, code_blockt &dest) { - assert(loop_end->is_goto() && loop_end->is_backwards_goto()); + PRECONDITION(loop_end->is_goto() && loop_end->is_backwards_goto()); if(target==loop_end) // 1: GOTO 1 return convert_goto_goto(target, dest); @@ -569,7 +570,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_while( code_whilet w(true_exprt{}, code_blockt{}); goto_programt::const_targett after_loop=loop_end; ++after_loop; - assert(after_loop!=goto_program.instructions.end()); + CHECK_RETURN(after_loop != goto_program.instructions.end()); copy_source_location(target, w); @@ -713,7 +714,7 @@ goto_programt::const_targett goto_program2codet::get_cases( to_equal_expr(*e_it).rhs(), cases_it, cases_it->get_target())); - assert(cases.back().value.is_not_nil()); + DATA_INVARIANT(cases.back().value.is_not_nil(), "cases should be set"); if(first_target==goto_program.instructions.end() || first_target->location_number> @@ -955,8 +956,9 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch( // as in case 1: case 2: code; we build a nested code_switch_caset if(targets_done.find(it->case_start)!=targets_done.end()) { - assert(it->case_selector==orig_target || - !it->case_selector->is_target()); + DATA_INVARIANT( + it->case_selector == orig_target || !it->case_selector->is_target(), + "valid case selector required"); // maintain the order to ensure convergence -> go to the innermost code_switch_caset *cscp=&to_code_switch_case( @@ -1033,12 +1035,12 @@ goto_programt::const_targett goto_program2codet::convert_goto_if( goto_programt::const_targett else_case=target->get_target(); goto_programt::const_targett before_else=else_case; goto_programt::const_targett end_if=target->get_target(); - assert(end_if!=goto_program.instructions.end()); + PRECONDITION(end_if != goto_program.instructions.end()); bool has_else=false; if(!target->is_backwards_goto()) { - assert(else_case!=goto_program.instructions.begin()); + PRECONDITION(else_case != goto_program.instructions.begin()); --before_else; // goto 1 @@ -1107,7 +1109,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue( goto_programt::const_targett upper_bound, code_blockt &dest) { - assert(!loop_last_stack.empty()); + PRECONDITION(!loop_last_stack.empty()); const cfg_dominatorst &dominators=loops.get_dominator_info(); // goto 1 @@ -1233,14 +1235,14 @@ goto_programt::const_targett goto_program2codet::convert_start_thread( goto_programt::const_targett upper_bound, code_blockt &dest) { - assert(target->is_start_thread()); + PRECONDITION(target->is_start_thread()); goto_programt::const_targett thread_start=target->get_target(); - assert(thread_start->location_number > target->location_number); + PRECONDITION(thread_start->location_number > target->location_number); goto_programt::const_targett next=target; ++next; - assert(next!=goto_program.instructions.end()); + CHECK_RETURN(next != goto_program.instructions.end()); // first check for old-style code: // __CPROVER_DUMP_0: START THREAD 1 @@ -1251,8 +1253,10 @@ goto_programt::const_targett goto_program2codet::convert_start_thread( { goto_programt::const_targett this_end=next; ++this_end; - assert(this_end->is_end_thread()); - assert(thread_start->location_number > this_end->location_number); + DATA_INVARIANT(this_end->is_end_thread(), "should be end-of-thread"); + DATA_INVARIANT( + thread_start->location_number > this_end->location_number, + "start of new thread must precede end of thread"); codet b=code_blockt(); convert_instruction(next, this_end, to_code_block(b)); @@ -1270,7 +1274,7 @@ goto_programt::const_targett goto_program2codet::convert_start_thread( b = std::move(l); } - assert(b.get_statement()==ID_label); + DATA_INVARIANT(b.get_statement() == ID_label, "must be label statement"); dest.add(std::move(b)); return this_end; } @@ -1293,11 +1297,15 @@ goto_programt::const_targett goto_program2codet::convert_start_thread( goto_programt::const_targett thread_end=next->get_target(); --thread_end; - assert(thread_start->location_number < thread_end->location_number); - assert(thread_end->is_end_thread()); + DATA_INVARIANT( + thread_start->location_number < thread_end->location_number, + "monotone location numbers"); + DATA_INVARIANT(thread_end->is_end_thread(), "should be end-of-thread"); - assert(upper_bound==goto_program.instructions.end() || - thread_end->location_number < upper_bound->location_number); + DATA_INVARIANT( + upper_bound == goto_program.instructions.end() || + thread_end->location_number < upper_bound->location_number, + "end or monotone location numbers"); /* end structure check */ // use pthreads if "code in new thread" is a function call to a function with @@ -1339,7 +1347,7 @@ goto_programt::const_targett goto_program2codet::convert_start_thread( b = std::move(l); } - assert(b.get_statement()==ID_label); + DATA_INVARIANT(b.get_statement() == ID_label, "should be label statement"); dest.add(std::move(b)); return thread_end; } @@ -1391,7 +1399,7 @@ void goto_program2codet::add_local_types(const typet &type) !type_names_set.insert(identifier).second) return; - assert(!identifier.empty()); + DATA_INVARIANT(!identifier.empty(), "identifier required"); type_names.push_back(identifier); } else if(type.id()==ID_pointer || @@ -1461,7 +1469,7 @@ void goto_program2codet::cleanup_code( code_labelt &cl=to_code_label(code); const irep_idt &label=cl.get_label(); - assert(!label.empty()); + DATA_INVARIANT(!label.empty(), "label must be set"); if(labels_in_use.find(label)==labels_in_use.end()) { @@ -1526,7 +1534,7 @@ void goto_program2codet::cleanup_code_block( codet &code, const irep_idt parent_stmt) { - assert(code.get_statement()==ID_block); + PRECONDITION(code.get_statement() == ID_block); exprt::operandst &operands=code.operands(); for(exprt::operandst::size_type i=0; @@ -1918,8 +1926,9 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast) typedef_names.find(typedef_str)==typedef_names.end()) expr.type().remove(ID_C_typedef); - assert(expr.type().id()!=ID_union && - expr.type().id()!=ID_struct); + DATA_INVARIANT( + !can_cast_type(expr.type()), + "typedef must not be that of a struct or union type"); } } else if(expr.id()==ID_symbol) diff --git a/src/goto-instrument/goto_program2code.h b/src/goto-instrument/goto_program2code.h index 7d11e767a6a..cfb514a4144 100644 --- a/src/goto-instrument/goto_program2code.h +++ b/src/goto-instrument/goto_program2code.h @@ -66,7 +66,7 @@ class goto_program2codet typedef_names(_typedef_names), system_headers(_system_headers) { - assert(local_static.empty()); + PRECONDITION(local_static.empty()); for(id_listt::const_iterator it=type_names.begin(); diff --git a/src/goto-instrument/havoc_loops.cpp b/src/goto-instrument/havoc_loops.cpp index 1e4f768a5cd..108eab9a94e 100644 --- a/src/goto-instrument/havoc_loops.cpp +++ b/src/goto-instrument/havoc_loops.cpp @@ -61,7 +61,7 @@ void havoc_loopst::havoc_loop( const goto_programt::targett loop_head, const loopt &loop) { - assert(!loop.empty()); + PRECONDITION(!loop.empty()); // first find out what can get changed in the loop assignst assigns; diff --git a/src/goto-instrument/k_induction.cpp b/src/goto-instrument/k_induction.cpp index d85c8fcd3d5..05fcc37a6f1 100644 --- a/src/goto-instrument/k_induction.cpp +++ b/src/goto-instrument/k_induction.cpp @@ -64,7 +64,7 @@ void k_inductiont::process_loop( const goto_programt::targett loop_head, const loopt &loop) { - assert(!loop.empty()); + PRECONDITION(!loop.empty()); // save the loop guard const exprt loop_guard = loop_head->condition(); @@ -126,14 +126,16 @@ void k_inductiont::process_loop( } // now turn any assertions in iterations 0..k-1 into assumptions - assert(iteration_points.size()==k+1); + DATA_INVARIANT( + iteration_points.size() == k + 1, "number of iteration points"); - assert(k>=1); + DATA_INVARIANT(k >= 1, "at least one iteration"); goto_programt::targett end=iteration_points[k-1]; for(goto_programt::targett t=loop_head; t!=end; t++) { - assert(t!=goto_function.body.instructions.end()); + DATA_INVARIANT( + t != goto_function.body.instructions.end(), "t is in range"); if(t->is_assert()) t->turn_into_assume(); } diff --git a/src/goto-instrument/loop_utils.cpp b/src/goto-instrument/loop_utils.cpp index a3f8144157d..d60f22316fb 100644 --- a/src/goto-instrument/loop_utils.cpp +++ b/src/goto-instrument/loop_utils.cpp @@ -20,7 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com goto_programt::targett get_loop_exit(const loopt &loop) { - assert(!loop.empty()); + PRECONDITION(!loop.empty()); // find the last instruction in the loop std::map loop_map; diff --git a/src/goto-instrument/rw_set.cpp b/src/goto-instrument/rw_set.cpp index 993b57a83a7..ee51a74feea 100644 --- a/src/goto-instrument/rw_set.cpp +++ b/src/goto-instrument/rw_set.cpp @@ -168,7 +168,7 @@ void _rw_set_loct::read_write_rec( } else if(expr.id()==ID_address_of) { - assert(expr.operands().size()==1); + PRECONDITION(expr.operands().size() == 1); } else if(expr.id()==ID_if) { diff --git a/src/goto-instrument/skip_loops.cpp b/src/goto-instrument/skip_loops.cpp index e4ae06e3e7c..688e33884f7 100644 --- a/src/goto-instrument/skip_loops.cpp +++ b/src/goto-instrument/skip_loops.cpp @@ -43,7 +43,7 @@ static bool skip_loops( goto_programt::targett loop_head=it->get_target(); goto_programt::targett next=it; ++next; - assert(next!=goto_program.instructions.end()); + CHECK_RETURN(next != goto_program.instructions.end()); goto_program.insert_before( loop_head, diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp index 05535c6fae2..4eb4565e416 100644 --- a/src/goto-instrument/stack_depth.cpp +++ b/src/goto-instrument/stack_depth.cpp @@ -62,7 +62,7 @@ static void stack_depth( const std::size_t i_depth, const exprt &max_depth) { - assert(!goto_program.instructions.empty()); + PRECONDITION(!goto_program.instructions.empty()); goto_programt::targett first=goto_program.instructions.begin(); @@ -81,7 +81,7 @@ static void stack_depth( first->source_location())); goto_programt::targett last=--goto_program.instructions.end(); - assert(last->is_end_function()); + DATA_INVARIANT(last->is_end_function(), "must be end of function"); goto_programt::instructiont minus_ins = goto_programt::make_assignment( code_assignt(symbol, minus_exprt(symbol, from_integer(1, symbol.type()))), diff --git a/src/goto-instrument/thread_instrumentation.cpp b/src/goto-instrument/thread_instrumentation.cpp index 631ecee1b90..5590f370fcf 100644 --- a/src/goto-instrument/thread_instrumentation.cpp +++ b/src/goto-instrument/thread_instrumentation.cpp @@ -33,7 +33,7 @@ void thread_exit_instrumentation(goto_programt &goto_program) goto_programt::targett end=goto_program.instructions.end(); end--; - assert(end->is_end_function()); + DATA_INVARIANT(end->is_end_function(), "must be end of function"); goto_program.insert_before_swap(end); diff --git a/src/goto-instrument/uninitialized.cpp b/src/goto-instrument/uninitialized.cpp index 6764aba1bee..a4b1cc1b58b 100644 --- a/src/goto-instrument/uninitialized.cpp +++ b/src/goto-instrument/uninitialized.cpp @@ -142,7 +142,8 @@ void uninitializedt::add_assertions( if(uninitialized.find(identifier)!=uninitialized.end()) { - assert(tracking.find(identifier)!=tracking.end()); + INVARIANT( + tracking.find(identifier) != tracking.end(), "not tracked"); const irep_idt new_identifier=id2string(identifier)+"#initialized"; // insert assertion diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp index 98094d7a9a0..f813b4843b3 100644 --- a/src/goto-instrument/unwind.cpp +++ b/src/goto-instrument/unwind.cpp @@ -28,8 +28,8 @@ void goto_unwindt::copy_segment( const goto_programt::const_targett end, // exclusive goto_programt &goto_program) // result { - assert(start->location_numberlocation_number); - assert(goto_program.empty()); + PRECONDITION(start->location_number < end->location_number); + PRECONDITION(goto_program.empty()); // build map for branch targets inside the loop typedef std::map target_mapt; @@ -43,7 +43,7 @@ void goto_unwindt::copy_segment( // make a copy std::vector target_vector; target_vector.reserve(target_map.size()); - assert(target_vector.empty()); + CHECK_RETURN(target_vector.empty()); for(goto_programt::const_targett t=start; t!=end; t++) { @@ -54,7 +54,7 @@ void goto_unwindt::copy_segment( target_vector.push_back(t_new); // store copied instruction } - assert(goto_program.instructions.size()==target_vector.size()); + CHECK_RETURN(goto_program.instructions.size() == target_vector.size()); // adjust intra-segment gotos for(std::size_t target_index = 0; target_index < target_vector.size(); @@ -73,7 +73,7 @@ void goto_unwindt::copy_segment( { unsigned j=m_it->second; - assert(jset_target(target_vector[j]); } } @@ -107,8 +107,8 @@ void goto_unwindt::unwind( const unwind_strategyt unwind_strategy, std::vector &iteration_points) { - assert(iteration_points.empty()); - assert(loop_head->location_numberlocation_number); + PRECONDITION(iteration_points.empty()); + PRECONDITION(loop_head->location_number < loop_exit->location_number); // rest program after unwound part goto_programt rest_program; @@ -135,7 +135,7 @@ void goto_unwindt::unwind( goto_programt::const_targett t=loop_exit; t--; - assert(t->is_backwards_goto()); + DATA_INVARIANT(t->is_backwards_goto(), "must be backwards goto"); exprt exit_cond = false_exprt(); // default is false @@ -175,7 +175,7 @@ void goto_unwindt::unwind( } - assert(!rest_program.empty()); + CHECK_RETURN(!rest_program.empty()); // to be filled with copies of the loop body goto_programt copies; @@ -234,7 +234,7 @@ void goto_unwindt::unwind( { goto_programt tmp_program; copy_segment(loop_head, loop_exit, tmp_program); - assert(!tmp_program.instructions.empty()); + CHECK_RETURN(!tmp_program.instructions.empty()); iteration_points[i]=--tmp_program.instructions.end(); @@ -312,7 +312,7 @@ void goto_unwindt::unwind( goto_programt::const_targett loop_head=i_it->get_target(); goto_programt::const_targett loop_exit=i_it; loop_exit++; - assert(loop_exit!=goto_program.instructions.end()); + CHECK_RETURN(loop_exit != goto_program.instructions.end()); unwind( function_id, goto_program, loop_head, loop_exit, *limit, unwind_strategy); diff --git a/src/goto-instrument/wmm/abstract_event.cpp b/src/goto-instrument/wmm/abstract_event.cpp index 41e8efb78f2..d240289c472 100644 --- a/src/goto-instrument/wmm/abstract_event.cpp +++ b/src/goto-instrument/wmm/abstract_event.cpp @@ -93,7 +93,7 @@ bool abstract_eventt::unsafe_pair_lwfence_param(const abstract_eventt &next, { } } - assert(false); + UNREACHABLE; /* unknown memory model */ return true; } @@ -156,7 +156,7 @@ bool abstract_eventt::unsafe_pair_asm(const abstract_eventt &next, { } } - assert(false); + UNREACHABLE; /* unknown memory model */ return true; } diff --git a/src/goto-instrument/wmm/abstract_event.h b/src/goto-instrument/wmm/abstract_event.h index bc5da6816bb..96e3034e044 100644 --- a/src/goto-instrument/wmm/abstract_event.h +++ b/src/goto-instrument/wmm/abstract_event.h @@ -170,7 +170,7 @@ class abstract_eventt:public graph_nodet case operationt::Lwfence: return "f"; case operationt::ASMfence: return "asm:"; } - assert(false); + UNREACHABLE; return "?"; } diff --git a/src/goto-instrument/wmm/cycle_collection.cpp b/src/goto-instrument/wmm/cycle_collection.cpp index a36ac99b851..403564f7289 100644 --- a/src/goto-instrument/wmm/cycle_collection.cpp +++ b/src/goto-instrument/wmm/cycle_collection.cpp @@ -70,7 +70,7 @@ void event_grapht::graph_explorert::collect_cycles( break; case Unknown: - assert(false); + UNREACHABLE; } if(order->empty()) @@ -494,7 +494,7 @@ bool event_grapht::graph_explorert::backtrack( mark[vertex]=false; } - assert(!point_stack.empty()); + DATA_INVARIANT(!point_stack.empty(), "element required"); point_stack.pop(); /* removes variable access */ @@ -542,7 +542,7 @@ bool event_grapht::graph_explorert::backtrack( if(!marked_stack.empty()) { - assert(marked_stack.top()==vertex); + DATA_INVARIANT(marked_stack.top() == vertex, "should match"); mark[vertex]=true; } else diff --git a/src/goto-instrument/wmm/event_graph.cpp b/src/goto-instrument/wmm/event_graph.cpp index 95e2a3712ba..5000107aceb 100644 --- a/src/goto-instrument/wmm/event_graph.cpp +++ b/src/goto-instrument/wmm/event_graph.cpp @@ -55,7 +55,7 @@ void event_grapht::print_rec_graph(std::ofstream &file, event_idt node_id, void event_grapht::print_graph() { - assert(!po_order.empty()); + PRECONDITION(!po_order.empty()); std::set visited; event_idt root=po_order.front(); std::ofstream file; @@ -1132,14 +1132,14 @@ std::string event_grapht::critical_cyclet::print_all( { std::string cycle; - assert(size() > 2); + PRECONDITION(size() > 2); /* removes all the internal events */ if(hide_internals) { critical_cyclet reduced(egraph, id); this->hide_internals(reduced); - assert(reduced.size() > 0); + CHECK_RETURN(reduced.size() > 0); cycle+=print_detail(reduced, map_id2var, map_var2id); cycle+=": "; cycle+=print_name(reduced, model); @@ -1169,7 +1169,7 @@ void event_grapht::critical_cyclet::hide_internals( break; prev_it=first_it; } - assert(first_it!=end()); + CHECK_RETURN(first_it != end()); reduced.push_back(*first_it); reduced_evts.insert(*first_it); @@ -1193,7 +1193,7 @@ void event_grapht::critical_cyclet::hide_internals( reduced_evts.insert(*cur_it); } for(; next_it!=end() && egraph[*next_it].is_fence(); ++next_it) {} - assert(next_it!=end()); + CHECK_RETURN(next_it != end()); if(reduced_evts.find(*next_it)==reduced_evts.end()) { reduced.push_back(*next_it); @@ -1210,7 +1210,7 @@ void event_grapht::critical_cyclet::hide_internals( const_iterator next_it=cur_it; ++next_it; - assert(next_it!=end()); + CHECK_RETURN(next_it != end()); if(cur.thread!=egraph[*next_it].thread) { @@ -1220,7 +1220,7 @@ void event_grapht::critical_cyclet::hide_internals( reduced_evts.insert(*cur_it); } for(; next_it!=end() && egraph[*next_it].is_fence(); ++next_it) {} - assert(next_it!=end()); + CHECK_RETURN(next_it != end()); if(reduced_evts.find(*next_it)==reduced_evts.end()) { reduced.push_back(*next_it); @@ -1234,7 +1234,7 @@ std::string event_grapht::critical_cyclet::print_name( const critical_cyclet &reduced, memory_modelt model) const { - assert(reduced.size()>=2); + PRECONDITION(reduced.size() >= 2); unsigned extra_fence_count=0; std::string name; @@ -1265,7 +1265,7 @@ std::string event_grapht::critical_cyclet::print_name( ++n_it; if(n_it==reduced.end()) { - assert(!wraparound); + INVARIANT(!wraparound, "no prior wraparound"); wraparound=true; first_done=true; ++extra_fence_count; @@ -1282,8 +1282,10 @@ std::string event_grapht::critical_cyclet::print_name( ++extra_fence_count; } const abstract_eventt &succ=egraph[*n_it]; - assert(succ.operation==abstract_eventt::operationt::Read || - succ.operation==abstract_eventt::operationt::Write); + DATA_INVARIANT( + succ.operation == abstract_eventt::operationt::Read || + succ.operation == abstract_eventt::operationt::Write, + "operation is read or write"); name += (model==Power?" Sync":" MFence"); name += (prev.variable==succ.variable?"s":"d") + prev.get_operation() + succ.get_operation(); @@ -1299,7 +1301,7 @@ std::string event_grapht::critical_cyclet::print_name( ++n_it; if(n_it==reduced.end()) { - assert(!wraparound); + INVARIANT(!wraparound, "no prior wraparound"); wraparound=true; first_done=true; ++extra_fence_count; @@ -1320,8 +1322,10 @@ std::string event_grapht::critical_cyclet::print_name( ++extra_fence_count; } const abstract_eventt &succ=egraph[*n_it]; - assert(succ.operation==abstract_eventt::operationt::Read || - succ.operation==abstract_eventt::operationt::Write); + DATA_INVARIANT( + succ.operation == abstract_eventt::operationt::Read || + succ.operation == abstract_eventt::operationt::Write, + "operation is read or write"); name += cand_name; name += (prev.variable==succ.variable?"s":"d") + prev.get_operation() + succ.get_operation(); @@ -1341,7 +1345,7 @@ std::string event_grapht::critical_cyclet::print_name( ++n_it; if(n_it==reduced.end()) { - assert(!wraparound); + INVARIANT(!wraparound, "no prior wraparound"); wraparound=true; first_done=true; ++extra_fence_count; @@ -1362,8 +1366,10 @@ std::string event_grapht::critical_cyclet::print_name( ++extra_fence_count; } const abstract_eventt &succ=egraph[*n_it]; - assert(succ.operation==abstract_eventt::operationt::Read || - succ.operation==abstract_eventt::operationt::Write); + DATA_INVARIANT( + succ.operation == abstract_eventt::operationt::Read || + succ.operation == abstract_eventt::operationt::Write, + "operation is read or write"); name += cand_name; name += (prev.variable==succ.variable?"s":"d") + prev.get_operation() + succ.get_operation(); @@ -1419,7 +1425,7 @@ std::string event_grapht::critical_cyclet::print_name( } else if(cur.variable!=ID_unknown && prev.variable!=ID_unknown) - assert(false); + UNREACHABLE; } prev_it=cur_it; @@ -1433,7 +1439,7 @@ std::string event_grapht::critical_cyclet::print_name( ++it) if(*it==' ') ++n_events; - assert(n_events==reduced.size()); + DATA_INVARIANT(n_events == reduced.size(), "number of events match"); return name; } @@ -1441,9 +1447,11 @@ std::string event_grapht::critical_cyclet::print_name( const abstract_eventt &first=egraph[reduced.front()]; const abstract_eventt &last=egraph[reduced.back()]; - assert(last.operation!=abstract_eventt::operationt::Fence && - last.operation!=abstract_eventt::operationt::Lwfence && - last.operation!=abstract_eventt::operationt::ASMfence); + DATA_INVARIANT( + last.operation != abstract_eventt::operationt::Fence && + last.operation != abstract_eventt::operationt::Lwfence && + last.operation != abstract_eventt::operationt::ASMfence, + "operation is not a fence"); if(first.operation==abstract_eventt::operationt::Fence || first.operation==abstract_eventt::operationt::Lwfence || @@ -1464,10 +1472,12 @@ std::string event_grapht::critical_cyclet::print_name( cand.fence_value()&1)) cand_name=(model==Power?" Sync":" MFence"); } - assert(it!=reduced.begin() && it!=reduced.end()); + CHECK_RETURN(it != reduced.begin() && it != reduced.end()); const abstract_eventt &succ=egraph[*it]; - assert(succ.operation==abstract_eventt::operationt::Read || - succ.operation==abstract_eventt::operationt::Write); + DATA_INVARIANT( + succ.operation == abstract_eventt::operationt::Read || + succ.operation == abstract_eventt::operationt::Write, + "operation is read or write"); name += cand_name; name += (last.variable==succ.variable?"s":"d") + last.get_operation() + succ.get_operation(); @@ -1520,7 +1530,7 @@ std::string event_grapht::critical_cyclet::print_name( } else if(last.variable!=ID_unknown && first.variable!=ID_unknown) - assert(false); + UNREACHABLE; #if 0 critical_cyclet::size_type n_events=extra_fence_count; diff --git a/src/goto-instrument/wmm/event_graph.h b/src/goto-instrument/wmm/event_graph.h index ca2e34b1ba3..5f4acaa338d 100644 --- a/src/goto-instrument/wmm/event_graph.h +++ b/src/goto-instrument/wmm/event_graph.h @@ -452,8 +452,8 @@ class event_grapht void add_po_edge(event_idt a, event_idt b) { - assert(a!=b); - assert(operator[](a).thread==operator[](b).thread); + PRECONDITION(a != b); + PRECONDITION(operator[](a).thread == operator[](b).thread); po_graph.add_edge(a, b); po_order.push_back(a); poUrfe_order.push_back(a); @@ -461,8 +461,8 @@ class event_grapht void add_po_back_edge(event_idt a, event_idt b) { - assert(a!=b); - assert(operator[](a).thread==operator[](b).thread); + PRECONDITION(a != b); + PRECONDITION(operator[](a).thread == operator[](b).thread); po_graph.add_edge(a, b); po_order.push_back(a); poUrfe_order.push_back(a); @@ -472,14 +472,14 @@ class event_grapht void add_com_edge(event_idt a, event_idt b) { - assert(a!=b); + PRECONDITION(a != b); com_graph.add_edge(a, b); poUrfe_order.push_back(a); } void add_undirected_com_edge(event_idt a, event_idt b) { - assert(a!=b); + PRECONDITION(a != b); add_com_edge(a, b); add_com_edge(b, a); } diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index e1673562649..3850c969da6 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -101,7 +101,7 @@ unsigned instrumentert::goto2graph_cfg( std::vector subgraph_index; num_sccs=egraph_alt.SCCs(subgraph_index); - assert(egraph_SCCs.empty()); + CHECK_RETURN(egraph_SCCs.empty()); egraph_SCCs.resize(num_sccs, std::set()); for(std::map::const_iterator it=map_vertex_gnode.begin(); @@ -949,7 +949,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign( <::const_iterator entry= instrumenter.map_vertex_gnode.find(id_it->second); - assert(entry!=instrumenter.map_vertex_gnode.end()); + CHECK_RETURN(entry != instrumenter.map_vertex_gnode.end()); egraph.add_com_edge(new_read_node, id_it->second); egraph_alt.add_edge(new_read_gnode, entry->second); egraph.add_com_edge(id_it->second, new_read_node); @@ -968,7 +968,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign( <::const_iterator entry= instrumenter.map_vertex_gnode.find(*id_it); - assert(entry!=instrumenter.map_vertex_gnode.end()); + CHECK_RETURN(entry != instrumenter.map_vertex_gnode.end()); egraph.add_com_edge(new_read_node, *id_it); egraph_alt.add_edge(new_read_gnode, entry->second); egraph.add_com_edge(*id_it, new_read_node); @@ -1059,7 +1059,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign( <::const_iterator entry= instrumenter.map_vertex_gnode.find(idr_it->second); - assert(entry!=instrumenter.map_vertex_gnode.end()); + CHECK_RETURN(entry != instrumenter.map_vertex_gnode.end()); egraph.add_com_edge(new_write_node, idr_it->second); egraph_alt.add_edge(new_write_gnode, entry->second); egraph.add_com_edge(idr_it->second, new_write_node); @@ -1078,7 +1078,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign( <::const_iterator entry= instrumenter.map_vertex_gnode.find(idw_it->second); - assert(entry!=instrumenter.map_vertex_gnode.end()); + CHECK_RETURN(entry != instrumenter.map_vertex_gnode.end()); egraph.add_com_edge(new_write_node, idw_it->second); egraph_alt.add_edge(new_write_gnode, entry->second); egraph.add_com_edge(idw_it->second, new_write_node); @@ -1097,7 +1097,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign( <::const_iterator entry= instrumenter.map_vertex_gnode.find(*id_it); - assert(entry!=instrumenter.map_vertex_gnode.end()); + CHECK_RETURN(entry != instrumenter.map_vertex_gnode.end()); egraph.add_com_edge(new_write_node, *id_it); egraph_alt.add_edge(new_write_gnode, entry->second); egraph.add_com_edge(*id_it, new_write_node); @@ -1116,7 +1116,7 @@ void instrumentert::cfg_visitort::visit_cfg_assign( <::const_iterator entry= instrumenter.map_vertex_gnode.find(*id_it); - assert(entry!=instrumenter.map_vertex_gnode.end()); + CHECK_RETURN(entry != instrumenter.map_vertex_gnode.end()); egraph.add_com_edge(new_write_node, *id_it); egraph_alt.add_edge(new_write_gnode, entry->second); egraph.add_com_edge(*id_it, new_write_node); @@ -1284,7 +1284,7 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet &cyc) if(thread_found) break; } - assert(current_po); + INVARIANT(current_po, "thread found"); const wmm_grapht::edgest &pos_cur=egraph.po_out(*e_it); const wmm_grapht::edgest &pos_next=egraph.po_out(*(++e_it)); diff --git a/src/goto-instrument/wmm/goto2graph.h b/src/goto-instrument/wmm/goto2graph.h index 7d778170dae..d9643cdeac0 100644 --- a/src/goto-instrument/wmm/goto2graph.h +++ b/src/goto-instrument/wmm/goto2graph.h @@ -409,10 +409,10 @@ class instrumentert /* sets rendering options */ void set_rendering_options(bool aligned, bool file, bool function) { + PRECONDITION(!file || !function); render_po_aligned = aligned; render_by_file = file; render_by_function = function; - assert(!render_by_file || !render_by_function); } /* prints outputs: diff --git a/src/goto-instrument/wmm/instrumenter_strategies.cpp b/src/goto-instrument/wmm/instrumenter_strategies.cpp index 11c582b717c..24b581c0486 100644 --- a/src/goto-instrument/wmm/instrumenter_strategies.cpp +++ b/src/goto-instrument/wmm/instrumenter_strategies.cpp @@ -46,7 +46,7 @@ void instrumentert::instrument_with_strategy(instrumentation_strategyt strategy) instrument_one_write_per_cycle_inserter(set_of_cycles); break; case my_events: - assert(false); + UNREACHABLE; } } else if(num_sccs!=0) @@ -71,7 +71,7 @@ void instrumentert::instrument_with_strategy(instrumentation_strategyt strategy) instrument_one_write_per_cycle_inserter(set_of_cycles_per_SCC[i]); break; case my_events: - assert(false); + UNREACHABLE; } } } diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 7e3c5ff5dd4..a66085357bc 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -431,8 +431,9 @@ void goto_convertt::do_cpp_new( const typet &return_type= code_type.return_type(); - assert(code_type.parameters().size()==1 || - code_type.parameters().size()==2); + DATA_INVARIANT( + code_type.parameters().size() == 1 || code_type.parameters().size() == 2, + "new has one or two parameters"); const symbolt &tmp_symbol = new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp); @@ -462,8 +463,9 @@ void goto_convertt::do_cpp_new( const typet &return_type=code_type.return_type(); - assert(code_type.parameters().size()==2 || - code_type.parameters().size()==3); + DATA_INVARIANT( + code_type.parameters().size() == 2 || code_type.parameters().size() == 3, + "placement new has two or three parameters"); const symbolt &tmp_symbol = new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp); diff --git a/src/json/json_parser.h b/src/json/json_parser.h index ed1b710bbf3..926a30e10bf 100644 --- a/src/json/json_parser.h +++ b/src/json/json_parser.h @@ -38,7 +38,7 @@ class json_parsert:public parsert void pop(jsont &dest) { - assert(!stack.empty()); + PRECONDITION(!stack.empty()); dest.swap(stack.top()); stack.pop(); } diff --git a/src/json/parser.y b/src/json/parser.y index 85df4c0ddfe..facaf48638d 100644 --- a/src/json/parser.y +++ b/src/json/parser.y @@ -26,10 +26,10 @@ extern int yyjsonleng; // really an int, not a size_t static std::string convert_TOK_STRING() { - assert(yyjsontext[0]=='"'); + PRECONDITION(yyjsontext[0]=='"'); std::size_t len=yyjsonleng; - assert(len>=2); - assert(yyjsontext[len-1]=='"'); + PRECONDITION(len>=2); + PRECONDITION(yyjsontext[len-1]=='"'); std::string result; result.reserve(len); for(char *p=yyjsontext+1; *p!='"' && *p!=0; p++) @@ -52,7 +52,9 @@ static std::string convert_TOK_STRING() // Character in hexadecimal Unicode representation, in the format // \uABCD, i.e. the following four digits are part of this character. char *last_hex_digit = p + 4; - assert(last_hex_digit < yyjsontext + len - 1); + INVARIANT( + last_hex_digit < yyjsontext + len - 1, + "all digits are in bounds"); std::string hex(++p, 4); result += codepoint_hex_to_utf8(hex); p = last_hex_digit; diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 8068cfe225d..c4b5a0a0956 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -810,7 +810,7 @@ void value_sett::get_value_set_rec( statement==ID_cpp_new_array) { PRECONDITION(suffix.empty()); - assert(expr_type.id()==ID_pointer); + PRECONDITION(expr_type.id() == ID_pointer); dynamic_object_exprt dynamic_object( to_pointer_type(expr_type).base_type()); @@ -1105,7 +1105,7 @@ void value_sett::dereference_rec( // remove pointer typecasts if(src.id()==ID_typecast) { - assert(src.type().id()==ID_pointer); + PRECONDITION(src.type().id() == ID_pointer); dereference_rec(to_typecast_expr(src).op(), dest); } diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index fdf9998e791..67d67a4a787 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -158,7 +158,7 @@ void value_set_fit::flatten_rec( #endif std::string identifier = id2string(e.identifier); - assert(seen.find(identifier + e.suffix)==seen.end()); + CHECK_RETURN(seen.find(identifier + e.suffix) == seen.end()); bool generalize_index = false; @@ -303,7 +303,7 @@ value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const const exprt &object = object_numbering[object_entry.first]; if(object.type().id()=="#REF#") { - assert(object.id()==ID_symbol); + DATA_INVARIANT(object.id() == ID_symbol, "reference to symbol required"); const irep_idt &ident = object.get(ID_identifier); valuest::const_iterator v_it = values.find(ident); @@ -630,7 +630,7 @@ void value_set_fit::get_value_set_rec( statement==ID_cpp_new_array) { PRECONDITION(suffix.empty()); - assert(expr.type().id()==ID_pointer); + PRECONDITION(expr.type().id() == ID_pointer); dynamic_object_exprt dynamic_object( to_pointer_type(expr.type()).base_type()); @@ -690,7 +690,7 @@ void value_set_fit::dereference_rec( // remove pointer typecasts if(src.id()==ID_typecast) { - assert(src.type().id()==ID_pointer); + PRECONDITION(src.type().id() == ID_pointer); dereference_rec(to_typecast_expr(src).op(), dest); } @@ -1018,7 +1018,8 @@ void value_set_fit::assign( if(rhs.id()==ID_struct || rhs.id()==ID_constant) { - assert(nosecond; for(index_sett::const_iterator it1= @@ -389,18 +389,20 @@ mp_integer boolbvt::get_value( std::size_t offset, std::size_t width) { + PRECONDITION(offset + width <= bv.size()); + mp_integer value=0; mp_integer weight=1; for(std::size_t bit_nr=offset; bit_nr(expr); } diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp index 08b469c40d5..0df4bf16267 100644 --- a/src/xmllang/graphml.cpp +++ b/src/xmllang/graphml.cpp @@ -54,7 +54,7 @@ static bool build_graph_rec( e_it!=xml.elements.end(); e_it++) { - assert(e_it->name=="data"); + DATA_INVARIANT(e_it->name == "data", "expected data node"); if(e_it->get_attribute("key")=="violation" && e_it->data=="true") @@ -143,7 +143,7 @@ static bool build_graph( graphmlt &dest, graphmlt::node_indext &entry) { - assert(dest.empty()); + PRECONDITION(dest.empty()); name_mapt name_to_node; std::map > defaults; @@ -156,6 +156,7 @@ static bool build_graph( defaults, dest, entrynode); + CHECK_RETURN(!entrynode.empty()); for(std::size_t i=0; !err && isecond; return err;