► analyses | |
ai.cpp | Abstract Interpretation |
ai.h | Abstract Interpretation |
ai_domain.cpp | Abstract Interpretation Domain |
ai_domain.h | Abstract Interpretation Domain |
ai_history.cpp | Abstract Interpretation history |
ai_history.h | Abstract Interpretation history |
ai_storage.h | Abstract Interpretation Storage |
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 |
call_stack_history.cpp | History for tracking the call stack and performing interprocedural analysis |
call_stack_history.h | History for tracking the call stack and performing interprocedural analysis |
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 | |
guard.h | Guard Data Structure |
guard_bdd.cpp | Implementation of guards using BDDs |
guard_bdd.h | Guard Data Structure Implementation using BDDs |
guard_expr.cpp | Symbolic Execution |
guard_expr.h | Guard Data Structure |
interval_analysis.cpp | Interval Analysis – implements the functionality necessary for performing abstract interpretation over interval domain for goto programs |
interval_analysis.h | Interval Analysis |
interval_domain.cpp | Interval Domain |
interval_domain.h | Interval Domain |
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 |
lexical_loops.h | Compute lexical loops in a goto_function |
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_control_flow_history.cpp | Track function-local control flow for loop unwinding and path senstivity |
local_control_flow_history.h | Track function-local control flow for loop unwinding and path senstivity |
local_may_alias.cpp | Field-insensitive, location-sensitive may-alias analysis |
local_may_alias.h | Field-insensitive, location-sensitive may-alias analysis |
local_safe_pointers.cpp | Local safe pointer analysis |
local_safe_pointers.h | Local safe pointer analysis |
locals.cpp | Local variables |
locals.h | Local variables whose address is taken |
loop_analysis.h | Data structure representing a loop in a GOTO program and an interface shared by all analyses that find program loops |
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) |
sese_regions.cpp | Single-entry, single-exit region analysis |
sese_regions.h | Single-entry, single-exit region analysis |
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_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 |
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_object_factory_parameters.cpp | |
c_object_factory_parameters.h | |
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_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_gcc_polymorphic_builtins.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 | |
gcc_version.cpp | |
gcc_version.h | |
merged_type.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 |
typedef_type.h | |
windows_builtin_headers.h | |
► assembler | |
assembler_parser.cpp | |
assembler_parser.h | |
remove_asm.cpp | Remove 'asm' statements by compiling them into suitable standard goto program instructions |
remove_asm.h | Remove 'asm' statements by compiling them into suitable standard goto program instructions |
► big-int | |
allocainc.h | |
► cbmc | |
c_test_input_generator.cpp | Test Input Generator for C |
c_test_input_generator.h | Test Input Generator for C |
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 |
► 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.cpp | |
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 | |
ADR | |
architectural | |
► 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 |
show_on_source.cpp | |
show_on_source.h | |
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 |
cl_message_handler.cpp | |
cl_message_handler.h | |
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_message_handler.cpp | |
gcc_message_handler.h | |
gcc_mode.cpp | GCC Mode |
gcc_mode.h | Base class for command line interpretation |
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 |
ms_cl_version.cpp | |
ms_cl_version.h | |
ms_link_cmdline.cpp | A special command line object for LINK options |
ms_link_cmdline.h | A special command line object for LINK options |
ms_link_mode.cpp | Visual Studio Link Mode |
ms_link_mode.h | Visual Studio Link Mode |
► goto-checker | |
all_properties_verifier.h | Goto Verifier for Verifying all Properties |
all_properties_verifier_with_fault_localization.h | Goto verifier for verifying all properties that stores traces and localizes faults |
all_properties_verifier_with_trace_storage.h | Goto verifier for verifying all properties that stores traces |
bmc_util.cpp | Bounded Model Checking Utilities |
bmc_util.h | Bounded Model Checking Utilities |
counterexample_beautification.cpp | Counterexample Beautification using Incremental SAT |
counterexample_beautification.h | Counterexample Beautification |
cover_goals_report_util.cpp | Cover Goals Reporting Utilities |
cover_goals_report_util.h | Cover Goals Reporting Utilities |
cover_goals_verifier_with_trace_storage.h | Goto verifier for covering goals that stores traces |
fault_localization_provider.h | Interface for Goto Checkers to provide Fault Localization |
goto_symex_fault_localizer.cpp | Fault Localization for Goto Symex |
goto_symex_fault_localizer.h | Fault Localization for Goto Symex |
goto_symex_property_decider.cpp | Property Decider for Goto-Symex |
goto_symex_property_decider.h | Property Decider for Goto-Symex |
goto_trace_provider.h | Interface for returning Goto Traces from Goto Checkers |
goto_trace_storage.cpp | Goto Trace Storage |
goto_trace_storage.h | Goto Trace Storage |
goto_verifier.cpp | Goto Verifier Interface |
goto_verifier.h | Goto Verifier Interface |
incremental_goto_checker.cpp | Incremental Goto Checker Interface |
incremental_goto_checker.h | Incremental Goto Checker Interface |
multi_path_symex_checker.cpp | Goto Checker using Bounded Model Checking |
multi_path_symex_checker.h | Goto Checker using Multi-Path Symbolic Execution |
multi_path_symex_only_checker.cpp | Goto Checker using Multi-Path Symbolic Execution only (no SAT solving) |
multi_path_symex_only_checker.h | Goto Checker using Multi-Path Symbolic Execution only (no SAT solving) |
properties.cpp | Properties |
properties.h | Properties |
report_util.cpp | Bounded Model Checking Utilities |
report_util.h | Bounded Model Checking Utilities |
single_loop_incremental_symex_checker.cpp | Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop |
single_loop_incremental_symex_checker.h | Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop |
single_path_symex_checker.cpp | Goto Checker using Single Path Symbolic Execution |
single_path_symex_checker.h | Goto Checker using Single Path Symbolic Execution |
single_path_symex_only_checker.cpp | Goto Checker using Single Path Symbolic Execution only |
single_path_symex_only_checker.h | Goto Checker using Single Path Symbolic Execution only |
solver_factory.cpp | Solver Factory |
solver_factory.h | Solver Factory |
stop_on_fail_verifier.h | Goto Verifier for stopping at the first failing property |
stop_on_fail_verifier_with_fault_localization.h | Goto Verifier for stopping at the first failing property and localizing the fault |
symex_bmc.cpp | Bounded Model Checking for ANSI-C |
symex_bmc.h | Bounded Model Checking for ANSI-C |
symex_bmc_incremental_one_loop.cpp | |
symex_bmc_incremental_one_loop.h | |
symex_coverage.cpp | Record and print code coverage of symbolic execution |
symex_coverage.h | Record and print code coverage of symbolic execution |
witness_provider.h | Interface for outputting GraphML Witnesses for Goto Checkers |
► 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_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-harness | |
common_harness_generator_options.h | |
function_call_harness_generator.cpp | |
function_call_harness_generator.h | |
function_harness_generator_options.h | |
goto_harness_generator.cpp | |
goto_harness_generator.h | |
goto_harness_generator_factory.cpp | |
goto_harness_generator_factory.h | |
goto_harness_main.cpp | |
goto_harness_parse_options.cpp | |
goto_harness_parse_options.h | |
memory_snapshot_harness_generator.cpp | |
memory_snapshot_harness_generator.h | |
memory_snapshot_harness_generator_options.h | |
recursive_initialization.cpp | |
recursive_initialization.h | |
► 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 |
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 |
aggressive_slicer.cpp | Aggressive program slicer |
aggressive_slicer.h | Aggressive slicer Consider the control flow graph of the goto program and a criterion description of aggressive slicer here |
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 |
generate_function_bodies.cpp | |
generate_function_bodies.h | |
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 |
insert_final_assert_false.cpp | Insert final assert false into a function |
insert_final_assert_false.h | Insert final assert false into a function |
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 | 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) |
nondet_static.h | 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) |
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 |
replace_calls.cpp | Replace calls Replaces calls to given functions with calls to other given functions |
replace_calls.h | Replace calls to given functions with calls to other given functions |
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 |
source_lines.cpp | Set of source code lines contributing to a basic block |
source_lines.h | Set of source code lines contributing to a basic block |
splice_call.cpp | Prepend a nullary call to another function useful for context/ environment setting in arbitrary nodes |
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 |
value_set_fi_fp_removal.cpp | |
value_set_fi_fp_removal.h | Flow insensitive value set function pointer removal |
► goto-programs | |
abstract_goto_model.h | Abstract interface to eager or lazy GOTO models |
add_malloc_may_fail_variable_initializations.cpp | |
add_malloc_may_fail_variable_initializations.h | |
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 |
destructor_tree.cpp | |
destructor_tree.h | |
elf_reader.cpp | Read ELF |
elf_reader.h | Read ELF |
ensure_one_backedge_per_target.cpp | Ensure one backedge per target |
ensure_one_backedge_per_target.h | Ensure one backedge per target |
format_strings.cpp | Format String Parser |
format_strings.h | Format String Parser |
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 |
goto_function.h | Goto Function |
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_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_expr.cpp | Expressions in JSON |
json_expr.h | Expressions in JSON |
json_goto_trace.cpp | Traces of GOTO Programs |
json_goto_trace.h | Traces of GOTO Programs |
label_function_pointer_call_sites.cpp | Label function pointer call sites across a goto model |
label_function_pointer_call_sites.h | Label function pointer call sites across a goto model |
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 |
name_mangler.cpp | |
name_mangler.h | Mangle names of file-local functions to make them unique |
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 |
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_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 | Replace function returns by assignments to global variables |
remove_returns.h | Replace function returns by assignments to global variables |
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 | Functions for replacing virtual function call with a static function calls in functions, groups of functions and goto programs |
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 |
restrict_function_pointers.cpp | |
restrict_function_pointers.h | Given goto functions and a list of function parameters or globals that are function pointers with lists of possible candidates, replace use of these function pointers with calls to the candidate |
rewrite_union.cpp | Symbolic Execution of ANSI-C |
rewrite_union.h | Symbolic Execution |
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 |
structured_trace_util.cpp | Utilities for printing location info steps in the trace in a format agnostic way |
structured_trace_util.h | Utilities for printing location info steps in the trace in a format agnostic way |
system_library_symbols.cpp | Goto Programs |
system_library_symbols.h | Goto Programs |
validate_goto_model.cpp | |
validate_goto_model.h | |
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_expr.cpp | Expressions in XML |
xml_expr.h | |
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 |
call_stack.h | |
complexity_limiter.cpp | |
complexity_limiter.h | Symbolic Execution |
complexity_violation.h | |
expr_skeleton.cpp | Expression skeleton |
expr_skeleton.h | Expression skeleton |
field_sensitivity.cpp | |
field_sensitivity.h | |
frame.h | Class for stack frames |
goto_state.cpp | |
goto_state.h | Goto_statet class definition |
goto_symex.cpp | Symbolic Execution |
goto_symex.h | Symbolic Execution |
goto_symex_is_constant.h | GOTO Symex constant propagation |
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 |
renamed.h | Class for expressions or types renamed up to a given level |
renaming_level.cpp | Renaming levels |
renaming_level.h | Renaming levels |
show_program.cpp | Output of the program (SSA) constraints |
show_program.h | Output of the program (SSA) constraints |
show_vcc.cpp | Output of the verification conditions (VCCs) |
show_vcc.h | Output of the verification conditions (VCCs) |
slice.cpp | Slicer for symex traces |
slice.h | Slicer for symex traces |
ssa_step.cpp | |
ssa_step.h | |
symex_assign.cpp | Symbolic Execution |
symex_assign.h | Symbolic Execution of assignments |
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_complexity_limit_exceeded_action.h | |
symex_config.h | Symbolic Execution |
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 Implementation of functions to build SSA equation |
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 | |
assignments_from_json.cpp | |
assignments_from_json.h | |
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 |
code_with_references.cpp | |
code_with_references.h | |
convert_java_nondet.cpp | Convert side_effect_expr_nondett expressions |
convert_java_nondet.h | Convert side_effect_expr_nondett expressions using java_object_factory |
create_array_with_type_intrinsic.cpp | Implementation of CProver.createArrayWithType intrinsic |
create_array_with_type_intrinsic.h | Implementation of CProver.createArrayWithType intrinsic |
expr2java.cpp | |
expr2java.h | |
generic_parameter_specialization_map.cpp | |
generic_parameter_specialization_map.h | |
generic_parameter_specialization_map_keys.cpp | |
generic_parameter_specialization_map_keys.h | Author: Diffblue Ltd |
jar_file.cpp | |
jar_file.h | |
jar_pool.cpp | |
jar_pool.h | |
java_bmc_util.cpp | Bounded Model Checking Utils for Java |
java_bmc_util.h | Bounded Model Checking Utils for Java |
java_bytecode_concurrency_instrumentation.cpp | |
java_bytecode_concurrency_instrumentation.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_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_base.cpp | |
java_class_loader_base.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_expr.h | Java-specific exprt subclasses |
java_local_variable_table.cpp | Java local variable table processing |
java_multi_path_symex_checker.cpp | |
java_multi_path_symex_checker.h | Goto Checker using Bounded Model Checking for Java |
java_multi_path_symex_only_checker.h | Goto Checker using Bounded Model Checking for Java |
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_object_factory_parameters.cpp | |
java_object_factory_parameters.h | |
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_single_path_symex_checker.cpp | |
java_single_path_symex_checker.h | Goto Checker using Single Path Symbolic Execution for Java |
java_single_path_symex_only_checker.h | Goto Checker using Single Path Symbolic Execution for Java |
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_literal_expr.h | Representation of a constant Java string |
java_string_literals.cpp | |
java_string_literals.h | |
java_trace_validation.cpp | |
java_trace_validation.h | |
java_types.cpp | |
java_types.h | |
java_utils.cpp | |
java_utils.h | |
lambda_synthesis.cpp | Java lambda code synthesis |
lambda_synthesis.h | Java lambda code synthesis |
lazy_goto_functions_map.h | Author: Diffblue Ltd |
lazy_goto_model.cpp | Author: Diffblue Ltd |
lazy_goto_model.h | Author: Diffblue Ltd |
lift_clinit_calls.cpp | |
lift_clinit_calls.h | |
load_method_by_regex.cpp | |
load_method_by_regex.h | Process a pattern to use as a regex for selecting extra entry points for ci_lazy_methodst |
mz_zip_archive.cpp | |
mz_zip_archive.h | |
pattern.h | Pattern matching for bytecode instructions |
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_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_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 |
► json | |
json_interface.cpp | JSON Commandline Interface |
json_interface.h | JSON Commandline Interface |
json_parser.cpp | |
json_parser.h | |
► json-symtab-language | |
json_symbol.cpp | |
json_symbol.h | |
json_symbol_table.cpp | |
json_symbol_table.h | |
json_symtab_language.cpp | |
json_symtab_language.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_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-analyzer | |
analyze_symbol.cpp | |
analyze_symbol.h | High-level interface to gdb |
gdb_api.cpp | Low-level interface to gdb |
gdb_api.h | Low-level interface to gdb |
memory_analyzer_main.cpp | Memory analyzer interface |
memory_analyzer_parse_options.cpp | Commandline parser for the memory analyzer executing main work |
memory_analyzer_parse_options.h | This code does the command line parsing for the memory-analyzer tool |
nonstd | |
► pointer-analysis | |
add_failed_symbols.cpp | Pointer Dereferencing |
add_failed_symbols.h | 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 | Object Numbering |
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.h | Value Set Propagation |
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.h | Value Set (Flow Insensitive, Sharing, 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.h | Value Set (Flow Insensitive, Sharing, Validity Regions) |
value_set_fivrns.h | Value Set (Flow Insensitive, Validity Regions) |
value_sets.h | Value Set Propagation |
► solvers | |
► bdd | |
► 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 |
bdd.h | Choice between the different interface to BDD libraries |
bdd_cudd.h | Interface to Cudd BDD functions that are used in CBMC BDD functions should only be accessed through this header file |
bdd_miniBDD.h | Interface to miniBDD functions that are used in CBMC BDD functions should only be accessed through this header file |
► 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_dimacs.cpp | Writing DIMACS Files |
bv_dimacs.h | Writing DIMACS Files |
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 | |
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 | |
byte_operators.cpp | |
expr_lowering.h | |
functions.cpp | |
functions.h | Uninterpreted Functions |
popcount.cpp | |
► prop | |
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 | |
prop.cpp | |
prop.h | |
prop_conv.cpp | |
prop_conv.h | |
prop_conv_solver.cpp | |
prop_conv_solver.h | |
prop_minimize.cpp | Minimize some target function incrementally |
prop_minimize.h | SAT Minimizer |
solver_resource_limits.h | Solver capability to set resource limits |
► 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 | |
► 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 | |
external_sat.cpp | Allows call an external SAT solver to allow faster integration of newer SAT solvers |
external_sat.h | Allows calling an external SAT solver to allow faster integration of newer SAT solvers |
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 | |
letify.cpp | Introduce LET for common subexpressions |
letify.h | |
smt2_conv.cpp | SMT Backend |
smt2_conv.h | |
smt2_dec.cpp | |
smt2_dec.h | |
smt2_format.cpp | |
smt2_format.h | |
smt2_parser.cpp | |
smt2_parser.h | |
smt2_solver.cpp | |
smt2_tokenizer.cpp | |
smt2_tokenizer.h | |
smt2irep.cpp | |
smt2irep.h | |
► strings | |
array_pool.cpp | |
array_pool.h | Associates arrays and length to pointers, so that the string refinement can transform builtin function calls with pointer arguments to formulas over arrays |
equation_symbol_mapping.cpp | |
equation_symbol_mapping.h | |
format_specifier.cpp | Format specifiers for String.format |
format_specifier.h | Format specifiers for String.format |
string_builtin_function.cpp | |
string_builtin_function.h | |
string_concatenation_builtin_function.cpp | Builtin functions for string concatenations |
string_concatenation_builtin_function.h | Builtin functions for string concatenations |
string_constraint.cpp | |
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_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_indexof.cpp | Generates string constraints for the family of indexOf and lastIndexOf 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_dependencies.cpp | |
string_dependencies.h | Keeps track of dependencies between strings |
string_format_builtin_function.cpp | Built-in function for String.format |
string_format_builtin_function.h | Built-in function for String.format |
string_insertion_builtin_function.cpp | |
string_insertion_builtin_function.h | |
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 | |
conflict_provider.h | Capability to check whether an expression is a reason for the solver returning UNSAT |
decision_procedure.cpp | Decision Procedure Interface |
decision_procedure.h | Decision Procedure Interface |
hardness_collector.h | Capability to collect the statistics of the complexity of individual solver queries |
solver_hardness.cpp | |
solver_hardness.h | |
stack_decision_procedure.h | Decision procedure with incremental solving with contexts and assumptions |
► statement-list | |
► converters | |
convert_bool_literal.cpp | Statement List Language Conversion |
convert_bool_literal.h | Statement List Language Conversion |
convert_dint_literal.cpp | Statement List Language Conversion |
convert_dint_literal.h | Statement List Language Conversion |
convert_int_literal.cpp | Statement List Language Conversion |
convert_int_literal.h | Statement List Language Conversion |
convert_real_literal.cpp | Statement List Language Conversion |
convert_real_literal.h | Statement List Language Conversion |
convert_string_value.cpp | Statement List Language Conversion |
convert_string_value.h | Statement List Language Conversion |
expr2statement_list.cpp | |
expr2statement_list.h | |
statement_list_types.cpp | Statement List Type Helper |
statement_list_types.h | Statement List Type Helper |
statement_list_entry_point.cpp | Statement List Language Entry Point |
statement_list_entry_point.h | Statement List Language Entry Point |
statement_list_language.cpp | Statement List Language Interface |
statement_list_language.h | Statement List Language Interface |
statement_list_parse_tree.cpp | Statement List Language Parse Tree |
statement_list_parse_tree.h | Statement List Language Parse Tree |
statement_list_parse_tree_io.cpp | Statement List Language Parse Tree Output |
statement_list_parse_tree_io.h | Statement List Language Parse Tree Output |
statement_list_parser.cpp | Statement List Language Parser |
statement_list_parser.h | Statement List Language Parser |
statement_list_typecheck.cpp | Statement List Language Type Checking |
statement_list_typecheck.h | Statement List Language Type Checking |
► symtab2gb | |
symtab2gb_main.cpp | Symtab2gb Main Module |
symtab2gb_parse_options.cpp | |
symtab2gb_parse_options.h | |
► unit | |
► testing-utils | |
call_graph_test_utils.cpp | |
call_graph_test_utils.h | |
expr_query.h | Helper class for querying expressions Throw CATCH exceptions when the query fails |
free_form_cmdline.cpp | |
free_form_cmdline.h | |
get_goto_model_from_c.cpp | |
get_goto_model_from_c.h | |
invariant.cpp | |
invariant.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 |
require_vectors_equal_unordered.h | |
run_test_with_compilers.cpp | |
run_test_with_compilers.h | Utility for running a test with different compilers |
use_catch.h | |
► util | |
allocate_objects.cpp | |
allocate_objects.h | |
arith_tools.cpp | |
arith_tools.h | |
array_element_from_pointer.cpp | |
array_element_from_pointer.h | |
array_name.cpp | Misc Utilities |
array_name.h | Misc Utilities |
as_const.h | |
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 | |
c_types_util.h | This file contains functions, that should support test for underlying c types, in cases where this is required for analysis purpose |
cmdline.cpp | |
cmdline.h | |
config.cpp | |
config.h | |
constructor_of.h | |
container_utils.h | |
cout_message.cpp | |
cout_message.h | |
cow.h | |
cprover_prefix.h | |
dense_integer_map.h | Dense integer map |
deprecate.h | |
dstring.cpp | Container for C-Strings |
dstring.h | Container for C-Strings |
edit_distance.cpp | |
edit_distance.h | |
endianness_map.cpp | |
endianness_map.h | |
exception_utils.cpp | |
exception_utils.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 | Forward depth-first search iterators These iterators' copy operations are expensive, so use auto&, and avoid std::next(), std::prev() and post-increment iterator |
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 | |
forward_list_as_map.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 |
identifier.cpp | |
identifier.h | |
ieee_float.cpp | |
ieee_float.h | |
infix.h | String infix shorthand |
integer_interval.h | |
interval.cpp | |
interval.h | |
interval_constraint.cpp | |
interval_constraint.h | |
interval_template.h | |
interval_union.cpp | |
interval_union.h | Union of intervals |
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_irep.cpp | Util |
json_irep.h | Util |
json_stream.cpp | |
json_stream.h | |
lazy.h | |
lispexpr.cpp | |
lispexpr.h | |
lispirep.cpp | |
lispirep.h | |
magic.h | Magic numbers used throughout the codebase |
make_unique.h | |
mathematical_expr.cpp | |
mathematical_expr.h | API to expression classes for 'mathematical' expressions |
mathematical_types.cpp | Mathematical types |
mathematical_types.h | Mathematical types |
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 | |
narrow.h | |
nfa.h | |
nodiscard.h | |
nondet.cpp | |
nondet.h | |
nondet_bool.h | Nondeterministic boolean helper |
numbering.h | |
object_factory_parameters.cpp | |
object_factory_parameters.h | |
optional.h | |
optional_utils.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_offset_sum.cpp | Pointer Analysis |
pointer_offset_sum.h | Pointer Dereferencing |
pointer_predicates.cpp | Various predicates over pointers in programs |
pointer_predicates.h | Various predicates over pointers in programs |
prefix.h | |
prefix_filter.cpp | Prefix Filtering |
prefix_filter.h | Prefix Filtering |
preprocessor.h | Preprocessing Base Class |
range.h | Ranges: pair of begin and end iterators, which can be initialized from containers, provide useful methods such as map, filter and concat which only manipulate iterators, and can be used with ranged-for |
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_if.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_n_way_ptr.h | |
small_shared_ptr.h | |
source_location.cpp | |
source_location.h | |
sparse_vector.h | Sparse Vectors |
ssa_expr.cpp | |
ssa_expr.h | |
std_code.cpp | Data structure representing different types of statements in a program |
std_code.h | |
std_expr.cpp | |
std_expr.h | API to expression classes |
std_types.cpp | Pre-defined types |
std_types.h | Pre-defined types |
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 | |
structured_data.cpp | |
structured_data.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 |
symbol_table_builder.h | |
tempdir.cpp | |
tempdir.h | |
tempfile.cpp | |
tempfile.h | |
threeval.cpp | |
threeval.h | |
timestamper.cpp | |
timestamper.h | Emit timestamps |
type.cpp | Implementations of some functions of typet |
type.h | Defines typet, type_with_subtypet and type_with_subtypest |
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 | |
validate.h | |
validate_code.cpp | |
validate_code.h | |
validate_expressions.cpp | |
validate_expressions.h | |
validate_helpers.h | |
validate_types.cpp | |
validate_types.h | |
validation_interface.h | |
validation_mode.h | |
version.h | |
xml.cpp | |
xml.h | |
xml_irep.cpp | |
xml_irep.h | |
► xmllang | |
graphml.cpp | Read/write graphs as GraphML |
graphml.h | Read/write graphs as GraphML |
xml_interface.cpp | XML Interface |
xml_interface.h | XML Interface |
xml_parse_tree.cpp | |
xml_parse_tree.h | |
xml_parser.cpp | |
xml_parser.h | |