cprover
nondet_volatile.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Volatile Variables
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H
13 #define CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H
14 
16 
17 bool is_volatile(
18  const symbol_tablet &symbol_table,
19  const typet &type);
20 
21 void nondet_volatile(
22  symbol_tablet &symbol_table,
23  goto_functionst &goto_functions);
24 
25 #endif // CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H
The type of an expression.
Definition: type.h:20
Goto Programs with Functions.
void nondet_volatile(symbol_tablet &symbol_table, goto_functionst &goto_functions)
The symbol table.
Definition: symbol_table.h:52
bool is_volatile(const symbol_tablet &symbol_table, const typet &type)