cprover
wmm.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: memory models
4
5Author: Vincent Nimal
6
7Date: 2012
8
9\*******************************************************************/
10
13
14#ifndef CPROVER_GOTO_INSTRUMENT_WMM_WMM_H
15#define CPROVER_GOTO_INSTRUMENT_WMM_WMM_H
16
18{
20 TSO=0,
21 PSO=1,
22 RMO=2,
23 Power=3
24};
25
27{
28 all=0,
34};
35
37{
40 no_loop=2
41};
42
43#endif // CPROVER_GOTO_INSTRUMENT_WMM_WMM_H
memory_modelt
Definition: wmm.h:18
@ Unknown
Definition: wmm.h:19
@ TSO
Definition: wmm.h:20
@ RMO
Definition: wmm.h:22
@ PSO
Definition: wmm.h:21
@ Power
Definition: wmm.h:23
loop_strategyt
Definition: wmm.h:37
@ all_loops
Definition: wmm.h:39
@ arrays_only
Definition: wmm.h:38
@ no_loop
Definition: wmm.h:40
instrumentation_strategyt
Definition: wmm.h:27
@ my_events
Definition: wmm.h:32
@ one_event_per_cycle
Definition: wmm.h:33
@ min_interference
Definition: wmm.h:29
@ read_first
Definition: wmm.h:30
@ all
Definition: wmm.h:28
@ write_first
Definition: wmm.h:31