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. More... | |
class | code_assertt |
An assertion. 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 | side_effect_expr_catcht |
A side effect that pushes/pops a catch handler. More... | |
class | code_try_catcht |
A try/catch block. More... | |
Definition at line 49 of file std_code.h.
References irept::id().
Referenced by code_blockt::append(), invariant_sett::apply_code(), value_sett::apply_code(), code_switcht::body(), code_whilet::body(), code_dowhilet::body(), code_fort::body(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_code_block(), goto_program2codet::cleanup_code_ifthenelse(), dump_ct::cleanup_expr(), goto_convertt::convert(), goto_convertt::convert_block(), goto_convertt::convert_bp_enforce(), jsil_convertt::convert_code(), expr2ct::convert_code_block(), expr2ct::convert_code_decl_block(), expr2ct::convert_code_ifthenelse(), 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_if(), goto_program2codet::convert_goto_switch(), goto_program2codet::convert_goto_while(), goto_convertt::convert_ifthenelse(), 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(), goto_program2codet::convert_start_thread(), goto_convertt::convert_start_thread(), expr2ct::convert_statement_expression(), goto_convertt::convert_switch(), goto_convertt::convert_try_catch(), expr2ct::convert_with_precedence(), copy_parent(), cpp_typecheckt::cpp_constructor(), goto_convertt::cpp_new_initializer(), goto_program_dereferencet::dereference_instruction(), flow_insensitive_analysis_baset::do_function_call(), goto_convertt::do_printf(), find_block_position_rec(), code_blockt::find_last_statement(), find_used_functions(), codet::first_statement(), gather_virtual_callsites(), code_try_catcht::get_catch_code(), code_try_catcht::get_catch_decl(), java_bytecode_convert_methodt::get_or_create_block_for_pcrange(), flow_insensitive_abstract_domain_baset::get_return_lhs(), goto_convert(), has_labels(), insert_at_label(), mm2cppt::instruction2cpp(), is_empty(), java_static_lifetime_init(), codet::last_statement(), model_argc_argv(), move_label_ifthenelse(), cpp_typecheckt::move_member_initializers(), mm2cppt::operator()(), jsil_convertt::operator()(), memory_model_tsot::program_order(), goto_convertt::remove_assignment(), goto_convertt::remove_statement_expression(), goto_convertt::remove_temporary_object(), java_bytecode_convert_methodt::replace_goto_target(), static_lifetime_init(), goto_symext::symex_dead(), goto_symext::symex_decl(), goto_symext::symex_other(), jsil_typecheckt::typecheck_block(), c_typecheck_baset::typecheck_block(), java_bytecode_typecheckt::typecheck_code(), c_typecheck_baset::typecheck_code(), 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(), jsil_typecheckt::typecheck_ifthenelse(), c_typecheck_baset::typecheck_ifthenelse(), 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(), flow_insensitive_analysis_baset::visit(), and yyjsilparse().
Definition at line 55 of file std_code.h.
References irept::id().
Definition at line 943 of file std_code.h.
References codet::get_statement().
Referenced by goto_convertt::convert(), expr2ct::convert_code(), is_empty(), remove_asmt::process_instruction(), and c_typecheck_baset::typecheck_asm().
Definition at line 949 of file std_code.h.
References codet::get_statement().
|
inline |
Definition at line 336 of file std_code.h.
References codet::get_statement().
Referenced by goto_convertt::convert(), and is_empty().
|
inline |
Definition at line 342 of file std_code.h.
References codet::get_statement().
|
inline |
Definition at line 178 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(), 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(), scratch_programt::fix_types(), 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(), is_empty(), mm_io(), mutex_init_instrumentation(), nondet_static(), nondet_volatile(), path_symext::operator()(), does_remove_constt::operator()(), acceleration_utilst::precondition(), polynomial_acceleratort::precondition(), const_function_pointer_propagationt::propagate(), 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(), goto_symext::symex_step(), constant_propagator_domaint::transform(), custom_bitvector_domaint::transform(), global_may_alias_domaint::transform(), escape_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 184 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 298 of file std_code.h.
References codet::get_statement().
Referenced by value_sett::apply_code(), goto_convertt::convert(), is_empty(), and wp().
|
inline |
Definition at line 304 of file std_code.h.
References codet::get_statement().
|
inline |
Definition at line 120 of file std_code.h.
References codet::get_statement().
Referenced by goto_convertt::convert(), expr2ct::convert_code(), goto_convert_functionst::convert_function(), java_bytecode_convert_methodt::convert_instructions(), expr2ct::convert_statement_expression(), find_block_position_rec(), java_bytecode_convert_methodt::get_or_create_block_for_pcrange(), is_empty(), java_static_lifetime_init(), move_label_ifthenelse(), 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 126 of file std_code.h.
References codet::get_statement().
|
inline |
Definition at line 884 of file std_code.h.
References codet::get_statement().
Referenced by goto_convertt::convert(), and is_empty().
|
inline |
Definition at line 890 of file std_code.h.
References codet::get_statement().
|
inline |
Definition at line 906 of file std_code.h.
References codet::get_statement().
Referenced by goto_convertt::convert(), and is_empty().
|
inline |
Definition at line 912 of file std_code.h.
References codet::get_statement().
|
inline |
Definition at line 260 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 266 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 218 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(), is_empty(), path_symext::operator()(), full_slicert::operator()(), constant_propagator_domaint::transform(), custom_bitvector_domaint::transform(), global_may_alias_domaint::transform(), escape_domaint::transform(), uninitialized_domaint::transform(), interval_domaint::transform(), cpp_typecheckt::typecheck_try_catch(), and wp().
|
inline |
Definition at line 225 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 531 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 538 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 981 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by goto_convertt::convert(), is_empty(), is_skip(), and goto_convertt::remove_statement_expression().
|
inline |
Definition at line 988 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Definition at line 597 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by goto_convertt::convert(), expr2ct::convert_code(), and is_empty().
Definition at line 604 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 700 of file std_code.h.
References codet::get_statement().
Referenced by string_abstractiont::abstract_function_call(), call_grapht::add(), const_function_pointer_propagationt::arg_stackt::add_args(), code_contractst::apply_contract(), local_may_aliast::build(), local_bitvector_analysist::build(), goto_program2codet::cleanup_code(), dump_ct::cleanup_expr(), 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(), 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(), path_searcht::drop_state(), const_function_pointer_propagationt::dup_caller_and_inline_callee(), interpretert::execute_function_call(), expressions_read(), expressions_written(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), find_used_functions(), gather_virtual_callsites(), goto_inlinet::get_call(), get_modifies(), function_modifiest::get_modifies(), havoc_loopst::get_modifies(), 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(), instrument_cover_goals(), remove_exceptionst::instrument_function_call(), is_empty(), is_fence(), is_lwfence(), list_calls_and_arguments(), nondet_static(), nondet_volatile(), path_symext::operator()(), check_call_sequencet::operator()(), const_function_pointer_propagationt::propagate(), 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(), replace_async(), show_call_sequences(), goto_symext::symex_step(), thread_exit_instrumentation(), constant_propagator_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(), value_set_domaint::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 706 of file std_code.h.
References codet::get_statement().
|
inline |
Definition at line 636 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by java_bytecode_convert_methodt::replace_goto_target(), and c_typecheck_baset::typecheck_code().
|
inline |
Definition at line 643 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 396 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(), is_empty(), java_bytecode_typecheckt::typecheck_code(), jsil_typecheckt::typecheck_code(), and c_typecheck_baset::typecheck_code().
|
inline |
Definition at line 403 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 803 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(), is_empty(), move_label_ifthenelse(), java_bytecode_typecheckt::typecheck_code(), jsil_typecheckt::typecheck_code(), and c_typecheck_baset::typecheck_code().
|
inline |
Definition at line 809 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 746 of file std_code.h.
References codet::get_statement().
Referenced by goto_convertt::convert(), expr2ct::convert_code_return(), goto_program2codet::convert_return(), expressions_read(), goto_rw(), is_empty(), goto_symext::return_assignment(), and jsil_typecheckt::typecheck_code().
|
inline |
Definition at line 752 of file std_code.h.
References codet::get_statement().
|
inline |
Definition at line 441 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by goto_convertt::convert(), is_empty(), java_bytecode_typecheckt::typecheck_code(), and c_typecheck_baset::typecheck_code().
|
inline |
Definition at line 448 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 862 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(), is_empty(), and c_typecheck_baset::typecheck_code().
|
inline |
Definition at line 868 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 1210 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by jsil_typecheckt::typecheck_code().
|
inline |
Definition at line 1216 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 486 of file std_code.h.
References codet::get_statement(), and exprt::operands().
Referenced by goto_convertt::convert(), expr2ct::convert_code(), is_empty(), and c_typecheck_baset::typecheck_code().
|
inline |
Definition at line 493 of file std_code.h.
References codet::get_statement(), and exprt::operands().
|
inline |
Definition at line 1023 of file std_code.h.
References irept::id().
Referenced by approximate_nondet_rec(), path_symext::assign(), 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(), local_may_aliast::get_rec(), local_bitvector_analysist::get_rec(), has_nondet(), path_symex_statet::instantiate_rec(), constant_propagator_domaint::valuest::is_constant(), is_empty(), goto_program2codet::scan_for_varargs(), goto_symext::symex_assign(), java_bytecode_typecheckt::typecheck_expr(), c_typecheck_baset::typecheck_expr_main(), and c_typecheck_baset::typecheck_expr_pointer_arithmetic().
|
inline |
Definition at line 1029 of file std_code.h.
References irept::id().
|
inlinestatic |
Definition at line 1143 of file std_code.h.
References irept::get(), and irept::id().
|
inlinestatic |
Definition at line 1150 of file std_code.h.
References irept::get(), and irept::id().
|
inline |
Definition at line 1083 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::cpp_destructor(), cpp_typecheckt::typecheck_cast_expr(), and c_typecheck_baset::typecheck_expr_side_effect().
|
inline |
Definition at line 1091 of file std_code.h.
References irept::get(), and irept::id().
|
inline |
Definition at line 1114 of file std_code.h.
References irept::get(), and irept::id().
Referenced by jsil_typecheckt::typecheck_expr_main().
|
inline |
Definition at line 1121 of file std_code.h.
References irept::get(), and irept::id().