▶ analyses | |
ai.cpp | Abstract Interpretation |
ai.h | Abstract Interpretation |
call_graph.cpp | Function Call Graphs |
call_graph.h | Function Call Graphs |
call_graph_helpers.cpp | Function Call Graph Helpers |
call_graph_helpers.h | Function Call Graph Helpers |
cfg_dominators.h | Compute dominators for CFG of goto_function |
constant_propagator.cpp | Constant Propagation |
constant_propagator.h | Constant propagation |
custom_bitvector_analysis.cpp | Field-insensitive, location-sensitive bitvector analysis |
custom_bitvector_analysis.h | Field-insensitive, location-sensitive bitvector analysis |
dependence_graph.cpp | Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010 |
dependence_graph.h | Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010 |
dirty.cpp | Local variables whose address is taken |
dirty.h | Variables whose address is taken |
does_remove_const.cpp | Analyses |
does_remove_const.h | Analyses |
escape_analysis.cpp | Field-insensitive, location-sensitive escape analysis |
escape_analysis.h | Field-insensitive, location-sensitive, over-approximative escape analysis |
flow_insensitive_analysis.cpp | Flow Insensitive Static Analysis |
flow_insensitive_analysis.h | Flow Insensitive Static Analysis |
global_may_alias.cpp | Field-insensitive, location-sensitive global may alias analysis |
global_may_alias.h | Field-insensitive, location-sensitive, over-approximative escape analysis |
goto_check.cpp | GOTO Programs |
goto_check.h | Program Transformation |
goto_rw.cpp | |
goto_rw.h | |
interval_analysis.cpp | Interval Analysis |
interval_analysis.h | Interval Analysis |
interval_domain.cpp | Interval Domain |
interval_domain.h | Interval Domain |
interval_template.h | |
invariant_propagation.cpp | Invariant Propagation |
invariant_propagation.h | Invariant Propagation |
invariant_set.cpp | Invariant Set |
invariant_set.h | Value Set |
invariant_set_domain.cpp | Invariant Set Domain |
invariant_set_domain.h | Value Set |
is_threaded.cpp | Over-approximate Concurrency for Threaded Goto Programs |
is_threaded.h | Over-approximate Concurrency for Threaded Goto Programs |
local_bitvector_analysis.cpp | Field-insensitive, location-sensitive may-alias analysis |
local_bitvector_analysis.h | Field-insensitive, location-sensitive bitvector analysis |
local_cfg.cpp | CFG for One Function |
local_cfg.h | CFG for One Function |
local_may_alias.cpp | Field-insensitive, location-sensitive may-alias analysis |
local_may_alias.h | Field-insensitive, location-sensitive may-alias analysis |
locals.cpp | Local variables |
locals.h | Local variables whose address is taken |
natural_loops.cpp | Dominators |
natural_loops.h | Compute natural loops in a goto_function |
reaching_definitions.cpp | Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis, Litvak et al., FSE 2010) |
reaching_definitions.h | Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis, Litvak et al., FSE 2010) |
static_analysis.cpp | Value Set Propagation |
static_analysis.h | Static Analysis |
uncaught_exceptions_analysis.cpp | Over-approximating uncaught exceptions analysis |
uncaught_exceptions_analysis.h | Over-approximative uncaught exceptions analysis |
uninitialized_domain.cpp | Detection for Uninitialized Local Variables |
uninitialized_domain.h | Detection for Uninitialized Local Variables |
▶ ansi-c | |
▶ library | |
converter.cpp | |
cprover.h | |
jsa.h | Counterexample-Guided Inductive Synthesis |
▶ literals | |
convert_character_literal.cpp | C Language Conversion |
convert_character_literal.h | C++ Language Conversion |
convert_float_literal.cpp | C++ Language Conversion |
convert_float_literal.h | C Language Conversion |
convert_integer_literal.cpp | C++ Language Conversion |
convert_integer_literal.h | C++ Language Conversion |
convert_string_literal.cpp | C/C++ Language Conversion |
convert_string_literal.h | C/C++ Language Conversion |
parse_float.cpp | Conversion of Expressions |
parse_float.h | ANSI-C Conversion / Type Checking |
unescape_string.cpp | ANSI-C Language Conversion |
unescape_string.h | ANSI-C Language Conversion |
anonymous_member.cpp | ANSI-C Language Type Checking |
anonymous_member.h | C Language Type Checking |
ansi_c_convert_type.cpp | SpecC Language Conversion |
ansi_c_convert_type.h | ANSI-C Language Conversion |
ansi_c_declaration.cpp | ANSI-C Language Type Checking |
ansi_c_declaration.h | ANSI-CC Language Type Checking |
ansi_c_entry_point.cpp | |
ansi_c_entry_point.h | |
ansi_c_internal_additions.cpp | |
ansi_c_internal_additions.h | |
ansi_c_language.cpp | |
ansi_c_language.h | |
ansi_c_lex.yy.cpp | |
ansi_c_parse_tree.cpp | |
ansi_c_parse_tree.h | |
ansi_c_parser.cpp | |
ansi_c_parser.h | |
ansi_c_scope.cpp | |
ansi_c_scope.h | |
ansi_c_typecheck.cpp | ANSI-C Language Type Checking |
ansi_c_typecheck.h | ANSI-C Language Type Checking |
ansi_c_y.tab.cpp | |
ansi_c_y.tab.h | |
arm_builtin_headers.h | |
builtin_factory.cpp | |
builtin_factory.h | |
c_misc.cpp | ANSI-C Misc Utilities |
c_misc.h | ANSI-C Misc Utilities |
c_nondet_symbol_factory.cpp | C Nondet Symbol Factory |
c_nondet_symbol_factory.h | C Nondet Symbol Factory |
c_preprocess.cpp | |
c_preprocess.h | |
c_qualifiers.cpp | |
c_qualifiers.h | |
c_storage_spec.cpp | |
c_storage_spec.h | |
c_typecast.cpp | |
c_typecast.h | |
c_typecheck_argc_argv.cpp | ANSI-C Conversion / Type Checking |
c_typecheck_base.cpp | ANSI-C Conversion / Type Checking |
c_typecheck_base.h | ANSI-C Language Type Checking |
c_typecheck_code.cpp | C Language Type Checking |
c_typecheck_expr.cpp | ANSI-C Language Type Checking |
c_typecheck_initializer.cpp | ANSI-C Conversion / Type Checking |
c_typecheck_type.cpp | C++ Language Type Checking |
c_typecheck_typecast.cpp | |
clang_builtin_headers.h | |
cprover_builtin_headers.h | |
cprover_library.cpp | |
cprover_library.h | |
cw_builtin_headers.h | |
designator.cpp | ANSI-C Language Type Checking |
designator.h | ANSI-C Language Type Checking |
expr2c.cpp | |
expr2c.h | |
expr2c_class.h | |
file_converter.cpp | Convert file contents to C strings |
gcc_builtin_headers_alpha.h | |
gcc_builtin_headers_arm.h | |
gcc_builtin_headers_generic.h | |
gcc_builtin_headers_ia32-2.h | |
gcc_builtin_headers_ia32-3.h | |
gcc_builtin_headers_ia32-4.h | |
gcc_builtin_headers_ia32.h | |
gcc_builtin_headers_math.h | |
gcc_builtin_headers_mem_string.h | |
gcc_builtin_headers_mips.h | |
gcc_builtin_headers_omp.h | |
gcc_builtin_headers_power.h | |
gcc_builtin_headers_tm.h | |
gcc_builtin_headers_types.h | |
gcc_builtin_headers_ubsan.h | |
gcc_types.cpp | |
gcc_types.h | |
padding.cpp | C++ Language Type Checking |
padding.h | ANSI-C Language Type Checking |
preprocessor_line.cpp | ANSI-C Language Conversion |
preprocessor_line.h | ANSI-C Language Conversion |
type2name.cpp | Type Naming for C |
type2name.h | Type Naming for C |
windows_builtin_headers.h | |
▶ assembler | |
assembler_lex.yy.cpp | |
assembler_parser.cpp | |
assembler_parser.h | |
▶ big-int | |
allocainc.h | |
▶ cbmc | |
all_properties.cpp | Symbolic Execution of ANSI-C |
all_properties_class.h | Symbolic Execution of ANSI-C |
bmc.cpp | Symbolic Execution of ANSI-C |
bmc.h | Bounded Model Checking for ANSI-C + HDL |
bmc_cover.cpp | Test-Suite Generation with BMC |
bv_cbmc.cpp | |
bv_cbmc.h | |
cbmc_dimacs.cpp | Writing DIMACS Files |
cbmc_dimacs.h | Writing DIMACS Files |
cbmc_languages.cpp | Language Registration |
cbmc_main.cpp | CBMC Main Module |
cbmc_parse_options.cpp | CBMC Command Line Option Processing |
cbmc_parse_options.h | CBMC Command Line Option Processing |
cbmc_solvers.cpp | Solvers for VCs Generated by Symbolic Execution of ANSI-C |
cbmc_solvers.h | Bounded Model Checking for ANSI-C + HDL |
counterexample_beautification.cpp | Counterexample Beautification using Incremental SAT |
counterexample_beautification.h | Counterexample Beautification |
fault_localization.cpp | Fault Localization |
fault_localization.h | Fault Localization |
show_vcc.cpp | Symbolic Execution of ANSI-C |
symex_bmc.cpp | Bounded Model Checking for ANSI-C |
symex_bmc.h | Bounded Model Checking for ANSI-C |
symex_coverage.cpp | Record and print code coverage of symbolic execution |
symex_coverage.h | Record and print code coverage of symbolic execution |
xml_interface.cpp | XML Interface |
xml_interface.h | XML Interface |
▶ clobber | |
clobber_main.cpp | Symex Main Module |
clobber_parse_options.cpp | Symex Command Line Options Processing |
clobber_parse_options.h | Command Line Parsing |
▶ cpp | |
▶ library | |
cprover.h | |
cpp_constructor.cpp | C++ Language Type Checking |
cpp_convert_type.cpp | C++ Language Type Conversion |
cpp_convert_type.h | C++ Language Conversion |
cpp_declaration.cpp | C++ Language Type Checking |
cpp_declaration.h | C++ Language Type Checking |
cpp_declarator.cpp | C++ Language Type Checking |
cpp_declarator.h | C++ Language Type Checking |
cpp_declarator_converter.cpp | C++ Language Type Checking |
cpp_declarator_converter.h | C++ Language Type Checking |
cpp_destructor.cpp | C++ Language Type Checking |
cpp_enum_type.cpp | C++ Language Type Checking |
cpp_enum_type.h | C++ Language Type Checking |
cpp_exception_id.cpp | C++ Language Type Checking |
cpp_exception_id.h | C++ Language Type Checking |
cpp_id.cpp | C++ Language Type Checking |
cpp_id.h | C++ Language Type Checking |
cpp_instantiate_template.cpp | C++ Language Type Checking |
cpp_internal_additions.cpp | |
cpp_internal_additions.h | |
cpp_is_pod.cpp | C++ Language Type Checking |
cpp_item.h | C++ Language Type Checking |
cpp_language.cpp | C++ Language Module |
cpp_language.h | C++ Language Module |
cpp_linkage_spec.h | C++ Language Type Checking |
cpp_member_spec.h | |
cpp_name.cpp | C++ Language Type Checking |
cpp_name.h | |
cpp_namespace_spec.cpp | C++ Language Type Checking |
cpp_namespace_spec.h | C++ Language Type Checking |
cpp_parse_tree.cpp | C++ Parser |
cpp_parse_tree.h | C++ Parser |
cpp_parser.cpp | C++ Parser |
cpp_parser.h | C++ Parser |
cpp_scope.cpp | C++ Language Type Checking |
cpp_scope.h | C++ Language Type Checking |
cpp_scopes.cpp | C++ Language Type Checking |
cpp_scopes.h | C++ Language Type Checking |
cpp_static_assert.h | C++ Language Type Checking |
cpp_storage_spec.h | |
cpp_template_args.h | C++ Language Type Checking |
cpp_template_parameter.h | |
cpp_template_type.h | |
cpp_token.h | C++ Parser: Token |
cpp_token_buffer.cpp | C++ Parser: Token Buffer |
cpp_token_buffer.h | C++ Parser: Token Buffer |
cpp_type2name.cpp | C++ Language Module |
cpp_type2name.h | C++ Language Module |
cpp_typecast.h | |
cpp_typecheck.cpp | C++ Language Type Checking |
cpp_typecheck.h | C++ Language Type Checking |
cpp_typecheck_bases.cpp | C++ Language Type Checking |
cpp_typecheck_code.cpp | C++ Language Type Checking |
cpp_typecheck_compound_type.cpp | C++ Language Type Checking |
cpp_typecheck_constructor.cpp | C++ Language Type Checking |
cpp_typecheck_conversions.cpp | C++ Language Type Checking |
cpp_typecheck_declaration.cpp | C++ Language Type Checking |
cpp_typecheck_destructor.cpp | C++ Language Type Checking |
cpp_typecheck_enum_type.cpp | C++ Language Type Checking |
cpp_typecheck_expr.cpp | C++ Language Type Checking |
cpp_typecheck_fargs.cpp | C++ Language Type Checking |
cpp_typecheck_fargs.h | C++ Language Type Checking |
cpp_typecheck_function.cpp | C++ Language Type Checking |
cpp_typecheck_initializer.cpp | C++ Language Type Checking |
cpp_typecheck_linkage_spec.cpp | C++ Language Type Checking |
cpp_typecheck_method_bodies.cpp | C++ Language Type Checking |
cpp_typecheck_namespace.cpp | C++ Language Type Checking |
cpp_typecheck_resolve.cpp | C++ Language Type Checking |
cpp_typecheck_resolve.h | C++ Language Type Checking |
cpp_typecheck_static_assert.cpp | C++ Language Type Checking |
cpp_typecheck_template.cpp | C++ Language Type Checking |
cpp_typecheck_type.cpp | C++ Language Type Checking |
cpp_typecheck_using.cpp | C++ Language Type Checking |
cpp_typecheck_virtual_table.cpp | C++ Language Type Checking |
cpp_using.h | C++ Language Type Checking |
cpp_util.cpp | |
cpp_util.h | |
cprover_library.cpp | |
cprover_library.h | |
expr2cpp.cpp | |
expr2cpp.h | |
parse.cpp | C++ Language Parsing |
template_map.cpp | C++ Language Type Checking |
template_map.h | C++ Language Type Checking |
▶ doc | |
▶ assets | |
driver.h | |
kdev_t.h | |
modules.h | |
▶ goto-analyzer | |
goto_analyzer_main.cpp | Goto-Analyser Main Module |
goto_analyzer_parse_options.cpp | Goto-Analyser Command Line Option Processing |
goto_analyzer_parse_options.h | Goto-Analyser Command Line Option Processing |
static_show_domain.cpp | |
static_show_domain.h | |
static_simplifier.cpp | |
static_simplifier.h | |
static_verifier.cpp | |
static_verifier.h | |
taint_analysis.cpp | Taint Analysis |
taint_analysis.h | Taint Analysis |
taint_parser.cpp | Taint Parser |
taint_parser.h | Taint Parser |
unreachable_instructions.cpp | List all unreachable instructions |
unreachable_instructions.h | List all unreachable instructions |
▶ goto-cc | |
armcc_cmdline.cpp | A special command line object to mimic ARM's armcc |
armcc_cmdline.h | A special command line object to mimic ARM's armcc |
armcc_mode.cpp | Command line option container |
armcc_mode.h | Base class for command line interpretation for CL |
as86_cmdline.cpp | A special command line object for as86 (of Bruce's C Compiler) |
as86_cmdline.h | A special command line object for as86 (of Bruce's C Compiler) Author: Michael Tautschnig Date: July 2016 |
as_cmdline.cpp | A special command line object for GNU Assembler |
as_cmdline.h | A special command line object for GNU Assembler Author: Michael Tautschnig Date: July 2016 |
as_mode.cpp | Assembler Mode |
as_mode.h | Assembler Mode |
bcc_cmdline.cpp | A special command line object for Bruce's C Compiler |
bcc_cmdline.h | A special command line object for Bruce's C Compiler Author: Michael Tautschnig Date: July 2016 |
compile.cpp | Compile and link source and object files |
compile.h | Compile and link source and object files |
cw_mode.cpp | Command line option container |
cw_mode.h | Base class for command line interpretation |
gcc_cmdline.cpp | A special command line object for the gcc-like options |
gcc_cmdline.h | A special command line object for the gcc-like options |
gcc_mode.cpp | GCC Mode |
gcc_mode.h | Base class for command line interpretation |
gcc_version.cpp | |
gcc_version.h | |
goto_cc_cmdline.cpp | Command line interpretation for goto-cc |
goto_cc_cmdline.h | Command line interpretation for goto-cc |
goto_cc_languages.cpp | Language Registration |
goto_cc_main.cpp | GOTO-CC Main Module |
goto_cc_mode.cpp | Command line option container |
goto_cc_mode.h | Command line interpretation for goto-cc |
hybrid_binary.cpp | Create hybrid binary with goto-binary section |
hybrid_binary.h | Create hybrid binary with goto-binary section |
ld_cmdline.cpp | A special command line object for the ld-like options |
ld_cmdline.h | A special command line object for the ld-like options |
ld_mode.cpp | LD Mode |
ld_mode.h | Base class for command line interpretation |
linker_script_merge.cpp | |
linker_script_merge.h | Merge linker script-defined symbols into a goto-program |
ms_cl_cmdline.cpp | A special command line object for the CL options |
ms_cl_cmdline.h | A special command line object for the gcc-like options |
ms_cl_mode.cpp | Visual Studio CL Mode |
ms_cl_mode.h | Visual Studio CL Mode |
▶ goto-diff | |
change_impact.cpp | Data and control-dependencies of syntactic diff |
change_impact.h | Data and control-dependencies of syntactic diff |
goto_diff.h | GOTO-DIFF Base Class |
goto_diff_base.cpp | GOTO-DIFF Base Class |
goto_diff_languages.cpp | Language Registration |
goto_diff_languages.h | GOTO-DIFF Languages |
goto_diff_main.cpp | GOTO-DIFF Main Module |
goto_diff_parse_options.cpp | GOTO-DIFF Command Line Option Processing |
goto_diff_parse_options.h | GOTO-DIFF Command Line Option Processing |
syntactic_diff.cpp | Syntactic GOTO-DIFF |
syntactic_diff.h | Syntactic GOTO-DIFF |
unified_diff.cpp | Unified diff (using LCSS) of goto functions |
unified_diff.h | Unified diff (using LCSS) of goto functions |
▶ goto-instrument | |
▶ accelerate | |
accelerate.cpp | Loop Acceleration |
accelerate.h | Loop Acceleration |
acceleration_utils.cpp | Loop Acceleration |
acceleration_utils.h | Loop Acceleration |
accelerator.h | Loop Acceleration |
all_paths_enumerator.cpp | Loop Acceleration |
all_paths_enumerator.h | Loop Acceleration |
cone_of_influence.cpp | Loop Acceleration |
cone_of_influence.h | Loop Acceleration |
disjunctive_polynomial_acceleration.cpp | Loop Acceleration |
disjunctive_polynomial_acceleration.h | Loop Acceleration |
enumerating_loop_acceleration.cpp | Loop Acceleration |
enumerating_loop_acceleration.h | Loop Acceleration |
loop_acceleration.h | Loop Acceleration |
overflow_instrumenter.cpp | Loop Acceleration |
overflow_instrumenter.h | Loop Acceleration |
path.cpp | Loop Acceleration |
path.h | Loop Acceleration |
path_enumerator.h | Loop Acceleration |
polynomial.cpp | Loop Acceleration |
polynomial.h | Loop Acceleration |
polynomial_accelerator.cpp | Loop Acceleration |
polynomial_accelerator.h | Loop Acceleration |
sat_path_enumerator.cpp | Loop Acceleration |
sat_path_enumerator.h | Loop Acceleration |
scratch_program.cpp | Loop Acceleration |
scratch_program.h | Loop Acceleration |
subsumed.h | Loop Acceleration |
trace_automaton.cpp | Loop Acceleration |
trace_automaton.h | Loop Acceleration |
util.cpp | Loop Acceleration |
util.h | Loop Acceleration |
▶ wmm | |
abstract_event.cpp | Abstract events |
abstract_event.h | Abstract events |
cycle_collection.cpp | Collection of cycles in graph of abstract events |
data_dp.cpp | Data dependencies |
data_dp.h | Data dependencies |
event_graph.cpp | Graph of abstract events |
event_graph.h | Graph of abstract events |
fence.cpp | Fences for instrumentation |
fence.h | Fences for instrumentation |
goto2graph.cpp | Turns a goto-program into an abstract event graph |
goto2graph.h | Instrumenter |
instrumenter_pensieve.h | Instrumenter |
instrumenter_strategies.cpp | Strategies for picking the abstract events to instrument |
pair_collection.cpp | Collection of pairs (for Pensieve's static delay-set analysis) in graph of abstract events |
shared_buffers.cpp | |
shared_buffers.h | |
weak_memory.cpp | Weak Memory Instrumentation for Threaded Goto Programs |
weak_memory.h | Weak Memory Instrumentation for Threaded Goto Programs |
wmm.h | Memory models |
alignment_checks.cpp | Alignment Checks |
alignment_checks.h | Alignment Checks |
branch.cpp | Branch Instrumentation |
branch.h | Branch Instrumentation |
call_sequences.cpp | Printing function call sequences for Ofer |
call_sequences.h | Memory-mapped I/O Instrumentation for Goto Programs |
code_contracts.cpp | Verify and use annotated invariants and pre/post-conditions |
code_contracts.h | Verify and use annotated invariants and pre/post-conditions |
concurrency.cpp | Encoding for Threaded Goto Programs |
concurrency.h | Encoding for Threaded Goto Programs |
count_eloc.cpp | Count effective lines of code |
count_eloc.h | Count effective lines of code |
cover.cpp | Coverage Instrumentation |
cover.h | Coverage Instrumentation |
cover_basic_blocks.cpp | Basic blocks detection for Coverage Instrumentation |
cover_basic_blocks.h | Basic blocks detection for Coverage Instrumentation |
cover_filter.cpp | Filters for the Coverage Instrumentation |
cover_filter.h | Filters for the Coverage Instrumentation |
cover_instrument.h | Coverage Instrumentation |
cover_instrument_branch.cpp | Coverage Instrumentation for Branches |
cover_instrument_condition.cpp | Coverage Instrumentation for Conditions |
cover_instrument_decision.cpp | Coverage Instrumentation for Decisions |
cover_instrument_location.cpp | Coverage Instrumentation for Location, i.e |
cover_instrument_mcdc.cpp | Coverage Instrumentation for MC/DC |
cover_instrument_other.cpp | Further coverage instrumentations |
cover_util.cpp | Coverage Instrumentation Utilities |
cover_util.h | Coverage Instrumentation Utilities |
document_properties.cpp | Subgoal Documentation |
document_properties.h | Documentation of Properties |
dot.cpp | Dump Goto-Program as DOT Graph |
dot.h | Dump Goto-Program as DOT Graph |
dump_c.cpp | Dump Goto-Program as C/C++ Source |
dump_c.h | Dump C from Goto Program |
dump_c_class.h | Dump Goto-Program as C/C++ Source |
full_slicer.cpp | Slicing |
full_slicer.h | Slicing |
full_slicer_class.h | Goto Program Slicing |
function.cpp | Function Entering and Exiting |
function.h | Function Entering and Exiting |
function_modifies.cpp | Modifies |
function_modifies.h | Modifies |
goto_instrument_languages.cpp | Language Registration |
goto_instrument_main.cpp | Main Module |
goto_instrument_parse_options.cpp | Main Module |
goto_instrument_parse_options.h | Command Line Parsing |
goto_program2code.cpp | Dump Goto-Program as C/C++ Source |
goto_program2code.h | Dump Goto-Program as C/C++ Source |
havoc_loops.cpp | Havoc Loops |
havoc_loops.h | Havoc Loops |
horn_encoding.cpp | Horn-clause Encoding |
horn_encoding.h | Horn-clause Encoding |
interrupt.cpp | Interrupt Instrumentation |
interrupt.h | Interrupt Instrumentation for Goto Programs |
k_induction.cpp | K-induction |
k_induction.h | K-induction |
loop_utils.cpp | Helper functions for k-induction and loop invariants |
loop_utils.h | Helper functions for k-induction and loop invariants |
mmio.cpp | Memory-mapped I/O Instrumentation for Goto Programs |
mmio.h | Memory-mapped I/O Instrumentation for Goto Programs |
model_argc_argv.cpp | Initialize command line arguments |
model_argc_argv.h | Initialize command line arguments |
nondet_static.cpp | Nondeterministic initialization of certain global scope variables |
nondet_static.h | Nondeterministic initialization of certain global scope variables |
nondet_volatile.cpp | Volatile Variables |
nondet_volatile.h | Volatile Variables |
object_id.cpp | Object Identifiers |
object_id.h | Object Identifiers |
points_to.cpp | Field-sensitive, location-insensitive points-to analysis |
points_to.h | Field-sensitive, location-insensitive points-to analysis |
race_check.cpp | Race Detection for Threaded Goto Programs |
race_check.h | Race Detection for Threaded Goto Programs |
reachability_slicer.cpp | 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) |
reachability_slicer.h | Slicing |
reachability_slicer_class.h | Goto Program Slicing |
remove_function.cpp | Remove function definition |
remove_function.h | Remove function definition |
rw_set.cpp | Race Detection for Threaded Goto Programs |
rw_set.h | Race Detection for Threaded Goto Programs |
show_locations.cpp | Show program locations |
show_locations.h | Show program locations |
skip_loops.cpp | Skip over selected loops by adding gotos |
skip_loops.h | Skip over selected loops by adding gotos |
splice_call.cpp | Prepend a nullary call to another function |
splice_call.h | Harnessing for goto functions |
stack_depth.cpp | Stack depth checks |
stack_depth.h | Stack depth checks |
thread_instrumentation.cpp | |
thread_instrumentation.h | |
undefined_functions.cpp | Handling of functions without body |
undefined_functions.h | Handling of functions without body |
uninitialized.cpp | Detection for Uninitialized Local Variables |
uninitialized.h | Detection for Uninitialized Local Variables |
unwind.cpp | Loop unwinding |
unwind.h | Loop unwinding |
unwindset.cpp | |
unwindset.h | Loop unwinding |
▶ goto-programs | |
abstract_goto_model.h | Abstract interface to eager or lazy GOTO models |
adjust_float_expressions.cpp | Symbolic Execution |
adjust_float_expressions.h | Symbolic Execution |
builtin_functions.cpp | Program Transformation |
cfg.h | Control Flow Graph |
class_hierarchy.cpp | Class Hierarchy |
class_hierarchy.h | Class Hierarchy |
class_identifier.cpp | Extract class identifier |
class_identifier.h | Extract class identifier |
compute_called_functions.cpp | Query Called Functions |
compute_called_functions.h | Query Called Functions |
destructor.cpp | Destructor Calls |
destructor.h | Destructor Calls |
elf_reader.cpp | Read ELF |
elf_reader.h | Read ELF |
format_strings.cpp | Format String Parser |
format_strings.h | Format String Parser |
generate_function_bodies.cpp | |
generate_function_bodies.h | |
goto_asm.cpp | Assembler -> Goto |
goto_clean_expr.cpp | Program Transformation |
goto_convert.cpp | Program Transformation |
goto_convert.h | Program Transformation |
goto_convert_class.h | Program Transformation |
goto_convert_exceptions.cpp | Program Transformation |
goto_convert_function_call.cpp | Program Transformation |
goto_convert_functions.cpp | |
goto_convert_functions.h | Goto Programs with Functions |
goto_convert_side_effect.cpp | Program Transformation |
goto_function.cpp | |
goto_function.h | |
goto_functions.cpp | Goto Programs with Functions |
goto_functions.h | Goto Programs with Functions |
goto_inline.cpp | Function Inlining |
goto_inline.h | Function Inlining |
goto_inline_class.cpp | Function Inlining |
goto_inline_class.h | |
goto_model.h | Symbol Table + CFG |
goto_program.cpp | Program Transformation |
goto_program.h | Concrete Goto Program |
goto_program_template.cpp | Goto Program Template |
goto_trace.cpp | Traces of GOTO Programs |
goto_trace.h | Traces of GOTO Programs |
graphml_witness.cpp | Witnesses for Traces and Proofs |
graphml_witness.h | Witnesses for Traces and Proofs |
initialize_goto_model.cpp | Get a Goto Program |
initialize_goto_model.h | Initialize a Goto Program |
instrument_preconditions.cpp | |
instrument_preconditions.h | |
interpreter.cpp | Interpreter for GOTO Programs |
interpreter.h | Interpreter for GOTO Programs |
interpreter_class.h | Interpreter for GOTO Programs |
interpreter_evaluate.cpp | Interpreter for GOTO Programs |
json_goto_trace.cpp | Traces of GOTO Programs |
json_goto_trace.h | Traces of GOTO Programs |
lazy_goto_functions_map.h | Author: Diffblue Ltd |
lazy_goto_model.cpp | Author: Diffblue Ltd |
lazy_goto_model.h | Author: Diffblue Ltd |
link_goto_model.cpp | Link Goto Programs |
link_goto_model.h | Read Goto Programs |
link_to_library.cpp | Library Linking |
link_to_library.h | Library Linking |
loop_ids.cpp | Loop IDs |
loop_ids.h | Loop IDs |
mm_io.cpp | Perform Memory-mapped I/O instrumentation |
mm_io.h | Perform Memory-mapped I/O instrumentation |
osx_fat_reader.cpp | Read Mach-O |
osx_fat_reader.h | Read OS X Fat Binaries |
parameter_assignments.cpp | Add parameter assignments |
parameter_assignments.h | Add parameter assignments |
pointer_arithmetic.cpp | |
pointer_arithmetic.h | |
printf_formatter.cpp | Printf Formatting |
printf_formatter.h | Printf Formatting |
property_checker.cpp | Property Checker Interface |
property_checker.h | Property Checker Interface |
read_bin_goto_object.cpp | Read goto object files |
read_bin_goto_object.h | Read goto object files |
read_goto_binary.cpp | Read Goto Programs |
read_goto_binary.h | Read Goto Programs |
rebuild_goto_start_function.cpp | Goto Programs Author: Thomas Kiley, thoma.nosp@m.s@di.nosp@m.ffblu.nosp@m.e.co.nosp@m.m |
rebuild_goto_start_function.h | Goto Programs Author: Thomas Kiley, thoma.nosp@m.s@di.nosp@m.ffblu.nosp@m.e.co.nosp@m.m |
remove_asm.cpp | Remove 'asm' statements by compiling into suitable standard code |
remove_asm.h | Remove 'asm' statements by compiling into suitable standard code |
remove_calls_no_body.cpp | Remove calls to functions without a body |
remove_calls_no_body.h | Remove calls to functions without a body |
remove_complex.cpp | Remove 'complex' data type |
remove_complex.h | Remove the 'complex' data type by compilation into structs |
remove_const_function_pointers.cpp | Goto Programs |
remove_const_function_pointers.h | Goto Programs |
remove_function_pointers.cpp | Program Transformation |
remove_function_pointers.h | Remove Indirect Function Calls |
remove_returns.cpp | Remove function return values |
remove_returns.h | Remove function returns |
remove_skip.cpp | Program Transformation |
remove_skip.h | Program Transformation |
remove_unreachable.cpp | Program Transformation |
remove_unreachable.h | Program Transformation |
remove_unused_functions.cpp | Unused function removal |
remove_unused_functions.h | Unused function removal |
remove_vector.cpp | Remove 'vector' data type |
remove_vector.h | Remove the 'vector' data type by compilation into arrays |
remove_virtual_functions.cpp | Remove Virtual Function (Method) Calls |
remove_virtual_functions.h | Remove Virtual Function (Method) Calls |
resolve_inherited_component.cpp | |
resolve_inherited_component.h | Given a class and a component (either field or method), find the closest parent that defines that component |
safety_checker.cpp | Safety Checker Interface |
safety_checker.h | Safety Checker Interface |
set_properties.cpp | Set Properties |
set_properties.h | Set the properties to check |
show_goto_functions.cpp | Show goto functions |
show_goto_functions.h | Show the goto functions |
show_goto_functions_json.cpp | Goto Program |
show_goto_functions_json.h | Goto Program |
show_goto_functions_xml.cpp | Goto Program |
show_goto_functions_xml.h | Goto Program |
show_properties.cpp | Show Claims |
show_properties.h | Show the properties |
show_symbol_table.cpp | Show the symbol table |
show_symbol_table.h | Show the symbol table |
slice_global_inits.cpp | Remove initializations of unused global variables |
slice_global_inits.h | Remove initializations of unused global variables |
string_abstraction.cpp | String Abstraction |
string_abstraction.h | String Abstraction |
string_instrumentation.cpp | String Abstraction |
string_instrumentation.h | String Abstraction |
system_library_symbols.cpp | Goto Programs |
system_library_symbols.h | Goto Programs |
vcd_goto_trace.cpp | Traces of GOTO Programs in VCD (Value Change Dump) Format |
vcd_goto_trace.h | Traces of GOTO Programs in VCD (Value Change Dump) Format |
wp.cpp | Weakest Preconditions |
wp.h | Weakest Preconditions |
write_goto_binary.cpp | Write GOTO binaries |
write_goto_binary.h | Write GOTO binaries |
xml_goto_trace.cpp | Traces of GOTO Programs |
xml_goto_trace.h | Traces of GOTO Programs |
▶ goto-symex | |
auto_objects.cpp | Symbolic Execution of ANSI-C |
build_goto_trace.cpp | Traces of GOTO Programs |
build_goto_trace.h | Traces of GOTO Programs |
equation_conversion_exceptions.h | Exceptions that can be raised during the equation conversion phase |
goto_symex.cpp | Symbolic Execution |
goto_symex.h | Symbolic Execution |
goto_symex_state.cpp | Symbolic Execution |
goto_symex_state.h | Symbolic Execution |
memory_model.cpp | Memory model for partial order concurrency |
memory_model.h | Memory models for partial order concurrency |
memory_model_pso.cpp | Memory model for partial order concurrency |
memory_model_pso.h | Memory models for partial order concurrency |
memory_model_sc.cpp | Memory model for partial order concurrency |
memory_model_sc.h | Memory models for partial order concurrency |
memory_model_tso.cpp | Memory model for partial order concurrency |
memory_model_tso.h | Memory models for partial order concurrency |
partial_order_concurrency.cpp | Add constraints to equation encoding partial orders on events |
partial_order_concurrency.h | Add constraints to equation encoding partial orders on events |
path_storage.cpp | |
path_storage.h | Storage of symbolic execution paths to resume |
postcondition.cpp | Symbolic Execution |
postcondition.h | Generate Equation using Symbolic Execution |
precondition.cpp | Symbolic Execution |
precondition.h | Generate Equation using Symbolic Execution |
rewrite_union.cpp | Symbolic Execution of ANSI-C |
rewrite_union.h | Symbolic Execution |
slice.cpp | Slicer for symex traces |
slice.h | Slicer for symex traces |
slice_by_trace.cpp | Slicer for symex traces |
slice_by_trace.h | Slicer for matching with trace files |
symex_assign.cpp | Symbolic Execution |
symex_atomic_section.cpp | Symbolic Execution |
symex_builtin_functions.cpp | Symbolic Execution of ANSI-C |
symex_catch.cpp | Symbolic Execution |
symex_clean_expr.cpp | Symbolic Execution of ANSI-C |
symex_dead.cpp | Symbolic Execution |
symex_decl.cpp | Symbolic Execution |
symex_dereference.cpp | Symbolic Execution of ANSI-C |
symex_dereference_state.cpp | Symbolic Execution of ANSI-C |
symex_dereference_state.h | Symbolic Execution of ANSI-C |
symex_function_call.cpp | Symbolic Execution of ANSI-C |
symex_goto.cpp | Symbolic Execution |
symex_main.cpp | Symbolic Execution |
symex_other.cpp | Symbolic Execution |
symex_slice_class.h | Slicer for symex traces |
symex_start_thread.cpp | Symbolic Execution |
symex_target.cpp | Symbolic Execution |
symex_target.h | Generate Equation using Symbolic Execution |
symex_target_equation.cpp | Symbolic Execution |
symex_target_equation.h | Generate Equation using Symbolic Execution |
symex_throw.cpp | Symbolic Execution |
▶ jbmc | |
▶ src | |
▶ janalyzer | |
janalyzer_main.cpp | JANALYZER Main Module |
janalyzer_parse_options.cpp | JANALYZER Command Line Option Processing |
janalyzer_parse_options.h | JANALYZER Command Line Option Processing |
▶ java_bytecode | |
▶ library | |
converter.cpp | |
bytecode_info.cpp | |
bytecode_info.h | |
character_refine_preprocess.cpp | Preprocess a goto-programs so that calls to the java Character library are replaced by simple expressions |
character_refine_preprocess.h | Preprocess a goto-programs so that calls to the java Character library are replaced by simple expressions |
ci_lazy_methods.cpp | |
ci_lazy_methods.h | Collect methods needed to be loaded using the lazy method |
ci_lazy_methods_needed.cpp | Context-insensitive lazy methods container |
ci_lazy_methods_needed.h | Context-insensitive lazy methods container |
convert_java_nondet.cpp | Convert side_effect_expr_nondett expressions |
convert_java_nondet.h | Convert side_effect_expr_nondett expressions |
expr2java.cpp | |
expr2java.h | |
generic_parameter_specialization_map_keys.cpp | |
generic_parameter_specialization_map_keys.h | Author: Diffblue Ltd |
jar_file.cpp | |
jar_file.h | |
java_bytecode_convert_class.cpp | JAVA Bytecode Language Conversion |
java_bytecode_convert_class.h | JAVA Bytecode Language Conversion |
java_bytecode_convert_method.cpp | JAVA Bytecode Language Conversion |
java_bytecode_convert_method.h | JAVA Bytecode Language Conversion |
java_bytecode_convert_method_class.h | JAVA Bytecode Language Conversion |
java_bytecode_convert_threadblock.cpp | |
java_bytecode_convert_threadblock.h | |
java_bytecode_instrument.cpp | |
java_bytecode_instrument.h | |
java_bytecode_internal_additions.cpp | |
java_bytecode_internal_additions.h | |
java_bytecode_language.cpp | |
java_bytecode_language.h | |
java_bytecode_parse_tree.cpp | |
java_bytecode_parse_tree.h | |
java_bytecode_parser.cpp | |
java_bytecode_parser.h | |
java_bytecode_typecheck.cpp | JAVA Bytecode Conversion / Type Checking |
java_bytecode_typecheck.h | JAVA Bytecode Language Type Checking |
java_bytecode_typecheck_code.cpp | JAVA Bytecode Conversion / Type Checking |
java_bytecode_typecheck_expr.cpp | JAVA Bytecode Conversion / Type Checking |
java_bytecode_typecheck_type.cpp | JAVA Bytecode Conversion / Type Checking |
java_class_loader.cpp | |
java_class_loader.h | |
java_class_loader_limit.cpp | Limit class path loading |
java_class_loader_limit.h | Limit class path loading |
java_entry_point.cpp | |
java_entry_point.h | |
java_enum_static_init_unwind_handler.cpp | Unwind loops in static initializers |
java_enum_static_init_unwind_handler.h | Unwind loops in static initializers |
java_local_variable_table.cpp | Java local variable table processing |
java_object_factory.cpp | |
java_object_factory.h | This module is responsible for the synthesis of code (in the form of a sequence of codet statements) that can allocate and initialize non-deterministically both primitive Java types and objects |
java_pointer_casts.cpp | JAVA Pointer Casts |
java_pointer_casts.h | JAVA Pointer Casts |
java_qualifiers.cpp | Java-specific type qualifiers |
java_qualifiers.h | Java-specific type qualifiers |
java_root_class.cpp | |
java_root_class.h | |
java_static_initializers.cpp | |
java_static_initializers.h | |
java_string_library_preprocess.cpp | Java_string_libraries_preprocess, gives code for methods on strings of the java standard library |
java_string_library_preprocess.h | Produce code for simple implementation of String Java libraries |
java_string_literals.cpp | |
java_string_literals.h | |
java_types.cpp | |
java_types.h | |
java_utils.cpp | |
java_utils.h | |
mz_zip_archive.cpp | |
mz_zip_archive.h | |
object_factory_parameters.h | |
remove_exceptions.cpp | Remove exception handling |
remove_exceptions.h | Remove function exceptional returns |
remove_instanceof.cpp | Remove Instance-of Operators |
remove_instanceof.h | Remove Instance-of Operators |
remove_java_new.cpp | Remove Java New Operators |
remove_java_new.h | Remove Java New Operators |
replace_java_nondet.cpp | Replace Java Nondet expressions |
replace_java_nondet.h | Replace Java Nondet expressions |
select_pointer_type.cpp | Handle selection of correct pointer type (for example changing abstract classes to concrete versions) |
select_pointer_type.h | Handle selection of correct pointer type (for example changing abstract classes to concrete versions) |
simple_method_stubbing.cpp | Java simple opaque stub generation |
simple_method_stubbing.h | Java simple opaque stub generation |
synthetic_methods_map.h | Synthetic methods are particular methods internally generated by the Java frontend, including thunks to ensure static initializers are run once and initializers created for unknown / stub types |
▶ jbmc | |
jbmc_main.cpp | CBMC Main Module |
jbmc_parse_options.cpp | JBMC Command Line Option Processing |
jbmc_parse_options.h | JBMC Command Line Option Processing |
▶ jdiff | |
java_syntactic_diff.cpp | Syntactic GOTO-DIFF for Java |
java_syntactic_diff.h | Syntactic GOTO-DIFF for Java |
jdiff_languages.cpp | Language Registration |
jdiff_languages.h | JDIFF Languages |
jdiff_main.cpp | JDIFF Main Module |
jdiff_parse_options.cpp | JDIFF Command Line Option Processing |
jdiff_parse_options.h | JDIFF Command Line Option Processing |
▶ miniz | |
miniz.cpp | |
miniz.h | |
▶ unit | |
▶ java-testing-utils | |
load_java_class.cpp | |
load_java_class.h | Utility for loading and parsing a specified java class file, returning the symbol table generated by this |
require_goto_statements.cpp | |
require_goto_statements.h | Utilties for inspecting goto functions |
require_parse_tree.cpp | |
require_parse_tree.h | Utilties for inspecting java_parse_treet |
require_type.cpp | |
require_type.h | Helper functions for requiring specific types If the type is of the wrong type, throw a CATCH exception Also checks associated properties and returns a casted version of the expression |
▶ jsil | |
expr2jsil.cpp | Jsil Language |
expr2jsil.h | Jsil Language |
jsil_convert.cpp | Jsil Language Conversion |
jsil_convert.h | Jsil Language Conversion |
jsil_entry_point.cpp | Jsil Language |
jsil_entry_point.h | Jsil Language |
jsil_internal_additions.cpp | Jsil Language |
jsil_internal_additions.h | Jsil Language |
jsil_language.cpp | Jsil Language |
jsil_language.h | Jsil Language |
jsil_lex.yy.cpp | |
jsil_parse_tree.cpp | Jsil Language |
jsil_parse_tree.h | Jsil Language |
jsil_parser.cpp | Jsil Language |
jsil_parser.h | Jsil Language |
jsil_typecheck.cpp | Jsil Language |
jsil_typecheck.h | Jsil Language |
jsil_types.cpp | Jsil Language |
jsil_types.h | Jsil Language |
jsil_y.tab.cpp | |
jsil_y.tab.h | |
▶ json | |
json_lex.yy.cpp | |
json_parser.cpp | |
json_parser.h | |
json_y.tab.cpp | |
json_y.tab.h | |
▶ langapi | |
language.cpp | Abstract interface to support a programming language |
language.h | Abstract interface to support a programming language |
language_file.cpp | |
language_file.h | |
language_ui.cpp | |
language_ui.h | |
language_util.cpp | |
language_util.h | |
mode.cpp | |
mode.h | |
▶ linking | |
linking.cpp | ANSI-C Linking |
linking.h | ANSI-C Linking |
linking_class.h | ANSI-C Linking |
remove_internal_symbols.cpp | Remove symbols that are internal only |
remove_internal_symbols.h | Remove symbols that are internal only |
static_lifetime_init.cpp | |
static_lifetime_init.h | |
▶ memory-models | |
mm2cpp.cpp | |
mm2cpp.h | |
mm_parser.cpp | |
mm_parser.h | |
mmcc_main.cpp | Mmcc Main Module |
mmcc_parse_options.cpp | Mmcc Command Line Option Processing |
mmcc_parse_options.h | Mmcc Command Line Option Processing |
▶ pointer-analysis | |
add_failed_symbols.cpp | Pointer Dereferencing |
add_failed_symbols.h | Pointer Dereferencing |
dereference.cpp | Symbolic Execution of ANSI-C |
dereference.h | Pointer Dereferencing |
dereference_callback.cpp | Pointer Dereferencing |
dereference_callback.h | Pointer Dereferencing |
goto_program_dereference.cpp | Dereferencing Operations on GOTO Programs |
goto_program_dereference.h | Value Set |
object_numbering.h | Value Set |
pointer_offset_sum.cpp | Pointer Analysis |
pointer_offset_sum.h | Pointer Dereferencing |
rewrite_index.cpp | Pointer Dereferencing |
rewrite_index.h | Pointer Dereferencing |
show_value_sets.cpp | Show Value Sets |
show_value_sets.h | Show Value Sets |
value_set.cpp | Value Set |
value_set.h | Value Set |
value_set_analysis.cpp | Value Set Propagation |
value_set_analysis.h | Value Set Propagation |
value_set_analysis_fi.cpp | Value Set Propagation (Flow Insensitive) |
value_set_analysis_fi.h | Value Set Propagation (flow insensitive) |
value_set_analysis_fivr.cpp | Value Set Propagation (Flow Insensitive) |
value_set_analysis_fivr.h | Value Set Propagation |
value_set_analysis_fivrns.cpp | Value Set Propagation (Flow Insensitive, Validity Regions) |
value_set_analysis_fivrns.h | Value Set Analysis (Flow Insensitive, Validity Regions) |
value_set_dereference.cpp | Symbolic Execution of ANSI-C |
value_set_dereference.h | Pointer Dereferencing |
value_set_domain.h | Value Set |
value_set_domain_fi.cpp | Value Set Domain (Flow Insensitive) |
value_set_domain_fi.h | Value Set (Flow Insensitive) |
value_set_domain_fivr.cpp | Value Set Domain (Flow Insensitive, Sharing, Validity Regions) |
value_set_domain_fivr.h | Value Set (Flow Insensitive, Sharing, Validity Regions) |
value_set_domain_fivrns.cpp | Value Set Domain (Flow Insensitive, Validity Regions) |
value_set_domain_fivrns.h | Value Set Domain (Flow Insensitive, Validity Regions) |
value_set_fi.cpp | Value Set (Flow Insensitive, Sharing) |
value_set_fi.h | Value Set (Flow Insensitive, Sharing) |
value_set_fivr.cpp | Value Set (Flow Insensitive, Sharing, Validity Regions) |
value_set_fivr.h | Value Set (Flow Insensitive, Sharing, Validity Regions) |
value_set_fivrns.cpp | Value Set (Flow Insensitive, Validity Regions) |
value_set_fivrns.h | Value Set (Flow Insensitive, Validity Regions) |
value_sets.h | Value Set Propagation |
▶ solvers | |
▶ flattening | |
arrays.cpp | |
arrays.h | Theory of Arrays with Extensionality |
boolbv.cpp | |
boolbv.h | |
boolbv_abs.cpp | |
boolbv_add_sub.cpp | |
boolbv_array.cpp | |
boolbv_array_of.cpp | |
boolbv_bitwise.cpp | |
boolbv_bswap.cpp | |
boolbv_bv_rel.cpp | |
boolbv_byte_extract.cpp | |
boolbv_byte_update.cpp | |
boolbv_case.cpp | |
boolbv_complex.cpp | |
boolbv_concatenation.cpp | |
boolbv_cond.cpp | |
boolbv_constant.cpp | |
boolbv_constraint_select_one.cpp | |
boolbv_div.cpp | |
boolbv_equality.cpp | |
boolbv_extractbit.cpp | |
boolbv_extractbits.cpp | |
boolbv_floatbv_op.cpp | |
boolbv_get.cpp | |
boolbv_ieee_float_rel.cpp | |
boolbv_if.cpp | |
boolbv_index.cpp | |
boolbv_let.cpp | |
boolbv_map.cpp | |
boolbv_map.h | |
boolbv_member.cpp | |
boolbv_mod.cpp | |
boolbv_mult.cpp | |
boolbv_not.cpp | |
boolbv_onehot.cpp | |
boolbv_overflow.cpp | |
boolbv_power.cpp | |
boolbv_quantifier.cpp | |
boolbv_reduction.cpp | |
boolbv_replication.cpp | |
boolbv_shift.cpp | |
boolbv_struct.cpp | |
boolbv_type.cpp | |
boolbv_type.h | |
boolbv_typecast.cpp | |
boolbv_unary_minus.cpp | |
boolbv_union.cpp | |
boolbv_update.cpp | |
boolbv_vector.cpp | |
boolbv_width.cpp | |
boolbv_width.h | |
boolbv_with.cpp | |
bv_conversion_exceptions.h | Exceptions that can be raised in bv_conversion |
bv_endianness_map.cpp | |
bv_endianness_map.h | |
bv_minimize.cpp | |
bv_minimize.h | SAT-optimizer for minimizing expressions |
bv_pointers.cpp | |
bv_pointers.h | |
bv_utils.cpp | |
bv_utils.h | |
c_bit_field_replacement_type.cpp | |
c_bit_field_replacement_type.h | |
equality.cpp | |
equality.h | |
flatten_byte_extract_exceptions.h | |
flatten_byte_operators.cpp | |
flatten_byte_operators.h | |
functions.cpp | |
functions.h | Uninterpreted Functions |
pointer_logic.cpp | Pointer Logic |
pointer_logic.h | Pointer Logic |
▶ floatbv | |
float_approximation.cpp | |
float_approximation.h | Floating Point with under/over-approximation |
float_bv.cpp | |
float_bv.h | |
float_utils.cpp | |
float_utils.h | |
▶ lowering | |
expr_lowering.h | |
popcount.cpp | |
▶ miniBDD | |
example.cpp | A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes |
miniBDD.cpp | A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes |
miniBDD.h | A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes |
▶ prop | |
aig.cpp | |
aig.h | AND-Inverter Graph |
aig_prop.cpp | |
aig_prop.h | |
bdd_expr.cpp | Conversion between exprt and miniBDD |
bdd_expr.h | Conversion between exprt and miniBDD |
cover_goals.cpp | Cover a set of goals incrementally |
cover_goals.h | Cover a set of goals incrementally |
literal.cpp | Literals |
literal.h | |
literal_expr.h | |
minimize.cpp | Minimize some target function incrementally |
minimize.h | SAT Minimizer |
prop.cpp | |
prop.h | |
prop_conv.cpp | |
prop_conv.h | |
▶ qbf | |
qbf_bdd_core.cpp | |
qbf_bdd_core.h | |
qbf_core.h | |
qbf_quantor.cpp | |
qbf_quantor.h | |
qbf_qube.cpp | |
qbf_qube.h | |
qbf_qube_core.cpp | |
qbf_qube_core.h | |
qbf_skizzo.cpp | |
qbf_skizzo.h | |
qbf_skizzo_core.cpp | |
qbf_skizzo_core.h | |
qbf_squolem.cpp | Squolem Backend |
qbf_squolem.h | Squolem Backend |
qbf_squolem_core.cpp | Squolem Backend (with proofs) |
qbf_squolem_core.h | Squolem Backend (with Proofs) |
qdimacs_cnf.cpp | |
qdimacs_cnf.h | |
qdimacs_core.cpp | |
qdimacs_core.h | |
▶ refinement | |
bv_refinement.h | Abstraction Refinement Loop |
bv_refinement_loop.cpp | |
refine_arithmetic.cpp | |
refine_arrays.cpp | |
string_builtin_function.cpp | |
string_builtin_function.h | |
string_constraint.h | Defines string constraints |
string_constraint_generator.h | Generates string constraints to link results from string functions with their arguments |
string_constraint_generator_code_points.cpp | Generates string constraints for Java functions dealing with code points |
string_constraint_generator_comparison.cpp | Generates string constraints for function comparing strings, such as: equals, equalsIgnoreCase, compareTo, hashCode, intern |
string_constraint_generator_concat.cpp | Generates string constraints for functions adding content add the end of strings |
string_constraint_generator_constants.cpp | Generates string constraints for constant strings |
string_constraint_generator_float.cpp | Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool |
string_constraint_generator_format.cpp | Generates string constraints for the Java format function |
string_constraint_generator_indexof.cpp | Generates string constraints for the family of indexOf and lastIndexOf java functions |
string_constraint_generator_insert.cpp | Generates string constraints for the family of insert Java functions |
string_constraint_generator_main.cpp | Generates string constraints to link results from string functions with their arguments |
string_constraint_generator_testing.cpp | Generates string constraints for string functions that return Boolean values |
string_constraint_generator_transformation.cpp | Generates string constraints for string transformations, that is, functions taking one string and returning another |
string_constraint_generator_valueof.cpp | Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool |
string_constraint_instantiation.cpp | Defines related function for string constraints |
string_constraint_instantiation.h | Defines related function for string constraints |
string_refinement.cpp | String support via creating string constraints and progressively instantiating the universal constraints as needed |
string_refinement.h | String support via creating string constraints and progressively instantiating the universal constraints as needed |
string_refinement_invariant.h | |
string_refinement_util.cpp | |
string_refinement_util.h | |
▶ sat | |
cnf.cpp | CNF Generation, via Tseitin |
cnf.h | CNF Generation, via Tseitin |
cnf_clause_list.cpp | CNF Generation |
cnf_clause_list.h | CNF Generation |
dimacs_cnf.cpp | |
dimacs_cnf.h | |
pbs_dimacs_cnf.cpp | |
pbs_dimacs_cnf.h | |
resolution_proof.cpp | |
resolution_proof.h | |
satcheck.h | |
satcheck_booleforce.cpp | |
satcheck_booleforce.h | |
satcheck_cadical.cpp | |
satcheck_cadical.h | |
satcheck_core.h | |
satcheck_glucose.cpp | |
satcheck_glucose.h | |
satcheck_ipasir.cpp | |
satcheck_ipasir.h | |
satcheck_lingeling.cpp | |
satcheck_lingeling.h | |
satcheck_minisat.cpp | |
satcheck_minisat.h | |
satcheck_minisat2.cpp | |
satcheck_minisat2.h | |
satcheck_picosat.cpp | |
satcheck_picosat.h | |
satcheck_zchaff.cpp | |
satcheck_zchaff.h | |
satcheck_zcore.cpp | |
satcheck_zcore.h | |
▶ smt2 | |
smt2_conv.cpp | SMT Backend |
smt2_conv.h | |
smt2_dec.cpp | |
smt2_dec.h | |
smt2_parser.cpp | |
smt2_parser.h | |
smt2_solver.cpp | |
smt2_tokenizer.cpp | |
smt2_tokenizer.h | |
smt2irep.cpp | |
smt2irep.h | |
▶ unit | |
▶ testing-utils | |
free_form_cmdline.cpp | |
free_form_cmdline.h | |
message.cpp | Global instance of null_message_handlert |
message.h | |
require_expr.cpp | Helper functions for requiring specific expressions If the expression is of the wrong type, throw a CATCH exception Also checks associated properties and returns a casted version of the expression |
require_expr.h | Helper functions for requiring specific expressions If the expression is of the wrong type, throw a CATCH exception Also checks associated properties and returns a casted version of the expression |
require_symbol.cpp | |
require_symbol.h | Helper functions for getting symbols from the symbol table during unit tests |
run_test_with_compilers.cpp | |
run_test_with_compilers.h | Utility for running a test with different compilers |
▶ util | |
arith_tools.cpp | |
arith_tools.h | |
array_name.cpp | Misc Utilities |
array_name.h | Misc Utilities |
base_exceptions.h | Generic exception types primarily designed for use with invariants |
base_type.cpp | Base Type Computation |
base_type.h | Base Type Computation |
bv_arithmetic.cpp | |
bv_arithmetic.h | |
byte_operators.cpp | |
byte_operators.h | Expression classes for byte-level operators |
c_types.cpp | |
c_types.h | |
cmdline.cpp | |
cmdline.h | |
config.cpp | |
config.h | |
container_utils.h | |
cout_message.cpp | |
cout_message.h | |
cow.h | |
cprover_prefix.h | |
decision_procedure.cpp | Decision Procedure Interface |
decision_procedure.h | Decision Procedure Interface |
deprecate.h | |
dstring.cpp | Container for C-Strings |
dstring.h | Container for C-Strings |
endianness_map.cpp | |
endianness_map.h | |
exit_codes.h | Document and give macros for the exit codes of CPROVER binaries |
expanding_vector.h | |
expr.cpp | Expression Representation |
expr.h | |
expr_cast.h | Templated functions to cast to specific exprt-derived classes |
expr_initializer.cpp | Expression Initialization |
expr_initializer.h | Expression Initialization |
expr_iterator.h | |
expr_util.cpp | |
expr_util.h | Deprecated expression utility functions |
file_util.cpp | File Utilities |
file_util.h | |
find_macros.cpp | |
find_macros.h | |
find_symbols.cpp | |
find_symbols.h | |
fixed_keys_map_wrapper.h | A wrapper for maps that gives read-write access to elements but without allowing addition or removal of elements |
fixedbv.cpp | |
fixedbv.h | |
format.h | |
format_constant.cpp | |
format_constant.h | |
format_expr.cpp | Expression Pretty Printing |
format_expr.h | |
format_number_range.cpp | Format vector of numbers into a compressed range |
format_number_range.h | Format vector of numbers into a compressed range |
format_spec.h | |
format_type.cpp | |
format_type.h | |
freer.h | |
fresh_symbol.cpp | Fresh auxiliary symbol creation |
fresh_symbol.h | Fresh auxiliary symbol creation |
get_base_name.cpp | |
get_base_name.h | |
get_module.cpp | Find module symbol using name |
get_module.h | Find module symbol using name |
graph.h | A Template Class for Graphs |
guard.cpp | Symbolic Execution |
guard.h | Guard Data Structure |
identifier.cpp | |
identifier.h | |
ieee_float.cpp | |
ieee_float.h | |
infix.h | String infix shorthand |
invariant.cpp | |
invariant.h | |
invariant_utils.cpp | Invariant helper utilities |
invariant_utils.h | |
irep.cpp | Internal Representation |
irep.h | |
irep_hash.cpp | Irep hash functions |
irep_hash.h | Irep hash functions |
irep_hash_container.cpp | Hashing IREPs |
irep_hash_container.h | IREP Hash Container |
irep_ids.cpp | Internal Representation |
irep_ids.h | Util |
irep_serialization.cpp | Binary irep conversions with hashing |
irep_serialization.h | Binary irep conversions with hashing |
journalling_symbol_table.h | Author: Diffblue Ltd |
json.cpp | |
json.h | |
json_expr.cpp | Expressions in JSON |
json_expr.h | Expressions in JSON |
json_irep.cpp | Util |
json_irep.h | Util |
json_stream.cpp | |
json_stream.h | |
lispexpr.cpp | |
lispexpr.h | |
lispirep.cpp | |
lispirep.h | |
magic.h | Magic numbers used throughout the codebase |
make_unique.h | |
memory_info.cpp | |
memory_info.h | |
merge_irep.cpp | |
merge_irep.h | |
message.cpp | |
message.h | |
mp_arith.cpp | |
mp_arith.h | |
namespace.cpp | Namespace |
namespace.h | |
nondet_bool.h | Nondeterministic boolean helper |
numbering.h | |
optional.h | |
options.cpp | Options |
options.h | Options |
parse_options.cpp | |
parse_options.h | |
parser.cpp | |
parser.h | Parser utilities |
pointer_offset_size.cpp | Pointer Logic |
pointer_offset_size.h | Pointer Logic |
pointer_predicates.cpp | Various predicates over pointers in programs |
pointer_predicates.h | Various predicates over pointers in programs |
prefix.h | |
preprocessor.h | Preprocessing Base Class |
rational.cpp | Rational Numbers |
rational.h | |
rational_tools.cpp | Rational Numbers |
rational_tools.h | |
ref_expr_set.cpp | Value Set |
ref_expr_set.h | Value Set |
reference_counting.h | Reference Counting |
refined_string_type.cpp | Type for string expressions used by the string solver |
refined_string_type.h | Type for string expressions used by the string solver |
rename.cpp | |
rename.h | |
rename_symbol.cpp | |
rename_symbol.h | |
replace_expr.cpp | |
replace_expr.h | |
replace_symbol.cpp | |
replace_symbol.h | |
run.cpp | |
run.h | |
sharing_map.h | Sharing map |
sharing_node.h | Sharing node |
signal_catcher.cpp | |
signal_catcher.h | |
simplify_expr.cpp | |
simplify_expr.h | |
simplify_expr_array.cpp | |
simplify_expr_boolean.cpp | |
simplify_expr_class.h | |
simplify_expr_floatbv.cpp | |
simplify_expr_int.cpp | |
simplify_expr_pointer.cpp | |
simplify_expr_struct.cpp | |
simplify_utils.cpp | |
simplify_utils.h | |
small_map.h | Small map |
small_shared_ptr.h | |
small_shared_two_way_ptr.h | |
source_location.cpp | |
source_location.h | |
sparse_vector.h | Sparse Vectors |
ssa_expr.cpp | |
ssa_expr.h | |
std_code.cpp | |
std_code.h | |
std_expr.cpp | |
std_expr.h | API to expression classes |
std_types.cpp | |
std_types.h | API to type classes |
string2int.cpp | |
string2int.h | |
string_constant.cpp | |
string_constant.h | |
string_container.cpp | Container for C-Strings |
string_container.h | Container for C-Strings |
string_expr.h | String expressions for the string solver |
string_hash.cpp | String hashing |
string_hash.h | String hashing |
string_utils.cpp | |
string_utils.h | |
suffix.h | |
symbol.cpp | |
symbol.h | Symbol table entry |
symbol_table.cpp | |
symbol_table.h | Author: Diffblue Ltd |
symbol_table_base.cpp | |
symbol_table_base.h | Author: Diffblue Ltd |
tempdir.cpp | |
tempdir.h | |
tempfile.cpp | |
tempfile.h | |
threeval.cpp | |
threeval.h | |
throw_with_nested.h | |
timestamper.cpp | |
timestamper.h | Emit timestamps |
type.cpp | |
type.h | |
type_eq.cpp | Type Checking |
type_eq.h | |
typecheck.cpp | |
typecheck.h | |
ui_message.cpp | |
ui_message.h | |
unicode.cpp | |
unicode.h | |
union_find.cpp | |
union_find.h | |
union_find_replace.cpp | |
union_find_replace.h | |
unwrap_nested_exception.cpp | |
unwrap_nested_exception.h | |
xml.cpp | |
xml.h | |
xml_expr.cpp | Expressions in XML |
xml_expr.h | |
xml_irep.cpp | |
xml_irep.h | |
▶ xmllang | |
graphml.cpp | Read/write graphs as GraphML |
graphml.h | Read/write graphs as GraphML |
xml_lex.yy.cpp | |
xml_parse_tree.cpp | |
xml_parse_tree.h | |
xml_parser.cpp | |
xml_parser.h | |
xml_y.tab.cpp | |
xml_y.tab.h | |