cprover
Class Hierarchy

Go to the graphical class hierarchy

This inheritance list is sorted roughly, but not completely, alphabetically:
[detail level 12345678910]
 C__CPROVER_jsa_abstract_heap
 C__CPROVER_jsa_abstract_nodeAbstract nodes may assume any of a set of pre-defined values (value_ref to abstract_ranget)
 C__CPROVER_jsa_abstract_rangeSet of pre-defined, possible values for abstract nodes
 C__CPROVER_jsa_concrete_nodeConcrete node with explicit value
 C__CPROVER_jsa_iteratorIterators 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
 Cai_domain_baset
 Caig_nodet
 Caigt
 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
 Cbdd_exprtTO_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
 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
 Ccode_contractst
 Cconcurrency_instrumentationt
 Ccone_of_influencet
 CconfigtGlobally accessible architectural configuration
 Cconst_expr_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
 Ccpp_convert_typet
 Ccpp_declarator_convertert
 Ccpp_idt
 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
 Ccycles_visitort
 Cdata
 Cdatat
 Cevent_grapht::critical_cyclet::delayt
 Csharing_mapt< keyT, valueT, hashT, predT >::delta_view_itemt
 Cdep_edget
 Cdereference_callbacktTO_BE_DOCUMENTED
 CdereferencetTO_BE_DOCUMENTED
 Cdesignatort
 Cdirtyt
 Cdocument_propertiest::doc_claimt
 Cdocument_propertiest
 Cdoes_remove_constt
 Cdomain_baset
 Cdott
 Cdplib_temp_filet
 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_maptMaps 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::exceptionSTL class
 Cjava_bytecode_parse_treet::methodt::exceptiont
 Cexpr2ct
 Cexpr_visitort
 Cfence_insertert
 Cfile
 Cfine_timet
 Cfixedbv_spect
 Cfixedbvt
 Clocal_bitvector_analysist::flagst
 Cfloat_bvt
 Cfloat_utilst
 Cflow_insensitive_abstract_domain_baset
 Cflow_insensitive_analysis_baset
 Cformat_spect
 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_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_symex_statet::goto_statet
 Cgoto_symex_statet
 Cgoto_symextThe main class for the forward symbolic simulator
 Cgoto_trace_steptTO_BE_DOCUMENTED
 Cgoto_tracetTO_BE_DOCUMENTED
 Cgoto_unwindt
 Cevent_grapht::graph_explorert
 Cgraph_nodet< E >This class represents a node in a directed graph
 Cgraph_nodet< dep_edget >
 Cgraph_nodet< empty_edget >
 Cgraph_nodet< xml_edget >
 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 > >
 Cgrapht< cfg_base_nodet< empty_cfg_nodet, goto_programt::const_targett > >
 Cgrapht< cfg_base_nodet< nodet, goto_programt::const_targett > >
 Cgrapht< cfg_base_nodet< nodet, goto_programt::targett > >
 Cgrapht< cfg_base_nodet< nodet, T > >
 Cgrapht< cfg_base_nodet< slicer_entryt, goto_programt::const_targett > >
 Cgrapht< cfg_base_nodet< T, I > >
 Cgrapht< cfg_base_nodet< T, unsigned > >
 Cgrapht< dep_nodet >
 Cgrapht< xml_graph_nodet >
 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 >::instructiontThis class represents an instruction in the GOTO intermediate representation
 Cinstrumentert
 Cinterpretert
 Cinterval_templatet< T >
 Cinv_object_storet
 Cinvariant_sett
 Cstd::ios_baseSTL class
 Ciostream
 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_serializationt
 Cxml_irep_convertt::ireps_containert
 Cirep_serializationt::ireps_containert
 CireptBase class for tree-like data structures with sharing
 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
 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
 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
 Cgoto_symex_statet::framet::loop_infot
 Cfault_localizationt::lpointt
 Cmain_function_resultt
 Cstd::map< K, T >STL class
 Cboolbv_mapt::map_bitt
 Cboolbv_mapt::map_entryt
 Ccpp_typecheck_resolvet::matcht
 Cmember_offset_iterator
 Cjava_bytecode_parse_treet::membert
 Cboolbv_widtht::membert
 Cinterpretert::memory_cellt
 Cmerge_full_irept
 Cmerge_irept
 Cmerged_irep_hash
 Cmerged_irepst
 Cmessage_handlert
 Cmessaget
 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
 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
 Cnatural_loops_templatet< P, T >
 Cnatural_loops_templatet< const goto_programt, goto_programt::const_targett >
 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
 Coperator_entryt
 Coptionst
 Ccmdlinet::optiont
 Cosx_fat_readert
 Coverflow_instrumentert
 Cparameter_assignmentst
 Cparse_options_baset
 CParser
 Cpath_accelerationt
 Cpath_acceleratort
 Cpath_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
 Cprop_assignmenttTO_BE_DOCUMENTED
 Cgoto_symex_statet::propagationt
 Cpath_searcht::property_entryt
 Cproperty_checkert::property_statust
 Cboolbvt::quantifiert
 Cqdimacs_cnft::quantifiert
 Crange_domain_baset
 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 >
 Cremove_asmt
 Cremove_exceptionst
 Cremove_instanceoft
 Cremove_returnst
 Cremove_static_init_loopst
 Cremove_virtual_functionst
 Crename_symbolt
 Cgoto_symex_statet::renaming_levelt
 Creplace_symbolt
 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_set_baset
 Csafe_pointer< T >
 Csafe_pointer< ci_lazy_methodst >
 Csaj_tabletProduce canonical ordering for associative and commutative binary operators
 Csave_scopet
 Cstd::set< K >STL class
 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
 Csimplify_exprt
 Creachability_slicert::slicer_entryt
 Cslicing_criteriont
 Csmt1_temp_filet
 Csmt2_parsert
 Csmt2_stringstreamt
 Csmt2_temp_filet
 Ccbmc_solverst::solvert
 Csorted_vector< K, bNoDuplicates, Pr, A >
 Csymex_targett::sourcet
 Csparse_bitvector_analysist< V >
 Csparse_bitvector_analysist< reaching_definitiont >
 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
 Cclauset::stept
 Cstreambuf
 Cstring_constraint_generatort
 Cstring_containert
 Cstring_hash
 Cstring_ptr_hash
 Cstring_ptrt
 Csubsumed_patht
 Csymbol_factoryt
 Csymbol_tabletThe symbol table
 CsymboltSymbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet
 Csymex_coveraget
 Csymex_slice_by_tracet
 Csymex_slicet
 Csymex_targett
 CT
 Ctaint_parse_treet
 Ctarget_to_loc_mapt
 Cgoto_convertt::targetst
 Cgrapht< N >::tarjant
 Ctdefl_compressor
 Ctdefl_output_buffer
 Ctdefl_sym_freq
 Ctemp_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_bvt::unpacked_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_dereferencetTO_BE_DOCUMENTED
 Cvalue_set_fit
 Cvalue_set_fivrnst
 Cvalue_set_fivrt
 Cvalue_setst
 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
 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
 Cxml_irep_convertt
 Cxml_parse_treet
 Cxml_symbol_convertt
 Cxmlt
 Cyy_buffer_state
 Cyy_trans_info
 Cyyalloc
 CYYSTYPE