cprover
|
Public Member Functions | |
string_instrumentationt (symbol_tablet &_symbol_table, message_handlert &_message_handler) | |
void | operator() (goto_programt &dest) |
void | operator() (goto_functionst &dest) |
Protected Attributes | |
symbol_tablet & | symbol_table |
namespacet | ns |
Additional Inherited Members |
Definition at line 55 of file string_instrumentation.cpp.
|
inline |
Definition at line 58 of file string_instrumentation.cpp.
|
protected |
Definition at line 391 of file string_instrumentation.cpp.
References goto_programt::add_instruction(), index_exprt::array(), format_tokent::ASTERISK, comment(), namespace_baset::follow(), from_integer(), irept::get_string(), irept::id(), index_exprt::index(), index_type(), is_string_type(), is_zero_string(), ns, exprt::op0(), parse_format_string(), format_tokent::STRING, typet::subtype(), format_tokent::TEXT, exprt::type(), and format_tokent::UNKNOWN.
Referenced by do_snprintf(), and do_sprintf().
|
protected |
Definition at line 494 of file string_instrumentation.cpp.
References goto_programt::add_instruction(), exprt::add_source_location(), ASSIGN, format_tokent::ASTERISK, buffer_size(), comment(), namespace_baset::follow(), from_integer(), irept::get_string(), irept::id(), invalidate_buffer(), is_string_type(), ns, exprt::op0(), parse_format_string(), format_tokent::STRING, typet::subtype(), format_tokent::TEXT, exprt::type(), format_tokent::UNKNOWN, and unsigned_int_type().
Referenced by do_fscanf().
|
protected |
Definition at line 358 of file string_instrumentation.cpp.
References goto_programt::add_instruction(), exprt::add_source_location(), code_function_callt::arguments(), ASSIGN, do_format_string_write(), messaget::eom(), messaget::error(), goto_programt::insert_before_swap(), irept::is_not_nil(), code_function_callt::lhs(), messaget::mstreamt::source_location, and exprt::type().
Referenced by do_function_call().
|
protected |
Definition at line 221 of file string_instrumentation.cpp.
References do_fscanf(), do_snprintf(), do_sprintf(), do_strchr(), do_strerror(), do_strncmp(), do_strrchr(), do_strstr(), do_strtok(), code_function_callt::function(), symbol_exprt::get_identifier(), remove_skip(), to_code_function_call(), and to_symbol_expr().
Referenced by instrument().
|
protected |
Definition at line 315 of file string_instrumentation.cpp.
References goto_programt::add_instruction(), exprt::add_source_location(), code_function_callt::arguments(), ASSIGN, buffer_size(), do_format_string_read(), messaget::eom(), messaget::error(), goto_programt::insert_before_swap(), irept::is_not_nil(), code_function_callt::lhs(), messaget::mstreamt::source_location, and exprt::type().
Referenced by do_function_call().
|
protected |
Definition at line 273 of file string_instrumentation.cpp.
References goto_programt::add_instruction(), exprt::add_source_location(), code_function_callt::arguments(), ASSIGN, do_format_string_read(), messaget::eom(), messaget::error(), goto_programt::insert_before_swap(), irept::is_not_nil(), code_function_callt::lhs(), messaget::mstreamt::source_location, and exprt::type().
Referenced by do_function_call().
|
protected |
|
protected |
Definition at line 646 of file string_instrumentation.cpp.
References goto_programt::add_instruction(), code_function_callt::arguments(), messaget::eom(), messaget::error(), goto_programt::insert_before_swap(), is_zero_string(), and messaget::mstreamt::source_location.
Referenced by do_function_call().
|
protected |
Definition at line 768 of file string_instrumentation.cpp.
References goto_programt::add_instruction(), ASSIGN, symbolt::base_name, char_type(), from_integer(), index_type(), symbol_tablet::insert(), goto_programt::insert_before_swap(), symbolt::is_lvalue, irept::is_nil(), symbolt::is_state_var, symbolt::is_static_lifetime, is_zero_string(), code_function_callt::lhs(), namespacet::lookup(), make_type(), symbolt::mode, symbolt::name, ns, symbolt::pretty_name, size_type(), exprt::source_location(), symbolt::symbol_expr(), symbol_table, symbol_table_baset::symbols, symbolt::type, and exprt::type().
Referenced by do_function_call().
|
protected |
Definition at line 639 of file string_instrumentation.cpp.
Referenced by do_function_call().
|
protected |
Definition at line 673 of file string_instrumentation.cpp.
References goto_programt::add_instruction(), code_function_callt::arguments(), messaget::eom(), messaget::error(), goto_programt::insert_before_swap(), is_zero_string(), and messaget::mstreamt::source_location.
Referenced by do_function_call().
|
protected |
Definition at line 700 of file string_instrumentation.cpp.
References goto_programt::add_instruction(), code_function_callt::arguments(), messaget::eom(), messaget::error(), goto_programt::insert_before_swap(), is_zero_string(), and messaget::mstreamt::source_location.
Referenced by do_function_call().
|
protected |
Definition at line 734 of file string_instrumentation.cpp.
References goto_programt::add_instruction(), code_function_callt::arguments(), messaget::eom(), messaget::error(), goto_programt::insert_before_swap(), is_zero_string(), and messaget::mstreamt::source_location.
Referenced by do_function_call().
|
protected |
Definition at line 202 of file string_instrumentation.cpp.
References ASSIGN, do_function_call(), and FUNCTION_CALL.
Referenced by operator()().
|
protected |
Definition at line 860 of file string_instrumentation.cpp.
References goto_programt::add_instruction(), index_exprt::array(), ASSIGN, symbolt::base_name, buffer_size(), from_integer(), irept::id(), index_exprt::index(), index_type(), symbol_tablet::insert(), symbolt::is_lvalue, symbolt::is_state_var, symbolt::is_static_lifetime, namespacet::lookup(), symbolt::mode, symbolt::name, ns, symbolt::pretty_name, size_type(), typet::subtype(), symbolt::symbol_expr(), symbol_table, symbol_table_baset::symbols, symbolt::type, exprt::type(), and unsigned_int_type().
Referenced by do_format_string_write().
|
inlineprotected |
Definition at line 141 of file string_instrumentation.cpp.
References configt::ansi_c, configt::ansi_ct::char_width, config, irept::id(), typet::subtype(), and to_bitvector_type().
Referenced by do_format_string_read(), and do_format_string_write().
Definition at line 74 of file string_instrumentation.cpp.
References namespace_baset::follow(), exprt::make_typecast(), ns, and exprt::type().
Referenced by do_strerror().
void string_instrumentationt::operator() | ( | goto_programt & | dest | ) |
Definition at line 196 of file string_instrumentation.cpp.
References Forall_goto_program_instructions, and instrument().
void string_instrumentationt::operator() | ( | goto_functionst & | dest | ) |
Definition at line 185 of file string_instrumentation.cpp.
References goto_functionst::function_map.
|
protected |
Definition at line 72 of file string_instrumentation.cpp.
Referenced by do_format_string_read(), do_format_string_write(), do_strerror(), invalidate_buffer(), and make_type().
|
protected |
Definition at line 71 of file string_instrumentation.cpp.
Referenced by do_strerror(), and invalidate_buffer().