cprover
musketeer Directory Reference
Directory dependency graph for musketeer:

Files

file  cycles_visitor.cpp [code]
 cycles visitor for computing edges involved for fencing
 
file  cycles_visitor.h [code]
 cycles visitor for computing edges involved for fencing
 
file  fence_assert.cpp [code]
 ILP construction for cycles affecting user-assertions and resolution.
 
file  fence_assert.h [code]
 ILP construction for cycles affecting user-assertions and resolution.
 
file  fence_inserter.cpp [code]
 ILP construction for all cycles and resolution.
 
file  fence_inserter.h [code]
 ILP construction for all cycles and resolution.
 
file  fence_shared.cpp [code]
 
file  fence_shared.h [code]
 (naive) Fence insertion
 
file  fence_user_def.cpp [code]
 ILP construction for cycles affecting user-assertions and resolution.
 
file  fence_user_def.h [code]
 ILP construction for cycles containing user-placed fences and resolution.
 
file  fencer.cpp [code]
 Fence inference: Main.
 
file  fencer.h [code]
 Fence inference.
 
file  graph_visitor.cpp [code]
 graph visitor for computing edges involved for fencing
 
file  graph_visitor.h [code]
 graph visitor for computing edges involved for fencing
 
file  ilp.h [code]
 ILP structure.
 
file  infer_mode.h [code]
 
file  languages.cpp [code]
 Language Registration.
 
file  musketeer_main.cpp [code]
 Main Module.
 
file  musketeer_parse_options.cpp [code]
 Main Module.
 
file  musketeer_parse_options.h [code]
 Command Line Parsing.
 
file  pensieve.cpp [code]
 
file  pensieve.h [code]
 Fence insertion following criteria of Pensieve (PPoPP'05)
 
file  propagate_const_function_pointers.cpp [code]
 Constant Function Pointer Propagation.
 
file  propagate_const_function_pointers.h [code]
 Constant Function Pointer Propagation.
 
file  replace_async.h [code]
 
file  version.h [code]