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