| C__dim3 | |
| C__ESBMC_exception_detail::__ESBMC_exception_slot | |
| C__esbmc_file_t | |
| C__ESBMC_exception_detail::__ESBMC_handled_exception | |
| 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 | |
| Cpreprocessor.function_value_types._Analysis | |
| Cpreprocessor.unbound_locals._Analysis | |
| Cpreprocessor.bound_method_dispatch._Dispatch | |
| Cpreprocessor.function_value_dispatch._Dispatch | |
| C_ESBMC_Mapping | |
| C_ESBMC_Mapping_fast | |
| Csys._FloatInfo | |
| Cpreprocessor.generator_mixin._GeneratorConsumerScan | |
| Cpreprocessor.check_type_lowering._Lowering | |
| Cpreprocessor.iter_next_lowering._Lowering | |
| Cpreprocessor.function_value_dispatch._Plan | |
| C_pthread_cleanup_buffer | |
| Cpreprocessor.bound_method_dispatch._Rebound | |
| Cparser.parser_cli._ResolverCallbacksDeps | |
| Cpreprocessor.unbound_locals._Rewriter | |
| Cpreprocessor.function_value_types._Scope | |
| Cpreprocessor.path_dependent_attributes._Uses | |
| Cabc.ABC | |
| Cabstor< constant_type > | |
| Cabstract_domain_baset | |
| Cvalue_set_domaint | |
| CAddtor< constant_type > | |
| Cadjust_arm< Pass > | 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 |
| Cait< cse_domaint > | |
| Cait< domainT > | |
| Cai_domain_baset | The interface offered by a domain, allows code to manipulate domains without knowing their exact type |
| Ccse_domaint | Abstract domain to obtain all available expressions (AE) |
| Cinterval_domaint | Trivial, conjunctive interval domain for both float and integers |
| Calgorithm< T > | Base interface to run an algorithm in esbmc |
| Calgorithm< goto_functionst > | |
| Cgoto_functions_algorithm | Base interface for goto-functions algorithms |
| Capply_intrinsic_unroller | This transformation detects whether the unroll intrinsic was used and then mark the loop with the specific unwind |
| Cassign_params_as_non_det | To make the counterexample trace complete in "--function" mode |
| 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_contractort | |
| Cgoto_cse | Global Common Subexpression Elimination algorithm |
| Cmark_decl_as_non_det | This will look over non-initialized local declarations and set them as nondet |
| 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 |
| 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 |
| Calgorithm< symex_target_equationt::SSA_stepst > | |
| Cssa_step_algorithm | Base interface for ssa-step algorithms |
| 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 |
| Cslicer | |
| Cclaim_slicer | Claim slicer: remove every other claim of the formula with the exception of the one to keep |
| Csimple_slice | Naive slicer: slice every step after the last assertion |
| 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 |
| Cssa_features | |
| 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 |
| Cgoto_symext::allocated_obj | Records for dynamically allocated blobs of memory |
| CAndtor< constant_type > | |
| Cconfigt::ansi_ct | |
| Ctyping.Any | |
| 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 | |
| Cclang_c_adjust_irep2::arm_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 |
| Ccode_contractst::arr_elem_snapshot_t | Snapshot for array element assigns compliance (Phase 2B) |
| Carray_convt::array_equality | |
| Carray_iface | |
| Carray_convt | |
| Cbitwuzla_convt | |
| Cboolector_convt | |
| Ccvc5_convt | |
| Ccvc_convt | |
| Cmathsat_convt | |
| Csmtlib_convt | |
| Cbitwuzllob_convt | Backend for Bitwuzllob, the integration of the Bitwuzla SMT solver into the massively parallel Mallob platform (Schreiber, Niemetz, Preiner, TACAS'26) |
| Cneurosym_convt | Backend for NeuroSym, a neural-guided SMT solver (a GAN proposes candidate models, with a Z3 fallback preserving soundness and completeness) |
| Cyices_convt | |
| Cz3_convt | |
| Carray_init_elem | |
| Carray_convt::array_of_val_rec | |
| Carray_convt::array_select | |
| Carray_convt::array_with | |
| Cpreprocessor.assignment_core_mixin.AssignmentCoreMixin | |
| Cpreprocessor.Preprocessor | |
| Cpreprocessor.assignment_visitors_mixin.AssignmentVisitorsMixin | |
| Cpreprocessor.Preprocessor | |
| Cpreprocessor.ast_utils_mixin.AstUtilsMixin | |
| Cpreprocessor.Preprocessor | |
| Catexit_key | |
| Cbase_type_eqt | |
| Cexceptions.BaseException | |
| Cexceptions.Exception | |
| Cexceptions.ArithmeticError | |
| Cexceptions.FloatingPointError | |
| Cexceptions.OverflowError | |
| Cexceptions.ZeroDivisionError | |
| Cexceptions.AssertionError | |
| Cexceptions.AttributeError | |
| Cexceptions.EOFError | |
| Cexceptions.ImportError | |
| Cexceptions.ModuleNotFoundError | |
| Cexceptions.LookupError | |
| Cexceptions.IndexError | |
| Cexceptions.KeyError | |
| Cexceptions.NameError | |
| Cexceptions.UnboundLocalError | |
| Cexceptions.OSError | |
| Cexceptions.FileExistsError | |
| Cexceptions.FileNotFoundError | |
| Cexceptions.PermissionError | |
| Cexceptions.RuntimeError | |
| Cexceptions.NotImplementedError | |
| Cexceptions.StopIteration | |
| Cexceptions.TypeError | |
| Cexceptions.ValueError | |
| Cexceptions.KeyboardInterrupt | |
| Cgoto_cfg::basic_block | A basic block is a sequence of instructions that has no branches in it |
| CBigInt | |
| Cbmct | |
| Cbounded_math | The transcendental functions shared by numpy |
| Cgoto_convertt::break_continue_targetst | |
| Cgoto_convertt::break_switch_targetst | |
| Ccmath_lowering_policy::budget | |
| Cby_id | |
| Ccontextt_detail::by_id | |
| Cby_order | |
| Ccontextt_detail::by_order | |
| CBytesDynamic | |
| CBytesPool | |
| CBytesStatic | |
| Cc_expr2stringt | |
| Ccpp_expr2stringt | |
| Cexpr2ct | |
| Cc_qualifierst | |
| Cc_typecastt | |
| Ctyping.Callable | |
| Cfunction_values::candidate | A function definition and the module AST it belongs to |
| 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 | |
| Cstd::char_traits< charT > | |
| Cstring_pool::chunk_t | |
| Cclang_c_adjust | Clang C adjuster class for: |
| Cclang_cpp_adjust | Clang C++ adjuster class for: |
| Cclang_c_adjust_irep2 | |
| Cclang_cpp_adjust_irep2 | IREP2-native adjust pass for the C++ frontend (Phase 7) |
| Cclang_c_convertert | |
| Cclang_cpp_convertert | |
| Cclang_c_lexert | |
| Cclang_c_maint | |
| Cclang_cpp_maint | |
| Cclass_definition | |
| Cclass_definition_hash | |
| Cpreprocessor.class_context_mixin.ClassContextMixin | |
| Cpreprocessor.Preprocessor | |
| Cframe_enforcert::classified_assignst | Classification of assigns targets into direct, pointer, and struct-field categories |
| Ctyping.ClassVar | |
| Cparser.parser_cli.CliDeps | |
| Cllm::clientt | Abstract LLM client |
| Cllm::cli_clientt | LLM client that invokes an external CLI tool |
| Ccmdlinet | |
| Ccnf_iface | |
| Cminisat_convt | |
| Ccode_contractst | Basic contract handling class Provides contract checking and replacement functionality at goto function level |
| CCoilNode | |
| Ccollected_nondet_value | Helper structure for collected nondet values |
| Csubprocess.CompletedProcess | |
| Ccomplex_handler | Dedicated handler for complex number operations in the Python frontend |
| Cconfigt | |
| Cllm::configt | |
| Cconst_target_hash | |
| Candersent::constraintt | |
| CContactNode | |
| Ccontextt | |
| CContractor | |
| CContractors | |
| Ccopy_cv_< Dest, Src > | |
| Ccopy_cv_< Dest, const Src > | |
| Ccopy_cv_< Dest, const volatile Src > | |
| Ccopy_cv_< Dest, volatile Src > | |
| Ccopy_ref_< Dest, Src > | |
| Ccopy_ref_< Dest, Src & > | |
| Ccopy_ref_< Dest, Src && > | |
| Cpreprocessor.core_visitors_mixin.CoreVisitorsMixin | |
| Cpreprocessor.Preprocessor | |
| Ccollections.Counter | |
| CCounterFBNode | |
| 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 | |
| Ccwe_rule_t | |
| Cpreprocessor.dataclass_mixin.DataclassMixin | |
| Cpreprocessor.Preprocessor | |
| Cdate_time | |
| Cdatetime.datetime | |
| 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 |
| Cdecimal.Decimal | |
| Cdefault_value_traits | |
| Cvalue_traits< underlying_type< T > > | |
| Cvalue_traits< T & > | |
| Cvalue_traits< T && > | |
| Cvalue_traits< bool > | |
| Cvalue_traits< char * > | |
| Cvalue_traits< char[N]> | |
| Cvalue_traits< const T > | |
| Cvalue_traits< const char * > | |
| Cvalue_traits< const char[N]> | |
| 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< 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< T > | |
| Cvalue_traits< T & > | |
| Cvalue_traits< T && > | |
| Cvalue_traits< const T > | |
| Cvalue_traits< const volatile T > | |
| Cvalue_traits< volatile T > | |
| Cgoto_symext::deferred_assumptiont | |
| Cdepth_counter_scope | |
| Cdereference_callbackt | Class providing interface to value set tracking code |
| Cgoto_program_dereferencet | |
| Csymex_dereference_statet | |
| Cdereferencet | Class containing expression dereference logic |
| Ctyping.Dict | |
| Cdiv_t | |
| Ctranscendental::domain | Outside [low, high] the result is NaN, and a periodic function is NaN at an infinity |
| Cdouble1 | |
| Cdouble3 | |
| Cirept::dt | |
| Cruntime_encoded_equationt::dual_unsat_exception | |
| Cdynamic_type_handler | |
| Cedget | |
| Celement_type_registry | The single owner of per-instance element-type tracking for the Python frontend: "which types does this container instance hold?" |
| Cparser.json_emitter.EmitPipelineDeps | |
| Cemplaced_type_of_< T > | |
| Cemplaced_type_of_< inserter< T > > | |
| Cemplaced_type_of_< T > | |
| Crw_sett::entryt | |
| Cvalue_sett::entryt | 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) |
| Cenum.Enum | |
| Cprintf_formattert::eol_exception | |
| CEqualitytor< constant_type > | |
| Cerror_builder | |
| Cescaped_codepoint | |
| Cexact_lu_factors | |
| CException | |
| Cpreprocessor.function_value_dispatch._Refused | |
| Csubprocess.CalledProcessError | |
| Cstd::exception | |
| Carray_type2t::array_size_excp | Common base for the two array-sizing exceptions thrown by array_type2t::get_width (and friends) |
| Carray_type2t::dyn_sized_array_excp | Exception for invalid manipulations of dynamically sized arrays |
| Carray_type2t::inf_sized_array_excp | Exception for invalid manipulations of an infinitely sized array |
| Cexception_specificationt | Canonical, function-boundary C++ exception specification |
| Cexception_typeidt | Closed-world numeric type-id registry for symbolic exception dispatch (issue #5075) |
| Cexp2f_data | |
| Creachability_treet::exploration_framet | |
| Ccmath_lowering_policy::expr_cost | |
| Cexpr_to_ibex_parser | This class will parse ESBMC expressions to ibex expressions: |
| Cpreprocessor.expression_rewrite_mixin.ExpressionRewriteMixin | |
| Cpreprocessor.Preprocessor | |
| Cfallible_call_t | |
| Cstd::false_type | |
| Cvalue_variadic_ctor_allowed< value< T >, value< T >, Args... > | |
| CFBInputPort | |
| CFBInWire | |
| CFBOutputPort | |
| CFBOutWire | |
| CFBVarDecl | |
| Cfd_set | |
| Cdataclasses.Field | |
| Cfile_operations::file_data | Read-only contents of a file, either bundled into the ESBMC binary or read from disk |
| Csmtlib_convt::file_emitter | |
| Cfile_operations::filesystemt | Files bundled into the binary, overlaid on the real filesystem |
| Cfixedbv_spect | |
| Cfixedbvt | |
| Cflat_array_shape_info | |
| Csmt_solver_baset::flat_storet | One element update an array with denotes, as an index into the array's flattened form and the value stored there |
| 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 |
| Cfloat.float | |
| Cfloat1 | |
| Cfloat3 | |
| Cfloat_traits_base< T, MantissaDigits, DecimalDigits > | |
| Cfloat_traits_base< double, std::numeric_limits< double >::digits, std::numeric_limits< double >::digits10 > | |
| Cfloat_traits< double > | |
| Cvalue_traits< double > | |
| Cfloat_traits_base< float, std::numeric_limits< float >::digits, std::numeric_limits< float >::digits10 > | |
| Cfloat_traits< float > | |
| Cvalue_traits< float > | |
| Cfloat_traits_base< long double, std::numeric_limits< long double >::digits, std::numeric_limits< long double >::digits10 > | |
| Cfloat_traits< long double > | |
| Cvalue_traits< long double > | |
| Cfloat_traits_base< T, std::numeric_limits< T >::digits, std::numeric_limits< T >::digits10 > | |
| Cfloat_traits< T > | |
| Cformat_spect | |
| Cformat_constantt | |
| Cformat_tokent | |
| Cformatter | |
| Cfmt::formatter< BigInt > | |
| Cfmt::formatter< expr2t > | |
| Cfmt::formatter< exprt > | |
| Cfmt::formatter< irep_idt > | |
| Cfmt::formatter< irept > | |
| Cfmt::formatter< locationt > | |
| Cfmt::formatter< side_effect_expr_function_callt > | |
| Cfmt::formatter< symbolt > | |
| Cfmt::formatter< type2t > | |
| Cfmt::formatter< typet > | |
| Cformatter_config | |
| Ctyping.ForwardRef | |
| Cfp_convt | |
| Cbitwuzla_convt | |
| Cboolector_convt | |
| Ccvc5_convt | |
| Ccvc_convt | |
| Cmathsat_convt | |
| Csmtlib_convt | |
| Cyices_convt | |
| Cz3_convt | |
| Cframe_enforcert | |
| Cgoto_symex_statet::framet | Stack frame tracking class |
| Csolidity_convertert::func_sig | |
| Cfunction | |
| Cfunction_call_builder | |
| Cfunction_call_cache | Dedicated cache for function-call resolution data |
| Cfunction_call_expr | |
| Cnumpy_call_expr | |
| Cfunction_hash | |
| Cesbmct::function_ref< Signature > | Type-erased callable reference: non-owning, two pointers wide, no heap allocation |
| Cesbmct::function_ref< R(Args...)> | |
| Cgoto_loopst::function_summaryt | Per-callee summary: the leaf symbols (post check_var_name filtering) that walking the callee's body would contribute to the current loop |
| 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 |
| Cpreprocessor.function_sentinel_mixin.FunctionSentinelMixin | |
| Cpreprocessor.Preprocessor | |
| Cpreprocessor.generator_mixin.GeneratorMixin | |
| Cpreprocessor.Preprocessor | |
| Ctyping.Generic | |
| 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 |
| Cgoto_checkt | |
| Cgoto_convertt | |
| Cgoto_convert_functionst | |
| Cgoto_coverage_rm | |
| Cgoto_coveraget | |
| Cgoto_function_serializationt | |
| Cgoto_functionst | |
| Cgoto_functiont | |
| Cgoto_inlinet | |
| Cgoto_loopst | |
| 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_program_serializationt | |
| Cgoto_programt | A generic container class for a control flow graph for one function, in the form of a goto-program |
| Cgoto_symex_statet | Class for storing a particular threads state |
| Cgoto_symext | Primay symbolic execution class |
| Cexecution_statet | Thread-aware symex state explored by reachability_treet |
| Cdfs_execution_statet | Execution state for DFS thread exploration |
| Cschedule_execution_statet | Execution state class for –schedule exploration |
| Cgoto_trace_stept | |
| Cgoto_tracet | |
| Cgrapht | |
| CGreaterthanequaltor< constant_type > | |
| CGreaterthantor< constant_type > | |
| Cgroup_opt_templ | |
| Cguard_seq | Oldest-first immutable sequence of guard conjuncts with O(1) copy |
| Cpicosha2::hash256_one_by_one | |
| Cstd::hash< assert_pair > | |
| Cstd::hash< irep_idt > | |
| Chash_numbering< T, hash_fkt > | |
| Cpreprocessor.helper_functions_mixin.HelperFunctionsMixin | |
| Cpreprocessor.Preprocessor | |
| Chost_rounding_mode | |
| Chtml_report | |
| Cgoto_functionst::id_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) |
| Carray_convt::idx_record | |
| CIEEE_addtor< constant_type > | |
| CIEEE_divtor< constant_type > | |
| CIEEE_equalitytor< constant_type > | |
| Cieee_float_spect | |
| Cieee_floatt | |
| CIEEE_multor< constant_type > | |
| CIEEE_notequalitytor< constant_type > | |
| CIEEE_subtor< constant_type > | |
| CImpliestor< constant_type > | |
| Cpreprocessor.import_typing_mixin.ImportTypingMixin | |
| Cpreprocessor.Preprocessor | |
| Cin6_addr | |
| Cin_addr | |
| Carray_convt::index_map_rec | |
| Candersent::indirect_callt | A call through a function pointer |
| Cinductive_step_disabled_exceptiont | |
| Cdataclasses.InitVar | |
| Cstd::input_iterator_tag | Marking input iterators |
| Cstd::forward_iterator_tag | Marking forward iterators |
| Cstd::bidirectional_iterator_tag | Marking bidirectional iterators |
| Cstd::random_access_iterator_tag | |
| Cinserted_type_of_< inserter< T >, false > | |
| Cinserted_type_of_< T, false > | |
| Cinserter< T > | |
| Cgoto_programt::instructiont | Container for an instruction of the goto-program |
| Cint.int | |
| Cint1 | |
| Cint3 | |
| Cinteger_limits< T > | |
| Cinteger_traits_base< T > | |
| Csigned_integer_traits< T > | |
| Cinteger_traits< T, false > | |
| Cinteger_traits< T, S > | |
| Cunsigned_integer_traits< T > | |
| Cinteger_traits< T, false > | |
| Cinteger_limits< signed char > | |
| Cinteger_traits_base< signed char > | |
| Csigned_integer_traits< signed char > | |
| Cinteger_traits< signed char > | |
| Cvalue_traits< signed char > | |
| Cinteger_limits< signed int > | |
| Cinteger_traits_base< signed int > | |
| Csigned_integer_traits< signed int > | |
| Cinteger_traits< signed int > | |
| Cvalue_traits< signed int > | |
| Cinteger_limits< signed long > | |
| Cinteger_traits_base< signed long > | |
| Csigned_integer_traits< signed long > | |
| Cinteger_traits< signed long > | |
| Cvalue_traits< signed long > | |
| Cinteger_limits< signed long long > | |
| Cinteger_traits_base< signed long long > | |
| Csigned_integer_traits< signed long long > | |
| Cinteger_traits< signed long long > | |
| Cvalue_traits< signed long long > | |
| Cinteger_limits< signed short > | |
| Cinteger_traits_base< signed short > | |
| Csigned_integer_traits< signed short > | |
| Cinteger_traits< signed short > | |
| Cvalue_traits< signed short > | |
| Cinteger_limits< unsigned char > | |
| Cinteger_traits_base< unsigned char > | |
| Csigned_integer_traits< unsigned char > | |
| Cinteger_traits< unsigned char > | |
| Cvalue_traits< unsigned char > | |
| Cinteger_limits< unsigned int > | |
| Cinteger_traits_base< unsigned int > | |
| Csigned_integer_traits< unsigned int > | |
| Cinteger_traits< unsigned int > | |
| Cvalue_traits< unsigned int > | |
| Cinteger_limits< unsigned long > | |
| Cinteger_traits_base< unsigned long > | |
| Csigned_integer_traits< unsigned long > | |
| Cinteger_traits< unsigned long > | |
| Cvalue_traits< unsigned long > | |
| Cinteger_limits< unsigned long long > | |
| Cinteger_traits_base< unsigned long long > | |
| Csigned_integer_traits< unsigned long long > | |
| Cinteger_traits< unsigned long long > | |
| Cvalue_traits< unsigned long long > | |
| Cinteger_limits< unsigned short > | |
| Cinteger_traits_base< unsigned short > | |
| Csigned_integer_traits< unsigned short > | |
| Cinteger_traits< unsigned short > | |
| Cvalue_traits< unsigned short > | |
| Cdereference_callbackt::internal_item | |
| Ctranscendental::interval | |
| Cinterval_analysis_ibex_contractor | |
| Cinterval_templatet< T > | This class is used to store intervals in the form of lower <= upper |
| Cinterval_templatet< BigInt > | |
| Cwrapped_interval | |
| Cinvariant | |
| Ctyping.IO | |
| Ctyping.BinaryIO | |
| Ctyping.TextIO | |
| Ciovec | |
| Cir_ieee_convt | Encapsulates the integer-encoding IEEE 754 path (–int-encoding –ir-ieee) |
| Cirep2_hash | |
| Cirep2t | Base class for every irep2 node |
| Cexpr2t | Base class for all expressions |
| Caddress_of2t | Address of operation |
| Cbitcast2t | Bitcast expression |
| Cbyte_extract2t | Extract byte from data |
| Cbyte_update2t | Update byte |
| Ccmp_three_way2t | C++20 three-way comparison a <=> b |
| 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_assign2t | |
| Ccode_assume2t | |
| Ccode_block2t | |
| Ccode_break2t | |
| Ccode_comma2t | |
| Ccode_continue2t | |
| Ccode_cpp_catch2t | |
| Ccode_cpp_throw2t | |
| Ccode_decl2t | code_decl2t — variable declaration, with optional initializer |
| Ccode_dowhile2t | |
| Ccode_for2t | |
| Ccode_function_call2t | |
| Ccode_goto2t | |
| Ccode_ifthenelse2t | |
| Ccode_label2t | |
| Ccode_printf2t | |
| Ccode_skip2t | |
| Ccode_switch2t | |
| Ccode_switch_case2t | V.4.2: one case/default arm of a switch body |
| Ccode_while2t | |
| Cconcat2t | Bit concatenation of two operands |
| Cconstant_array2t | Constant array |
| Cconstant_array_of2t | Constant array of one particular value |
| Cconstant_bool2t | Constant boolean value |
| 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 |
| Cdereference2t | Dereference operation |
| Cdynamic_object2t | Record a dynamicly allocated object |
| Cexists2t | |
| Cextract2t | |
| Cforall2t | |
| Cieee_fma2t | IEEE fused multiply-add operation |
| Cieee_sqrt2t | IEEE sqrt operation |
| Cif2t | If-then-else expression |
| Cindex2t | Array index operation |
| Cinvalid_pointer2t | |
| Cmember2t | Member operation |
| Cmember_ref2t | Member reference |
| Cnearbyint2t | Nearbyint expression |
| Cnew_object2t | C++ constructor "this" placeholder (exprt("new_object")) |
| Cnot2t | Not operation |
| Cobject_descriptor2t | |
| Coverflow2t | Check whether operand overflows |
| Coverflow_cast2t | Test if a cast overflows |
| Coverflow_neg2t | Test for negation overflows |
| Cpointer_offset2t | Extract pointer offset |
| Cptr_mem2t | Member pointer |
| Csame_object2t | Same-object operation |
| Csideeffect2t | Irep for various side effects |
| Csideeffect_assign2t | V.4.2: wraps C-frontend sideeffect assignment nodes — simple = and compound +=, -=, etc |
| Csizeof2t | Sizeof(T) expression |
| Csymbol2t | Symbol type |
| Ctypecast2t | Typecast expression |
| Cuninterpreted_func2t | Uninterpreted-function application |
| Cwith2t | With operation |
| Ctype2t | Base class for all types |
| Carray_type2t | Array type |
| Cbool_type2t | Boolean type |
| Ccode_type2t | Type of functions |
| Ccomplex_type2t | Complex number type |
| Ccpp_name_type2t | C++ Name type |
| Cempty_type2t | Empty type |
| Cfixedbv_type2t | Fixed bitvector type |
| Cfloatbv_type2t | Floating-point bitvector type |
| Cpointer_type2t | Pointer type |
| Csignedbv_type2t | Signed integer type |
| Cstruct_type2t | Struct type |
| Csymbol_type2t | Symbolic type |
| Cunion_type2t | Union type |
| Cunsignedbv_type2t | Unsigned integer type |
| Cvector_type2t | Vector type |
| Cirep_container< T > | Reference counted container for irep2 nodes |
| Cirep_container< expr2t > | |
| Cguard2tc | Path-condition guard container |
| Cirep_full_eq | |
| Cirep_full_hash | |
| Cirep_hash | |
| Cirep_idt | |
| Cirep_serializationt | |
| Cirep_serializationt::ireps_containert | |
| Cirept | |
| Cexprt | |
| Caddress_of_exprt | |
| Cand_exprt | |
| Carray_of_exprt | |
| Cbinary_exprt | |
| Cdiv_exprt | |
| Cminus_exprt | |
| Cmod_exprt | |
| Cmult_exprt | |
| Cplus_exprt | |
| Ccode_typet::argumentt | |
| Ccodet | |
| Ccode_assertt | |
| Ccode_assignt | |
| Ccode_assumet | |
| Ccode_blockt | |
| Ccode_breakt | |
| Ccode_continuet | |
| Ccode_deadt | A removal of a local variable |
| Ccode_declt | |
| Ccode_expressiont | |
| Ccode_function_callt | A `switch' instruction */ class code_switcht : public codet { public: inline code_switcht() : codet("switch") { operands().resize(2); } |
| Ccode_ifthenelset | |
| Ccode_labelt | |
| Ccode_returnt | |
| Ccode_skipt | |
| Ccode_switch_caset | A switch-case |
| Cconstant_exprt | |
| Cfalse_exprt | |
| Ctrue_exprt | The boolean constant true |
| Cdereference_exprt | |
| Cdynamic_object_exprt | |
| Cif_exprt | |
| Cimplies_exprt | |
| Cindex_exprt | |
| Cmember_exprt | |
| Cmember_ref_exprt | |
| Cnil_exprt | |
| Cnot_exprt | |
| Cobject_descriptor_exprt | |
| Cor_exprt | |
| Cpredicate_exprt | |
| Cbinary_relation_exprt | |
| Cequality_exprt | |
| Cside_effect_exprt | |
| Cside_effect_expr_function_callt | |
| Cside_effect_expr_nondett | |
| Cstring_constantt | |
| Cstruct_exprt | Struct constructor from list of elements |
| Cstruct_union_typet::componentt | |
| Csymbol_exprt | |
| Ctranst | |
| Ctype_exprt | |
| Ctypecast_exprt | |
| Cunary_exprt | Generic base class for unary expressions |
| Cunion_exprt | Union constructor from single element |
| Cwith_exprt | |
| Clocationt | |
| Ctypet | |
| Carray_typet | |
| Cbool_typet | |
| Cbv_typet | |
| Cfixedbv_typet | |
| Cfloatbv_typet | |
| Csignedbv_typet | |
| Cunsignedbv_typet | |
| Ccode_typet | |
| Cempty_typet | |
| Cintcap_typet | |
| Cpointer_typet | |
| Creference_typet | |
| Cptrmem_typet | |
| Cstruct_union_typet | |
| Ccomplex_typet | |
| Cstruct_typet | |
| Cunion_typet | |
| Csymbol_typet | |
| Cuintcap_typet | |
| Cvector_typet | This type maps the vectors |
| Ccode_contractst::is_fresh_mapping_t | Structure to store is_fresh mapping information |
| CIsfinitetor< constant_type > | |
| CIsinftor< constant_type > | |
| CIsnantor< constant_type > | |
| CIsnormaltor< constant_type > | |
| Ctyping.Iterable | |
| Ctyping.Iterator | |
| Citimerspec | |
| Cjimple_ast | Base interface for Jimple AST |
| Cjimple_class_member | This class will hold any member of a Jimple File |
| Cjimple_class_field | A class (or interface) field of a Jimple file |
| Cjimple_method | A class (or interface) method of a Jimple file |
| Cjimple_expr | Base interface to hold jimple expressions |
| Cjimple_binop | A binary operation |
| Cjimple_cast | A cast operation |
| Cjimple_constant | A number constant (in decimal) |
| Cjimple_deref | Access of arrays |
| Cjimple_expr_invoke | The result of a function call |
| Cjimple_lengthof | Get the number of elements of an array (not bits/bytes) |
| Cjimple_newarray | Allocates a new array (dynamic) |
| Cjimple_new | Allocates a type |
| Cjimple_nondet | Nondet call (This in an extension) |
| Cjimple_static_member | A static member of object/class |
| Cjimple_symbol | The value of a symbol (variable) |
| Cjimple_virtual_invoke | The result of a function call |
| Cjimple_virtual_member | A virtual member of object |
| Cjimple_file | Main AST for Class/Interface |
| Cjimple_method_body | A Jimple method declaration |
| Cjimple_empty_method_body | A Jimple method definition |
| Cjimple_full_method_body | A Jimple method definition |
| Cjimple_method_field | The contents of a Jimple method |
| Cjimple_declaration | Class to hold declaration statements in Jimple |
| Cjimple_statement | Base class for Jimple Statements |
| Cjimple_assertion | |
| Cjimple_assignment | An assignment statement |
| Cjimple_goto | Goto statement |
| Cjimple_identity | |
| Cjimple_if | An IF statement |
| Cjimple_invoke | A function call |
| Cjimple_label | A GOTO label |
| Cjimple_return | Return statement |
| Cjimple_throw | A throw statement |
| Cjimple_modifiers | AST parsing for modifiers |
| Cjimple_type | |
| Cjimple_converter | |
| Cparser.json_emitter.JsonEmitterDeps | |
| Ck_path_spanning_sett | |
| Cesbmct::kind_excluded_field_bytes< K, class > | |
| Cesbmct::kind_excluded_field_bytes< K, std::void_t< decltype(K::excluded_field_bytes)> > | |
| Cconfigt::language_stdt | |
| Clanguage_uit | |
| Cc2goto_parseopt | |
| Cesbmc_parseoptionst | |
| Cpython2goto_parseopt | |
| Clanguagest | |
| Clanguaget | |
| Cclang_c_languaget | |
| Cclang_cpp_languaget | |
| Csolidity_languaget | |
| Cjimple_languaget | |
| Cld_languaget | |
| Cpython_languaget | |
| Cld_converter | |
| CLdAst | |
| CLdIR | |
| CLdIRBuilder | |
| CLdIRNode | |
| CLdIRRung | |
| Cldiv_t | |
| CLdLocation | |
| CLdProperty | |
| CLdVerifyOptions | |
| CLdVerifyResult | |
| CLdVerifyRunner | |
| CLessthanequaltor< constant_type > | |
| CLessthantor< constant_type > | |
| Cclang_c_lexert::LexerContext | |
| Clibrary_load_report | |
| Cqueue.LifoQueue | |
| Ctyping.List | |
| Clist_elem_info | |
| Cpython_list::list_eq_target | |
| Cliteralt | |
| Clldiv_t | |
| Clocal_var | |
| Cthreading.Lock | |
| Cthreading_deadlock.Lock | |
| Clogf_data | |
| Cstd::logic_error | |
| Cirep2_cast_error | |
| Clong1 | |
| Clong3 | |
| Clonglong1 | |
| Clonglong3 | |
| Cgoto_programt::instructiont::loop_contract_datat | |
| Cpreprocessor.loop_mixin.LoopMixin | |
| Cpreprocessor.Preprocessor | |
| Cloopst | |
| Cmapping_t | |
| Cmapping_t_fast | |
| Cmbstate_t | |
| Cesbmct::member_traits< P > | |
| Cesbmct::member_traits< const M C::* > | |
| Cesbmct::member_traits< M C::* > | |
| Cgoto_symex_statet::merge_statet | Snapshot of the symbolic data needed to merge a deferred path |
| Cllm::message_t | |
| Cmessaget | |
| Cmode_table_et | |
| Cdereferencet::modet | The different ways in which a pointer may be accessed |
| Cmodule | |
| Cpython_param_annotations::module_ast | One module's AST |
| Cmodule_locator | |
| Cmodule_manager | |
| Cpreprocessor.module_lifecycle_mixin.ModuleLifecycleMixin | |
| Cpreprocessor.Preprocessor | |
| Cpreprocessor.module_rewrite_mixin.ModuleRewriteMixin | |
| Cpreprocessor.Preprocessor | |
| Cmsghdr | |
| CMultor< constant_type > | |
| Crenaming::level1t::name_rec_hash | |
| Crenaming::level2t::name_rec_hash | |
| Crenaming::level1t::name_record | |
| Crenaming::level2t::name_record | |
| Cnamespacet | |
| Cnative_value_maker< T, T > | |
| Cnative_value_traits< T, NodeType > | |
| Cnative_value_traits< bool, node_type::boolean > | |
| Cvalue_traits< bool > | |
| Cnative_value_traits< date, node_type::date > | |
| Cvalue_traits< date > | |
| Cnative_value_traits< date_time, node_type::date_time > | |
| Cvalue_traits< date_time > | |
| Cnative_value_traits< time, node_type::time > | |
| Cvalue_traits< time > | |
| CNegator< constant_type > | |
| Cnested_func | |
| CNetworkNode | |
| Cnode | |
| Carray | |
| Ctable | |
| Cnode_type_getter< T > | |
| Cnode_type_getter< array > | |
| Cnode_type_getter< table > | |
| Cnode_type_getter< void > | |
| Cnode_unwrapper< T > | |
| Cnode_unwrapper< const value< T > > | |
| Cnode_unwrapper< const volatile value< T > > | |
| Cnode_unwrapper< value< T > > | |
| Cnode_unwrapper< volatile value< T > > | |
| Cnode_view< typename > | |
| Cnode_wrapper< T > | |
| 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 | |
| Cunsigned_union_find::nodet | |
| Cast.NodeTransformer | |
| Cparser.import_resolver._SubmoduleImportSplitter | |
| Cparser.nested_class_imports._QualifyImportedNestedClasses | |
| Cpreprocessor.bound_method_dispatch._Replace | |
| Cpreprocessor.bound_method_values._Reads | |
| Cpreprocessor.check_type_lowering._CallSites | |
| Cpreprocessor.class_context_mixin._QualifyNestedClasses | |
| Cpreprocessor.coroutine_lowering._Lowering | |
| Cpreprocessor.dotted_imports._Rename | |
| Cpreprocessor.expression_rewrite_mixin.ExpressionRewriteMixin._ListCompExpressionLowerer | |
| Cpreprocessor.function_value_dispatch._Codes | |
| Cpreprocessor.function_value_dispatch._Returns | |
| Cpreprocessor.generator_mixin.GeneratorMixin._YieldFromToFor | |
| Cpreprocessor.generator_mixin.GeneratorMixin._YieldReplacer | |
| Cpreprocessor.generator_mixin.GeneratorMixin._YieldToAppend | |
| Cpreprocessor.match_lowering._MatchLowering | |
| Cpreprocessor.match_lowering._ReadSubject | |
| Cpreprocessor.namedtuple_lowering._Lowering | |
| Cpreprocessor.path_dependent_attributes._Rewrite | |
| CNodeTransformer | |
| Cpreprocessor.Preprocessor | |
| CNotequaltor< constant_type > | |
| Cnumbering< T > | |
| Cunion_find< irep_idt > | |
| Cunion_find< T > | |
| Cdynamic_type_detail::numeric_bindingt | |
| Cnumeric_value | |
| 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
|
| Cpreprocessor.numpy_constructor_mixin.NumpyConstructorMixin | |
| Cpreprocessor.Preprocessor | |
| Cvalue_sett::object_map_dt | |
| Cvalue_sett::objectt | Record for an object reference |
| Copt_templ | |
| Ctyping.Optional | |
| Coptionst | |
| COrtor< constant_type > | |
| Csymex_target_equationt::SSA_stept::output_datat | |
| Cstd::output_iterator_tag | Marking output iterators |
| Coverflow_checkst | What goto_check will instrument on the guards this pass emits |
| Ccode_contractst::param_extentt | Byte extent of a harness-allocated pointer parameter |
| Cexecution_statet::parked_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 |
| Cparse_integer_traits< 10 > | |
| Cparse_integer_traits< 16 > | |
| Cparse_integer_traits< 2 > | |
| Cparse_integer_traits< 8 > | |
| Cparse_key_buffer | |
| Cparse_result | |
| Cparse_scope | |
| Cwaypoint::parsed_constraintt | |
| Cparsed_string | |
| Cparseoptions_baset | |
| Cc2goto_parseopt | |
| Cesbmc_parseoptionst | |
| Cpython2goto_parseopt | |
| Cparser | |
| Cparser.bootstrap.ParserModuleDeps | |
| Cparsert | |
| Cpath | |
| Cpath_component | |
| Cpattern_checker | |
| Cpersistent_map< K, V, Hash > | Persistent (structurally shared) map with O(1) copy |
| Cpersistent_set< K, Hash > | Persistent set with O(1) copy, the value-less analogue of persistent_map |
| Ctranscendental::piece | The results for an argument in [from, to] |
| CPlcopenXmlParser | |
| Cpointee_address_equalt | Functor to check whether iterators from different collections point at the same object |
| Cpointer_logict | |
| Cpointer_logict::pointert | |
| Cpollfd | |
| Cpp_range | |
| Cpreprocessor.preprocessor_state_mixin.PreprocessorStateMixin | |
| Cpreprocessor.Preprocessor | |
| Cprintf_formattert | |
| Csmtlib_convt::process_emitter | |
| 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 |
| Ctransition_systemt::propertyt | |
| CProtocol | |
| Cparser.json_emitter.ImportResolverLike | |
| Cparser.parser_cli.ImportResolverLike | |
| Cparser.parser_cli.ThreadingLoweringLike | |
| 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 | |
| Ccode_contractst::ptr_deref_snapshot_t | Snapshot for pointer-parameter dereference assigns compliance (Phase 2C) |
| Ccode_contractst::ptr_field_snapshot_t | Per-field snapshot for pointer-struct-field assigns compliance |
| Csmt_solver_baset::ptr_flatten_entry | One pointer flattened to its machine representation by a bitcast |
| Cpugi_doc_wrapper | |
| CPyConstValue | Represents a constant Python value for compile-time evaluation |
| Cpytest_generator | Generates pytest test-cases for Python programs |
| Cpython_adjust | V.1k (b) IREP2-native Python adjuster (phases B.0–B.2) |
| Cpython_annotation< Json > | |
| 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 |
| Cpython_dict_handler | Handles Python dictionary operations for ESBMC verification |
| Cpython_exception_handler | Handles Python exception-related statement conversion |
| Cpython_lambda | |
| Cpython_list | |
| Cpython_math | Handles mathematical operations for Python-to-C conversion |
| Cpython_set | Handles Python set operations and set-specific functionality |
| Cpython_typechecking | |
| Cdereferencet::quantifier_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) |
| Cqueue.Queue | |
| Cir_ieee_convt::ra_interval_t | Interval [lo, hi] in the real-arithmetic SMT encoding |
| Creachability_treet | Class to explore states reachable through threading |
| Creachability_treet::reduction_statst | Why the schedule space shrank |
| Crenaming::renaming_levelt | |
| Crenaming::level1t | |
| Crenaming::level2t | |
| Cexecution_statet::ex_state_level2t | Execution_statet specific level2t |
| Cexecution_statet::state_hashing_level2t | State-hashing level2t |
| Creplace_symbolt | |
| Cfix_symbolt | |
| Cparser.import_resolver.ResolverCallbacks | |
| Cresultt | |
| Crewrite_op | |
| CRungElement | |
| CRungNode | |
| Cstd::runtime_error | |
| CLdParseError | |
| CLdPropertyParseError | |
| CTypeCheckError | |
| CUnsupportedConstructError | |
| Cpython_int_overflow_excp | |
| Csmtlib_convt::external_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) |
| Cstring_constantt::mb_conversion_error | |
| Crw_sett | |
| Csat_iface | |
| Ccnf_convt | |
| Cminisat_convt | |
| Csc_clock | |
| Csc_inout< T > | |
| Csc_module | |
| Csc_sensitive | |
| Csc_signal< T > | |
| Cscalar_value | |
| Csched_param | |
| Creachability_treet::scheduler_framet | |
| Cpython_converter::scope_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 |
| Cdynamic_type_handler::scope_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 |
| Cscope_walker | |
| Cstring_method_dispatch::search_args_parsedt | |
| Csem_t | |
| Cpreprocessor.sequence_iterator_mixin.SequenceIteratorMixin | |
| Cpreprocessor.Preprocessor | |
| Ctyping.Set | |
| Csexpr | |
| Cpython_list::shallow_push_call | |
| Cshort1 | |
| Cshort3 | |
| CSignbittor< constant_type > | |
| 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 |
| Ctyping.Sized | |
| Csmanip | |
| Csmt_ast | |
| Csolver_smt_ast< bitwuzla::Term > | |
| Cbitw_smt_ast | |
| Csolver_smt_ast< BoolectorNode * > | |
| Cbtor_smt_ast | |
| Csolver_smt_ast< cvc5::Term > | |
| Ccvc5_smt_ast | |
| Csolver_smt_ast< CVC4::Expr > | |
| Ccvc_smt_ast | |
| Csolver_smt_ast< msat_term > | |
| Cmathsat_smt_ast | |
| Csolver_smt_ast< term_t > | |
| Cyices_smt_ast | |
| Csolver_smt_ast< z3::expr > | |
| Cz3_smt_ast | |
| Carray_ast | |
| Cbitblast_smt_ast | |
| Csmtlib_smt_ast | |
| Csolver_smt_ast< solver_ast > | |
| Ctuple_node_smt_ast | Function app representing a tuple sorted value |
| Ctuple_sym_smt_ast | |
| Carray_sym_smt_ast | |
| Csmt_solver_baset::smt_cache_entryt | |
| Csmt_convt | Slim, frontend-facing SMT interface |
| Csmt_solver_baset | The base SMT-conversion class/interface |
| Cbitblast_convt | |
| Cminisat_convt | |
| Cbitwuzla_convt | |
| Cboolector_convt | |
| Ccvc5_convt | |
| Ccvc_convt | |
| Cmathsat_convt | |
| Csmtlib_convt | |
| Cyices_convt | |
| Cz3_convt | |
| Csmt_sort | |
| Cbitblast_smt_sort | |
| Csmtlib_smt_sort | |
| Csolver_smt_sort< solver_sort > | |
| Cframe_enforcert::snapshot_entryt | Snapshot entry: maps an original expression to its snapshot symbol |
| Csockaddr | |
| Csockaddr_in | |
| Csockaddr_in6 | |
| Csockaddr_storage | |
| Csol_llc_ret | |
| Csolidity_convertert | |
| Cruntime_encoded_equationt::solver_statet | |
| Csource_position | |
| Csource_region | |
| Csymex_targett::sourcet | |
| Cspinlock_t | |
| Cstring_method_dispatch::split_method_argst | |
| Cssa_cone_keyt | A cone's 128-bit key |
| Csymex_target_equationt::SSA_stept | |
| Cst_fb_translator | |
| Cstack_budget_guardt< Tag > | 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 | |
| Cmessaget::statet | |
| Ctransition_systemt::statet | |
| Cstatic_analysis_baset | |
| Cstatic_analysist< value_set_domaint > | |
| Cvalue_set_analysist | |
| Cstatic_analysist< T > | |
| Cpython_list::strided_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) |
| Cpython_list::strided_view_desc | A numpy array or view as a scalar base pointer plus its axes: the descriptor every N-D view is built from |
| Cstring_builder | Helper class for building and manipulating string expressions in Python frontend Handles null-termination, character extraction, and string concatenation |
| Cstring_handler | Handles all string-related operations for Python-to-C conversion |
| Cstring_pool | |
| Cstring_traits< T > | |
| Cstring_traits< char * > | |
| Cvalue_traits< char * > | |
| Cstring_traits< char[N]> | |
| Cvalue_traits< char[N]> | |
| Cstring_traits< const char * > | |
| Cvalue_traits< const char * > | |
| Cstring_traits< const char[N]> | |
| Cvalue_traits< const char[N]> | |
| Cstring_traits< std::string > | |
| Cvalue_traits< std::string > | |
| Cstring_traits< std::string_view > | |
| Cvalue_traits< std::string_view > | |
| Cstring_view_equal | |
| Cstring_view_hash | |
| Cio.StringIO | |
| Cclang_cpp_convertert::subobject_destructort | |
| CSubtor< constant_type > | |
| Csymbol_generator | |
| Csymbol_id | |
| Csymbol_serializationt | |
| Csmtlib_convt::symbol_table_rec | |
| Ctype2t::symbolic_type_excp | Symbolic type exception class |
| Csymbolt | |
| Cgoto_symext::symex_resultt | Class recording the outcome of symbolic execution |
| Csymex_targett | |
| Csymex_target_equationt | |
| Cruntime_encoded_equationt | |
| Csymtab_entryt | |
| Ctable_init_pair | |
| Ctable_iterator< IsConst > | |
| Ctable_vector_scope | |
| Cgoto_convertt::targetst | |
| Cunittest.TestCase | |
| Cthreading.Thread | |
| Cthreading_deadlock.Thread | |
| Cthread_key | |
| CthreadsList | |
| Cgoto_convertt::throw_targett | |
| Ctime | |
| Ctime_offset | |
| CTimerFBNode | |
| Ctimespec | |
| Ctimeval | |
| Ctimezone | |
| Ctm | |
| Cfile_operations::tmp_dir_override | Points the temp directory the functions below create paths in at dir for the lifetime of this object, restoring it on destruction |
| Cfile_operations::tmp_path | Represents a temporary path, which is (optionally) removed by the destructor |
| Cfile_operations::tmp_file | Temporary path to an open file with an associated FILE handle |
| Ctoken | |
| CTOML_PARSE_ERROR_BASE | |
| Carray_convt::touched_array | |
| Cexecution_statet::transition_footprintt | The objects one transition read and wrote, as MPOR records them |
| Cexecution_statet::transition_resultt | |
| Ctransition_systemt | Transition system here represents a sequential circuit |
| Cconfigt::triple | |
| Cstd::true_type | |
| Cvalue_variadic_ctor_allowed< value< T >, value< T >, Args... > | |
| Cvalue_variadic_ctor_allowed<... > | |
| 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 |
| Ctyping.Tuple | |
| Ctuple_handler | Handler for Python tuple operations |
| Ctuple_iface | |
| Csmt_tuple_node_flattener | |
| Csmt_tuple_sym_flattener | |
| Cyices_convt | |
| Cz3_convt | |
| Ctvt | |
| Ctyping.Type | |
| Ctype2_hash | |
| Ctype_handler | |
| Ctype_utils | |
| CTypeChecker | |
| Ctypecheckt | |
| CTypedDict | |
| Cparser.import_resolver.ModuleImportInfo | |
| CTypeError | |
| Cpreprocessor.core_visitors_mixin.CallBindingError | |
| CTypeFlags | |
| Cpreprocessor.type_inference_mixin.TypeInferenceMixin | |
| Cpreprocessor.Preprocessor | |
| Cuchar1 | |
| Cuchar3 | |
| Csmt_solver_baset::uf_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) |
| Cuint1 | |
| Culong1 | |
| Culong3 | |
| Culonglong1 | |
| Culonglong3 | |
| Cunderlying_type_< T, bool > | |
| Cunderlying_type_< T, false > | |
| Ctyping.Union | |
| Cpreprocessor.unittest_mixin.UnittestMixin | |
| Cpreprocessor.Preprocessor | |
| Cunsigned_union_find | |
| 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_interface | |
| Cutf8_reader< T > | |
| Cvalue< typename > | |
| 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_setst | |
| Candersent | |
| Cvalue_set_analysist | |
| Cvalue_sett | |
| Cvalue_traits_base_selector< T, bool > | |
| Cvalue_traits_base_selector< T, true > | |
| Crenaming::level2t::valuet | |
| Cvar_assignment_info | |
| Cpreprocessor.vararg_mixin.VarargMixin | |
| Cpreprocessor.Preprocessor | |
| CVarDecl | |
| CVariableUses | |
| Cvart | |
| Cvsa_not_implemented_exception | |
| Cw_guardst | |
| Cwaypoint | |
| Cbmct::witness_recordt | One enumerated witness for a failing property |
| Cxmlt | |
| CXortor< constant_type > | |
| Cyaml_parser | |
| CYamlPropertyParser | |
| Cyamlt | |
1.15.0