cprover
string_abstractiont Class Reference

Replace all uses of char * by a struct that carries that string, and also the underlying allocation and the C string length. More...

#include <string_abstraction.h>

+ Inheritance diagram for string_abstractiont:
+ Collaboration diagram for string_abstractiont:

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 message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. 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::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 commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 
- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 

Detailed Description

Replace all uses of char * by a struct that carries that string, and also the underlying allocation and the C string length.

This will become useful (with some modifications) for supporting strings in the C frontend, as the string solver expects a struct that bundles the string length and the underlying character array.

Definition at line 27 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 44 of file string_abstraction.h.

◆ localst

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

Definition at line 139 of file string_abstraction.h.

Member Enumeration Documentation

◆ whatt

enum string_abstractiont::whatt
strongprotected
Enumerator
IS_ZERO 
LENGTH 
SIZE 

Definition at line 108 of file string_abstraction.h.

Constructor & Destructor Documentation

◆ string_abstractiont()

string_abstractiont::string_abstractiont ( symbol_tablet _symbol_table,
message_handlert _message_handler 
)

Definition at line 93 of file string_abstraction.cpp.

Member Function Documentation

◆ abstract() [1/2]

void string_abstractiont::abstract ( goto_programt dest)
protected

Definition at line 226 of file string_abstraction.cpp.

◆ abstract() [2/2]

goto_programt::targett string_abstractiont::abstract ( goto_programt dest,
goto_programt::targett  it 
)
protected

Definition at line 440 of file string_abstraction.cpp.

◆ abstract_assign()

goto_programt::targett string_abstractiont::abstract_assign ( goto_programt dest,
goto_programt::targett  it 
)
protected

Definition at line 493 of file string_abstraction.cpp.

◆ abstract_char_assign()

goto_programt::targett string_abstractiont::abstract_char_assign ( goto_programt dest,
goto_programt::targett  it 
)
protected

Definition at line 1104 of file string_abstraction.cpp.

◆ abstract_function_call()

void string_abstractiont::abstract_function_call ( goto_programt::targett  it)
protected

Definition at line 525 of file string_abstraction.cpp.

◆ abstract_pointer_assign()

goto_programt::targett string_abstractiont::abstract_pointer_assign ( goto_programt dest,
goto_programt::targett  it 
)
protected

Definition at line 1062 of file string_abstraction.cpp.

◆ 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

Definition at line 198 of file string_abstraction.cpp.

◆ add_dummy_symbol_and_value()

symbol_exprt string_abstractiont::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 
)
protected

Definition at line 376 of file string_abstraction.cpp.

◆ add_str_arguments()

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

Definition at line 162 of file string_abstraction.cpp.

◆ build() [1/2]

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

Definition at line 741 of file string_abstraction.cpp.

◆ build() [2/2]

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

Definition at line 626 of file string_abstraction.cpp.

◆ build_abstraction_type()

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

Definition at line 660 of file string_abstraction.cpp.

◆ build_abstraction_type_rec()

const typet & string_abstractiont::build_abstraction_type_rec ( const typet type,
const abstraction_types_mapt known 
)
protected

Definition at line 679 of file string_abstraction.cpp.

◆ build_array()

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

Definition at line 839 of file string_abstraction.cpp.

◆ build_if()

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

Definition at line 811 of file string_abstraction.cpp.

◆ build_new_symbol()

void string_abstractiont::build_new_symbol ( const symbolt symbol,
const irep_idt identifier,
const typet type 
)
protected

Definition at line 975 of file string_abstraction.cpp.

◆ build_pointer()

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

Definition at line 865 of file string_abstraction.cpp.

◆ build_symbol()

bool string_abstractiont::build_symbol ( const symbol_exprt sym,
exprt dest 
)
protected

Definition at line 948 of file string_abstraction.cpp.

◆ build_symbol_constant()

bool string_abstractiont::build_symbol_constant ( const mp_integer zero_length,
const mp_integer buf_size,
exprt dest 
)
protected

Definition at line 1007 of file string_abstraction.cpp.

◆ build_type()

typet string_abstractiont::build_type ( whatt  what)
staticprotected

Definition at line 113 of file string_abstraction.cpp.

◆ build_unknown() [1/2]

exprt string_abstractiont::build_unknown ( const typet type,
bool  write 
)
protected

Definition at line 921 of file string_abstraction.cpp.

◆ build_unknown() [2/2]

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

Definition at line 897 of file string_abstraction.cpp.

◆ build_wrap()

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

Definition at line 25 of file string_abstraction.cpp.

◆ 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

Definition at line 1169 of file string_abstraction.cpp.

◆ declare_define_locals()

void string_abstractiont::declare_define_locals ( goto_programt dest)
protected

Definition at line 241 of file string_abstraction.cpp.

◆ has_string_macros()

bool string_abstractiont::has_string_macros ( const exprt expr)
staticprotected

Definition at line 581 of file string_abstraction.cpp.

◆ is_char_type()

bool string_abstractiont::is_char_type ( const typet type) const
inlineprotected

Definition at line 58 of file string_abstraction.h.

◆ is_ptr_string_struct()

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

Definition at line 55 of file string_abstraction.cpp.

◆ 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

Definition at line 276 of file string_abstraction.cpp.

◆ make_type()

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

Definition at line 69 of file string_abstraction.h.

◆ make_val_or_dummy_rec()

exprt string_abstractiont::make_val_or_dummy_rec ( goto_programt dest,
goto_programt::targett  ref_instr,
const symbolt symbol,
const typet source_type 
)
protected

Definition at line 306 of file string_abstraction.cpp.

◆ member()

exprt string_abstractiont::member ( const exprt a,
whatt  what 
)
protected

Definition at line 1320 of file string_abstraction.cpp.

◆ move_lhs_arithmetic()

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

Definition at line 1050 of file string_abstraction.cpp.

◆ operator()() [1/2]

void string_abstractiont::operator() ( goto_functionst dest)

Definition at line 127 of file string_abstraction.cpp.

◆ operator()() [2/2]

void string_abstractiont::operator() ( goto_programt dest)

Definition at line 152 of file string_abstraction.cpp.

◆ replace_string_macros()

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

Definition at line 595 of file string_abstraction.cpp.

◆ value_assignments()

goto_programt::targett string_abstractiont::value_assignments ( goto_programt dest,
goto_programt::targett  it,
const exprt lhs,
const exprt rhs 
)
protected

Definition at line 1202 of file string_abstraction.cpp.

◆ 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

Definition at line 1249 of file string_abstraction.cpp.

◆ 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

Definition at line 1280 of file string_abstraction.cpp.

Member Data Documentation

◆ abstraction_types_map

abstraction_types_mapt string_abstractiont::abstraction_types_map
protected

Definition at line 45 of file string_abstraction.h.

◆ arg_suffix

const std::string string_abstractiont::arg_suffix
protected

Definition at line 38 of file string_abstraction.h.

◆ current_args

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

Definition at line 47 of file string_abstraction.h.

◆ initialization

goto_programt string_abstractiont::initialization
protected

Definition at line 137 of file string_abstraction.h.

◆ locals

localst string_abstractiont::locals
protected

Definition at line 140 of file string_abstraction.h.

◆ ns

namespacet string_abstractiont::ns
protected

Definition at line 41 of file string_abstraction.h.

◆ string_struct

typet string_abstractiont::string_struct
protected

Definition at line 136 of file string_abstraction.h.

◆ sym_suffix

std::string string_abstractiont::sym_suffix
protected

Definition at line 39 of file string_abstraction.h.

◆ symbol_table

symbol_tablet& string_abstractiont::symbol_table
protected

Definition at line 40 of file string_abstraction.h.

◆ temporary_counter

unsigned string_abstractiont::temporary_counter
protected

Definition at line 42 of file string_abstraction.h.


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