File List

Here is a list of all files with brief descriptions:

[detail level 12345]

architectural
▼ 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
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
nondet.cpp
nondet.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
▼ src
► analyses
► variable-sensitivity
abstract_aggregate_object.h	Common behaviour for abstract objects modelling aggregate values - arrays, structs, etc
abstract_environment.cpp
abstract_environment.h	An abstract version of a program environment
abstract_object.cpp
abstract_object.h	Abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual variables in the general non-relational domain
abstract_object_set.cpp
abstract_object_set.h	Unordered set of value objects
abstract_object_statistics.h	Statistics gathering for the variable senstivity domain
abstract_pointer_object.cpp
abstract_pointer_object.h	The base of all pointer abstractions
abstract_value_object.cpp
abstract_value_object.h	Common behaviour for abstract objects modelling values - constants, intervals, etc
constant_abstract_value.cpp
constant_abstract_value.h	An abstraction of a single value that just stores a constant
constant_pointer_abstract_object.cpp
constant_pointer_abstract_object.h	An abstraction of a pointer that tracks a single pointer
context_abstract_object.cpp
context_abstract_object.h	General implementation of a an abstract_objectt which can track side information in the form of a 'context' associated with a wrapped abstract_objectt of some other type
data_dependency_context.cpp	Maintain data dependencies as a context in the variable sensitivity domain
data_dependency_context.h	Maintain data dependencies as a context in the variable sensitivity domain
full_array_abstract_object.cpp
full_array_abstract_object.h	An abstraction of an array value
full_struct_abstract_object.cpp
full_struct_abstract_object.h	An abstraction of a structure that stores one abstract object per field
interval_abstract_value.cpp
interval_abstract_value.h	An interval to represent a set of possible values
liveness_context.cpp
liveness_context.h	Maintain a context in the variable sensitvity domain that records the liveness region for a given abstract_objectt
location_update_visitor.h
map_visit.h
three_way_merge_abstract_interpreter.cpp	An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivity domain's three-way-merge operation on returning from a function call
three_way_merge_abstract_interpreter.h	An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivity domain's three-way-merge operation on returning from a function call
two_value_array_abstract_object.h	The base type of all abstract array representations
two_value_pointer_abstract_object.cpp
two_value_pointer_abstract_object.h
two_value_struct_abstract_object.h	The base of all structure abstractions
two_value_union_abstract_object.h	The base of all union abstractions
value_set_abstract_object.cpp	Value Set Abstract Object
value_set_abstract_object.h	Value Set Abstract Object
value_set_pointer_abstract_object.cpp	Value Set of Pointer Abstract Object
value_set_pointer_abstract_object.h	Value Set of Pointer Abstract Object
variable_sensitivity_configuration.cpp	Captures the user-supplied configuration for VSD, determining which domain abstractions are used, flow sensitivity, etc
variable_sensitivity_configuration.h	Captures the user-supplied configuration for VSD, determining which domain abstractions are used, flow sensitivity, etc
variable_sensitivity_dependence_graph.cpp
variable_sensitivity_dependence_graph.h	A forked and modified version of analyses/dependence_graph
variable_sensitivity_domain.cpp
variable_sensitivity_domain.h	There are different ways of handling arrays, structures, unions and pointers
variable_sensitivity_object_factory.cpp
variable_sensitivity_object_factory.h	Tracks the user-supplied configuration for VSD and build the correct type of abstract object when needed
widened_range.cpp
widened_range.h
write_location_context.cpp
write_location_context.h	Maintain a context in the variable sensitvity domain that records write locations for a given abstract_objectt
write_stack.cpp	Represents a stack of write operations to an addressable memory location
write_stack.h	Represents a stack of write operations to an addressable memory location
write_stack_entry.cpp	Represents an entry in the write_stackt
write_stack_entry.h	Represents an entry in the write_stackt
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_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
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
► compiler_headers
arm_builtin_headers.h
clang_builtin_headers.h
cw_builtin_headers.h
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-5.h
gcc_builtin_headers_ia32-6.h
gcc_builtin_headers_ia32-7.h
gcc_builtin_headers_ia32-8.h
gcc_builtin_headers_ia32-9.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
windows_builtin_headers.h
► goto-conversion
builtin_functions.cpp	Program Transformation
destructor.cpp	Destructor Calls
destructor.h	Destructor Calls
format_strings.cpp	Format String Parser
format_strings.h	Format String Parser
goto_asm.cpp	Assembler -> Goto
goto_check_c.cpp	Checks for Errors in C/C++ Programs
goto_check_c.h	Program Transformation
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
link_to_library.cpp	Library Linking
link_to_library.h	Library Linking
scope_tree.cpp
scope_tree.h
string_instrumentation.cpp	String Abstraction
string_instrumentation.h	String Abstraction
► library
cegis.c
converter.cpp
cprover.h	CPROVER built-in declarations to perform library checks
cprover_contracts.c	Types and functions for dynamic frames instrumentation in contracts
ctype.c
err.c
errno.c
fcntl.c
fenv.c
float.c
gcc.c
getopt.c
inet.c
intrin.c
java.io.c
jsa.h	Counterexample-Guided Inductive Synthesis
locale.c
math.c
mman.c
netdb.c
process.c
pthread_lib.c
pwd.c
random.c
semaphore.c
setjmp.c
signal.c
stdio.c
stdlib.c
string.c
strings.c
syslog.c
threads.c
time.c
unistd.c
windows.c
x86_assembler.c
► 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
allocate_objects.cpp
allocate_objects.h
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
builtin_factory.cpp
builtin_factory.h
c_expr.cpp
c_expr.h	API to expression classes that are internal to the C frontend
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_shadow_memory_builtin.cpp
c_typecheck_type.cpp	C++ Language Type Checking
c_typecheck_typecast.cpp
cprover_builtin_headers.h
cprover_library.cpp
cprover_library.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_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
printf_formatter.cpp	Printf Formatting
printf_formatter.h	Printf Formatting
type2name.cpp	Type Naming for C
type2name.h	Type Naming for C
typedef_type.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
new.c
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
► cprover
address_taken.cpp	Address Taken
address_taken.h	Address Taken
axioms.cpp	Axioms
axioms.h	Axioms
bv_pointers_wide.cpp
bv_pointers_wide.h
c_safety_checks.cpp	Checks for Errors in C/C++ Programs
c_safety_checks.h	Checks for Errors in C/C++ Programs
counterexample_found.cpp	Counterexample Found
counterexample_found.h	Counterexample Found
cprover_main.cpp	Cprover Main Module
cprover_parse_options.cpp	Cprover Command Line Options Processing
cprover_parse_options.h	Command Line Parsing
endianness_map_wide.cpp
endianness_map_wide.h
equality_propagation.cpp	Equality Propagation
equality_propagation.h	Equality Propagation
find_variables.cpp	Find Variables
find_variables.h	Find Variables
flatten_ok_expr.cpp
flatten_ok_expr.h
format_hooks.cpp
format_hooks.h
free_symbols.cpp
free_symbols.h	Free Symbols
generalization.cpp	Generalization
generalization.h	Generalization
inductiveness.cpp	Inductiveness
inductiveness.h	Inductiveness
instrument_contracts.cpp	Instrument Contracts
instrument_contracts.h	Instrument Given Invariants
instrument_given_invariants.cpp	Instrument Given Invariants
instrument_given_invariants.h	Instrument Given Invariants
may_alias.cpp	May Alias
may_alias.h	May Alias
may_be_same_object.cpp	May Be Same Object
may_be_same_object.h	May Be Same Object
propagate.cpp	Propagate
propagate.h	Propagate
report_properties.cpp	Solver
report_properties.h	Property Reporting
report_traces.cpp	Solver
report_traces.h	Report Traces
sentinel_dll.cpp	Axioms
sentinel_dll.h
simplify_state_expr.cpp	Simplify State Expressions
simplify_state_expr.h	Simplify State Expression
solver.cpp	Solver
solver.h	Equality Propagation
solver_progress.cpp	Solver Progress Reporting
solver_progress.h	Solver Progress Reporting
solver_types.cpp	Solver Types
solver_types.h	Solver
state.cpp
state.h
state_encoding.cpp
state_encoding.h	State Encoding
state_encoding_targets.cpp
state_encoding_targets.h
variable_encoding.cpp	Variable Encoding
variable_encoding.h	Variable Encoding
wcwidth.c
► crangler
c_defines.cpp	C_defines
c_defines.h	C_defines
c_wrangler.cpp	C Wrangler
c_wrangler.h	C Wrangler
crangler_main.cpp	CRANGLER Main Module
crangler_parse_options.cpp	CRANGLER Command Line Option Processing
crangler_parse_options.h	CRANGLER Command Line Option Processing
cscanner.cpp
cscanner.h	Cscanner
ctoken.cpp	Ctoken
ctoken.h	Ctoken
ctokenit.cpp	Ctokenit
ctokenit.h	Ctokenit
mini_c_parser.cpp	Mini C Parser
mini_c_parser.h	Mini C Parser
► goto-analyzer
build_analyzer.cpp
build_analyzer.h
goto_analyzer_languages.cpp	Language Registration
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-bmc
goto_bmc_main.cpp
goto_bmc_parse_options.cpp
goto_bmc_parse_options.h
► 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
fatal_assertions.cpp	Fatal Assertions
fatal_assertions.h	Fatal Assertions
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-inspect
goto_inspect_main.cpp
goto_inspect_parse_options.cpp
goto_inspect_parse_options.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
► contracts
► doc
developer
user
► dynamic-frames
dfcc.cpp
dfcc.h	Main class orchestrating the the whole program transformation for function contracts with Dynamic Frame Condition Checking (DFCC)
dfcc_cfg_info.cpp
dfcc_cfg_info.h	Class that computes CFG information about the loop structure of a GOTO function for the purpose of dynamic frame conditions checking and loop contract instrumentation
dfcc_check_loop_normal_form.cpp
dfcc_check_loop_normal_form.h	Checks normal form properties of natural loops in a GOTO program
dfcc_contract_clauses_codegen.cpp
dfcc_contract_clauses_codegen.h	Translates assigns and frees clauses of a function contract or loop contract into goto programs that build write sets or havoc write sets
dfcc_contract_functions.cpp
dfcc_contract_functions.h	Translates assigns and frees clauses of a function contract into goto functions that allow to build and havoc write sets dynamically
dfcc_contract_handler.cpp
dfcc_contract_handler.h	Specialisation of dfcc_contract_handlert for contracts
dfcc_contract_mode.cpp
dfcc_contract_mode.h	Enum type representing the contract checking and replacement modes
dfcc_infer_loop_assigns.cpp
dfcc_infer_loop_assigns.h	Infer a set of assigns clause targets for a natural loop
dfcc_instrument.cpp
dfcc_instrument.h	Add instrumentation to a goto program to perform frame condition checks
dfcc_instrument_loop.cpp
dfcc_instrument_loop.h	This class applies the loop contract transformation to a loop in a goto function
dfcc_is_cprover_symbol.cpp
dfcc_is_cprover_symbol.h
dfcc_is_freeable.cpp
dfcc_is_freeable.h	Instruments occurrences of is_freeable predicates in programs encoding requires and ensures clauses of contracts
dfcc_is_fresh.cpp
dfcc_is_fresh.h	Instruments occurrences of is_fresh predicates in programs encoding requires and ensures clauses of contracts
dfcc_library.cpp
dfcc_library.h	Dynamic frame condition checking library loading
dfcc_lift_memory_predicates.cpp
dfcc_lift_memory_predicates.h	Collects all user-defined predicates that call functions is_fresh, pointer_in_range, obeys_contract and lifts them to function taking pointers by reference
dfcc_loop_nesting_graph.cpp
dfcc_loop_nesting_graph.h	Builds a graph describing how loops are nested in a GOTO program
dfcc_loop_tags.cpp
dfcc_loop_tags.h	Functions that allow to tag GOTO instructions with loop identifiers and loop instruction type: head, body, exiting, latch
dfcc_obeys_contract.cpp
dfcc_obeys_contract.h	Instruments occurrences of obeys_contract predicates in programs encoding requires and ensures clauses of contracts
dfcc_pointer_in_range.cpp
dfcc_pointer_in_range.h	Instruments occurrences of pointer_in_range predicates in programs encoding requires and ensures clauses of contracts
dfcc_root_object.cpp
dfcc_root_object.h	Utility functions that compute root object expressions for assigns clause targets and LHS expressions
dfcc_spec_functions.cpp
dfcc_spec_functions.h	Translate functions that specify assignable and freeable targets declaratively into active functions that build write sets dynamically by rewriting calls to front-end functions into calls to library functions defining their dynamic semantics
dfcc_swap_and_wrap.cpp
dfcc_swap_and_wrap.h	Given a function_id and contract_id, swaps its body to a function with a fresh mangled name, instruments it for dynamic frame condition checking, and replaces the original function's body with instructions encoding contract checking against the mangled function, or contract replacement
dfcc_utils.cpp
dfcc_utils.h	Dynamic frame condition checking utility functions
dfcc_wrapper_program.cpp
dfcc_wrapper_program.h	Generates the body of a wrapper function from a contract for contract checking or contract replacement
cfg_info.h	Classes providing CFG-based information about symbols to guide simplifications in function and loop assigns clause checking
contracts.cpp	Verify and use annotated loop and function contracts
contracts.h	Verify and use annotated invariants and pre/post-conditions
contracts_wrangler.cpp	Parse and annotate contracts
contracts_wrangler.h	Parse and annotate contracts
havoc_assigns_clause_targets.cpp	Havoc multiple and possibly dependent targets simultaneously
havoc_assigns_clause_targets.h	Havoc function assigns clauses
inlining_decorator.cpp
inlining_decorator.h
instrument_spec_assigns.cpp	Specify write set in code contracts
instrument_spec_assigns.h	Specify write set in function contracts
loop_contract_config.h	Config for loop contract
memory_predicates.cpp	Predicates to specify memory footprint in function contracts
memory_predicates.h	Predicates to specify memory footprint in function contracts
utils.cpp
utils.h
► 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
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_assume.cpp	Author: Diffblue Ltd
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_assigns.cpp	Compute objects assigned to in a function
function_assigns.h	Compute objects assigned to in a function
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
havoc_utils.cpp	Utilities for building havoc code for expressions
havoc_utils.h	Utilities for building havoc code for expressions
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
adjust_float_expressions.cpp	Symbolic Execution
adjust_float_expressions.h	Symbolic Execution
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
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
goto_check.cpp	GOTO Programs
goto_check.h	Checks for Errors in C and Java Programs
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 This gives a number of different interfaces to the function inlining functionality of goto_inlinet
goto_inline_class.cpp	Function Inlining
goto_inline_class.h	Function Inlining This is a class that encapsulates the state and functionality needed to do inline multiple function calls
goto_instruction_code.cpp	Data structures representing instructions in a GOTO program
goto_instruction_code.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
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
process_goto_program.cpp	Get a Goto Program
process_goto_program.h
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_rw_ok.cpp
rewrite_rw_ok.h	Rewrite r/w/rw_ok expressions to ones including prophecy variables recording the state
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
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_code.cpp
validate_code.h
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_can_forward_propagate.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
shadow_memory.cpp	Symex Shadow Memory Instrumentation
shadow_memory.h	Symex Shadow Memory Instrumentation
shadow_memory_field_definitions.h	Symex Shadow Memory Field Definitions
shadow_memory_state.h	Symex Shadow Memory Instrumentation State
shadow_memory_util.cpp	Symex Shadow Memory Instrumentation Utilities
shadow_memory_util.h	Symex Shadow Memory Instrumentation Utilities
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
solver_hardness.cpp
solver_hardness.h
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_set_return_value.cpp	Symbolic Execution of ANSI-C
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
► goto-synthesizer
cegis_evaluator.cpp	Evaluate if an expression is consistent with examples
cegis_evaluator.h	Evaluate if an expression is consistent with examples
cegis_verifier.cpp	Verifier for Counterexample-Guided Synthesis
cegis_verifier.h	Verifier for Counterexample-Guided Synthesis
dump_loop_contracts.cpp	Dump Loop Contracts as JSON
dump_loop_contracts.h	Dump Loop Contracts as JSON
enumerative_loop_contracts_synthesizer.cpp	Enumerative Loop Contracts Synthesizer
enumerative_loop_contracts_synthesizer.h	Enumerative Loop Contracts Synthesizer
expr_enumerator.cpp
expr_enumerator.h	Enumerator Interface
goto_synthesizer_languages.cpp	Language Registration
goto_synthesizer_main.cpp	Main Module
goto_synthesizer_parse_options.cpp	Main Module
goto_synthesizer_parse_options.h	Command Line Parsing
loop_contracts_synthesizer_base.h	Loop Contracts Synthesizer Interface
synthesizer_utils.cpp
synthesizer_utils.h
► 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
► libcprover-cpp
api.cpp
api.h
api_options.cpp
api_options.h
verification_result.cpp	Interface for the various verification engines providing results
verification_result.h	Interface for the various verification engines providing results
► libcprover-rust
► include
c_api.h
c_errors.h
► other
example.c
► linking
casting_replace_symbol.cpp	ANSI-C Linking
casting_replace_symbol.h	ANSI-C Linking
linking.cpp	ANSI-C Linking
linking.h	ANSI-C Linking
linking_class.h	ANSI-C Linking
linking_diagnostics.cpp	ANSI-C Linking
linking_diagnostics.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
► 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
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_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_fi.cpp	Value Set (Flow Insensitive, Sharing)
value_set_fi.h	Value Set (Flow Insensitive, Sharing)
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_bitreverse.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_mod_rem.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_update_bit.cpp
boolbv_update_bits.cpp
boolbv_width.cpp
boolbv_width.h
boolbv_with.cpp
bv_dimacs.cpp	Writing DIMACS Files
bv_dimacs.h	Writing DIMACS Files
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
literal_vector_expr.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
functions.cpp
functions.h	Uninterpreted Functions
► 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
► smt2_incremental
► ast
smt_commands.cpp
smt_commands.h
smt_index.cpp
smt_index.h
smt_logics.cpp
smt_logics.h
smt_options.cpp
smt_options.h
smt_responses.cpp
smt_responses.h
smt_sorts.cpp
smt_sorts.h	Data structure for smt sorts
smt_terms.cpp
smt_terms.h
► encoding
enum_encoding.cpp
enum_encoding.h
nondet_padding.cpp
nondet_padding.h	Expressions for use in incremental SMT2 decision procedure
struct_encoding.cpp
struct_encoding.h
► theories
smt_array_theory.cpp
smt_array_theory.h
smt_bit_vector_theory.cpp
smt_bit_vector_theory.h
smt_core_theory.cpp
smt_core_theory.h
construct_value_expr_from_smt.cpp
construct_value_expr_from_smt.h
convert_expr_to_smt.cpp
convert_expr_to_smt.h
object_tracking.cpp
object_tracking.h	Data structures and algorithms used by smt2_incremental_decision_proceduret to track data about the objects which pointers point to
response_or_error.h
smt2_incremental_decision_procedure.cpp
smt2_incremental_decision_procedure.h	Decision procedure with incremental SMT2 solving
smt_is_dynamic_object.cpp
smt_is_dynamic_object.h
smt_object_size.cpp
smt_object_size.h
smt_response_validation.cpp	Validation of smt response parse trees to produce either a strongly typed smt_responset representation, or a set of error messages
smt_response_validation.h
smt_solver_process.cpp
smt_solver_process.h
smt_to_smt2_string.cpp
smt_to_smt2_string.h	Streaming SMT data structures to a string based output stream
type_size_mapping.cpp
type_size_mapping.h	Utilities for making a map of types to associated sizes
► 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
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
► util
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
bitvector_expr.cpp
bitvector_expr.h	API to expression classes for bitvectors
bitvector_types.cpp	Pre-defined bitvector types
bitvector_types.h	Pre-defined bitvector types
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
console.cpp
console.h	Console
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
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
floatbv_expr.cpp
floatbv_expr.h	API to expression classes for floating-point arithmetic
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
help_formatter.cpp
help_formatter.h	Help Formatter
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
lower_byte_operators.cpp
magic.h	Magic numbers used throughout the codebase
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
memory_units.cpp
memory_units.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
nondet_bool.h	Nondeterministic boolean helper
numbering.h
object_factory_parameters.cpp
object_factory_parameters.h
optional_utils.h
options.cpp	Options
options.h	Options
parse_options.cpp
parse_options.h
parser.cpp
parser.h	Parser utilities
piped_process.cpp	Subprocess communication with pipes
piped_process.h	Subprocess communication with pipes
pointer_expr.cpp
pointer_expr.h	API to expression classes for Pointers
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_code_base.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
substitute_symbols.cpp	Free Symbols
substitute_symbols.h	Symbol Substitution
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_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
▼ 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
smt2irep.cpp
smt2irep.h
use_catch.h