| ▶Ndetail | |
| 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 |
| 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_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 | |
| 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 generic base class for binary expressions |
| Cbinary_predicate_exprt | A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly two arguments |
| Cbinary_relation_exprt | A generic 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 bitvector 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 proper Booleans |
| ▶Cboolbv_mapt | |
| Cmap_bitt | |
| Cmap_entryt | |
| ▶Cboolbv_widtht | |
| Centryt | |
| Cmembert | |
| ▶Cboolbvt | |
| Cquantifiert | |
| Cbswap_exprt | The byte swap expression |
| Cbv_arithmetict | |
| Cbv_cbmct | |
| 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_big_endian_exprt | TO_BE_DOCUMENTED |
| Cbyte_extract_exprt | TO_BE_DOCUMENTED |
| Cbyte_extract_little_endian_exprt | TO_BE_DOCUMENTED |
| Cbyte_update_big_endian_exprt | TO_BE_DOCUMENTED |
| Cbyte_update_exprt | TO_BE_DOCUMENTED |
| Cbyte_update_little_endian_exprt | TO_BE_DOCUMENTED |
| Cbytecode_infot | |
| Cc_bit_field_typet | Type for c bit fields |
| Cc_bool_typet | The C/C++ Booleans |
| Cc_enum_tag_typet | An enum tag type |
| ▶Cc_enum_typet | The type of C enums |
| Cc_enum_membert | |
| Cc_qualifierst | |
| Cc_storage_spect | |
| Cc_typecastt | |
| Cc_typecheck_baset | |
| ▶Ccall_grapht | |
| 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 |
| Ccbmc_dimacst | |
| Ccbmc_parse_optionst | |
| ▶Ccbmc_solverst | |
| Csolvert | |
| 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 | C++ class type |
| Cbaset | |
| ▶Cclauset | |
| Cstept | |
| Cclobber_parse_optionst | |
| ▶Ccmdlinet | |
| Coptiont | |
| Ccnf_clause_list_assignmentt | |
| Ccnf_clause_listt | |
| Ccnf_solvert | |
| Ccnft | |
| Ccode_asmt | An inline assembler statement |
| Ccode_assertt | A non-fatal assertion, which checks a condition then permits execution to continue |
| Ccode_assignt | Assignment |
| Ccode_assumet | An assumption, which must hold in subsequent code |
| Ccode_blockt | Sequential composition |
| Ccode_breakt | A break for ‘for’ and ‘while’ loops |
| Ccode_continuet | A continue for ‘for’ and ‘while’ loops |
| Ccode_contractst | |
| Ccode_deadt | A removal of a local variable |
| Ccode_declt | A declaration of a local variable |
| Ccode_dowhilet | A ‘do while’ instruction |
| Ccode_expressiont | An expression statement |
| Ccode_fort | A ‘for’ instruction |
| Ccode_function_callt | A function call |
| Ccode_gotot | A ‘goto’ instruction |
| Ccode_ifthenelset | An if-then-else |
| Ccode_labelt | 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 | Return from a function |
| Ccode_skipt | Skip |
| Ccode_switch_caset | A switch-case |
| Ccode_switcht | A ‘switch’ instruction |
| Ccode_try_catcht | A try/catch block |
| ▶Ccode_typet | Base type of functions |
| Cparametert | |
| Ccode_whilet | A ‘while’ instruction |
| Ccodet | A statement in a programming language |
| Ccompilet | |
| Ccomplex_exprt | Complex constructor from a pair of numbers |
| Ccomplex_typet | Complex numbers made of pair of given subtype |
| Cconcatenation_exprt | Concatenation of bit-vector operands |
| Cconcurrency_aware_ait | |
| Cconcurrency_aware_static_analysist | |
| ▶Cconcurrency_instrumentationt | |
| Cshared_vart | |
| Cthread_local_vart | |
| Cconcurrent_cfg_baset | |
| 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_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) |
| 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 | TO_BE_DOCUMENTED |
| Cdereference_exprt | Operator to dereference a pointer |
| Cdereferencet | TO_BE_DOCUMENTED |
| ▶Cdesignatort | |
| Centryt | |
| Cdimacs_cnf_dumpt | |
| Cdimacs_cnft | |
| Cdirtyt | |
| Cdisjunctive_polynomial_accelerationt | |
| Cdispatch_table_entryt | |
| Cdiv_exprt | Division (integer and real) |
| ▶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 | TO_BE_DOCUMENTED |
| 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 | A generic enumeration type (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 | |
| 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 | |
| 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_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 | |
| 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 | |
| Cgoto_functiont | |
| ▶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 | |
| ▶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_statet | |
| ▶Cframet | |
| Cloop_infot | |
| Cgoto_statet | |
| Clevel0t | |
| Clevel1t | |
| Clevel2t | |
| Cpropagationt | |
| Crenaming_levelt | |
| 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 |
| Cieee_float_spect | |
| Cieee_floatt | |
| Cif_exprt | The trinary if-then-else operator |
| Cimplies_exprt | Boolean implication |
| Cinclude_pattern_filtert | Filters functions that match the provided pattern |
| Cincomplete_array_typet | Arrays without size |
| 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 |
| Cinflate_state | |
| Cinode | |
| Cinstrumenter_pensievet | |
| ▶Cinstrumentert | |
| Ccfg_visitort | |
| Cinteger_typet | Unbounded, signed integers |
| 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 | |
| Cinvariant_failedt | A logic error, augmented with a distinguished field to hold a backtrace |
| Cinvariant_propagationt | |
| Cinvariant_set_domaint | |
| Cinvariant_sett | |
| Cirep_full_eq | |
| Cirep_full_hash | |
| Cirep_full_hash_containert | |
| Cirep_hash | |
| ▶Cirep_hash_container_baset | |
| Cirep_entryt | |
| Cpointer_hasht | |
| Cvector_hasht | |
| Cirep_hash_containert | |
| Cirep_hash_mapt | |
| ▶Cirep_serializationt | |
| Cireps_containert | |
| ▶Cirept | Base class for tree-like data structures with sharing |
| Cdt | |
| 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 |
| ▶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_limitt | |
| Cjava_class_loadert | |
| 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_symbol_typet | Type for a generic symbol, extends symbol_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_factoryt | |
| Cjava_qualifierst | |
| Cjava_simple_method_stubst | |
| Cjava_string_library_preprocesst | |
| Cjava_syntactic_difft | |
| Cjbmc_parse_optionst | |
| Cjdiff_languagest | |
| Cjdiff_parse_optionst | |
| 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_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 | Model that holds partially loaded map of functions |
| 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 | |
| ▶Cmathematical_function_typet | A type for mathematical functions (do not confuse with functions/methods in code) |
| Cvariablet | |
| Cmember_designatort | |
| Cmember_exprt | Extract member of struct or union |
| Cmember_offset_iterator | |
| Cmemory_model_baset | |
| Cmemory_model_psot | |
| Cmemory_model_sct | |
| Cmemory_model_tsot | |
| Cmerge_full_irept | |
| Cmerge_irept | |
| Cmerged_irep_hash | |
| Cmerged_irepst | |
| Cmerged_irept | |
| Cmessage_handlert | |
| ▶Cmessaget | |
| 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 |
| Cmm2cppt | |
| Cmm_parsert | |
| Cmmcc_parse_optionst | |
| Cmod_exprt | Binary modulo |
| ▶Cmonomialt | |
| Ctermt | |
| Cmonotonic_timestampert | |
| Cms_cl_cmdlinet | |
| Cms_cl_modet | |
| Cms_link_cmdlinet | |
| Cms_link_modet | |
| Cmult_exprt | Binary multiplication |
| Cmulti_ary_exprt | A generic base class for multi-ary expressions |
| Cmulti_namespacet | |
| 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 | |
| Cnamespacet | TO_BE_DOCUMENTED |
| Cnatural_loops_templatet | |
| Cnatural_loopst | |
| Cnatural_typet | Natural numbers (which include zero) |
| Cnew_scopet | |
| Cnil_exprt | The NIL expression |
| Cnil_typet | The NIL type |
| 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 | Inequality |
| Cnull_message_handlert | |
| Cnull_pointer_exprt | The null pointer constant |
| 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 |
| 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 |
| 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 generic 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, unsigned > | |
| 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 |
| Crational_typet | Unbounded, signed rational numbers |
| Crationalt | |
| Crd_range_domaint | |
| ▶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 | |
| 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 | |
| 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 function call side effect |
| Cside_effect_expr_nondett | A side effect that returns a non-deterministically chosen value |
| Cside_effect_expr_throwt | A side effect that throws an exception |
| Cside_effect_exprt | An expression containing a side effect |
| Csign_exprt | Sign of an expression |
| 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_parsert | |
| Cidt | |
| Csmt2_solvert | |
| Csmt2_stringstreamt | |
| Csmt2_temp_filet | |
| Csmt2_tokenizert | |
| Csmt2irept | |
| 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 | |
| Csparse_vectort | |
| Cssa_exprt | Expression providing an SSA-renamed symbol of expressions |
| Cstatic_analysis_baset | |
| Cstatic_analysist | |
| 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 | |
| Cformat_specifiert | |
| Cstring_constraintt | Universally quantified string constraint
|
| 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_exprt | |
| 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 | TO_BE_DOCUMENTED |
| Cstruct_exprt | Struct constructor from list of elements |
| Cstruct_tag_typet | A struct tag type |
| Cstruct_typet | Structure type |
| ▶Cstruct_union_typet | Base type of C structs and unions, and C++ classes |
| 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_tablet | The symbol table |
| Csymbol_typet | A reference into the symbol table |
| Csymbolt | Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet |
| Csymex_bmct | |
| ▶Csymex_coveraget | |
| Ccoverage_infot | |
| Csymex_dereference_statet | |
| Csymex_slice_by_tracet | |
| Csymex_slicet | |
| ▶Csymex_target_equationt | |
| CSSA_stept | |
| ▶Csymex_targett | |
| Csourcet | |
| Csyntactic_difft | |
| Csystem_library_symbolst | |
| Ctag_typet | A generic tag-based type |
| Ctaint_analysist | |
| ▶Ctaint_parse_treet | |
| Crulet | |
| Ctdefl_compressor | |
| Ctdefl_output_buffer | |
| Ctdefl_sym_freq | |
| Ctemp_dirt | |
| Ctemp_working_dirt | |
| Ctemplate_mapt | |
| Ctemplate_numberingt | |
| Ctemplate_parametert | |
| Ctemplate_typet | |
| Ctemporary_filet | |
| Ctimestampert | Timestamp class hierarchy |
| Ctinfl_decompressor_tag | |
| Ctinfl_huff_table | |
| Cto_be_merged_irep_hash | |
| Cto_be_merged_irept | |
| Ctrace_automatont | |
| Ctrace_optionst | |
| Ctranst | A 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 | |
| Ctype_with_subtypet | |
| Ctypecast_exprt | Semantic type conversion |
| Ctypecheckt | |
| Ctypedef_typet | A typedef |
| Ctypet | The type of an expression |
| Cui_message_handlert | |
| Cunary_exprt | Generic base class for unary expressions |
| Cunary_minus_exprt | The unary minus expression |
| Cunary_predicate_exprt | A generic 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 | |
| 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 |
| 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 |
| Cunwindsett | |
| Cupdate_exprt | Operator to update elements in structs and arrays |
| Cvalue_set_analysis_fit | |
| Cvalue_set_analysis_fivrnst | |
| Cvalue_set_analysis_fivrt | |
| Cvalue_set_analysis_templatet | |
| ▶Cvalue_set_dereferencet | TO_BE_DOCUMENTED |
| 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 | A constant-size array type |
| Cvisited_nodet | A node type with an extra bit |
| Cvoid_typet | The void type |
| 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.14