| C__CPROVER_jsa_abstract_heap | |
| C__CPROVER_jsa_abstract_node | Abstract nodes may assume any of a set of pre-defined values (value_ref to abstract_ranget) |
| C__CPROVER_jsa_abstract_range | Set of pre-defined, possible values for abstract nodes |
| C__CPROVER_jsa_concrete_node | Concrete node with explicit value |
| C__CPROVER_jsa_iterator | Iterators point to a node and give the relative index within that node |
| C__CPROVER_pipet | |
| Cpartial_order_concurrencyt::a_rect | |
| Cacceleratet | |
| Cacceleration_utilst | |
| Clinkingt::adjust_type_infot | |
| ▶Cai_baset | |
| ▶Cait< domainT > | |
| Cconcurrency_aware_ait< domainT > | |
| ▶Cait< constant_propagator_domaint > | |
| Cconstant_propagator_ait | |
| ▶Cait< custom_bitvector_domaint > | |
| Ccustom_bitvector_analysist | |
| ▶Cait< dep_graph_domaint > | |
| Cdependence_grapht | |
| ▶Cait< escape_domaint > | |
| Cescape_analysist | |
| ▶Cait< global_may_alias_domaint > | |
| Cglobal_may_alias_analysist | |
| Cait< interval_domaint > | |
| ▶Cait< invariant_set_domaint > | |
| Cinvariant_propagationt | |
| ▶Cait< rd_range_domaint > | |
| ▶Cconcurrency_aware_ait< rd_range_domaint > | |
| Creaching_definitions_analysist | |
| Cait< uninitialized_domaint > | |
| ▶Cai_domain_baset | |
| Cconstant_propagator_domaint | |
| Ccustom_bitvector_domaint | |
| Cdep_graph_domaint | |
| Cescape_domaint | |
| Cglobal_may_alias_domaint | |
| Cinterval_domaint | |
| Cinvariant_set_domaint | |
| Cis_threaded_domaint | |
| Crd_range_domaint | |
| Cuninitialized_domaint | |
| Caig_nodet | |
| ▶Caigt | |
| Caig_plus_constraintst | |
| Cjava_bytecode_parse_treet::annotationt | |
| Cansi_c_identifiert | |
| Cansi_c_parse_treet | |
| Cansi_c_scopet | |
| Cconfigt::ansi_ct | |
| Cbv_refinementt::approximationt | |
| Cgoto_cc_cmdlinet::argt | |
| Carrayst::array_equalityt | |
| Cautomatont | |
| Cbase_type_eqt | |
| Cbasic_blockst | |
| ▶Cstd::basic_string< Char > | STL class |
| ▶Cstd::string | STL class |
| Clispsymbolt | |
| Cbdd_exprt | TO_BE_DOCUMENTED |
| Cjava_bytecode_convert_methodt::block_tree_nodet | |
| Cboolbv_mapt | |
| Cboolbv_widtht | |
| Cgoto_convertt::break_continue_targetst | |
| Cgoto_convertt::break_switch_targetst | |
| Cbv_arithmetict | |
| Cbv_spect | |
| Cbv_utilst | |
| Cbytecode_infot | |
| Cjava_bytecode_parsert::bytecodet | |
| Cc_qualifierst | |
| Cc_sizeoft | |
| Cc_storage_spect | |
| ▶Cc_typecastt | |
| Ccpp_typecastt | |
| Ccall_grapht | |
| Ccheck_call_sequencet::call_stack_entryt | |
| Cgoto_program2codet::caset | |
| Ccfg_dominators_templatet< P, T, post_dom > | |
| Ccfg_dominators_templatet< const goto_programt, goto_programt::const_targett, false > | |
| Ccfg_dominators_templatet< goto_programt, goto_programt::targett, false > | |
| Ccfg_dominators_templatet< P, T, false > | |
| Cfull_slicert::cfg_nodet | |
| Cinstrumentert::cfg_visitort | |
| Cshared_bufferst::cfg_visitort | |
| Cchange_impactt | |
| Ccheck_call_sequencet | |
| Cci_lazy_methodst | |
| Cclass_hierarchyt | |
| Cjava_bytecode_parse_treet::classt | |
| Cclauset | |
| Cescape_domaint::cleanupt | |
| ▶Ccmdlinet | |
| ▶Cgoto_cc_cmdlinet | |
| Carmcc_cmdlinet | |
| Cas86_cmdlinet | |
| Cas_cmdlinet | |
| Cbcc_cmdlinet | |
| Cgcc_cmdlinet | |
| Cld_cmdlinet | |
| Cms_cl_cmdlinet | |
| Ccode_contractst | |
| Cconcurrency_instrumentationt | |
| Ccone_of_influencet | |
| Cconfigt | Globally accessible architectural configuration |
| ▶Cconst_expr_visitort | |
| Cfind_index_visitort | |
| Cfind_qvar_visitort | |
| Cconst_function_pointer_propagationt | |
| Cconst_graph_visitort | |
| Cconst_target_hash_templatet< codeT, guardT > | |
| Cprop_conv_storet::constraintst | |
| Cprop_conv_storet::constraintt | |
| Cjava_bytecode_convert_methodt::converted_instructiont | |
| Ccounterexample_beautificationt | |
| Cgoto_program_coverage_recordt::coverage_conditiont | |
| Csymex_coveraget::coverage_infot | |
| Cgoto_program_coverage_recordt::coverage_linet | |
| ▶Ccoverage_recordt | |
| Cgoto_program_coverage_recordt | |
| Ccpp_convert_typet | |
| Ccpp_declarator_convertert | |
| ▶Ccpp_idt | |
| ▶Ccpp_scopet | |
| Ccpp_root_scopet | |
| Ccpp_parse_treet | |
| Ccpp_save_scopet | |
| Ccpp_saved_template_mapt | |
| Ccpp_scopest | |
| Ccpp_token_buffert | |
| Ccpp_tokent | |
| Ccpp_typecheck_fargst | |
| Ccpp_typecheck_resolvet | |
| Cconfigt::cppt | |
| Ccprover_library_entryt | |
| ▶Ccvc_temp_filet | |
| Ccvc_dect | |
| Ccycles_visitort | |
| Cdata | |
| Cdatat | |
| Cevent_grapht::critical_cyclet::delayt | |
| Csharing_mapt< keyT, valueT, hashT, predT >::delta_view_itemt | |
| Cdep_edget | |
| ▶Cdereference_callbackt | TO_BE_DOCUMENTED |
| Cgoto_program_dereferencet | |
| Csymex_dereference_statet | |
| Cdereferencet | TO_BE_DOCUMENTED |
| Cdesignatort | |
| Cdirtyt | |
| Cdocument_propertiest::doc_claimt | |
| Cdocument_propertiest | |
| Cdoes_remove_constt | |
| ▶Cdomain_baset | |
| Cvalue_set_domaint | |
| Cdott | |
| ▶Cdplib_temp_filet | |
| Cdplib_dect | |
| Cdstring_hash | |
| Cdstringt | |
| Cirept::dt | |
| Csharing_nodet< keyT, valueT, predT, no_sharing >::dt | |
| Cdump_ct | |
| Cjava_bytecode_parse_treet::annotationt::element_value_pairt | |
| CElf32_Ehdr | |
| CElf32_Shdr | |
| CElf64_Ehdr | |
| CElf64_Shdr | |
| Celf_readert | |
| Cempty_cfg_nodet | |
| Cempty_edget | |
| Cendianness_mapt | Maps a big-endian offset to a little-endian offset |
| Cjava_class_loadert::jar_map_entryt::entryt | |
| Cvalue_sett::entryt | |
| Cvalue_set_fit::entryt | |
| Cvalue_set_fivrt::entryt | |
| Cvalue_set_fivrnst::entryt | |
| Cboolbv_widtht::entryt | |
| Cinv_object_storet::entryt | |
| Csatcheck_smvsat_interpolatort::entryt | |
| Crw_set_baset::entryt | |
| Cclass_hierarchyt::entryt | |
| Cdesignatort::entryt | |
| Cprintf_formattert::eol_exceptiont | |
| Cevent_grapht | |
| ▶Cstd::exception | STL class |
| ▶Cerror_baset | |
| Cerror_streamt | |
| ▶Cstd::logic_error | STL class |
| ▶Cinvariant_failedt | A logic error, augmented with a distinguished field to hold a backtrace |
| Cbad_cast_exceptiont | |
| Cnullptr_exceptiont | |
| Cjava_bytecode_parse_treet::methodt::exceptiont | |
| ▶Cexpr2ct | |
| Cexpr2cppt | |
| Cexpr2javat | |
| Cexpr2jsilt | |
| ▶Cexpr_visitort | |
| Csmt2_convt::let_visitort | |
| ▶Cfence_insertert | |
| Cfence_assert_insertert | |
| Cfence_user_def_insertert | |
| Cfile | |
| ▶Cfine_timet | |
| Cabsolute_timet | |
| Ctime_periodt | |
| Cfixedbv_spect | |
| Cfixedbvt | |
| Clocal_bitvector_analysist::flagst | |
| Cfloat_bvt | |
| ▶Cfloat_utilst | |
| Cfloat_approximationt | |
| ▶Cflow_insensitive_abstract_domain_baset | |
| Cvalue_set_domain_fit | |
| Cvalue_set_domain_fivrnst | |
| Cvalue_set_domain_fivrt | |
| ▶Cflow_insensitive_analysis_baset | |
| Cflow_insensitive_analysist< T > | |
| ▶Cflow_insensitive_analysist< value_set_domain_fit > | |
| Cvalue_set_analysis_fit | |
| ▶Cflow_insensitive_analysist< value_set_domain_fivrnst > | |
| Cvalue_set_analysis_fivrnst | |
| ▶Cflow_insensitive_analysist< value_set_domain_fivrt > | |
| Cvalue_set_analysis_fivrt | |
| ▶Cformat_spect | |
| Cformat_constantt | |
| Cformat_tokent | |
| Cpath_symex_statet::framet | |
| Cgoto_symex_statet::framet | |
| Cfull_slicert | |
| Clocst::function_entryt | |
| Cfunctionst::function_infot | |
| Cfunction_modifiest | |
| Cfunctionst | |
| Cremove_virtual_functionst::functiont | |
| Ccover_goalst::goalt | |
| Cbmc_all_propertiest::goalt | |
| Cbmc_covert::goalt | |
| Cgoto_checkt | |
| Cgoto_function_templatet< bodyT > | |
| Cgoto_functions_templatet< bodyT > | |
| ▶Cgoto_functions_templatet< goto_programt > | |
| Cgoto_functionst | |
| Cgoto_inlinet::goto_inline_logt::goto_inline_log_infot | |
| Cgoto_inlinet::goto_inline_logt | |
| Cgoto_modelt | |
| Cgoto_program2codet | |
| Cgoto_program_templatet< codeT, guardT > | A generic container class for the GOTO intermediate representation of one function |
| ▶Cgoto_program_templatet< codet, exprt > | |
| ▶Cgoto_programt | A specialization of goto_program_templatet over goto programs in which instructions have codet type |
| Cscratch_programt | |
| Cgoto_symex_statet::goto_statet | |
| Cgoto_symex_statet | |
| ▶Cgoto_symext | The main class for the forward symbolic simulator |
| Csymex_bmct | |
| Cgoto_trace_stept | TO_BE_DOCUMENTED |
| Cgoto_tracet | TO_BE_DOCUMENTED |
| Cgoto_unwindt | |
| ▶Cevent_grapht::graph_explorert | |
| Cevent_grapht::graph_conc_explorert | |
| Cevent_grapht::graph_pensieve_explorert | |
| ▶Cgraph_nodet< E > | This class represents a node in a directed graph |
| Cvisited_nodet< E > | A node type with an extra bit |
| ▶Cgraph_nodet< dep_edget > | |
| Cdep_nodet | |
| ▶Cgraph_nodet< empty_edget > | |
| Cabstract_eventt | |
| Ccfg_base_nodet< T, I > | |
| ▶Cgraph_nodet< xml_edget > | |
| Cxml_graph_nodet | |
| Cgraphml_witnesst | |
| Cgrapht< N > | A generic directed graph with a parametric node type |
| Cgrapht< abstract_eventt > | |
| ▶Cgrapht< cfg_base_nodet< cfg_nodet, goto_programt::const_targett > > | |
| Ccfg_baset< cfg_nodet > | |
| ▶Cgrapht< cfg_base_nodet< empty_cfg_nodet, goto_programt::const_targett > > | |
| Ccfg_baset< empty_cfg_nodet > | |
| ▶Cgrapht< cfg_base_nodet< nodet, goto_programt::const_targett > > | |
| ▶Ccfg_baset< nodet, const goto_programt, goto_programt::const_targett > | |
| Cprocedure_local_cfg_baset< nodet, const goto_programt, goto_programt::const_targett > | |
| ▶Cgrapht< cfg_base_nodet< nodet, goto_programt::targett > > | |
| ▶Ccfg_baset< nodet, goto_programt, goto_programt::targett > | |
| Cprocedure_local_cfg_baset< nodet, goto_programt, goto_programt::targett > | |
| ▶Cgrapht< cfg_base_nodet< nodet, T > > | |
| ▶Ccfg_baset< nodet, P, T > | |
| Cprocedure_local_cfg_baset< nodet, P, T > | |
| ▶Cgrapht< cfg_base_nodet< slicer_entryt, goto_programt::const_targett > > | |
| Ccfg_baset< slicer_entryt > | |
| ▶Cgrapht< cfg_base_nodet< T, I > > | |
| ▶Ccfg_baset< T, P, I > | A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO program |
| ▶Cconcurrent_cfg_baset< T, P, I > | |
| Cprocedure_local_concurrent_cfg_baset< T, P, I > | |
| ▶Cprocedure_local_cfg_baset< T, P, I > | |
| Cprocedure_local_concurrent_cfg_baset< T, P, I > | |
| ▶Cgrapht< cfg_base_nodet< T, unsigned > > | |
| Cprocedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, unsigned > | |
| ▶Cgrapht< dep_nodet > | |
| Cdependence_grapht | |
| ▶Cgrapht< xml_graph_nodet > | |
| Cgraphmlt | |
| Cgoto_convertt::guarded_gotot | |
| Chavoc_loopst | |
| Cjava_bytecode_convert_methodt::holet | |
| Ccvc_convt::identifiert | |
| Cdplib_convt::identifiert | |
| Csmt1_convt::identifiert | |
| Csmt2_convt::identifiert | |
| Cidentifiert | |
| Cieee_float_spect | |
| Cieee_floatt | |
| Cilpt | |
| Cinflate_state | |
| Cinode | |
| Cbmc_covert::goalt::instancet | |
| Ccpp_typecheckt::instantiation_levelt | |
| Ccpp_typecheckt::instantiationt | |
| Cjava_bytecode_parse_treet::instructiont | |
| Cgoto_program_templatet< codeT, guardT >::instructiont | This class represents an instruction in the GOTO intermediate representation |
| ▶Cinstrumentert | |
| Cinstrumenter_pensievet | |
| Cinterpretert | |
| Cinterval_templatet< T > | |
| Cinv_object_storet | |
| Cinvariant_sett | |
| ▶Cstd::ios_base | STL class |
| ▶Cstd::basic_ios< Char > | STL class |
| ▶Cstd::basic_ostream< Char > | STL class |
| ▶Cstd::basic_ostringstream< Char > | STL class |
| ▶Cstd::ostringstream | STL class |
| Cerror_streamt | |
| Cmessaget::mstreamt | |
| ▶Ciostream | |
| Cpipe_streamt | |
| Cxml_irep_convertt::irep_content_eq | |
| Cirep_full_eq | |
| Cxml_irep_convertt::irep_full_hash | |
| Cirep_full_hash | |
| Cirep_hash | |
| ▶Cirep_hash_container_baset | |
| Cirep_full_hash_containert | |
| Cirep_hash_containert | |
| Cirep_serializationt | |
| Cxml_irep_convertt::ireps_containert | |
| Cirep_serializationt::ireps_containert | |
| ▶Cirept | Base class for tree-like data structures with sharing |
| Cc_enum_typet::c_enum_membert | |
| Ccpp_itemt | |
| Ccpp_member_spect | |
| Ccpp_namet | |
| Ccpp_namet::namet | |
| Ccpp_storage_spect | |
| ▶Ccpp_template_args_baset | |
| Ccpp_template_args_non_tct | |
| Ccpp_template_args_tct | |
| Ccpp_usingt | |
| ▶Cexprt | Base class for all expressions |
| Cansi_c_declarationt | |
| Cansi_c_declaratort | |
| Carray_exprt | Array constructor from list of elements |
| ▶Cbinary_exprt | A generic base class for binary expressions |
| ▶Cbinary_predicate_exprt | A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly two arguments |
| ▶Cbinary_relation_exprt | A generic base class for relations, i.e., binary predicates |
| Cequal_exprt | Equality |
| Cieee_float_equal_exprt | IEEE-floating-point equality |
| Cieee_float_notequal_exprt | IEEE floating-point disequality |
| Cnotequal_exprt | Inequality |
| Cextractbit_exprt | Extracts a single bit of a bit-vector operand |
| Ccomplex_exprt | Complex constructor from a pair of numbers |
| Cdiv_exprt | Division (integer and real) |
| Cfactorial_power_exprt | Falling factorial power |
| Cfloatbv_typecast_exprt | Semantic type conversion from/to floating-point formats |
| Cimplies_exprt | Boolean implication |
| Cminus_exprt | Binary minus |
| Cmod_exprt | Binary modulo |
| Cpower_exprt | Exponentiation |
| Crem_exprt | Remainder of division |
| Creplication_exprt | Bit-vector replication |
| ▶Cshift_exprt | A base class for shift operators |
| Cashr_exprt | Arithmetic right shift |
| Clshr_exprt | Logical right shift |
| Cshl_exprt | Left shift |
| ▶Cbyte_extract_exprt | TO_BE_DOCUMENTED |
| Cbyte_extract_big_endian_exprt | TO_BE_DOCUMENTED |
| Cbyte_extract_little_endian_exprt | TO_BE_DOCUMENTED |
| ▶Cbyte_update_exprt | TO_BE_DOCUMENTED |
| Cbyte_update_big_endian_exprt | TO_BE_DOCUMENTED |
| Cbyte_update_little_endian_exprt | TO_BE_DOCUMENTED |
| Ccode_typet::parametert | |
| ▶Ccodet | A statement in a programming language |
| Ccode_asmt | An inline assembler statement |
| Ccode_assertt | An assertion |
| Ccode_assignt | Assignment |
| Ccode_assumet | An assumption |
| Ccode_blockt | Sequential composition |
| Ccode_breakt | A break for ‘for’ and ‘while’ loops |
| Ccode_continuet | A continue for ‘for’ and ‘while’ loops |
| Ccode_deadt | A removal of a local variable |
| Ccode_declt | A declaration of a local variable |
| Ccode_dowhilet | A ‘do while’ instruction |
| Ccode_expressiont | An expression statement |
| Ccode_fort | A ‘for’ instruction |
| Ccode_function_callt | A function call |
| Ccode_gotot | A ‘goto’ instruction |
| Ccode_ifthenelset | An if-then-else |
| Ccode_labelt | A label for branch targets |
| Ccode_returnt | Return from a function |
| Ccode_skipt | Skip |
| Ccode_switch_caset | A switch-case |
| Ccode_switcht | A ‘switch’ instruction |
| Ccode_try_catcht | A try/catch block |
| Ccode_whilet | A ‘while’ instruction |
| Cconcatenation_exprt | Concatenation of bit-vector operands |
| ▶Cconstant_exprt | A constant literal expression |
| Cfalse_exprt | The boolean constant false |
| Cnull_pointer_exprt | The null pointer constant |
| Ctrue_exprt | The boolean constant true |
| Ccpp_declarationt | |
| Ccpp_declaratort | |
| Ccpp_linkage_spect | |
| Ccpp_namespace_spect | |
| Ccpp_static_assertt | |
| Cdereference_exprt | Operator to dereference a pointer |
| Cdynamic_object_exprt | TO_BE_DOCUMENTED |
| Cexists_exprt | An exists expression |
| Cextractbits_exprt | Extracts a sub-range of a bit-vector operand |
| Cforall_exprt | A forall expression |
| Cfunction_application_exprt | Application of (mathematical) function |
| Cguardt | |
| Cieee_float_op_exprt | IEEE floating-point operations |
| Cif_exprt | The trinary if-then-else operator |
| Cindex_designatort | |
| Cindex_exprt | Array index operator |
| Cinfinity_exprt | An expression denoting infinity |
| Cjsil_declarationt | |
| Clet_exprt | A let expression |
| Cmember_designatort | |
| Cmember_exprt | Extract member of struct or union |
| ▶Cmulti_ary_exprt | A generic base class for multi-ary expressions |
| Cand_exprt | Boolean AND |
| Cbitand_exprt | Bit-wise AND |
| Cbitor_exprt | Bit-wise OR |
| Cbitxor_exprt | Bit-wise XOR |
| Cmult_exprt | Binary multiplication |
| Cor_exprt | Boolean OR |
| Cplus_exprt | The plus expression |
| Cnil_exprt | The NIL expression |
| Cnot_exprt | Boolean negation |
| Cobject_descriptor_exprt | Split an expression into a base object and a (byte) offset |
| ▶Cpredicate_exprt | A generic base class for expressions that are predicates, i.e., boolean-typed |
| Cliteral_exprt | |
| ▶Cside_effect_exprt | An expression containing a side effect |
| Cside_effect_expr_catcht | A side effect that pushes/pops a catch handler |
| Cside_effect_expr_function_callt | A function call side effect |
| Cside_effect_expr_nondett | A side effect that returns a non-deterministically chosen value |
| Cside_effect_expr_throwt | A side effect that throws an exception |
| Csmt2_convt::smt2_symbolt | |
| Cstring_constantt | |
| Cstring_constraintt | |
| Cstring_not_contains_constraintt | |
| ▶Cstruct_exprt | Struct constructor from list of elements |
| Cstring_exprt | |
| Cstruct_union_typet::componentt | |
| ▶Csymbol_exprt | Expression to hold a symbol (variable) |
| Cdecorated_symbol_exprt | Expression to hold a symbol (variable) |
| Cssa_exprt | Expression providing an SSA-renamed symbol of expressions |
| Ctemplate_parametert | |
| Ctranst | A transition system, consisting of state invariant, initial state predicate, and transition predicate |
| Ctype_exprt | An expression denoting a type |
| Ctypecast_exprt | Semantic type conversion |
| ▶Cunary_exprt | Generic base class for unary expressions |
| Cabs_exprt | Absolute value |
| Caddress_of_exprt | Operator to return the address of an object |
| Carray_of_exprt | Array constructor from single element |
| Cbitnot_exprt | Bit-wise negation of bit-vectors |
| Cunary_minus_exprt | The unary minus expression |
| ▶Cunary_predicate_exprt | A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly one argument |
| Cisfinite_exprt | Evaluates to true if the operand is finite |
| Cisinf_exprt | Evaluates to true if the operand is infinite |
| Cisnan_exprt | Evaluates to true if the operand is NaN |
| Cisnormal_exprt | Evaluates to true if the operand is a normal number |
| Csign_exprt | Sign of an expression |
| Cunion_exprt | Union constructor from single element |
| Cupdate_exprt | Operator to update elements in structs and arrays |
| Cvector_exprt | Vector constructor from list of elements |
| Cwith_exprt | Operator to update elements in structs and arrays |
| Cmerged_irept | |
| Csource_locationt | |
| Cto_be_merged_irept | |
| ▶Ctypet | The type of an expression |
| Cbool_typet | The proper Booleans |
| ▶Ccode_typet | Base type of functions |
| Cjsil_builtin_code_typet | |
| Cjsil_spec_code_typet | |
| Ccpp_enum_typet | |
| ▶Cempty_typet | The empty type |
| Cvoid_typet | The void type |
| Cenumeration_typet | A generic enumeration type (not to be confused with C enums) |
| Cinteger_typet | Unbounded, signed integers |
| Cnatural_typet | Natural numbers (which include zero) |
| Cnil_typet | The NIL type |
| Crange_typet | A type for subranges of integers |
| Crational_typet | Unbounded, signed rational numbers |
| Creal_typet | Unbounded, signed real numbers |
| Cstring_typet | TO_BE_DOCUMENTED |
| ▶Cstruct_union_typet | Base type of C structs and unions, and C++ classes |
| ▶Cstruct_typet | Structure type |
| Cclass_typet | C++ class type |
| Crefined_string_typet | |
| ▶Cunion_typet | The union type |
| Cjsil_union_typet | |
| Csymbol_typet | A reference into the symbol table |
| ▶Ctag_typet | A generic tag-based type |
| Cc_enum_tag_typet | An enum tag type |
| Cstruct_tag_typet | A struct tag type |
| Cunion_tag_typet | A union tag type |
| Ctemplate_typet | |
| Ctype_with_subtypest | |
| ▶Ctype_with_subtypet | |
| Carray_typet | Arrays with given size |
| ▶Cbitvector_typet | Base class of bitvector types |
| Cbv_typet | Fixed-width bit-vector without numerical interpretation |
| Cc_bit_field_typet | Type for c bit fields |
| Cc_bool_typet | The C/C++ Booleans |
| Cfixedbv_typet | Fixed-width bit-vector with signed fixed-point interpretation |
| Cfloatbv_typet | Fixed-width bit-vector with IEEE floating-point interpretation |
| ▶Cpointer_typet | The pointer type |
| Creference_typet | The reference type |
| Csignedbv_typet | Fixed-width bit-vector with two's complement interpretation |
| Cunsignedbv_typet | Fixed-width bit-vector with unsigned binary interpretation |
| Cc_enum_typet | The type of C enums |
| Ccomplex_typet | Complex numbers made of pair of given subtype |
| Cincomplete_array_typet | Arrays without size |
| Cvector_typet | A constant-size array type |
| Cis_name_equalt | |
| Cis_predecessor_oft | |
| Cis_threadedt | |
| Cis_virtual_name_equalt | |
| Cjava_class_loadert::jar_map_entryt | |
| Cjava_bytecode_parse_treet | |
| Cjava_bytecode_vtable_factoryt | |
| Cjava_object_factoryt | |
| Cconfigt::javat | |
| Cjsil_parse_treet | |
| Cjson_irept | |
| ▶Cjsont | |
| Cjson_arrayt | |
| Cjson_falset | |
| Cjson_nullt | |
| Cjson_numbert | |
| Cjson_objectt | |
| Cjson_stringt | |
| Cjson_truet | |
| Ck_inductiont | |
| Clanguage_entryt | |
| Clanguage_filet | |
| Clanguage_modulet | |
| Clanguagest | |
| Carrayst::lazy_constraintt | |
| Cgoto_convertt::leave_targett | |
| Clinear_recurrencet | |
| Cdocument_propertiest::linet | |
| ▶Cstd::list< T > | STL class |
| Cevent_grapht::critical_cyclet | |
| Cformat_token_listt | |
| Crange_domaint | |
| Cliteralt | |
| Cpath_searcht::loc_datat | |
| Clocal_bitvector_analysist::loc_infot | |
| Clocal_may_aliast::loc_infot | |
| Cloc_reft | |
| Clocal_bitvector_analysist | |
| Clocal_cfgt | |
| Clocal_may_alias_factoryt | |
| Clocal_may_aliast | |
| Cjava_bytecode_convert_methodt::local_variable_with_holest | |
| Cjava_bytecode_parse_treet::methodt::local_variablet | |
| Clocalst | |
| Clocst | |
| Cloct | |
| ▶Cloop_accelerationt | |
| Cdisjunctive_polynomial_accelerationt | |
| Cenumerating_loop_accelerationt | |
| Cgoto_symex_statet::framet::loop_infot | |
| Cfault_localizationt::lpointt | |
| Cmain_function_resultt | |
| ▶Cstd::map< K, T > | STL class |
| Ccfg_baset< T, P, I >::entry_mapt | |
| Cvalue_set_fit::object_map_dt | |
| Cvalue_sett::object_map_dt | |
| Cboolbv_mapt::map_bitt | |
| Cboolbv_mapt::map_entryt | |
| Ccpp_typecheck_resolvet::matcht | |
| Cmember_offset_iterator | |
| ▶Cjava_bytecode_parse_treet::membert | |
| Cjava_bytecode_parse_treet::fieldt | |
| Cjava_bytecode_parse_treet::methodt | |
| Cboolbv_widtht::membert | |
| Cinterpretert::memory_cellt | |
| Cmerge_full_irept | |
| Cmerge_irept | |
| Cmerged_irep_hash | |
| Cmerged_irepst | |
| ▶Cmessage_handlert | |
| Cnull_message_handlert | |
| ▶Cstream_message_handlert | |
| Ccerr_message_handlert | |
| Ccout_message_handlert | |
| ▶Cui_message_handlert | |
| Cconsole_message_handlert | |
| Cgcc_message_handlert | |
| ▶Cmessaget | |
| Cansi_c_convert_typet | |
| ▶Cbmc_all_propertiest | |
| Cfault_localizationt | |
| Cbmc_covert | |
| Cbv_minimizet | |
| Ccbmc_solverst | |
| Ccharacter_refine_preprocesst | |
| Ccover_goalst | Try to cover some given set of goals incrementally |
| ▶Cdecision_proceduret | |
| ▶Cprop_convt | |
| ▶Ccvc_convt | |
| Ccvc_dect | |
| ▶Cdplib_convt | |
| Cdplib_dect | |
| ▶Cprop_conv_solvert | TO_BE_DOCUMENTED |
| ▶Cequalityt | |
| ▶Carrayst | |
| ▶Cboolbvt | |
| ▶Cbv_pointerst | |
| ▶Cbv_cbmct | |
| Ccbmc_dimacst | |
| Cbv_minimizing_dect | |
| ▶Cbv_refinementt | |
| Cstring_refinementt | |
| Cprop_conv_storet | |
| ▶Csmt1_convt | |
| Csmt1_dect | Decision procedure interface for various SMT 1.x solvers |
| ▶Csmt2_convt | |
| Csmt2_dect | Decision procedure interface for various SMT 2.x solvers |
| ▶Cgoto_cc_modet | |
| Carmcc_modet | |
| Cas_modet | |
| Ccw_modet | |
| Cgcc_modet | |
| Cms_cl_modet | |
| ▶Cgoto_convertt | |
| Cgoto_convert_functionst | |
| ▶Cgoto_difft | |
| Csyntactic_difft | |
| Cgoto_inlinet | |
| Cjar_filet | |
| Cjar_poolt | |
| Cjava_bytecode_convert_classt | |
| Cjava_bytecode_convert_methodt | |
| Cjava_class_loader_limitt | |
| Cjava_class_loadert | |
| Cjsil_convertt | |
| Clanguage_filest | |
| ▶Clanguage_uit | |
| Ccbmc_parse_optionst | |
| Cclobber_parse_optionst | |
| Ccompilet | |
| Cgoto_analyzer_parse_optionst | |
| ▶Cgoto_diff_languagest | |
| Cgoto_diff_parse_optionst | |
| Cgoto_fence_inserter_parse_optionst | |
| Cgoto_instrument_parse_optionst | |
| Csymex_parse_optionst | |
| ▶Clanguaget | |
| Cansi_c_languaget | |
| Ccpp_languaget | |
| Cjava_bytecode_languaget | |
| Cjsil_languaget | |
| ▶Cparsert | |
| Cansi_c_parsert | |
| Cassembler_parsert | |
| Ccpp_parsert | |
| Cjava_bytecode_parsert | |
| Cjsil_parsert | |
| Cjson_parsert | |
| Cmm_parsert | |
| Cxml_parsert | |
| ▶Cpartial_order_concurrencyt | |
| ▶Cmemory_model_baset | |
| ▶Cmemory_model_sct | |
| ▶Cmemory_model_tsot | |
| Cmemory_model_psot | |
| Cpreprocessort | |
| Cprop_minimizet | Computes a satisfying assignment of minimal cost according to a const function using incremental SAT |
| Cproperty_checkert | |
| ▶Cpropt | TO_BE_DOCUMENTED |
| ▶Caig_prop_baset | |
| ▶Caig_prop_constraintt | |
| Caig_prop_solvert | |
| ▶Ccnft | |
| ▶Ccnf_clause_listt | |
| Ccnf_clause_list_assignmentt | |
| ▶Cdimacs_cnft | |
| Cpbs_dimacs_cnft | |
| ▶Cqdimacs_cnft | |
| Cqbf_quantort | |
| Cqbf_qubet | |
| Cqbf_skizzot | |
| Cqbf_squolemt | |
| ▶Cqdimacs_coret | |
| ▶Cqbf_bdd_certificatet | |
| Cqbf_bdd_coret | |
| Cqbf_skizzo_coret | |
| Cqbf_qube_coret | |
| Cqbf_squolem_coret | |
| Csatcheck_limmatt | |
| Csatcheck_zcoret | |
| ▶Csatcheck_zchaff_baset | |
| Csatcheck_zchafft | |
| ▶Ccnf_solvert | |
| ▶Csatcheck_booleforce_baset | |
| Csatcheck_booleforce_coret | |
| Csatcheck_booleforcet | |
| Csatcheck_glucose_baset< T > | |
| ▶Csatcheck_glucose_baset< Glucose::SimpSolver > | |
| Csatcheck_glucose_simplifiert | |
| ▶Csatcheck_glucose_baset< Glucose::Solver > | |
| Csatcheck_glucose_no_simplifiert | |
| Csatcheck_lingelingt | |
| ▶Csatcheck_minisat1_baset | |
| ▶Csatcheck_minisat1t | |
| ▶Csatcheck_minisat1_prooft | |
| Csatcheck_minisat1_coret | |
| Csatcheck_minisat2_baset< T > | |
| ▶Csatcheck_minisat2_baset< Minisat::SimpSolver > | |
| Csatcheck_minisat_simplifiert | |
| ▶Csatcheck_minisat2_baset< Minisat::Solver > | |
| Csatcheck_minisat_no_simplifiert | |
| Csatcheck_picosatt | |
| Csatcheck_precosatt | |
| ▶Csatcheck_smvsatt | |
| Csatcheck_smvsat_coret | |
| Csatcheck_smvsat_interpolatort | |
| Cdimacs_cnf_dumpt | |
| Ccvc_propt | |
| Cdplib_propt | |
| Cprop_wrappert | |
| Csmt1_propt | |
| Csmt2_propt | |
| Cremove_const_function_pointerst | |
| Cremove_function_pointerst | |
| ▶Csafety_checkert | |
| Cbmct | |
| Cpath_searcht | |
| Cstatic_analyzert | |
| Cstring_abstractiont | |
| Cstring_instrumentationt | |
| Csymex_bmct | |
| Ctaint_analysist | |
| ▶Ctypecheckt | |
| ▶Cc_typecheck_baset | |
| Cansi_c_typecheckt | |
| Ccpp_typecheckt | |
| Cjava_bytecode_typecheckt | |
| Cjsil_typecheckt | |
| Clinkingt | |
| Czero_initializert | |
| Ccpp_typecheckt::method_bodyt | |
| Cmini_bdd_applyt | |
| Cmini_bdd_mgrt | |
| Cmini_bdd_nodet | |
| Cmini_bddt | |
| Cmip_vart | |
| Cmm2cppt | |
| Cmonomialt | |
| ▶Cstd::multimap< K, T > | STL class |
| Cguarded_range_domaint | |
| Cmz_stream_s | |
| Cmz_zip_archive | |
| Cmz_zip_archive_file_stat | |
| Cmz_zip_array | |
| Cmz_zip_internal_state_tag | |
| Cmz_zip_writer_add_state | |
| ▶Cnamespace_baset | |
| ▶Cnamespacet | TO_BE_DOCUMENTED |
| Cc_typecheck_baset | |
| Cmulti_namespacet | |
| Cnatural_loops_templatet< P, T > | |
| ▶Cnatural_loops_templatet< const goto_programt, goto_programt::const_targett > | |
| Cnatural_loopst | |
| Cnatural_loops_templatet< goto_programt, goto_programt::targett > | |
| Cnew_scopet | |
| Cunsigned_union_find::nodet | |
| Ccfg_dominators_templatet< P, T, post_dom >::nodet | |
| Clocal_cfgt::nodet | |
| Cobject_idt | |
| Cvalue_set_fivrt::object_map_dt | |
| Cvalue_set_fivrnst::object_map_dt | |
| Cprop_minimizet::objectivet | |
| Cvalue_sett::objectt | |
| Cvalue_set_fivrnst::objectt | |
| Cvalue_set_fit::objectt | |
| Cvalue_set_fivrt::objectt | |
| ▶Ccover_goalst::observert | |
| Cbmc_all_propertiest | |
| Cbmc_covert | |
| Coperator_entryt | |
| Coptionst | |
| Ccmdlinet::optiont | |
| Cosx_fat_readert | |
| Coverflow_instrumentert | |
| Cparameter_assignmentst | |
| ▶Cparse_options_baset | |
| Ccbmc_parse_optionst | |
| Cclobber_parse_optionst | |
| Cgoto_analyzer_parse_optionst | |
| Cgoto_diff_parse_optionst | |
| Cgoto_fence_inserter_parse_optionst | |
| Cgoto_instrument_parse_optionst | |
| Cmmcc_parse_optionst | |
| Csymex_parse_optionst | |
| CParser | |
| ▶Cpath_accelerationt | |
| Cpolynomial_acceleratort | |
| Cpath_acceleratort | |
| ▶Cpath_enumeratort | |
| Call_paths_enumeratort | |
| Csat_path_enumeratort | |
| Cpath_nodet | |
| Cpath_replayt | |
| Cpath_symex_historyt | |
| Cpath_symex_statet | |
| Cpath_symex_step_reft | |
| Cpath_symex_stept | |
| Cpath_symext | |
| Cpatternt | |
| Cpointer_arithmetict | |
| Cirep_hash_container_baset::pointer_hasht | |
| Cpointer_logict | |
| Cpointer_logict::pointert | |
| Cpoints_tot | |
| Cpolynomial_acceleratort::polynomial_array_assignment | |
| Cacceleration_utilst::polynomial_array_assignmentt | |
| Cpolynomialt | |
| Cjava_bytecode_parsert::pool_entryt | |
| Cpostconditiont | |
| Cbv_pointerst::postponedt | |
| Cpreconditiont | |
| Cprintf_formattert | |
| ▶CProofTraverser | |
| Cminisat_prooft | |
| ▶Cprop_assignmentt | TO_BE_DOCUMENTED |
| Cpropt | TO_BE_DOCUMENTED |
| Cgoto_symex_statet::propagationt | |
| Cpath_searcht::property_entryt | |
| Cproperty_checkert::property_statust | |
| Cboolbvt::quantifiert | |
| Cqdimacs_cnft::quantifiert | |
| ▶Crange_domain_baset | |
| Cguarded_range_domaint | |
| Crange_domaint | |
| Crationalt | |
| Creachability_slicert | |
| Creaching_definitiont | |
| Crecursion_countert | |
| Cref_expr_set_dt | |
| Creference_counting< T > | |
| Creference_counting< object_map_dt > | |
| ▶Creference_counting< ref_expr_set_dt > | |
| Cref_expr_sett | |
| Cremove_asmt | |
| Cremove_exceptionst | |
| Cremove_instanceoft | |
| Cremove_returnst | |
| Cremove_static_init_loopst | |
| Cremove_virtual_functionst | |
| Crename_symbolt | |
| ▶Cgoto_symex_statet::renaming_levelt | |
| Cgoto_symex_statet::level0t | |
| Cgoto_symex_statet::level1t | |
| Cgoto_symex_statet::level2t | |
| ▶Creplace_symbolt | |
| Creplace_symbol_extt | |
| Cresolution_prooft< T > | |
| Cresolution_prooft< clauset > | |
| Crestrictt | |
| Cmini_bdd_mgrt::reverse_keyt | |
| Cfloat_bvt::rounding_mode_bitst | |
| Cfloat_utilst::rounding_mode_bitst | |
| Ctaint_parse_treet::rulet | |
| ▶Crw_range_sett | |
| ▶Crw_range_set_value_sett | |
| Crw_guarded_range_set_value_sett | |
| ▶Crw_set_baset | |
| ▶C_rw_set_loct | |
| Crw_set_loct | |
| Crw_set_with_trackt | |
| Crw_set_functiont | |
| Csafe_pointer< T > | |
| Csafe_pointer< ci_lazy_methodst > | |
| Csaj_tablet | Produce canonical ordering for associative and commutative binary operators |
| Csave_scopet | |
| ▶Cstd::set< K > | STL class |
| Cconst_function_pointer_propagationt::arg_stackt | |
| Cdata_dpt | |
| Cshared_bufferst | |
| Cconcurrency_instrumentationt::shared_vart | |
| Csharing_mapt< keyT, valueT, hashT, predT > | |
| Csharing_nodet< keyT, valueT, predT, no_sharing > | |
| Csharing_nodet< key_type, mapped_type, key_equal > | |
| Cshow_goto_functions_jsont | |
| Cshow_goto_functions_xmlt | |
| ▶Csimple_insertiont | |
| ▶Cfence_all_sharedt | |
| Cfence_all_shared_aegt | |
| Cfence_volatilet | |
| Csimplify_exprt | |
| Creachability_slicert::slicer_entryt | |
| ▶Cslicing_criteriont | |
| Cassert_criteriont | |
| Cproperties_criteriont | |
| ▶Csmt1_temp_filet | |
| Csmt1_dect | Decision procedure interface for various SMT 1.x solvers |
| ▶Csmt2_parsert | |
| Csmt2irept | |
| ▶Csmt2_stringstreamt | |
| Csmt2_dect | Decision procedure interface for various SMT 2.x solvers |
| Csmt2_temp_filet | |
| Ccbmc_solverst::solvert | |
| Csorted_vector< K, bNoDuplicates, Pr, A > | |
| Csymex_targett::sourcet | |
| Csparse_bitvector_analysist< V > | |
| ▶Csparse_bitvector_analysist< reaching_definitiont > | |
| Creaching_definitions_analysist | |
| Csymex_target_equationt::SSA_stept | |
| Cinterpretert::stack_framet | |
| Cjava_bytecode_parse_treet::methodt::stack_map_table_entryt | |
| Ccheck_call_sequencet::state_hash | |
| Ccheck_call_sequencet::statet | |
| ▶Cstatic_analysis_baset | |
| ▶Cstatic_analysist< T > | |
| Cconcurrency_aware_static_analysist< T > | |
| ▶Cstatic_analysist< value_set_domaint > | |
| Cvalue_set_analysist | |
| Cclauset::stept | |
| ▶Cstreambuf | |
| Cfiledescriptor_streambuft | |
| Cstring_constraint_generatort | |
| Cstring_containert | |
| Cstring_hash | |
| Cstring_ptr_hash | |
| Cstring_ptrt | |
| Csubsumed_patht | |
| Csymbol_factoryt | |
| Csymbol_tablet | The symbol table |
| ▶Csymbolt | Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet |
| Cauxiliary_symbolt | Internally generated symbol table entryThis is a symbol generated as part of translation to or modification of the intermediate representation |
| Cparameter_symbolt | Symbol table entry of function parameterThis is a symbol generated as part of type checking |
| Ctype_symbolt | Symbol table entry describing a data typeThis is a symbol generated as part of type checking |
| Csymex_coveraget | |
| Csymex_slice_by_tracet | |
| Csymex_slicet | |
| ▶Csymex_targett | |
| Csymex_target_equationt | |
| ▶CT | |
| Ccfg_base_nodet< T, I > | |
| Creference_counting< T >::dt | |
| Ctaint_parse_treet | |
| Ctarget_to_loc_mapt | |
| Cgoto_convertt::targetst | |
| Cgrapht< N >::tarjant | |
| Ctdefl_compressor | |
| Ctdefl_output_buffer | |
| Ctdefl_sym_freq | |
| ▶Ctemp_dirt | |
| Ctemp_working_dirt | |
| Ctemplate_mapt | |
| Ctemporary_filet | |
| Cmonomialt::termt | |
| Cbmc_covert::testt | |
| Cconcurrency_instrumentationt::thread_local_vart | |
| Cpath_symex_statet::threadt | |
| Cgoto_symex_statet::threadt | |
| Cgoto_convertt::throw_targett | |
| Ctimert | |
| Ctinfl_decompressor_tag | |
| Ctinfl_huff_table | |
| Cto_be_merged_irep_hash | |
| Ctrace_automatont | |
| Ctvt | |
| Cdump_ct::typedef_infot | |
| Cequalityt::typestructt | |
| Cxml_irep_convertt::ul_eq | |
| Cxml_irep_convertt::ul_hash | |
| Cunified_difft | |
| Cuninitializedt | |
| ▶Cfloat_utilst::unpacked_floatt | |
| Cfloat_utilst::biased_floatt | |
| Cfloat_utilst::unbiased_floatt | |
| ▶Cfloat_bvt::unpacked_floatt | |
| Cfloat_bvt::biased_floatt | |
| Cfloat_bvt::unbiased_floatt | |
| Cunsigned_union_find | |
| Cgoto_unwindt::unwind_logt | |
| Cvalue_set_fivrnst::object_map_dt::validity_ranget | |
| Cvalue_set_fivrt::object_map_dt::validity_ranget | |
| Cvalue_set_dereferencet | TO_BE_DOCUMENTED |
| Cvalue_set_fit | |
| Cvalue_set_fivrnst | |
| Cvalue_set_fivrt | |
| ▶Cvalue_setst | |
| Cvalue_set_analysis_fit | |
| Cvalue_set_analysis_fivrnst | |
| Cvalue_set_analysis_fivrt | |
| Cvalue_set_analysist | |
| Cvalue_sett | |
| Cconstant_propagator_domaint::valuest | |
| Cvalue_set_dereferencet::valuet | |
| Csmt1_dect::valuet | |
| Cvar_mapt::var_infot | |
| Cvar_mapt | |
| Cpath_symex_statet::var_statet | |
| Cmini_bdd_mgrt::var_table_entryt | |
| Cjava_bytecode_convert_methodt::variablet | |
| Cshared_bufferst::varst | |
| ▶Cstd::vector< T > | STL class |
| Cexpanding_vectort< T > | |
| Cexpanding_vectort< flagst > | |
| Cexpanding_vectort< path_searcht::loc_datat > | |
| Cexpanding_vectort< variablest > | |
| Chash_numbering< T, hash_fkt > | |
| Chash_numbering< dstringt, dstring_hash > | |
| Chash_numbering< exprt, irep_hash > | |
| Chash_numbering< irep_idt, irep_id_hash > | |
| Chash_numbering< packedt, vector_hasht > | |
| Clispexprt | |
| ▶Cnumbering< T > | |
| Cunion_find< T > | |
| Cnumbering< dstringt > | |
| ▶Cnumbering< exprt > | |
| Cunion_find< exprt > | |
| ▶Cnumbering< irep_idt > | |
| Cunion_find< irep_idt > | |
| Cirep_hash_container_baset::vector_hasht | |
| Ccustom_bitvector_domaint::vectorst | |
| Cjava_bytecode_parse_treet::methodt::verification_type_infot | |
| Cconfigt::verilogt | |
| Cw_guardst | |
| Cxml_edget | |
| Cxml_goto_function_convertt | |
| Cxml_goto_program_convertt | |
| ▶Cxml_interfacet | |
| Ccbmc_parse_optionst | |
| Cxml_irep_convertt | |
| Cxml_parse_treet | |
| Cxml_symbol_convertt | |
| Cxmlt | |
| Cyy_buffer_state | |
| Cyy_trans_info | |
| Cyyalloc | |
| CYYSTYPE | |
1.8.14