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
17
enum
memory_modelt
18
{
19
Unknown
=-1,
20
TSO
=0,
21
PSO
=1,
22
RMO
=2,
23
Power
=3
24
};
25
26
enum
instrumentation_strategyt
27
{
28
all
=0,
29
min_interference
=1,
30
read_first
=2,
31
write_first
=3,
32
my_events
=4,
33
one_event_per_cycle
=5
34
};
35
36
enum
loop_strategyt
37
{
38
arrays_only
=0,
39
all_loops
=1,
40
no_loop
=2
41
};
42
43
#endif // CPROVER_GOTO_INSTRUMENT_WMM_WMM_H
instrumentation_strategyt
instrumentation_strategyt
Definition:
wmm.h:26
Power
Definition:
wmm.h:23
all_loops
Definition:
wmm.h:39
write_first
Definition:
wmm.h:31
RMO
Definition:
wmm.h:22
read_first
Definition:
wmm.h:30
loop_strategyt
loop_strategyt
Definition:
wmm.h:36
min_interference
Definition:
wmm.h:29
memory_modelt
memory_modelt
Definition:
wmm.h:17
arrays_only
Definition:
wmm.h:38
PSO
Definition:
wmm.h:21
one_event_per_cycle
Definition:
wmm.h:33
my_events
Definition:
wmm.h:32
Unknown
Definition:
wmm.h:19
TSO
Definition:
wmm.h:20
no_loop
Definition:
wmm.h:40
all
Definition:
wmm.h:28
goto-instrument
wmm
wmm.h
Generated by
1.8.12