cprover
goto-instrument Directory Reference
Directory dependency graph for goto-instrument:

Directories

directory  accelerate
 
directory  wmm
 

Files

file  alignment_checks.cpp [code]
 Alignment Checks.
 
file  alignment_checks.h [code]
 Alignment Checks.
 
file  branch.cpp [code]
 Branch Instrumentation.
 
file  branch.h [code]
 Branch Instrumentation.
 
file  call_sequences.cpp [code]
 Printing function call sequences for Ofer.
 
file  call_sequences.h [code]
 Memory-mapped I/O Instrumentation for Goto Programs.
 
file  code_contracts.cpp [code]
 Verify and use annotated invariants and pre/post-conditions.
 
file  code_contracts.h [code]
 Verify and use annotated invariants and pre/post-conditions.
 
file  concurrency.cpp [code]
 Encoding for Threaded Goto Programs.
 
file  concurrency.h [code]
 Encoding for Threaded Goto Programs.
 
file  count_eloc.cpp [code]
 Count effective lines of code.
 
file  count_eloc.h [code]
 Count effective lines of code.
 
file  cover.cpp [code]
 Coverage Instrumentation.
 
file  cover.h [code]
 Coverage Instrumentation.
 
file  document_properties.cpp [code]
 Subgoal Documentation.
 
file  document_properties.h [code]
 Documentation of Properties.
 
file  dot.cpp [code]
 Dump Goto-Program as DOT Graph.
 
file  dot.h [code]
 Dump Goto-Program as DOT Graph.
 
file  dump_c.cpp [code]
 Dump Goto-Program as C/C++ Source.
 
file  dump_c.h [code]
 Dump C from Goto Program.
 
file  dump_c_class.h [code]
 Dump Goto-Program as C/C++ Source.
 
file  full_slicer.cpp [code]
 Slicing.
 
file  full_slicer.h [code]
 Slicing.
 
file  full_slicer_class.h [code]
 Goto Program Slicing.
 
file  function.cpp [code]
 Function Entering and Exiting.
 
file  function.h [code]
 Function Entering and Exiting.
 
file  function_modifies.cpp [code]
 Modifies.
 
file  function_modifies.h [code]
 Modifies.
 
file  goto_instrument_languages.cpp [code]
 Language Registration.
 
file  goto_instrument_main.cpp [code]
 Main Module.
 
file  goto_instrument_parse_options.cpp [code]
 Main Module.
 
file  goto_instrument_parse_options.h [code]
 Command Line Parsing.
 
file  goto_program2code.cpp [code]
 Dump Goto-Program as C/C++ Source.
 
file  goto_program2code.h [code]
 Dump Goto-Program as C/C++ Source.
 
file  havoc_loops.cpp [code]
 Havoc Loops.
 
file  havoc_loops.h [code]
 Havoc Loops.
 
file  horn_encoding.cpp [code]
 Horn-clause Encoding.
 
file  horn_encoding.h [code]
 Horn-clause Encoding.
 
file  interrupt.cpp [code]
 Interrupt Instrumentation.
 
file  interrupt.h [code]
 Interrupt Instrumentation for Goto Programs.
 
file  k_induction.cpp [code]
 k-induction
 
file  k_induction.h [code]
 k-induction
 
file  loop_utils.cpp [code]
 Helper functions for k-induction and loop invariants.
 
file  loop_utils.h [code]
 Helper functions for k-induction and loop invariants.
 
file  mmio.cpp [code]
 Memory-mapped I/O Instrumentation for Goto Programs.
 
file  mmio.h [code]
 Memory-mapped I/O Instrumentation for Goto Programs.
 
file  model_argc_argv.cpp [code]
 Initialize command line arguments.
 
file  model_argc_argv.h [code]
 Initialize command line arguments.
 
file  nondet_static.cpp [code]
 Nondeterministic initialization of certain global scope variables.
 
file  nondet_static.h [code]
 Nondeterministic initialization of certain global scope variables.
 
file  nondet_volatile.cpp [code]
 Volatile Variables.
 
file  nondet_volatile.h [code]
 Volatile Variables.
 
file  object_id.cpp [code]
 Object Identifiers.
 
file  object_id.h [code]
 Object Identifiers.
 
file  points_to.cpp [code]
 Field-sensitive, location-insensitive points-to analysis.
 
file  points_to.h [code]
 Field-sensitive, location-insensitive points-to analysis.
 
file  race_check.cpp [code]
 Race Detection for Threaded Goto Programs.
 
file  race_check.h [code]
 Race Detection for Threaded Goto Programs.
 
file  reachability_slicer.cpp [code]
 Slicer.
 
file  reachability_slicer.h [code]
 Slicing.
 
file  reachability_slicer_class.h [code]
 Goto Program Slicing.
 
file  remove_function.cpp [code]
 Remove function definition.
 
file  remove_function.h [code]
 Remove function definition.
 
file  rw_set.cpp [code]
 Race Detection for Threaded Goto Programs.
 
file  rw_set.h [code]
 Race Detection for Threaded Goto Programs.
 
file  show_locations.cpp [code]
 Show program locations.
 
file  show_locations.h [code]
 Show program locations.
 
file  skip_loops.cpp [code]
 Skip over selected loops by adding gotos.
 
file  skip_loops.h [code]
 Skip over selected loops by adding gotos.
 
file  stack_depth.cpp [code]
 Stack depth checks.
 
file  stack_depth.h [code]
 Stack depth checks.
 
file  thread_instrumentation.cpp [code]
 
file  thread_instrumentation.h [code]
 
file  undefined_functions.cpp [code]
 Handling of functions without body.
 
file  undefined_functions.h [code]
 Handling of functions without body.
 
file  uninitialized.cpp [code]
 Detection for Uninitialized Local Variables.
 
file  uninitialized.h [code]
 Detection for Uninitialized Local Variables.
 
file  unwind.cpp [code]
 Loop unwinding.
 
file  unwind.h [code]
 Loop unwinding.