Class List

Here are the classes, structs, unions and interfaces with brief descriptions:

[detail level 1234]

N__ESBMC_exception_detail
C__ESBMC_exception_slot
C__ESBMC_handled_exception
Nabc
CABC
Ncmath_lowering_policy	Budget model that decides when cmath calls should be lowered inline vs dispatched to the Python model
Cexpr_cost
Cbudget
Ncollections
CCounter
Ncontextt_detail
Cby_id
Cby_order
Ndataclasses
CInitVar
CField
Ndatetime
Cdatetime
Ndecimal
CDecimal
Ndynamic_type_detail
Cnumeric_bindingt
Nenum
CEnum
Nesbmct	Containers and field-walking infrastructure for irep2 nodes
Cfunction_ref	Type-erased callable reference: non-owning, two pointers wide, no heap allocation
Cfunction_ref< R(Args...)>
Cmember_traits
Cmember_traits< M C::* >
Cmember_traits< const M C::* >
Ckind_excluded_field_bytes
Ckind_excluded_field_bytes< K, std::void_t< decltype(K::excluded_field_bytes)> >
Nexceptions
CBaseException
CException
CKeyboardInterrupt
CValueError
CTypeError
CAttributeError
CArithmeticError
CFloatingPointError
CLookupError
CIndexError
CKeyError
CZeroDivisionError
COverflowError
CAssertionError
CNameError
CUnboundLocalError
COSError
CFileNotFoundError
CFileExistsError
CPermissionError
CStopIteration
CRuntimeError
CNotImplementedError
CEOFError
CImportError
CModuleNotFoundError
Nfile_operations	This file will contains helper functions for manipulating files
Cfile_data	Read-only contents of a file, either bundled into the ESBMC binary or read from disk
Ctmp_path	Represents a temporary path, which is (optionally) removed by the destructor
Ctmp_file	Temporary path to an open file with an associated FILE handle
Ctmp_dir_override	Points the temp directory the functions below create paths in at dir for the lifetime of this object, restoring it on destruction
Cfilesystemt	Files bundled into the binary, overlaid on the real filesystem
Nfloat
Cfloat
Nfmt
Cformatter< BigInt >
Cformatter< expr2t >
Cformatter< exprt >
Cformatter< irep_idt >
Cformatter< irept >
Cformatter< locationt >
Cformatter< side_effect_expr_function_callt >
Cformatter< symbolt >
Cformatter< type2t >
Cformatter< typet >
Nint
Cint
Nio
CStringIO
Nllm
Ccli_clientt	LLM client that invokes an external CLI tool
Cmessage_t
Cconfigt
Cclientt	Abstract LLM client
Nparser
Nbootstrap
CParserModuleDeps
Nimport_resolver
CModuleImportInfo
CResolverCallbacks
C_SubmoduleImportSplitter
Njson_emitter
CImportResolverLike
CJsonEmitterDeps
CEmitPipelineDeps
Nnested_class_imports
C_QualifyImportedNestedClasses
Nparser_cli
CImportResolverLike
CThreadingLoweringLike
CCliDeps
C_ResolverCallbacksDeps
Npicosha2
Chash256_one_by_one
Npreprocessor
Nassignment_core_mixin
CAssignmentCoreMixin
Nassignment_visitors_mixin
CAssignmentVisitorsMixin
Nast_utils_mixin
CAstUtilsMixin
Nbound_method_dispatch
C_Dispatch
C_Replace
C_Rebound
Nbound_method_values
C_Reads
Ncheck_type_lowering
C_Lowering
C_CallSites
Nclass_context_mixin
C_QualifyNestedClasses
CClassContextMixin
Ncore_visitors_mixin
CCallBindingError
CCoreVisitorsMixin
Ncoroutine_lowering
C_Lowering
Ndataclass_mixin
CDataclassMixin
Ndotted_imports
C_Rename
Nexpression_rewrite_mixin
CExpressionRewriteMixin
C_ListCompExpressionLowerer
Nfunction_sentinel_mixin
CFunctionSentinelMixin
Nfunction_value_dispatch
C_Refused
C_Plan
C_Codes
C_Returns
C_Dispatch
Nfunction_value_types
C_Scope
C_Analysis
Ngenerator_mixin
C_GeneratorConsumerScan
CGeneratorMixin
C_YieldFromToFor
C_YieldToAppend
C_YieldReplacer
Nhelper_functions_mixin
CHelperFunctionsMixin
Nimport_typing_mixin
CImportTypingMixin
Niter_next_lowering
C_Lowering
Nloop_mixin
CLoopMixin
Nmatch_lowering
C_ReadSubject
C_MatchLowering
Nmodule_lifecycle_mixin
CModuleLifecycleMixin
Nmodule_rewrite_mixin
CModuleRewriteMixin
Nnamedtuple_lowering
C_Lowering
Nnumpy_constructor_mixin
CNumpyConstructorMixin
Npath_dependent_attributes
C_Uses
C_Rewrite
Npreprocessor_state_mixin
CPreprocessorStateMixin
Nsequence_iterator_mixin
CSequenceIteratorMixin
Ntype_inference_mixin
CTypeInferenceMixin
Nunbound_locals
C_Analysis
C_Rewriter
Nunittest_mixin
CUnittestMixin
Nvararg_mixin
CVarargMixin
CPreprocessor
Npython_param_annotations
Cmodule_ast	One module's AST
Nqueue
CQueue
CLifoQueue
Nrenaming
Crenaming_levelt
Clevel1t
Cname_record
Cname_rec_hash
Clevel2t
Cname_record
Cname_rec_hash
Cvaluet
Nstd
Cchar_traits
Cinput_iterator_tag	Marking input iterators
Coutput_iterator_tag	Marking output iterators
Cforward_iterator_tag	Marking forward iterators
Cbidirectional_iterator_tag	Marking bidirectional iterators
Crandom_access_iterator_tag
Chash< irep_idt >
Chash< assert_pair >
Nstring_method_dispatch
Csplit_method_argst
Csearch_args_parsedt
Nsubprocess
CCalledProcessError
CCompletedProcess
Nsys
C_FloatInfo
Nthreading
CLock
CThread
Nthreading_deadlock
CLock
CThread
Ntranscendental	Bounds on the transcendental functions numpy
Cinterval
Cpiece	The results for an argument in [from, to]
Cdomain	Outside [low, high] the result is NaN, and a periodic function is NaN at an infinity
Ntyping
CAny
CCallable
CClassVar
CDict
CGeneric
CIterable
CIterator
CList
COptional
CSet
CSized
CTuple
CType
CForwardRef
CUnion
CIO
CBinaryIO
CTextIO
Nunittest
CTestCase
C__dim3
C__esbmc_file_t
C__ESBMC_pointer_cell
C__ESBMC_PyListObj	Minimal representation of a Python-like list object
C__ESBMC_PyObj	Minimal representation of a Python-like object
C__ESBMC_PySliceObj	Minimal representation of a Python slice object
C__ESBMC_PyType	Type object representation for Python-like types
C__pthread_start_data
C__uint3
C_ESBMC_Mapping
C_ESBMC_Mapping_fast
C_pthread_cleanup_buffer
Cabstor
Cabstract_domain_baset
Caddress_of2t	Address of operation
Caddress_of_exprt
CAddtor
Cadjust_arm	Phase 6 (C.3) IREP2-native adjuster for the C frontend
Cai_baset	This is the basic interface of the abstract interpreter with default implementations of the core functionality
Cai_domain_baset	The interface offered by a domain, allows code to manipulate domains without knowing their exact type
Cait
Calgorithm	Base interface to run an algorithm in esbmc
Cand_exprt
Candersent
Cconstraintt
Cindirect_callt	A call through a function pointer
CAndtor
Capply_intrinsic_unroller	This transformation detects whether the unroll intrinsic was used and then mark the loop with the specific unwind
Carange_materialize_result
Carg_struct
Carg_struct1
Carg_struct1_ui
Carg_struct2
Carg_struct2_i
Carg_struct_c3
Carg_struct_d1
Carg_struct_d2
Carg_struct_f5i2
Carg_struct_ffloat
Carg_struct_fint
Carg_struct_float
Carg_struct_fuint
Carg_struct_fuintint
Carg_struct_fuintt
Carg_struct_i_ui_ull_f
Carg_struct_intt
Carg_struct_iuull
Carg_struct_no_params
Carg_struct_u1
Carg_struct_u2
Carg_struct_u3
CArithFBNode
Carray
Carray_ast
Carray_convt
Cindex_map_rec
Cidx_record
Carray_select
Carray_equality
Carray_with
Carray_of_val_rec
Ctouched_array
Carray_iface
Carray_init_elem
Carray_of_exprt
Carray_sym_smt_ast
Carray_type2t	Array type
Carray_size_excp	Common base for the two array-sizing exceptions thrown by array_type2t::get_width (and friends)
Cinf_sized_array_excp	Exception for invalid manipulations of an infinitely sized array
Cdyn_sized_array_excp	Exception for invalid manipulations of dynamically sized arrays
Carray_typet
Cassertion_cache	@Brief This class stores all asserts conditions and guards for a given SSA, if some pair was already added then it will assume that it is UNSAT
Cassign_params_as_non_det	To make the counterexample trace complete in "--function" mode
Catexit_key
Cbase_type_eqt
CBigInt
Cbinary_exprt
Cbinary_relation_exprt
Cbitblast_convt
Cbitblast_smt_ast
Cbitblast_smt_sort
Cbitcast2t	Bitcast expression
Cbitw_smt_ast
Cbitwuzla_convt
Cbitwuzllob_convt	Backend for Bitwuzllob, the integration of the Bitwuzla SMT solver into the massively parallel Mallob platform (Schreiber, Niemetz, Preiner, TACAS'26)
Cbmct
Cwitness_recordt	One enumerated witness for a failing property
Cbool_type2t	Boolean type
Cbool_typet
Cboolector_convt
Cbounded_loop_unroller	This goes through every loop of the program and tries to check if it is a bounded loop, if it is, it will be unrolled all times needed
Cbounded_math	The transcendental functions shared by numpy
Cbtor_smt_ast
Cbv_typet
Cby_id
Cby_order
Cbyte_extract2t	Extract byte from data
Cbyte_update2t	Update byte
CBytesDynamic
CBytesPool
CBytesStatic
Cc2goto_parseopt
Cc_expr2stringt
Cc_qualifierst
Cc_typecastt
Ccbmc_adapted_resultt	Result of adapting a CBMC parse into ESBMC irep conventions
Ccbmc_functiont
Ccbmc_instructiont	Intermediate parse of a CBMC instruction (mirrors cbmc.rs CBMCInstruction)
Ccbmc_irep_readert	Low-level reader for the CBMC goto-binary format (version 6)
Ccbmc_parse_resultt
Ccbmc_symbolt	Intermediate, pre-adaptation parse of a CBMC symbol (mirrors cbmc.rs CBMCSymbol)
Cchained_subarray_literal_indices
Cchar1
Cchar3
Cclaim_slicer	Claim slicer: remove every other claim of the formula with the exception of the one to keep
Cclang_c_adjust	Clang C adjuster class for:
Cclang_c_adjust_irep2
Carm_info	One arm of the dispatch, as much of it as a caller may see: what it is called, and the guard deciding whether it claims a node
Cclang_c_convertert
Cclang_c_languaget
Cclang_c_lexert
CLexerContext
Cclang_c_maint
Cclang_cpp_adjust	Clang C++ adjuster class for:
Cclang_cpp_adjust_irep2	IREP2-native adjust pass for the C++ frontend (Phase 7)
Cclang_cpp_convertert
Csubobject_destructort
Cclang_cpp_languaget
Cclang_cpp_maint
Cclass_definition
Cclass_definition_hash
Ccmdlinet
Ccmp_three_way2t	C++20 three-way comparison a <=> b
Ccnf_convt
Ccnf_iface
Ccode_asm2t
Ccode_assert2t	V.4.3: code_assert / code_assume — single-guard code kinds emitted by the Python / C++ frontends for assert and __ESBMC_assume
Ccode_assertt
Ccode_assign2t
Ccode_assignt
Ccode_assume2t
Ccode_assumet
Ccode_block2t
Ccode_blockt
Ccode_break2t
Ccode_breakt
Ccode_comma2t
Ccode_continue2t
Ccode_continuet
Ccode_contractst	Basic contract handling class Provides contract checking and replacement functionality at goto function level
Cis_fresh_mapping_t	Structure to store is_fresh mapping information
Cptr_field_snapshot_t	Per-field snapshot for pointer-struct-field assigns compliance
Cptr_deref_snapshot_t	Snapshot for pointer-parameter dereference assigns compliance (Phase 2C)
Carr_elem_snapshot_t	Snapshot for array element assigns compliance (Phase 2B)
Cparam_extentt	Byte extent of a harness-allocated pointer parameter
Ccode_cpp_catch2t
Ccode_cpp_throw2t
Ccode_deadt	A removal of a local variable
Ccode_decl2t	code_decl2t — variable declaration, with optional initializer
Ccode_declt
Ccode_dowhile2t
Ccode_expressiont
Ccode_for2t
Ccode_function_call2t
Ccode_function_callt	A `switch' instruction */ class code_switcht : public codet { public: inline code_switcht() : codet("switch") { operands().resize(2); }
Ccode_goto2t
Ccode_ifthenelse2t
Ccode_ifthenelset
Ccode_label2t
Ccode_labelt
Ccode_printf2t
Ccode_returnt
Ccode_skip2t
Ccode_skipt
Ccode_switch2t
Ccode_switch_case2t	V.4.2: one case/default arm of a switch body
Ccode_switch_caset	A switch-case
Ccode_type2t	Type of functions
Ccode_typet
Cargumentt
Ccode_while2t
Ccodet
CCoilNode
Ccollected_nondet_value	Helper structure for collected nondet values
Ccomplex_handler	Dedicated handler for complex number operations in the Python frontend
Ccomplex_type2t	Complex number type
Ccomplex_typet
Cconcat2t	Bit concatenation of two operands
Cconfigt
Ctriple
Clanguage_stdt
Cansi_ct
Cconst_target_hash
Cconstant_array2t	Constant array
Cconstant_array_of2t	Constant array of one particular value
Cconstant_bool2t	Constant boolean value
Cconstant_exprt
Cconstant_fixedbv2t	Constant fixedbv class
Cconstant_floatbv2t	Constant floatbv class
Cconstant_int2t	Constant integer class
Cconstant_string2t	Constant class for string constants
Cconstant_struct2t	Constant structure
Cconstant_union2t	Constant union expression
Cconstant_vector2t	Constant vector
CContactNode
Ccontextt
CContractor
CContractors
Ccopy_cv_
Ccopy_cv_< Dest, const Src >
Ccopy_cv_< Dest, const volatile Src >
Ccopy_cv_< Dest, volatile Src >
Ccopy_ref_
Ccopy_ref_< Dest, Src & >
Ccopy_ref_< Dest, Src && >
CCounterFBNode
Ccpp_expr2stringt
Ccpp_name_type2t	C++ Name type
Ccse_domaint	Abstract domain to obtain all available expressions (AE)
CCspMap	This class is for mapping the variables with their names and intervals
Cctest_generator	This generates CTest test-cases for C programs
Ccublashandle
CcudaDeviceProp
CcudaDevicesList	Structure that represents the devices of CUDA
Ccudnnactivationdescriptor
Ccudnnconvbwdfilter
Ccudnnconvolbwd
Ccudnnconvoldesc
Ccudnndivnormmd
Ccudnnfilterdesc
Ccudnnhandle
Ccudnnlrndesc
Ccudnntensordesc
CcurandStateScrambledSobol32
CcurandStateScrambledSobol64
CcurandStateSobol32
CcurandStateSobol64
CcurandStateTest
CcurandStateXORWOW
Ccvc5_convt
Ccvc5_smt_ast
Ccvc_convt
Ccvc_smt_ast
Ccwe_rule_t
Cdate_time
Cdead_code_finding_t
Cdead_store_advisoryt	One dead-store advisory (CWE-563, "Assignment to Variable without Use"): an assignment whose left-hand side is never read on any subsequent path
Cdefault_value_traits
Cdepth_counter_scope
Cdereference2t	Dereference operation
Cdereference_callbackt	Class providing interface to value set tracking code
Cinternal_item
Cdereference_exprt
Cdereferencet	Class containing expression dereference logic
Cmodet	The different ways in which a pointer may be accessed
Cquantifier_scopet	Records what a forall2t/exists2t binds while its body is walked, so the index fold in dereference_expr_nonscalar leaves the bound variable alone: the rename callback carries no quantifier context and would substitute the like-named program variable's SSA value (rename_quantified guards the same concern at the renaming layer, #7024)
Cdfs_execution_statet	Execution state for DFS thread exploration
Cdiv_exprt
Cdiv_t
Cdouble1
Cdouble3
Cdynamic_object2t	Record a dynamicly allocated object
Cdynamic_object_exprt
Cdynamic_type_handler
Cscope_guard	RAII: adds dynamic_type_names to the transient tagged-name set for the duration of converting one if/else's branches; removes on exit only what it added, keeping nested invocations independent
Cedget
Celement_type_registry	The single owner of per-instance element-type tracking for the Python frontend: "which types does this container instance hold?"
Cemplaced_type_of_
Cemplaced_type_of_< inserter< T > >
Cemplaced_type_of_< T >
Cempty_type2t	Empty type
Cempty_typet
Cequality_exprt
CEqualitytor
Cerror_builder
Cesbmc_parseoptionst
Cescaped_codepoint
Cexact_lu_factors
Cexception_specificationt	Canonical, function-boundary C++ exception specification
Cexception_typeidt	Closed-world numeric type-id registry for symbolic exception dispatch (issue #5075)
Cexecution_statet	Thread-aware symex state explored by reachability_treet
Cparked_patht	A path the transition parked for a deferred merge: the sibling arm of a branch, or the continuation a return parked at end_of_function
Ctransition_resultt
Cex_state_level2t	Execution_statet specific level2t
Cstate_hashing_level2t	State-hashing level2t
Ctransition_footprintt	The objects one transition read and wrote, as MPOR records them
Cexists2t
Cexp2f_data
Cexpr2ct
Cexpr2t	Base class for all expressions
Cexpr_to_ibex_parser	This class will parse ESBMC expressions to ibex expressions:
Cexprt
Cextract2t
Cfallible_call_t
Cfalse_exprt
CFBInputPort
CFBInWire
CFBOutputPort
CFBOutWire
CFBVarDecl
Cfd_set
Cfix_symbolt
Cfixedbv_spect
Cfixedbv_type2t	Fixed bitvector type
Cfixedbv_typet
Cfixedbvt
Cflat_array_shape_info
Cflattened_pointert	The pointer whose flattened representation is bits [lo, lo + width) of e whenever untouched holds (nil: always), looking through extracts, byte updates that leave those bits alone and the member layout of flatten_to_bitvector
Cfloat1
Cfloat3
Cfloat_traits
Cfloat_traits_base
Cfloatbv_type2t	Floating-point bitvector type
Cfloatbv_typet
Cforall2t
Cformat_constantt
Cformat_spect
Cformat_tokent
Cformatter
Cformatter_config
Cfp_convt
Cframe_enforcert
Csnapshot_entryt	Snapshot entry: maps an original expression to its snapshot symbol
Cclassified_assignst	Classification of assigns targets into direct, pointer, and struct-field categories
Cfunction
Cfunction_call_builder
Cfunction_call_cache	Dedicated cache for function-call resolution data
Cfunction_call_expr
Cfunction_hash
Cfunction_values	The functions a Python expression may evaluate to, gathered from every binding of the names it reads: assignments in any branch, the arguments a parameter takes at every call site, the elements of a list literal it indexes and the values a function it calls returns
Ccandidate	A function definition and the module AST it belongs to
Cget_expr_depth_guard
Cglobal_scope
CGNode
Cgoto2ct
Cgoto_atomicity_checkt
Cgoto_binary_reader
Cgoto_cfg	An implementation of a control flow graph for goto programs
Cbasic_block	A basic block is a sequence of instructions that has no branches in it
Cgoto_check_dead_store	Intra-procedural dead-store detector (CWE-563)
Cgoto_check_excessive_alloc	Detect memory allocations whose requested size can exceed a configurable byte bound K (CWE-789, "Memory Allocation with Excessive Size Value")
Cgoto_check_unchecked_return	Detect uses of a fallible call's return value that are not first constrained to the call's success domain (CWE-252, "Unchecked Return Value")
Cgoto_check_uninit_vars	Detect reads of uninitialised automatic-storage locals (CWE-457)
Cgoto_checkt
Cgoto_contractort
Cgoto_convert_functionst
Cgoto_convertt
Ctargetst
Cbreak_continue_targetst
Cbreak_switch_targetst
Cthrow_targett
Cgoto_coverage_rm
Cgoto_coveraget
Cgoto_cse	Global Common Subexpression Elimination algorithm
Cgoto_function_serializationt
Cgoto_functions_algorithm	Base interface for goto-functions algorithms
Cgoto_functionst
Cid_string_order	Order function_map by the id's string content, not by irep_idt's default operator< (which compares the string-pool interning index)
Cgoto_functiont
Cgoto_inlinet
Cgoto_loop_invariant_combinedt	Handles the Branch 1 (invariant inductivity check) for one function in the combined –loop-invariant + –k-induction mode
Cgoto_loop_invariantt
Cgoto_loopst
Cfunction_summaryt	Per-callee summary: the leaf symbols (post check_var_name filtering) that walking the callee's body would contribute to the current loop
Cgoto_program_dereferencet
Cgoto_program_serializationt
Cgoto_programt	A generic container class for a control flow graph for one function, in the form of a goto-program
Cinstructiont	Container for an instruction of the goto-program
Cloop_contract_datat
Cgoto_symex_statet	Class for storing a particular threads state
Cmerge_statet	Snapshot of the symbolic data needed to merge a deferred path
Cframet	Stack frame tracking class
Cgoto_symext	Primay symbolic execution class
Callocated_obj	Records for dynamically allocated blobs of memory
Csymex_resultt	Class recording the outcome of symbolic execution
Cdeferred_assumptiont
Cgoto_trace_stept
Cgoto_tracet
Cgrapht
CGreaterthanequaltor
CGreaterthantor
Cgroup_opt_templ
Cguard2tc	Path-condition guard container
Cguard_seq	Oldest-first immutable sequence of guard conjuncts with O(1) copy
Chash_numbering
Chost_rounding_mode
Chtml_report
CIEEE_addtor
CIEEE_divtor
CIEEE_equalitytor
Cieee_float_spect
Cieee_floatt
Cieee_fma2t	IEEE fused multiply-add operation
CIEEE_multor
CIEEE_notequalitytor
Cieee_sqrt2t	IEEE sqrt operation
CIEEE_subtor
Cif2t	If-then-else expression
Cif_exprt
Cimplies_exprt
CImpliestor
Cin6_addr
Cin_addr
Cindex2t	Array index operation
Cindex_exprt
Cinductive_step_disabled_exceptiont
Cinserted_type_of_< inserter< T >, false >
Cinserted_type_of_< T, false >
Cinserter
Cint1
Cint3
Cintcap_typet
Cinteger_limits
Cinteger_traits
Cinteger_traits< T, false >
Cinteger_traits_base
Cinterval_analysis_ibex_contractor
Cinterval_domaint	Trivial, conjunctive interval domain for both float and integers
Cinterval_templatet	This class is used to store intervals in the form of lower <= upper
Cinvalid_pointer2t
Cinvariant
Ciovec
Cir_ieee_convt	Encapsulates the integer-encoding IEEE 754 path (–int-encoding –ir-ieee)
Cra_interval_t	Interval [lo, hi] in the real-arithmetic SMT encoding
Cirep2_cast_error
Cirep2_hash
Cirep2t	Base class for every irep2 node
Cirep_container	Reference counted container for irep2 nodes
Cirep_full_eq
Cirep_full_hash
Cirep_hash
Cirep_idt
Cirep_serializationt
Cireps_containert
Cirept
Cdt
CIsfinitetor
CIsinftor
CIsnantor
CIsnormaltor
Citimerspec
Cjimple_assertion
Cjimple_assignment	An assignment statement
Cjimple_ast	Base interface for Jimple AST
Cjimple_binop	A binary operation
Cjimple_cast	A cast operation
Cjimple_class_field	A class (or interface) field of a Jimple file
Cjimple_class_member	This class will hold any member of a Jimple File
Cjimple_constant	A number constant (in decimal)
Cjimple_converter
Cjimple_declaration	Class to hold declaration statements in Jimple
Cjimple_deref	Access of arrays
Cjimple_empty_method_body	A Jimple method definition
Cjimple_expr	Base interface to hold jimple expressions
Cjimple_expr_invoke	The result of a function call
Cjimple_file	Main AST for Class/Interface
Cjimple_full_method_body	A Jimple method definition
Cjimple_goto	Goto statement
Cjimple_identity
Cjimple_if	An IF statement
Cjimple_invoke	A function call
Cjimple_label	A GOTO label
Cjimple_languaget
Cjimple_lengthof	Get the number of elements of an array (not bits/bytes)
Cjimple_method	A class (or interface) method of a Jimple file
Cjimple_method_body	A Jimple method declaration
Cjimple_method_field	The contents of a Jimple method
Cjimple_modifiers	AST parsing for modifiers
Cjimple_new	Allocates a type
Cjimple_newarray	Allocates a new array (dynamic)
Cjimple_nondet	Nondet call (This in an extension)
Cjimple_return	Return statement
Cjimple_statement	Base class for Jimple Statements
Cjimple_static_member	A static member of object/class
Cjimple_symbol	The value of a symbol (variable)
Cjimple_throw	A throw statement
Cjimple_type
Cjimple_virtual_invoke	The result of a function call
Cjimple_virtual_member	A virtual member of object
Ck_path_spanning_sett
Clanguage_uit
Clanguagest
Clanguaget
Cld_converter
Cld_languaget
CLdAst
CLdIR
CLdIRBuilder
CLdIRNode
CLdIRRung
Cldiv_t
CLdLocation
CLdParseError
CLdProperty
CLdPropertyParseError
CLdVerifyOptions
CLdVerifyResult
CLdVerifyRunner
CLessthanequaltor
CLessthantor
Clibrary_load_report
Clist_elem_info
Cliteralt
Clldiv_t
Clocal_var
Clocationt
Clogf_data
Clong1
Clong3
Clonglong1
Clonglong3
Cloopst
Cmapping_t
Cmapping_t_fast
Cmark_decl_as_non_det	This will look over non-initialized local declarations and set them as nondet
Cmathsat_convt
Cmathsat_smt_ast
Cmbstate_t
Cmember2t	Member operation
Cmember_exprt
Cmember_ref2t	Member reference
Cmember_ref_exprt
Cmessaget
Cstatet
Cminisat_convt
Cminus_exprt
Cmod_exprt
Cmode_table_et
Cmodule
Cmodule_locator
Cmodule_manager
Cmsghdr
Cmult_exprt
CMultor
Cnamespacet
Cnative_value_maker< T, T >
Cnative_value_traits
Cnearbyint2t	Nearbyint expression
CNegator
Cnested_func
CNetworkNode
Cneurosym_convt	Backend for NeuroSym, a neural-guided SMT solver (a GAN proposes candidate models, with a Z3 fallback preserving soundness and completeness)
Cnew_object2t	C++ constructor "this" placeholder (exprt("new_object"))
Cnil_exprt
Cnode_type_getter
Cnode_type_getter< array >
Cnode_type_getter< table >
Cnode_type_getter< void >
Cnode_unwrapper
Cnode_unwrapper< const value< T > >
Cnode_unwrapper< const volatile value< T > >
Cnode_unwrapper< value< T > >
Cnode_unwrapper< volatile value< T > >
Cnode_view
Cnode_wrapper
Cnode_wrapper< bool >
Cnode_wrapper< const T >
Cnode_wrapper< const volatile T >
Cnode_wrapper< date >
Cnode_wrapper< date_time >
Cnode_wrapper< double >
Cnode_wrapper< int64_t >
Cnode_wrapper< std::string >
Cnode_wrapper< time >
Cnode_wrapper< volatile T >
Cnodet
Cnot2t	Not operation
Cnot_exprt
CNotequaltor
Cnumbering
Cnumeric_value
Cnumpy_call_expr
Cnumpy_nditer	np.nditer as an iterator object over named arrays and views (ADR-NP-003): the converter keeps its position in hidden variables and lowers every read through the operand's own subscript, in the order NumPy visits it (C, F, or K: memory order, negative strides undone)
Cnumpy_nditer_item	A name bound to what an nditer yields: the element (or the external-loop chunk) of one operand at the position captured when it was bound
Cnumpy_nditer_operand	One operand of an nditer: a named array or view and its layout in elements (a negative stride walks backwards, 0 repeats a broadcast axis)
Cnumpy_nditer_state	The static description of an np.nditer: its operands, the iteration shape, and the order the positions are visited in
Cnumpy_param_call_site
Cnumpy_random	np.random
Cobject_descriptor2t
Cobject_descriptor_exprt
Copt_templ
Coptionst
Cor_exprt
COrtor
Coverflow2t	Check whether operand overflows
Coverflow_cast2t	Test if a cast overflows
Coverflow_checkst	What goto_check will instrument on the guards this pass emits
Coverflow_neg2t	Test for negation overflows
Cparse_integer_traits< 10 >
Cparse_integer_traits< 16 >
Cparse_integer_traits< 2 >
Cparse_integer_traits< 8 >
Cparse_key_buffer
Cparse_result
Cparse_scope
Cparsed_string
Cparseoptions_baset
Cparser
Cparsert
Cpath
Cpath_component
Cpattern_checker
Cpersistent_map	Persistent (structurally shared) map with O(1) copy
Cpersistent_set	Persistent set with O(1) copy, the value-less analogue of persistent_map
CPlcopenXmlParser
Cplus_exprt
Cpointee_address_equalt	Functor to check whether iterators from different collections point at the same object
Cpointer_logict
Cpointert
Cpointer_offset2t	Extract pointer offset
Cpointer_type2t	Pointer type
Cpointer_typet
Cpollfd
Cpp_range
Cpredicate_exprt
Cprintf_formattert
Ceol_exception
Cproof_cachet	Content-addressed store of claims already proved unsatisfiable
Cproperty_countst	How many properties reached each verdict, and how wide the id and line columns must be to line the rows up
Cproperty_encoder
Cproperty_locationt	Where a property lives, kept apart from the table key so the report can sort by source position and print a path once per file rather than once per line
Cproperty_resultt	A verdict together with where it applies and a note explaining how it was reached – that a discharge came from interval analysis rather than the solver, or that it was vacuous
Cproperty_rowt	One line of the property report: a verdict together with everything needed to order and print it
Cproperty_verdict_tablet	One verdict per property for a whole verification run
Cpthread_attr_t
Cpthread_barrier_t
Cpthread_barrierattr_t
Cpthread_cond_t
Cpthread_condattr_t
Cpthread_mutex_t
Cpthread_mutexattr_t
Cpthread_rwlock_t
Cpthread_rwlockattr_t
Cpthread_spinlock_t
Cptr_mem2t	Member pointer
Cptrmem_typet
Cpugi_doc_wrapper
CPyConstValue	Represents a constant Python value for compile-time evaluation
Cpytest_generator	Generates pytest test-cases for Python programs
Cpython2goto_parseopt
Cpython_adjust	V.1k (b) IREP2-native Python adjuster (phases B.0–B.2)
Cpython_annotation
Cpython_class
Cpython_class_builder
Cpython_consteval	Lightweight Python AST evaluator for compile-time function evaluation
Cpython_converter	Main converter for transforming Python AST into ESBMC's intermediate representation
Cscope_bindings	How one scope binds a name: by an import, by anything else, or by a global/nonlocal declaration handing it to an outer scope
Cpython_dict_handler	Handles Python dictionary operations for ESBMC verification
Cpython_exception_handler	Handles Python exception-related statement conversion
Cpython_int_overflow_excp
Cpython_lambda
Cpython_languaget
Cpython_list
Cstrided_axis	One axis of a strided view, in elements: its extent and stride are constants unless the matching expression is set (a signed 64-bit temporary computed at run time)
Cstrided_view_desc	A numpy array or view as a scalar base pointer plus its axes: the descriptor every N-D view is built from
Cshallow_push_call
Clist_eq_target
Cpython_math	Handles mathematical operations for Python-to-C conversion
Cpython_set	Handles Python set operations and set-specific functionality
Cpython_typechecking
Creachability_treet	Class to explore states reachable through threading
Creduction_statst	Why the schedule space shrank
Cscheduler_framet
Cexploration_framet
Creference_typet
Creplace_symbolt
Cresultt
Crewrite_op
CRungElement
CRungNode
Cruntime_encoded_equationt
Cdual_unsat_exception
Csolver_statet
Crw_sett
Centryt
Csame_object2t	Same-object operation
Csat_iface
Csc_clock
Csc_inout
Csc_module
Csc_sensitive
Csc_signal
Cscalar_value
Csched_param
Cschedule_execution_statet	Execution state class for –schedule exploration
Cscope_walker
Csem_t
Csexpr
Cshort1
Cshort3
Cside_effect_expr_function_callt
Cside_effect_expr_nondett
Cside_effect_exprt
Csideeffect2t	Irep for various side effects
Csideeffect_assign2t	V.4.2: wraps C-frontend sideeffect assignment nodes — simple = and compound +=, -=, etc
CSignbittor
Csigned_integer_traits
Csignedbv_type2t	Signed integer type
Csignedbv_typet
Csimple_slice	Naive slicer: slice every step after the last assertion
Csimplification_check_scopet	Reports the stats and uninstalls the checker when it goes out of scope
Csimplification_equivalence_checkert	Asks an SMT solver whether simplifier rewrites preserved meaning
Csizeof2t	Sizeof(T) expression
Cslicer
Csmanip
Csmt_ast
Csmt_convt	Slim, frontend-facing SMT interface
Csmt_solver_baset	The base SMT-conversion class/interface
Cflat_storet	One element update an array with denotes, as an index into the array's flattened form and the value stored there
Csmt_cache_entryt
Cuf_ackermann_entry	One recorded uninterpreted-function application in the Ackermannisation fallback: the argument asts, the fresh result ast, and the context level at which it was created (so it can be pruned on the matching pop, since pop_ctx deletes the asts made since the push)
Cptr_flatten_entry	One pointer flattened to its machine representation by a bitcast
Csmt_sort
Csmt_tuple_node_flattener
Csmt_tuple_sym_flattener
Csmtlib_convt
Cprocess_emitter
Cfile_emitter
Csymbol_table_rec
Cexternal_process_died	Thrown when the external solver process can no longer provide a usable answer: a write hit EPIPE (the process died) or its response could not be parsed (typically EOF from a dead process)
Csmtlib_smt_ast
Csmtlib_smt_sort
Csockaddr
Csockaddr_in
Csockaddr_in6
Csockaddr_storage
Csol_llc_ret
Csolidity_convertert
Cfunc_sig
Csolidity_languaget
Csolver_smt_ast
Csolver_smt_sort
Csource_position
Csource_region
Cspinlock_t
Cssa_cone_keyt	A cone's 128-bit key
Cssa_features
Cssa_step_algorithm	Base interface for ssa-step algorithms
Cst_fb_translator
Cstack_budget_guardt	Bound the stack a recursive tree walk may consume, so a pathologically deep expression or type yields a diagnostic instead of SIGSEGV (esbmc/esbmc#5048)
Cstack_framet
Cstatic_analysis_baset
Cstatic_analysist
Cstring_builder	Helper class for building and manipulating string expressions in Python frontend Handles null-termination, character extraction, and string concatenation
Cstring_constantt
Cmb_conversion_error
Cstring_handler	Handles all string-related operations for Python-to-C conversion
Cstring_pool
Cchunk_t
Cstring_traits
Cstring_view_equal
Cstring_view_hash
Cstruct_exprt	Struct constructor from list of elements
Cstruct_type2t	Struct type
Cstruct_typet
Cstruct_union_typet
Ccomponentt
CSubtor
Csymbol2t	Symbol type
Csymbol_exprt
Csymbol_generator
Csymbol_id
Csymbol_serializationt
Csymbol_type2t	Symbolic type
Csymbol_typet
Csymbolt
Csymex_dereference_statet
Csymex_slicet	Class for the symex-slicer, this slicer is to be executed on SSA formula in order to remove every symbol that does not depends on it
Csymex_target_equationt
CSSA_stept
Coutput_datat
Csymex_targett
Csourcet
Csymmetry_breakingt	SSA transformation pass that recognises lhs = ite(cond, t, e) max/min idioms in the equation and injects the redundant bounds they imply (t <= lhs && e <= lhs for a max, <= reversed for a min) as extra ASSUME steps
Csymtab_entryt
Ctable
Ctable_init_pair
Ctable_iterator
Ctable_vector_scope
Cthread_key
CthreadsList
Ctime
Ctime_offset
CTimerFBNode
Ctimespec
Ctimeval
Ctimezone
Ctm
Ctoken
CTOML_PARSE_ERROR_BASE
Ctransition_systemt	Transition system here represents a sequential circuit
Cpropertyt
Cstatet
Ctranst
Ctrue_exprt	The boolean constant true
Cts_enginet	BMC over a transition system, unrolled step by step in a single solver
Cts_step_renamert	Instantiates expressions at one step, sharing the rewrite across calls so subterms common to several expressions are copied once
Ctuple_handler	Handler for Python tuple operations
Ctuple_iface
Ctuple_node_smt_ast	Function app representing a tuple sorted value
Ctuple_sym_smt_ast
Ctvt
Ctype2_hash
Ctype2t	Base class for all types
Csymbolic_type_excp	Symbolic type exception class
Ctype_exprt
Ctype_handler
Ctype_utils
Ctypecast2t	Typecast expression
Ctypecast_exprt
CTypeChecker
CTypeCheckError
Ctypecheckt
CTypeFlags
Ctypet
Cuchar1
Cuchar3
Cuint1
Cuintcap_typet
Culong1
Culong3
Culonglong1
Culonglong3
Cunary_exprt	Generic base class for unary expressions
Cunderlying_type_
Cunderlying_type_< T, false >
Cuninterpreted_func2t	Uninterpreted-function application
Cunion_exprt	Union constructor from single element
Cunion_find
Cunion_type2t	Union type
Cunion_typet
Cunsigned_integer_traits
Cunsigned_union_find
Cnodet
Cunsignedbv_type2t	Unsigned integer type
Cunsignedbv_typet
Cunsound_loop_unroller	This is the base class that unroll a loop (in an unsound way), the idea is to copy-paste the contents of the loop N times and ignore its conditions
CUnsupportedConstructError
CUserFBDef
CUserFBExec
CUserFBInstance
Cushort1
Cushort3
Cutf8_buffered_reader
Cutf8_byte_stream< std::basic_string_view< Char > >
Cutf8_byte_stream< std::istream >
Cutf8_codepoint
Cutf8_reader
Cutf8_reader_interface
Cvalue
Cvalue_kinds	The coarse kinds of value (str, number, bool, None) a Python expression may produce, read from the module AST alone: the bindings of the names it reads, the arguments a parameter takes at every call site and its default, and what the functions and lambdas it calls return, following a function passed down a chain of parameters
Cvalue_set_analysist
Cvalue_set_domaint
Cvalue_setst
Cvalue_sett
Cobjectt	Record for an object reference
Cobject_map_dt
Centryt	Record for a particular value set: stores the identity of the variable that points at this set of objects, and the objects themselves (with associated offset data)
Cvalue_traits
Cvalue_traits< bool >
Cvalue_traits< char * >
Cvalue_traits< char[N]>
Cvalue_traits< const char * >
Cvalue_traits< const char[N]>
Cvalue_traits< const T >
Cvalue_traits< const volatile T >
Cvalue_traits< date >
Cvalue_traits< date_time >
Cvalue_traits< double >
Cvalue_traits< float >
Cvalue_traits< long double >
Cvalue_traits< signed char >
Cvalue_traits< signed int >
Cvalue_traits< signed long >
Cvalue_traits< signed long long >
Cvalue_traits< signed short >
Cvalue_traits< std::string >
Cvalue_traits< std::string_view >
Cvalue_traits< T & >
Cvalue_traits< T && >
Cvalue_traits< time >
Cvalue_traits< unsigned char >
Cvalue_traits< unsigned int >
Cvalue_traits< unsigned long >
Cvalue_traits< unsigned long long >
Cvalue_traits< unsigned short >
Cvalue_traits< volatile T >
Cvalue_traits_base_selector
Cvalue_traits_base_selector< T, true >
Cvalue_variadic_ctor_allowed
Cvalue_variadic_ctor_allowed< value< T >, value< T >, Args... >
Cvar_assignment_info
CVarDecl
CVariableUses
Cvart
Cvector_type2t	Vector type
Cvector_typet	This type maps the vectors
Cvsa_not_implemented_exception
Cw_guardst
Cwaypoint
Cparsed_constraintt
Cwith2t	With operation
Cwith_exprt
Cwrapped_interval
Cxmlt
CXortor
Cyaml_parser
CYamlPropertyParser
Cyamlt
Cyices_convt
Cyices_smt_ast
Cz3_convt
Cz3_smt_ast