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
 CahistoricaltThe common case of history is to only care about where you are now, not how you got there! Invariants are not checkable due to C++..
 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_domain_factory_default_constructort
 Cai_domain_factoryt
 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_history_factory_default_constructortAn easy factory implementation for histories that don't need parameters
 Cai_recursive_interproceduralt
 Cai_storage_basetThis is the basic interface for storing domains
 CaitAit supplies three of the four components needed: an abstract interpreter (in this case handling function calls via recursion), a history factory (using the simplest possible history objects) and storage (one domain per location)
 Call_paths_enumeratort
 Call_properties_verifier_with_fault_localizationtRequires an incremental goto checker that is a goto_trace_providert and fault_localization_providert
 Call_properties_verifier_with_trace_storaget
 Call_properties_verifiert
 Callocate_objectst
 Calready_typechecked_exprt
 Calready_typechecked_typet
 Canalysis_exceptiontThrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an error)
 Cancestry_resulttResult of an attempt to find ancestor information about two nodes
 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_comprehension_exprtExpression to define a mapping from an argument (index) to elements
 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
 CassignmenttAssignment from the rhs value to the lhs variable
 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_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
 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 whose two operands have the same type
 Cbinding_exprtA base class for variable bindings (quantifiers, let, lambda)
 Cbitand_exprtBit-wise AND
 Cbitnot_exprtBit-wise negation of bit-vectors
 Cbitor_exprtBit-wise OR
 Cbitvector_typetBase class of fixed-width bit-vector types
 Cbitxor_exprtBit-wise XOR
 Cbool_typetThe Boolean type
 Cboolbv_mapt
 Cboolbv_widtht
 Cboolbvt
 Cboundst
 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_exprtExpression of type type extracted from some object op starting at position offset (given in number of bytes)
 Cbyte_update_exprtExpression corresponding to op() where the bytes starting at position offset (given in number of bytes) have been updated with value
 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_test_input_generatort
 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_stack_history_factoryt
 Ccall_stack_historytRecords the call stack Care must be taken when using this on recursive code; it will need the domain to be capable of limiting the recursion
 Ccall_stackt
 Ccall_validate_fullt
 Ccall_validatet
 Ccasting_replace_symbolt
 Ccbmc_invariants_should_throwtHelper to enable invariant throwing as above bounded to an object lifetime:
 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_templatetDominator graph
 Ccfg_instruction_to_dense_integertFunctor 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
 Cchange_impactt
 Ccharacter_refine_preprocesst
 Ccheck_call_sequencet
 Cci_lazy_methods_neededt
 Cci_lazy_methodst
 Ccl_message_handlert
 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_method_descriptor_exprtAn expression describing a method on a class
 Cclass_typetClass type
 Cclauset
 Ccmdlinet
 Ccnf_clause_list_assignmentt
 Ccnf_clause_listt
 Ccnf_solvert
 Ccnft
 Ccode_asm_gcctcodet representation of an inline assembler statement, for the gcc flavor
 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_bodytThis class is used to interface between a language frontend and goto-convert – it communicates the identifiers of the parameters of a function or method
 Ccode_function_calltcodet representation of a function call statement
 Ccode_gcc_switch_case_rangetcodet representation of a switch-case, i.e. a case statement within a switch
 Ccode_gototcodet representation of a goto statement
 Ccode_ifthenelsetcodet representation of an if-then-else statement
 Ccode_inputtA codet representing the declaration that an input of a particular description has a value which corresponds to the value of a given expression (or expressions)
 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_outputtA codet representing the declaration that an output of a particular description has a value which corresponds to the value of a given expression (or expressions)
 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
 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
 Ccode_without_referencestCode that should not contain reference
 CcodetData structure for representing an arbitrary statement in a program
 Ccompare_base_name_and_descriptort
 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
 Ccomplexity_limitertSymex complexity module
 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_aitBase class for concurrency-aware abstract interpretation
 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
 Cconflict_providert
 Cconsole_message_handlert
 Cconst_depth_iteratort
 Cconst_expr_visitort
 Cconst_target_hash
 Cconst_unique_depth_iteratort
 Cconstant_exprtA constant literal expression
 Cconstant_interval_exprtRepresents an interval of values
 Cconstant_propagator_ait
 Cconstant_propagator_domaint
 Cconstant_propagator_is_constantt
 Cconstructor_oftA type of functor which wraps around the set of constructors of a type
 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_goals_verifier_with_trace_storaget
 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
 Cdefault_trace_stept
 Cdense_integer_maptA 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
 Cdep_edget
 Cdep_graph_domain_factorytThis ensures that all domains are constructed with the node ID that links them to the graph part of the dependency graph
 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
 Cdeserialization_exceptiontThrown when failing to deserialize a value from some low level format, like JSON or raw bytes
 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
 Cdestructt< 0, pointee_baset, Ts... >
 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
 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
 Cdiv_exprtDivision
 Cdjb_manglertMangle identifiers by hashing their working directory with djb2 hash
 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
 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_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
 Cexpr2stltClass for saving the internal state of the conversion process
 Cexpr_initializert
 Cexpr_protectedtBase class for all expressions
 Cexpr_querytWrapper 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
 Cexpr_visitort
 CexprtBase class for all expressions
 Cexternal_satt
 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
 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
 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
 Cfile_filtert
 Cfile_name_manglertMangle identifiers by including their filename
 Cfilter_iteratortIterator which only stops at elements for which some given function f is true
 Cfixed_keys_map_wrappert
 Cfixedbv_spect
 Cfixedbv_typetFixed-width bit-vector with signed fixed-point interpretation
 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
 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_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
 Cforward_list_as_maptImplementation of map-like interface using a forward list
 CframetStack frames – these are used for function calls and for exceptions
 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_call_harness_generatortFunction harness generator that for a specified goto-function generates a harness that sets up its arguments and calls it
 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
 Cfunction_name_manglertMangles the names in an entire program and its symbol table
 Cfunction_pointer_restrictionst
 Cfunctionst
 Cgcc_cmdlinet
 Cgcc_message_handlert
 Cgcc_modet
 Cgcc_versiont
 Cgdb_apitInterface for running and querying GDB
 Cgdb_interaction_exceptiont
 Cgdb_value_extractortInterface for extracting values from GDB (building on gdb_apit)
 Cgenerate_function_bodies_errort
 Cgenerate_function_bodiestBase class for replace_function_body implementations
 Cgeneric_parameter_specialization_map_keyst
 Cgeneric_parameter_specialization_maptAuthor: Diffblue Ltd
 Cget_typetGet the type with the given index in the parameter pack
 Cget_virtual_calleest
 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_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_harness_generator_factorytHelper to select harness type by name
 Cgoto_harness_generatort
 Cgoto_harness_parse_optionst
 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_model_validation_optionst
 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_statetContainer for data that varies per program point, e.g
 Cgoto_symex_fault_localizert
 Cgoto_symex_is_constantt
 Cgoto_symex_property_decidertProvides management of goal variables that encode properties
 Cgoto_symex_statetCentral data structure: state
 Cgoto_symextThe main class for the forward symbolic simulator
 Cgoto_trace_constant_pointer_exprtVariety of constant expression only used in the context of a GOTO trace, to give both the numeric value and the symbolic value of a pointer, e.g
 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
 Cgraph_nodetThis class represents a node in a directed graph
 Cgraphml_witnesst
 Cgraphmlt
 CgraphtA generic directed graph with a parametric node type
 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
 Cguarded_range_domaint
 Chardness_collectort
 Chavoc_generate_function_bodiest
 Chavoc_loopst
 Chistory_sensitive_storaget
 Cidentifiert
 Cidentity_functortIdentity functor. When we use C++20 this can be replaced with std::identity
 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
 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
 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_designatort
 Cindex_exprtArray index operator
 Cindex_set_pairt
 Cinfinity_exprtAn expression denoting infinity
 Cinfix_opt
 Cinflate_state
 Cinode
 Cinsert_final_assert_falset
 Cinstrumenter_pensievet
 Cinstrumentert
 Cinteger_bitvector_typetFixed-width bit-vector representing a signed or unsigned integer
 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
 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
 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_failure_containingtAuthor: Diffblue Ltd
 Cinvariant_propagationt
 Cinvariant_set_domain_factorytPass the necessary arguments to the invariant_set_domaint's when constructed
 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
 CireptThere are a large number of kinds of tree structured or tree-like data in CPROVER
 Cis_constanttDetermine whether an expression is constant
 Cis_dynamic_object_exprtEvaluates to true if the operand is a pointer to a dynamic object
 Cis_invalid_pointer_exprt
 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_boxed_type_infotReturn type for get_boxed_type_info_by_name
 Cjava_bytecode_convert_classt
 Cjava_bytecode_convert_methodt
 Cjava_bytecode_instrumentt
 Cjava_bytecode_language_optionst
 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_parameter_tagtClass to hold a Java generic type parameter (also called type variable), e.g., T in List<T>
 Cjava_generic_parametertReference that points to a java_generic_parameter_tagt
 Cjava_generic_struct_tag_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_generic_typetReference that points to a java_generic_struct_tag_typet
 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_instanceof_exprt
 Cjava_method_typet
 Cjava_multi_path_symex_checkert
 Cjava_multi_path_symex_only_checkert
 Cjava_object_factory_parameterst
 Cjava_object_factoryt
 Cjava_primitive_type_infotReturn type for get_java_primitive_type_info
 Cjava_qualifierst
 Cjava_reference_typetThis is a specialization of reference_typet
 Cjava_simple_method_stubst
 Cjava_single_path_symex_checkert
 Cjava_single_path_symex_only_checkert
 Cjava_string_library_preprocesst
 Cjava_string_literal_exprt
 Cjava_syntactic_difft
 Cjbmc_parse_optionst
 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
 Clabelt
 Clanguage_entryt
 Clanguage_filest
 Clanguage_filet
 Clanguage_modulet
 Clanguaget
 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
 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
 Clazyt
 Cld_cmdlinet
 Cld_modet
 Clet_exprtA let expression
 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
 Clexical_loops_templatetMain driver for working out if a class (normally goto_programt) has any lexical loops
 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
 Clinked_loop_analysist
 Clinker_script_mergetSynthesise definitions of symbols that are defined in linker scripts
 Clinkingt
 Clispexprt
 Clispsymbolt
 Cliteral_exprt
 Cliteralt
 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_control_flow_history_factoryt
 Clocal_control_flow_historytWhether we track forwards and / or backwards jumps is compile-time fixed as it does not need to be variable and because there may be a lot of history objects created
 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
 Clocation_sensitive_storagetThe most conventional storage; one domain per location
 Cloop_analysist
 Cloop_templatetA loop, specified as a set of instructions
 Cloop_with_parent_analysis_templatet
 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)
 Cmax_exprt+∞ upper bound for intervals
 Cmember_designatort
 Cmember_exprtExtract member of struct or union
 Cmemory_analyzer_parse_optionst
 Cmemory_model_baset
 Cmemory_model_psot
 Cmemory_model_sct
 Cmemory_model_tsot
 Cmemory_snapshot_harness_generatortGenerates a harness which first assigns global variables with values from a given memory snapshot and then calls a specified function
 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
 Cmin_exprt-∞ upper bound for intervals
 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
 Cmulti_path_symex_checkertPerforms a multi-path symbolic execution using goto-symex and calls a SAT/SMT solver to check the status of the properties
 Cmulti_path_symex_only_checkert
 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
 CnfatVery simple NFA implementation Not super performant, but should be good enough for our purposes
 Cnil_exprtThe NIL expression
 Cno_unique_unimplemented_method_exceptiont
 Cnon_sharing_treetBase class for tree-like data structures without sharing
 Cnondet_instruction_infotHolds information about any discovered nondet methods, with extreme type- safety
 Cnondet_symbol_exprtExpression to hold a nondeterministic choice
 Cnondet_volatilet
 Cnot_exprtBoolean negation
 Cnotequal_exprtDisequality
 Cnull_message_handlert
 Cnull_pointer_exprtThe null pointer constant
 Cnullary_exprtAn expression without operands
 Cnullptr_exceptiont
 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_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_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
 Cosx_mach_o_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_concurrencytBase class for implementing memory models via additional constraints for SSA equations
 Cpath_acceleratort
 Cpath_enumeratort
 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
 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
 Cprefix_filtertProvides filtering of strings vai inclusion/exclusion lists of prefixes
 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_solvert
 Cprop_convt
 Cprop_minimizetComputes a satisfying assignment of minimal cost according to a const function using incremental SAT
 Cproperties_criteriont
 Cproperty_infot
 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_domain_factorytThis ensures that all domains are constructed with the appropriate pointer back to the analysis engine itself
 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
 Crecursion_set_entrytRecursion-set entry owner class
 Crecursive_initialization_configt
 Crecursive_initializationtClass for generating initialisation code for compound structures
 Cref_count_iftUsed in tree_nodet for activating or not reference counting
 Cref_count_ift< true >
 Cref_expr_set_dt
 Cref_expr_sett
 Creference_allocationtAllocation code which contains a reference
 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
 CrenamedtWrapper for expressions or types which have been renamed up to a given level
 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
 Creturn_value_visitortPredicate to be used with the exprt::visit() function
 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
 Csese_region_analysist
 Cshared_bufferst
 Csharing_maptA map implemented as a tree where subtrees can be shared between different maps
 Csharing_nodet
 Csharing_treetBase class for tree-like data structures with sharing
 Cshift_exprtA base class for shift operators
 Cshl_exprtLeft shift
 Cshow_goto_functions_jsont
 Cshow_goto_functions_xmlt
 Cside_effect_expr_assigntA side_effect_exprt that performs an assignment
 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_statement_expressiontA side_effect_exprt that contains a statement
 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
 Csingle_function_filtert
 Csingle_loop_incremental_symex_checkertPerforms a multi-path symbolic execution using goto-symex that incrementally unwinds a given loop and calls a SAT/SMT solver to check the status of the properties after each iteration
 Csingle_path_symex_checkertUses goto-symex to symbolically execute each path in the goto model and calls a solver to find property violations
 Csingle_path_symex_only_checkertUses goto-symex to generate a symex_target_equationt for each path
 Cslicing_criteriont
 Csmall_maptMap from small integers to values
 Csmall_shared_n_way_pointee_baset
 Csmall_shared_n_way_ptrtThis class is similar to small_shared_ptrt and boost's intrusive_ptr
 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
 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
 Csolver_hardnesstA structure that facilitates collecting the complexity statistics from a decision procedure
 Csolver_resource_limitst
 Csource_linest
 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_assignment_stept
 Cssa_exprtExpression providing an SSA-renamed symbol of expressions
 CSSA_steptSingle SSA step in the equation
 Cstack_decision_proceduret
 Cstatement_list_languagetImplements the language interface for the Statement List language
 Cstatement_list_parse_treetIntermediate representation of a parsed Statement List file before converting it into a goto program
 Cstatement_list_parsertResponsible for starting the parse process and to translate the result into a statement_list_parse_treet
 Cstatement_list_typechecktClass for encapsulating the current state of the type check
 Cstatic_analysis_baset
 Cstatic_analysist
 Cstatic_verifier_resultt
 Cstop_on_fail_verifier_with_fault_localizationtStops when the first failing property is found and localizes the fault Requires an incremental goto checker that is a goto_trace_providert and fault_localization_providert
 Cstop_on_fail_verifiertStops when the first failing property is found
 Cstream_message_handlert
 Cstring_abstractiontReplace all uses of char * by a struct that carries that string, and also the underlying allocation and the C string length
 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_format_builtin_functiontBuilt-in function for String.format()
 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_data_entryt
 Cstructured_datatA way of representing nested key/value data
 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
 CsymboltSymbol table entry
 Csymex_assigntFunctor for symex assignment
 Csymex_bmc_incremental_one_loopt
 Csymex_bmct
 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_dereference_statetCallback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value sets (from goto-symex's working value set) and retrieve or create failed symbols on demand
 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_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
 Csymtab2gb_parse_optionst
 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_parameter_symbol_typetTemplate parameter symbol that is a type
 Ctemplate_parametert
 Ctemplate_typet
 Ctemporary_filet
 Cternary_exprtAn expression with three operands
 Ctest_inputst
 CtimestampertTimestamp class hierarchy
 Ctinfl_decompressor_tag
 Ctinfl_huff_table
 Cto_be_merged_irep_hash
 Cto_be_merged_irept
 Ctrace_automatont
 Ctrace_map_storaget
 Ctrace_optionstOptions for printing the trace using show_goto_trace
 CtranstTransition system, consisting of state invariant, initial state predicate, and transition predicate
 Ctree_nodetA node with data in a tree, it contains:
 Ctrivial_functions_filtertFilters out trivial functions
 Ctrue_exprtThe Boolean constant true
 Ctuple_exprt
 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
 Cuninitialized_typet
 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_templatetThis template class implements a data-flow analysis which keeps track of what values different variables might have at different points in the program
 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_templatetThis is the domain for a value set analysis
 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
 Cw_guardst
 Cwall_clock_timestampert
 Cwith_exprtOperator to update elements in structs and arrays
 Cwitness_providertAn implementation of incremental_goto_checkert may implement this interface to provide GraphML witnesses
 Cwrapper_goto_modeltClass providing the abstract GOTO model interface onto an unrelated symbol table and goto_functionst
 Cxml_edget
 Cxml_graph_nodet
 Cxml_parse_treet
 Cxml_parsert
 Cxmlt
 Cxor_exprtBoolean XOR
 Czip_iteratortZip two ranges to make a range of pairs