cprover
Class List
Here are the classes, structs, unions and interfaces with brief descriptions:
[detail level 123]
 Ndetail
 Nrequire_goto_statements
 Nrequire_parse_tree
 Nrequire_type
 NstdSTL namespace
 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
 C_rw_set_loct
 Cabs_exprtAbsolute value
 Cabstract_eventt
 Cabstract_goto_modeltAbstract interface to eager or lazy GOTO models
 Cacceleratet
 Cacceleration_utilst
 Caddress_of_aware_replace_symboltReplace symbols with constants while maintaining syntactically valid expressions
 Caddress_of_exprtOperator to return the address of an object
 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_basetThe basic interface of an abstract interpreter
 Cai_domain_basetThe interface offered by a domain, allows code to manipulate domains without knowing their exact type
 Cait
 Call_paths_enumeratort
 Canalysis_exceptiontThrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an error)
 Cand_exprtBoolean AND
 Cannotated_typet
 Cansi_c_convert_typet
 Cansi_c_declarationt
 Cansi_c_declaratort
 Cansi_c_identifiert
 Cansi_c_languaget
 Cansi_c_parse_treet
 Cansi_c_parsert
 Cansi_c_scopet
 Cansi_c_typecheckt
 Carmcc_cmdlinet
 Carmcc_modet
 Carray_exprtArray constructor from list of elements
 Carray_list_exprtArray constructor from a list of index-element pairs Operands are index/value pairs, alternating
 Carray_of_exprtArray constructor from single element
 Carray_pooltCorrespondance between arrays and pointers string representations
 Carray_string_exprt
 Carray_typetArrays with given size
 Carrayst
 Cas86_cmdlinet
 Cas_cmdlinet
 Cas_modet
 Cashr_exprtArithmetic right shift
 Cassembler_parsert
 Cassert_criteriont
 Cassert_false_generate_function_bodiest
 Cassert_false_then_assume_false_generate_function_bodiest
 Cassume_false_generate_function_bodiest
 Cautomatont
 Cauxiliary_symboltInternally generated symbol table entryThis is a symbol generated as part of translation to or modification of the intermediate representation
 Cbad_cast_exceptiont
 Cbase_ref_infot
 Cbase_type_eqt
 Cbcc_cmdlinet
 Cbdd_exprtTO_BE_DOCUMENTED
 Cbinary_exprtA base class for binary expressions
 Cbinary_predicate_exprtA base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two arguments
 Cbinary_relation_exprtA base class for relations, i.e., binary predicates
 Cbitand_exprtBit-wise AND
 Cbitnot_exprtBit-wise negation of bit-vectors
 Cbitor_exprtBit-wise OR
 Cbitvector_conversion_exceptiont
 Cbitvector_typetBase class of fixed-width bit-vector types
 Cbitxor_exprtBit-wise XOR
 Cbmc_all_propertiest
 Cbmc_covert
 CbmctBounded model checking or path exploration for goto-programs
 Cbool_typetThe Boolean type
 Cboolbv_mapt
 Cboolbv_widtht
 Cboolbvt
 Cbswap_exprtThe byte swap expression
 Cbv_arithmetict
 Cbv_dimacst
 Cbv_endianness_maptMap bytes according to the configured endianness
 Cbv_minimizet
 Cbv_minimizing_dect
 Cbv_pointerst
 Cbv_refinementt
 Cbv_spect
 Cbv_typetFixed-width bit-vector without numerical interpretation
 Cbv_utilst
 Cbyte_extract_exprtTO_BE_DOCUMENTED
 Cbyte_update_exprtTO_BE_DOCUMENTED
 Cbytecode_infot
 Cc_bit_field_typetType for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they have a subtype)
 Cc_bool_typetThe C/C++ Booleans
 Cc_enum_tag_typetC enum tag type, i.e., c_enum_typet with an identifier
 Cc_enum_typetThe type of C enums
 Cc_object_factory_parameterst
 Cc_qualifierst
 Cc_storage_spect
 Cc_typecastt
 Cc_typecheck_baset
 Ccall_checkt
 Ccall_graphtA call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection
 Ccall_validate_fullt
 Ccall_validatet
 Ccasting_replace_symbolt
 Ccbmc_parse_optionst
 Ccerr_message_handlert
 Ccfg_base_nodet
 Ccfg_basetA multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO program
 Ccfg_dominators_templatet
 Cchange_impactt
 Ccharacter_refine_preprocesst
 Ccheck_call_sequencet
 Cci_lazy_methods_neededt
 Cci_lazy_methodst
 Cclass_hierarchy_graph_nodetClass hierarchy graph node: simply contains a class identifier
 Cclass_hierarchy_graphtClass hierarchy, represented using grapht and therefore suitable for use with generic graph algorithms
 Cclass_hierarchytNon-graph-based representation of the class hierarchy
 Cclass_infotCorresponds to the CONSTANT_Class_info Structure Described in Java 8 specification 4.4.1
 Cclass_typetClass type
 Cclauset
 Ccmdlinet
 Ccnf_clause_list_assignmentt
 Ccnf_clause_listt
 Ccnf_solvert
 Ccnft
 Ccode_asmtcodet representation of an inline assembler statement
 Ccode_asserttA non-fatal assertion, which checks a condition then permits execution to continue
 Ccode_assigntA codet representing an assignment in the program
 Ccode_assumetAn assumption, which must hold in subsequent code
 Ccode_blocktA codet representing sequential composition of program statements
 Ccode_breaktcodet representation of a break statement (within a for or while loop)
 Ccode_continuetcodet representation of a continue statement (within a for or while loop)
 Ccode_contractst
 Ccode_deadtA codet representing the removal of a local variable going out of scope
 Ccode_decltA codet representing the declaration of a local variable
 Ccode_dowhiletcodet representation of a do while statement
 Ccode_expressiontcodet representation of an expression statement
 Ccode_fortcodet representation of a for statement
 Ccode_function_calltcodet representation of a function call statement
 Ccode_gototcodet representation of a goto statement
 Ccode_ifthenelsetcodet representation of an if-then-else statement
 Ccode_labeltcodet representation of a label for branch targets
 Ccode_landingpadtA statement that catches an exception, assigning the exception in flight to an expression (e.g
 Ccode_pop_catchtPops an exception handler from the stack of active handlers (i.e
 Ccode_push_catchtPushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ..
 Ccode_returntcodet representation of a "return from a function" statement
 Ccode_skiptA codet representing a skip statement
 Ccode_switch_casetcodet representation of a switch-case, i.e. a case statement within a switch
 Ccode_switchtcodet representing a switch statement
 Ccode_try_catchtcodet representation of a try/catch block
 Ccode_typetBase type of functions
 Ccode_whiletcodet representing a while statement
 CcodetData structure for representing an arbitrary statement in a program
 Ccompilet
 Ccomplex_exprtComplex constructor from a pair of numbers
 Ccomplex_imag_exprtImaginary part of the expression describing a complex number
 Ccomplex_real_exprtReal part of the expression describing a complex number
 Ccomplex_typetComplex numbers made of pair of given subtype
 Cconcat_iteratortOn increment, increments a first iterator and when the corresponding end iterator is reached, starts to increment a second one
 Cconcatenation_exprtConcatenation of bit-vector operands
 Cconcurrency_aware_ait
 Cconcurrency_aware_static_analysist
 Cconcurrency_instrumentationt
 Cconcurrent_cfg_baset
 Ccond_exprtThis is a parametric version of an if-expression: it returns the value of the first case (using the ordering of the operands) whose condition evaluates to true
 Ccone_of_influencet
 CconfigtGlobally accessible architectural configuration
 Cconsole_message_handlert
 Cconst_depth_iteratort
 Cconst_expr_visitort
 Cconst_target_hash
 Cconst_unique_depth_iteratort
 Cconstant_exprtA constant literal expression
 Cconstant_propagator_ait
 Cconstant_propagator_domaint
 Cconversion_dependenciestThis is structure is here to facilitate passing arguments to the conversion functions
 Ccopy_on_write_pointeetA helper class to store use-counts of copy-on-write objects
 Ccopy_on_writetA utility class for writing types with copy-on-write behaviour (like irep)
 Ccounterexample_beautificationt
 Ccout_message_handlert
 Ccover_assertion_instrumentertAssertion coverage instrumenter
 Ccover_basic_blocks_javat
 Ccover_basic_blockst
 Ccover_blocks_baset
 Ccover_branch_instrumentertBranch coverage instrumenter
 Ccover_condition_instrumentertCondition coverage instrumenter
 Ccover_configt
 Ccover_cover_instrumentert__CPROVER_cover coverage instrumenter
 Ccover_decision_instrumentertDecision coverage instrumenter
 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
 Ccover_location_instrumentertBasic block coverage instrumenter
 Ccover_mcdc_instrumentertMC/DC coverage instrumenter
 Ccover_path_instrumentertPath coverage instrumenter
 Ccoverage_recordt
 Ccpp_convert_typet
 Ccpp_declarationt
 Ccpp_declarator_convertert
 Ccpp_declaratort
 Ccpp_enum_typet
 Ccpp_idt
 Ccpp_itemt
 Ccpp_languaget
 Ccpp_linkage_spect
 Ccpp_member_spect
 Ccpp_namespace_spect
 Ccpp_namet
 Ccpp_parse_treet
 Ccpp_parsert
 Ccpp_root_scopet
 Ccpp_save_scopet
 Ccpp_saved_template_mapt
 Ccpp_scopest
 Ccpp_scopet
 Ccpp_static_assertt
 Ccpp_storage_spect
 Ccpp_template_args_baset
 Ccpp_template_args_non_tct
 Ccpp_template_args_tct
 Ccpp_token_buffert
 Ccpp_tokent
 Ccpp_typecastt
 Ccpp_typecheck_fargst
 Ccpp_typecheck_resolvet
 Ccpp_typecheckt
 Ccpp_usingt
 Ccprover_exception_basetBase class for exceptions thrown in the cprover project
 Ccprover_library_entryt
 Ccustom_bitvector_analysist
 Ccustom_bitvector_domaint
 Ccw_modet
 Cd_containert
 Cd_internalt
 Cd_leaft
 Cdata
 Cdata_dpt
 Cdatat
 Cdecision_proceduret
 Cdecorated_symbol_exprtExpression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_local
 Cdep_edget
 Cdep_graph_domaint
 Cdep_nodet
 Cdependence_grapht
 Cdepth_iterator_basetDepth first search iterator base - iterates over supplied expression and all its operands recursively
 Cdepth_iterator_expr_statetHelper class for depth_iterator_baset
 Cdepth_iteratort
 Cdereference_callbacktBase class for pointer value set analysis
 Cdereference_exprtOperator to dereference a pointer
 CdereferencetWrapper for a function which dereference a pointer-expression
 Cdeserialization_exceptiontThrown when failing to deserialize a value from some low level format, like JSON or raw bytes
 Cdesignatort
 Cdiagnostics_helpertHelper 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 >
 Cdimacs_cnf_dumpt
 Cdimacs_cnft
 Cdirtyt
 Cdisjunctive_polynomial_accelerationt
 Cdispatch_table_entryt
 Cdiv_exprtDivision
 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_ct
 Cdynamic_object_exprtRepresentation of heap-allocated objects
 CElf32_Ehdr
 CElf32_Shdr
 CElf64_Ehdr
 CElf64_Shdr
 Celf_readert
 Cempty_cfg_nodet
 Cempty_edget
 Cempty_typetThe empty type
 Cendianness_maptMaps a big-endian offset to a little-endian offset
 Cenumerating_loop_accelerationt
 Cenumeration_typetAn enumeration type, i.e., a type with elements (not to be confused with C enums)
 Cequal_exprtEquality
 Cequalityt
 Cequation_conversion_exceptiont
 Cequation_symbol_mappingtMaps equation to expressions contained in them and conversely expressions to equations that contain them
 Cescape_analysist
 Cescape_domaint
 Cevent_grapht
 Cexists_exprtAn exists expression
 Cexpanding_vectort
 Cexpr2c_configurationtUsed for configuring the behaviour of expr2c and type2c
 Cexpr2cppt
 Cexpr2ct
 Cexpr2javat
 Cexpr2jsilt
 Cexpr_initializert
 Cexpr_visitort
 CexprtBase class for all expressions
 Cextractbit_exprtExtracts a single bit of a bit-vector operand
 Cextractbits_exprtExtracts a sub-range of a bit-vector operand
 Cfactorial_power_exprtFalling factorial power
 Cfalse_exprtThe Boolean constant false
 Cfault_localizationt
 Cfieldref_exprtRepresents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as an argument to a getstatic and putstatic instruction
 Cfile
 Cfilter_iteratortIterator which only stops at elements for which some given function f is true
 Cfind_qvar_visitort
 Cfixed_keys_map_wrappert
 Cfixedbv_spect
 Cfixedbv_typetFixed-width bit-vector with signed fixed-point interpretation
 Cfixedbvt
 Cflatten_byte_extract_exceptiont
 Cfloat_approximationt
 Cfloat_bvt
 Cfloat_utilst
 Cfloatbv_typecast_exprtSemantic type conversion from/to floating-point formats
 Cfloatbv_typetFixed-width bit-vector with IEEE floating-point interpretation
 Cflow_insensitive_abstract_domain_baset
 Cflow_insensitive_analysis_baset
 Cflow_insensitive_analysist
 Cforall_exprtA forall expression
 Cformat_constantt
 Cformat_containertThe below enables convenient syntax for feeding objects into streams, via stream << format(o)
 Cformat_elementt
 Cformat_specifiert
 Cformat_spect
 Cformat_textt
 Cformat_tokent
 Cfree_form_cmdlinetAn implementation of cmdlinet to be used in tests
 CfreertA functor wrapping std::free
 Cfull_slicert
 Cfunction_application_exprtApplication of (mathematical) function
 Cfunction_filter_basetBase class for filtering functions
 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
 Cfunction_modifiest
 Cfunctionst
 Cgcc_cmdlinet
 Cgcc_message_handlert
 Cgcc_modet
 Cgcc_versiont
 Cgenerate_function_bodies_errort
 Cgenerate_function_bodiestBase class for replace_function_body implementations
 Cgeneric_parameter_specialization_map_keyst
 Cglobal_may_alias_analysistThis is a may analysis (i.e
 Cglobal_may_alias_domaint
 Cgoal_filter_basetBase class for filtering goals
 Cgoal_filterstA collection of goal filters to be applied in conjunction
 Cgoto_analyzer_parse_optionst
 Cgoto_cc_cmdlinet
 Cgoto_cc_modet
 Cgoto_checkt
 Cgoto_convert_functionst
 Cgoto_convertt
 Cgoto_diff_languagest
 Cgoto_diff_parse_optionst
 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_inlinet
 Cgoto_instrument_parse_optionst
 Cgoto_model_functiontInterface providing access to a single function in a GOTO model, plus its associated symbol table
 Cgoto_modelt
 Cgoto_null_checktReturn structure for get_null_checked_expr and get_conditional_checked_expr
 Cgoto_program2codet
 Cgoto_program_coverage_recordt
 Cgoto_program_dereferencetWrapper for functions removing dereferences in expressions contained in a goto program
 Cgoto_programtA generic container class for the GOTO intermediate representation of one function
 Cgoto_symex_is_constantt
 Cgoto_symex_statet
 Cgoto_symextThe main class for the forward symbolic simulator
 Cgoto_trace_steptTO_BE_DOCUMENTED
 Cgoto_tracetTO_BE_DOCUMENTED
 Cgoto_unwindt
 Cgraph_nodetThis class represents a node in a directed graph
 Cgraphml_witnesst
 Cgraphmlt
 CgraphtA generic directed graph with a parametric node type
 Cguarded_range_domaint
 Cguardt
 Chavoc_generate_function_bodiest
 Chavoc_loopst
 Cidentifiert
 Cieee_float_equal_exprtIEEE-floating-point equality
 Cieee_float_notequal_exprtIEEE floating-point disequality
 Cieee_float_op_exprtIEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)
 Cieee_float_spect
 Cieee_floatt
 Cif_exprtThe trinary if-then-else operator
 Cimplies_exprtBoolean implication
 Cin_function_criteriont
 Cinclude_pattern_filtertFilters functions that match the provided pattern
 Cincomplete_array_typetArrays without size
 Cincorrect_goto_program_exceptiontThrown when a goto program that's being processed is in an invalid format, for example passing the wrong number of arguments to functions
 Cincorrect_source_program_exceptiont
 Cincremental_dirtytWrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly once
 Cindex_designatort
 Cindex_exprtArray index operator
 Cindex_set_pairt
 Cindicator_maskt
 Cindicator_maskt< T, B, std::integral_constant< T, 0 > >
 Cinfinity_exprtAn expression denoting infinity
 Cinfix_opt
 Cinflate_state
 Cinode
 Cinstrumenter_pensievet
 Cinstrumentert
 Cinteger_typetUnbounded, signed integers (mathematical integers, not bitvectors)
 Cinternal_functions_filtertFilters out CPROVER internal functions
 Cinternal_goals_filtertFilters out goals with source locations considered internal
 Cinterpretert
 Cinterval_domaint
 Cinterval_sparse_arraytRepresents arrays by the indexes up to which the value remains the same
 Cinterval_templatet
 Cinv_object_storet
 Cinvalid_command_line_argument_exceptiontThrown when users pass incorrect command line arguments, for example passing no files to analysis or setting two mutually exclusive flags
 Cinvalid_source_file_exceptiontThrown when we can't handle something in an input source file
 Cinvariant_failedtA logic error, augmented with a distinguished field to hold a backtrace
 Cinvariant_propagationt
 Cinvariant_set_domaint
 Cinvariant_sett
 Cinvariant_with_diagnostics_failedtA class that includes diagnostic information related to an invariant violation
 Cirep_full_eq
 Cirep_full_hash
 Cirep_full_hash_containert
 Cirep_hash
 Cirep_hash_container_baset
 Cirep_hash_containert
 Cirep_hash_mapt
 Cirep_pretty_diagnosticst
 Cirep_serializationt
 CireptBase class for tree-like data structures with sharing
 Cis_constanttDetermine whether an expression is constant
 Cis_predecessor_oft
 Cis_threaded_domaint
 Cis_threadedt
 Cisfinite_exprtEvaluates to true if the operand is finite
 Cisinf_exprtEvaluates to true if the operand is infinite
 Cisnan_exprtEvaluates to true if the operand is NaN
 Cisnormal_exprtEvaluates to true if the operand is a normal number
 Cjanalyzer_parse_optionst
 Cjar_filetClass representing a .jar archive
 Cjar_pooltA chache for jar_filet objects, by file name
 Cjava_annotationt
 Cjava_bytecode_convert_classt
 Cjava_bytecode_convert_methodt
 Cjava_bytecode_instrumentt
 Cjava_bytecode_languaget
 Cjava_bytecode_parse_treet
 Cjava_bytecode_parsert
 Cjava_bytecode_typecheckt
 Cjava_class_loader_basetBase class for maintaining classpath
 Cjava_class_loader_limittClass representing a filter for class file loading
 Cjava_class_loadertClass responsible to load .class files
 Cjava_class_typet
 Cjava_generic_class_typetClass to hold a class with generics, extends the java class type with a vector of java generic type parameters (also called type variables)
 Cjava_generic_parametertClass to hold a Java generic type parameter (also called type variable), e.g., T in List<T>
 Cjava_generic_struct_tag_typetType for a generic symbol, extends struct_tag_typet with a vector of java generic types
 Cjava_generic_typetClass to hold type with generic type arguments, for example java.util.List in either a reference of type List<Integer> or List<T> (here T must have been concretized already to create this object so technically it is an argument rather than parameter/variable, but in the symbol table this still shows as the parameter T)
 Cjava_implicitly_generic_class_typetType to hold a Java class that is implicitly generic, e.g., an inner class of a generic outer class or a derived class of a generic base class
 Cjava_method_typet
 Cjava_object_factory_parameterst
 Cjava_object_factoryt
 Cjava_qualifierst
 Cjava_simple_method_stubst
 Cjava_string_library_preprocesst
 Cjava_syntactic_difft
 Cjbmc_parse_optionst
 Cjdiff_languagest
 Cjdiff_parse_optionst
 Cjournalling_symbol_tabletA symbol table wrapper that records which entries have been updated/removedA caller can pass a journalling_symbol_tablet into a callee that is expected to mutate it somehow, then after it has run inspect the recording table's journal to determine what has changed more cheaply than examining every symbol
 Cjsil_builtin_code_typet
 Cjsil_convertt
 Cjsil_declarationt
 Cjsil_languaget
 Cjsil_parse_treet
 Cjsil_parsert
 Cjsil_spec_code_typet
 Cjsil_typecheckt
 Cjsil_union_typet
 Cjson_arrayt
 Cjson_falset
 Cjson_irept
 Cjson_nullt
 Cjson_numbert
 Cjson_objectt
 Cjson_parsert
 Cjson_stream_arraytProvides methods for streaming JSON arrays
 Cjson_stream_objecttProvides methods for streaming JSON objects
 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)
 Cjson_stringt
 Cjson_symtab_languaget
 Cjson_truet
 Cjsont
 Ck_inductiont
 Clanguage_entryt
 Clanguage_filest
 Clanguage_filet
 Clanguage_modulet
 Clanguage_uit
 Clanguaget
 Clazy_goto_functions_maptProvides a wrapper for a map of lazily loaded goto_functiont
 Clazy_goto_modeltA GOTO model that produces function bodies on demand
 Cld_cmdlinet
 Cld_modet
 Clet_exprtA let expression
 Clinker_script_mergetSynthesise definitions of symbols that are defined in linker scripts
 Clinkingt
 Clispexprt
 Clispsymbolt
 Cliteral_exprt
 Cliteralt
 Clocal_bitvector_analysist
 Clocal_cfgt
 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
 Clocalst
 Clshr_exprtLogical right shift
 Cmain_function_resultt
 Cmap_iteratortIterator which applies some given function f after each increment and returns its result on dereference
 Cmathematical_function_typetA type for mathematical functions (do not confuse with functions/methods in code)
 Cmember_designatort
 Cmember_exprtExtract member of struct or union
 Cmemory_model_baset
 Cmemory_model_psot
 Cmemory_model_sct
 Cmemory_model_tsot
 Cmerge_full_irept
 Cmerge_irept
 Cmerged_irep_hash
 Cmerged_irepst
 Cmerged_irept
 Cmerged_typetHolds a combination of types
 Cmessage_handlert
 CmessagetClass that provides messages with a built-in verbosity 'level'
 Cmethod_bytecodet
 Cmethod_handle_infot
 Cmini_bdd_applyt
 Cmini_bdd_mgrt
 Cmini_bdd_nodet
 Cmini_bddt
 Cminisat_prooft
 Cminus_exprtBinary minus
 Cmissing_outer_class_symbol_exceptiontAn exception that is raised checking whether a class is implicitly generic if a symbol for an outer class is missing
 Cmod_exprtModulo
 Cmonomialt
 Cmonotonic_timestampert
 Cms_cl_cmdlinet
 Cms_cl_modet
 Cms_cl_versiont
 Cms_link_cmdlinet
 Cms_link_modet
 Cmult_exprtBinary multiplication Associativity is not specified
 Cmulti_ary_exprtA base class for multi-ary expressions Associativity is not specified
 Cmulti_namespacetA multi namespace is essentially a namespace, with a list of namespaces
 Cmz_stream_s
 Cmz_zip_archive
 Cmz_zip_archive_file_stat
 Cmz_zip_archive_statet
 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
 Cname_and_type_infotCorresponds to the CONSTANT_NameAndType_info Structure Described in Java 8 specification 4.4.6
 Cnamespace_basetBasic interface for a namespace
 CnamespacetA namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in them
 Cnatural_loops_templatetMain driver for working out if a class (normally goto_programt) has any natural loops
 Cnatural_loopstA concretized version of natural_loops_templatet<const goto_programt, goto_programt::const_targett>
 Cnatural_typetNatural numbers including zero (mathematical integers, not bitvectors)
 Cnew_scopet
 Cnil_exprtThe NIL expression
 Cnil_typetThe NIL type, i.e., an invalid type, no value
 Cnon_byte_alignedt
 Cnon_const_array_sizet
 Cnon_const_byte_extraction_sizet
 Cnon_constant_widtht
 Cnondet_instruction_infotHolds information about any discovered nondet methods, with extreme type- safety
 Cnondet_symbol_exprtExpression to hold a nondeterministic choice
 Cnot_exprtBoolean negation
 Cnotequal_exprtDisequality
 Cnull_message_handlert
 Cnull_pointer_exprtThe null pointer constant
 Cnullary_exprtAn expression without operands
 Cnullptr_exceptiont
 Cnum_bitst
 Cnum_bitst< 0 >
 Cnum_bitst< 1 >
 Cnumeric_casttNumerical 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_descriptor_exprtSplit an expression into a base object and a (byte) offset
 Cobject_factory_parameterst
 Cobject_idt
 Coperator_entryt
 Coptionst
 Cor_exprtBoolean OR
 Cosx_fat_readert
 Coverflow_instrumentert
 Cparameter_assignmentst
 Cparameter_symboltSymbol table entry of function parameterThis is a symbol generated as part of type checking
 Cparse_floatt
 Cparse_options_baset
 CParser
 Cparsert
 Cpartial_order_concurrencyt
 Cpath_acceleratort
 Cpath_enumeratort
 Cpath_explorertSymbolic execution from a saved branch point
 Cpath_fifotFIFO save queue: paths are resumed in the order that they were saved
 Cpath_lifotLIFO save queue: depth-first search, try to finish paths
 Cpath_nodet
 Cpath_storagetStorage for symbolic execution paths to be resumed later
 Cpath_strategy_choosertFactory and information for path_storaget
 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
 Cpbs_dimacs_cnft
 Cplus_exprtThe plus expression Associativity is not specified
 Cpointee_address_equaltFunctor to check whether iterators from different collections point at the same object
 Cpointer_arithmetict
 Cpointer_logict
 Cpointer_typetThe pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they have a subtype)
 Cpoints_tot
 Cpolynomial_acceleratort
 Cpolynomialt
 Cpopcount_exprtThe popcount (counting the number of bits set to 1) expression
 Cpostconditiont
 Cpower_exprtExponentiation
 Cpreconditiont
 Cpredicate_exprtA base class for expressions that are predicates, i.e., Boolean-typed
 Cpreprocessort
 Cprintf_formattert
 Cprocedure_local_cfg_baset
 Cprocedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >
 Cprocedure_local_concurrent_cfg_baset
 Cprop_conv_solvertTO_BE_DOCUMENTED
 Cprop_convt
 Cprop_minimizetComputes a satisfying assignment of minimal cost according to a const function using incremental SAT
 Cproperties_criteriont
 Cproperty_checkert
 CproptTO_BE_DOCUMENTED
 Cqbf_bdd_certificatet
 Cqbf_bdd_coret
 Cqbf_quantort
 Cqbf_qube_coret
 Cqbf_qubet
 Cqbf_skizzo_coret
 Cqbf_skizzot
 Cqbf_squolem_coret
 Cqbf_squolemt
 Cqdimacs_cnft
 Cqdimacs_coret
 Cqualifierst
 Cquantifier_exprtA base class for quantifier expressions
 Crange_domain_baset
 Crange_domaint
 Crange_typetA type for subranges of integers
 CrangetA range is a pair of a begin and an end iterators
 Crational_typetUnbounded, signed rational numbers
 Crationalt
 Crd_range_domaintBecause the class is inherited from ai_domain_baset, its instance represents an element of a domain of the reaching definitions abstract interpretation analysis
 Creachability_slicert
 Creaching_definitions_analysist
 Creaching_definitiontIdentifies a GOTO instruction where a given variable is defined (i.e
 Creal_typetUnbounded, signed real numbers
 Crebuild_goto_start_function_baset
 Crecursion_set_entrytRecursion-set entry owner class
 Cref_expr_set_dt
 Cref_expr_sett
 Creference_counting
 Creference_typetThe reference type
 Crefined_string_exprt
 Crefined_string_typet
 Crem_exprtRemainder of division
 Cremove_asmt
 Cremove_calls_no_bodyt
 Cremove_const_function_pointerst
 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_java_newt
 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
 Creplication_exprtBit-vector replication
 Cresolution_prooft
 Cresolve_inherited_componentt
 Crestrictt
 Crw_guarded_range_set_value_sett
 Crw_range_set_value_sett
 Crw_range_sett
 Crw_set_baset
 Crw_set_functiont
 Crw_set_loct
 Crw_set_with_trackt
 Csafety_checkert
 Csaj_tabletProduce canonical ordering for associative and commutative binary operators
 Csat_path_enumeratort
 Csatcheck_booleforce_baset
 Csatcheck_booleforce_coret
 Csatcheck_booleforcet
 Csatcheck_cadicalt
 Csatcheck_glucose_baset
 Csatcheck_glucose_no_simplifiert
 Csatcheck_glucose_simplifiert
 Csatcheck_ipasirtInterface for generic SAT solver interface IPASIR
 Csatcheck_lingelingt
 Csatcheck_minisat1_baset
 Csatcheck_minisat1_coret
 Csatcheck_minisat1_prooft
 Csatcheck_minisat1t
 Csatcheck_minisat2_baset
 Csatcheck_minisat_no_simplifiert
 Csatcheck_minisat_simplifiert
 Csatcheck_picosatt
 Csatcheck_zchaff_baset
 Csatcheck_zchafft
 Csatcheck_zcoret
 Csave_scopet
 Cscratch_programt
 Cselect_pointer_typet
 Cshared_bufferst
 Csharing_maptA map implemented as a tree where subtrees can be shared between different maps
 Csharing_node_baset
 Csharing_node_innert
 Csharing_node_leaft
 Cshift_exprtA base class for shift operators
 Cshl_exprtLeft shift
 Cshow_goto_functions_jsont
 Cshow_goto_functions_xmlt
 Cside_effect_expr_function_calltA side_effect_exprt representation of a function call side effect
 Cside_effect_expr_nondettA side_effect_exprt that returns a non-deterministically chosen value
 Cside_effect_expr_throwtA side_effect_exprt representation of a side effect that throws an exception
 Cside_effect_exprtAn expression containing a side effect
 Csign_exprtSign of an expression Predicate is true if _op is negative, false otherwise
 Csignedbv_typetFixed-width bit-vector with two's complement interpretation
 Csimplify_exprt
 Cslicing_criteriont
 Csmall_maptMap from small integers to values
 Csmall_shared_pointeetA helper class to store use-counts of objects held by small shared pointers
 Csmall_shared_ptrtThis 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_two_way_pointeet
 Csmall_shared_two_way_ptrtThis class is similar to small_shared_ptrt and boost's intrusive_ptr
 Csmt2_convt
 Csmt2_dectDecision procedure interface for various SMT 2.x solvers
 Csmt2_format_containert
 Csmt2_message_handlert
 Csmt2_parsert
 Csmt2_solvert
 Csmt2_stringstreamt
 Csmt2_tokenizert
 Csmt2irept
 Csolver_factoryt
 Csource_locationt
 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_analysistAn instance of this class provides an assignment of unique numeric ID to each inserted reaching_definitiont instance
 Csparse_vectort
 Cssa_exprtExpression providing an SSA-renamed symbol of expressions
 Cstatic_analysis_baset
 Cstatic_analysist
 Cstatic_verifier_resultt
 Cstream_message_handlert
 Cstring_abstractiont
 Cstring_axiomst
 Cstring_builtin_function_with_no_evaltFunctions that are not yet supported in this class but are supported by string_constraint_generatort
 Cstring_builtin_functiontBase class for string functions that are built in the solver
 Cstring_concat_char_builtin_functiontAdding a character at the end of a string
 Cstring_concatenation_builtin_functiont
 Cstring_constantt
 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_creation_builtin_functiontString creation from other types
 Cstring_dependenciestKeep track of dependencies between strings
 Cstring_hash
 Cstring_insertion_builtin_functiontString inserting a string into another one
 Cstring_instrumentationt
 Cstring_not_contains_constrainttConstraints to encode non containement of strings
 Cstring_of_int_builtin_functiontString creation from integer types
 Cstring_ptr_hash
 Cstring_ptrt
 Cstring_refinementt
 Cstring_set_char_builtin_functiontSetting a character at a particular position of a string
 Cstring_test_builtin_functiontString test
 Cstring_to_lower_case_builtin_functiontConverting each uppercase character of Basic Latin and Latin-1 supplement to the corresponding lowercase character
 Cstring_to_upper_case_builtin_functiontConverting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding uppercase character
 Cstring_transformation_builtin_functiontString builtin_function transforming one string into another
 Cstring_typetString type
 Cstruct_exprtStruct constructor from list of elements
 Cstruct_tag_typetA struct tag type, i.e., struct_typet with an identifier
 Cstruct_typetStructure type, corresponds to C style structs
 Cstruct_union_typetBase type for structs and unions
 Cstructured_pool_entryt
 Cstub_global_initializer_factoryt
 Csubsumed_patht
 Csymbol_exprtExpression to hold a symbol (variable)
 Csymbol_factoryt
 Csymbol_generatortGeneration of fresh symbols of a given type
 Csymbol_table_basetThe symbol table base class interface
 Csymbol_table_buildertAuthor: Diffblue Ltd
 Csymbol_tabletThe symbol table
 Csymbol_typetA reference into the symbol table
 CsymboltSymbol table entry
 Csymex_bmct
 Csymex_configtConfiguration of the symbolic execution
 Csymex_coveraget
 Csymex_dereference_statet
 Csymex_level0tFunctor to set the level 0 renaming of SSA expressions
 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_renaming_leveltWrapper for a current_names map, which maps each identifier to an SSA expression and a counter
 Csymex_slice_by_tracet
 Csymex_slicet
 Csymex_target_equationtInheriting the interface of symex_targett this class represents the SSA form of the input program as a list of SSA_stept
 Csymex_targettThe interface of the target container for symbolic execution to record its symbolic steps into
 Csyntactic_difft
 Csystem_exceptiontThrown when some external system fails unexpectedly
 Csystem_library_symbolst
 Ctag_typetA tag-based type, i.e., typet with an identifier
 Ctaint_analysist
 Ctaint_parse_treet
 Ctdefl_compressor
 Ctdefl_output_buffer
 Ctdefl_sym_freq
 Ctemp_dirt
 Ctemplate_mapt
 Ctemplate_numberingt
 Ctemplate_parametert
 Ctemplate_typet
 Ctemporary_filet
 Cternary_exprtAn expression with three operands
 CtimestampertTimestamp class hierarchy
 Ctinfl_decompressor_tag
 Ctinfl_huff_table
 Cto_be_merged_irep_hash
 Cto_be_merged_irept
 Ctrace_automatont
 Ctrace_optionst
 CtranstTransition system, consisting of state invariant, initial state predicate, and transition predicate
 Ctrivial_functions_filtertFilters out trivial functions
 Ctrue_exprtThe Boolean constant true
 Ctvt
 Ctype_exprtAn expression denoting a type
 Ctype_symboltSymbol table entry describing a data typeThis is a symbol generated as part of type checking
 Ctype_with_subtypestType with multiple subtypes
 Ctype_with_subtypetType with a single subtype
 Ctypecast_exprtSemantic type conversion
 Ctypecheckt
 Ctypedef_typetA typedef
 CtypetThe type of an expression, extends irept
 Cui_message_handlert
 Cunary_exprtGeneric base class for unary expressions
 Cunary_minus_exprtThe unary minus expression
 Cunary_plus_exprtThe unary plus expression
 Cunary_predicate_exprtA base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argument
 Cuncaught_exceptions_analysistComputes in exceptions_map an overapproximation of the exceptions thrown by each method
 Cuncaught_exceptions_domaint
 Cunchecked_replace_symbolt
 Cunified_difft
 Cuninitialized_domaint
 Cuninitializedt
 Cunion_exprtUnion constructor from single element
 Cunion_find
 Cunion_find_replacetSimilar interface to union-find for expressions, with a function for replacing sub-expressions by their result for find
 Cunion_tag_typetA union tag type, i.e., union_typet with an identifier
 Cunion_typetThe union type
 Cunsigned_union_find
 Cunsignedbv_typetFixed-width bit-vector with unsigned binary interpretation
 Cunsupported_java_class_signature_exceptiontAn exception that is raised for unsupported class signature
 Cunsupported_operation_exceptiontThrown when we encounter an instruction, parameters to an instruction etc
 Cunwindsett
 Cupdate_exprtOperator to update elements in structs and arrays
 Cuser_input_error_exceptiont
 Cvalue_set_analysis_fit
 Cvalue_set_analysis_fivrnst
 Cvalue_set_analysis_fivrt
 Cvalue_set_analysis_templatet
 Cvalue_set_dereferencetWrapper for a function dereferencing pointer expressions using a value set
 Cvalue_set_domain_fit
 Cvalue_set_domain_fivrnst
 Cvalue_set_domain_fivrt
 Cvalue_set_domain_templatet
 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
 Cvector_exprtVector constructor from list of elements
 Cvector_typetThe vector type
 Cvisited_nodetA node type with an extra bit
 Cvoid_typetThe void type, the same as empty_typet
 Cw_guardst
 Cwall_clock_timestampert
 Cwith_exprtOperator to update elements in structs and arrays
 Cwrapper_goto_modeltClass providing the abstract GOTO model interface onto an unrelated symbol table and goto_functionst
 Cxml_edget
 Cxml_graph_nodet
 Cxml_interfacet
 Cxml_parse_treet
 Cxml_parsert
 Cxmlt
 Cxor_exprtBoolean XOR
 Cyy_buffer_state
 Cyy_trans_info
 Cyyalloc
 CYYSTYPE