cprover
fence_volatilet Class Reference
Inheritance diagram for fence_volatilet:
[legend]
Collaboration diagram for fence_volatilet:
[legend]

Public Member Functions

 fence_volatilet (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 ()
 
bool is_volatile (const typet &src) const
 we can determine whether an access is volatile just by looking at the type of the variables involved in the expression. More...
 
- Protected Member Functions inherited from simple_insertiont
void print_to_file () const
 

Additional Inherited Members

- Protected Attributes inherited from simple_insertiont
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 165 of file fence_shared.cpp.

Constructor & Destructor Documentation

◆ fence_volatilet()

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

Definition at line 172 of file fence_shared.cpp.

Member Function Documentation

◆ compute()

◆ is_volatile()

bool fence_volatilet::is_volatile ( const typet src) const
protected

we can determine whether an access is volatile just by looking at the type of the variables involved in the expression.

We assume that the program is correctly typed (i.e., volatile-marked)

Definition at line 184 of file fence_shared.cpp.

References irept::get_bool(), typet::has_subtype(), typet::has_subtypes(), irept::id(), typet::subtype(), typet::subtypes(), simple_insertiont::symbol_table, symbol_tablet::symbols, and to_symbol_type().

Referenced by compute().


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