File List

Here is a list of all files with brief descriptions:

[detail level 123]

▶ analyses
ai.cpp	Abstract Interpretation
ai.h	Abstract Interpretation
call_graph.cpp	Function Call Graphs
call_graph.h	Function Call Graphs
cfg_dominators.h	Compute dominators for CFG of goto_function
constant_propagator.cpp	Constant Propagation
constant_propagator.h	Constant propagation
custom_bitvector_analysis.cpp	Field-insensitive, location-sensitive bitvector analysis
custom_bitvector_analysis.h	Field-insensitive, location-sensitive bitvector analysis
dependence_graph.cpp	Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010
dependence_graph.h	Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010
dirty.cpp	Local variables whose address is taken
dirty.h	Variables whose address is taken
does_remove_const.cpp	Analyses
does_remove_const.h	Analyses
escape_analysis.cpp	Field-insensitive, location-sensitive escape analysis
escape_analysis.h	Field-insensitive, location-sensitive, over-approximative escape analysis
flow_insensitive_analysis.cpp	Flow Insensitive Static Analysis
flow_insensitive_analysis.h	Flow Insensitive Static Analysis
global_may_alias.cpp	Field-insensitive, location-sensitive global may alias analysis
global_may_alias.h	Field-insensitive, location-sensitive, over-approximative escape analysis
goto_check.cpp	GOTO Programs
goto_check.h	Program Transformation
goto_rw.cpp
goto_rw.h
interval_analysis.cpp	Interval Analysis
interval_analysis.h	Interval Analysis
interval_domain.cpp	Interval Domain
interval_domain.h	Interval Domain
interval_template.h
invariant_propagation.cpp	Invariant Propagation
invariant_propagation.h	Invariant Propagation
invariant_set.cpp	Invariant Set
invariant_set.h	Value Set
invariant_set_domain.cpp	Invariant Set Domain
invariant_set_domain.h	Value Set
is_threaded.cpp	Over-approximate Concurrency for Threaded Goto Programs
is_threaded.h	Over-approximate Concurrency for Threaded Goto Programs
local_bitvector_analysis.cpp	Field-insensitive, location-sensitive may-alias analysis
local_bitvector_analysis.h	Field-insensitive, location-sensitive bitvector analysis
local_cfg.cpp	CFG for One Function
local_cfg.h	CFG for One Function
local_may_alias.cpp	Field-insensitive, location-sensitive may-alias analysis
local_may_alias.h	Field-insensitive, location-sensitive may-alias analysis
locals.cpp	Local variables
locals.h	Local variables whose address is taken
natural_loops.cpp	Dominators
natural_loops.h	Compute natural loops in a goto_function
reaching_definitions.cpp	Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis, Litvak et al., FSE 2010)
reaching_definitions.h	Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis, Litvak et al., FSE 2010)
replace_symbol_ext.cpp	Modified expression replacement for constant propagator
replace_symbol_ext.h	Modified expression replacement for constant propagator
static_analysis.cpp	Value Set Propagation
static_analysis.h	Static Analysis
uninitialized_domain.cpp	Detection for Uninitialized Local Variables
uninitialized_domain.h	Detection for Uninitialized Local Variables
▶ ansi-c
▶ library
converter.cpp
cprover.h
jsa.h	Counterexample-Guided Inductive Synthesis
▶ literals
convert_character_literal.cpp	C Language Conversion
convert_character_literal.h	C++ Language Conversion
convert_float_literal.cpp	C++ Language Conversion
convert_float_literal.h	C Language Conversion
convert_integer_literal.cpp	C++ Language Conversion
convert_integer_literal.h	C++ Language Conversion
convert_string_literal.cpp	C/C++ Language Conversion
convert_string_literal.h	C/C++ Language Conversion
parse_float.cpp	Conversion of Expressions
parse_float.h	ANSI-C Conversion / Type Checking
unescape_string.cpp	ANSI-C Language Conversion
unescape_string.h	ANSI-C Language Conversion
anonymous_member.cpp	ANSI-C Language Type Checking
anonymous_member.h	C Language Type Checking
ansi_c_convert_type.cpp	SpecC Language Conversion
ansi_c_convert_type.h	ANSI-C Language Conversion
ansi_c_declaration.cpp	ANSI-C Language Type Checking
ansi_c_declaration.h	ANSI-CC Language Type Checking
ansi_c_entry_point.cpp
ansi_c_entry_point.h
ansi_c_internal_additions.cpp
ansi_c_internal_additions.h
ansi_c_language.cpp
ansi_c_language.h
ansi_c_lex.yy.cpp
ansi_c_parse_tree.cpp
ansi_c_parse_tree.h
ansi_c_parser.cpp
ansi_c_parser.h
ansi_c_scope.cpp
ansi_c_scope.h
ansi_c_typecheck.cpp	ANSI-C Language Type Checking
ansi_c_typecheck.h	ANSI-C Language Type Checking
ansi_c_y.tab.cpp
ansi_c_y.tab.h
arm_builtin_headers.h
c_misc.cpp	ANSI-C Misc Utilities
c_misc.h	ANSI-C Misc Utilities
c_nondet_symbol_factory.cpp	C Nondet Symbol Factory
c_nondet_symbol_factory.h	C Nondet Symbol Factory
c_preprocess.cpp
c_preprocess.h
c_qualifiers.cpp
c_qualifiers.h
c_sizeof.cpp	Conversion of sizeof Expressions
c_sizeof.h
c_storage_spec.cpp
c_storage_spec.h
c_typecast.cpp
c_typecast.h
c_typecheck_argc_argv.cpp	ANSI-C Conversion / Type Checking
c_typecheck_base.cpp	ANSI-C Conversion / Type Checking
c_typecheck_base.h	ANSI-C Language Type Checking
c_typecheck_code.cpp	C Language Type Checking
c_typecheck_expr.cpp	ANSI-C Language Type Checking
c_typecheck_initializer.cpp	ANSI-C Conversion / Type Checking
c_typecheck_type.cpp	C++ Language Type Checking
c_typecheck_typecast.cpp
clang_builtin_headers.h
cprover_library.cpp
cprover_library.h
cw_builtin_headers.h
designator.cpp	ANSI-C Language Type Checking
designator.h	ANSI-C Language Type Checking
expr2c.cpp
expr2c.h
expr2c_class.h
file_converter.cpp	Convert file contents to C strings
gcc_builtin_headers_alpha.h
gcc_builtin_headers_arm.h
gcc_builtin_headers_generic.h
gcc_builtin_headers_ia32-2.h
gcc_builtin_headers_ia32-3.h
gcc_builtin_headers_ia32-4.h
gcc_builtin_headers_ia32.h
gcc_builtin_headers_math.h
gcc_builtin_headers_mem_string.h
gcc_builtin_headers_mips.h
gcc_builtin_headers_omp.h
gcc_builtin_headers_power.h
gcc_builtin_headers_tm.h
gcc_builtin_headers_ubsan.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
string_constant.cpp
string_constant.h
type2name.cpp	Type Naming for C
type2name.h	Type Naming for C
▶ assembler
assembler_lex.yy.cpp
assembler_parser.cpp
assembler_parser.h
▶ big-int
allocainc.h
▶ cbmc
all_properties.cpp	Symbolic Execution of ANSI-C
all_properties_class.h	Symbolic Execution of ANSI-C
bmc.cpp	Symbolic Execution of ANSI-C
bmc.h	Bounded Model Checking for ANSI-C + HDL
bmc_cover.cpp	Test-Suite Generation with BMC
bv_cbmc.cpp
bv_cbmc.h
cbmc_dimacs.cpp	Writing DIMACS Files
cbmc_dimacs.h	Writing DIMACS Files
cbmc_languages.cpp	Language Registration
cbmc_main.cpp	CBMC Main Module
cbmc_parse_options.cpp	CBMC Command Line Option Processing
cbmc_parse_options.h	CBMC Command Line Option Processing
cbmc_solvers.cpp	Solvers for VCs Generated by Symbolic Execution of ANSI-C
cbmc_solvers.h	Bounded Model Checking for ANSI-C + HDL
counterexample_beautification.cpp	Counterexample Beautification using Incremental SAT
counterexample_beautification.h	Counterexample Beautification
fault_localization.cpp	Fault Localization
fault_localization.h	Fault Localization
show_vcc.cpp	Symbolic Execution of ANSI-C
symex_bmc.cpp	Bounded Model Checking for ANSI-C
symex_bmc.h	Bounded Model Checking for ANSI-C
symex_coverage.cpp	Record and print code coverage of symbolic execution
symex_coverage.h	Record and print code coverage of symbolic execution
version.h
xml_interface.cpp	XML Interface
xml_interface.h	XML Interface
▶ clobber
clobber_main.cpp	Symex Main Module
clobber_parse_options.cpp	Symex Command Line Options Processing
clobber_parse_options.h	Command Line Parsing
▶ cpp
cpp_constructor.cpp	C++ Language Type Checking
cpp_convert_type.cpp	C++ Language Type Conversion
cpp_convert_type.h	C++ Language Conversion
cpp_declaration.cpp	C++ Language Type Checking
cpp_declaration.h	C++ Language Type Checking
cpp_declarator.cpp	C++ Language Type Checking
cpp_declarator.h	C++ Language Type Checking
cpp_declarator_converter.cpp	C++ Language Type Checking
cpp_declarator_converter.h	C++ Language Type Checking
cpp_destructor.cpp	C++ Language Type Checking
cpp_enum_type.cpp	C++ Language Type Checking
cpp_enum_type.h	C++ Language Type Checking
cpp_exception_id.cpp	C++ Language Type Checking
cpp_exception_id.h	C++ Language Type Checking
cpp_id.cpp	C++ Language Type Checking
cpp_id.h	C++ Language Type Checking
cpp_instantiate_template.cpp	C++ Language Type Checking
cpp_internal_additions.cpp
cpp_internal_additions.h
cpp_is_pod.cpp	C++ Language Type Checking
cpp_item.h	C++ Language Type Checking
cpp_language.cpp	C++ Language Module
cpp_language.h	C++ Language Module
cpp_linkage_spec.h	C++ Language Type Checking
cpp_member_spec.h
cpp_name.cpp	C++ Language Type Checking
cpp_name.h
cpp_namespace_spec.cpp	C++ Language Type Checking
cpp_namespace_spec.h	C++ Language Type Checking
cpp_parse_tree.cpp	C++ Parser
cpp_parse_tree.h	C++ Parser
cpp_parser.cpp	C++ Parser
cpp_parser.h	C++ Parser
cpp_scope.cpp	C++ Language Type Checking
cpp_scope.h	C++ Language Type Checking
cpp_scopes.cpp	C++ Language Type Checking
cpp_scopes.h	C++ Language Type Checking
cpp_static_assert.h	C++ Language Type Checking
cpp_storage_spec.h
cpp_template_args.h	C++ Language Type Checking
cpp_template_parameter.h
cpp_template_type.h
cpp_token.h	C++ Parser: Token
cpp_token_buffer.cpp	C++ Parser: Token Buffer
cpp_token_buffer.h	C++ Parser: Token Buffer
cpp_type2name.cpp	C++ Language Module
cpp_type2name.h	C++ Language Module
cpp_typecast.h
cpp_typecheck.cpp	C++ Language Type Checking
cpp_typecheck.h	C++ Language Type Checking
cpp_typecheck_bases.cpp	C++ Language Type Checking
cpp_typecheck_code.cpp	C++ Language Type Checking
cpp_typecheck_compound_type.cpp	C++ Language Type Checking
cpp_typecheck_constructor.cpp	C++ Language Type Checking
cpp_typecheck_conversions.cpp	C++ Language Type Checking
cpp_typecheck_declaration.cpp	C++ Language Type Checking
cpp_typecheck_destructor.cpp	C++ Language Type Checking
cpp_typecheck_enum_type.cpp	C++ Language Type Checking
cpp_typecheck_expr.cpp	C++ Language Type Checking
cpp_typecheck_fargs.cpp	C++ Language Type Checking
cpp_typecheck_fargs.h	C++ Language Type Checking
cpp_typecheck_function.cpp	C++ Language Type Checking
cpp_typecheck_initializer.cpp	C++ Language Type Checking
cpp_typecheck_linkage_spec.cpp	C++ Language Type Checking
cpp_typecheck_method_bodies.cpp	C++ Language Type Checking
cpp_typecheck_namespace.cpp	C++ Language Type Checking
cpp_typecheck_resolve.cpp	C++ Language Type Checking
cpp_typecheck_resolve.h	C++ Language Type Checking
cpp_typecheck_static_assert.cpp	C++ Language Type Checking
cpp_typecheck_template.cpp	C++ Language Type Checking
cpp_typecheck_type.cpp	C++ Language Type Checking
cpp_typecheck_using.cpp	C++ Language Type Checking
cpp_typecheck_virtual_table.cpp	C++ Language Type Checking
cpp_using.h	C++ Language Type Checking
cpp_util.cpp
cpp_util.h
expr2cpp.cpp
expr2cpp.h
parse.cpp	C++ Language Parsing
recursion_counter.h	C++ Language Type Checking
template_map.cpp	C++ Language Type Checking
template_map.h	C++ Language Type Checking
▶ doc
▶ assets
driver.h
kdev_t.h
modules.h
▶ goto-analyzer
goto_analyzer_main.cpp	Goto-Analyser Main Module
goto_analyzer_parse_options.cpp	Goto-Analyser Command Line Option Processing
goto_analyzer_parse_options.h	Goto-Analyser Command Line Option Processing
static_analyzer.cpp
static_analyzer.h
taint_analysis.cpp	Taint Analysis
taint_analysis.h	Taint Analysis
taint_parser.cpp	Taint Parser
taint_parser.h	Taint Parser
unreachable_instructions.cpp	List all unreachable instructions
unreachable_instructions.h	List all unreachable instructions
▶ goto-cc
▶ xml_binaries
read_goto_object.cpp	Read goto object files
read_goto_object.h	Read goto object files
xml_goto_function.cpp	Convert goto functions to xml structures and back
xml_goto_function.h	Convert goto functions into xml structures and back
xml_goto_function_hashing.cpp	Convert goto functions to xml structures and back (with irep hashing)
xml_goto_function_hashing.h	Convert goto functions into xml structures and back (with irep hashing)
xml_goto_program.cpp	Convert goto programs to xml structures and back
xml_goto_program.h	Convert goto programs into xml structures and back
xml_goto_program_hashing.cpp	Convert goto programs to xml structures and back (with irep hashing)
xml_goto_program_hashing.h	Convert goto programs into xml structures and back (with irep hashing)
xml_irep_hashing.cpp	XML-irep conversions with hashing
xml_irep_hashing.h	XML-irep conversions with hashing
xml_symbol.cpp	Compile and link source and object files
xml_symbol.h	Converts symbols to xml structures and back
xml_symbol_hashing.cpp	XML-symbol conversions with irep hashing
xml_symbol_hashing.h	XML-symbol conversions with irep hashing
armcc_cmdline.cpp	A special command line object to mimic ARM's armcc
armcc_cmdline.h	A special command line object to mimic ARM's armcc
armcc_mode.cpp	Command line option container
armcc_mode.h	Base class for command line interpretation for CL
as86_cmdline.cpp	A special command line object for as86 (of Bruce's C Compiler)
as86_cmdline.h	A special command line object for as86 (of Bruce's C Compiler) Author: Michael Tautschnig Date: July 2016
as_cmdline.cpp	A special command line object for GNU Assembler
as_cmdline.h	A special command line object for GNU Assembler Author: Michael Tautschnig Date: July 2016
as_mode.cpp	Assembler Mode
as_mode.h	Assembler Mode
bcc_cmdline.cpp	A special command line object for Bruce's C Compiler
bcc_cmdline.h	A special command line object for Bruce's C Compiler Author: Michael Tautschnig Date: July 2016
compile.cpp	Compile and link source and object files
compile.h	Compile and link source and object files
cw_mode.cpp	Command line option container
cw_mode.h	Base class for command line interpretation
gcc_cmdline.cpp	A special command line object for the gcc-like options
gcc_cmdline.h	A special command line object for the gcc-like options
gcc_mode.cpp	GCC Mode
gcc_mode.h	Base class for command line interpretation
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
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
ms_cl_cmdline.cpp	A special command line object for the CL options
ms_cl_cmdline.h	A special command line object for the gcc-like options
ms_cl_mode.cpp	Visual Studio CL Mode
ms_cl_mode.h	Visual Studio CL Mode
▶ goto-diff
change_impact.cpp	Data and control-dependencies of syntactic diff
change_impact.h	Data and control-dependencies of syntactic diff
goto_diff.h	GOTO-DIFF Base Class
goto_diff_base.cpp	GOTO-DIFF Base Class
goto_diff_languages.cpp	Language Registration
goto_diff_languages.h	GOTO-DIFF Languages
goto_diff_main.cpp	GOTO-DIFF Main Module
goto_diff_parse_options.cpp	GOTO-DIFF Command Line Option Processing
goto_diff_parse_options.h	GOTO-DIFF Command Line Option Processing
syntactic_diff.cpp	Syntactic GOTO-DIFF
syntactic_diff.h	Syntactic GOTO-DIFF
unified_diff.cpp	Unified diff (using LCSS) of goto functions
unified_diff.h	Unified diff (using LCSS) of goto functions
▶ goto-instrument
▶ accelerate
accelerate.cpp	Loop Acceleration
accelerate.h	Loop Acceleration
acceleration_utils.cpp	Loop Acceleration
acceleration_utils.h	Loop Acceleration
accelerator.h	Loop Acceleration
all_paths_enumerator.cpp	Loop Acceleration
all_paths_enumerator.h	Loop Acceleration
cone_of_influence.cpp	Loop Acceleration
cone_of_influence.h	Loop Acceleration
disjunctive_polynomial_acceleration.cpp	Loop Acceleration
disjunctive_polynomial_acceleration.h	Loop Acceleration
enumerating_loop_acceleration.cpp	Loop Acceleration
enumerating_loop_acceleration.h	Loop Acceleration
linearize.cpp	Loop Acceleration
linearize.h	Loop Acceleration
loop_acceleration.h	Loop Acceleration
overflow_instrumenter.cpp	Loop Acceleration
overflow_instrumenter.h	Loop Acceleration
path.cpp	Loop Acceleration
path.h	Loop Acceleration
path_acceleration.h	Loop Acceleration
path_enumerator.h	Loop Acceleration
polynomial.cpp	Loop Acceleration
polynomial.h	Loop Acceleration
polynomial_accelerator.cpp	Loop Acceleration
polynomial_accelerator.h	Loop Acceleration
sat_path_enumerator.cpp	Loop Acceleration
sat_path_enumerator.h	Loop Acceleration
scratch_program.cpp	Loop Acceleration
scratch_program.h	Loop Acceleration
subsumed.h	Loop Acceleration
trace_automaton.cpp	Loop Acceleration
trace_automaton.h	Loop Acceleration
util.cpp	Loop Acceleration
util.h	Loop Acceleration
▶ wmm
abstract_event.cpp	Abstract events
abstract_event.h	Abstract events
cycle_collection.cpp	Collection of cycles in graph of abstract events
data_dp.cpp	Data dependencies
data_dp.h	Data dependencies
event_graph.cpp	Graph of abstract events
event_graph.h	Graph of abstract events
fence.cpp	Fences for instrumentation
fence.h	Fences for instrumentation
goto2graph.cpp	Turns a goto-program into an abstract event graph
goto2graph.h	Instrumenter
instrumenter_pensieve.h	Instrumenter
instrumenter_strategies.cpp	Strategies for picking the abstract events to instrument
pair_collection.cpp	Collection of pairs (for Pensieve's static delay-set analysis) in graph of abstract events
shared_buffers.cpp
shared_buffers.h
weak_memory.cpp	Weak Memory Instrumentation for Threaded Goto Programs
weak_memory.h	Weak Memory Instrumentation for Threaded Goto Programs
wmm.h	Memory models
alignment_checks.cpp	Alignment Checks
alignment_checks.h	Alignment Checks
branch.cpp	Branch Instrumentation
branch.h	Branch Instrumentation
call_sequences.cpp	Printing function call sequences for Ofer
call_sequences.h	Memory-mapped I/O Instrumentation for Goto Programs
code_contracts.cpp	Verify and use annotated invariants and pre/post-conditions
code_contracts.h	Verify and use annotated invariants and pre/post-conditions
concurrency.cpp	Encoding for Threaded Goto Programs
concurrency.h	Encoding for Threaded Goto Programs
count_eloc.cpp	Count effective lines of code
count_eloc.h	Count effective lines of code
cover.cpp	Coverage Instrumentation
cover.h	Coverage Instrumentation
document_properties.cpp	Subgoal Documentation
document_properties.h	Documentation of Properties
dot.cpp	Dump Goto-Program as DOT Graph
dot.h	Dump Goto-Program as DOT Graph
dump_c.cpp	Dump Goto-Program as C/C++ Source
dump_c.h	Dump C from Goto Program
dump_c_class.h	Dump Goto-Program as C/C++ Source
full_slicer.cpp	Slicing
full_slicer.h	Slicing
full_slicer_class.h	Goto Program Slicing
function.cpp	Function Entering and Exiting
function.h	Function Entering and Exiting
function_modifies.cpp	Modifies
function_modifies.h	Modifies
goto_instrument_languages.cpp	Language Registration
goto_instrument_main.cpp	Main Module
goto_instrument_parse_options.cpp	Main Module
goto_instrument_parse_options.h	Command Line Parsing
goto_program2code.cpp	Dump Goto-Program as C/C++ Source
goto_program2code.h	Dump Goto-Program as C/C++ Source
havoc_loops.cpp	Havoc Loops
havoc_loops.h	Havoc Loops
horn_encoding.cpp	Horn-clause Encoding
horn_encoding.h	Horn-clause Encoding
interrupt.cpp	Interrupt Instrumentation
interrupt.h	Interrupt Instrumentation for Goto Programs
k_induction.cpp	K-induction
k_induction.h	K-induction
loop_utils.cpp	Helper functions for k-induction and loop invariants
loop_utils.h	Helper functions for k-induction and loop invariants
mmio.cpp	Memory-mapped I/O Instrumentation for Goto Programs
mmio.h	Memory-mapped I/O Instrumentation for Goto Programs
model_argc_argv.cpp	Initialize command line arguments
model_argc_argv.h	Initialize command line arguments
nondet_static.cpp	Nondeterministic initialization of certain global scope variables
nondet_static.h	Nondeterministic initialization of certain global scope variables
nondet_volatile.cpp	Volatile Variables
nondet_volatile.h	Volatile Variables
object_id.cpp	Object Identifiers
object_id.h	Object Identifiers
points_to.cpp	Field-sensitive, location-insensitive points-to analysis
points_to.h	Field-sensitive, location-insensitive points-to analysis
race_check.cpp	Race Detection for Threaded Goto Programs
race_check.h	Race Detection for Threaded Goto Programs
reachability_slicer.cpp	Slicer
reachability_slicer.h	Slicing
reachability_slicer_class.h	Goto Program Slicing
remove_function.cpp	Remove function definition
remove_function.h	Remove function definition
rw_set.cpp	Race Detection for Threaded Goto Programs
rw_set.h	Race Detection for Threaded Goto Programs
show_locations.cpp	Show program locations
show_locations.h	Show program locations
skip_loops.cpp	Skip over selected loops by adding gotos
skip_loops.h	Skip over selected loops by adding gotos
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
▶ goto-programs
basic_blocks.cpp	Group Basic Blocks in Goto Program
basic_blocks.h	Group Basic Blocks in Goto Program
builtin_functions.cpp	Program Transformation
cfg.h	Control Flow Graph
class_hierarchy.cpp	Class Hierarchy
class_hierarchy.h	Class Hierarchy
class_identifier.cpp	Extract class identifier
class_identifier.h	Extract class identifier
compute_called_functions.cpp	Query Called Functions
compute_called_functions.h	Query Called Functions
destructor.cpp	Destructor Calls
destructor.h	Destructor Calls
elf_reader.cpp	Read ELF
elf_reader.h	Read ELF
format_strings.cpp	Format String Parser
format_strings.h	Format String Parser
goto_asm.cpp	Assembler -> Goto
goto_clean_expr.cpp	Program Transformation
goto_convert.cpp	Program Transformation
goto_convert.h	Program Transformation
goto_convert_class.h	Program Transformation
goto_convert_exceptions.cpp	Program Transformation
goto_convert_function_call.cpp	Program Transformation
goto_convert_functions.cpp
goto_convert_functions.h	Goto Programs with Functions
goto_convert_new_switch_case.cpp	Program Transformation
goto_convert_side_effect.cpp	Program Transformation
goto_functions.cpp	Goto Programs with Functions
goto_functions.h	Goto Programs with Functions
goto_functions_template.h	Goto Programs with Functions
goto_inline.cpp	Function Inlining
goto_inline.h	Function Inlining
goto_inline_class.cpp	Function Inlining
goto_inline_class.h
goto_model.h	Symbol Table + CFG
goto_program.cpp	Program Transformation
goto_program.h	Concrete Goto Program
goto_program_irep.cpp	Goto_programt -> irep conversion
goto_program_irep.h	Goto_programt -> irep conversion
goto_program_template.cpp	Goto Program Template
goto_program_template.h	Goto Program Template
goto_trace.cpp	Traces of GOTO Programs
goto_trace.h	Traces of GOTO Programs
graphml_witness.cpp	Witnesses for Traces and Proofs
graphml_witness.h	Witnesses for Traces and Proofs
initialize_goto_model.cpp	Get a Goto Program
initialize_goto_model.h	Initialize a Goto Program
interpreter.cpp	Interpreter for GOTO Programs
interpreter.h	Interpreter for GOTO Programs
interpreter_class.h	Interpreter for GOTO Programs
interpreter_evaluate.cpp	Interpreter for GOTO Programs
json_goto_trace.cpp	Traces of GOTO Programs
json_goto_trace.h	Traces of GOTO Programs
link_to_library.cpp	Library Linking
link_to_library.h	Library Linking
loop_ids.cpp	Loop IDs
loop_ids.h	Loop IDs
mm_io.cpp	Perform Memory-mapped I/O instrumentation
mm_io.h	Perform Memory-mapped I/O instrumentation
osx_fat_reader.cpp	Read Mach-O
osx_fat_reader.h	Read OS X Fat Binaries
parameter_assignments.cpp	Add parameter assignments
parameter_assignments.h	Add parameter assignments
pointer_arithmetic.cpp
pointer_arithmetic.h
property_checker.cpp	Property Checker Interface
property_checker.h	Property Checker Interface
read_bin_goto_object.cpp	Read goto object files
read_bin_goto_object.h	Read goto object files
read_goto_binary.cpp	Read Goto Programs
read_goto_binary.h	Read Goto Programs
remove_asm.cpp	Remove 'asm' statements by compiling into suitable standard code
remove_asm.h	Remove 'asm' statements by compiling into suitable standard code
remove_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_exceptions.cpp	Remove exception handling
remove_exceptions.h	Remove function exceptional returns
remove_function_pointers.cpp	Program Transformation
remove_function_pointers.h	Remove Indirect Function Calls
remove_instanceof.cpp	Remove Instance-of Operators
remove_instanceof.h	Remove Instance-of Operators
remove_returns.cpp	Remove function return values
remove_returns.h	Remove function returns
remove_skip.cpp	Program Transformation
remove_skip.h	Program Transformation
remove_static_init_loops.cpp	Unwind loops in static initializers
remove_static_init_loops.h	Unwind loops in static initializers
remove_unreachable.cpp	Program Transformation
remove_unreachable.h	Program Transformation
remove_unused_functions.cpp	Unused function removal
remove_unused_functions.h	Unused function removal
remove_vector.cpp	Remove 'vector' data type
remove_vector.h	Remove the 'vector' data type by compilation into arrays
remove_virtual_functions.cpp	Remove Virtual Function (Method) Calls
remove_virtual_functions.h	Remove Virtual Function (Method) Calls
safety_checker.cpp	Safety Checker Interface
safety_checker.h	Safety Checker Interface
set_properties.cpp	Set Properties
set_properties.h	Set the properties to check
show_goto_functions.cpp	Show goto functions
show_goto_functions.h	Show the goto functions
show_goto_functions_json.cpp	Goto Program
show_goto_functions_json.h	Goto Program
show_goto_functions_xml.cpp	Goto Program
show_goto_functions_xml.h	Goto Program
show_properties.cpp	Show Claims
show_properties.h	Show the properties
show_symbol_table.cpp	Show the symbol table
show_symbol_table.h	Show the symbol table
slice_global_inits.cpp	Remove initializations of unused global variables
slice_global_inits.h	Remove initializations of unused global variables
string_abstraction.cpp	String Abstraction
string_abstraction.h	String Abstraction
string_instrumentation.cpp	String Abstraction
string_instrumentation.h	String Abstraction
vcd_goto_trace.cpp	Traces of GOTO Programs in VCD (Value Change Dump) Format
vcd_goto_trace.h	Traces of GOTO Programs in VCD (Value Change Dump) Format
wp.cpp	Weakest Preconditions
wp.h	Weakest Preconditions
write_goto_binary.cpp	Write GOTO binaries
write_goto_binary.h	Write GOTO binaries
xml_goto_trace.cpp	Traces of GOTO Programs
xml_goto_trace.h	Traces of GOTO Programs
▶ goto-symex
adjust_float_expressions.cpp	Symbolic Execution
adjust_float_expressions.h	Symbolic Execution
auto_objects.cpp	Symbolic Execution of ANSI-C
build_goto_trace.cpp	Traces of GOTO Programs
build_goto_trace.h	Traces of GOTO Programs
goto_symex.cpp	Symbolic Execution
goto_symex.h	Symbolic Execution
goto_symex_state.cpp	Symbolic Execution
goto_symex_state.h	Symbolic Execution
memory_model.cpp	Memory model for partial order concurrency
memory_model.h	Memory models for partial order concurrency
memory_model_pso.cpp	Memory model for partial order concurrency
memory_model_pso.h	Memory models for partial order concurrency
memory_model_sc.cpp	Memory model for partial order concurrency
memory_model_sc.h	Memory models for partial order concurrency
memory_model_tso.cpp	Memory model for partial order concurrency
memory_model_tso.h	Memory models for partial order concurrency
partial_order_concurrency.cpp	Add constraints to equation encoding partial orders on events
partial_order_concurrency.h	Add constraints to equation encoding partial orders on events
postcondition.cpp	Symbolic Execution
postcondition.h	Generate Equation using Symbolic Execution
precondition.cpp	Symbolic Execution
precondition.h	Generate Equation using Symbolic Execution
rewrite_union.cpp	Symbolic Execution of ANSI-C
rewrite_union.h	Symbolic Execution
slice.cpp	Slicer for symex traces
slice.h	Slicer for symex traces
slice_by_trace.cpp	Slicer for symex traces
slice_by_trace.h	Slicer for matching with trace files
symex_assign.cpp	Symbolic Execution
symex_atomic_section.cpp	Symbolic Execution
symex_builtin_functions.cpp	Symbolic Execution of ANSI-C
symex_catch.cpp	Symbolic Execution
symex_clean_expr.cpp	Symbolic Execution of ANSI-C
symex_dead.cpp	Symbolic Execution
symex_decl.cpp	Symbolic Execution
symex_dereference.cpp	Symbolic Execution of ANSI-C
symex_dereference_state.cpp	Symbolic Execution of ANSI-C
symex_dereference_state.h	Symbolic Execution of ANSI-C
symex_function_call.cpp	Symbolic Execution of ANSI-C
symex_goto.cpp	Symbolic Execution
symex_main.cpp	Symbolic Execution
symex_other.cpp	Symbolic Execution
symex_slice_class.h	Slicer for symex traces
symex_start_thread.cpp	Symbolic Execution
symex_target.cpp	Symbolic Execution
symex_target.h	Generate Equation using Symbolic Execution
symex_target_equation.cpp	Symbolic Execution
symex_target_equation.h	Generate Equation using Symbolic Execution
symex_throw.cpp	Symbolic Execution
▶ java_bytecode
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	Context-insensitive lazy methods container
ci_lazy_methods.h	Context-insensitive lazy methods container
expr2java.cpp
expr2java.h
jar_file.cpp
jar_file.h	JAR File Reading
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_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_bytecode_vtable.cpp
java_bytecode_vtable.h
java_class_loader.cpp
java_class_loader.h
java_class_loader_limit.cpp	Limit class path loading
java_class_loader_limit.h	Limit class path loading
java_entry_point.cpp
java_entry_point.h
java_local_variable_table.cpp	Java local variable table processing
java_object_factory.cpp
java_object_factory.h
java_pointer_casts.cpp	JAVA Pointer Casts
java_pointer_casts.h	JAVA Pointer Casts
java_root_class.cpp
java_root_class.h
java_types.cpp
java_types.h
java_utils.cpp
java_utils.h
▶ jsil
expr2jsil.cpp	Jsil Language
expr2jsil.h	Jsil Language
jsil_convert.cpp	Jsil Language Conversion
jsil_convert.h	Jsil Language Conversion
jsil_entry_point.cpp	Jsil Language
jsil_entry_point.h	Jsil Language
jsil_internal_additions.cpp	Jsil Language
jsil_internal_additions.h	Jsil Language
jsil_language.cpp	Jsil Language
jsil_language.h	Jsil Language
jsil_lex.yy.cpp
jsil_parse_tree.cpp	Jsil Language
jsil_parse_tree.h	Jsil Language
jsil_parser.cpp	Jsil Language
jsil_parser.h	Jsil Language
jsil_typecheck.cpp	Jsil Language
jsil_typecheck.h	Jsil Language
jsil_types.cpp	Jsil Language
jsil_types.h	Jsil Language
jsil_y.tab.cpp
jsil_y.tab.h
▶ json
json_lex.yy.cpp
json_parser.cpp
json_parser.h
json_y.tab.cpp
json_y.tab.h
▶ langapi
language_ui.cpp
language_ui.h
language_util.cpp
language_util.h
languages.cpp
languages.h
mode.cpp
mode.h
▶ linking
linking.cpp	ANSI-C Linking
linking.h	ANSI-C Linking
linking_class.h	ANSI-C Linking
remove_internal_symbols.cpp	Remove symbols that are internal only
remove_internal_symbols.h	Remove symbols that are internal only
static_lifetime_init.cpp
static_lifetime_init.h
zero_initializer.cpp	Linking: Zero Initialization
zero_initializer.h	Linking: Zero Initialization
▶ memory-models
mm2cpp.cpp
mm2cpp.h
mm_parser.cpp
mm_parser.h
mmcc_main.cpp	Mmcc Main Module
mmcc_parse_options.cpp	Mmcc Command Line Option Processing
mmcc_parse_options.h	Mmcc Command Line Option Processing
▶ miniz
miniz.cpp
miniz.h
▶ musketeer
cycles_visitor.cpp	Cycles visitor for computing edges involved for fencing
cycles_visitor.h	Cycles visitor for computing edges involved for fencing
fence_assert.cpp	ILP construction for cycles affecting user-assertions and resolution
fence_assert.h	ILP construction for cycles affecting user-assertions and resolution
fence_inserter.cpp	ILP construction for all cycles and resolution
fence_inserter.h	ILP construction for all cycles and resolution
fence_shared.cpp
fence_shared.h	(naive) Fence insertion
fence_user_def.cpp	ILP construction for cycles affecting user-assertions and resolution
fence_user_def.h	ILP construction for cycles containing user-placed fences and resolution
fencer.cpp	Fence inference: Main
fencer.h	Fence inference
graph_visitor.cpp	Graph visitor for computing edges involved for fencing
graph_visitor.h	Graph visitor for computing edges involved for fencing
ilp.h	ILP structure
infer_mode.h
languages.cpp	Language Registration
musketeer_main.cpp	Main Module
musketeer_parse_options.cpp	Main Module
musketeer_parse_options.h	Command Line Parsing
pensieve.cpp
pensieve.h	Fence insertion following criteria of Pensieve (PPoPP'05)
propagate_const_function_pointers.cpp	Constant Function Pointer Propagation
propagate_const_function_pointers.h	Constant Function Pointer Propagation
replace_async.h
version.h
▶ path-symex
build_goto_trace.cpp	Build Goto Trace from State History
build_goto_trace.h	Build Goto Trace from Path Symex History
loc_ref.h	Program Locations
locs.cpp	Program Locations
locs.h	CFG made of Program Locations, built from goto_functionst
path_replay.cpp	Dense Data Structure for Path Replay
path_replay.h	Dense Data Structure for Path Replay
path_symex.cpp	Concrete Symbolic Transformer
path_symex.h	Concrete Symbolic Transformer
path_symex_class.h	Concrete Symbolic Transformer
path_symex_history.cpp	History of path-based symbolic simulator
path_symex_history.h	History for path-based symbolic simulator
path_symex_state.cpp	State of path-based symbolic simulator
path_symex_state.h	State of path-based symbolic simulator
path_symex_state_read.cpp	State of path-based symbolic simulator
var_map.cpp	Variable Numbering
var_map.h	Variable Numbering
▶ pointer-analysis
add_failed_symbols.cpp	Pointer Dereferencing
add_failed_symbols.h	Pointer Dereferencing
dereference.cpp	Symbolic Execution of ANSI-C
dereference.h	Pointer Dereferencing
dereference_callback.cpp	Pointer Dereferencing
dereference_callback.h	Pointer Dereferencing
goto_program_dereference.cpp	Dereferencing Operations on GOTO Programs
goto_program_dereference.h	Value Set
object_numbering.h	Value Set
pointer_offset_sum.cpp	Pointer Analysis
pointer_offset_sum.h	Pointer Dereferencing
rewrite_index.cpp	Pointer Dereferencing
rewrite_index.h	Pointer Dereferencing
show_value_sets.cpp	Show Value Sets
show_value_sets.h	Show Value Sets
value_set.cpp	Value Set
value_set.h	Value Set
value_set_analysis.cpp	Value Set Propagation
value_set_analysis.h	Value Set Propagation
value_set_analysis_fi.cpp	Value Set Propagation (Flow Insensitive)
value_set_analysis_fi.h	Value Set Propagation (flow insensitive)
value_set_analysis_fivr.cpp	Value Set Propagation (Flow Insensitive)
value_set_analysis_fivr.h	Value Set Propagation
value_set_analysis_fivrns.cpp	Value Set Propagation (Flow Insensitive, Validity Regions)
value_set_analysis_fivrns.h	Value Set Analysis (Flow Insensitive, Validity Regions)
value_set_dereference.cpp	Symbolic Execution of ANSI-C
value_set_dereference.h	Pointer Dereferencing
value_set_domain.cpp	Value Set
value_set_domain.h	Value Set
value_set_domain_fi.cpp	Value Set Domain (Flow Insensitive)
value_set_domain_fi.h	Value Set (Flow Insensitive)
value_set_domain_fivr.cpp	Value Set Domain (Flow Insensitive, Sharing, Validity Regions)
value_set_domain_fivr.h	Value Set (Flow Insensitive, Sharing, Validity Regions)
value_set_domain_fivrns.cpp	Value Set Domain (Flow Insensitive, Validity Regions)
value_set_domain_fivrns.h	Value Set Domain (Flow Insensitive, Validity Regions)
value_set_fi.cpp	Value Set (Flow Insensitive, Sharing)
value_set_fi.h	Value Set (Flow Insensitive, Sharing)
value_set_fivr.cpp	Value Set (Flow Insensitive, Sharing, Validity Regions)
value_set_fivr.h	Value Set (Flow Insensitive, Sharing, Validity Regions)
value_set_fivrns.cpp	Value Set (Flow Insensitive, Validity Regions)
value_set_fivrns.h	Value Set (Flow Insensitive, Validity Regions)
value_sets.h	Value Set Propagation
▶ solvers
▶ cvc
cvc_conv.cpp
cvc_conv.h
cvc_dec.cpp
cvc_dec.h
cvc_prop.cpp
cvc_prop.h
▶ dplib
dplib_conv.cpp
dplib_conv.h
dplib_dec.cpp
dplib_dec.h
dplib_prop.cpp
dplib_prop.h
▶ flattening
arrays.cpp
arrays.h	Theory of Arrays with Extensionality
boolbv.cpp
boolbv.h
boolbv_abs.cpp
boolbv_add_sub.cpp
boolbv_array.cpp
boolbv_array_of.cpp
boolbv_bitwise.cpp
boolbv_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_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_minimize.cpp
bv_minimize.h	SAT-optimizer for minimizing expressions
bv_pointers.cpp
bv_pointers.h
bv_utils.cpp
bv_utils.h
c_bit_field_replacement_type.cpp
c_bit_field_replacement_type.h
equality.cpp
equality.h
flatten_byte_operators.cpp
flatten_byte_operators.h
functions.cpp
functions.h	Uninterpreted Functions
pointer_logic.cpp	Pointer Logic
pointer_logic.h	Pointer Logic
▶ floatbv
float_approximation.cpp
float_approximation.h	Floating Point with under/over-approximation
float_bv.cpp
float_bv.h
float_utils.cpp
float_utils.h
▶ miniBDD
example.cpp	A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes
miniBDD.cpp	A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes
miniBDD.h	A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes
▶ prop
aig.cpp
aig.h	AND-Inverter Graph
aig_prop.cpp
aig_prop.h
bdd_expr.cpp	Conversion between exprt and miniBDD
bdd_expr.h	Conversion between exprt and miniBDD
cover_goals.cpp	Cover a set of goals incrementally
cover_goals.h	Cover a set of goals incrementally
literal.cpp	Literals
literal.h
literal_expr.h
minimize.cpp	Minimize some target function incrementally
minimize.h	SAT Minimizer
prop.cpp
prop.h
prop_assignment.cpp
prop_assignment.h
prop_conv.cpp
prop_conv.h
prop_conv_store.cpp
prop_conv_store.h
prop_wrapper.h
▶ qbf
qbf_bdd_core.cpp
qbf_bdd_core.h
qbf_core.h
qbf_quantor.cpp
qbf_quantor.h
qbf_qube.cpp
qbf_qube.h
qbf_qube_core.cpp
qbf_qube_core.h
qbf_skizzo.cpp
qbf_skizzo.h
qbf_skizzo_core.cpp
qbf_skizzo_core.h
qbf_squolem.cpp	Squolem Backend
qbf_squolem.h	Squolem Backend
qbf_squolem_core.cpp	Squolem Backend (with proofs)
qbf_squolem_core.h	Squolem Backend (with Proofs)
qdimacs_cnf.cpp
qdimacs_cnf.h
qdimacs_core.cpp
qdimacs_core.h
▶ refinement
bv_refinement.h	Abstraction Refinement Loop
bv_refinement_loop.cpp
refine_arithmetic.cpp
refine_arrays.cpp
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
string_constraint.h	Defines string constraints
string_constraint_generator.h	Generates string constraints to link results from string functions with their arguments
string_constraint_generator_code_points.cpp	Generates string constraints for Java functions dealing with code points
string_constraint_generator_comparison.cpp	Generates string constraints for function comparing strings, such as: equals, equalsIgnoreCase, compareTo, hashCode, intern
string_constraint_generator_concat.cpp	Generates string constraints for functions adding content add the end of strings
string_constraint_generator_constants.cpp	Generates string constraints for constant strings
string_constraint_generator_indexof.cpp	Generates string constraints for the family of indexOf and lastIndexOf java functions
string_constraint_generator_insert.cpp	Generates string constraints for the family of insert Java functions
string_constraint_generator_main.cpp	Generates string constraints to link results from string functions with their arguments
string_constraint_generator_testing.cpp	Generates string constraints for string functions that return Boolean values
string_constraint_generator_transformation.cpp	Generates string constraints for string transformations, that is, functions taking one string and returning another
string_constraint_generator_valueof.cpp	Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool
string_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
▶ sat
cnf.cpp	CNF Generation, via Tseitin
cnf.h	CNF Generation, via Tseitin
cnf_clause_list.cpp	CNF Generation
cnf_clause_list.h	CNF Generation
dimacs_cnf.cpp
dimacs_cnf.h
pbs_dimacs_cnf.cpp
pbs_dimacs_cnf.h
read_dimacs_cnf.cpp	Reading DIMACS CNF
read_dimacs_cnf.h	Reading DIMACS CNF
resolution_proof.cpp
resolution_proof.h
satcheck.cpp
satcheck.h
satcheck_booleforce.cpp
satcheck_booleforce.h
satcheck_core.h
satcheck_glucose.cpp
satcheck_glucose.h
satcheck_limmat.cpp
satcheck_limmat.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_precosat.cpp
satcheck_precosat.h
satcheck_smvsat.cpp
satcheck_smvsat.h
satcheck_zchaff.cpp
satcheck_zchaff.h
satcheck_zcore.cpp
satcheck_zcore.h
▶ smt1
smt1_conv.cpp	SMT Version 1 Backend
smt1_conv.h	SMT Version 1 Backend
smt1_dec.cpp
smt1_dec.h
smt1_prop.cpp
smt1_prop.h
▶ smt2
smt2_conv.cpp	SMT Backend
smt2_conv.h
smt2_dec.cpp
smt2_dec.h
smt2_parser.cpp
smt2_parser.h
smt2_prop.cpp
smt2_prop.h
smt2irep.cpp
smt2irep.h
▶ symex
path_search.cpp	Path-based Symbolic Execution
path_search.h	Path-based Symbolic Execution
symex_cover.cpp	Symex Test Suite Generation
symex_main.cpp	Symex Main Module
symex_parse_options.cpp	Symex Command Line Options Processing
symex_parse_options.h	Command Line Parsing
▶ util
arith_tools.cpp
arith_tools.h
array_name.cpp	Misc Utilities
array_name.h	Misc Utilities
base_exceptions.h	Generic exception types primarily designed for use with invariants
base_type.cpp	Base Type Computation
base_type.h	Base Type Computation
bv_arithmetic.cpp
bv_arithmetic.h
byte_operators.cpp
byte_operators.h	Expression classes for byte-level operators
c_types.cpp
c_types.h
cmdline.cpp
cmdline.h
config.cpp
config.h
cout_message.cpp
cout_message.h
cprover_prefix.h
decision_procedure.cpp	Decision Procedure Interface
decision_procedure.h	Decision Procedure Interface
dstring.cpp	Container for C-Strings
dstring.h	Container for C-Strings
endianness_map.cpp
endianness_map.h
error.h
expanding_vector.h
expr.cpp	Expression Representation
expr.h
expr_util.cpp
expr_util.h	Deprecated expression utility functions
file_util.cpp	File Utilities
file_util.h
find_macros.cpp
find_macros.h
find_symbols.cpp
find_symbols.h
fixedbv.cpp
fixedbv.h
format_constant.cpp
format_constant.h
format_spec.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.cpp	A Template Class for Graphs
graph.h	A Template Class for Graphs
guard.cpp	Symbolic Execution
guard.h	Guard Data Structure
identifier.cpp
identifier.h
ieee_float.cpp
ieee_float.h
infix.h	String infix shorthand
invariant.cpp
invariant.h
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
json.cpp
json.h
json_expr.cpp	Expressions in JSON
json_expr.h	Expressions in JSON
json_irep.cpp	Util
json_irep.h	Util
language.cpp	Abstract interface to support a programming language
language.h	Abstract interface to support a programming language
language_file.cpp
language_file.h
lispexpr.cpp
lispexpr.h
lispirep.cpp
lispirep.h
memory_info.cpp
memory_info.h
merge_irep.cpp
merge_irep.h
message.cpp
message.h
mp_arith.cpp
mp_arith.h
namespace.cpp	Namespace
namespace.h
numbering.h
options.cpp	Options
options.h	Options
parse_options.cpp
parse_options.h
parser.cpp
parser.h	Parser utilities
pipe_stream.cpp	A stdin/stdout pipe as STL stream
pipe_stream.h	A stdin/stdout pipe as STL stream
pointer_offset_size.cpp	Pointer Logic
pointer_offset_size.h	Pointer Logic
pointer_predicates.cpp	Various predicates over pointers in programs
pointer_predicates.h	Various predicates over pointers in programs
prefix.h
preprocessor.h	Preprocessing Base Class
rational.cpp	Rational Numbers
rational.h
rational_tools.cpp	Rational Numbers
rational_tools.h
ref_expr_set.cpp	Value Set
ref_expr_set.h	Value Set
reference_counting.h	Reference Counting
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
safe_pointer.h	Simple checked pointers
sharing_map.h	Sharing map
sharing_node.h	Sharing node
signal_catcher.cpp
signal_catcher.h
simplify_expr.cpp
simplify_expr.h
simplify_expr_array.cpp
simplify_expr_boolean.cpp
simplify_expr_class.h
simplify_expr_floatbv.cpp
simplify_expr_int.cpp
simplify_expr_pointer.cpp
simplify_expr_struct.cpp
simplify_utils.cpp
simplify_utils.h
sorted_vector.h
source_location.cpp
source_location.h
ssa_expr.cpp
ssa_expr.h
std_code.cpp
std_code.h
std_expr.cpp
std_expr.h	API to expression classes
std_types.cpp
std_types.h	API to type classes
string2int.cpp
string2int.h
string_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
substitute.cpp
substitute.h
suffix.h
symbol.cpp
symbol.h	Symbol table entry
symbol_table.cpp
symbol_table.h	Symbol table
tempdir.cpp
tempdir.h
tempfile.cpp
tempfile.h
threeval.cpp
threeval.h
time_stopping.cpp	Time Stopping
time_stopping.h	Time Stopping
timer.cpp	Time Stopping
timer.h	Time Stopping
type.cpp
type.h
type_eq.cpp	Type Checking
type_eq.h
typecheck.cpp
typecheck.h
ui_message.cpp
ui_message.h
unicode.cpp
unicode.h
union_find.cpp
union_find.h
xml.cpp
xml.h
xml_expr.cpp	Expressions in XML
xml_expr.h
xml_irep.cpp
xml_irep.h
▶ xmllang
graphml.cpp	Read/write graphs as GraphML
graphml.h	Read/write graphs as GraphML
xml_lex.yy.cpp
xml_parse_tree.cpp
xml_parse_tree.h
xml_parser.cpp
xml_parser.h
xml_y.tab.cpp
xml_y.tab.h