cprover
function_modifiest Class Reference

#include <function_modifies.h>

Collaboration diagram for function_modifiest:
[legend]

Public Types

typedef std::set< exprtmodifiest
 

Public Member Functions

 function_modifiest (const goto_functionst &_goto_functions)
 
void get_modifies (const local_may_aliast &local_may_alias, const goto_programt::const_targett, modifiest &)
 
void get_modifies_lhs (const local_may_aliast &, const goto_programt::const_targett, const exprt &lhs, modifiest &)
 
void get_modifies_function (const exprt &, modifiest &)
 
void operator() (const exprt &function, modifiest &modifies)
 

Protected Types

typedef std::map< irep_idt, modifiestfunction_mapt
 

Protected Attributes

const goto_functionstgoto_functions
 
function_mapt function_map
 

Detailed Description

Definition at line 18 of file function_modifies.h.

Member Typedef Documentation

§ function_mapt

Definition at line 51 of file function_modifies.h.

§ modifiest

Definition at line 26 of file function_modifies.h.

Constructor & Destructor Documentation

§ function_modifiest()

function_modifiest::function_modifiest ( const goto_functionst _goto_functions)
inlineexplicit

Definition at line 21 of file function_modifies.h.

Member Function Documentation

§ get_modifies()

§ get_modifies_function()

void function_modifiest::get_modifies_function ( const exprt function,
modifiest modifies 
)

§ get_modifies_lhs()

void function_modifiest::get_modifies_lhs ( const local_may_aliast local_may_alias,
const goto_programt::const_targett  t,
const exprt lhs,
modifiest modifies 
)

§ operator()()

void function_modifiest::operator() ( const exprt function,
modifiest modifies 
)
inline

Definition at line 43 of file function_modifies.h.

References get_modifies_function().

Member Data Documentation

§ function_map

function_mapt function_modifiest::function_map
protected

Definition at line 52 of file function_modifies.h.

Referenced by get_modifies_function().

§ goto_functions

const goto_functionst& function_modifiest::goto_functions
protected

Definition at line 49 of file function_modifies.h.

Referenced by get_modifies_function().


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