CBMC
|
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 |