cprover
|
Volatile Variables. More...
Go to the source code of this file.
Functions | |
bool | is_volatile (const symbol_tablet &symbol_table, const typet &src) |
void | nondet_volatile_rhs (const symbol_tablet &symbol_table, exprt &expr) |
void | nondet_volatile_lhs (const symbol_tablet &symbol_table, exprt &expr) |
void | nondet_volatile (symbol_tablet &symbol_table, goto_programt &goto_program) |
void | nondet_volatile (goto_modelt &goto_model) |
Volatile Variables.
Definition in file nondet_volatile.cpp.
bool is_volatile | ( | const symbol_tablet & | symbol_table, |
const typet & | src | ||
) |
Definition at line 19 of file nondet_volatile.cpp.
References irept::get_bool(), irept::id(), is_volatile(), symbol_table_baset::symbols, and to_symbol_type().
Referenced by is_volatile(), and nondet_volatile_rhs().
void nondet_volatile | ( | symbol_tablet & | symbol_table, |
goto_programt & | goto_program | ||
) |
Definition at line 80 of file nondet_volatile.cpp.
References code_function_callt::arguments(), goto_programt::instructiont::code, Forall_goto_program_instructions, goto_program, goto_programt::instructiont::guard, goto_programt::instructiont::is_assert(), goto_programt::instructiont::is_assign(), goto_programt::instructiont::is_assume(), goto_programt::instructiont::is_function_call(), goto_programt::instructiont::is_goto(), code_function_callt::lhs(), nondet_volatile_lhs(), nondet_volatile_rhs(), code_assignt::rhs(), to_code_assign(), and to_code_function_call().
Referenced by goto_instrument_parse_optionst::instrument_goto_program(), and nondet_volatile().
void nondet_volatile | ( | goto_modelt & | goto_model | ) |
Definition at line 122 of file nondet_volatile.cpp.
References Forall_goto_functions, goto_modelt::goto_functions, nondet_volatile(), goto_modelt::symbol_table, and goto_functionst::update().
void nondet_volatile_lhs | ( | const symbol_tablet & | symbol_table, |
exprt & | expr | ||
) |
Definition at line 57 of file nondet_volatile.cpp.
References irept::id(), nondet_volatile_rhs(), to_dereference_expr(), to_if_expr(), to_index_expr(), and to_member_expr().
Referenced by nondet_volatile().
void nondet_volatile_rhs | ( | const symbol_tablet & | symbol_table, |
exprt & | expr | ||
) |
Definition at line 37 of file nondet_volatile.cpp.
References Forall_operands, irept::id(), is_volatile(), irept::remove(), exprt::source_location(), irept::swap(), and exprt::type().
Referenced by nondet_volatile(), and nondet_volatile_lhs().