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 (symbol_tablet &symbol_table, goto_functionst &goto_functions) |
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_tablet::symbols, and to_symbol_type().
Referenced by fence_volatilet::compute(), is_volatile(), fence_volatilet::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(), Forall_goto_program_instructions, 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 | ( | symbol_tablet & | symbol_table, |
goto_functionst & | goto_functions | ||
) |
Definition at line 122 of file nondet_volatile.cpp.
References Forall_goto_functions, nondet_volatile(), and goto_functions_templatet< bodyT >::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(), irept::swap(), and exprt::type().
Referenced by nondet_volatile(), and nondet_volatile_lhs().