cprover
simple_insertiont Class Referenceabstract
Inheritance diagram for simple_insertiont:
[legend]
Collaboration diagram for simple_insertiont:
[legend]

Public Member Functions

 simple_insertiont (messaget &_message, value_setst &_value_sets, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
 
virtual ~simple_insertiont ()
 
void do_it ()
 

Protected Member Functions

virtual void compute ()=0
 
void print_to_file () const
 

Protected Attributes

messagetmessage
 
value_setstvalue_sets
 
const symbol_tabletsymbol_table
 
const namespacet ns
 
const goto_functionstgoto_functions
 
struct {
   std::list< symbol_exprt >   writes
 
   std::list< symbol_exprt >   reads
 
fenced_edges
 

Detailed Description

Definition at line 35 of file fence_shared.cpp.

Constructor & Destructor Documentation

§ simple_insertiont()

simple_insertiont::simple_insertiont ( messaget _message,
value_setst _value_sets,
const symbol_tablet _symbol_table,
const goto_functionst _goto_functions 
)
inlineexplicit

Definition at line 108 of file fence_shared.cpp.

§ ~simple_insertiont()

virtual simple_insertiont::~simple_insertiont ( )
inlinevirtual

Definition at line 117 of file fence_shared.cpp.

Member Function Documentation

§ compute()

virtual void simple_insertiont::compute ( )
protectedpure virtual

Implemented in fence_volatilet, fence_all_shared_aegt, and fence_all_sharedt.

Referenced by do_it().

§ do_it()

void simple_insertiont::do_it ( )
inline

Definition at line 119 of file fence_shared.cpp.

References compute(), and print_to_file().

Referenced by fence_all_shared(), fence_all_shared_aeg(), and fence_volatile().

§ print_to_file()

void simple_insertiont::print_to_file ( ) const
inlineprotected

Definition at line 53 of file fence_shared.cpp.

References fenced_edges, namespacet::lookup(), and OUTPUT.

Referenced by do_it().

Member Data Documentation

§ fenced_edges

§ goto_functions

§ message

§ ns

const namespacet simple_insertiont::ns
protected

§ reads

std::list<symbol_exprt> simple_insertiont::reads

Definition at line 47 of file fence_shared.cpp.

§ symbol_table

const symbol_tablet& simple_insertiont::symbol_table
protected

Definition at line 40 of file fence_shared.cpp.

Referenced by fence_volatilet::is_volatile().

§ value_sets

value_setst& simple_insertiont::value_sets
protected

§ writes

std::list<symbol_exprt> simple_insertiont::writes

Definition at line 46 of file fence_shared.cpp.


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