cprover
|
#include <string_abstraction.h>
Public Member Functions | |
string_abstractiont (symbol_tablet &_symbol_table, message_handlert &_message_handler) | |
void | operator() (goto_programt &dest) |
void | operator() (goto_functionst &dest) |
Protected Types | |
enum | whatt { whatt::IS_ZERO, whatt::LENGTH, whatt::SIZE } |
typedef ::std::map< typet, typet > | abstraction_types_mapt |
typedef std::unordered_map< irep_idt, irep_idt > | localst |
Static Protected Member Functions | |
static bool | has_string_macros (const exprt &expr) |
static typet | build_type (whatt what) |
Protected Attributes | |
const std::string | arg_suffix |
std::string | sym_suffix |
symbol_tablet & | symbol_table |
namespacet | ns |
unsigned | temporary_counter |
abstraction_types_mapt | abstraction_types_map |
::std::set< irep_idt > | current_args |
typet | string_struct |
goto_programt | initialization |
localst | locals |
Additional Inherited Members |
Definition at line 22 of file string_abstraction.h.
|
protected |
Definition at line 39 of file string_abstraction.h.
|
protected |
Definition at line 137 of file string_abstraction.h.
|
strongprotected |
Enumerator | |
---|---|
IS_ZERO | |
LENGTH | |
SIZE |
Definition at line 106 of file string_abstraction.h.
string_abstractiont::string_abstractiont | ( | symbol_tablet & | _symbol_table, |
message_handlert & | _message_handler | ||
) |
Definition at line 91 of file string_abstraction.cpp.
References build_type(), struct_union_typet::components(), IS_ZERO, LENGTH, SIZE, and string_struct.
|
protected |
Definition at line 454 of file string_abstraction.cpp.
References abstract_assign(), abstract_function_call(), ASSERT, ASSIGN, ASSUME, ATOMIC_BEGIN, ATOMIC_END, CATCH, DEAD, DECL, END_FUNCTION, END_THREAD, FUNCTION_CALL, GOTO, has_string_macros(), INCOMPLETE_GOTO, LOCATION, NO_INSTRUCTION_TYPE, OTHER, replace_string_macros(), RETURN, SKIP, START_THREAD, THROW, and UNREACHABLE.
|
protected |
Definition at line 234 of file string_abstraction.cpp.
References declare_define_locals(), Forall_goto_program_instructions, and locals.
|
protected |
Definition at line 503 of file string_abstraction.cpp.
References abstract_char_assign(), abstract_pointer_assign(), namespace_baset::follow(), has_string_macros(), irept::id(), is_char_type(), code_assignt::lhs(), move_lhs_arithmetic(), ns, replace_string_macros(), code_assignt::rhs(), exprt::source_location(), to_code_assign(), and exprt::type().
Referenced by abstract().
|
protected |
Definition at line 1104 of file string_abstraction.cpp.
References index_exprt::array(), build_type(), build_wrap(), char_assign(), from_integer(), irept::id(), index_exprt::index(), irept::is_nil(), irept::is_not_nil(), exprt::is_zero(), LENGTH, code_assignt::lhs(), make_type(), member(), pointer_arithmetict::offset, exprt::op0(), pointer_arithmetict::pointer, code_assignt::rhs(), to_code_assign(), to_dereference_expr(), to_index_expr(), and exprt::type().
Referenced by abstract_assign().
|
protected |
Definition at line 530 of file string_abstraction.cpp.
References code_function_callt::arguments(), build_abstraction_type(), build_unknown(), build_wrap(), messaget::eom(), messaget::error(), from_integer(), code_function_callt::function(), irept::get(), irept::id(), index_type(), irept::is_nil(), is_ptr_argument(), namespacet::lookup(), ns, code_typet::parameters(), irept::set(), typet::subtype(), to_code_function_call(), to_code_type(), symbolt::type, and type_eq().
Referenced by abstract().
|
protected |
Definition at line 1059 of file string_abstraction.cpp.
References exprt::add_source_location(), build_abstraction_type(), build_unknown(), build_wrap(), goto_programt::instructiont::code, goto_programt::instructiont::function, irept::id(), goto_programt::insert_before_swap(), irept::is_nil(), code_assignt::lhs(), goto_programt::instructiont::make_assignment(), exprt::op0(), code_assignt::rhs(), goto_programt::instructiont::source_location, to_code_assign(), exprt::type(), and value_assignments().
Referenced by abstract_assign().
|
protected |
Definition at line 206 of file string_abstraction.cpp.
References symbolt::base_name, symbol_tablet::insert(), is_ptr_argument(), symbolt::location, irept::make_nil(), symbolt::mode, symbolt::module, symbolt::name, pointer_type(), symbolt::pretty_name, symbol_table, symbolt::type, and symbolt::value.
Referenced by add_str_arguments().
|
protected |
Definition at line 388 of file string_abstraction.cpp.
References goto_programt::add_instruction(), symbolt::base_name, build_type(), build_unknown(), dstringt::empty(), irept::id(), id2string(), symbol_tablet::insert(), is_char_type(), irept::is_not_nil(), IS_ZERO, LENGTH, symbolt::location, irept::make_nil(), make_type(), make_val_or_dummy_rec(), symbolt::mode, symbolt::module, symbolt::name, ns, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), symbolt::pretty_name, SIZE, array_typet::size(), string_struct, typet::subtype(), symbolt::symbol_expr(), symbol_table, to_array_type(), symbolt::type, type_eq(), and symbolt::value.
Referenced by make_val_or_dummy_rec().
|
protected |
Definition at line 169 of file string_abstraction.cpp.
References add_argument(), arg_suffix, build_abstraction_type(), current_args, symbol_tablet::get_writeable(), id2string(), irept::is_nil(), code_typet::parameters(), symbol_table, to_code_type(), and symbolt::type.
Referenced by operator()().
|
protected |
Definition at line 625 of file string_abstraction.cpp.
References build_unknown(), build_wrap(), irept::id(), LENGTH, member(), exprt::op0(), exprt::operands(), pointer_offset(), messaget::result(), SIZE, exprt::type(), and UNREACHABLE.
Referenced by build(), build_wrap(), and replace_string_macros().
Definition at line 741 of file string_abstraction.cpp.
References index_exprt::array(), build(), build_abstraction_type(), build_array(), build_if(), build_pointer(), build_symbol(), build_symbol_constant(), build_wrap(), member_exprt::get_component_name(), irept::id(), id2string(), index_exprt::index(), is_char_type(), irept::is_nil(), ns, exprt::op0(), dereference_exprt::pointer(), member_exprt::struct_op(), typet::subtype(), to_array_expr(), to_dereference_expr(), to_if_expr(), to_index_expr(), to_member_expr(), to_symbol_expr(), to_typecast_expr(), exprt::type(), and type_eq().
Definition at line 659 of file string_abstraction.cpp.
References abstraction_types_map, build_abstraction_type_rec(), namespace_baset::follow(), and ns.
Referenced by abstract_function_call(), abstract_pointer_assign(), add_str_arguments(), build(), build_symbol(), and build_wrap().
|
protected |
Definition at line 678 of file string_abstraction.cpp.
References abstraction_types_map, struct_union_typet::components(), irept::find(), namespace_baset::follow(), irept::id(), is_char_type(), irept::is_nil(), ns, pointer_type(), array_typet::size(), string_struct, typet::subtype(), to_array_type(), and to_struct_union_type().
Referenced by build_abstraction_type().
|
protected |
Definition at line 837 of file string_abstraction.cpp.
References build_symbol_constant(), is_char_type(), array_typet::size(), to_array_type(), and to_integer().
Referenced by build().
Definition at line 809 of file string_abstraction.cpp.
References build_unknown(), build_wrap(), if_exprt::cond(), if_exprt::false_case(), irept::swap(), if_exprt::true_case(), and exprt::type().
Referenced by build().
|
protected |
Definition at line 971 of file string_abstraction.cpp.
References goto_programt::add_instruction(), symbolt::base_name, dstringt::empty(), id2string(), initialization, symbol_tablet::insert(), goto_programt::instructions, symbolt::is_static_lifetime, symbolt::is_thread_local, locals, symbolt::location, make_decl_and_def(), irept::make_nil(), symbolt::mode, symbolt::module, symbolt::name, symbolt::pretty_name, sym_suffix, symbol_table, symbolt::type, and symbolt::value.
Referenced by build_symbol().
|
protected |
Definition at line 861 of file string_abstraction.cpp.
References build_wrap(), irept::id(), is_char_type(), address_of_exprt::object(), pointer_arithmetict::pointer, to_address_of_expr(), and to_index_expr().
Referenced by build().
|
protected |
Definition at line 944 of file string_abstraction.cpp.
References arg_suffix, build_abstraction_type(), build_new_symbol(), current_args, symbol_exprt::get_identifier(), id2string(), irept::is_nil(), is_ptr_argument(), namespacet::lookup(), symbolt::name, ns, typet::subtype(), sym_suffix, symbolt::symbol_expr(), symbol_table, symbol_table_baset::symbols, symbolt::type, and exprt::type().
Referenced by build().
|
protected |
Definition at line 1002 of file string_abstraction.cpp.
References goto_programt::add_instruction(), symbolt::base_name, build_type(), from_integer(), id2string(), initialization, symbol_tablet::insert(), integer2string(), symbolt::is_file_local, symbolt::is_static_lifetime, symbolt::is_thread_local, LENGTH, irept::make_nil(), symbolt::mode, symbolt::name, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), symbolt::pretty_name, SIZE, string_struct, symbolt::symbol_expr(), symbol_table, symbol_table_baset::symbols, symbolt::type, and symbolt::value.
Referenced by build(), and build_array().
Definition at line 120 of file string_abstraction.cpp.
References IS_ZERO, LENGTH, SIZE, and size_type().
Referenced by abstract_char_assign(), add_dummy_symbol_and_value(), build_symbol_constant(), build_unknown(), member(), and string_abstractiont().
Definition at line 893 of file string_abstraction.cpp.
References build_type(), IS_ZERO, LENGTH, messaget::result(), and SIZE.
Referenced by abstract_function_call(), abstract_pointer_assign(), add_dummy_symbol_and_value(), build(), and build_if().
Definition at line 917 of file string_abstraction.cpp.
References symbolt::base_name, symbol_tablet::insert(), locals, namespacet::lookup(), irept::make_nil(), symbolt::mode, symbolt::module, symbolt::name, ns, symbolt::pretty_name, symbol_table, temporary_counter, to_string(), symbolt::type, and symbolt::value.
Definition at line 23 of file string_abstraction.cpp.
References build(), build_abstraction_type(), messaget::eom(), irept::id(), ns, typet::subtype(), exprt::type(), type_eq(), and messaget::warning().
Referenced by abstract_char_assign(), abstract_function_call(), abstract_pointer_assign(), build(), build_if(), and build_pointer().
|
protected |
Definition at line 1165 of file string_abstraction.cpp.
References goto_programt::add_instruction(), goto_programt::insert_before_swap(), irept::is_not_nil(), IS_ZERO, member(), and move_lhs_arithmetic().
Referenced by abstract_char_assign().
|
protected |
Definition at line 249 of file string_abstraction.cpp.
References Forall_goto_program_instructions, code_declt::get_identifier(), goto_programt::insert_before_swap(), goto_programt::instructions, locals, make_decl_and_def(), and to_code_decl().
Referenced by abstract().
|
staticprotected |
Definition at line 583 of file string_abstraction.cpp.
References forall_operands, and irept::id().
Referenced by abstract(), and abstract_assign().
|
inlineprotected |
Definition at line 53 of file string_abstraction.h.
References configt::ansi_c, configt::ansi_ct::char_width, config, namespace_baset::follow(), bitvector_typet::get_width(), irept::id(), ns, and to_bitvector_type().
Referenced by abstract_assign(), add_dummy_symbol_and_value(), build(), build_abstraction_type_rec(), build_array(), and build_pointer().
|
protected |
Definition at line 52 of file string_abstraction.cpp.
References irept::id(), ns, string_struct, typet::subtype(), and type_eq().
Referenced by make_val_or_dummy_rec(), and member().
|
protected |
Definition at line 284 of file string_abstraction.cpp.
References goto_programt::add_instruction(), namespace_baset::follow(), irept::is_nil(), irept::is_not_nil(), namespacet::lookup(), make_val_or_dummy_rec(), ns, symbolt::symbol_expr(), symbolt::type, and symbolt::value.
Referenced by build_new_symbol(), and declare_define_locals().
Definition at line 67 of file string_abstraction.h.
References namespace_baset::follow(), irept::is_not_nil(), exprt::make_typecast(), ns, and exprt::type().
Referenced by abstract_char_assign(), and add_dummy_symbol_and_value().
|
protected |
Definition at line 319 of file string_abstraction.cpp.
References add_dummy_symbol_and_value(), goto_programt::add_instruction(), struct_union_typet::components(), namespace_baset::follow(), irept::id(), is_ptr_string_struct(), member(), ns, string_struct, typet::subtype(), symbolt::symbol_expr(), to_array_type(), to_struct_union_type(), symbolt::type, exprt::type(), and type_eq().
Referenced by add_dummy_symbol_and_value(), and make_decl_and_def().
Definition at line 1333 of file string_abstraction.cpp.
References build_type(), irept::id(), irept::is_nil(), is_ptr_string_struct(), IS_ZERO, LENGTH, ns, messaget::result(), SIZE, string_struct, exprt::type(), and type_eq().
Referenced by abstract_char_assign(), build(), char_assign(), make_val_or_dummy_rec(), and value_assignments_string_struct().
Definition at line 1047 of file string_abstraction.cpp.
References irept::id(), exprt::op0(), exprt::op1(), and exprt::type().
Referenced by abstract_assign(), and char_assign().
void string_abstractiont::operator() | ( | goto_programt & | dest | ) |
Definition at line 159 of file string_abstraction.cpp.
References goto_programt::clear(), goto_programt::destructive_append(), initialization, and goto_programt::swap().
void string_abstractiont::operator() | ( | goto_functionst & | dest | ) |
Definition at line 134 of file string_abstraction.cpp.
References add_str_arguments(), goto_programt::clear(), current_args, goto_programt::destructive_append(), goto_functionst::entry_point(), Forall_goto_functions, goto_functionst::function_map, id2string(), initialization, main(), and sym_suffix.
|
protected |
Definition at line 597 of file string_abstraction.cpp.
References build(), Forall_operands, irept::id(), IS_ZERO, LENGTH, exprt::op0(), exprt::operands(), SIZE, and irept::swap().
Referenced by abstract(), and abstract_assign().
|
protected |
Definition at line 1202 of file string_abstraction.cpp.
References struct_union_typet::components(), from_integer(), irept::id(), ns, string_struct, typet::subtype(), to_array_type(), to_if_expr(), to_integer(), to_struct_union_type(), exprt::type(), type_eq(), value_assignments_if(), and value_assignments_string_struct().
Referenced by abstract_pointer_assign(), and value_assignments_if().
|
protected |
Definition at line 1249 of file string_abstraction.cpp.
References goto_programt::add_instruction(), if_exprt::cond(), if_exprt::false_case(), GOTO, goto_programt::insert_before_swap(), SKIP, if_exprt::true_case(), and value_assignments().
Referenced by value_assignments().
|
protected |
Definition at line 1287 of file string_abstraction.cpp.
References goto_programt::add_instruction(), ASSIGN, goto_programt::insert_before_swap(), IS_ZERO, LENGTH, member(), and SIZE.
Referenced by value_assignments().
|
protected |
Definition at line 40 of file string_abstraction.h.
Referenced by build_abstraction_type(), and build_abstraction_type_rec().
|
protected |
Definition at line 33 of file string_abstraction.h.
Referenced by add_str_arguments(), and build_symbol().
|
protected |
Definition at line 42 of file string_abstraction.h.
Referenced by add_str_arguments(), build_symbol(), and operator()().
|
protected |
Definition at line 135 of file string_abstraction.h.
Referenced by build_new_symbol(), build_symbol_constant(), and operator()().
|
protected |
Definition at line 138 of file string_abstraction.h.
Referenced by abstract(), build_new_symbol(), build_unknown(), and declare_define_locals().
|
protected |
Definition at line 36 of file string_abstraction.h.
Referenced by abstract_assign(), abstract_function_call(), add_dummy_symbol_and_value(), build(), build_abstraction_type(), build_abstraction_type_rec(), build_symbol(), build_unknown(), build_wrap(), is_char_type(), is_ptr_string_struct(), make_decl_and_def(), make_type(), make_val_or_dummy_rec(), member(), and value_assignments().
|
protected |
Definition at line 134 of file string_abstraction.h.
Referenced by add_dummy_symbol_and_value(), build_abstraction_type_rec(), build_symbol_constant(), is_ptr_string_struct(), make_val_or_dummy_rec(), member(), string_abstractiont(), and value_assignments().
|
protected |
Definition at line 34 of file string_abstraction.h.
Referenced by build_new_symbol(), build_symbol(), and operator()().
|
protected |
Definition at line 35 of file string_abstraction.h.
Referenced by add_argument(), add_dummy_symbol_and_value(), add_str_arguments(), build_new_symbol(), build_symbol(), build_symbol_constant(), and build_unknown().
|
protected |
Definition at line 37 of file string_abstraction.h.
Referenced by build_unknown().