cprover
Class Hierarchy

Go to the graphical class hierarchy

This inheritance list is sorted roughly, but not completely, alphabetically:
[detail level 12345678]
 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
 Cframet::active_loop_infot
 Clinkingt::adjust_type_infot
 Caggressive_slicertThe aggressive slicer removes the body of all the functions except those on the shortest path, those within the call-depth of the shortest path, those given by name as command line argument, and those that contain a given irep_idt snippet If no properties are set by the user, we preserve all functions on the shortest paths to each property
 Cai_basetThis is the basic interface of the abstract interpreter with default implementations of the core functionality
 Cai_domain_basetThe interface offered by a domain, allows code to manipulate domains without knowing their exact type
 Cai_domain_factory_baset
 Cai_history_basetA history object is an abstraction / representation of the control-flow part of a set of traces
 Cai_history_factory_basetAs more detailed histories can get complex (for example, nested loops or deep, mutually recursive call stacks) they often need some user controls or limits
 Cai_storage_basetThis is the basic interface for storing domains
 Callocate_objectst
 Cancestry_resulttResult of an attempt to find ancestor information about two nodes
 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
 Csolver_hardnesst::assertion_statst
 CassignmenttAssignment from the rhs value to the lhs variable
 Cautomatont
 Cbase_type_eqt
 Cstd::basic_string< Char >STL class
 Cbdd_exprtConversion between exprt and bbdt This encapsulate a bdd_managert, thus BDDs created with this class should only be combined with BDDs created using the same instance of bdd_exprt
 Cbdd_managertManager for BDD creation
 Cbdd_nodetLow level access to the structure of the BDD, read-only
 CbddtLogical operations on BDDs
 Ccover_basic_blockst::block_infot
 Cjava_bytecode_convert_methodt::block_tree_nodet
 Cboolbv_mapt
 Cboolbv_widtht
 Cboundst
 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_minimizet
 Cbv_spect
 Cbv_utilst
 Cbytecode_infot
 Cc_storage_spect
 Cc_test_input_generatort
 Cc_typecastt
 Ccall_checkt< Base, T >
 Ccall_graphtA call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection
 Ccall_stack_historyt::call_stack_entryt
 Ccheck_call_sequencet::call_stack_entryt
 Ccall_validate_fullt< Base, T >
 Ccall_validatet< Base, T >
 Cgoto_program2codet::caset
 Ccbmc_invariants_should_throwtHelper to enable invariant throwing as above bounded to an object lifetime:
 Ccfg_dominators_templatet< P, T, post_dom >Dominator graph
 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 >
 Ccfg_instruction_to_dense_integert< T >Functor to convert cfg nodes into dense integers, used by cfg_baset
 Ccfg_instruction_to_dense_integert< goto_programt::const_targett >GOTO-instruction to location number functor
 Cfull_slicert::cfg_nodet
 Cinstrumentert::cfg_visitort
 Cshared_bufferst::cfg_visitort
 Cchange_impactt
 Ccharacter_refine_preprocesst
 Ccheck_call_sequencet
 Cci_lazy_methods_neededt
 Cclass_hierarchytNon-graph-based representation of the class hierarchy
 Cmethod_bytecodet::class_method_and_bytecodetPair of class id and methodt
 Cjava_class_loader_baset::classpath_entrytAn entry in the classpath
 Cjava_bytecode_parse_treet::classt
 Cclauset
 Cescape_domaint::cleanupt
 Ccmdlinet
 Ccode_contractst
 Ccode_with_references_listtWrapper around a list of shared pointer to code_with_referencest objects, which provides a nicer interface
 Ccode_with_referencestBase class for code which can contain references which can get replaced before generating actual codet
 Cmessaget::commandt
 Ccompare_base_name_and_descriptort
 Cai_history_baset::compare_historytIn a number of places we need to work with sets of histories so that these (a) make use of the immutability and sharing and (b) ownership can be transfered if necessary, we use shared pointers rather than references
 Ccomplexity_limitertSymex complexity module
 Ccomponentt
 Cconcat_iteratort< first_iteratort, second_iteratort >On increment, increments a first iterator and when the corresponding end iterator is reached, starts to increment a second one
 Cconcurrency_instrumentationt
 Cgoto_checkt::conditiont
 Ccone_of_influencet
 Cbv_refinementt::configt
 Cstring_refinementt::configt
 CconfigtGlobally accessible architectural configuration
 Cconflict_providert
 Cconst_expr_visitort
 Csmall_mapt< T, Ind, Num >::const_iteratorConst iterator
 Cconst_target_hash
 Csmall_mapt< T, Ind, Num >::const_value_iteratorConst value iterator
 Crecursive_initializationt::constructor_keyt
 Cconstructor_oft< constructedt >A type of functor which wraps around the set of constructors of a type
 Cgeneric_parameter_specialization_mapt::container_paramtThe index of the container and the type parameter inside that container
 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_goalstTry to cover some given set of goals incrementally
 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_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_exception_basetBase class for exceptions thrown in the cprover project
 Ccprover_library_entryt
 Cevent_grapht::critical_cyclet
 Cdata
 Cdata_dpt
 Cdatat
 Cdecision_proceduret
 Cdefault_trace_stept
 Cevent_grapht::critical_cyclet::delayt
 Csharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::delta_view_itemt
 Cdense_integer_mapt< K, V, KeyToDenseInteger >A map type that is backed by a vector, which relies on the ability to (a) see the keys that might be used in advance of their usage, and (b) map those keys onto a dense range of integers
 Cdense_integer_mapt< goto_programt::const_targett, entryt, cfg_instruction_to_dense_integert< goto_programt::const_targett > >
 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_callbacktBase class for pointer value set analysis
 Cdesignatort
 Cdestructor_and_idtResult of a tree query holding both destructor codet and the ID of the node that held it
 Cdestructor_treetTree to keep track of the destructors generated along each branch of a function
 Cdestructt< I, pointee_baset, Ts >
 Cdestructt< 0, pointee_baset, Ts... >
 Cdiagnostics_helpert< T >Helper to give us some diagnostic in a usable form on assertion failure
 Cdiagnostics_helpert< char * >
 Cdiagnostics_helpert< char[N]>
 Cdiagnostics_helpert< dstringt >
 Cdiagnostics_helpert< irep_pretty_diagnosticst >
 Cdiagnostics_helpert< source_locationt >
 Cdiagnostics_helpert< std::string >
 CdirtytDirty variables are ones which have their address taken so we can't reliably work out where they may be assigned and are also considered shared state in the presence of multi-threading
 Cdisjunctive_polynomial_accelerationt
 Cdispatch_table_entryt
 Cdjb_manglertMangle identifiers by hashing their working directory with djb2 hash
 Cdocument_propertiest::doc_claimt
 Cdocument_propertiest
 Cdoes_remove_constt
 Cdomain_baset
 Cdott
 Cdstring_hash
 Cdstringtdstringt has one field, an unsigned integer no which is an index into a static table of strings
 Cdump_c_configurationtUsed for configuring the behaviour of dump_c
 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
 Cmemory_snapshot_harness_generatort::entry_goto_locationtUser provided goto location: function name and (maybe) location number; the structure wraps this option with a parser
 Cmemory_snapshot_harness_generatort::entry_locationtWraps the information needed to identify the entry point
 Ccfg_baset< T, P, I >::entry_mapt
 Cmemory_snapshot_harness_generatort::entry_source_locationtUser provided source location: file name and line number; the structure wraps this option with a parser
 Cinv_object_storet::entryt
 Crw_set_baset::entryt
 Cclass_hierarchyt::entryt
 Cdesignatort::entryt
 Cvalue_sett::entrytRepresents a row of a value_sett
 Cvalue_set_fit::entryt
 Cvalue_set_fivrt::entryt
 Cvalue_set_fivrnst::entryt
 Cboolbv_widtht::entryt
 Cenumerating_loop_accelerationt
 Cprintf_formattert::eol_exceptiont
 Cmessaget::eomt
 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
 Cexpr2c_configurationtUsed for configuring the behaviour of expr2c and type2c
 Cexpr2ct
 Cexpr2stltClass for saving the internal state of the conversion process
 Cdetail::expr_dynamic_cast_return_typet< Ret, T >
 Cexpr_initializert< nondet >
 Cexpr_queryt< T >Wrapper for optionalt<exprt> with useful method for queries to be used in unit tests
 Cexpr_skeletontExpression in which some part is missing and can be substituted for another expression
 Cdetail::expr_try_dynamic_cast_return_typet< Ret, T >
 Cexpr_visitort
 Cfalse_type
 Csharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::falset
 Cfat_header_prefixt
 Cfault_localization_providertAn implementation of incremental_goto_checkert may implement this interface to provide fault localization information
 Cfault_location_infot
 Cfield_sensitivitytControl granularity of object accesses
 Cfile
 Cfile_name_manglertMangle identifiers by including their filename
 Cfilter_iteratort< iteratort >Iterator which only stops at elements for which some given function f is true
 Cfixed_keys_map_wrappert< mapt >
 Cfixedbv_spect
 Cfixedbvt
 Cflag_resettSet a Boolean flag to a new value (via set_flag) and restore the previous value when the entire object goes out of scope
 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
 Cformat_specifiertField names follow the OpenJDK implementation: http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/9b8c96f96a0f/src/share/classes/java/util/Formatter.java#l2569
 Cformat_spect
 Cformat_textt
 Cformat_tokent
 Cstd::forward_list< T >STL class
 CframetStack frames – these are used for function calls and for exceptions
 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
 Cfunction_name_manglert< MangleFun >Mangles the names in an entire program and its symbol table
 Cfunction_pointer_restrictionst
 Cfunctionst
 Cgcc_versiont
 Cgdb_apitInterface for running and querying GDB
 Cgdb_value_extractortInterface for extracting values from GDB (building on gdb_apit)
 Cgenerate_function_bodiestBase class for replace_function_body implementations
 Cgeneric_parameter_specialization_map_keyst
 Cgeneric_parameter_specialization_maptAuthor: Diffblue Ltd
 Cget_typet< I, Ts >Get the type with the given index in the parameter pack
 Cget_virtual_calleest
 Cgoal_filterstA collection of goal filters to be applied in conjunction
 Ccover_goalst::goalt
 Cgoto_symex_property_decidert::goalt
 Cgoto_checkt
 Cgoto_difft
 Cgoto_functionstA collection of goto functions
 Cgoto_functiontA goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers)
 Cgoto_harness_parse_optionst::goto_harness_configt
 Cgoto_harness_generator_factorytHelper to select harness type by name
 Cgoto_harness_generatort
 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_model_validation_optionst
 Cgoto_null_checktReturn structure for get_null_checked_expr and get_conditional_checked_expr
 Cgoto_program2codet
 Cgoto_programtA generic container class for the GOTO intermediate representation of one function
 Cgoto_statetContainer for data that varies per program point, e.g
 Cgoto_symex_fault_localizert
 Cgoto_symex_property_decidertProvides management of goal variables that encode properties
 Cgoto_symextThe main class for the forward symbolic simulator
 Cgoto_trace_providertAn implementation of incremental_goto_checkert may implement this interface to provide goto traces
 Cgoto_trace_steptStep of the trace of a GOTO program
 Cgoto_trace_storaget
 Cgoto_tracetTrace of a GOTO program
 Cgoto_unwindt
 Cgoto_verifiertAn implementation of goto_verifiert checks all properties in a goto model
 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, goto_programt::const_targett > >
 Cgrapht< cfg_base_nodet< T, I > >
 Cgrapht< cfg_base_nodet< T, java_bytecode_convert_methodt::method_offsett > >
 Cgrapht< class_hierarchy_graph_nodet >
 Cgrapht< dep_nodet >
 Cgrapht< destructor_treet::destructor_nodet >
 Cgrapht< function_nodet >
 Cgrapht< xml_graph_nodet >
 Cguard_bddt
 Cguard_expr_managertThis is unused by this implementation of guards, but can be used by other implementations of the same interface
 Cguard_exprt
 Chardness_collectort
 Csolver_hardnesst::hardness_ssa_keyt
 Cstd::hash< dstringt >Default hash function of dstringt for use with STL containers
 Cstd::hash< solver_hardnesst::hardness_ssa_keyt >
 Cstd::hash< string_not_contains_constraintt >
 Chavoc_loopst
 Cjava_bytecode_convert_methodt::holet
 Cidentifiert
 Csmt2_convt::identifiert
 Cidentity_functortIdentity functor. When we use C++20 this can be replaced with std::identity
 Csmt2_parsert::idt
 Cieee_float_spect
 Cieee_floatt
 Cfunction_call_harness_generatort::impltThis contains implementation details of function call harness generator to avoid leaking them out into the header
 Cincremental_dirtytWrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly once
 Cincremental_goto_checkertAn implementation of incremental_goto_checkert provides functionality for checking a set of properties and returning counterexamples one by one to the caller
 Cindex_set_pairt
 Cinfix_opt
 Cinflate_state
 Cresolve_inherited_componentt::inherited_componentt
 Cinode
 Cinsert_final_assert_falset
 Ccpp_typecheckt::instantiation_levelt
 Ccpp_typecheckt::instantiationt
 Cgoto_programt::instructiontThis class represents an instruction in the GOTO intermediate representation
 Cjava_bytecode_parse_treet::instructiont
 Cstatement_list_parse_treet::instructiontRepresents a regular Statement List instruction which consists out of one or more codet tokens
 Cinstrumentert
 Cinterval_templatet< T >
 Cinterval_uniontRepresents a set of integers by a union of intervals, which are stored in increasing order for efficient union and intersection (linear time in both cases)
 Cinv_object_storet
 Cinvariant_failedtA logic error, augmented with a distinguished field to hold a backtrace
 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_pretty_diagnosticst
 Cirep_serializationt
 Cirep_serializationt::ireps_containert
 Cis_constanttDetermine whether an expression is constant
 Cis_predecessor_oft
 Cis_threadedt
 Citerator
 Csymbol_table_baset::iteratort
 Cjar_filetClass representing a .jar archive
 Cjar_pooltA chache for jar_filet objects, by file name
 Cjava_boxed_type_infotReturn type for get_boxed_type_info_by_name
 Cjava_bytecode_language_optionst
 Cjava_bytecode_parse_treet
 Cjava_object_factoryt
 Cjava_primitive_type_infotReturn type for get_java_primitive_type_info
 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
 Clabelt
 Cjava_bytecode_parse_treet::classt::lambda_method_handlet
 Clanguage_entryt
 Clanguage_filet
 Clanguage_modulet
 Clazy_class_to_declared_symbols_maptMap classes to the symbols they declare but is only computed once it is needed and the map is then kept
 Carrayst::lazy_constraintt
 Clazy_goto_functions_maptProvides a wrapper for a map of lazily loaded goto_functiont
 Clazyt< valuet >
 Cgoto_convertt::leave_targett
 Cletifyt::let_count_idt
 CletifytIntroduce LET for common subexpressions
 Clevenshtein_automatontSimple automaton that can detect whether a string can be transformed into another with a limited number of deletions, insertions or substitutions
 Clinear_functiontCanonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given by constant_coefficient 2 and coefficients: x -> 2, y -> -1
 Cdocument_propertiest::linet
 Cliteralt
 Clocal_may_aliast::loc_infot
 Clocal_bitvector_analysist
 Clocal_cfgt
 Clocal_control_flow_decisiontRecords all local control-flow decisions up to a limit of number of histories per location
 Clocal_may_alias_factoryt
 Clocal_may_aliast
 Clocal_safe_pointerstA very simple, cheap analysis to determine when dereference operations are trivially guarded by a check against a null pointer access
 Cjava_bytecode_convert_methodt::local_variable_with_holest
 Cjava_bytecode_parse_treet::methodt::local_variablet
 Clocalst
 Cloop_analysist< T >
 Cloop_analysist< goto_programt::const_targett >
 Cloop_analysist< goto_programt::targett >
 Cframet::loop_infot
 Cloop_templatet< T >A loop, specified as a set of instructions
 Cmain_function_resultt
 Cboolbv_mapt::map_bitt
 Cboolbv_mapt::map_entryt
 Cmap_iteratort< iteratort, outputt >Iterator which applies some given function f after each increment and returns its result on dereference
 CMatcherBase
 Ccpp_typecheck_resolvet::matcht
 Cjava_bytecode_parse_treet::membert
 Cboolbv_widtht::membert
 Cgdb_apit::memory_addresstMemory address imbued with the explicit boolean data indicating if the address is null or not
 Cinterpretert::memory_cellt
 Cgdb_value_extractort::memory_scopet
 Cmerge_full_irept
 Cmerge_irept
 Cmerged_irep_hash
 Cmerged_irepst
 Cmessage_handlert
 CmessagetClass that provides messages with a built-in verbosity 'level'
 Ccpp_typecheckt::method_bodyt
 Cmethod_bytecodet
 Cmethodt
 Cmini_bdd_applyt
 Cmini_bdd_mgrt
 Cmini_bdd_nodet
 Cmini_bddt
 Cmonomialt
 Cms_cl_versiont
 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
 Csmt2_parsert::named_termt
 Cnamespace_basetBasic interface for a namespace
 Cstatement_list_typecheckt::nesting_stack_entrytEvery time branching occurs inside of a boolean expression string in STL, the current value of the RLO and OR bits are saved and put on a separate stack
 Cstatement_list_parse_treet::networktRepresentation of a network in Siemens TIA
 Cnew_scopet
 Cnfat< T >Very simple NFA implementation Not super performant, but should be good enough for our purposes
 Cnfat< char >
 Cstring_dependenciest::node_hashHash function for nodes
 Clocal_cfgt::nodet
 Cunsigned_union_find::nodet
 Ccfg_dominators_templatet< P, T, post_dom >::nodet
 Cstring_dependenciest::nodet
 Cnon_sharing_treet< derivedt, named_subtreest >Base class for tree-like data structures without sharing
 Cnondet_instruction_infotHolds information about any discovered nondet methods, with extreme type- safety
 Cnondet_volatilet
 Csharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::noop_value_comparatort
 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_creation_infotValues passed around between most functions of the recursive deterministic assignment algorithm entered from assign_from_json
 Cobject_creation_referencetInformation to store when several references point to the same Java object
 Cobject_factory_parameterst
 Cobject_idt
 Cvalue_set_fit::object_map_dt
 Cvalue_set_fivrt::object_map_dt
 Cvalue_set_fivrnst::object_map_dt
 Cprop_minimizet::objectivet
 Ccover_goalst::observert
 Coperator_entryt
 Ccmdlinet::option_namest
 Coptionst
 Ccmdlinet::optiont
 Cosx_fat_readert
 Cosx_mach_o_readert
 Coverflow_instrumentert
 Cgraphml_witnesst::pair_hash< S, T >
 Cparameter_assignmentst
 Cparse_floatt
 Cparse_options_baset
 Cstring_constraint_generatort::parseint_argumentstArgument block for parseInt and cousins, common to parseInt itself and CProverString.isValidInt
 CParser
 Cpath_acceleratort
 Cpath_enumeratort
 Cpath_nodet
 Cpath_storagetStorage for symbolic execution paths to be resumed later
 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
 Cgdb_apit::pointer_valuetData associated with the value of a pointer, i.e
 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
 Cprefix_filtertProvides filtering of strings vai inclusion/exclusion lists of prefixes
 Cmemory_snapshot_harness_generatort::preordert< Key >Simple structure for linearising posets
 Cgeneric_parameter_specialization_mapt::printertA wrapper for a generic_parameter_specialization_mapt and a namespacet that can be output to a stream
 Cprintf_formattert
 CProofTraverser
 Cprop_minimizetComputes a satisfying assignment of minimal cost according to a const function using incremental SAT
 Cproperty_infot
 CproptTO_BE_DOCUMENTED
 Cqualifierst
 Cboolbvt::quantifiert
 Cqdimacs_cnft::quantifiert
 Crange_domain_baset
 Cranget< iteratort >A range is a pair of a begin and an end iterators
 Crationalt
 Creachability_slicert
 Creaching_definitiontIdentifies a GOTO instruction where a given variable is defined (i.e
 Csharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::real_value_comparatort
 Crecursion_set_entrytRecursion-set entry owner class
 Crecursive_initialization_configt
 Crecursive_initializationtClass for generating initialisation code for compound structures
 Cref_count_ift< enabled >Used in tree_nodet for activating or not reference counting
 Cref_count_ift< sharing >
 Cref_count_ift< true >
 Cref_expr_set_dt
 Creference_counting< T, empty >
 Creference_counting< object_map_dt >
 Creference_counting< object_map_dt, empty_object_map >
 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_function_pointerst
 Cremove_instanceoft
 Cremove_returnst
 Cremove_virtual_functionst
 Crename_symbolt
 Creplace_callst
 Creplace_symboltReplace expression or type symbols by an expression or type, respectively
 Creplacement_predicatetPatterns of expressions that should be replaced
 Cresolution_prooft< T >
 Cresolution_prooft< clauset >
 Cresolve_inherited_componentt
 Crestrictt
 Csimplify_exprt::resultt< T >
 Cincremental_goto_checkert::resultt
 Cmini_bdd_mgrt::reverse_keyt
 Cfloat_utilst::rounding_mode_bitst
 Cfloat_bvt::rounding_mode_bitst
 Ctaint_parse_treet::rulet
 Crw_range_sett
 Crw_set_baset
 Csaj_tabletProduce canonical ordering for associative and commutative binary operators
 Csolver_hardnesst::sat_hardnesst
 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
 Cosx_mach_o_readert::sectiont
 Cselect_pointer_typet
 Csese_region_analysist
 Caddress_of_aware_replace_symbolt::set_require_lvalue_and_backupt
 Cshared_bufferst
 Cconcurrency_instrumentationt::shared_vart
 Csharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::sharing_map_statstStats about sharing between several sharing map instances
 Csharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >A map implemented as a tree where subtrees can be shared between different maps
 Csharing_mapt< dstringt, exprt >
 Csharing_mapt< irep_idt, entryt >
 Csharing_mapt< irep_idt, std::pair< ssa_exprt, std::size_t > >
 Csharing_nodet< keyT, valueT, equalT >
 Csharing_nodet< key_type, mapped_type >
 Csharing_treet< derivedt, named_subtreest >Base class for tree-like data structures with sharing
 Csharing_treet< irept, std::map< irep_namet, irept > >
 Cshow_goto_functions_jsont
 Cshow_goto_functions_xmlt
 Csmt2_parsert::signature_with_parameter_idst
 Csimplify_exprt
 Creachability_slicert::slicer_entryt
 Cslicing_criteriont
 Csmall_mapt< T, Ind, Num >Map from small integers to values
 Csmall_mapt< innert >
 Csmall_shared_n_way_pointee_baset< N, Num >
 Csmall_shared_n_way_ptrt< Ts >This class is similar to small_shared_ptrt and boost's intrusive_ptr
 Csmall_shared_n_way_ptrt< d_containert< key_type, mapped_type, equalT >, d_leaft< key_type, mapped_type, equalT >, d_internalt< key_type, mapped_type, equalT > >
 Csmall_shared_n_way_ptrt< d_containert< keyT, valueT, equalT >, d_leaft< keyT, valueT, equalT >, d_internalt< keyT, valueT, equalT > >
 Csmall_shared_pointeet< Num >A helper class to store use-counts of objects held by small shared pointers
 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
 Csmt2_format_containert< T >
 Csmt2_parsert
 Csmt2_stringstreamt
 Csmt2_tokenizert
 Csolver_factoryt
 Csolver_hardnesstA structure that facilitates collecting the complexity statistics from a decision procedure
 Csolver_resource_limitst
 Csolver_factoryt::solvert
 Csource_linest
 Cmemory_snapshot_harness_generatort::source_location_matchtWraps the information for source location match candidates
 Csymex_targett::sourcetIdentifies source in the context of symbolic execution
 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 >An instance of this class provides an assignment of unique numeric ID to each inserted reaching_definitiont instance
 Csparse_bitvector_analysist< reaching_definitiont >
 Csparse_vectort< T >
 Csparse_vectort< memory_cellt >
 CSSA_steptSingle SSA step in the equation
 Cinterpretert::stack_framet
 Cjava_bytecode_parse_treet::methodt::stack_map_table_entryt
 Ccheck_call_sequencet::state_hash
 Cstatement_list_parse_treetIntermediate representation of a parsed Statement List file before converting it into a goto program
 Cnfat< T >::statetA state is a set of possibly active transitions
 Ccheck_call_sequencet::statet
 Cstatic_analysis_baset
 Cstatic_verifier_resultt
 Cclauset::stept
 Cstring_axiomst
 Cstring_builtin_functiontBase class for string functions that are built in the solver
 Cstring_constraint_generatort
 Cstring_constraintstCollection of constraints of different types: existential formulas, universal formulas, and "not contains" (universal with one alternation)
 Cstring_constraintt
 Cstring_containert
 Cstring_dependenciestKeep track of dependencies between strings
 Cstring_hash
 Cstring_dependenciest::string_nodetA string node points to builtin_function on which it depends
 Cstring_not_contains_constrainttConstraints to encode non containement of strings
 Cstring_ptr_hash
 Cstring_ptrt
 Cstructured_data_entryt
 Cstructured_datatA way of representing nested key/value data
 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
 Csymex_assigntFunctor for symex assignment
 Csymex_complexity_limit_exceeded_actiontDefault heuristic transformation that cancels branches when complexity has been breached
 Csymex_configtConfiguration used for a symbolic execution
 Csymex_coveraget
 Csymex_level1tFunctor to set the level 1 renaming of SSA expressions
 Csymex_level2tFunctor to set the level 2 renaming of SSA expressions
 Csymex_nondet_generatortFunctor generating fresh nondet symbols
 Csymex_slicet
 Csymex_targettThe interface of the target container for symbolic execution to record its symbolic steps into
 Csystem_library_symbolst
 CT
 Ctaint_analysist
 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
 Ctest_inputst
 Cconcurrency_instrumentationt::thread_local_vart
 Cgoto_symex_statet::threadt
 Cgoto_convertt::throw_targett
 Cstatement_list_parse_treet::tia_moduletBase element of all modules in the Totally Integrated Automation (TIA) portal by Siemens
 CtimestampertTimestamp class hierarchy
 Ctinfl_decompressor_tag
 Ctinfl_huff_table
 Cto_be_merged_irep_hash
 Ctrace_automatont
 Ctrace_optionstOptions for printing the trace using show_goto_trace
 Cnfat< T >::transitiont
 Ctvt
 Clocal_safe_pointerst::type_comparetComparator that regards type-equal expressions as equal, and otherwise uses the natural (operator<) ordering on irept
 Cdump_ct::typedef_infot
 Cequalityt::typestructt
 Cuncaught_exceptions_analysistComputes in exceptions_map an overapproximation of the exceptions thrown by each method
 Cuncaught_exceptions_domaint
 Cunderlyingt
 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_utilst::unpacked_floatt
 Cfloat_bvt::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_dereferencetWrapper for a function dereferencing pointer expressions using a value set
 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::valuetReturn value for build_reference_to; see that method for documentation
 Cstatement_list_parse_treet::var_declarationtStruct for a single variable declaration in Statement List
 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
 Cwitness_providertAn implementation of incremental_goto_checkert may implement this interface to provide GraphML witnesses
 Cxml_edget
 Cxml_parse_treet
 Cxmlt
 Czip_iteratort< first_iteratort, second_iteratort, same_size >Zip two ranges to make a range of pairs