| ►Ndetail | |
| Calways_falset | |
| Cexpr_dynamic_cast_return_typet | |
| Cexpr_try_dynamic_cast_return_typet | |
| ►Nrequire_goto_statements | |
| Cno_decl_found_exceptiont | |
| Cpointer_assignment_locationt | |
| ►Nrequire_parse_tree | |
| Cexpected_instructiont | |
| ►Nrequire_type | |
| Cexpected_type_argumentt | |
| ►Nstd | STL namespace |
| Chash< dstringt > | Default hash function of dstringt for use with STL containers |
| Chash< string_not_contains_constraintt > | |
| C__CPROVER_jsa_abstract_heap | |
| C__CPROVER_jsa_abstract_node | Abstract nodes may assume any of a set of pre-defined values (value_ref to abstract_ranget) |
| C__CPROVER_jsa_abstract_range | Set of pre-defined, possible values for abstract nodes |
| C__CPROVER_jsa_concrete_node | Concrete node with explicit value |
| C__CPROVER_jsa_iterator | Iterators point to a node and give the relative index within that node |
| C__CPROVER_pipet | |
| C_rw_set_loct | |
| Cabs_exprt | Absolute value |
| Cabstract_eventt | |
| Cabstract_goto_modelt | Abstract interface to eager or lazy GOTO models |
| Cacceleratet | |
| ►Cacceleration_utilst | |
| Cpolynomial_array_assignmentt | |
| ►Caddress_of_aware_replace_symbolt | Replace symbols with constants while maintaining syntactically valid expressions |
| Cset_require_lvalue_and_backupt | |
| Caddress_of_exprt | Operator to return the address of an object |
| Caggressive_slicert | The 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_baset | The basic interface of an abstract interpreter |
| Cai_domain_baset | The interface offered by a domain, allows code to manipulate domains without knowing their exact type |
| Cait | |
| Call_paths_enumeratort | |
| Canalysis_exceptiont | Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an error) |
| Cand_exprt | Boolean 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_exprt | Array constructor from list of elements |
| Carray_list_exprt | Array constructor from a list of index-element pairs Operands are index/value pairs, alternating |
| Carray_of_exprt | Array constructor from single element |
| Carray_poolt | Correspondance between arrays and pointers string representations |
| Carray_string_exprt | |
| Carray_typet | Arrays with given size |
| ►Carrayst | |
| Carray_equalityt | |
| Clazy_constraintt | |
| Cas86_cmdlinet | |
| Cas_cmdlinet | |
| Cas_modet | |
| Cashr_exprt | Arithmetic 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_symbolt | Internally 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_exprt | TO_BE_DOCUMENTED |
| Cbinary_exprt | A base class for binary expressions |
| Cbinary_predicate_exprt | A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two arguments |
| Cbinary_relation_exprt | A base class for relations, i.e., binary predicates |
| Cbitand_exprt | Bit-wise AND |
| Cbitnot_exprt | Bit-wise negation of bit-vectors |
| Cbitor_exprt | Bit-wise OR |
| Cbitvector_conversion_exceptiont | |
| Cbitvector_typet | Base class of fixed-width bit-vector types |
| Cbitxor_exprt | Bit-wise XOR |
| ►Cbmc_all_propertiest | |
| Cgoalt | |
| ►Cbmc_covert | |
| ►Cgoalt | |
| Cinstancet | |
| Ctestt | |
| Cbmct | Bounded model checking or path exploration for goto-programs |
| Cbool_typet | The Boolean type |
| ►Cboolbv_mapt | |
| Cmap_bitt | |
| Cmap_entryt | |
| ►Cboolbv_widtht | |
| Centryt | |
| Cmembert | |
| ►Cboolbvt | |
| Cquantifiert | |
| Cbswap_exprt | The byte swap expression |
| Cbv_arithmetict | |
| Cbv_dimacst | |
| Cbv_endianness_mapt | Map bytes according to the configured endianness |
| Cbv_minimizet | |
| Cbv_minimizing_dect | |
| ►Cbv_pointerst | |
| Cpostponedt | |
| ►Cbv_refinementt | |
| Capproximationt | |
| Cconfigt | |
| Cinfot | |
| Cbv_spect | |
| Cbv_typet | Fixed-width bit-vector without numerical interpretation |
| Cbv_utilst | |
| Cbyte_extract_exprt | TO_BE_DOCUMENTED |
| Cbyte_update_exprt | TO_BE_DOCUMENTED |
| Cbytecode_infot | |
| Cc_bit_field_typet | Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they have a subtype) |
| Cc_bool_typet | The C/C++ Booleans |
| Cc_enum_tag_typet | C enum tag type, i.e., c_enum_typet with an identifier |
| ►Cc_enum_typet | The type of C enums |
| Cc_enum_membert | |
| Cc_object_factory_parameterst | |
| Cc_qualifierst | |
| Cc_storage_spect | |
| Cc_typecastt | |
| Cc_typecheck_baset | |
| Ccall_checkt | |
| ►Ccall_grapht | A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection |
| Cdirected_grapht | Directed graph representation of this call graph |
| Cedge_with_callsitest | Edge of the directed graph representation of this call graph |
| Cfunction_nodet | Node of the directed graph representation of this call graph |
| Ccall_validate_fullt | |
| Ccall_validatet | |
| Ccasting_replace_symbolt | |
| Ccbmc_parse_optionst | |
| Ccerr_message_handlert | |
| Ccfg_base_nodet | |
| ►Ccfg_baset | A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO program |
| Centry_mapt | |
| ►Ccfg_dominators_templatet | |
| Cnodet | |
| Cchange_impactt | |
| Ccharacter_refine_preprocesst | |
| ►Ccheck_call_sequencet | |
| Ccall_stack_entryt | |
| Cstate_hash | |
| Cstatet | |
| Cci_lazy_methods_neededt | |
| ►Cci_lazy_methodst | |
| Cconvert_method_resultt | |
| Cclass_hierarchy_graph_nodet | Class hierarchy graph node: simply contains a class identifier |
| Cclass_hierarchy_grapht | Class hierarchy, represented using grapht and therefore suitable for use with generic graph algorithms |
| ►Cclass_hierarchyt | Non-graph-based representation of the class hierarchy |
| Centryt | |
| Cclass_infot | Corresponds to the CONSTANT_Class_info Structure Described in Java 8 specification 4.4.1 |
| Cclass_typet | Class type |
| ►Cclauset | |
| Cstept | |
| ►Ccmdlinet | |
| Coptiont | |
| Ccnf_clause_list_assignmentt | |
| Ccnf_clause_listt | |
| Ccnf_solvert | |
| Ccnft | |
| Ccode_asmt | codet representation of an inline assembler statement |
| Ccode_assertt | A non-fatal assertion, which checks a condition then permits execution to continue |
| Ccode_assignt | A codet representing an assignment in the program |
| Ccode_assumet | An assumption, which must hold in subsequent code |
| Ccode_blockt | A codet representing sequential composition of program statements |
| Ccode_breakt | codet representation of a break statement (within a for or while loop) |
| Ccode_continuet | codet representation of a continue statement (within a for or while loop) |
| Ccode_contractst | |
| Ccode_deadt | A codet representing the removal of a local variable going out of scope |
| Ccode_declt | A codet representing the declaration of a local variable |
| Ccode_dowhilet | codet representation of a do while statement |
| Ccode_expressiont | codet representation of an expression statement |
| Ccode_fort | codet representation of a for statement |
| Ccode_function_callt | codet representation of a function call statement |
| Ccode_gotot | codet representation of a goto statement |
| Ccode_ifthenelset | codet representation of an if-then-else statement |
| Ccode_labelt | codet representation of a label for branch targets |
| Ccode_landingpadt | A statement that catches an exception, assigning the exception in flight to an expression (e.g |
| Ccode_pop_catcht | Pops an exception handler from the stack of active handlers (i.e |
| ►Ccode_push_catcht | Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 .. |
| Cexception_list_entryt | |
| Ccode_returnt | codet representation of a "return from a function" statement |
| Ccode_skipt | A codet representing a skip statement |
| Ccode_switch_caset | codet representation of a switch-case, i.e. a case statement within a switch |
| Ccode_switcht | codet representing a switch statement |
| Ccode_try_catcht | codet representation of a try/catch block |
| ►Ccode_typet | Base type of functions |
| Cparametert | |
| Ccode_whilet | codet representing a while statement |
| Ccodet | Data structure for representing an arbitrary statement in a program |
| Ccompilet | |
| Ccomplex_exprt | Complex constructor from a pair of numbers |
| Ccomplex_imag_exprt | Imaginary part of the expression describing a complex number |
| Ccomplex_real_exprt | Real part of the expression describing a complex number |
| Ccomplex_typet | Complex numbers made of pair of given subtype |
| Cconcat_iteratort | On increment, increments a first iterator and when the corresponding end iterator is reached, starts to increment a second one |
| Cconcatenation_exprt | Concatenation of bit-vector operands |
| Cconcurrency_aware_ait | |
| Cconcurrency_aware_static_analysist | |
| ►Cconcurrency_instrumentationt | |
| Cshared_vart | |
| Cthread_local_vart | |
| Cconcurrent_cfg_baset | |
| Ccond_exprt | This 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 | |
| ►Cconfigt | Globally accessible architectural configuration |
| Cansi_ct | |
| Cbv_encodingt | |
| Ccppt | |
| Cjavat | |
| Cverilogt | |
| Cconsole_message_handlert | |
| Cconst_depth_iteratort | |
| Cconst_expr_visitort | |
| Cconst_target_hash | |
| Cconst_unique_depth_iteratort | |
| Cconstant_exprt | A constant literal expression |
| Cconstant_propagator_ait | |
| ►Cconstant_propagator_domaint | |
| Cvaluest | |
| Cconversion_dependenciest | This is structure is here to facilitate passing arguments to the conversion functions |
| Ccopy_on_write_pointeet | A helper class to store use-counts of copy-on-write objects |
| Ccopy_on_writet | A utility class for writing types with copy-on-write behaviour (like irep) |
| Ccounterexample_beautificationt | |
| Ccout_message_handlert | |
| Ccover_assertion_instrumentert | Assertion coverage instrumenter |
| Ccover_basic_blocks_javat | |
| ►Ccover_basic_blockst | |
| Cblock_infot | |
| Ccover_blocks_baset | |
| Ccover_branch_instrumentert | Branch coverage instrumenter |
| Ccover_condition_instrumentert | Condition coverage instrumenter |
| Ccover_configt | |
| Ccover_cover_instrumentert | __CPROVER_cover coverage instrumenter |
| Ccover_decision_instrumentert | Decision coverage instrumenter |
| ►Ccover_goalst | Try to cover some given set of goals incrementally |
| Cgoalt | |
| Cobservert | |
| Ccover_instrumenter_baset | Base class for goto program coverage instrumenters |
| Ccover_instrumenterst | A collection of instrumenters to be run |
| Ccover_location_instrumentert | Basic block coverage instrumenter |
| Ccover_mcdc_instrumentert | MC/DC coverage instrumenter |
| Ccover_path_instrumentert | Path 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 | |
| Cnamet | |
| 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 | |
| Cmatcht | |
| ►Ccpp_typecheckt | |
| Cinstantiation_levelt | |
| Cinstantiationt | |
| Cmethod_bodyt | |
| Ccpp_usingt | |
| Ccprover_exception_baset | Base class for exceptions thrown in the cprover project |
| Ccprover_library_entryt | |
| Ccustom_bitvector_analysist | |
| ►Ccustom_bitvector_domaint | |
| Cvectorst | |
| Ccw_modet | |
| Cd_containert | |
| Cd_internalt | |
| Cd_leaft | |
| Cdata | |
| Cdata_dpt | |
| Cdatat | |
| Cdecision_proceduret | |
| Cdecorated_symbol_exprt | Expression 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_baset | Depth first search iterator base - iterates over supplied expression and all its operands recursively |
| Cdepth_iterator_expr_statet | Helper class for depth_iterator_baset |
| Cdepth_iteratort | |
| Cdereference_callbackt | Base class for pointer value set analysis |
| Cdereference_exprt | Operator to dereference a pointer |
| Cdereferencet | Wrapper for a function which dereference a pointer-expression |
| Cdeserialization_exceptiont | Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes |
| ►Cdesignatort | |
| Centryt | |
| Cdiagnostics_helpert | Helper to give us some diagnostic in a usable form on assertion failure |
| Cdiagnostics_helpert< char * > | |
| Cdiagnostics_helpert< char[N]> | |
| Cdiagnostics_helpert< dstringt > | |
| Cdiagnostics_helpert< irep_pretty_diagnosticst > | |
| Cdiagnostics_helpert< source_locationt > | |
| Cdiagnostics_helpert< std::string > | |
| Cdimacs_cnf_dumpt | |
| Cdimacs_cnft | |
| Cdirtyt | |
| Cdisjunctive_polynomial_accelerationt | |
| Cdispatch_table_entryt | |
| Cdiv_exprt | Division |
| ►Cdocument_propertiest | |
| Cdoc_claimt | |
| Clinet | |
| Cdoes_remove_constt | |
| Cdomain_baset | |
| Cdott | |
| Cdstring_hash | |
| Cdstringt | dstringt has one field, an unsigned integer no which is an index into a static table of strings |
| ►Cdump_ct | |
| Ctypedef_infot | |
| Cdynamic_object_exprt | Representation of heap-allocated objects |
| CElf32_Ehdr | |
| CElf32_Shdr | |
| CElf64_Ehdr | |
| CElf64_Shdr | |
| Celf_readert | |
| Cempty_cfg_nodet | |
| Cempty_edget | |
| Cempty_typet | The empty type |
| Cendianness_mapt | Maps a big-endian offset to a little-endian offset |
| Cenumerating_loop_accelerationt | |
| Cenumeration_typet | An enumeration type, i.e., a type with elements (not to be confused with C enums) |
| Cequal_exprt | Equality |
| ►Cequalityt | |
| Ctypestructt | |
| Cequation_conversion_exceptiont | |
| Cequation_symbol_mappingt | Maps equation to expressions contained in them and conversely expressions to equations that contain them |
| Cescape_analysist | |
| ►Cescape_domaint | |
| Ccleanupt | |
| ►Cevent_grapht | |
| ►Ccritical_cyclet | |
| Cdelayt | |
| Cgraph_conc_explorert | |
| Cgraph_explorert | |
| Cgraph_pensieve_explorert | |
| Cexists_exprt | An exists expression |
| Cexpanding_vectort | |
| Cexpr2c_configurationt | Used for configuring the behaviour of expr2c and type2c |
| Cexpr2cppt | |
| Cexpr2ct | |
| Cexpr2javat | |
| Cexpr2jsilt | |
| Cexpr_initializert | |
| Cexpr_visitort | |
| Cexprt | Base class for all expressions |
| Cextractbit_exprt | Extracts a single bit of a bit-vector operand |
| Cextractbits_exprt | Extracts a sub-range of a bit-vector operand |
| Cfactorial_power_exprt | Falling factorial power |
| Cfalse_exprt | The Boolean constant false |
| ►Cfault_localizationt | |
| Clpointt | |
| Cfieldref_exprt | Represents 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_iteratort | Iterator which only stops at elements for which some given function f is true |
| Cfind_qvar_visitort | |
| Cfixed_keys_map_wrappert | |
| Cfixedbv_spect | |
| Cfixedbv_typet | Fixed-width bit-vector with signed fixed-point interpretation |
| Cfixedbvt | |
| Cflatten_byte_extract_exceptiont | |
| Cfloat_approximationt | |
| ►Cfloat_bvt | |
| Cbiased_floatt | |
| Crounding_mode_bitst | |
| Cunbiased_floatt | |
| Cunpacked_floatt | |
| ►Cfloat_utilst | |
| Cbiased_floatt | |
| Crounding_mode_bitst | |
| Cunbiased_floatt | |
| Cunpacked_floatt | |
| Cfloatbv_typecast_exprt | Semantic type conversion from/to floating-point formats |
| Cfloatbv_typet | Fixed-width bit-vector with IEEE floating-point interpretation |
| Cflow_insensitive_abstract_domain_baset | |
| Cflow_insensitive_analysis_baset | |
| Cflow_insensitive_analysist | |
| Cforall_exprt | A forall expression |
| Cformat_constantt | |
| Cformat_containert | The 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_cmdlinet | An implementation of cmdlinet to be used in tests |
| Cfreert | A functor wrapping std::free |
| ►Cfull_slicert | |
| Ccfg_nodet | |
| Cfunction_application_exprt | Application of (mathematical) function |
| Cfunction_filter_baset | Base class for filtering functions |
| Cfunction_filterst | A collection of function filters to be applied in conjunction |
| Cfunction_indicest | Helper class that maintains a map from function name to grapht node index and adds nodes to the graph on demand |
| Cfunction_modifiest | |
| ►Cfunctionst | |
| Cfunction_infot | |
| Cgcc_cmdlinet | |
| Cgcc_message_handlert | |
| Cgcc_modet | |
| Cgcc_versiont | |
| Cgenerate_function_bodies_errort | |
| Cgenerate_function_bodiest | Base class for replace_function_body implementations |
| Cgeneric_parameter_specialization_map_keyst | |
| Cglobal_may_alias_analysist | This is a may analysis (i.e |
| Cglobal_may_alias_domaint | |
| Cgoal_filter_baset | Base class for filtering goals |
| Cgoal_filterst | A collection of goal filters to be applied in conjunction |
| Cgoto_analyzer_parse_optionst | |
| ►Cgoto_cc_cmdlinet | |
| Cargt | |
| Cgoto_cc_modet | |
| ►Cgoto_checkt | |
| Cconditiont | |
| Cgoto_convert_functionst | |
| ►Cgoto_convertt | |
| Cbreak_continue_targetst | |
| Cbreak_switch_targetst | |
| Cleave_targett | |
| Ctargetst | |
| Cthrow_targett | |
| Cgoto_diff_languagest | |
| Cgoto_diff_parse_optionst | |
| Cgoto_difft | |
| Cgoto_functionst | A collection of goto functions |
| Cgoto_functiont | A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers) |
| ►Cgoto_inlinet | |
| ►Cgoto_inline_logt | |
| Cgoto_inline_log_infot | |
| Cgoto_instrument_parse_optionst | |
| Cgoto_model_functiont | Interface providing access to a single function in a GOTO model, plus its associated symbol table |
| Cgoto_modelt | |
| Cgoto_null_checkt | Return structure for get_null_checked_expr and get_conditional_checked_expr |
| ►Cgoto_program2codet | |
| Ccaset | |
| ►Cgoto_program_coverage_recordt | |
| Ccoverage_conditiont | |
| Ccoverage_linet | |
| Cgoto_program_dereferencet | Wrapper for functions removing dereferences in expressions contained in a goto program |
| ►Cgoto_programt | A generic container class for the GOTO intermediate representation of one function |
| Cinstructiont | This class represents an instruction in the GOTO intermediate representation |
| Cgoto_symex_is_constantt | |
| ►Cgoto_symex_statet | |
| ►Cframet | |
| Cloop_infot | |
| Cgoto_statet | |
| Cthreadt | |
| Cgoto_symext | The main class for the forward symbolic simulator |
| Cgoto_trace_stept | TO_BE_DOCUMENTED |
| Cgoto_tracet | TO_BE_DOCUMENTED |
| ►Cgoto_unwindt | |
| Cunwind_logt | |
| Cgraph_nodet | This class represents a node in a directed graph |
| Cgraphml_witnesst | |
| Cgraphmlt | |
| ►Cgrapht | A generic directed graph with a parametric node type |
| Ctarjant | |
| Cguarded_range_domaint | |
| Cguardt | |
| Chavoc_generate_function_bodiest | |
| Chavoc_loopst | |
| Cidentifiert | |
| Cieee_float_equal_exprt | IEEE-floating-point equality |
| Cieee_float_notequal_exprt | IEEE floating-point disequality |
| Cieee_float_op_exprt | IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2) |
| Cieee_float_spect | |
| Cieee_floatt | |
| Cif_exprt | The trinary if-then-else operator |
| Cimplies_exprt | Boolean implication |
| Cin_function_criteriont | |
| Cinclude_pattern_filtert | Filters functions that match the provided pattern |
| Cincomplete_array_typet | Arrays without size |
| Cincorrect_goto_program_exceptiont | Thrown 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_dirtyt | Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly once |
| Cindex_designatort | |
| Cindex_exprt | Array index operator |
| Cindex_set_pairt | |
| Cindicator_maskt | |
| Cindicator_maskt< T, B, std::integral_constant< T, 0 > > | |
| Cinfinity_exprt | An expression denoting infinity |
| Cinfix_opt | |
| Cinflate_state | |
| Cinode | |
| Cinstrumenter_pensievet | |
| ►Cinstrumentert | |
| Ccfg_visitort | |
| Cinteger_typet | Unbounded, signed integers (mathematical integers, not bitvectors) |
| Cinternal_functions_filtert | Filters out CPROVER internal functions |
| Cinternal_goals_filtert | Filters out goals with source locations considered internal |
| ►Cinterpretert | |
| Cfunction_assignments_contextt | |
| Cfunction_assignmentt | |
| Cmemory_cellt | |
| Cstack_framet | |
| Cinterval_domaint | |
| Cinterval_sparse_arrayt | Represents arrays by the indexes up to which the value remains the same |
| Cinterval_templatet | |
| ►Cinv_object_storet | |
| Centryt | |
| Cinvalid_command_line_argument_exceptiont | Thrown when users pass incorrect command line arguments, for example passing no files to analysis or setting two mutually exclusive flags |
| Cinvalid_source_file_exceptiont | Thrown when we can't handle something in an input source file |
| Cinvariant_failedt | A logic error, augmented with a distinguished field to hold a backtrace |
| Cinvariant_propagationt | |
| Cinvariant_set_domaint | |
| Cinvariant_sett | |
| Cinvariant_with_diagnostics_failedt | A 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_entryt | |
| Cpointer_hasht | |
| Cvector_hasht | |
| Cirep_hash_containert | |
| Cirep_hash_mapt | |
| Cirep_pretty_diagnosticst | |
| ►Cirep_serializationt | |
| Cireps_containert | |
| ►Cirept | Base class for tree-like data structures with sharing |
| Cdt | |
| Cis_constantt | Determine whether an expression is constant |
| Cis_predecessor_oft | |
| Cis_threaded_domaint | |
| Cis_threadedt | |
| Cisfinite_exprt | Evaluates to true if the operand is finite |
| Cisinf_exprt | Evaluates to true if the operand is infinite |
| Cisnan_exprt | Evaluates to true if the operand is NaN |
| Cisnormal_exprt | Evaluates to true if the operand is a normal number |
| Cjanalyzer_parse_optionst | |
| Cjar_filet | Class representing a .jar archive |
| Cjar_poolt | A chache for jar_filet objects, by file name |
| ►Cjava_annotationt | |
| Cvaluet | |
| Cjava_bytecode_convert_classt | |
| ►Cjava_bytecode_convert_methodt | |
| Cblock_tree_nodet | |
| Cconverted_instructiont | |
| Cholet | |
| Clocal_variable_with_holest | |
| Cvariablet | |
| Cjava_bytecode_instrumentt | |
| Cjava_bytecode_languaget | |
| ►Cjava_bytecode_parse_treet | |
| ►Cannotationt | |
| Celement_value_pairt | |
| ►Cclasst | |
| Clambda_method_handlet | |
| Cfieldt | |
| Cinstructiont | |
| Cmembert | |
| ►Cmethodt | |
| Cexceptiont | |
| Clocal_variablet | |
| Cstack_map_table_entryt | |
| Cverification_type_infot | |
| ►Cjava_bytecode_parsert | |
| Cbytecodet | |
| Cpool_entryt | |
| Cjava_bytecode_typecheckt | |
| ►Cjava_class_loader_baset | Base class for maintaining classpath |
| Cclasspath_entryt | An entry in the classpath |
| Cjava_class_loader_limitt | Class representing a filter for class file loading |
| Cjava_class_loadert | Class responsible to load .class files |
| Cjava_class_typet | |
| Cjava_generic_class_typet | Class 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_parametert | Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T> |
| Cjava_generic_struct_tag_typet | Type for a generic symbol, extends struct_tag_typet with a vector of java generic types |
| Cjava_generic_typet | Class 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_typet | Type 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_tablet | A 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_arrayt | Provides methods for streaming JSON arrays |
| Cjson_stream_objectt | Provides methods for streaming JSON objects |
| Cjson_streamt | This 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_mapt | Provides a wrapper for a map of lazily loaded goto_functiont |
| Clazy_goto_modelt | A GOTO model that produces function bodies on demand |
| Cld_cmdlinet | |
| Cld_modet | |
| Clet_exprt | A let expression |
| Clinker_script_merget | Synthesise definitions of symbols that are defined in linker scripts |
| ►Clinkingt | |
| Cadjust_type_infot | |
| Clispexprt | |
| Clispsymbolt | |
| Cliteral_exprt | |
| Cliteralt | |
| ►Clocal_bitvector_analysist | |
| Cflagst | |
| ►Clocal_cfgt | |
| Cnodet | |
| Clocal_may_alias_factoryt | |
| ►Clocal_may_aliast | |
| Cloc_infot | |
| ►Clocal_safe_pointerst | A very simple, cheap analysis to determine when dereference operations are trivially guarded by a check against a null pointer access |
| Cbase_type_comparet | Comparator that regards base_type_eq expressions as equal, and otherwise uses the natural (operator<) ordering on irept |
| Clocalst | |
| Clshr_exprt | Logical right shift |
| Cmain_function_resultt | |
| Cmap_iteratort | Iterator which applies some given function f after each increment and returns its result on dereference |
| Cmathematical_function_typet | A type for mathematical functions (do not confuse with functions/methods in code) |
| Cmember_designatort | |
| Cmember_exprt | Extract 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_typet | Holds a combination of types |
| Cmessage_handlert | |
| ►Cmessaget | Class that provides messages with a built-in verbosity 'level' |
| Ccommandt | |
| Ceomt | |
| Cmstreamt | |
| ►Cmethod_bytecodet | |
| Cclass_method_and_bytecodet | Pair of class id and methodt |
| Cmethod_handle_infot | |
| Cmini_bdd_applyt | |
| ►Cmini_bdd_mgrt | |
| Creverse_keyt | |
| Cvar_table_entryt | |
| Cmini_bdd_nodet | |
| Cmini_bddt | |
| Cminisat_prooft | |
| Cminus_exprt | Binary minus |
| Cmissing_outer_class_symbol_exceptiont | An exception that is raised checking whether a class is implicitly generic if a symbol for an outer class is missing |
| Cmod_exprt | Modulo |
| ►Cmonomialt | |
| Ctermt | |
| Cmonotonic_timestampert | |
| Cms_cl_cmdlinet | |
| Cms_cl_modet | |
| Cms_cl_versiont | |
| Cms_link_cmdlinet | |
| Cms_link_modet | |
| Cmult_exprt | Binary multiplication Associativity is not specified |
| Cmulti_ary_exprt | A base class for multi-ary expressions Associativity is not specified |
| Cmulti_namespacet | A 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_archivet | Thin 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_infot | Corresponds to the CONSTANT_NameAndType_info Structure Described in Java 8 specification 4.4.6 |
| Cnamespace_baset | Basic interface for a namespace |
| Cnamespacet | A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in them |
| Cnatural_loops_templatet | Main driver for working out if a class (normally goto_programt) has any natural loops |
| Cnatural_loopst | A concretized version of natural_loops_templatet<const goto_programt, goto_programt::const_targett> |
| Cnatural_typet | Natural numbers including zero (mathematical integers, not bitvectors) |
| Cnew_scopet | |
| Cnil_exprt | The NIL expression |
| Cnil_typet | The 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_infot | Holds information about any discovered nondet methods, with extreme type- safety |
| Cnondet_symbol_exprt | Expression to hold a nondeterministic choice |
| Cnot_exprt | Boolean negation |
| Cnotequal_exprt | Disequality |
| Cnull_message_handlert | |
| Cnull_pointer_exprt | The null pointer constant |
| Cnullary_exprt | An expression without operands |
| Cnullptr_exceptiont | |
| Cnum_bitst | |
| Cnum_bitst< 0 > | |
| Cnum_bitst< 1 > | |
| Cnumeric_castt | Numerical cast provides a unified way of converting from one numerical type to another |
| Cnumeric_castt< mp_integer > | Convert expression to mp_integer |
| Cnumeric_castt< T, typename std::enable_if< std::is_integral< T >::value >::type > | Convert mp_integer or expr to any integral type |
| Cobject_descriptor_exprt | Split an expression into a base object and a (byte) offset |
| Cobject_factory_parameterst | |
| Cobject_idt | |
| Coperator_entryt | |
| Coptionst | |
| Cor_exprt | Boolean OR |
| Cosx_fat_readert | |
| Coverflow_instrumentert | |
| Cparameter_assignmentst | |
| Cparameter_symbolt | Symbol table entry of function parameterThis is a symbol generated as part of type checking |
| Cparse_floatt | |
| Cparse_options_baset | |
| CParser | |
| Cparsert | |
| ►Cpartial_order_concurrencyt | |
| Ca_rect | |
| Cpath_acceleratort | |
| Cpath_enumeratort | |
| Cpath_explorert | Symbolic execution from a saved branch point |
| Cpath_fifot | FIFO save queue: paths are resumed in the order that they were saved |
| Cpath_lifot | LIFO save queue: depth-first search, try to finish paths |
| Cpath_nodet | |
| ►Cpath_storaget | Storage for symbolic execution paths to be resumed later |
| Cpatht | Information saved at a conditional goto to resume execution |
| Cpath_strategy_choosert | Factory and information for path_storaget |
| Cpatternt | Given 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_exprt | The plus expression Associativity is not specified |
| Cpointee_address_equalt | Functor to check whether iterators from different collections point at the same object |
| Cpointer_arithmetict | |
| ►Cpointer_logict | |
| Cpointert | |
| Cpointer_typet | The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they have a subtype) |
| Cpoints_tot | |
| ►Cpolynomial_acceleratort | |
| Cpolynomial_array_assignment | |
| Cpolynomialt | |
| Cpopcount_exprt | The popcount (counting the number of bits set to 1) expression |
| Cpostconditiont | |
| Cpower_exprt | Exponentiation |
| Cpreconditiont | |
| Cpredicate_exprt | A base class for expressions that are predicates, i.e., Boolean-typed |
| Cpreprocessort | |
| ►Cprintf_formattert | |
| Ceol_exceptiont | |
| 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 | TO_BE_DOCUMENTED |
| Cprop_convt | |
| ►Cprop_minimizet | Computes a satisfying assignment of minimal cost according to a const function using incremental SAT |
| Cobjectivet | |
| Cproperties_criteriont | |
| ►Cproperty_checkert | |
| Cproperty_statust | |
| Cpropt | TO_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 | |
| Cquantifiert | |
| Cqdimacs_coret | |
| Cqualifierst | |
| Cquantifier_exprt | A base class for quantifier expressions |
| Crange_domain_baset | |
| Crange_domaint | |
| Crange_typet | A type for subranges of integers |
| Cranget | A range is a pair of a begin and an end iterators |
| Crational_typet | Unbounded, signed rational numbers |
| Crationalt | |
| Crd_range_domaint | Because 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 | |
| Csearch_stack_entryt | A search stack entry, used in tracking nodes to mark reachable when walking over the CFG in fixedpoint_to_assertions and fixedpoint_from_assertions |
| Cslicer_entryt | |
| Creaching_definitions_analysist | |
| Creaching_definitiont | Identifies a GOTO instruction where a given variable is defined (i.e |
| Creal_typet | Unbounded, signed real numbers |
| Crebuild_goto_start_function_baset | |
| Crecursion_set_entryt | Recursion-set entry owner class |
| Cref_expr_set_dt | |
| Cref_expr_sett | |
| ►Creference_counting | |
| Cdt | |
| Creference_typet | The reference type |
| Crefined_string_exprt | |
| Crefined_string_typet | |
| Crem_exprt | Remainder of division |
| Cremove_asmt | |
| Cremove_calls_no_bodyt | |
| Cremove_const_function_pointerst | |
| Cremove_exceptionst | Lowers 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_symbolt | Replace expression or type symbols by an expression or type, respectively |
| Creplacement_predicatet | Patterns of expressions that should be replaced |
| Creplication_exprt | Bit-vector replication |
| Cresolution_prooft | |
| ►Cresolve_inherited_componentt | |
| Cinherited_componentt | |
| Crestrictt | |
| Crw_guarded_range_set_value_sett | |
| Crw_range_set_value_sett | |
| Crw_range_sett | |
| ►Crw_set_baset | |
| Centryt | |
| Crw_set_functiont | |
| Crw_set_loct | |
| Crw_set_with_trackt | |
| Csafety_checkert | |
| Csaj_tablet | Produce 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_ipasirt | Interface 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 | |
| Ccfg_visitort | |
| Cvarst | |
| ►Csharing_mapt | A map implemented as a tree where subtrees can be shared between different maps |
| Cdelta_view_itemt | |
| Csharing_map_statst | Stats about sharing between several sharing map instances |
| Csharing_node_baset | |
| Csharing_node_innert | |
| Csharing_node_leaft | |
| Cshift_exprt | A base class for shift operators |
| Cshl_exprt | Left shift |
| Cshow_goto_functions_jsont | |
| Cshow_goto_functions_xmlt | |
| Cside_effect_expr_function_callt | A side_effect_exprt representation of a function call side effect |
| Cside_effect_expr_nondett | A side_effect_exprt that returns a non-deterministically chosen value |
| Cside_effect_expr_throwt | A side_effect_exprt representation of a side effect that throws an exception |
| Cside_effect_exprt | An expression containing a side effect |
| Csign_exprt | Sign of an expression Predicate is true if _op is negative, false otherwise |
| Csignedbv_typet | Fixed-width bit-vector with two's complement interpretation |
| Csimplify_exprt | |
| Cslicing_criteriont | |
| ►Csmall_mapt | Map from small integers to values |
| Cconst_iterator | Const iterator |
| Cconst_value_iterator | Const value iterator |
| Csmall_shared_pointeet | A helper class to store use-counts of objects held by small shared pointers |
| Csmall_shared_ptrt | This class is really similar to boost's intrusive_pointer, but can be a bit simpler seeing as we're only using it one place |
| Csmall_shared_two_way_pointeet | |
| Csmall_shared_two_way_ptrt | This class is similar to small_shared_ptrt and boost's intrusive_ptr |
| ►Csmt2_convt | |
| Cidentifiert | |
| Clet_count_idt | |
| Clet_visitort | |
| Csmt2_symbolt | |
| Csmt2_dect | Decision procedure interface for various SMT 2.x solvers |
| Csmt2_format_containert | |
| Csmt2_message_handlert | |
| ►Csmt2_parsert | |
| Cidt | |
| Cnamed_termt | |
| Csignature_with_parameter_idst | |
| Csmt2_solvert | |
| Csmt2_stringstreamt | |
| ►Csmt2_tokenizert | |
| Csmt2_errort | |
| Csmt2irept | |
| ►Csolver_factoryt | |
| Csolvert | |
| Csource_locationt | |
| Csparse_arrayt | Represents arrays of the form array_of(x) with {i:=a} with {j:=b} ... by a default value x and a list of entries (i,a), (j,b) etc |
| Csparse_bitvector_analysist | An instance of this class provides an assignment of unique numeric ID to each inserted reaching_definitiont instance |
| Csparse_vectort | |
| Cssa_exprt | Expression 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_evalt | Functions that are not yet supported in this class but are supported by string_constraint_generatort |
| Cstring_builtin_functiont | Base class for string functions that are built in the solver |
| Cstring_concat_char_builtin_functiont | Adding a character at the end of a string |
| Cstring_concatenation_builtin_functiont | |
| Cstring_constantt | |
| Cstring_constraint_generatort | |
| Cstring_constraintst | Collection of constraints of different types: existential formulas, universal formulas, and "not contains" (universal with one alternation) |
| Cstring_constraintt | |
| Cstring_containert | |
| Cstring_creation_builtin_functiont | String creation from other types |
| ►Cstring_dependenciest | Keep track of dependencies between strings |
| Cbuiltin_function_nodet | A builtin function node contains a builtin function call |
| Cnode_hash | Hash function for nodes |
| Cnodet | |
| Cstring_nodet | A string node points to builtin_function on which it depends |
| Cstring_hash | |
| Cstring_insertion_builtin_functiont | String inserting a string into another one |
| Cstring_instrumentationt | |
| Cstring_not_contains_constraintt | Constraints to encode non containement of strings |
| Cstring_of_int_builtin_functiont | String creation from integer types |
| Cstring_ptr_hash | |
| Cstring_ptrt | |
| ►Cstring_refinementt | |
| Cconfigt | |
| Cinfot | String_refinementt constructor arguments |
| Cstring_set_char_builtin_functiont | Setting a character at a particular position of a string |
| Cstring_test_builtin_functiont | String test |
| Cstring_to_lower_case_builtin_functiont | Converting each uppercase character of Basic Latin and Latin-1 supplement to the corresponding lowercase character |
| Cstring_to_upper_case_builtin_functiont | Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding uppercase character |
| Cstring_transformation_builtin_functiont | String builtin_function transforming one string into another |
| Cstring_typet | String type |
| Cstruct_exprt | Struct constructor from list of elements |
| Cstruct_tag_typet | A struct tag type, i.e., struct_typet with an identifier |
| ►Cstruct_typet | Structure type, corresponds to C style structs |
| Cbaset | Base class or struct that a class or struct inherits from |
| ►Cstruct_union_typet | Base type for structs and unions |
| Ccomponentt | |
| Cstructured_pool_entryt | |
| Cstub_global_initializer_factoryt | |
| Csubsumed_patht | |
| Csymbol_exprt | Expression to hold a symbol (variable) |
| Csymbol_factoryt | |
| Csymbol_generatort | Generation of fresh symbols of a given type |
| ►Csymbol_table_baset | The symbol table base class interface |
| Citeratort | |
| Csymbol_table_buildert | Author: Diffblue Ltd |
| Csymbol_tablet | The symbol table |
| Csymbol_typet | A reference into the symbol table |
| Csymbolt | Symbol table entry |
| Csymex_bmct | |
| Csymex_configt | Configuration of the symbolic execution |
| ►Csymex_coveraget | |
| Ccoverage_infot | |
| Csymex_dereference_statet | |
| Csymex_level0t | Functor to set the level 0 renaming of SSA expressions |
| Csymex_level1t | Functor to set the level 1 renaming of SSA expressions |
| Csymex_level2t | Functor to set the level 2 renaming of SSA expressions |
| Csymex_nondet_generatort | Functor generating fresh nondet symbols |
| Csymex_renaming_levelt | Wrapper for a current_names map, which maps each identifier to an SSA expression and a counter |
| Csymex_slice_by_tracet | |
| Csymex_slicet | |
| ►Csymex_target_equationt | Inheriting the interface of symex_targett this class represents the SSA form of the input program as a list of SSA_stept |
| CSSA_stept | Single SSA step in the equation |
| ►Csymex_targett | The interface of the target container for symbolic execution to record its symbolic steps into |
| Csourcet | Identifies source in the context of symbolic execution |
| Csyntactic_difft | |
| Csystem_exceptiont | Thrown when some external system fails unexpectedly |
| Csystem_library_symbolst | |
| Ctag_typet | A tag-based type, i.e., typet with an identifier |
| Ctaint_analysist | |
| ►Ctaint_parse_treet | |
| Crulet | |
| Ctdefl_compressor | |
| Ctdefl_output_buffer | |
| Ctdefl_sym_freq | |
| Ctemp_dirt | |
| Ctemplate_mapt | |
| Ctemplate_numberingt | |
| Ctemplate_parametert | |
| Ctemplate_typet | |
| Ctemporary_filet | |
| Cternary_exprt | An expression with three operands |
| Ctimestampert | Timestamp class hierarchy |
| Ctinfl_decompressor_tag | |
| Ctinfl_huff_table | |
| Cto_be_merged_irep_hash | |
| Cto_be_merged_irept | |
| Ctrace_automatont | |
| Ctrace_optionst | |
| Ctranst | Transition system, consisting of state invariant, initial state predicate, and transition predicate |
| Ctrivial_functions_filtert | Filters out trivial functions |
| Ctrue_exprt | The Boolean constant true |
| Ctvt | |
| Ctype_exprt | An expression denoting a type |
| Ctype_symbolt | Symbol table entry describing a data typeThis is a symbol generated as part of type checking |
| Ctype_with_subtypest | Type with multiple subtypes |
| Ctype_with_subtypet | Type with a single subtype |
| Ctypecast_exprt | Semantic type conversion |
| Ctypecheckt | |
| Ctypedef_typet | A typedef |
| Ctypet | The type of an expression, extends irept |
| Cui_message_handlert | |
| Cunary_exprt | Generic base class for unary expressions |
| Cunary_minus_exprt | The unary minus expression |
| Cunary_plus_exprt | The unary plus expression |
| Cunary_predicate_exprt | A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argument |
| Cuncaught_exceptions_analysist | Computes in exceptions_map an overapproximation of the exceptions thrown by each method |
| Cuncaught_exceptions_domaint | |
| Cunchecked_replace_symbolt | |
| Cunified_difft | |
| Cuninitialized_domaint | |
| Cuninitializedt | |
| Cunion_exprt | Union constructor from single element |
| Cunion_find | |
| Cunion_find_replacet | Similar interface to union-find for expressions, with a function for replacing sub-expressions by their result for find |
| Cunion_tag_typet | A union tag type, i.e., union_typet with an identifier |
| Cunion_typet | The union type |
| ►Cunsigned_union_find | |
| Cnodet | |
| Cunsignedbv_typet | Fixed-width bit-vector with unsigned binary interpretation |
| Cunsupported_java_class_signature_exceptiont | An exception that is raised for unsupported class signature |
| Cunsupported_operation_exceptiont | Thrown when we encounter an instruction, parameters to an instruction etc |
| Cunwindsett | |
| Cupdate_exprt | Operator 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_dereferencet | Wrapper for a function dereferencing pointer expressions using a value set |
| Cvaluet | Return value for build_reference_to; see that method for documentation |
| Cvalue_set_domain_fit | |
| Cvalue_set_domain_fivrnst | |
| Cvalue_set_domain_fivrt | |
| Cvalue_set_domain_templatet | |
| ►Cvalue_set_fit | |
| Centryt | |
| Cobject_map_dt | |
| ►Cvalue_set_fivrnst | |
| Centryt | |
| ►Cobject_map_dt | |
| Cvalidity_ranget | |
| ►Cvalue_set_fivrt | |
| Centryt | |
| ►Cobject_map_dt | |
| Cvalidity_ranget | |
| Cvalue_setst | |
| ►Cvalue_sett | State type in value_set_domaint, used in value-set analysis and goto-symex |
| Centryt | Represents a row of a value_sett |
| Cobject_map_dt | Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances) |
| Cvector_exprt | Vector constructor from list of elements |
| Cvector_typet | The vector type |
| Cvisited_nodet | A node type with an extra bit |
| Cvoid_typet | The void type, the same as empty_typet |
| Cw_guardst | |
| Cwall_clock_timestampert | |
| Cwith_exprt | Operator to update elements in structs and arrays |
| Cwrapper_goto_modelt | Class 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_exprt | Boolean XOR |
| Cyy_buffer_state | |
| Cyy_trans_info | |
| Cyyalloc | |
| CYYSTYPE | |
1.8.15