cprover
|
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 | 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_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_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] |
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 | 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 | splice_call.cpp [code] |
Prepend a nullary call to another function. | |
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. | |