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)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

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, unsigned format_string_inx, unsigned 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, unsigned format_string_inx, unsigned 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 mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 53 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 56 of file string_instrumentation.cpp.

References operator()().

Member Function Documentation

§ do_format_string_read()

§ do_format_string_write()

§ 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

Referenced by make_type().

§ 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 632 of file string_instrumentation.cpp.

Referenced by do_function_call(), and make_type().

§ do_strrchr()

§ do_strstr()

§ do_strtok()

§ instrument()

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

Definition at line 190 of file string_instrumentation.cpp.

References ASSIGN, do_function_call(), and FUNCTION_CALL.

Referenced by make_type(), and operator()().

§ invalidate_buffer()

§ is_string_type()

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

§ make_type()

§ operator()() [1/2]

void string_instrumentationt::operator() ( goto_programt dest)

Definition at line 184 of file string_instrumentation.cpp.

References Forall_goto_program_instructions, and instrument().

Referenced by string_instrumentationt().

§ operator()() [2/2]

void string_instrumentationt::operator() ( goto_functionst dest)

Member Data Documentation

§ ns

namespacet string_instrumentationt::ns
protected

§ symbol_table

symbol_tablet& string_instrumentationt::symbol_table
protected

Definition at line 69 of file string_instrumentation.cpp.

Referenced by do_strerror(), and invalidate_buffer().


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