cprover
Class List
Here are the classes, structs, unions and interfaces with brief descriptions:
[detail level 123]
 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
 Cabsolute_timet
 Cabstract_eventt
 Cacceleratet
 Cacceleration_utilst
 Caddress_of_exprtOperator to return the address of an object
 Cai_baset
 Cai_domain_baset
 Caig_nodet
 Caig_plus_constraintst
 Caig_prop_baset
 Caig_prop_constraintt
 Caig_prop_solvert
 Caigt
 Cait
 Call_paths_enumeratort
 Cand_exprtBoolean AND
 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_of_exprtArray constructor from single element
 Carray_typetArrays with given size
 Carrayst
 Cas86_cmdlinet
 Cas_cmdlinet
 Cas_modet
 Cashr_exprtArithmetic right shift
 Cassembler_parsert
 Cassert_criteriont
 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_type_eqt
 Cbasic_blockst
 Cbcc_cmdlinet
 Cbdd_exprtTO_BE_DOCUMENTED
 Cbinary_exprtA generic base class for binary expressions
 Cbinary_predicate_exprtA generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly two arguments
 Cbinary_relation_exprtA generic base class for relations, i.e., binary predicates
 Cbitand_exprtBit-wise AND
 Cbitnot_exprtBit-wise negation of bit-vectors
 Cbitor_exprtBit-wise OR
 Cbitvector_typetBase class of bitvector types
 Cbitxor_exprtBit-wise XOR
 Cbmc_all_propertiest
 Cbmc_covert
 Cbmct
 Cbool_typetThe proper Booleans
 Cboolbv_mapt
 Cboolbv_widtht
 Cboolbvt
 Cbv_arithmetict
 Cbv_cbmct
 Cbv_minimizet
 Cbv_minimizing_dect
 Cbv_pointerst
 Cbv_refinementt
 Cbv_spect
 Cbv_typetFixed-width bit-vector without numerical interpretation
 Cbv_utilst
 Cbyte_extract_big_endian_exprtTO_BE_DOCUMENTED
 Cbyte_extract_exprtTO_BE_DOCUMENTED
 Cbyte_extract_little_endian_exprtTO_BE_DOCUMENTED
 Cbyte_update_big_endian_exprtTO_BE_DOCUMENTED
 Cbyte_update_exprtTO_BE_DOCUMENTED
 Cbyte_update_little_endian_exprtTO_BE_DOCUMENTED
 Cbytecode_infot
 Cc_bit_field_typetType for c bit fields
 Cc_bool_typetThe C/C++ Booleans
 Cc_enum_tag_typetAn enum tag type
 Cc_enum_typetThe type of C enums
 Cc_qualifierst
 Cc_sizeoft
 Cc_storage_spect
 Cc_typecastt
 Cc_typecheck_baset
 Ccall_grapht
 Ccbmc_dimacst
 Ccbmc_parse_optionst
 Ccbmc_solverst
 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_methodst
 Cclass_hierarchyt
 Cclass_typetC++ class type
 Cclauset
 Cclobber_parse_optionst
 Ccmdlinet
 Ccnf_clause_list_assignmentt
 Ccnf_clause_listt
 Ccnf_solvert
 Ccnft
 Ccode_asmtAn inline assembler statement
 Ccode_asserttAn assertion
 Ccode_assigntAssignment
 Ccode_assumetAn assumption
 Ccode_blocktSequential composition
 Ccode_breaktA break for ‘for’ and ‘while’ loops
 Ccode_continuetA continue for ‘for’ and ‘while’ loops
 Ccode_contractst
 Ccode_deadtA removal of a local variable
 Ccode_decltA declaration of a local variable
 Ccode_dowhiletA ‘do while’ instruction
 Ccode_expressiontAn expression statement
 Ccode_fortA ‘for’ instruction
 Ccode_function_calltA function call
 Ccode_gototA ‘goto’ instruction
 Ccode_ifthenelsetAn if-then-else
 Ccode_labeltA label for branch targets
 Ccode_returntReturn from a function
 Ccode_skiptSkip
 Ccode_switch_casetA switch-case
 Ccode_switchtA ‘switch’ instruction
 Ccode_try_catchtA try/catch block
 Ccode_typetBase type of functions
 Ccode_whiletA ‘while’ instruction
 CcodetA statement in a programming language
 Ccompilet
 Ccomplex_exprtComplex constructor from a pair of numbers
 Ccomplex_typetComplex numbers made of pair of given subtype
 Cconcatenation_exprtConcatenation of bit-vector operands
 Cconcurrency_aware_ait
 Cconcurrency_aware_static_analysist
 Cconcurrency_instrumentationt
 Cconcurrent_cfg_baset
 Ccone_of_influencet
 CconfigtGlobally accessible architectural configuration
 Cconsole_message_handlert
 Cconst_expr_visitort
 Cconst_function_pointer_propagationt
 Cconst_graph_visitort
 Cconst_target_hash_templatet
 Cconstant_exprtA constant literal expression
 Cconstant_propagator_ait
 Cconstant_propagator_domaint
 Ccounterexample_beautificationt
 Ccout_message_handlert
 Ccover_goalstTry to cover some given set of goals incrementally
 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_library_entryt
 Ccustom_bitvector_analysist
 Ccustom_bitvector_domaint
 Ccvc_convt
 Ccvc_dect
 Ccvc_propt
 Ccvc_temp_filet
 Ccw_modet
 Ccycles_visitort
 Cdata
 Cdata_dpt
 Cdatat
 Cdecision_proceduret
 Cdecorated_symbol_exprtExpression to hold a symbol (variable)
 Cdep_edget
 Cdep_graph_domaint
 Cdep_nodet
 Cdependence_grapht
 Cdereference_callbacktTO_BE_DOCUMENTED
 Cdereference_exprtOperator to dereference a pointer
 CdereferencetTO_BE_DOCUMENTED
 Cdesignatort
 Cdimacs_cnf_dumpt
 Cdimacs_cnft
 Cdirtyt
 Cdisjunctive_polynomial_accelerationt
 Cdiv_exprtDivision (integer and real)
 Cdocument_propertiest
 Cdoes_remove_constt
 Cdomain_baset
 Cdott
 Cdplib_convt
 Cdplib_dect
 Cdplib_propt
 Cdplib_temp_filet
 Cdstring_hash
 Cdstringt
 Cdump_ct
 Cdynamic_object_exprtTO_BE_DOCUMENTED
 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_typetA generic enumeration type (not to be confused with C enums)
 Cequal_exprtEquality
 Cequalityt
 Cerror_baset
 Cerror_streamt
 Cescape_analysist
 Cescape_domaint
 Cevent_grapht
 Cexists_exprtAn exists expression
 Cexpanding_vectort
 Cexpr2cppt
 Cexpr2ct
 Cexpr2javat
 Cexpr2jsilt
 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
 Cfence_all_shared_aegt
 Cfence_all_sharedt
 Cfence_assert_insertert
 Cfence_insertert
 Cfence_user_def_insertert
 Cfence_volatilet
 Cfile
 Cfiledescriptor_streambuft
 Cfind_index_visitort
 Cfind_qvar_visitort
 Cfine_timet
 Cfixedbv_spect
 Cfixedbv_typetFixed-width bit-vector with signed fixed-point interpretation
 Cfixedbvt
 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_spect
 Cformat_token_listt
 Cformat_tokent
 Cfull_slicert
 Cfunction_application_exprtApplication of (mathematical) function
 Cfunction_modifiest
 Cfunctionst
 Cgcc_cmdlinet
 Cgcc_message_handlert
 Cgcc_modet
 Cglobal_may_alias_analysist
 Cglobal_may_alias_domaint
 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_fence_inserter_parse_optionst
 Cgoto_function_templatet
 Cgoto_functions_templatet
 Cgoto_functionst
 Cgoto_inlinet
 Cgoto_instrument_parse_optionst
 Cgoto_modelt
 Cgoto_program2codet
 Cgoto_program_coverage_recordt
 Cgoto_program_dereferencet
 Cgoto_program_templatetA generic container class for the GOTO intermediate representation of one function
 Cgoto_programtA specialization of goto_program_templatet over goto programs in which instructions have codet type
 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
 Chash_numbering
 Chavoc_loopst
 Cidentifiert
 Cieee_float_equal_exprtIEEE-floating-point equality
 Cieee_float_notequal_exprtIEEE floating-point disequality
 Cieee_float_op_exprtIEEE floating-point operations
 Cieee_float_spect
 Cieee_floatt
 Cif_exprtThe trinary if-then-else operator
 Cilpt
 Cimplies_exprtBoolean implication
 Cincomplete_array_typetArrays without size
 Cindex_designatort
 Cindex_exprtArray index operator
 Cinfinity_exprtAn expression denoting infinity
 Cinflate_state
 Cinode
 Cinstrumenter_pensievet
 Cinstrumentert
 Cinteger_typetUnbounded, signed integers
 Cinterpretert
 Cinterval_domaint
 Cinterval_templatet
 Cinv_object_storet
 Cinvariant_failedtA logic error, augmented with a distinguished field to hold a backtrace
 Cinvariant_propagationt
 Cinvariant_set_domaint
 Cinvariant_sett
 Cirep_full_eq
 Cirep_full_hash
 Cirep_full_hash_containert
 Cirep_hash
 Cirep_hash_container_baset
 Cirep_hash_containert
 Cirep_serializationt
 CireptBase class for tree-like data structures with sharing
 Cis_name_equalt
 Cis_predecessor_oft
 Cis_threaded_domaint
 Cis_threadedt
 Cis_virtual_name_equalt
 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
 Cjar_filet
 Cjar_poolt
 Cjava_bytecode_convert_classt
 Cjava_bytecode_convert_methodt
 Cjava_bytecode_languaget
 Cjava_bytecode_parse_treet
 Cjava_bytecode_parsert
 Cjava_bytecode_typecheckt
 Cjava_bytecode_vtable_factoryt
 Cjava_class_loader_limitt
 Cjava_class_loadert
 Cjava_object_factoryt
 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_stringt
 Cjson_truet
 Cjsont
 Ck_inductiont
 Clanguage_entryt
 Clanguage_filest
 Clanguage_filet
 Clanguage_modulet
 Clanguage_uit
 Clanguagest
 Clanguaget
 Cld_cmdlinet
 Clet_exprtA let expression
 Clinear_recurrencet
 Clinkingt
 Clispexprt
 Clispsymbolt
 Cliteral_exprt
 Cliteralt
 Cloc_reft
 Clocal_bitvector_analysist
 Clocal_cfgt
 Clocal_may_alias_factoryt
 Clocal_may_aliast
 Clocalst
 Clocst
 Cloct
 Cloop_accelerationt
 Clshr_exprtLogical right shift
 Cmain_function_resultt
 Cmember_designatort
 Cmember_exprtExtract member of struct or union
 Cmember_offset_iterator
 Cmemory_model_baset
 Cmemory_model_psot
 Cmemory_model_sct
 Cmemory_model_tsot
 Cmerge_full_irept
 Cmerge_irept
 Cmerged_irep_hash
 Cmerged_irepst
 Cmerged_irept
 Cmessage_handlert
 Cmessaget
 Cmini_bdd_applyt
 Cmini_bdd_mgrt
 Cmini_bdd_nodet
 Cmini_bddt
 Cminisat_prooft
 Cminus_exprtBinary minus
 Cmip_vart
 Cmm2cppt
 Cmm_parsert
 Cmmcc_parse_optionst
 Cmod_exprtBinary modulo
 Cmonomialt
 Cms_cl_cmdlinet
 Cms_cl_modet
 Cmult_exprtBinary multiplication
 Cmulti_ary_exprtA generic base class for multi-ary expressions
 Cmulti_namespacet
 Cmz_stream_s
 Cmz_zip_archive
 Cmz_zip_archive_file_stat
 Cmz_zip_array
 Cmz_zip_internal_state_tag
 Cmz_zip_writer_add_state
 Cnamespace_baset
 CnamespacetTO_BE_DOCUMENTED
 Cnatural_loops_templatet
 Cnatural_loopst
 Cnatural_typetNatural numbers (which include zero)
 Cnew_scopet
 Cnil_exprtThe NIL expression
 Cnil_typetThe NIL type
 Cnot_exprtBoolean negation
 Cnotequal_exprtInequality
 Cnull_message_handlert
 Cnull_pointer_exprtThe null pointer constant
 Cnullptr_exceptiont
 Cnumbering
 Cobject_descriptor_exprtSplit an expression into a base object and a (byte) offset
 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_options_baset
 CParser
 Cparsert
 Cpartial_order_concurrencyt
 Cpath_accelerationt
 Cpath_acceleratort
 Cpath_enumeratort
 Cpath_nodet
 Cpath_replayt
 Cpath_searcht
 Cpath_symex_historyt
 Cpath_symex_statet
 Cpath_symex_step_reft
 Cpath_symex_stept
 Cpath_symext
 Cpatternt
 Cpbs_dimacs_cnft
 Cpipe_streamt
 Cplus_exprtThe plus expression
 Cpointer_arithmetict
 Cpointer_logict
 Cpointer_typetThe pointer type
 Cpoints_tot
 Cpolynomial_acceleratort
 Cpolynomialt
 Cpostconditiont
 Cpower_exprtExponentiation
 Cpreconditiont
 Cpredicate_exprtA generic 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, unsigned >
 Cprocedure_local_concurrent_cfg_baset
 Cprop_assignmenttTO_BE_DOCUMENTED
 Cprop_conv_solvertTO_BE_DOCUMENTED
 Cprop_conv_storet
 Cprop_convt
 Cprop_minimizetComputes a satisfying assignment of minimal cost according to a const function using incremental SAT
 Cprop_wrappert
 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
 Crange_domain_baset
 Crange_domaint
 Crange_typetA type for subranges of integers
 Crational_typetUnbounded, signed rational numbers
 Crationalt
 Crd_range_domaint
 Creachability_slicert
 Creaching_definitions_analysist
 Creaching_definitiont
 Creal_typetUnbounded, signed real numbers
 Crecursion_countert
 Cref_expr_set_dt
 Cref_expr_sett
 Creference_counting
 Creference_typetThe reference type
 Crefined_string_typet
 Crem_exprtRemainder of division
 Cremove_asmt
 Cremove_const_function_pointerst
 Cremove_exceptionst
 Cremove_function_pointerst
 Cremove_instanceoft
 Cremove_returnst
 Cremove_static_init_loopst
 Cremove_virtual_functionst
 Crename_symbolt
 Creplace_symbol_extt
 Creplace_symbolt
 Creplication_exprtBit-vector replication
 Cresolution_prooft
 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
 Csafe_pointer
 Csafety_checkert
 Csaj_tabletProduce canonical ordering for associative and commutative binary operators
 Csat_path_enumeratort
 Csatcheck_booleforce_baset
 Csatcheck_booleforce_coret
 Csatcheck_booleforcet
 Csatcheck_glucose_baset
 Csatcheck_glucose_no_simplifiert
 Csatcheck_glucose_simplifiert
 Csatcheck_limmatt
 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_precosatt
 Csatcheck_smvsat_coret
 Csatcheck_smvsat_interpolatort
 Csatcheck_smvsatt
 Csatcheck_zchaff_baset
 Csatcheck_zchafft
 Csatcheck_zcoret
 Csave_scopet
 Cscratch_programt
 Cshared_bufferst
 Csharing_mapt
 Csharing_nodet
 Cshift_exprtA base class for shift operators
 Cshl_exprtLeft shift
 Cshow_goto_functions_jsont
 Cshow_goto_functions_xmlt
 Cside_effect_expr_catchtA side effect that pushes/pops a catch handler
 Cside_effect_expr_function_calltA function call side effect
 Cside_effect_expr_nondettA side effect that returns a non-deterministically chosen value
 Cside_effect_expr_throwtA side effect that throws an exception
 Cside_effect_exprtAn expression containing a side effect
 Csign_exprtSign of an expression
 Csignedbv_typetFixed-width bit-vector with two's complement interpretation
 Csimple_insertiont
 Csimplify_exprt
 Cslicing_criteriont
 Csmt1_convt
 Csmt1_dectDecision procedure interface for various SMT 1.x solvers
 Csmt1_propt
 Csmt1_temp_filet
 Csmt2_convt
 Csmt2_dectDecision procedure interface for various SMT 2.x solvers
 Csmt2_parsert
 Csmt2_propt
 Csmt2_stringstreamt
 Csmt2_temp_filet
 Csmt2irept
 Csorted_vector
 Csource_locationt
 Csparse_bitvector_analysist
 Cssa_exprtExpression providing an SSA-renamed symbol of expressions
 Cstatic_analysis_baset
 Cstatic_analysist
 Cstatic_analyzert
 Cstream_message_handlert
 Cstring_abstractiont
 Cstring_constantt
 Cstring_constraint_generatort
 Cstring_constraintt
 Cstring_containert
 Cstring_exprt
 Cstring_hash
 Cstring_instrumentationt
 Cstring_not_contains_constraintt
 Cstring_ptr_hash
 Cstring_ptrt
 Cstring_refinementt
 Cstring_typetTO_BE_DOCUMENTED
 Cstruct_exprtStruct constructor from list of elements
 Cstruct_tag_typetA struct tag type
 Cstruct_typetStructure type
 Cstruct_union_typetBase type of C structs and unions, and C++ classes
 Csubsumed_patht
 Csymbol_exprtExpression to hold a symbol (variable)
 Csymbol_factoryt
 Csymbol_tabletThe symbol table
 Csymbol_typetA reference into the symbol table
 CsymboltSymbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet
 Csymex_bmct
 Csymex_coveraget
 Csymex_dereference_statet
 Csymex_parse_optionst
 Csymex_slice_by_tracet
 Csymex_slicet
 Csymex_target_equationt
 Csymex_targett
 Csyntactic_difft
 Ctag_typetA generic tag-based type
 Ctaint_analysist
 Ctaint_parse_treet
 Ctarget_to_loc_mapt
 Ctdefl_compressor
 Ctdefl_output_buffer
 Ctdefl_sym_freq
 Ctemp_dirt
 Ctemp_working_dirt
 Ctemplate_mapt
 Ctemplate_parametert
 Ctemplate_typet
 Ctemporary_filet
 Ctime_periodt
 Ctimert
 Ctinfl_decompressor_tag
 Ctinfl_huff_table
 Cto_be_merged_irep_hash
 Cto_be_merged_irept
 Ctrace_automatont
 CtranstA transition system, consisting of state invariant, initial state predicate, and transition predicate
 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_subtypest
 Ctype_with_subtypet
 Ctypecast_exprtSemantic type conversion
 Ctypecheckt
 CtypetThe type of an expression
 Cui_message_handlert
 Cunary_exprtGeneric base class for unary expressions
 Cunary_minus_exprtThe unary minus expression
 Cunary_predicate_exprtA generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly one argument
 Cunified_difft
 Cuninitialized_domaint
 Cuninitializedt
 Cunion_exprtUnion constructor from single element
 Cunion_find
 Cunion_tag_typetA union tag type
 Cunion_typetThe union type
 Cunsigned_union_find
 Cunsignedbv_typetFixed-width bit-vector with unsigned binary interpretation
 Cupdate_exprtOperator to update elements in structs and arrays
 Cvalue_set_analysis_fit
 Cvalue_set_analysis_fivrnst
 Cvalue_set_analysis_fivrt
 Cvalue_set_analysist
 Cvalue_set_dereferencetTO_BE_DOCUMENTED
 Cvalue_set_domain_fit
 Cvalue_set_domain_fivrnst
 Cvalue_set_domain_fivrt
 Cvalue_set_domaint
 Cvalue_set_fit
 Cvalue_set_fivrnst
 Cvalue_set_fivrt
 Cvalue_setst
 Cvalue_sett
 Cvar_mapt
 Cvector_exprtVector constructor from list of elements
 Cvector_typetA constant-size array type
 Cvisited_nodetA node type with an extra bit
 Cvoid_typetThe void type
 Cw_guardst
 Cwith_exprtOperator to update elements in structs and arrays
 Cxml_edget
 Cxml_goto_function_convertt
 Cxml_goto_program_convertt
 Cxml_graph_nodet
 Cxml_interfacet
 Cxml_irep_convertt
 Cxml_parse_treet
 Cxml_parsert
 Cxml_symbol_convertt
 Cxmlt
 Cyy_buffer_state
 Cyy_trans_info
 Cyyalloc
 CYYSTYPE
 Czero_initializert