CBMC
goto-instrument Directory Reference
+ Directory dependency graph for goto-instrument:

Directories

directory  accelerate
 
directory  contracts
 
directory  wmm
 

Files

file  aggressive_slicer.cpp [code]
 Aggressive program slicer.
 
file  aggressive_slicer.h [code]
 Aggressive slicer Consider the control flow graph of the goto program and a criterion description of aggressive slicer here.
 
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  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  cover_basic_blocks.cpp [code]
 Basic blocks detection for Coverage Instrumentation.
 
file  cover_basic_blocks.h [code]
 Basic blocks detection for Coverage Instrumentation.
 
file  cover_filter.cpp [code]
 Filters for the Coverage Instrumentation.
 
file  cover_filter.h [code]
 Filters for the Coverage Instrumentation.
 
file  cover_instrument.h [code]
 Coverage Instrumentation.
 
file  cover_instrument_assume.cpp [code]
 Author: Diffblue Ltd.
 
file  cover_instrument_branch.cpp [code]
 Coverage Instrumentation for Branches.
 
file  cover_instrument_condition.cpp [code]
 Coverage Instrumentation for Conditions.
 
file  cover_instrument_decision.cpp [code]
 Coverage Instrumentation for Decisions.
 
file  cover_instrument_location.cpp [code]
 Coverage Instrumentation for Location, i.e.
 
file  cover_instrument_mcdc.cpp [code]
 Coverage Instrumentation for MC/DC.
 
file  cover_instrument_other.cpp [code]
 Further coverage instrumentations.
 
file  cover_util.cpp [code]
 Coverage Instrumentation Utilities.
 
file  cover_util.h [code]
 Coverage Instrumentation Utilities.
 
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_assigns.cpp [code]
 Compute objects assigned to in a function.
 
file  function_assigns.h [code]
 Compute objects assigned to in a function.
 
file  generate_function_bodies.cpp [code]
 
file  generate_function_bodies.h [code]
 
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  havoc_utils.cpp [code]
 Utilities for building havoc code for expressions.
 
file  havoc_utils.h [code]
 Utilities for building havoc code for expressions.
 
file  horn_encoding.cpp [code]
 Horn-clause Encoding.
 
file  horn_encoding.h [code]
 Horn-clause Encoding.
 
file  insert_final_assert_false.cpp [code]
 Insert final assert false into a function.
 
file  insert_final_assert_false.h [code]
 Insert final assert false into a function.
 
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]
 Nondeterministically initializes global scope variables, except for constants (such as string literals, final fields) and internal variables (such as CPROVER and symex variables, language specific internal variables).
 
file  nondet_static.h [code]
 Nondeterministically initializes global scope variables, except for constants (such as string literals, final fields) and internal variables (such as CPROVER and symex variables, language specific internal 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]
 Reachability Slicer Consider the control flow graph of the goto program and a criterion, and remove the parts of the graph from which the criterion is not reachable (and possibly, depending on the parameters, keep those that can be reached from the criterion).
 
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  replace_calls.cpp [code]
 Replace calls Replaces calls to given functions with calls to other given functions.
 
file  replace_calls.h [code]
 Replace calls to given functions with calls to other given functions.
 
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  source_lines.cpp [code]
 Set of source code lines contributing to a basic block.
 
file  source_lines.h [code]
 Set of source code lines contributing to a basic block.
 
file  splice_call.cpp [code]
 Prepend a nullary call to another function useful for context/ environment setting in arbitrary nodes.
 
file  splice_call.h [code]
 Harnessing for goto functions.
 
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.
 
file  unwindset.cpp [code]
 
file  unwindset.h [code]
 Loop unwinding.
 
file  value_set_fi_fp_removal.cpp [code]
 
file  value_set_fi_fp_removal.h [code]
 flow insensitive value set function pointer removal