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
 Cabstract_goto_modeltAbstract interface to eager or lazy GOTO models
 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
 Carray_pooltCorrespondance between arrays and pointers string representations
 Cautomatont
 Cbase_type_eqt
 Cstd::basic_string< Char >STL class
 Cbdd_exprtTO_BE_DOCUMENTED
 Ccover_basic_blockst::block_infot
 Cjava_bytecode_convert_methodt::block_tree_nodet
 Cboolbv_mapt
 Cboolbv_widtht
 Cgoto_convertt::break_continue_targetst
 Cgoto_convertt::break_switch_targetst
 Cstring_dependenciest::builtin_function_nodetA builtin function node contains a builtin function call
 Cbv_arithmetict
 Cconfigt::bv_encodingt
 Cbv_spect
 Cbv_utilst
 Cbytecode_infot
 Cjava_bytecode_parsert::bytecodet
 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_methods_neededt
 Cclass_hierarchyt
 Cmethod_bytecodet::class_method_and_bytecodetPair of class id and methodt
 Cjava_bytecode_parse_treet::classt
 Cclauset
 Cescape_domaint::cleanupt
 Ccmdlinet
 Ccode_contractst
 Cconcurrency_instrumentationt
 Ccone_of_influencet
 Cbv_refinementt::configt
 Cstring_refinementt::configt
 CconfigtGlobally accessible architectural configuration
 Cconst_expr_visitort
 Csmall_mapt< T, Ind, Num >::const_iteratorConst iterator
 Cconst_target_hash
 Csmall_mapt< T, Ind, Num >::const_value_iteratorConst value iterator
 Cconversion_dependenciestThis is structure is here to facilitate passing arguments to the conversion functions
 Cci_lazy_methodst::convert_method_resultt
 Cjava_bytecode_convert_methodt::converted_instructiont
 Ccopy_on_write_pointeet< Num >A helper class to store use-counts of copy-on-write objects
 Ccopy_on_writet< T >A utility class for writing types with copy-on-write behaviour (like irep)
 Ccounterexample_beautificationt
 Ccover_blocks_baset
 Ccover_configt
 Ccover_instrumenter_basetBase class for goto program coverage instrumenters
 Ccover_instrumenterstA collection of instrumenters to be run
 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
 Cevent_grapht::critical_cyclet
 Cdata
 Cdata_dpt
 Cdatat
 Cevent_grapht::critical_cyclet::delayt
 Csharing_mapt< keyT, valueT, hashT, equalT >::delta_view_itemt
 Cdep_edget
 Cdepth_iterator_baset< depth_iterator_t >Depth first search iterator base - iterates over supplied expression and all its operands recursively
 Cdepth_iterator_baset< const_depth_iteratort >
 Cdepth_iterator_baset< const_unique_depth_iteratort >
 Cdepth_iterator_baset< depth_iteratort >
 Cdepth_iterator_expr_statetHelper class for depth_iterator_baset
 Cdereference_callbacktTO_BE_DOCUMENTED
 CdereferencetTO_BE_DOCUMENTED
 Cdesignatort
 Cdirtyt
 Cdispatch_table_entryt
 Cdocument_propertiest::doc_claimt
 Cdocument_propertiest
 Cdoes_remove_constt
 Cdomain_baset
 Cdott
 Cdstring_hash
 Cdstringt
 Cirept::dt
 Cdump_ct
 Ccall_grapht::edge_with_callsitestEdge of the directed graph representation of this call graph
 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
 Ccfg_baset< T, P, I >::entry_mapt
 Cvalue_sett::entrytRepresents a row of a value_sett
 Cvalue_set_fit::entryt
 Cvalue_set_fivrt::entryt
 Cvalue_set_fivrnst::entryt
 Cboolbv_widtht::entryt
 Cinv_object_storet::entryt
 Crw_set_baset::entryt
 Cclass_hierarchyt::entryt
 Cdesignatort::entryt
 Cprintf_formattert::eol_exceptiont
 Cequation_symbol_mappingtMaps equation to expressions contained in them and conversely expressions to equations that contain them
 Cevent_grapht
 Cstd::exceptionSTL class
 Cjava_bytecode_parse_treet::methodt::exceptiont
 Cexpanding_vectort< T >
 Cexpanding_vectort< variablest >
 Crequire_parse_tree::expected_instructiont
 Crequire_type::expected_type_argumentt
 Cexpr2ct
 Cdetail::expr_dynamic_cast_return_typet< Ret, T >
 Cdetail::expr_try_dynamic_cast_return_typet< Ret, T >
 Cexpr_visitort
 Cfile
 Cfixed_keys_map_wrappert< mapt >
 Cfixedbv_spect
 Cfixedbvt
 Clocal_bitvector_analysist::flagst
 Cfloat_bvt
 Cfloat_utilst
 Cflow_insensitive_abstract_domain_baset
 Cflow_insensitive_analysis_baset
 Cformat_containert< T >The below enables convenient syntax for feeding objects into streams, via stream << format(o)
 Cformat_elementt
 Cstring_constraint_generatort::format_specifiert
 Cformat_spect
 Cformat_textt
 Cformat_tokent
 Cgoto_symex_statet::framet
 CfreertA functor wrapping std::free
 Cfull_slicert
 Cinterpretert::function_assignments_contextt
 Cinterpretert::function_assignmentt
 Cfunction_filterstA collection of function filters to be applied in conjunction
 Cfunction_indicestHelper class that maintains a map from function name to grapht node index and adds nodes to the graph on demand
 Cfunctionst::function_infot
 Cfunction_modifiest
 Cfunctionst
 Cgcc_versiont
 Cgenerate_function_bodiestBase class for replace_function_body implementations
 Cgeneric_parameter_specialization_map_keyst
 Cgoal_filterstA collection of goal filters to be applied in conjunction
 Ccover_goalst::goalt
 Cbmc_all_propertiest::goalt
 Cbmc_covert::goalt
 Cgoto_checkt
 Cgoto_functionst
 Cgoto_functiont
 Cgoto_inlinet::goto_inline_logt::goto_inline_log_infot
 Cgoto_inlinet::goto_inline_logt
 Cgoto_model_functiontInterface providing access to a single function in a GOTO model, plus its associated symbol table
 Cgoto_program2codet
 Cgoto_programtA generic container class for the GOTO intermediate representation of one function
 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< edge_with_callsitest >
 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< class_hierarchy_graph_nodet >
 Cgrapht< dep_nodet >
 Cgrapht< function_nodet >
 Cgrapht< xml_graph_nodet >
 Cstd::hash< dstringt >Default hash function of dstringt for use with STL containers
 Chavoc_loopst
 Cjava_bytecode_convert_methodt::holet
 Csmt2_convt::identifiert
 Cidentifiert
 Csmt2_parsert::idt
 Cieee_float_spect
 Cieee_floatt
 Cincremental_dirtytWrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly once
 Cindex_set_pairt
 Cindicator_maskt< T, B, U >
 Cindicator_maskt< T, B, std::integral_constant< T, 0 > >
 Cinflate_state
 Cresolve_inherited_componentt::inherited_componentt
 Cinode
 Cbmc_covert::goalt::instancet
 Ccpp_typecheckt::instantiation_levelt
 Ccpp_typecheckt::instantiationt
 Cjava_bytecode_parse_treet::instructiont
 Cgoto_programt::instructiontThis class represents an instruction in the GOTO intermediate representation
 Cinstrumentert
 Cinterval_templatet< T >
 Cinv_object_storet
 Cinvariant_sett
 Cstd::ios_baseSTL class
 Cirep_hash_container_baset::irep_entryt
 Cirep_full_eq
 Cirep_full_hash
 Cirep_hash
 Cirep_hash_container_baset
 Cirep_hash_mapt< Key, T >
 Cirep_serializationt
 Cirep_serializationt::ireps_containert
 CireptBase class for tree-like data structures with sharing
 Cis_predecessor_oft
 Cis_threadedt
 Csymbol_table_baset::iteratort
 Cjar_filetClass representing a .jar archive
 Cjava_bytecode_parse_treet
 Cjava_object_factoryt
 Cjava_simple_method_stubst
 Cconfigt::javat
 Cjsil_parse_treet
 Cjson_irept
 Cjson_streamtThis class provides a facility for streaming JSON objects directly to the output instead of waiting for the object to be fully formed in memory and then print it (as done using jsont)
 Cjsont
 Ck_inductiont
 Cjava_bytecode_parse_treet::classt::lambda_method_handlet
 Clanguage_entryt
 Clanguage_filet
 Clanguage_modulet
 Carrayst::lazy_constraintt
 Clazy_goto_functions_maptProvides a wrapper for a map of lazily loaded goto_functiont
 Cgoto_convertt::leave_targett
 Csmt2_convt::let_count_idt
 Cdocument_propertiest::linet
 Cliteralt
 Clocal_may_aliast::loc_infot
 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
 Cloop_accelerationt
 Cgoto_symex_statet::framet::loop_infot
 Cfault_localizationt::lpointt
 Cmain_function_resultt
 Cboolbv_mapt::map_bitt
 Cboolbv_mapt::map_entryt
 Ccpp_typecheck_resolvet::matcht
 Cmember_offset_iterator
 Cboolbv_widtht::membert
 Cjava_bytecode_parse_treet::membert
 Cinterpretert::memory_cellt
 Cmerge_full_irept
 Cmerge_irept
 Cmerged_irep_hash
 Cmerged_irepst
 Cmessage_handlert
 Cmessaget
 Ccpp_typecheckt::method_bodyt
 Cmethod_bytecodet
 Cmini_bdd_applyt
 Cmini_bdd_mgrt
 Cmini_bdd_nodet
 Cmini_bddt
 Cmm2cppt
 Cmonomialt
 Cmz_stream_s
 Cmz_zip_archive
 Cmz_zip_archive_file_stat
 Cmz_zip_archivetThin object-oriented wrapper around the MZ Zip library Zip file reader and extractor
 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
 Cstring_dependenciest::node_hashHash function for nodes
 Cunsigned_union_find::nodet
 Ccfg_dominators_templatet< P, T, post_dom >::nodet
 Clocal_cfgt::nodet
 Cstring_dependenciest::nodet
 Cnondet_instruction_infotHolds information about any discovered nondet methods, with extreme type- safety
 Cnum_bitst< N >
 Cnum_bitst< 0 >
 Cnum_bitst< 1 >
 Cnumeric_castt< Target, typename >Numerical cast provides a unified way of converting from one numerical type to another
 Cnumeric_castt< mp_integer >Convert expression to mp_integer
 Cnumeric_castt< T, typename std::enable_if< std::is_integral< T >::value >::type >Convert mp_integer or expr to any integral type
 Cobject_factory_parameterst
 Cobject_idt
 Cvalue_set_fit::object_map_dt
 Cvalue_set_fivrnst::object_map_dt
 Cvalue_sett::object_map_dtRepresents a set of expressions (exprt instances) with corresponding offsets (offsett instances)
 Cvalue_set_fivrt::object_map_dt
 Cprop_minimizet::objectivet
 Ccover_goalst::observert
 Coperator_entryt
 Coptionst
 Ccmdlinet::optiont
 Cosx_fat_readert
 Coverflow_instrumentert
 Cparameter_assignmentst
 Cparse_floatt
 Cparse_options_baset
 CParser
 Cpath_acceleratort
 Cpath_enumeratort
 Cpath_nodet
 Cpath_storagetStorage for symbolic execution paths to be resumed later
 Cpath_strategy_choosertFactory and information for path_storaget
 Cpath_storaget::pathtInformation saved at a conditional goto to resume execution
 CpatterntGiven a string of the format '?blah?', will return true when compared against a string that matches appart from any characters that are '?' in the original string
 Cpointee_address_equaltFunctor to check whether iterators from different collections point at the same object
 Cpointer_arithmetict
 Crequire_goto_statements::pointer_assignment_locationt
 Cirep_hash_container_baset::pointer_hasht
 Cpointer_logict
 Cpointer_logict::pointert
 Cpoints_tot
 Cpolynomial_acceleratort
 Cpolynomial_acceleratort::polynomial_array_assignment
 Cacceleration_utilst::polynomial_array_assignmentt
 Cpolynomialt
 Cjava_bytecode_parsert::pool_entryt
 Cpostconditiont
 Cbv_pointerst::postponedt
 Cpreconditiont
 Cprintf_formattert
 CProofTraverser
 Cgoto_symex_statet::propagationt
 Cproperty_checkert::property_statust
 Cqualifierst
 Cqdimacs_cnft::quantifiert
 Cboolbvt::quantifiert
 Crange_domain_baset
 Crationalt
 Creachability_slicert
 Creaching_definitiont
 Crecursion_set_entrytRecursion-set entry owner class
 Cref_expr_set_dt
 Creference_counting< T >
 Creference_counting< object_map_dt >
 Creference_counting< ref_expr_set_dt >
 Cremove_asmt
 Cremove_calls_no_bodyt
 Cremove_exceptionstLowers high-level exception descriptions into low-level operations suitable for symex and other analyses that don't understand the THROW or CATCH GOTO instructions
 Cremove_instanceoft
 Cremove_returnst
 Cremove_virtual_functionst
 Crename_symbolt
 Cgoto_symex_statet::renaming_levelt
 Creplace_symbolt
 Creplacement_predicatetPatterns of expressions that should be replaced
 Cresolution_prooft< T >
 Cresolution_prooft< clauset >
 Cresolve_inherited_componentt
 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
 Csaj_tabletProduce canonical ordering for associative and commutative binary operators
 Csave_scopet
 Creachability_slicert::search_stack_entrytA search stack entry, used in tracking nodes to mark reachable when walking over the CFG in fixedpoint_to_assertions and fixedpoint_from_assertions
 Cselect_pointer_typet
 Cshared_bufferst
 Cconcurrency_instrumentationt::shared_vart
 Csharing_mapt< keyT, valueT, hashT, equalT >A map implemented as a tree where subtrees can be shared between different maps
 Csharing_node_baset
 Cshow_goto_functions_jsont
 Cshow_goto_functions_xmlt
 Csimplify_exprt
 Creachability_slicert::slicer_entryt
 Cslicing_criteriont
 Csmall_mapt< T, Ind, Num >Map from small integers to values
 Csmall_mapt< innert >
 Csmall_shared_pointeet< Num >A helper class to store use-counts of objects held by small shared pointers
 Csmall_shared_pointeet< unsigned >
 Csmall_shared_ptrt< T >This class is really similar to boost's intrusive_pointer, but can be a bit simpler seeing as we're only using it one place
 Csmall_shared_ptrt< d_leaft< keyT, valueT, equalT > >
 Csmall_shared_two_way_pointeet< Num >
 Csmall_shared_two_way_ptrt< U, V >This class is similar to small_shared_ptrt and boost's intrusive_ptr
 Csmall_shared_two_way_ptrt< d_internalt< key_type, mapped_type, equalT >, d_containert< key_type, mapped_type, equalT > >
 Csmall_shared_two_way_ptrt< d_internalt< keyT, valueT, equalT >, d_containert< keyT, valueT, equalT > >
 Csmt2_stringstreamt
 Csmt2_temp_filet
 Ccbmc_solverst::solvert
 Csymex_targett::sourcet
 Csparse_arraytRepresents arrays of the form array_of(x) with {i:=a} with {j:=b} ... by a default value x and a list of entries (i,a), (j,b) etc
 Csparse_bitvector_analysist< V >
 Csparse_bitvector_analysist< reaching_definitiont >
 Csparse_vectort< T >
 Csparse_vectort< memory_cellt >
 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
 Cstring_axiomst
 Cstring_builtin_functiontBase class for string functions that are built in the solver
 Cstring_constraint_generatort
 Cstring_constraintt

Universally quantified string constraint

 Cstring_containert
 Cstring_dependenciestKeep track of dependencies between strings
 Cstring_exprt< child_t >
 Cstring_exprt< array_string_exprt >
 Cstring_exprt< refined_string_exprt >
 Cstring_hash
 Cstring_dependenciest::string_nodetA string node points to builtin_function on which it depends
 Cstring_ptr_hash
 Cstring_ptrt
 Cstructured_pool_entryt
 Cstub_global_initializer_factoryt
 Csubsumed_patht
 Csymbol_factoryt
 Csymbol_generatortGeneration of fresh symbols of a given type
 Csymbol_table_basetThe symbol table base class interface
 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
 Csystem_library_symbolst
 CT
 Ctaint_parse_treet
 Cgoto_convertt::targetst
 Cgrapht< N >::tarjant
 Ctdefl_compressor
 Ctdefl_output_buffer
 Ctdefl_sym_freq
 Ctemp_dirt
 Ctemplate_mapt
 Ctemplate_numberingt< Map >
 Ctemplate_numberingt< dstringt >
 Ctemplate_numberingt< dstringt, dstring_hash >
 Ctemplate_numberingt< exprt >
 Ctemplate_numberingt< exprt, irep_hash >
 Ctemplate_numberingt< irep_idt >
 Ctemplate_numberingt< irep_idt, irep_id_hash >
 Ctemplate_numberingt< packedt, vector_hasht >
 Ctemplate_numberingt< T >
 Ctemporary_filet
 Cmonomialt::termt
 Cbmc_covert::testt
 Cconcurrency_instrumentationt::thread_local_vart
 Cgoto_symex_statet::threadt
 Cgoto_convertt::throw_targett
 CtimestampertTimestamp class hierarchy
 Ctinfl_decompressor_tag
 Ctinfl_huff_table
 Cto_be_merged_irep_hash
 Ctrace_automatont
 Ctrace_optionst
 Ctvt
 Cdump_ct::typedef_infot
 Cequalityt::typestructt
 Cuncaught_exceptions_analysistComputes in exceptions_map an overapproximation of the exceptions thrown by each method
 Cuncaught_exceptions_domaint
 Cunified_difft
 Cuninitializedt
 Cunion_find< T >
 Cunion_find< exprt >
 Cunion_find< irep_idt >
 Cunion_find_replacetSimilar interface to union-find for expressions, with a function for replacing sub-expressions by their result for find
 Cfloat_bvt::unpacked_floatt
 Cfloat_utilst::unpacked_floatt
 Cunsigned_union_find
 Cgoto_unwindt::unwind_logt
 Cunwindsett
 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_settState type in value_set_domaint, used in value-set analysis and goto-symex
 Cconstant_propagator_domaint::valuest
 Cvalue_set_dereferencet::valuet
 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_interfacet
 Cxml_parse_treet
 Cxmlt
 Cyy_buffer_state
 Cyy_trans_info
 Cyyalloc
 CYYSTYPE