CBMC
Public Member Functions | Private Member Functions | Static Private Member Functions | Private Attributes | List of all members
nondet_volatilet Class Reference
+ Collaboration diagram for nondet_volatilet:

Public Member Functions

 nondet_volatilet (goto_modelt &goto_model, const optionst &options)
 
void operator() ()
 

Private Member Functions

void handle_volatile_expression (exprt &expr, const namespacet &ns, goto_programt &pre, goto_programt &post)
 
void nondet_volatile_rhs (const symbol_table_baset &symbol_table, exprt &expr, goto_programt &pre, goto_programt &post)
 
void nondet_volatile_lhs (const symbol_table_baset &symbol_table, exprt &expr, goto_programt &pre, goto_programt &post)
 
void nondet_volatile (symbol_table_baset &symbol_table, goto_programt &goto_program)
 
const symbolt & typecheck_variable (const irep_idt &id, const namespacet &ns)
 
void typecheck_model (const irep_idt &id, const symbolt &variable, const namespacet &ns)
 
void typecheck_options (const optionst &options)
 

Static Private Member Functions

static bool is_volatile (const namespacet &ns, const typet &src)
 

Private Attributes

goto_modelt & goto_model
 
bool all_nondet
 
std::set< irep_idt > nondet_variables
 
std::map< irep_idt, irep_idt > variable_models
 

Detailed Description

Definition at line 27 of file nondet_volatile.cpp.

Constructor & Destructor Documentation

◆ nondet_volatilet()

nondet_volatilet::nondet_volatilet ( goto_modelt &  goto_model,
const optionst &  options 
)
inline

Definition at line 30 of file nondet_volatile.cpp.

Member Function Documentation

◆ handle_volatile_expression()

void nondet_volatilet::handle_volatile_expression ( exprt &  expr,
const namespacet &  ns,
goto_programt &  pre,
goto_programt &  post 
)
private

Definition at line 108 of file nondet_volatile.cpp.

◆ is_volatile()

bool nondet_volatilet::is_volatile ( const namespacet &  ns,
const typet &  src 
)
staticprivate

Definition at line 93 of file nondet_volatile.cpp.

◆ nondet_volatile()

void nondet_volatilet::nondet_volatile ( symbol_table_baset &  symbol_table,
goto_programt &  goto_program 
)
private

Definition at line 215 of file nondet_volatile.cpp.

◆ nondet_volatile_lhs()

void nondet_volatilet::nondet_volatile_lhs ( const symbol_table_baset &  symbol_table,
exprt &  expr,
goto_programt &  pre,
goto_programt &  post 
)
private

Definition at line 186 of file nondet_volatile.cpp.

◆ nondet_volatile_rhs()

void nondet_volatilet::nondet_volatile_rhs ( const symbol_table_baset &  symbol_table,
exprt &  expr,
goto_programt &  pre,
goto_programt &  post 
)
private

Definition at line 165 of file nondet_volatile.cpp.

◆ operator()()

void nondet_volatilet::operator() ( void  )
inline

Definition at line 36 of file nondet_volatile.cpp.

◆ typecheck_model()

void nondet_volatilet::typecheck_model ( const irep_idt &  id,
const symbolt &  variable,
const namespacet &  ns 
)
private

Definition at line 299 of file nondet_volatile.cpp.

◆ typecheck_options()

void nondet_volatilet::typecheck_options ( const optionst &  options)
private

Definition at line 340 of file nondet_volatile.cpp.

◆ typecheck_variable()

const symbolt & nondet_volatilet::typecheck_variable ( const irep_idt &  id,
const namespacet &  ns 
)
private

Definition at line 272 of file nondet_volatile.cpp.

Member Data Documentation

◆ all_nondet

bool nondet_volatilet::all_nondet
private

Definition at line 88 of file nondet_volatile.cpp.

◆ goto_model

goto_modelt& nondet_volatilet::goto_model
private

Definition at line 85 of file nondet_volatile.cpp.

◆ nondet_variables

std::set<irep_idt> nondet_volatilet::nondet_variables
private

Definition at line 89 of file nondet_volatile.cpp.

◆ variable_models

std::map<irep_idt, irep_idt> nondet_volatilet::variable_models
private

Definition at line 90 of file nondet_volatile.cpp.

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