CBMC
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
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 52 of file string_instrumentation.cpp.

Constructor & Destructor Documentation

◆ string_instrumentationt()

string_instrumentationt::string_instrumentationt ( symbol_table_baset &  _symbol_table)
inlineexplicit

Definition at line 55 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 356 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 450 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 327 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 203 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 290 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 254 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 604 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 712 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 596 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 627 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 650 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 681 of file string_instrumentation.cpp.

◆ instrument()

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

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

◆ is_string_type()

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

Definition at line 138 of file string_instrumentation.cpp.

◆ operator()() [1/2]

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

Definition at line 178 of file string_instrumentation.cpp.

◆ operator()() [2/2]

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

Definition at line 189 of file string_instrumentation.cpp.

Member Data Documentation

◆ ns

namespacet string_instrumentationt::ns
protected

Definition at line 65 of file string_instrumentation.cpp.

◆ symbol_table

symbol_table_baset& string_instrumentationt::symbol_table
protected

Definition at line 64 of file string_instrumentation.cpp.

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