CBMC
wmm.h File Reference
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Enumerations

enum  memory_modelt {
  Unknown =-1, TSO =0, PSO =1, RMO =2,
  Power =3
}
 
enum  instrumentation_strategyt {
  all =0, min_interference =1, read_first =2, write_first =3,
  my_events =4, one_event_per_cycle =5
}
 
enum  loop_strategyt { arrays_only =0, all_loops =1, no_loop =2 }
 

Detailed Description

memory models

Definition in file wmm.h.

Enumeration Type Documentation

◆ instrumentation_strategyt

Enumerator
all 
min_interference 
read_first 
write_first 
my_events 
one_event_per_cycle 

Definition at line 26 of file wmm.h.

◆ loop_strategyt

Enumerator
arrays_only 
all_loops 
no_loop 

Definition at line 36 of file wmm.h.

◆ memory_modelt

Enumerator
Unknown 
TSO 
PSO 
RMO 
Power 

Definition at line 17 of file wmm.h.