cprover
|
A function call. More...
#include <std_code.h>
Public Types | |
typedef exprt::operandst | argumentst |
![]() | |
typedef std::vector< exprt > | operandst |
![]() | |
typedef std::vector< irept > | subt |
typedef std::map< irep_namet, irept > | named_subt |
Public Member Functions | |
code_function_callt () | |
exprt & | lhs () |
const exprt & | lhs () const |
exprt & | function () |
const exprt & | function () const |
argumentst & | arguments () |
const argumentst & | arguments () const |
![]() | |
codet () | |
codet (const irep_idt &statement) | |
void | set_statement (const irep_idt &statement) |
const irep_idt & | get_statement () const |
codet & | first_statement () |
const codet & | first_statement () const |
codet & | last_statement () |
const codet & | last_statement () const |
class code_blockt & | make_block () |
![]() | |
exprt () | |
exprt (const irep_idt &_id) | |
exprt (const irep_idt &_id, const typet &_type) | |
typet & | type () |
const typet & | type () const |
bool | has_operands () const |
operandst & | operands () |
const operandst & | operands () const |
exprt & | op0 () |
exprt & | op1 () |
exprt & | op2 () |
exprt & | op3 () |
const exprt & | op0 () const |
const exprt & | op1 () const |
const exprt & | op2 () const |
const exprt & | op3 () const |
void | reserve_operands (operandst::size_type n) |
void | move_to_operands (exprt &expr) |
void | move_to_operands (exprt &e1, exprt &e2) |
void | move_to_operands (exprt &e1, exprt &e2, exprt &e3) |
void | copy_to_operands (const exprt &expr) |
void | copy_to_operands (const exprt &e1, const exprt &e2) |
void | copy_to_operands (const exprt &e1, const exprt &e2, const exprt &e3) |
void | make_typecast (const typet &_type) |
void | make_not () |
void | make_true () |
void | make_false () |
void | make_bool (bool value) |
bool | is_constant () const |
bool | is_true () const |
bool | is_false () const |
bool | is_zero () const |
bool | is_one () const |
bool | is_boolean () const |
const source_locationt & | find_source_location () const |
const source_locationt & | source_location () const |
source_locationt & | add_source_location () |
exprt & | add_expr (const irep_idt &name) |
const exprt & | find_expr (const irep_idt &name) const |
void | visit (class expr_visitort &visitor) |
void | visit (class const_expr_visitort &visitor) const |
depth_iteratort | depth_begin () |
depth_iteratort | depth_end () |
const_depth_iteratort | depth_begin () const |
const_depth_iteratort | depth_end () const |
const_depth_iteratort | depth_cbegin () const |
const_depth_iteratort | depth_cend () const |
depth_iteratort | depth_begin (std::function< exprt &()> mutate_root) const |
const_unique_depth_iteratort | unique_depth_begin () const |
const_unique_depth_iteratort | unique_depth_end () const |
const_unique_depth_iteratort | unique_depth_cbegin () const |
const_unique_depth_iteratort | unique_depth_cend () const |
![]() | |
bool | is_nil () const |
bool | is_not_nil () const |
irept (const irep_idt &_id) | |
irept () | |
irept (const irept &irep) | |
irept (irept &&irep) | |
irept & | operator= (const irept &irep) |
irept & | operator= (irept &&irep) |
~irept () | |
const irep_idt & | id () const |
const std::string & | id_string () const |
void | id (const irep_idt &_data) |
const irept & | find (const irep_namet &name) const |
irept & | add (const irep_namet &name) |
irept & | add (const irep_namet &name, const irept &irep) |
const std::string & | get_string (const irep_namet &name) const |
const irep_idt & | get (const irep_namet &name) const |
bool | get_bool (const irep_namet &name) const |
signed int | get_int (const irep_namet &name) const |
unsigned int | get_unsigned_int (const irep_namet &name) const |
std::size_t | get_size_t (const irep_namet &name) const |
long long | get_long_long (const irep_namet &name) const |
void | set (const irep_namet &name, const irep_idt &value) |
void | set (const irep_namet &name, const irept &irep) |
void | set (const irep_namet &name, const long long value) |
void | remove (const irep_namet &name) |
void | move_to_sub (irept &irep) |
void | move_to_named_sub (const irep_namet &name, irept &irep) |
bool | operator== (const irept &other) const |
bool | operator!= (const irept &other) const |
void | swap (irept &irep) |
bool | operator< (const irept &other) const |
defines ordering on the internal representation More... | |
bool | ordering (const irept &other) const |
defines ordering on the internal representation More... | |
int | compare (const irept &i) const |
defines ordering on the internal representation More... | |
void | clear () |
void | make_nil () |
subt & | get_sub () |
const subt & | get_sub () const |
named_subt & | get_named_sub () |
const named_subt & | get_named_sub () const |
named_subt & | get_comments () |
const named_subt & | get_comments () const |
std::size_t | hash () const |
std::size_t | full_hash () const |
bool | full_eq (const irept &other) const |
std::string | pretty (unsigned indent=0, unsigned max_indent=0) const |
const dt & | read () const |
dt & | write () |
Additional Inherited Members | |
![]() | |
void | detach () |
![]() | |
static bool | is_comment (const irep_namet &name) |
static void | remove_ref (dt *old_data) |
static void | nonrecursive_destructor (dt *old_data) |
Does the same as remove_ref, but using an explicit stack instead of recursion. More... | |
![]() | |
dt * | data |
![]() | |
static dt | empty_d |
A function call.
The function call instruction has three operands. The first is the expression that is used to store the return value. The second is the function called. The third is a vector of argument values.
Definition at line 828 of file std_code.h.
Definition at line 858 of file std_code.h.
|
inline |
Definition at line 831 of file std_code.h.
References irept::id(), lhs(), irept::make_nil(), exprt::op2(), and exprt::operands().
|
inline |
Definition at line 860 of file std_code.h.
References exprt::op2(), and exprt::operands().
Referenced by string_abstractiont::abstract_function_call(), actuals_replace_map(), code_contractst::add_contract_check(), code_contractst::apply_contract(), goto_program2codet::cleanup_code(), dump_ct::cleanup_expr(), goto_checkt::collect_allocations(), _rw_set_loct::compute(), character_refine_preprocesst::convert_char_function(), expr2javat::convert_code_function_call(), expr2ct::convert_code_function_call(), character_refine_preprocesst::convert_compare(), goto_convertt::convert_cpp_delete(), goto_program2codet::convert_decl(), goto_convertt::convert_decl(), character_refine_preprocesst::convert_digit_char(), character_refine_preprocesst::convert_for_digit(), goto_convertt::convert_function_call(), java_bytecode_convert_methodt::convert_invoke(), character_refine_preprocesst::convert_is_ideographic(), character_refine_preprocesst::convert_is_ISO_control_char(), character_refine_preprocesst::convert_is_low_surrogate(), character_refine_preprocesst::convert_is_surrogate_pair(), java_bytecode_convert_methodt::convert_monitorenter(), java_bytecode_convert_methodt::convert_monitorexit(), goto_program2codet::convert_start_thread(), character_refine_preprocesst::convert_to_code_point(), create_static_function_call(), goto_convertt::do_cpp_new(), string_instrumentationt::do_fscanf(), goto_convertt::do_function_call_other(), goto_convertt::do_function_call_symbol(), parameter_assignmentst::do_function_calls(), goto_convertt::do_scanf(), string_instrumentationt::do_snprintf(), string_instrumentationt::do_sprintf(), string_instrumentationt::do_strchr(), string_instrumentationt::do_strrchr(), string_instrumentationt::do_strstr(), string_instrumentationt::do_strtok(), interpretert::execute_function_call(), expressions_read(), remove_function_pointerst::fix_argument_types(), function_to_call(), remove_asmt::gcc_asm_function_call(), java_object_factoryt::gen_nondet_struct_init(), generate_ansi_c_start_function(), generate_java_start_function(), get_thread_block_identifier(), goto_checkt::goto_check(), goto_rw(), escape_analysist::insert_cleanup(), concurrency_instrumentationt::instrument(), taint_analysist::instrument(), cover_cover_instrumentert::instrument(), java_bytecode_instrumentt::instrument_code(), instrument_endThread(), instrument_getCurrentThreadID(), instrument_start_thread(), java_static_lifetime_init(), list_calls_and_arguments(), java_string_library_preprocesst::make_object_get_class_code(), mm_io(), mutex_init_instrumentation(), nondet_volatile(), remove_calls_no_bodyt::operator()(), goto_convertt::remove_function_call(), remove_function_pointerst::remove_function_pointer(), remove_virtual_functionst::remove_virtual_function(), constant_propagator_ait::replace(), static_simplifier(), goto_symext::symex_function_call_code(), goto_symext::symex_step(), goto_symext::symex_trace(), constant_propagator_domaint::transform(), custom_bitvector_domaint::transform(), escape_domaint::transform(), value_set_domain_fivrt::transform(), value_set_domain_fivrnst::transform(), value_set_domain_fit::transform(), java_bytecode_typecheckt::typecheck_code(), jsil_typecheckt::typecheck_function_call(), c_typecheck_baset::typecheck_side_effect_statement_expression(), flow_insensitive_analysis_baset::visit(), static_analysis_baset::visit(), and ai_baset::visit().
|
inline |
Definition at line 865 of file std_code.h.
References exprt::op2(), and exprt::operands().
|
inline |
Definition at line 848 of file std_code.h.
References exprt::op1().
Referenced by string_abstractiont::abstract_function_call(), actuals_replace_map(), code_contractst::add_contract_check(), code_contractst::apply_contract(), goto_program2codet::cleanup_code(), dump_ct::cleanup_expr(), dump_ct::cleanup_harness(), clinit_wrapper_do_recursive_calls(), 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(), expr2javat::convert_code_function_call(), expr2ct::convert_code_function_call(), goto_convertt::convert_cpp_delete(), goto_program2codet::convert_decl(), goto_convertt::convert_function_call(), goto_program2codet::convert_instruction(), java_bytecode_convert_methodt::convert_invoke(), java_bytecode_convert_methodt::convert_monitorenter(), java_bytecode_convert_methodt::convert_monitorexit(), goto_program2codet::convert_start_thread(), convert_threadblock(), create_static_function_call(), goto_program_dereferencet::dereference_instruction(), goto_convertt::do_cpp_new(), string_instrumentationt::do_function_call(), flow_insensitive_analysis_baset::do_function_call(), goto_convertt::do_function_call_other(), goto_convertt::do_function_call_symbol(), parameter_assignmentst::do_function_calls(), remove_returnst::do_function_calls(), goto_convertt::do_scanf(), interpretert::execute_function_call(), require_goto_statements::find_function_calls(), find_used_functions(), remove_function_pointerst::fix_argument_types(), remove_function_pointerst::fix_return_type(), forall_callsites(), remove_exceptionst::function_or_callees_may_throw(), function_to_call(), ci_lazy_methodst::gather_virtual_callsites(), remove_asmt::gcc_asm_function_call(), java_object_factoryt::gen_nondet_struct_init(), generate_ansi_c_start_function(), generate_java_start_function(), java_bytecode_convert_methodt::get_clinit_call(), get_destructor(), function_modifiest::get_modifies(), havoc_loopst::get_modifies(), goto_checkt::goto_check(), goto_rw(), escape_analysist::insert_cleanup(), concurrency_instrumentationt::instrument(), taint_analysist::instrument(), cover_cover_instrumentert::instrument(), java_bytecode_instrumentt::instrument_code(), remove_exceptionst::instrument_function_call(), interrupt(), is_fence(), is_lwfence(), is_nondet_returning_object(), remove_calls_no_bodyt::is_opaque_function_call(), java_static_lifetime_init(), jsil_entry_point(), list_calls_and_arguments(), java_string_library_preprocesst::make_object_get_class_code(), mm_io(), model_argc_argv(), mutex_init_instrumentation(), nondet_static(), taint_analysist::operator()(), check_call_sequencet::operator()(), goto_convertt::remove_function_call(), 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(), character_refine_preprocesst::replace_character_call(), show_call_sequences(), static_lifetime_init(), static_simplifier(), goto_symext::symex_function_call(), goto_symext::symex_function_call_code(), goto_symext::symex_function_call_symbol(), goto_symext::symex_step(), thread_exit_instrumentation(), constant_propagator_domaint::transform(), uncaught_exceptions_domaint::transform(), custom_bitvector_domaint::transform(), escape_domaint::transform(), rd_range_domaint::transform_function_call(), java_bytecode_typecheckt::typecheck_code(), jsil_typecheckt::typecheck_function_call(), c_typecheck_baset::typecheck_side_effect_statement_expression(), 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 853 of file std_code.h.
References exprt::op1().
|
inline |
Definition at line 838 of file std_code.h.
References exprt::op0().
Referenced by code_contractst::add_contract_check(), code_contractst::apply_contract(), local_may_aliast::build(), local_bitvector_analysist::build(), check_and_replace_target(), goto_program2codet::cleanup_code(), code_function_callt(), _rw_set_loct::compute(), goto_program2codet::convert_assign_varargs(), character_refine_preprocesst::convert_char_function(), jsil_convertt::convert_code(), expr2javat::convert_code_function_call(), expr2ct::convert_code_function_call(), character_refine_preprocesst::convert_compare(), goto_convertt::convert_cpp_delete(), goto_program2codet::convert_decl(), character_refine_preprocesst::convert_digit_char(), character_refine_preprocesst::convert_for_digit(), goto_convertt::convert_function_call(), java_bytecode_convert_methodt::convert_invoke(), character_refine_preprocesst::convert_is_ideographic(), character_refine_preprocesst::convert_is_ISO_control_char(), character_refine_preprocesst::convert_is_low_surrogate(), character_refine_preprocesst::convert_is_surrogate_pair(), java_bytecode_convert_methodt::convert_monitorenter(), java_bytecode_convert_methodt::convert_monitorexit(), goto_program2codet::convert_start_thread(), character_refine_preprocesst::convert_to_code_point(), goto_program_dereferencet::dereference_instruction(), goto_convertt::do_cpp_new(), string_instrumentationt::do_fscanf(), flow_insensitive_analysis_baset::do_function_call(), goto_convertt::do_function_call_other(), goto_convertt::do_function_call_symbol(), remove_returnst::do_function_calls(), goto_convertt::do_scanf(), string_instrumentationt::do_snprintf(), string_instrumentationt::do_sprintf(), string_instrumentationt::do_strerror(), interpretert::execute_function_call(), expressions_read(), expressions_written(), remove_function_pointerst::fix_return_type(), function_to_call(), remove_asmt::gcc_asm_function_call(), generate_ansi_c_start_function(), generate_java_start_function(), get_modifies(), function_modifiest::get_modifies(), havoc_loopst::get_modifies(), function_modifiest::get_modifies_lhs(), goto_rw(), escape_analysist::insert_cleanup(), java_bytecode_instrumentt::instrument_code(), instrument_getCurrentThreadID(), jsil_entry_point(), java_string_library_preprocesst::make_object_get_class_code(), nondet_volatile(), remove_calls_no_bodyt::operator()(), goto_convertt::remove_function_call(), remove_function_pointerst::remove_function_pointer(), goto_symext::symex_function_call_code(), goto_symext::symex_step(), interval_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_function_call(), c_typecheck_baset::typecheck_side_effect_statement_expression(), and remove_returnst::undo_function_calls().
|
inline |
Definition at line 843 of file std_code.h.
References exprt::op0().