cprover
string_abstractiont Class Reference

#include <string_abstraction.h>

Inheritance diagram for string_abstractiont:
[legend]
Collaboration diagram for string_abstractiont:
[legend]

Public Member Functions

 string_abstractiont (symbol_tablet &_symbol_table, message_handlert &_message_handler)
 
void operator() (goto_programt &dest)
 
void operator() (goto_functionst &dest)
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

Protected Types

enum  whatt { whatt::IS_ZERO, whatt::LENGTH, whatt::SIZE }
 
typedef ::std::map< typet, typetabstraction_types_mapt
 
typedef std::unordered_map< irep_idt, irep_idt, irep_id_hashlocalst
 

Protected Member Functions

void replace_string_macros (exprt &expr, bool lhs, const source_locationt &)
 
void move_lhs_arithmetic (exprt &lhs, exprt &rhs)
 
bool is_char_type (const typet &type) const
 
bool is_ptr_string_struct (const typet &type) const
 
void make_type (exprt &dest, const typet &type)
 
goto_programt::targett abstract (goto_programt &dest, goto_programt::targett it)
 
goto_programt::targett abstract_assign (goto_programt &dest, goto_programt::targett it)
 
goto_programt::targett abstract_pointer_assign (goto_programt &dest, goto_programt::targett it)
 
goto_programt::targett abstract_char_assign (goto_programt &dest, goto_programt::targett it)
 
goto_programt::targett char_assign (goto_programt &dest, goto_programt::targett target, const exprt &new_lhs, const exprt &lhs, const exprt &rhs)
 
void abstract_function_call (goto_programt &dest, goto_programt::targett it)
 
goto_programt::targett value_assignments (goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt &rhs)
 
goto_programt::targett value_assignments_if (goto_programt &dest, goto_programt::targett target, const exprt &lhs, const if_exprt &rhs)
 
goto_programt::targett value_assignments_string_struct (goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt &rhs)
 
exprt build (const exprt &pointer, whatt what, bool write, const source_locationt &)
 
bool build (const exprt &object, exprt &dest, bool write)
 
bool build_wrap (const exprt &object, exprt &dest, bool write)
 
bool build_if (const if_exprt &o_if, exprt &dest, bool write)
 
bool build_array (const array_exprt &object, exprt &dest, bool write)
 
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)
 
exprt build_unknown (whatt what, bool write)
 
exprt build_unknown (const typet &type, bool write)
 
const typetbuild_abstraction_type (const typet &type)
 
const typetbuild_abstraction_type_rec (const typet &type, const abstraction_types_mapt &known)
 
bool build_pointer (const exprt &object, exprt &dest, bool write)
 
void build_new_symbol (const symbolt &symbol, const irep_idt &identifier, const typet &type)
 
exprt member (const exprt &a, whatt what)
 
void abstract (goto_programt &dest)
 
void add_str_arguments (const irep_idt &name, goto_functionst::goto_functiont &fct)
 
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)
 
exprt make_val_or_dummy_rec (goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const typet &source_type)
 
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)
 
void declare_define_locals (goto_programt &dest)
 

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_tabletsymbol_table
 
namespacet ns
 
unsigned temporary_counter
 
abstraction_types_mapt abstraction_types_map
 
::std::set< irep_idtcurrent_args
 
typet string_struct
 
goto_programt initialization
 
localst locals
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 22 of file string_abstraction.h.

Member Typedef Documentation

§ abstraction_types_mapt

typedef ::std::map< typet, typet > string_abstractiont::abstraction_types_mapt
protected

Definition at line 39 of file string_abstraction.h.

§ localst

typedef std::unordered_map<irep_idt, irep_idt, irep_id_hash> string_abstractiont::localst
protected

Definition at line 137 of file string_abstraction.h.

Member Enumeration Documentation

§ whatt

enum string_abstractiont::whatt
strongprotected
Enumerator
IS_ZERO 
LENGTH 
SIZE 

Definition at line 106 of file string_abstraction.h.

Constructor & Destructor Documentation

§ string_abstractiont()

string_abstractiont::string_abstractiont ( symbol_tablet _symbol_table,
message_handlert _message_handler 
)

Member Function Documentation

§ abstract() [1/2]

§ abstract() [2/2]

void string_abstractiont::abstract ( goto_programt dest)
protected

§ abstract_assign()

§ abstract_char_assign()

§ abstract_function_call()

§ abstract_pointer_assign()

§ add_argument()

void string_abstractiont::add_argument ( code_typet::parameterst str_args,
const symbolt fct_symbol,
const typet type,
const irep_idt base_name,
const irep_idt identifier 
)
protected

§ add_dummy_symbol_and_value()

§ add_str_arguments()

void string_abstractiont::add_str_arguments ( const irep_idt name,
goto_functionst::goto_functiont fct 
)
protected

§ build() [1/2]

exprt string_abstractiont::build ( const exprt pointer,
whatt  what,
bool  write,
const source_locationt source_location 
)
protected

§ build() [2/2]

§ build_abstraction_type()

const typet & string_abstractiont::build_abstraction_type ( const typet type)
protected

§ build_abstraction_type_rec()

§ build_array()

bool string_abstractiont::build_array ( const array_exprt object,
exprt dest,
bool  write 
)
protected

§ build_if()

bool string_abstractiont::build_if ( const if_exprt o_if,
exprt dest,
bool  write 
)
protected

§ build_new_symbol()

§ build_pointer()

bool string_abstractiont::build_pointer ( const exprt object,
exprt dest,
bool  write 
)
protected

§ build_symbol()

§ build_symbol_constant()

§ build_type()

typet string_abstractiont::build_type ( whatt  what)
staticprotected

§ build_unknown() [1/2]

exprt string_abstractiont::build_unknown ( whatt  what,
bool  write 
)
protected

§ build_unknown() [2/2]

§ build_wrap()

bool string_abstractiont::build_wrap ( const exprt object,
exprt dest,
bool  write 
)
protected

§ char_assign()

§ declare_define_locals()

§ has_string_macros()

bool string_abstractiont::has_string_macros ( const exprt expr)
staticprotected

Definition at line 578 of file string_abstraction.cpp.

References forall_operands, and irept::id().

Referenced by abstract(), and abstract_assign().

§ is_char_type()

§ is_ptr_string_struct()

bool string_abstractiont::is_ptr_string_struct ( const typet type) const
protected

Definition at line 56 of file string_abstraction.cpp.

References irept::id(), ns, string_struct, typet::subtype(), and type_eq().

Referenced by is_char_type(), make_val_or_dummy_rec(), and member().

§ make_decl_and_def()

§ make_type()

§ make_val_or_dummy_rec()

§ member()

§ move_lhs_arithmetic()

void string_abstractiont::move_lhs_arithmetic ( exprt lhs,
exprt rhs 
)
protected

Definition at line 1038 of file string_abstraction.cpp.

References irept::id(), exprt::op0(), exprt::op1(), and exprt::type().

Referenced by abstract_assign(), and char_assign().

§ operator()() [1/2]

§ operator()() [2/2]

§ replace_string_macros()

void string_abstractiont::replace_string_macros ( exprt expr,
bool  lhs,
const source_locationt source_location 
)
protected

§ value_assignments()

§ value_assignments_if()

§ value_assignments_string_struct()

goto_programt::targett string_abstractiont::value_assignments_string_struct ( goto_programt dest,
goto_programt::targett  target,
const exprt lhs,
const exprt rhs 
)
protected

Member Data Documentation

§ abstraction_types_map

abstraction_types_mapt string_abstractiont::abstraction_types_map
protected

Definition at line 40 of file string_abstraction.h.

Referenced by build_abstraction_type(), and build_abstraction_type_rec().

§ arg_suffix

const std::string string_abstractiont::arg_suffix
protected

Definition at line 33 of file string_abstraction.h.

Referenced by add_str_arguments(), and build_symbol().

§ current_args

::std::set< irep_idt > string_abstractiont::current_args
protected

Definition at line 42 of file string_abstraction.h.

Referenced by add_str_arguments(), build_symbol(), and operator()().

§ initialization

goto_programt string_abstractiont::initialization
protected

Definition at line 135 of file string_abstraction.h.

Referenced by build_new_symbol(), build_symbol_constant(), and operator()().

§ locals

localst string_abstractiont::locals
protected

§ ns

§ string_struct

§ sym_suffix

std::string string_abstractiont::sym_suffix
protected

Definition at line 34 of file string_abstraction.h.

Referenced by build_new_symbol(), build_symbol(), and operator()().

§ symbol_table

§ temporary_counter

unsigned string_abstractiont::temporary_counter
protected

Definition at line 37 of file string_abstraction.h.

Referenced by build_unknown().


The documentation for this class was generated from the following files: