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 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 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_basetsymbol_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 362 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 456 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 333 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 209 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 296 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 260 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 610 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 718 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 602 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 633 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 656 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 687 of file string_instrumentation.cpp.

◆ instrument()

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

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

◆ is_string_type()

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

Definition at line 144 of file string_instrumentation.cpp.

◆ make_type()

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

Definition at line 67 of file string_instrumentation.cpp.

◆ operator()() [1/2]

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

Definition at line 184 of file string_instrumentation.cpp.

◆ operator()() [2/2]

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

Definition at line 195 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: