cprover
Loading...
Searching...
No Matches
string_instrumentationt Class Reference
Collaboration diagram for string_instrumentationt:

Public Member Functions

 string_instrumentationt (symbol_table_baset &_symbol_table)
void operator() (goto_programt &dest)
void operator() (goto_functionst &dest)

Protected Member Functions

void instrument (goto_programt &dest, goto_programt::targett it)
void do_function_call (goto_programt &dest, goto_programt::targett target)
void do_sprintf (goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
void do_snprintf (goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
void do_strcat (goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt::operandst &arguments)
void do_strncmp (goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt::operandst &arguments)
void do_strchr (goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
void do_strrchr (goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
void do_strstr (goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
void do_strtok (goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
void do_strerror (goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt::operandst &arguments)
void do_fscanf (goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
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_table_baset & symbol_table
namespacet ns

Detailed Description

Definition at line 51 of file string_instrumentation.cpp.

Constructor & Destructor Documentation

◆ string_instrumentationt()

string_instrumentationt::string_instrumentationt ( symbol_table_baset & _symbol_table)
inlineexplicit

Definition at line 54 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

Definition at line 351 of file string_instrumentation.cpp.

◆ 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

Definition at line 447 of file string_instrumentation.cpp.

◆ do_fscanf()

void string_instrumentationt::do_fscanf ( goto_programt & dest,
goto_programt::targett target,
const exprt & lhs,
const exprt::operandst & arguments )
protected

Definition at line 322 of file string_instrumentation.cpp.

◆ do_function_call()

void string_instrumentationt::do_function_call ( goto_programt & dest,
goto_programt::targett target )
protected

Definition at line 199 of file string_instrumentation.cpp.

◆ do_snprintf()

void string_instrumentationt::do_snprintf ( goto_programt & dest,
goto_programt::targett target,
const exprt & lhs,
const exprt::operandst & arguments )
protected

Definition at line 285 of file string_instrumentation.cpp.

◆ do_sprintf()

void string_instrumentationt::do_sprintf ( goto_programt & dest,
goto_programt::targett target,
const exprt & lhs,
const exprt::operandst & arguments )
protected

Definition at line 249 of file string_instrumentation.cpp.

◆ do_strcat()

void string_instrumentationt::do_strcat ( goto_programt & dest,
goto_programt::targett it,
const exprt & lhs,
const exprt::operandst & arguments )
protected

◆ do_strchr()

void string_instrumentationt::do_strchr ( goto_programt & dest,
goto_programt::targett target,
const exprt & lhs,
const exprt::operandst & arguments )
protected

Definition at line 599 of file string_instrumentation.cpp.

◆ do_strerror()

void string_instrumentationt::do_strerror ( goto_programt & dest,
goto_programt::targett it,
const exprt & lhs,
const exprt::operandst & arguments )
protected

Definition at line 707 of file string_instrumentation.cpp.

◆ do_strncmp()

void string_instrumentationt::do_strncmp ( goto_programt & dest,
goto_programt::targett it,
const exprt & lhs,
const exprt::operandst & arguments )
protected

Definition at line 591 of file string_instrumentation.cpp.

◆ do_strrchr()

void string_instrumentationt::do_strrchr ( goto_programt & dest,
goto_programt::targett target,
const exprt & lhs,
const exprt::operandst & arguments )
protected

Definition at line 622 of file string_instrumentation.cpp.

◆ do_strstr()

void string_instrumentationt::do_strstr ( goto_programt & dest,
goto_programt::targett target,
const exprt & lhs,
const exprt::operandst & arguments )
protected

Definition at line 645 of file string_instrumentation.cpp.

◆ do_strtok()

void string_instrumentationt::do_strtok ( goto_programt & dest,
goto_programt::targett target,
const exprt & lhs,
const exprt::operandst & arguments )
protected

Definition at line 676 of file string_instrumentation.cpp.

◆ instrument()

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

Definition at line 191 of file string_instrumentation.cpp.

◆ invalidate_buffer()

void string_instrumentationt::invalidate_buffer ( goto_programt & dest,
goto_programt::const_targett target,
const exprt & buffer,
const typet & buf_type,
const mp_integer & limit )
protected

Definition at line 786 of file string_instrumentation.cpp.

◆ is_string_type()

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

Definition at line 137 of file string_instrumentation.cpp.

◆ operator()() [1/2]

void string_instrumentationt::operator() ( goto_functionst & dest)

Definition at line 175 of file string_instrumentation.cpp.

◆ operator()() [2/2]

void string_instrumentationt::operator() ( goto_programt & dest)

Definition at line 185 of file string_instrumentation.cpp.

Member Data Documentation

◆ ns

namespacet string_instrumentationt::ns
protected

Definition at line 64 of file string_instrumentation.cpp.

◆ symbol_table

symbol_table_baset& string_instrumentationt::symbol_table
protected

Definition at line 63 of file string_instrumentation.cpp.

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