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)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...
 

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_idtlocalst
 

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 unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
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> 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()

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

◆ declare_define_locals()

void string_abstractiont::declare_define_locals ( goto_programt dest)
protected

◆ has_string_macros()

bool string_abstractiont::has_string_macros ( const exprt expr)
staticprotected

Definition at line 583 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 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().

◆ make_decl_and_def()

void string_abstractiont::make_decl_and_def ( goto_programt dest,
goto_programt::targett  ref_instr,
const irep_idt identifier,
const irep_idt source_sym 
)
protected

◆ make_type()

void string_abstractiont::make_type ( exprt dest,
const typet type 
)
inlineprotected

◆ make_val_or_dummy_rec()

◆ member()

◆ move_lhs_arithmetic()

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

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().

◆ operator()() [1/2]

void string_abstractiont::operator() ( goto_programt dest)

◆ 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()

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

◆ 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: