CBMC
wmm.h File Reference

memory models More...

+ 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.