|
| 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
|
| |
Directory dependency graph for goto-instrument: