File List

Here is a list of all files with brief descriptions:

[detail level 12345678]

src
big-int
allocainc.h
bigint.cpp
bigint.hh
c2goto
headers
__esbmc
stddefs.h
arpa
inet.h
bits
pthreadtypes.h
thread-shared-types.h
netinet
in.h
sys
_pthread
_pthread_attr_t.h
_pthread_cond_t.h
_pthread_condattr_t.h
_pthread_key_t.h
_pthread_mutex_t.h
_pthread_mutexattr_t.h
_pthread_once_t.h
_pthread_rwlock_t.h
_pthread_rwlockattr_t.h
_pthread_t.h
_pthread_types.h
_types
_pthread_attr_t.h
_pthreadtypes.h
select.h
socket.h
time.h
ubuntu20.04
kernel_5.15.0-76
include
asm
uaccess.h
linux
gfp.h
slab.h
spinlock.h
corecrt_math.h
ctype.h
fenv.h
limits.h
pthread.h
sched.h
semaphore.h
stdarg.h
stdbool.h
stddef.h
stdio.h
stdlib.h
string.h
threads.h
time.h
wchar.h
library
cpp
exception.cpp
probe.cpp
libm
musl
__cosdf.c
__math_divzero.c
__math_divzerof.c
__math_invalid.c
__math_invalidf.c
__math_invalidl.c
__math_oflow.c
__math_oflowf.c
__math_uflow.c
__math_uflowf.c
__math_xflow.c
__math_xflowf.c
__rem_pio2_large.c
__rem_pio2f.c
__sindf.c
acosf.c
alltypes.h
asinf.c
atanhf.c
cbrt.c
cbrtf.c
cosf.c
endian.h
erff.c
exp2f.c
exp2f_data.c
exp2f_data.h
expf.c
expm1f.c
libm.h
log10.c
log1pf.c
logf.c
logf_data.c
logf_data.h
sinf.c
tanhf.c
acos.c
acosh.c
asin.c
asinh.c
atan.c
atanh.c
cbrtl.c
ceil.c
copysign.c
cos.c
cosh.c
exp.c
exp2.c
fabs.c
fdim.c
floor.c
fmax.c
fmin.c
fmod.c
fpclassify.c
frexp.c
hypot.c
logb.c
modf.c
nan.c
nextafter.c
pow.c
remainder.c
remquo.c
rint.c
round.c
sin.c
sinh.c
sqrt.c
tan.c
tanh.c
trunc.c
python
linalg.c
list.c
math.c
python_types.h
scalar.c
slice.c
string.c
umath.c
solidity
solidity_abi.c
solidity_address.c
solidity_array.c
solidity_blockchain.c
solidity_builtins.c
solidity_bytes.c
solidity_crypto.c
solidity_mapping.c
solidity_misc.c
solidity_string.c
solidity_types.h
solidity_units.c
builtin_libs.c
complex.c
ctype.c
fenv.c
getopt.c
inet.c
io.c
kernel.c
libintl.c
locale.c
ltl.c
pthread_lib.c
semaphore_lib.c
setjmp.c
socket_lib.c
stdlib.c
string.c
strings.c
syserr.c
threads_lib.c
time.c
verifier.c
wchar.c
c2goto.cpp
cprover_blank_library.cpp
cprover_libc_sources.cpp
cprover_library.cpp
cprover_library.h
clang-c-frontend
AST
build_ast.cpp
build_ast.h
vfs_adapter.cpp
vfs_adapter.h
vfs_paths.h
headers
transform.py
builtin_names.cpp
builtin_names.h
c_preprocess.cpp
c_preprocess.h
clang_ast_dump.cpp
clang_ast_dump.h
clang_c_adjust.h
clang_c_adjust_code.cpp
clang_c_adjust_expr.cpp
clang_c_adjust_guards.h
clang_c_adjust_irep2.cpp
clang_c_adjust_irep2.h
clang_c_adjust_polymorphic_functions.cpp
clang_c_base_layout.cpp
clang_c_base_layout.h
clang_c_convert.cpp
clang_c_convert.h
clang_c_convert_literals.cpp
clang_c_language.cpp
clang_c_language.h
clang_c_lexer.cpp
clang_c_lexer.h
clang_c_main.cpp
clang_c_main.h
clang_headers.cpp
nested_func_transform.cpp
nested_func_transform.h
padding.cpp	Struct/union padding and alignment computation
padding.h	ANSI-C Language Type Checking
typecast.cpp
typecast.h
clang-cpp-frontend
abstract_includes
cpp_includes.h
clang_cpp_adjust.h
clang_cpp_adjust_code.cpp
clang_cpp_adjust_code_gen.cpp
clang_cpp_adjust_expr.cpp
clang_cpp_adjust_irep2.cpp
clang_cpp_adjust_irep2.h
clang_cpp_code_gen.h
clang_cpp_convert.cpp
clang_cpp_convert.h
clang_cpp_convert_bind.cpp
clang_cpp_convert_vft.cpp
clang_cpp_destructor_call.cpp
clang_cpp_destructor_call.h
clang_cpp_exception_id.cpp
clang_cpp_exception_id.h
clang_cpp_language.cpp
clang_cpp_language.h
clang_cpp_main.cpp
clang_cpp_main.h
esbmc_internal_cpp.cpp
esbmc_internal_cpp.h
cpp
library
boost
config
compiler
gcc.hpp
no_tr1
utility.hpp
platform
linux.hpp
posix_features.hpp
select_compiler_config.hpp
select_platform_config.hpp
select_stdlib_config.hpp
suffix.hpp
user.hpp
date_time
posix_time
posix_time.hpp
compiler_config.hpp
locale_config.hpp
detail
workaround.hpp
asio.hpp
bind.hpp
config.hpp
cstdint.hpp
filesystem.hpp
CUDA
builtin_types.h
call_kernel.h
cublas.h
cuda.h
cuda_device_runtime_api.h
cuda_error.h
cuda_runtime_api.h
cudnn.h
curand.h
curand_kernel.h
curand_precalc.h
device_launch_parameters.h
driver_types.h
host_defines.h
math_functions.h
sm_atomic_functions.h
vector_types.h
Qt
QtCore
qstate.h
systemc
communication
sc_clock.h
sc_signal.h
sc_signal_ports.h
kernel
sc_module.h
sc_sensitive.h
sc_wait.h
char_traits.h
definitions.h
iterator_tags.h
libstl.cpp
math.h
min_max.h
OM_compiler_defs.h
systemc.h
uchar.h
esbmc
parseoptions
bmc_strategy.cpp
command_line_options.cpp
driver.cpp
function_contracts.cpp
goto_program.cpp
k_induction.cpp
process_goto_program.cpp
property_monitors.cpp
ts_strategy.cpp
bmc.cpp
bmc.h
esbmc_parseoptions.h
globals.cpp
globals.h
main.cpp
non_termination.cpp
non_termination.h
options.cpp
property_report.cpp
property_report.h
ranking_synthesis.cpp
ranking_synthesis.h
show_vcc.cpp
goto-programs
abstract-interpretation
ai.cpp	Abstract Interpretation
ai.h	Abstract Interpretation
ai_domain.cpp	Abstract Interpretation Domain
ai_domain.h	Abstract Interpretation Domain
bitwise_bounds.h
gcse.cpp
gcse.h
interval_analysis.cpp	Interval Analysis
interval_analysis.h	Interval Analysis
interval_domain.cpp	Interval Domain
interval_domain.h	Interval Domain
interval_template.h
wrapped_interval.h
contracts
contracts.cpp
contracts.h
add_race_assertions.cpp
add_race_assertions.h
add_restrict_assertions.cpp
add_restrict_assertions.h
assign_params_as_non_det.cpp
assign_params_as_non_det.h
builtin_functions.cpp
cbmc_adapter.cpp
cbmc_adapter.h
dead_store_advisory.h
dead_store_analysis.cpp
dead_store_analysis.h
destructor.cpp
destructor.h
exception_globals.cpp
exception_globals.h
exception_typeid.cpp
exception_typeid.h
format_strings.cpp
format_strings.h
frame_enforcer.cpp	Implementation of the observational frame rule
frame_enforcer.h	Observational frame-rule enforcement for verification
goto_atomicity_check.cpp
goto_atomicity_check.h
goto_binary_reader.cpp
goto_binary_reader.h
goto_cfg.cpp
goto_cfg.h
goto_check.cpp
goto_check.h
goto_check_excessive_alloc.cpp
goto_check_excessive_alloc.h
goto_check_unchecked_return.cpp
goto_check_unchecked_return.h
goto_check_uninit_vars.cpp
goto_check_uninit_vars.h
goto_contractor.cpp
goto_contractor.h
goto_convert.cpp
goto_convert_class.h
goto_convert_functions.cpp
goto_convert_functions.h
goto_coverage.cpp
goto_coverage.h
goto_coverage_rm.cpp
goto_function.cpp
goto_function_serialization.cpp
goto_function_serialization.h
goto_functions.h
goto_functions_algorithm.cpp
goto_functions_algorithm.h
goto_inline.cpp
goto_inline.h
goto_invariant_synthesis.cpp
goto_invariant_synthesis.h
goto_k_induction.cpp
goto_k_induction.h
goto_loop_invariant.cpp
goto_loop_invariant.h
goto_loop_simplify.cpp
goto_loop_simplify.h
goto_loops.cpp
goto_loops.h
goto_main.cpp
goto_program.cpp
goto_program.h
goto_program_irep.cpp
goto_program_irep.h
goto_program_serialization.cpp
goto_program_serialization.h
goto_sideeffects.cpp
goto_termination.cpp
goto_termination.h
k_path_spanning.cpp
k_path_spanning.h
lift_call_expressions.cpp
lift_call_expressions.h
loop_numbers.cpp
loop_numbers.h
loop_unroll.cpp
loop_unroll.h
loopst.cpp
loopst.h
lower_longjmp.cpp
lower_longjmp.h
mark_decl_as_non_det.cpp
mark_decl_as_non_det.h
property_verdict.cpp
property_verdict.h
read_bin_goto_object.cpp
read_bin_goto_object.h
read_cbmc_goto_object.cpp
read_cbmc_goto_object.h
remove_exceptions.cpp
remove_exceptions.h
remove_library_assertions.cpp
remove_library_assertions.h
remove_no_op.cpp
remove_no_op.h
remove_unreachable.cpp
remove_unreachable.h
rw_set.cpp
rw_set.h
set_claims.cpp
set_claims.h
show_claims.cpp
show_claims.h
static_analysis.cpp
static_analysis.h
write_goto_binary.cpp
write_goto_binary.h
goto-symex
engine
builtin_functions
bounded_math.cpp
cpp_memory.cpp
io.cpp
memory_alloc.cpp
memory_ops.cpp
misc.cpp
object_size.cpp
python_builtins.cpp
run_builtin.cpp
threads.cpp
va_arg.cpp
witness.cpp
dynamic_allocation.cpp
dynamic_allocation.h
goto_symex.h
symex_assign.cpp
symex_dereference.cpp
symex_function.cpp
symex_goto.cpp
symex_main.cpp
symex_other.cpp
symex_stack.cpp
symex_valid_object.cpp
equation
features.cpp
features.h
slice.cpp
slice.h
ssa_step_algorithm.cpp
ssa_step_algorithm.h
symex_symmetry.cpp
symex_symmetry.h
symex_target.cpp
symex_target.h
symex_target_equation.cpp
symex_target_equation.h
scheduler
execution_state.cpp
execution_state.h
reachability_tree.cpp
reachability_tree.h
reachability_tree_cin.cpp
state
goto_symex_state.cpp
goto_symex_state.h
renaming.cpp
renaming.h
testgen
ctest.cpp
ctest.h
pytest.cpp
pytest.h
test_gen_guard.h
trace
build_goto_trace.cpp
build_goto_trace.h
goto_trace.cpp
goto_trace.h
html.cpp
json.cpp
printf_formatter.cpp
printf_formatter.h
sarif.cpp
sarif.h
xml_goto_trace.cpp
xml_goto_trace.h
witness
witnesses.cpp
witnesses.h
symex_invariant.cpp
symex_invariant.h
waypoint.h
goto2c
expr2c.cpp
expr2c.h
goto2c.h
goto2c_check.cpp
goto2c_preprocess.cpp
goto2c_translate.cpp
irep2
expr_kinds.inc
guard_seq.h
irep2.h	Classes and definitions for non-stringy internal representation
irep2_content_hash.cpp
irep2_content_hash.h
irep2_crc.cpp
irep2_dispatch.h
irep2_expr.cpp
irep2_expr.h
irep2_guard.cpp
irep2_guard.h
irep2_type.cpp
irep2_type.h
irep2_utils.cpp
irep2_utils.h
simplification_check.cpp
simplification_check.h
type_kinds.inc
jimple-frontend
AST
jimple_ast.h
jimple_class_field.cpp
jimple_class_member.h
jimple_declaration.cpp
jimple_declaration.h
jimple_expr.cpp
jimple_expr.h
jimple_file.cpp
jimple_file.h
jimple_method.cpp
jimple_method_body.cpp
jimple_method_body.h
jimple_modifiers.cpp
jimple_modifiers.h
jimple_statement.cpp
jimple_statement.h
jimple_type.cpp
jimple_type.h
jimple-converter.cpp
jimple-converter.h
jimple-language.cpp
jimple-language.h
jimple-parser.cpp
jimple-typecheck.cpp
langapi
language_ui.cpp
language_ui.h
language_util.cpp
language_util.h
languages.h
mode.cpp
mode.h
ld-frontend
ir
ld_ir.cpp
ld_ir.h
ld_ir_builder.cpp
ld_ir_builder.h
ir_gen
ld_converter.cpp
ld_converter.h
st_fb_translator.cpp
st_fb_translator.h
parser
ld_ast.cpp
ld_ast.h
plcopen_xml_parser.cpp
plcopen_xml_parser.h
property
property_encoder.cpp
property_encoder.h
yaml_property_parser.cpp
yaml_property_parser.h
semantics
sos_semantics.cpp
sos_semantics.h
type_checker.cpp
type_checker.h
verify
ld_verify.cpp
ld_verify.h
ld_language.cpp
ld_language.h
lib
toml.hpp
llm
cli_llm_client.cpp
cli_llm_client.h
llm_client.cpp
llm_client.h
pointer-analysis
andersen.cpp
andersen.h	Andersen-style (inclusion-based) points-to analysis
dereference.cpp
dereference.h	The dereferencing code's purpose is to take a symbol with pointer type that is being dereferenced, and translate it to an expression representing the values it read or wrote to/from
goto_program_dereference.cpp
goto_program_dereference.h
show_value_sets.cpp
show_value_sets.h
value_set.cpp
value_set.h
value_set_analysis.cpp
value_set_analysis.h
value_set_domain.cpp
value_set_domain.h
value_sets.h
python-frontend
class
python_class.cpp
python_class.h
python_class_builder.cpp
python_class_builder.h
consteval
python_consteval.cpp
python_consteval.h
converter
converter_binop.cpp
converter_class.cpp
converter_compare.cpp
converter_dunder.cpp
converter_expr.cpp
converter_funcall.cpp
converter_funcdef.cpp
converter_internal.h
converter_stmt.cpp
converter_symbols.cpp
converter_types.cpp
converter_unop.cpp
converter_util.cpp
converter_view_builtins.cpp
converter_view_escape.cpp
converter_view_hoist.cpp
converter_view_rebind.cpp
value_kinds.cpp
value_kinds.h
dynamic_type
dynamic_type_handler.cpp
dynamic_type_handler.h
literal_divergence.h
exception
exception_utils.cpp
exception_utils.h
python_exception_handler.cpp
python_exception_handler.h
function_call
builder.cpp
builder.h
builtins.cpp
cache.h
expr.cpp
expr.h
str_conv.cpp
lambda
python_lambda.cpp
python_lambda.h
math
bounded_math.cpp
bounded_math.h
cmath_lowering_policy.cpp
cmath_lowering_policy.h
complex_handler.cpp
complex_handler.h
complex_handler_utils.cpp
complex_handler_utils.h
convert_float_literal.cpp
convert_float_literal.h
math_guard_utils.cpp
math_guard_utils.h
parse_float.cpp
parse_float.h
python_int_overflow.h
python_math.cpp
python_math.h
models
numpy
linalg.py
os
path.py
abc.py
builtins.py
cmath.py
collections.py
consensus.py
dataclasses.py
datetime.py
decimal.py
enum.py
esbmc.py
exceptions.py
float.py
heapq.py
int.py
io.py
math.py
nondet.py
numpy.py
os.py
queue.py
random.py
range.py
re.py
string.py
subprocess.py
sys.py
threading.py
threading_deadlock.py
time.py
torch.py
typing.py
unittest.py
module
global_scope.h
module.h
module_locator.cpp
module_locator.h
module_manager.cpp
module_manager.h
numpy
ndarray_shape.cpp
ndarray_shape.h
numpy_call_expr.cpp
numpy_call_expr.h
numpy_nditer.cpp
numpy_nditer.h
numpy_random.cpp
numpy_random.h
numpy_reducer_shared.h
parser
__init__.py
__main__.py
bootstrap.py
class_collision.py
constant_annotations.py
import_resolver.py
json_emitter.py
nested_class_imports.py
parser.py
parser_cli.py
range_alias_pipeline.py
rewrite_re.py
threading_lowering.py
typecheck.py
preprocessor
__init__.py
assignment_core_mixin.py
assignment_visitors_mixin.py
ast_utils_mixin.py
bound_method_dispatch.py
bound_method_values.py
check_type_lowering.py
class_context_mixin.py
core_visitors_mixin.py
coroutine_lowering.py
dataclass_mixin.py
decorator_lowering.py
dotted_imports.py
expression_rewrite_mixin.py
function_sentinel_mixin.py
function_value_dispatch.py
function_value_types.py
generator_mixin.py
helper_functions_mixin.py
import_typing_mixin.py
iter_next_lowering.py
itertools_lowering.py
loop_mixin.py
match_lowering.py
module_lifecycle_mixin.py
module_rewrite_mixin.py
namedtuple_lowering.py
numpy_constructor_mixin.py
path_dependent_attributes.py
preprocessor_state_mixin.py
receiver_classes.py
rejection.py
sequence_iterator_mixin.py
sibling_defs.py
skipped_base_init.py
type_inference_mixin.py
unbound_locals.py
unittest_mixin.py
vararg_mixin.py
zip_lowering.py
python-dict
dict_access.cpp
dict_assignment.cpp
dict_compare.cpp
dict_construction.cpp
dict_core.cpp
dict_methods.cpp
dict_nested.cpp
dict_type_resolution.cpp
python_dict_handler.h	Handler for Python dictionary operations in ESBMC's Python frontend
python_dict_internal.h
python-list
list_access.cpp
list_comprehension.cpp
list_construction.cpp
list_mutation.cpp
list_query.cpp
list_set_ops.cpp
list_strided_consumers.cpp
list_string_ops.cpp
list_type_inference.cpp
list_type_inference.h
python_list.h
python_list_internal.h
python_annotation
annotation_conversion.inl
annotation_expr.inl
annotation_intrinsics.cpp
annotation_intrinsics.h
annotation_parser.cpp
annotation_parser.h
annotation_symbolic.inl
annotation_utils.cpp
annotation_utils.h
function_values.cpp
function_values.h
python_annotation.h
set
python_set.cpp
python_set.h
string
char_utils.cpp
char_utils.h
string_builder.cpp
string_builder.h
string_handler.cpp
string_handler.h
string_handler_utils.cpp
string_handler_utils.h
string_method_dispatch.h
string_method_handler.cpp
tuple
tuple_handler.cpp
tuple_handler.h
type
element_type_registry.cpp
element_type_registry.h
python_typechecking.cpp
python_typechecking.h
type_handler.cpp
type_handler.h
type_utils.h
json_utils.h
param_annotations.cpp
param_annotations.h
python2goto.cpp
python_adjust.cpp
python_adjust.h
python_blank_library.cpp
python_converter.cpp
python_converter.h
python_expr_builder.cpp
python_expr_builder.h
python_frontend_limits.h
python_language.cpp
python_language.h
python_library.cpp
python_library.h
symbol_id.cpp
symbol_id.h
solidity-frontend
pattern_check.cpp	Implementation of pattern-based vulnerability detection
pattern_check.h	Pattern-based vulnerability detection for Solidity contracts
solidity_convert.cpp	Top-level conversion driver and static member initialization
solidity_convert.h	Core AST-to-irep2 converter for the Solidity frontend
solidity_convert_builtin.cpp	Built-in function and low-level call handling for the Solidity frontend
solidity_convert_call.cpp	Function call conversion for the Solidity frontend
solidity_convert_constructor.cpp	Constructor conversion for the Solidity frontend
solidity_convert_contract.cpp	Contract-level conversion for the Solidity frontend
solidity_convert_decl.cpp	Declaration conversion for the Solidity frontend
solidity_convert_expr.cpp	Expression conversion for the Solidity frontend
solidity_convert_inheritance.cpp	Contract inheritance handling for the Solidity frontend
solidity_convert_literals.cpp	Literal conversion for the Solidity frontend
solidity_convert_mapping.cpp	Mapping type conversion for the Solidity frontend
solidity_convert_modifier.cpp	Function and modifier definition conversion for the Solidity frontend
solidity_convert_ref.cpp	Reference and symbol resolution for the Solidity frontend
solidity_convert_stmt.cpp	Statement conversion for the Solidity frontend
solidity_convert_tuple.cpp	Tuple expression conversion for the Solidity frontend
solidity_convert_type.cpp	Type conversion for the Solidity frontend
solidity_convert_util.cpp	Utility and helper functions for the Solidity converter
solidity_grammar.cpp	Implementation of Solidity grammar classification functions
solidity_grammar.h	Solidity grammar enumerations and classification helpers
solidity_language.cpp	Implementation of the Solidity language frontend
solidity_language.h	Solidity language frontend interface for ESBMC
typecast.cpp	Implementation of Solidity type casting utilities
typecast.h	Type casting utilities for the Solidity frontend
solvers
bitwuzla
bitwuzla_conv.cpp
bitwuzla_conv.h
bitwuzllob
bitwuzllob_conv.cpp
bitwuzllob_conv.h
boolector
boolector_conv.cpp
boolector_conv.h
cvc4
cvc_conv.cpp
cvc_conv.h
try_cvc4.cpp
cvc5
cvc5_conv.cpp
cvc5_conv.h
try_cvc5.cpp
mathsat
mathsat_conv.cpp
mathsat_conv.h
try_msat.c
minisat
minisat_conv.cpp
minisat_conv.h
neurosym
neurosym_conv.cpp
neurosym_conv.h
prop
literal.h
pointer_logic.cpp
pointer_logic.h
sat
bitblast_conv.cpp
bitblast_conv.h
cnf_conv.cpp
cnf_conv.h
cnf_iface.h
sat_iface.h
smt
fp
fp_conv.cpp
fp_conv.h
ir_ieee_conv.cpp
ir_ieee_conv.h
tuple
smt_tuple.cpp	So, the SMT-encoding-with-no-tuple-support
smt_tuple.h
smt_tuple_array_ast.cpp
smt_tuple_array_ast.h
smt_tuple_node.cpp
smt_tuple_node.h
smt_tuple_node_ast.cpp
smt_tuple_node_ast.h
smt_tuple_sort.h
smt_tuple_sym.cpp
smt_tuple_sym.h
smt_tuple_sym_ast.cpp
smt_tuple_sym_ast.h
array_conv.cpp
array_conv.h
simplification_equivalence.cpp
simplification_equivalence.h
smt_array.h
smt_ast.h
smt_bitcast.cpp
smt_byteops.cpp
smt_casts.cpp
smt_conv.cpp
smt_conv.h	SMT conversion tools and utilities
smt_fp_conv.cpp
smt_fp_rounding_utils.h
smt_memspace.cpp	Modelling the memory address space of C isn't something that is handled during any of the higher levels of ESBMC; it's instead left until the conversion to SMT to be handled
smt_overflow.cpp
smt_result.h
smt_solver.cpp
smt_solver.h
smt_sort.h
smtlib
oneshot_process.cpp
oneshot_process.h
smtlib_conv.cpp
smtlib_conv.h
yices
try_yices.c
yices_conv.cpp
yices_conv.h
z3
try_z3.c
z3_conv.cpp
z3_conv.h
solve.cpp
solve.h
transition-system
transition_system.cpp
transition_system.h
ts_engines.cpp
ts_engines.h
ts_extraction.cpp
ts_extraction.h
ts_slice.cpp
ts_slice.h
util
arith
arith_tools.cpp
arith_tools.h
bitvector.cpp
bitvector.h
fixedbv.cpp
fixedbv.h
format_constant.cpp
format_constant.h
format_spec.h
ieee_float.cpp
ieee_float.h
mp_arith.cpp
mp_arith.h
transcendental.cpp
transcendental.h
base
algorithm.h
breakpoint.h
compiler_defs.h
cwe_mapping.cpp
cwe_mapping.h
encoding.cpp
encoding.h
filesystem.cpp
filesystem.h
host_rounding_mode.h
i2string.cpp
i2string.h
numbering.h
picosha2.h
prefix.h
signal_catcher.cpp
signal_catcher.h
stack_budget.h
string_pool.cpp
string_pool.h
threeval.cpp
threeval.h
time_stopping.cpp
time_stopping.h
union_find.cpp
union_find.h
usr_utils.cpp
usr_utils.h
xml.cpp
xml.h
yaml_parser.cpp
yaml_parser.h
config
cmdline.cpp
cmdline.h
config.cpp
config.h
config_file.cpp
config_file.h
options.cpp
options.h
parseoptions.cpp
parseoptions.h
expr
array2string.cpp
array2string.h
array_name.cpp
array_name.h
base_type.cpp
base_type.h
expr_reassociate.cpp
expr_reassociate.h
expr_simplifier.cpp
expr_util.cpp
expr_util.h
string2array.cpp
string2array.h
string_constant.cpp
string_constant.h
symbolic_types.cpp
symbolic_types.h
type2name.cpp
type2name.h
type_byte_size.cpp
type_byte_size.h
irep
expr.cpp
expr.h
irep.cpp
irep.h
irep_idt.h
irep_serialization.cpp
irep_serialization.h
location.cpp
location.h
migrate.cpp
migrate.h
pad_names.h
std_code.cpp
std_code.h
std_expr.h
std_types.cpp
std_types.h
type.cpp
type.h
xml_irep.cpp
xml_irep.h
lang
c_builtins.h
c_expr2string.cpp
c_expr2string.h
c_link.cpp
c_link.h
c_misc.cpp
c_misc.h
c_qualifiers.cpp
c_qualifiers.h
c_sizeof.cpp
c_sizeof.h
c_typecast.cpp
c_typecast.h
c_types.cpp
c_types.h
cpp_expr2string.cpp
cpp_expr2string.h
exception_specification.cpp
exception_specification.h
fallible_calls.cpp
fallible_calls.h
language.h
parser.cpp
parser.h
python_types.cpp
python_types.h
typecheck.cpp
typecheck.h
message
formats
bigint.h
expr2t.h
exprt.h
irep_idt.h
irept.h
locationt.h
side_efect_expr_function_callt.h
symbol.h
type2t.h
typet.h
format.h
message.cpp
message.h
ssa
cache.cpp
cache.h
cache_defs.h
fingerprint.cpp
fingerprint.h
goto_expr_factory.cpp
goto_expr_factory.h
proof_cache.cpp
proof_cache.h
symtab
base_subobject.h
context.cpp
context.h
cprover_prefix.h
fix_symbol.cpp
fix_symbol.h
namespace.cpp
namespace.h
pretty.h
rename.cpp
rename.h
replace_symbol.cpp
replace_symbol.h
show_symbol_table.cpp
show_symbol_table.h
symbol.cpp
symbol.h
symbol_generator.cpp
symbol_generator.h
symbol_serialization.cpp
symbol_serialization.h
persistent_map.h