CBMC
|
memory models More...
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 } |
memory models
Definition in file wmm.h.
enum loop_strategyt |
enum memory_modelt |