CBMC
wmm Directory Reference
+ Directory dependency graph for wmm:

Files

file  abstract_event.cpp [code]
 abstract events
 
file  abstract_event.h [code]
 abstract events
 
file  cycle_collection.cpp [code]
 collection of cycles in graph of abstract events
 
file  data_dp.cpp [code]
 data dependencies
 
file  data_dp.h [code]
 data dependencies
 
file  event_graph.cpp [code]
 graph of abstract events
 
file  event_graph.h [code]
 graph of abstract events
 
file  fence.cpp [code]
 Fences for instrumentation.
 
file  fence.h [code]
 Fences for instrumentation.
 
file  goto2graph.cpp [code]
 Turns a goto-program into an abstract event graph.
 
file  goto2graph.h [code]
 Instrumenter.
 
file  instrumenter_pensieve.h [code]
 Instrumenter.
 
file  instrumenter_strategies.cpp [code]
 Strategies for picking the abstract events to instrument.
 
file  pair_collection.cpp [code]
 collection of pairs (for Pensieve's static delay-set analysis) in graph of abstract events
 
file  shared_buffers.cpp [code]
 
file  shared_buffers.h [code]
 
file  weak_memory.cpp [code]
 Weak Memory Instrumentation for Threaded Goto Programs.
 
file  weak_memory.h [code]
 Weak Memory Instrumentation for Threaded Goto Programs.
 
file  wmm.h [code]
 memory models