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
15
#include <
goto-programs/goto_model.h
>
16
17
bool
is_volatile
(
18
const
symbol_tablet
&,
19
const
typet
&);
20
21
void
nondet_volatile
(
goto_modelt
&);
22
23
#endif // CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H
typet
The type of an expression, extends irept.
Definition:
type.h:27
is_volatile
bool is_volatile(const symbol_tablet &, const typet &)
Definition:
nondet_volatile.cpp:19
goto_modelt
Definition:
goto_model.h:24
goto_model.h
Symbol Table + CFG.
symbol_tablet
The symbol table.
Definition:
symbol_table.h:19
nondet_volatile
void nondet_volatile(goto_modelt &)
Definition:
nondet_volatile.cpp:122
goto-instrument
nondet_volatile.h
Generated by
1.8.14