cprover
File List
Here is a list of all files with brief descriptions:
[detail level
1
2
3
4
5
]
►
analyses
ai.cpp
ai.h
ai_domain.cpp
ai_domain.h
call_graph.cpp
call_graph.h
call_graph_helpers.cpp
call_graph_helpers.h
cfg_dominators.h
constant_propagator.cpp
constant_propagator.h
custom_bitvector_analysis.cpp
custom_bitvector_analysis.h
dependence_graph.cpp
dependence_graph.h
dirty.cpp
dirty.h
does_remove_const.cpp
does_remove_const.h
escape_analysis.cpp
escape_analysis.h
flow_insensitive_analysis.cpp
flow_insensitive_analysis.h
global_may_alias.cpp
global_may_alias.h
goto_check.cpp
goto_check.h
goto_rw.cpp
goto_rw.h
interval_analysis.cpp
interval_analysis.h
interval_domain.cpp
interval_domain.h
interval_template.h
invariant_propagation.cpp
invariant_propagation.h
invariant_set.cpp
invariant_set.h
invariant_set_domain.cpp
invariant_set_domain.h
is_threaded.cpp
is_threaded.h
local_bitvector_analysis.cpp
local_bitvector_analysis.h
local_cfg.cpp
local_cfg.h
local_may_alias.cpp
local_may_alias.h
local_safe_pointers.cpp
local_safe_pointers.h
locals.cpp
locals.h
natural_loops.cpp
natural_loops.h
reaching_definitions.cpp
reaching_definitions.h
static_analysis.cpp
static_analysis.h
uncaught_exceptions_analysis.cpp
uncaught_exceptions_analysis.h
uninitialized_domain.cpp
uninitialized_domain.h
►
ansi-c
►
library
converter.cpp
cprover.h
jsa.h
►
literals
convert_character_literal.cpp
convert_character_literal.h
convert_float_literal.cpp
convert_float_literal.h
convert_integer_literal.cpp
convert_integer_literal.h
convert_string_literal.cpp
convert_string_literal.h
parse_float.cpp
parse_float.h
unescape_string.cpp
unescape_string.h
anonymous_member.cpp
anonymous_member.h
ansi_c_convert_type.cpp
ansi_c_convert_type.h
ansi_c_declaration.cpp
ansi_c_declaration.h
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_typecheck.h
ansi_c_y.tab.cpp
ansi_c_y.tab.h
arm_builtin_headers.h
builtin_factory.cpp
builtin_factory.h
c_misc.cpp
c_misc.h
c_nondet_symbol_factory.cpp
c_nondet_symbol_factory.h
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_argc_argv.cpp
c_typecheck_base.cpp
c_typecheck_base.h
c_typecheck_code.cpp
c_typecheck_expr.cpp
c_typecheck_initializer.cpp
c_typecheck_type.cpp
c_typecheck_typecast.cpp
clang_builtin_headers.h
cprover_builtin_headers.h
cprover_library.cpp
cprover_library.h
cw_builtin_headers.h
designator.cpp
designator.h
expr2c.cpp
expr2c.h
expr2c_class.h
file_converter.cpp
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
merged_type.h
padding.cpp
padding.h
preprocessor_line.cpp
preprocessor_line.h
type2name.cpp
type2name.h
typedef_type.h
windows_builtin_headers.h
►
assembler
assembler_lex.yy.cpp
assembler_parser.cpp
assembler_parser.h
►
big-int
allocainc.h
►
cbmc
all_properties.cpp
all_properties_class.h
bmc.cpp
bmc.h
bmc_cover.cpp
cbmc_languages.cpp
cbmc_main.cpp
cbmc_parse_options.cpp
cbmc_parse_options.h
counterexample_beautification.cpp
counterexample_beautification.h
fault_localization.cpp
fault_localization.h
symex_bmc.cpp
symex_bmc.h
symex_coverage.cpp
symex_coverage.h
xml_interface.cpp
xml_interface.h
►
cpp
►
library
cprover.h
cpp_constructor.cpp
cpp_convert_type.cpp
cpp_convert_type.h
cpp_declaration.cpp
cpp_declaration.h
cpp_declarator.cpp
cpp_declarator.h
cpp_declarator_converter.cpp
cpp_declarator_converter.h
cpp_destructor.cpp
cpp_enum_type.cpp
cpp_enum_type.h
cpp_exception_id.cpp
cpp_exception_id.h
cpp_id.cpp
cpp_id.h
cpp_instantiate_template.cpp
cpp_internal_additions.cpp
cpp_internal_additions.h
cpp_is_pod.cpp
cpp_item.h
cpp_language.cpp
cpp_language.h
cpp_linkage_spec.h
cpp_member_spec.h
cpp_name.cpp
cpp_name.h
cpp_namespace_spec.cpp
cpp_namespace_spec.h
cpp_parse_tree.cpp
cpp_parse_tree.h
cpp_parser.cpp
cpp_parser.h
cpp_scope.cpp
cpp_scope.h
cpp_scopes.cpp
cpp_scopes.h
cpp_static_assert.h
cpp_storage_spec.h
cpp_template_args.h
cpp_template_parameter.h
cpp_template_type.h
cpp_token.h
cpp_token_buffer.cpp
cpp_token_buffer.h
cpp_type2name.cpp
cpp_type2name.h
cpp_typecast.h
cpp_typecheck.cpp
cpp_typecheck.h
cpp_typecheck_bases.cpp
cpp_typecheck_code.cpp
cpp_typecheck_compound_type.cpp
cpp_typecheck_constructor.cpp
cpp_typecheck_conversions.cpp
cpp_typecheck_declaration.cpp
cpp_typecheck_destructor.cpp
cpp_typecheck_enum_type.cpp
cpp_typecheck_expr.cpp
cpp_typecheck_fargs.cpp
cpp_typecheck_fargs.h
cpp_typecheck_function.cpp
cpp_typecheck_initializer.cpp
cpp_typecheck_linkage_spec.cpp
cpp_typecheck_method_bodies.cpp
cpp_typecheck_namespace.cpp
cpp_typecheck_resolve.cpp
cpp_typecheck_resolve.h
cpp_typecheck_static_assert.cpp
cpp_typecheck_template.cpp
cpp_typecheck_type.cpp
cpp_typecheck_using.cpp
cpp_typecheck_virtual_table.cpp
cpp_using.h
cpp_util.cpp
cpp_util.h
cprover_library.cpp
cprover_library.h
expr2cpp.cpp
expr2cpp.h
parse.cpp
template_map.cpp
template_map.h
►
doc
architectural
►
assets
driver.h
kdev_t.h
modules.h
►
goto-analyzer
goto_analyzer_main.cpp
goto_analyzer_parse_options.cpp
goto_analyzer_parse_options.h
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.h
taint_parser.cpp
taint_parser.h
unreachable_instructions.cpp
unreachable_instructions.h
►
goto-cc
armcc_cmdline.cpp
armcc_cmdline.h
armcc_mode.cpp
armcc_mode.h
as86_cmdline.cpp
as86_cmdline.h
as_cmdline.cpp
as_cmdline.h
as_mode.cpp
as_mode.h
bcc_cmdline.cpp
bcc_cmdline.h
compile.cpp
compile.h
cw_mode.cpp
cw_mode.h
gcc_cmdline.cpp
gcc_cmdline.h
gcc_mode.cpp
gcc_mode.h
gcc_version.cpp
gcc_version.h
goto_cc_cmdline.cpp
goto_cc_cmdline.h
goto_cc_languages.cpp
goto_cc_main.cpp
goto_cc_mode.cpp
goto_cc_mode.h
hybrid_binary.cpp
hybrid_binary.h
ld_cmdline.cpp
ld_cmdline.h
ld_mode.cpp
ld_mode.h
linker_script_merge.cpp
linker_script_merge.h
Merge linker script-defined symbols into a goto-program
ms_cl_cmdline.cpp
ms_cl_cmdline.h
ms_cl_mode.cpp
ms_cl_mode.h
ms_cl_version.cpp
ms_cl_version.h
ms_link_cmdline.cpp
ms_link_cmdline.h
ms_link_mode.cpp
ms_link_mode.h
►
goto-checker
solver_factory.cpp
solver_factory.h
►
goto-diff
change_impact.cpp
change_impact.h
goto_diff.h
goto_diff_base.cpp
goto_diff_languages.cpp
goto_diff_languages.h
goto_diff_main.cpp
goto_diff_parse_options.cpp
goto_diff_parse_options.h
syntactic_diff.cpp
syntactic_diff.h
unified_diff.cpp
unified_diff.h
►
goto-instrument
►
accelerate
accelerate.cpp
accelerate.h
acceleration_utils.cpp
acceleration_utils.h
accelerator.h
all_paths_enumerator.cpp
all_paths_enumerator.h
cone_of_influence.cpp
cone_of_influence.h
disjunctive_polynomial_acceleration.cpp
disjunctive_polynomial_acceleration.h
enumerating_loop_acceleration.cpp
enumerating_loop_acceleration.h
overflow_instrumenter.cpp
overflow_instrumenter.h
path.cpp
path.h
path_enumerator.h
polynomial.cpp
polynomial.h
polynomial_accelerator.cpp
polynomial_accelerator.h
sat_path_enumerator.cpp
sat_path_enumerator.h
scratch_program.cpp
scratch_program.h
subsumed.h
trace_automaton.cpp
trace_automaton.h
util.cpp
util.h
►
wmm
abstract_event.cpp
abstract_event.h
cycle_collection.cpp
data_dp.cpp
data_dp.h
event_graph.cpp
event_graph.h
fence.cpp
fence.h
goto2graph.cpp
goto2graph.h
instrumenter_pensieve.h
instrumenter_strategies.cpp
pair_collection.cpp
shared_buffers.cpp
shared_buffers.h
weak_memory.cpp
weak_memory.h
wmm.h
aggressive_slicer.cpp
aggressive_slicer.h
alignment_checks.cpp
alignment_checks.h
branch.cpp
branch.h
call_sequences.cpp
call_sequences.h
code_contracts.cpp
code_contracts.h
concurrency.cpp
concurrency.h
count_eloc.cpp
count_eloc.h
cover.cpp
cover.h
cover_basic_blocks.cpp
cover_basic_blocks.h
cover_filter.cpp
cover_filter.h
cover_instrument.h
cover_instrument_branch.cpp
cover_instrument_condition.cpp
cover_instrument_decision.cpp
cover_instrument_location.cpp
cover_instrument_mcdc.cpp
cover_instrument_other.cpp
cover_util.cpp
cover_util.h
document_properties.cpp
document_properties.h
dot.cpp
dot.h
dump_c.cpp
dump_c.h
dump_c_class.h
full_slicer.cpp
full_slicer.h
full_slicer_class.h
function.cpp
function.h
function_modifies.cpp
function_modifies.h
goto_instrument_languages.cpp
goto_instrument_main.cpp
goto_instrument_parse_options.cpp
goto_instrument_parse_options.h
goto_program2code.cpp
goto_program2code.h
havoc_loops.cpp
havoc_loops.h
horn_encoding.cpp
horn_encoding.h
interrupt.cpp
interrupt.h
k_induction.cpp
k_induction.h
loop_utils.cpp
loop_utils.h
mmio.cpp
mmio.h
model_argc_argv.cpp
model_argc_argv.h
nondet_static.cpp
nondet_static.h
nondet_volatile.cpp
nondet_volatile.h
object_id.cpp
object_id.h
points_to.cpp
points_to.h
race_check.cpp
race_check.h
reachability_slicer.cpp
reachability_slicer.h
reachability_slicer_class.h
remove_function.cpp
remove_function.h
rw_set.cpp
rw_set.h
show_locations.cpp
show_locations.h
skip_loops.cpp
skip_loops.h
splice_call.cpp
splice_call.h
stack_depth.cpp
stack_depth.h
thread_instrumentation.cpp
thread_instrumentation.h
undefined_functions.cpp
undefined_functions.h
uninitialized.cpp
uninitialized.h
unwind.cpp
unwind.h
unwindset.cpp
unwindset.h
►
goto-programs
abstract_goto_model.h
adjust_float_expressions.cpp
adjust_float_expressions.h
builtin_functions.cpp
cfg.h
class_hierarchy.cpp
class_hierarchy.h
class_identifier.cpp
class_identifier.h
compute_called_functions.cpp
compute_called_functions.h
destructor.cpp
destructor.h
elf_reader.cpp
elf_reader.h
format_strings.cpp
format_strings.h
generate_function_bodies.cpp
generate_function_bodies.h
goto_asm.cpp
goto_clean_expr.cpp
goto_convert.cpp
goto_convert.h
goto_convert_class.h
goto_convert_exceptions.cpp
goto_convert_function_call.cpp
goto_convert_functions.cpp
goto_convert_functions.h
goto_convert_side_effect.cpp
goto_function.cpp
goto_function.h
goto_functions.cpp
goto_functions.h
goto_inline.cpp
goto_inline.h
goto_inline_class.cpp
goto_inline_class.h
goto_model.h
goto_program.cpp
goto_program.h
goto_trace.cpp
goto_trace.h
graphml_witness.cpp
graphml_witness.h
initialize_goto_model.cpp
initialize_goto_model.h
instrument_preconditions.cpp
instrument_preconditions.h
interpreter.cpp
interpreter.h
interpreter_class.h
interpreter_evaluate.cpp
json_goto_trace.cpp
json_goto_trace.h
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_model.h
link_to_library.cpp
link_to_library.h
loop_ids.cpp
loop_ids.h
mm_io.cpp
mm_io.h
osx_fat_reader.cpp
osx_fat_reader.h
parameter_assignments.cpp
parameter_assignments.h
pointer_arithmetic.cpp
pointer_arithmetic.h
printf_formatter.cpp
printf_formatter.h
property_checker.cpp
property_checker.h
read_bin_goto_object.cpp
read_bin_goto_object.h
read_goto_binary.cpp
read_goto_binary.h
rebuild_goto_start_function.cpp
rebuild_goto_start_function.h
remove_asm.cpp
remove_asm.h
remove_calls_no_body.cpp
remove_calls_no_body.h
remove_complex.cpp
remove_complex.h
remove_const_function_pointers.cpp
remove_const_function_pointers.h
remove_function_pointers.cpp
remove_function_pointers.h
remove_returns.cpp
remove_returns.h
remove_skip.cpp
remove_skip.h
remove_unreachable.cpp
remove_unreachable.h
remove_unused_functions.cpp
remove_unused_functions.h
remove_vector.cpp
remove_vector.h
remove_virtual_functions.cpp
remove_virtual_functions.h
replace_calls.cpp
replace_calls.h
resolve_inherited_component.cpp
resolve_inherited_component.h
rewrite_union.cpp
rewrite_union.h
safety_checker.cpp
safety_checker.h
set_properties.cpp
set_properties.h
show_goto_functions.cpp
show_goto_functions.h
show_goto_functions_json.cpp
show_goto_functions_json.h
show_goto_functions_xml.cpp
show_goto_functions_xml.h
show_properties.cpp
show_properties.h
show_symbol_table.cpp
show_symbol_table.h
slice_global_inits.cpp
slice_global_inits.h
string_abstraction.cpp
string_abstraction.h
string_instrumentation.cpp
string_instrumentation.h
system_library_symbols.cpp
system_library_symbols.h
vcd_goto_trace.cpp
vcd_goto_trace.h
wp.cpp
wp.h
write_goto_binary.cpp
write_goto_binary.h
xml_goto_trace.cpp
xml_goto_trace.h
►
goto-symex
auto_objects.cpp
build_goto_trace.cpp
build_goto_trace.h
equation_conversion_exceptions.h
goto_symex.cpp
goto_symex.h
goto_symex_state.cpp
goto_symex_state.h
memory_model.cpp
memory_model.h
memory_model_pso.cpp
memory_model_pso.h
memory_model_sc.cpp
memory_model_sc.h
memory_model_tso.cpp
memory_model_tso.h
partial_order_concurrency.cpp
partial_order_concurrency.h
path_storage.cpp
path_storage.h
Storage of symbolic execution paths to resume
postcondition.cpp
postcondition.h
precondition.cpp
precondition.h
renaming_level.cpp
renaming_level.h
show_program.cpp
show_program.h
show_vcc.cpp
show_vcc.h
slice.cpp
slice.h
slice_by_trace.cpp
slice_by_trace.h
symex_assign.cpp
symex_atomic_section.cpp
symex_builtin_functions.cpp
symex_catch.cpp
symex_clean_expr.cpp
symex_dead.cpp
symex_decl.cpp
symex_dereference.cpp
symex_dereference_state.cpp
symex_dereference_state.h
symex_function_call.cpp
symex_goto.cpp
symex_main.cpp
symex_other.cpp
symex_slice_class.h
symex_start_thread.cpp
symex_target.cpp
symex_target.h
symex_target_equation.cpp
symex_target_equation.h
symex_throw.cpp
►
jbmc
►
src
►
janalyzer
janalyzer_main.cpp
janalyzer_parse_options.cpp
janalyzer_parse_options.h
►
java_bytecode
►
library
converter.cpp
bytecode_info.cpp
bytecode_info.h
character_refine_preprocess.cpp
character_refine_preprocess.h
ci_lazy_methods.cpp
ci_lazy_methods.h
ci_lazy_methods_needed.cpp
ci_lazy_methods_needed.h
convert_java_nondet.cpp
convert_java_nondet.h
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
jar_pool.cpp
jar_pool.h
java_bytecode_concurrency_instrumentation.cpp
java_bytecode_concurrency_instrumentation.h
java_bytecode_convert_class.cpp
java_bytecode_convert_class.h
java_bytecode_convert_method.cpp
java_bytecode_convert_method.h
java_bytecode_convert_method_class.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_typecheck.h
java_bytecode_typecheck_code.cpp
java_bytecode_typecheck_expr.cpp
java_bytecode_typecheck_type.cpp
java_class_loader.cpp
java_class_loader.h
java_class_loader_base.cpp
java_class_loader_base.h
java_class_loader_limit.cpp
java_class_loader_limit.h
java_entry_point.cpp
java_entry_point.h
java_enum_static_init_unwind_handler.cpp
java_enum_static_init_unwind_handler.h
java_local_variable_table.cpp
java_object_factory.cpp
java_object_factory.h
java_object_factory_parameters.cpp
java_object_factory_parameters.h
java_pointer_casts.cpp
java_pointer_casts.h
java_qualifiers.cpp
java_qualifiers.h
java_root_class.cpp
java_root_class.h
java_static_initializers.cpp
java_static_initializers.h
java_string_library_preprocess.cpp
java_string_library_preprocess.h
java_string_literals.cpp
java_string_literals.h
java_types.cpp
java_types.h
java_utils.cpp
java_utils.h
load_method_by_regex.cpp
load_method_by_regex.h
mz_zip_archive.cpp
mz_zip_archive.h
remove_exceptions.cpp
remove_exceptions.h
remove_instanceof.cpp
remove_instanceof.h
remove_java_new.cpp
remove_java_new.h
replace_java_nondet.cpp
replace_java_nondet.h
select_pointer_type.cpp
select_pointer_type.h
simple_method_stubbing.cpp
simple_method_stubbing.h
synthetic_methods_map.h
►
jbmc
jbmc_main.cpp
jbmc_parse_options.cpp
jbmc_parse_options.h
►
jdiff
java_syntactic_diff.cpp
java_syntactic_diff.h
jdiff_languages.cpp
jdiff_languages.h
jdiff_main.cpp
jdiff_parse_options.cpp
jdiff_parse_options.h
►
miniz
miniz.cpp
miniz.h
►
unit
►
java-testing-utils
load_java_class.cpp
load_java_class.h
require_goto_statements.cpp
require_goto_statements.h
require_parse_tree.cpp
require_parse_tree.h
require_type.cpp
require_type.h
►
jsil
expr2jsil.cpp
expr2jsil.h
jsil_convert.cpp
jsil_convert.h
jsil_entry_point.cpp
jsil_entry_point.h
jsil_internal_additions.cpp
jsil_internal_additions.h
jsil_language.cpp
jsil_language.h
jsil_lex.yy.cpp
jsil_parse_tree.cpp
jsil_parse_tree.h
jsil_parser.cpp
jsil_parser.h
jsil_typecheck.cpp
jsil_typecheck.h
jsil_types.cpp
jsil_types.h
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
►
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
language.h
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
linking.h
linking_class.h
remove_internal_symbols.cpp
remove_internal_symbols.h
static_lifetime_init.cpp
static_lifetime_init.h
nonstd
►
pointer-analysis
add_failed_symbols.cpp
add_failed_symbols.h
dereference.cpp
dereference.h
dereference_callback.h
goto_program_dereference.cpp
goto_program_dereference.h
object_numbering.h
pointer_offset_sum.cpp
pointer_offset_sum.h
rewrite_index.cpp
rewrite_index.h
show_value_sets.cpp
show_value_sets.h
value_set.cpp
value_set.h
value_set_analysis.cpp
value_set_analysis.h
value_set_analysis_fi.cpp
value_set_analysis_fi.h
value_set_analysis_fivr.cpp
value_set_analysis_fivr.h
value_set_analysis_fivrns.cpp
value_set_analysis_fivrns.h
value_set_dereference.cpp
value_set_dereference.h
value_set_domain.h
value_set_domain_fi.cpp
value_set_domain_fi.h
value_set_domain_fivr.cpp
value_set_domain_fivr.h
value_set_domain_fivrns.cpp
value_set_domain_fivrns.h
value_set_fi.cpp
value_set_fi.h
value_set_fivr.cpp
value_set_fivr.h
value_set_fivrns.cpp
value_set_fivrns.h
value_sets.h
►
solvers
►
flattening
arrays.cpp
arrays.h
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
bv_dimacs.cpp
bv_dimacs.h
bv_endianness_map.cpp
bv_endianness_map.h
bv_minimize.cpp
bv_minimize.h
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
functions.cpp
functions.h
pointer_logic.cpp
pointer_logic.h
►
floatbv
float_approximation.cpp
float_approximation.h
float_bv.cpp
float_bv.h
float_utils.cpp
float_utils.h
►
lowering
byte_operators.cpp
expr_lowering.h
flatten_byte_extract_exceptions.h
popcount.cpp
►
miniBDD
example.cpp
miniBDD.cpp
miniBDD.h
Small BDD implementation
►
prop
bdd_expr.cpp
bdd_expr.h
Binary decision diagram
cover_goals.cpp
cover_goals.h
literal.cpp
literal.h
literal_expr.h
minimize.cpp
minimize.h
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
qbf_squolem.h
qbf_squolem_core.cpp
qbf_squolem_core.h
qdimacs_cnf.cpp
qdimacs_cnf.h
qdimacs_core.cpp
qdimacs_core.h
►
refinement
bv_refinement.h
bv_refinement_loop.cpp
refine_arithmetic.cpp
refine_arrays.cpp
string_builtin_function.cpp
string_builtin_function.h
string_constraint.cpp
string_constraint.h
string_constraint_generator.h
string_constraint_generator_code_points.cpp
string_constraint_generator_comparison.cpp
string_constraint_generator_concat.cpp
string_constraint_generator_constants.cpp
string_constraint_generator_float.cpp
string_constraint_generator_format.cpp
string_constraint_generator_indexof.cpp
string_constraint_generator_insert.cpp
string_constraint_generator_main.cpp
string_constraint_generator_testing.cpp
string_constraint_generator_transformation.cpp
string_constraint_generator_valueof.cpp
string_constraint_instantiation.cpp
string_constraint_instantiation.h
string_refinement.cpp
string_refinement.h
string_refinement_invariant.h
string_refinement_util.cpp
string_refinement_util.h
►
sat
cnf.cpp
cnf.h
cnf_clause_list.cpp
cnf_clause_list.h
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
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
►
unit
►
testing-utils
call_graph_test_utils.cpp
call_graph_test_utils.h
free_form_cmdline.cpp
free_form_cmdline.h
message.cpp
message.h
require_expr.cpp
require_expr.h
require_symbol.cpp
require_symbol.h
require_vectors_equal_unordered.h
run_test_with_compilers.cpp
run_test_with_compilers.h
►
util
arith_tools.cpp
arith_tools.h
array_name.cpp
array_name.h
base_exceptions.h
base_type.cpp
base_type.h
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.h
deprecate.h
dstring.cpp
dstring.h
endianness_map.cpp
endianness_map.h
exception_utils.cpp
exception_utils.h
exit_codes.h
expanding_vector.h
expr.cpp
expr.h
expr_cast.h
Templated functions to cast to specific exprt-derived classes
expr_initializer.cpp
expr_initializer.h
expr_iterator.h
expr_util.cpp
expr_util.h
Deprecated expression utility functions
file_util.cpp
file_util.h
find_macros.cpp
find_macros.h
find_symbols.cpp
find_symbols.h
fixed_keys_map_wrapper.h
fixedbv.cpp
fixedbv.h
format.h
format_constant.cpp
format_constant.h
format_expr.cpp
format_expr.h
format_number_range.cpp
format_number_range.h
format_spec.h
format_type.cpp
format_type.h
freer.h
fresh_symbol.cpp
fresh_symbol.h
get_base_name.cpp
get_base_name.h
get_module.cpp
get_module.h
graph.h
guard.cpp
guard.h
identifier.cpp
identifier.h
ieee_float.cpp
ieee_float.h
infix.h
invariant.cpp
invariant.h
invariant_utils.cpp
invariant_utils.h
irep.cpp
irep.h
irep_hash.cpp
irep_hash.h
irep_hash_container.cpp
irep_hash_container.h
irep_ids.cpp
irep_ids.h
irep_serialization.cpp
irep_serialization.h
journalling_symbol_table.h
Author: Diffblue Ltd
json.cpp
json.h
json_expr.cpp
json_expr.h
json_irep.cpp
json_irep.h
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
mathematical_types.cpp
mathematical_types.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.h
nondet.cpp
nondet.h
nondet_bool.h
numbering.h
object_factory_parameters.cpp
object_factory_parameters.h
optional.h
optional_utils.h
options.cpp
options.h
parse_options.cpp
parse_options.h
parser.cpp
parser.h
pointer_offset_size.cpp
pointer_offset_size.h
pointer_predicates.cpp
pointer_predicates.h
prefix.h
preprocessor.h
range.h
rational.cpp
rational.h
rational_tools.cpp
rational_tools.h
ref_expr_set.cpp
ref_expr_set.h
reference_counting.h
refined_string_type.cpp
refined_string_type.h
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_node.h
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_shared_ptr.h
small_shared_two_way_ptr.h
source_location.cpp
source_location.h
sparse_vector.h
ssa_expr.cpp
ssa_expr.h
std_code.cpp
std_code.h
std_expr.cpp
std_expr.h
std_types.cpp
std_types.h
string2int.cpp
string2int.h
string_constant.cpp
string_constant.h
string_container.cpp
string_container.h
string_expr.h
string_hash.cpp
string_hash.h
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
symbol_table_builder.h
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_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
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.cpp
version.h
xml.cpp
xml.h
xml_expr.cpp
xml_expr.h
xml_irep.cpp
xml_irep.h
►
xmllang
graphml.cpp
graphml.h
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
Generated by
1.8.16