cprover
Loading...
Searching...
No Matches
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() ( )
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: