cprover
|
Go to the source code of this file.
Classes | |
class | codet |
A statement in a programming language. More... | |
class | code_blockt |
Sequential composition. More... | |
class | code_skipt |
Skip. More... | |
class | code_assignt |
Assignment. More... | |
class | code_declt |
A declaration of a local variable. More... | |
class | code_deadt |
A removal of a local variable. More... | |
class | code_assumet |
An assumption, which must hold in subsequent code. More... | |
class | code_assertt |
A non-fatal assertion, which checks a condition then permits execution to continue. More... | |
class | code_ifthenelset |
An if-then-else. More... | |
class | code_switcht |
A ‘switch’ instruction. More... | |
class | code_whilet |
A ‘while’ instruction. More... | |
class | code_dowhilet |
A ‘do while’ instruction. More... | |
class | code_fort |
A ‘for’ instruction. More... | |
class | code_gotot |
A ‘goto’ instruction. More... | |
class | code_function_callt |
A function call. More... | |
class | code_returnt |
Return from a function. More... | |
class | code_labelt |
A label for branch targets. More... | |
class | code_switch_caset |
A switch-case. More... | |
class | code_breakt |
A break for ‘for’ and ‘while’ loops. More... | |
class | code_continuet |
A continue for ‘for’ and ‘while’ loops. More... | |
class | code_asmt |
An inline assembler statement. More... | |
class | code_expressiont |
An expression statement. More... | |
class | side_effect_exprt |
An expression containing a side effect. More... | |
class | side_effect_expr_nondett |
A side effect that returns a non-deterministically chosen value. More... | |
class | side_effect_expr_function_callt |
A function call side effect. More... | |
class | side_effect_expr_throwt |
A side effect that throws an exception. More... | |
class | code_push_catcht |
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ... More... | |
class | code_push_catcht::exception_list_entryt |
class | code_pop_catcht |
Pops an exception handler from the stack of active handlers (i.e. More... | |
class | code_landingpadt |
A statement that catches an exception, assigning the exception in flight to an expression (e.g. More... | |
class | code_try_catcht |
A try/catch block. More... | |
Namespaces | |
detail | |
|
inline |
Definition at line 1198 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 429 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 230 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 382 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 157 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 1123 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 1153 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 334 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 281 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 701 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 1245 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 777 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 901 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 827 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 512 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 1021 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 1685 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 1640 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 1609 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 955 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 187 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 1091 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 575 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 1757 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 638 of file std_code.h.
References detail::can_cast_code_impl().
|
inline |
Definition at line 67 of file std_code.h.
|
inline |
Definition at line 1465 of file std_code.h.
References detail::can_cast_side_effect_expr_impl().
|
inline |
Definition at line 1370 of file std_code.h.
References detail::can_cast_side_effect_expr_impl().
Referenced by is_nondet_pointer().
|
inline |
Definition at line 1510 of file std_code.h.
References detail::can_cast_side_effect_expr_impl().
|
inline |
Definition at line 1318 of file std_code.h.
code_blockt create_fatal_assertion | ( | const exprt & | condition, |
const source_locationt & | source_location | ||
) |
Create a fatal assertion, which checks a condition and then halts if it does not hold.
Equivalent to ASSERT(condition); ASSUME(condition)
.
Source level assertions should probably use this, whilst checks that are normally non-fatal at runtime, such as integer overflows, should use code_assertt by itself.
condition | condition to assert |
source_location | source location to attach to the generated code; conventionally this should have comment and property_class fields set to indicate the nature of the assertion. |
Definition at line 110 of file std_code.cpp.
References exprt::add_source_location(), exprt::copy_to_operands(), loc, and exprt::operands().
Referenced by java_bytecode_instrumentt::check_arithmetic_exception(), java_bytecode_instrumentt::check_array_access(), java_bytecode_instrumentt::check_array_length(), java_bytecode_instrumentt::check_class_cast(), and java_bytecode_instrumentt::check_null_dereference().
Definition at line 75 of file std_code.h.
References irept::id().
Referenced by allocate_dynamic_object_with_decl(), code_blockt::append(), invariant_sett::apply_code(), value_sett::apply_code_rec(), code_switcht::body(), code_whilet::body(), code_dowhilet::body(), code_fort::body(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_code_block(), dump_ct::cleanup_expr(), dump_ct::cleanup_harness(), goto_convertt::convert(), goto_convertt::convert_block(), jsil_convertt::convert_code(), expr2ct::convert_code_block(), expr2ct::convert_code_decl_block(), expr2ct::convert_code_switch(), goto_convertt::convert_cpp_delete(), goto_convertt::convert_CPROVER_try_catch(), goto_convertt::convert_CPROVER_try_finally(), goto_convertt::convert_dowhile(), goto_convertt::convert_for(), goto_convert_functionst::convert_function(), cpp_typecheckt::convert_function(), goto_convertt::convert_gcc_switch_case_range(), goto_program2codet::convert_goto_switch(), goto_program2codet::convert_goto_while(), java_bytecode_convert_methodt::convert_instructions(), goto_convertt::convert_label(), goto_program2codet::convert_labels(), goto_convertt::convert_msc_try_except(), goto_convertt::convert_msc_try_finally(), expr2ct::convert_statement_expression(), convert_threadblock(), goto_convertt::convert_try_catch(), expr2javat::convert_with_precedence(), expr2ct::convert_with_precedence(), copy_parent(), cpp_typecheckt::cpp_constructor(), goto_convertt::cpp_new_initializer(), goto_convertt::do_printf(), find_block_position_rec(), code_blockt::find_last_statement(), codet::first_statement(), format_rec(), ci_lazy_methodst::gather_virtual_callsites(), require_goto_statements::get_all_statements(), code_try_catcht::get_catch_code(), code_try_catcht::get_catch_decl(), java_bytecode_convert_methodt::get_or_create_block_for_pcrange(), goto_convert(), has_labels(), insert_at_label(), mm2cppt::instruction2cpp(), java_bytecode_instrumentt::instrument_code(), instrument_synchronized_code(), java_bytecode_instrument(), java_bytecode_instrument_symbol(), java_static_lifetime_init(), codet::last_statement(), model_argc_argv(), monitor_exits(), move_label_ifthenelse(), cpp_typecheckt::move_member_initializers(), mm2cppt::operator()(), jsil_convertt::operator()(), goto_convertt::remove_assignment(), goto_convertt::remove_statement_expression(), goto_convertt::remove_temporary_object(), java_bytecode_convert_methodt::replace_goto_target(), static_lifetime_init(), jsil_typecheckt::typecheck_block(), c_typecheck_baset::typecheck_block(), java_bytecode_typecheckt::typecheck_code(), c_typecheck_baset::typecheck_code(), cpp_typecheckt::typecheck_compound_declarator(), java_bytecode_typecheckt::typecheck_expr(), c_typecheck_baset::typecheck_expr_operands(), c_typecheck_baset::typecheck_for(), c_typecheck_baset::typecheck_function_body(), c_typecheck_baset::typecheck_gcc_switch_case_range(), cpp_typecheckt::typecheck_ifthenelse(), jsil_typecheckt::typecheck_non_type_symbol(), c_typecheck_baset::typecheck_side_effect_statement_expression(), c_typecheck_baset::typecheck_start_thread(), cpp_typecheckt::typecheck_switch(), cpp_typecheckt::typecheck_try_catch(), cpp_typecheckt::typecheck_while(), and yyjsilparse().
Definition at line 81 of file std_code.h.
References irept::id().
Definition at line 1206 of file std_code.h.
References codet::get_statement().
Referenced by goto_convertt::convert(), expr2ct::convert_code(), remove_asmt::process_instruction(), and c_typecheck_baset::typecheck_asm().
Definition at line 1212 of file std_code.h.
References codet::get_statement().
|
inline |
Definition at line 437 of file std_code.h.
References codet::get_statement().
Referenced by goto_convertt::convert(), and java_bytecode_instrumentt::instrument_code().
|
inline |
Definition at line 443 of file std_code.h.
References codet::get_statement().
|
inline |
Definition at line 240 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by string_abstractiont::abstract_assign(), string_abstractiont::abstract_char_assign(), string_abstractiont::abstract_pointer_assign(), overflow_instrumentert::add_overflow_checks(), local_may_aliast::build(), local_bitvector_analysist::build(), check_and_replace_target(), cone_of_influencet::cone_of_influence(), polynomial_acceleratort::cone_of_influence(), goto_convertt::convert(), goto_program2codet::convert_assign(), goto_program2codet::convert_assign_varargs(), jsil_convertt::convert_code(), expr2ct::convert_code(), goto_program2codet::convert_decl(), goto_convertt::convert_init(), interpretert::execute_assign(), expressions_read(), expressions_written(), filter_out(), acceleration_utilst::find_modified(), require_goto_statements::find_pointer_assignments(), require_goto_statements::find_struct_component_assignments(), require_goto_statements::find_this_component_assignment(), scratch_programt::fix_types(), format_rec(), acceleration_utilst::gather_array_assignments(), get_modifies(), function_modifiest::get_modifies(), havoc_loopst::get_modifies(), goto_checkt::goto_check(), goto_rw(), implicit(), goto_inlinet::insert_function_body(), concurrency_instrumentationt::instrument(), escape_analysist::instrument(), java_bytecode_instrumentt::instrument_code(), is_assignment_from(), mm_io(), mutex_init_instrumentation(), nondet_static(), nondet_volatile(), does_remove_constt::operator()(), replace_callst::operator()(), acceleration_utilst::precondition(), polynomial_acceleratort::precondition(), print_global_state_size(), goto_convertt::remove_assignment(), goto_convertt::remove_statement_expression(), constant_propagator_ait::replace(), remove_returnst::restore_returns(), goto_program2codet::scan_for_varargs(), slice_global_inits(), static_simplifier(), goto_symext::symex_step(), constant_propagator_domaint::transform(), custom_bitvector_domaint::transform(), escape_domaint::transform(), global_may_alias_domaint::transform(), interval_domaint::transform(), invariant_set_domaint::transform(), java_bytecode_typecheckt::typecheck_code(), jsil_typecheckt::typecheck_code(), remove_returnst::undo_function_calls(), and wp().
|
inline |
Definition at line 246 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 390 of file std_code.h.
References codet::get_statement().
Referenced by value_sett::apply_code_rec(), goto_convertt::convert(), and wp().
|
inline |
Definition at line 396 of file std_code.h.
References codet::get_statement().
|
inline |
Definition at line 165 of file std_code.h.
References codet::get_statement().
Referenced by java_bytecode_instrumentt::add_expr_instrumentation(), goto_convertt::convert(), expr2ct::convert_code(), goto_convert_functionst::convert_function(), java_bytecode_convert_methodt::convert_instructions(), expr2ct::convert_statement_expression(), goto_convertt::convert_switch(), find_block_position_rec(), format_rec(), java_bytecode_convert_methodt::get_or_create_block_for_pcrange(), instrument_synchronized_code(), java_static_lifetime_init(), move_label_ifthenelse(), java_bytecode_instrumentt::prepend_instrumentation(), goto_convertt::remove_statement_expression(), static_lifetime_init(), jsil_declarationt::to_symbol(), c_typecheck_baset::typecheck_for(), c_typecheck_baset::typecheck_side_effect_statement_expression(), cpp_typecheckt::typecheck_try_catch(), and yyjsilparse().
|
inline |
Definition at line 171 of file std_code.h.
References codet::get_statement().
|
inline |
Definition at line 1131 of file std_code.h.
References codet::get_statement().
Referenced by goto_convertt::convert().
|
inline |
Definition at line 1137 of file std_code.h.
References codet::get_statement().
|
inline |
Definition at line 1161 of file std_code.h.
References codet::get_statement().
Referenced by goto_convertt::convert().
|
inline |
Definition at line 1167 of file std_code.h.
References codet::get_statement().
|
inline |
Definition at line 344 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by local_may_aliast::build(), local_bitvector_analysist::build(), goto_program2codet::build_dead_map(), goto_rw(), escape_analysist::instrument(), full_slicert::operator()(), constant_propagator_domaint::transform(), custom_bitvector_domaint::transform(), global_may_alias_domaint::transform(), escape_domaint::transform(), interval_domaint::transform(), and rd_range_domaint::transform_dead().
|
inline |
Definition at line 350 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 291 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by uninitializedt::add_assertions(), localst::build(), local_may_aliast::build(), local_bitvector_analysist::build(), goto_convertt::convert(), goto_program2codet::convert_decl(), string_abstractiont::declare_define_locals(), code_try_catcht::get_catch_decl(), goto_rw(), remove_exceptionst::instrument_exceptions(), full_slicert::operator()(), require_goto_statements::require_declaration_of_name(), constant_propagator_domaint::transform(), custom_bitvector_domaint::transform(), escape_domaint::transform(), global_may_alias_domaint::transform(), uninitialized_domaint::transform(), interval_domaint::transform(), cpp_typecheckt::typecheck_try_catch(), and wp().
|
inline |
Definition at line 298 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 711 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by goto_program2codet::cleanup_code(), expr2ct::convert_code(), and c_typecheck_baset::typecheck_code().
|
inline |
Definition at line 718 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 1255 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by goto_convertt::convert(), java_bytecode_instrumentt::instrument_code(), is_skip(), and goto_convertt::remove_statement_expression().
|
inline |
Definition at line 1262 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Definition at line 787 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by goto_convertt::convert(), and expr2ct::convert_code().
Definition at line 794 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 909 of file std_code.h.
References codet::get_statement().
Referenced by string_abstractiont::abstract_function_call(), code_contractst::apply_contract(), local_may_aliast::build(), local_bitvector_analysist::build(), check_and_replace_target(), goto_program2codet::cleanup_code(), dump_ct::cleanup_expr(), dump_ct::cleanup_harness(), goto_checkt::collect_allocations(), _rw_set_loct::compute(), compute_called_functions(), cfg_baset< cfg_nodet >::compute_edges_function_call(), procedure_local_cfg_baset< nodet, goto_programt, goto_programt::targett >::compute_edges_function_call(), goto_convertt::convert(), expr2javat::convert_code(), expr2ct::convert_code(), goto_program2codet::convert_decl(), goto_program2codet::convert_start_thread(), convert_threadblock(), goto_program_dereferencet::dereference_instruction(), string_instrumentationt::do_function_call(), flow_insensitive_analysis_baset::do_function_call(), parameter_assignmentst::do_function_calls(), remove_returnst::do_function_calls(), interpretert::execute_function_call(), expressions_read(), expressions_written(), require_goto_statements::find_function_calls(), find_used_functions(), forall_callsites(), remove_exceptionst::function_or_callees_may_throw(), ci_lazy_methodst::gather_virtual_callsites(), goto_inlinet::get_call(), get_modifies(), function_modifiest::get_modifies(), havoc_loopst::get_modifies(), get_nondet_instruction_info(), flow_insensitive_abstract_domain_baset::get_return_lhs(), static_analysis_baset::get_return_lhs(), goto_checkt::goto_check(), goto_rw(), concurrency_instrumentationt::instrument(), taint_analysist::instrument(), cover_cover_instrumentert::instrument(), java_bytecode_instrumentt::instrument_code(), remove_exceptionst::instrument_function_call(), instrument_preconditions(), is_fence(), is_lwfence(), remove_calls_no_bodyt::is_opaque_function_call(), list_calls_and_arguments(), model_argc_argv(), nondet_static(), nondet_volatile(), remove_calls_no_bodyt::operator()(), replace_callst::operator()(), check_call_sequencet::operator()(), remove_function_pointerst::remove_function_pointer(), remove_function_pointerst::remove_function_pointers(), remove_virtual_functionst::remove_virtual_function(), remove_virtual_functionst::remove_virtual_functions(), constant_propagator_ait::replace(), show_call_sequences(), splice_call(), static_simplifier(), goto_symext::symex_step(), thread_exit_instrumentation(), constant_propagator_domaint::transform(), uncaught_exceptions_domaint::transform(), custom_bitvector_domaint::transform(), escape_domaint::transform(), interval_domaint::transform(), value_set_domain_fivrt::transform(), value_set_domain_fivrnst::transform(), value_set_domain_fit::transform(), rd_range_domaint::transform(), rd_range_domaint::transform_end_function(), rd_range_domaint::transform_function_call(), java_bytecode_typecheckt::typecheck_code(), jsil_typecheckt::typecheck_code(), c_typecheck_baset::typecheck_side_effect_statement_expression(), jsil_typecheckt::typecheck_try_catch(), undefined_function_abort_path(), remove_returnst::undo_function_calls(), flow_insensitive_analysis_baset::visit(), static_analysis_baset::visit(), ai_baset::visit(), instrumentert::cfg_visitort::visit_cfg_function_call(), and shared_bufferst::cfg_visitort::weak_memory().
|
inline |
Definition at line 915 of file std_code.h.
References codet::get_statement().
|
inline |
Definition at line 837 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by goto_convertt::convert(), java_bytecode_convert_methodt::replace_goto_target(), and c_typecheck_baset::typecheck_code().
|
inline |
Definition at line 844 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 522 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by goto_program2codet::cleanup_code_ifthenelse(), goto_convertt::convert(), expr2ct::convert_code(), goto_program2codet::convert_goto_while(), java_bytecode_instrumentt::instrument_code(), java_bytecode_typecheckt::typecheck_code(), jsil_typecheckt::typecheck_code(), and c_typecheck_baset::typecheck_code().
|
inline |
Definition at line 529 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 1031 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by goto_program2codet::cleanup_code(), goto_convertt::convert(), expr2ct::convert_code(), java_bytecode_convert_methodt::convert_instructions(), goto_program2codet::convert_labels(), java_bytecode_convert_methodt::get_or_create_block_for_pcrange(), insert_at_label(), java_bytecode_instrumentt::instrument_code(), move_label_ifthenelse(), java_bytecode_typecheckt::typecheck_code(), jsil_typecheckt::typecheck_code(), and c_typecheck_baset::typecheck_code().
|
inline |
Definition at line 1037 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inlinestatic |
Definition at line 1693 of file std_code.h.
References codet::get_statement().
Referenced by expr2javat::convert_with_precedence(), remove_exceptionst::instrument_exception_handler(), and goto_programt::output_instruction().
|
inlinestatic |
Definition at line 1699 of file std_code.h.
References codet::get_statement().
|
inlinestatic |
Definition at line 1648 of file std_code.h.
References codet::get_statement().
|
inlinestatic |
Definition at line 1654 of file std_code.h.
References codet::get_statement().
|
inlinestatic |
Definition at line 1617 of file std_code.h.
References codet::get_statement().
Referenced by finish_catch_push_targets(), and remove_exceptionst::instrument_exceptions().
|
inlinestatic |
Definition at line 1623 of file std_code.h.
References codet::get_statement().
|
inline |
Definition at line 963 of file std_code.h.
References codet::get_statement().
Referenced by check_and_replace_target(), goto_convertt::convert(), expr2ct::convert_code_return(), goto_program2codet::convert_return(), expressions_read(), goto_rw(), is_return_with_variable(), goto_symext::return_assignment(), and jsil_typecheckt::typecheck_code().
|
inline |
Definition at line 969 of file std_code.h.
References codet::get_statement().
|
inline |
Definition at line 585 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by goto_convertt::convert(), java_bytecode_instrumentt::instrument_code(), java_bytecode_typecheckt::typecheck_code(), and c_typecheck_baset::typecheck_code().
|
inline |
Definition at line 592 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 1101 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by goto_convertt::convert(), expr2ct::convert_code(), goto_program2codet::convert_goto_switch(), and c_typecheck_baset::typecheck_code().
|
inline |
Definition at line 1107 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 1767 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by jsil_typecheckt::typecheck_code().
|
inline |
Definition at line 1773 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 648 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by goto_convertt::convert(), expr2ct::convert_code(), and c_typecheck_baset::typecheck_code().
|
inline |
Definition at line 655 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 1326 of file std_code.h.
References irept::id().
Referenced by approximate_nondet_rec(), goto_convertt::clean_expr(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_expr(), goto_convertt::convert_assign(), goto_program2codet::convert_assign_varargs(), jsil_convertt::convert_code(), goto_program2codet::convert_return(), interpretert::evaluate(), interpretert::execute_assign(), local_may_aliast::get_rec(), local_bitvector_analysist::get_rec(), has_nondet(), java_bytecode_instrumentt::instrument_expr(), constant_propagator_domaint::valuest::is_constant(), remove_java_newt::lower_java_new(), require_expr::require_side_effect_expr(), require_goto_statements::require_struct_array_component_assignment(), goto_program2codet::scan_for_varargs(), goto_symext::symex_assign(), to_side_effect_expr_nondet(), java_bytecode_typecheckt::typecheck_expr(), c_typecheck_baset::typecheck_expr_main(), and c_typecheck_baset::typecheck_expr_pointer_arithmetic().
|
inline |
Definition at line 1332 of file std_code.h.
References irept::id().
|
inline |
Definition at line 1474 of file std_code.h.
References irept::get(), and irept::id().
Referenced by goto_convertt::clean_expr(), goto_program2codet::cleanup_code(), jsil_convertt::convert_code(), expr2ct::convert_with_precedence(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::typecheck_cast_expr(), and c_typecheck_baset::typecheck_expr_side_effect().
|
inline |
Definition at line 1482 of file std_code.h.
References irept::get(), and irept::id().
|
inline |
Definition at line 1378 of file std_code.h.
References to_side_effect_expr().
Referenced by insert_nondet_init_code().
|
inline |
Definition at line 1385 of file std_code.h.
References to_side_effect_expr().
|
inline |
Definition at line 1518 of file std_code.h.
References irept::get(), and irept::id().
Referenced by jsil_typecheckt::typecheck_expr_main().
|
inline |
Definition at line 1525 of file std_code.h.
References irept::get(), and irept::id().
|
inline |
Definition at line 235 of file std_code.h.
References validate_operands().
|
inline |
Definition at line 286 of file std_code.h.
References validate_operands().
|
inline |
Definition at line 339 of file std_code.h.
References validate_operands().
|
inline |
Definition at line 517 of file std_code.h.
References validate_operands().
|
inline |
Definition at line 580 of file std_code.h.
References validate_operands().
|
inline |
Definition at line 643 of file std_code.h.
References validate_operands().
|
inline |
Definition at line 706 of file std_code.h.
References validate_operands().
|
inline |
Definition at line 782 of file std_code.h.
References validate_operands().
|
inline |
Definition at line 832 of file std_code.h.
References validate_operands().
|
inline |
Definition at line 1026 of file std_code.h.
References validate_operands().
|
inline |
Definition at line 1096 of file std_code.h.
References validate_operands().
|
inline |
Definition at line 1250 of file std_code.h.
References validate_operands().
|
inline |
Definition at line 1762 of file std_code.h.
References validate_operands().