cprover
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
fence_all_shared_aegt Class Reference
Inheritance diagram for fence_all_shared_aegt:
[legend]
Collaboration diagram for fence_all_shared_aegt:
[legend]

Public Member Functions

 fence_all_shared_aegt (messaget &_message, value_setst &_value_sets, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
 
- Public Member Functions inherited from fence_all_sharedt
 fence_all_sharedt (messaget &_message, value_setst &_value_sets, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
 
- Public Member Functions inherited from simple_insertiont
 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

void compute ()
 
void fence_all_shared_aeg_explore (const goto_programt &code)
 
- Protected Member Functions inherited from simple_insertiont
void print_to_file () const
 

Protected Attributes

std::set< irep_idt > visited_functions
 
- Protected Attributes inherited from simple_insertiont
messaget & message
 
value_setst & value_sets
 
const symbol_tablet & symbol_table
 
const namespacet ns
 
const goto_functionst & goto_functions
 
struct {
   std::list< symbol_exprt >   writes
 
   std::list< symbol_exprt >   reads
 
} fenced_edges
 

Detailed Description

Definition at line 143 of file fence_shared.cpp.

Constructor & Destructor Documentation

◆ fence_all_shared_aegt()

fence_all_shared_aegt::fence_all_shared_aegt ( messaget &  _message,
value_setst &  _value_sets,
const symbol_tablet &  _symbol_table,
const goto_functionst &  _goto_functions 
)
inline

Definition at line 155 of file fence_shared.cpp.

Member Function Documentation

◆ compute()

void fence_all_shared_aegt::compute ( )
protectedvirtual

Reimplemented from fence_all_sharedt.

Definition at line 415 of file fence_shared.cpp.

References goto_functions_templatet< goto_programt >::entry_point(), messaget::eom(), fence_all_shared_aeg_explore(), goto_functions_templatet< bodyT >::function_map, simple_insertiont::goto_functions, main(), simple_insertiont::message, and messaget::status().

◆ fence_all_shared_aeg_explore()

void fence_all_shared_aegt::fence_all_shared_aeg_explore ( const goto_programt &  code)
protected

Definition at line 432 of file fence_shared.cpp.

References CPROVER_PREFIX, messaget::debug(), rw_set_with_trackt::dereferenced_from, goto_functions_templatet< goto_programt >::entry_point(), messaget::eom(), simple_insertiont::fenced_edges, forall_goto_program_instructions, forall_rw_set_r_entries, forall_rw_set_w_entries, code_function_callt::function(), goto_functions_templatet< bodyT >::function_map, symbol_exprt::get_identifier(), simple_insertiont::goto_functions, has_prefix(), irept::id(), id2string(), symbolt::is_shared(), namespacet::lookup(), simple_insertiont::message, simple_insertiont::ns, rw_set_baset::entryt::object, rw_set_baset::r_entries, rw_set_with_trackt::set_reads, rw_set_baset::entryt::symbol_expr, to_code_function_call(), to_symbol_expr(), symbolt::type, simple_insertiont::value_sets, visited_functions, rw_set_baset::w_entries, and messaget::warning().

Referenced by compute().

Member Data Documentation

◆ visited_functions

std::set<irep_idt> fence_all_shared_aegt::visited_functions
protected

Definition at line 147 of file fence_shared.cpp.

Referenced by fence_all_shared_aeg_explore().

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