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) |
void | negate () |
bool | sum (const exprt &expr) |
bool | mul (const exprt &expr) |
bool | subtract (const exprt &expr) |
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 |
![]() | |
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 657 of file std_code.h.
Definition at line 687 of file std_code.h.
|
inline |
Definition at line 660 of file std_code.h.
References irept::id(), lhs(), irept::make_nil(), exprt::op2(), and exprt::operands().
|
inline |
Definition at line 689 of file std_code.h.
References exprt::op2(), and exprt::operands().
Referenced by string_abstractiont::abstract_function_call(), const_function_pointer_propagationt::arg_stackt::add_args(), code_contractst::add_contract_check(), ansi_c_entry_point(), 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_instructions(), 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(), goto_program2codet::convert_start_thread(), character_refine_preprocesst::convert_to_code_point(), 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(), const_function_pointer_propagationt::dup_caller_and_inline_callee(), interpretert::execute_function_call(), expressions_read(), remove_function_pointerst::fix_argument_types(), path_symext::function_call_rec(), function_to_call(), remove_asmt::gcc_asm_function_call(), goto_inlinet::get_call(), goto_checkt::goto_check(), goto_rw(), escape_analysist::insert_cleanup(), concurrency_instrumentationt::instrument(), taint_analysist::instrument(), instrument_cover_goals(), java_entry_point(), list_calls_and_arguments(), mm_io(), mutex_init_instrumentation(), nondet_volatile(), goto_convertt::remove_function_call(), remove_function_pointerst::remove_function_pointer(), remove_virtual_functionst::remove_virtual_function(), constant_propagator_ait::replace(), replace_async(), goto_symext::symex_function_call_code(), goto_symext::symex_step(), goto_symext::symex_trace(), custom_bitvector_domaint::transform(), escape_domaint::transform(), value_set_domain_fivrt::transform(), value_set_domain_fivrnst::transform(), value_set_domain_fit::transform(), value_set_domaint::transform(), java_bytecode_typecheckt::typecheck_code(), cpp_typecheckt::typecheck_compound_declarator(), 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 694 of file std_code.h.
References exprt::op2(), and exprt::operands().
|
inline |
Definition at line 677 of file std_code.h.
References exprt::op1().
Referenced by string_abstractiont::abstract_function_call(), call_grapht::add(), code_contractst::add_contract_check(), ansi_c_entry_point(), code_contractst::apply_contract(), 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(), 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_instructions(), goto_program2codet::convert_start_thread(), 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(), path_searcht::drop_state(), const_function_pointer_propagationt::dup_caller_and_inline_callee(), interpretert::execute_function_call(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), find_used_functions(), remove_function_pointerst::fix_argument_types(), remove_function_pointerst::fix_return_type(), path_symext::function_call(), function_to_call(), gather_virtual_callsites(), remove_asmt::gcc_asm_function_call(), goto_inlinet::get_call(), get_destructor(), function_modifiest::get_modifies(), havoc_loopst::get_modifies(), get_virtual_method_targets(), goto_checkt::goto_check(), goto_rw(), escape_analysist::insert_cleanup(), concurrency_instrumentationt::instrument(), taint_analysist::instrument(), instrument_cover_goals(), remove_exceptionst::instrument_function_call(), interrupt(), is_fence(), is_lwfence(), java_entry_point(), java_static_lifetime_init(), jsil_entry_point(), list_calls_and_arguments(), mm_io(), mutex_init_instrumentation(), nondet_static(), taint_analysist::operator()(), check_call_sequencet::operator()(), const_function_pointer_propagationt::propagate(), 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(), replace_async(), character_refine_preprocesst::replace_character_call(), show_call_sequences(), static_lifetime_init(), 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(), custom_bitvector_domaint::transform(), escape_domaint::transform(), rd_range_domaint::transform_function_call(), java_bytecode_typecheckt::typecheck_code(), cpp_typecheckt::typecheck_compound_declarator(), 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 682 of file std_code.h.
References exprt::op1().
|
inline |
Definition at line 667 of file std_code.h.
References exprt::op0().
Referenced by code_contractst::add_contract_check(), ansi_c_entry_point(), code_contractst::apply_contract(), local_may_aliast::build(), local_bitvector_analysist::build(), 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_instructions(), 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(), 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(), path_symext::function_call_rec(), function_to_call(), remove_asmt::gcc_asm_function_call(), goto_inlinet::get_call(), get_modifies(), function_modifiest::get_modifies(), havoc_loopst::get_modifies(), function_modifiest::get_modifies_lhs(), goto_rw(), escape_analysist::insert_cleanup(), java_entry_point(), java_static_lifetime_init(), jsil_entry_point(), nondet_volatile(), 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 672 of file std_code.h.
References exprt::op0().