cprover
string_instrumentationt Class Reference
Inheritance diagram for string_instrumentationt:
[legend]
Collaboration diagram for string_instrumentationt:
[legend]

Public Member Functions

 string_instrumentationt (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 Member Functions

void make_type (exprt &dest, const typet &type)
 
void instrument (goto_programt &dest, goto_programt::targett it)
 
void do_function_call (goto_programt &dest, goto_programt::targett it)
 
void do_sprintf (goto_programt &dest, goto_programt::targett it, code_function_callt &call)
 
void do_snprintf (goto_programt &dest, goto_programt::targett it, code_function_callt &call)
 
void do_strcat (goto_programt &dest, goto_programt::targett it, code_function_callt &call)
 
void do_strncmp (goto_programt &dest, goto_programt::targett it, code_function_callt &call)
 
void do_strchr (goto_programt &dest, goto_programt::targett it, code_function_callt &call)
 
void do_strrchr (goto_programt &dest, goto_programt::targett it, code_function_callt &call)
 
void do_strstr (goto_programt &dest, goto_programt::targett it, code_function_callt &call)
 
void do_strtok (goto_programt &dest, goto_programt::targett it, code_function_callt &call)
 
void do_strerror (goto_programt &dest, goto_programt::targett it, code_function_callt &call)
 
void do_fscanf (goto_programt &dest, goto_programt::targett it, code_function_callt &call)
 
void do_format_string_read (goto_programt &dest, goto_programt::const_targett target, const code_function_callt::argumentst &arguments, std::size_t format_string_inx, std::size_t argument_start_inx, const std::string &function_name)
 
void do_format_string_write (goto_programt &dest, goto_programt::const_targett target, const code_function_callt::argumentst &arguments, std::size_t format_string_inx, std::size_t argument_start_inx, const std::string &function_name)
 
bool is_string_type (const typet &t) const
 
void invalidate_buffer (goto_programt &dest, goto_programt::const_targett target, const exprt &buffer, const typet &buf_type, const mp_integer &limit)
 

Protected Attributes

symbol_tabletsymbol_table
 
namespacet ns
 
- 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 55 of file string_instrumentation.cpp.

Constructor & Destructor Documentation

◆ string_instrumentationt()

string_instrumentationt::string_instrumentationt ( symbol_tablet _symbol_table,
message_handlert _message_handler 
)
inline

Definition at line 58 of file string_instrumentation.cpp.

Member Function Documentation

◆ do_format_string_read()

void string_instrumentationt::do_format_string_read ( goto_programt dest,
goto_programt::const_targett  target,
const code_function_callt::argumentst arguments,
std::size_t  format_string_inx,
std::size_t  argument_start_inx,
const std::string &  function_name 
)
protected

◆ do_format_string_write()

void string_instrumentationt::do_format_string_write ( goto_programt dest,
goto_programt::const_targett  target,
const code_function_callt::argumentst arguments,
std::size_t  format_string_inx,
std::size_t  argument_start_inx,
const std::string &  function_name 
)
protected

◆ do_fscanf()

◆ do_function_call()

◆ do_snprintf()

◆ do_sprintf()

◆ do_strcat()

void string_instrumentationt::do_strcat ( goto_programt dest,
goto_programt::targett  it,
code_function_callt call 
)
protected

◆ do_strchr()

◆ do_strerror()

◆ do_strncmp()

void string_instrumentationt::do_strncmp ( goto_programt dest,
goto_programt::targett  it,
code_function_callt call 
)
protected

Definition at line 637 of file string_instrumentation.cpp.

Referenced by do_function_call().

◆ do_strrchr()

◆ do_strstr()

◆ do_strtok()

◆ instrument()

void string_instrumentationt::instrument ( goto_programt dest,
goto_programt::targett  it 
)
protected

Definition at line 202 of file string_instrumentation.cpp.

References ASSIGN, do_function_call(), and FUNCTION_CALL.

Referenced by operator()().

◆ invalidate_buffer()

◆ is_string_type()

bool string_instrumentationt::is_string_type ( const typet t) const
inlineprotected

◆ make_type()

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

Definition at line 74 of file string_instrumentation.cpp.

References namespace_baset::follow(), exprt::make_typecast(), ns, and exprt::type().

Referenced by do_strerror().

◆ operator()() [1/2]

void string_instrumentationt::operator() ( goto_programt dest)

Definition at line 196 of file string_instrumentation.cpp.

References Forall_goto_program_instructions, and instrument().

◆ operator()() [2/2]

void string_instrumentationt::operator() ( goto_functionst dest)

Definition at line 185 of file string_instrumentation.cpp.

References goto_functionst::function_map.

Member Data Documentation

◆ ns

namespacet string_instrumentationt::ns
protected

◆ symbol_table

symbol_tablet& string_instrumentationt::symbol_table
protected

Definition at line 71 of file string_instrumentation.cpp.

Referenced by do_strerror(), and invalidate_buffer().


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