12 #ifndef CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H 13 #define CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H 55 if(type.
id()==ID_symbol)
58 if(type.
id()!=ID_signedbv &&
59 type.
id()!=ID_unsignedbv)
110 const exprt &pointer,
137 typedef std::unordered_map<irep_idt, irep_idt, irep_id_hash>
localst;
166 const typet &source_type);
183 #endif // CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H goto_programt::targett abstract_pointer_assign(goto_programt &dest, goto_programt::targett it)
The type of an expression.
bool build_array(const array_exprt &object, exprt &dest, bool write)
const typet & follow(const typet &src) const
struct configt::ansi_ct ansi_c
const std::string arg_suffix
const typet & build_abstraction_type_rec(const typet &type, const abstraction_types_mapt &known)
void make_type(exprt &dest, const typet &type)
exprt build_unknown(whatt what, bool write)
goto_programt::targett char_assign(goto_programt &dest, goto_programt::targett target, const exprt &new_lhs, const exprt &lhs, const exprt &rhs)
goto_programt initialization
goto_programt::targett abstract_char_assign(goto_programt &dest, goto_programt::targett it)
void declare_define_locals(goto_programt &dest)
void move_lhs_arithmetic(exprt &lhs, exprt &rhs)
Goto Programs with Functions.
std::vector< parametert > parameterst
bool build_wrap(const exprt &object, exprt &dest, bool write)
void build_new_symbol(const symbolt &symbol, const irep_idt &identifier, const typet &type)
The trinary if-then-else operator.
static typet build_type(whatt what)
void add_str_arguments(const irep_idt &name, goto_functionst::goto_functiont &fct)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void add_argument(code_typet::parameterst &str_args, const symbolt &fct_symbol, const typet &type, const irep_idt &base_name, const irep_idt &identifier)
void make_decl_and_def(goto_programt &dest, goto_programt::targett ref_instr, const irep_idt &identifier, const irep_idt &source_sym)
const irep_idt & id() const
::std::set< irep_idt > current_args
void replace_string_macros(exprt &expr, bool lhs, const source_locationt &)
bool build_symbol(const symbol_exprt &sym, exprt &dest)
bool build_symbol_constant(const mp_integer &zero_length, const mp_integer &buf_size, exprt &dest)
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
bool is_char_type(const typet &type) const
::std::map< typet, typet > abstraction_types_mapt
goto_programt::targett abstract_assign(goto_programt &dest, goto_programt::targett it)
API to expression classes.
exprt make_val_or_dummy_rec(goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const typet &source_type)
symbol_tablet & symbol_table
std::unordered_map< irep_idt, irep_idt, irep_id_hash > localst
exprt build(const exprt &pointer, whatt what, bool write, const source_locationt &)
goto_function_templatet< goto_programt > goto_functiont
goto_programt::targett value_assignments(goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt &rhs)
goto_programt::targett value_assignments_string_struct(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt &rhs)
const typet & build_abstraction_type(const typet &type)
std::size_t get_width() const
void abstract_function_call(goto_programt &dest, goto_programt::targett it)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
void operator()(goto_programt &dest)
string_abstractiont(symbol_tablet &_symbol_table, message_handlert &_message_handler)
Base class for all expressions.
symbol_exprt add_dummy_symbol_and_value(goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const irep_idt &component_name, const typet &type, const typet &source_type)
unsigned temporary_counter
bool build_pointer(const exprt &object, exprt &dest, bool write)
bool build_if(const if_exprt &o_if, exprt &dest, bool write)
Expression to hold a symbol (variable)
bool is_ptr_string_struct(const typet &type) const
goto_programt::targett value_assignments_if(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const if_exprt &rhs)
static bool has_string_macros(const exprt &expr)
exprt member(const exprt &a, whatt what)
abstraction_types_mapt abstraction_types_map
void make_typecast(const typet &_type)
array constructor from list of elements
instructionst::iterator targett
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.