| 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 |
| Cabsolute_timet | |
| Cabstract_eventt | |
| Cacceleratet | |
| ▶Cacceleration_utilst | |
| Cpolynomial_array_assignmentt | |
| Caddress_of_exprt | Operator to return the address of an object |
| Cai_baset | |
| Cai_domain_baset | |
| Caig_nodet | |
| Caig_plus_constraintst | |
| Caig_prop_baset | |
| Caig_prop_constraintt | |
| Caig_prop_solvert | |
| Caigt | |
| Cait | |
| Call_paths_enumeratort | |
| Cand_exprt | Boolean AND |
| Cansi_c_convert_typet | |
| Cansi_c_declarationt | |
| Cansi_c_declaratort | |
| Cansi_c_identifiert | |
| Cansi_c_languaget | |
| Cansi_c_parse_treet | |
| Cansi_c_parsert | |
| Cansi_c_scopet | |
| Cansi_c_typecheckt | |
| Carmcc_cmdlinet | |
| Carmcc_modet | |
| Carray_exprt | Array constructor from list of elements |
| Carray_of_exprt | Array constructor from single element |
| 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 | |
| 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_type_eqt | |
| Cbasic_blockst | |
| 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_typet | Base class of bitvector types |
| Cbitxor_exprt | Bit-wise XOR |
| ▶Cbmc_all_propertiest | |
| Cgoalt | |
| ▶Cbmc_covert | |
| ▶Cgoalt | |
| Cinstancet | |
| Ctestt | |
| Cbmct | |
| Cbool_typet | The proper Booleans |
| ▶Cboolbv_mapt | |
| Cmap_bitt | |
| Cmap_entryt | |
| ▶Cboolbv_widtht | |
| Centryt | |
| Cmembert | |
| ▶Cboolbvt | |
| Cquantifiert | |
| Cbv_arithmetict | |
| Cbv_cbmct | |
| Cbv_minimizet | |
| Cbv_minimizing_dect | |
| ▶Cbv_pointerst | |
| Cpostponedt | |
| ▶Cbv_refinementt | |
| Capproximationt | |
| 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_sizeoft | |
| Cc_storage_spect | |
| Cc_typecastt | |
| Cc_typecheck_baset | |
| Ccall_grapht | |
| 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_methodst | |
| ▶Cclass_hierarchyt | |
| Centryt | |
| Cclass_typet | C++ class type |
| ▶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 | An assertion |
| Ccode_assignt | Assignment |
| Ccode_assumet | An assumption |
| 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_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 | |
| Ccppt | |
| Cjavat | |
| Cverilogt | |
| Cconsole_message_handlert | |
| Cconst_expr_visitort | |
| ▶Cconst_function_pointer_propagationt | |
| Carg_stackt | |
| Cconst_graph_visitort | |
| Cconst_target_hash_templatet | |
| Cconstant_exprt | A constant literal expression |
| Cconstant_propagator_ait | |
| ▶Cconstant_propagator_domaint | |
| Cvaluest | |
| Ccounterexample_beautificationt | |
| Ccout_message_handlert | |
| ▶Ccover_goalst | Try to cover some given set of goals incrementally |
| Cgoalt | |
| Cobservert | |
| 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 | |
| ▶Ccvc_convt | |
| Cidentifiert | |
| Ccvc_dect | |
| Ccvc_propt | |
| Ccvc_temp_filet | |
| Ccw_modet | |
| Ccycles_visitort | |
| Cdata | |
| Cdata_dpt | |
| Cdatat | |
| Cdecision_proceduret | |
| Cdecorated_symbol_exprt | Expression to hold a symbol (variable) |
| Cdep_edget | |
| Cdep_graph_domaint | |
| Cdep_nodet | |
| Cdependence_grapht | |
| 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 | |
| Cdiv_exprt | Division (integer and real) |
| ▶Cdocument_propertiest | |
| Cdoc_claimt | |
| Clinet | |
| Cdoes_remove_constt | |
| Cdomain_baset | |
| Cdott | |
| ▶Cdplib_convt | |
| Cidentifiert | |
| Cdplib_dect | |
| Cdplib_propt | |
| Cdplib_temp_filet | |
| Cdstring_hash | |
| Cdstringt | |
| ▶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 | |
| Cerror_baset | |
| Cerror_streamt | |
| 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_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 | |
| Cfence_all_shared_aegt | |
| Cfence_all_sharedt | |
| Cfence_assert_insertert | |
| Cfence_insertert | |
| Cfence_user_def_insertert | |
| Cfence_volatilet | |
| Cfile | |
| Cfiledescriptor_streambuft | |
| Cfind_index_visitort | |
| Cfind_qvar_visitort | |
| Cfine_timet | |
| Cfixedbv_spect | |
| Cfixedbv_typet | Fixed-width bit-vector with signed fixed-point interpretation |
| Cfixedbvt | |
| 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_spect | |
| Cformat_token_listt | |
| Cformat_tokent | |
| ▶Cfull_slicert | |
| Ccfg_nodet | |
| Cfunction_application_exprt | Application of (mathematical) function |
| Cfunction_modifiest | |
| ▶Cfunctionst | |
| Cfunction_infot | |
| Cgcc_cmdlinet | |
| Cgcc_message_handlert | |
| Cgcc_modet | |
| Cglobal_may_alias_analysist | |
| Cglobal_may_alias_domaint | |
| Cgoto_analyzer_parse_optionst | |
| ▶Cgoto_cc_cmdlinet | |
| Cargt | |
| Cgoto_cc_modet | |
| Cgoto_checkt | |
| Cgoto_convert_functionst | |
| ▶Cgoto_convertt | |
| Cbreak_continue_targetst | |
| Cbreak_switch_targetst | |
| Cguarded_gotot | |
| Cleave_targett | |
| Ctargetst | |
| Cthrow_targett | |
| Cgoto_diff_languagest | |
| Cgoto_diff_parse_optionst | |
| Cgoto_difft | |
| Cgoto_fence_inserter_parse_optionst | |
| Cgoto_function_templatet | |
| Cgoto_functions_templatet | |
| Cgoto_functionst | |
| ▶Cgoto_inlinet | |
| ▶Cgoto_inline_logt | |
| Cgoto_inline_log_infot | |
| Cgoto_instrument_parse_optionst | |
| Cgoto_modelt | |
| ▶Cgoto_program2codet | |
| Ccaset | |
| ▶Cgoto_program_coverage_recordt | |
| Ccoverage_conditiont | |
| Ccoverage_linet | |
| Cgoto_program_dereferencet | |
| ▶Cgoto_program_templatet | A generic container class for the GOTO intermediate representation of one function |
| Cinstructiont | This class represents an instruction in the GOTO intermediate representation |
| Cgoto_programt | A specialization of goto_program_templatet over goto programs in which instructions have codet type |
| ▶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 | |
| Chash_numbering | |
| 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 |
| Cilpt | |
| Cimplies_exprt | Boolean implication |
| Cincomplete_array_typet | Arrays without size |
| Cindex_designatort | |
| Cindex_exprt | Array index operator |
| Cinfinity_exprt | An expression denoting infinity |
| Cinflate_state | |
| Cinode | |
| Cinstrumenter_pensievet | |
| ▶Cinstrumentert | |
| Ccfg_visitort | |
| Cinteger_typet | Unbounded, signed integers |
| ▶Cinterpretert | |
| Cmemory_cellt | |
| Cstack_framet | |
| Cinterval_domaint | |
| 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 | |
| Cpointer_hasht | |
| Cvector_hasht | |
| Cirep_hash_containert | |
| ▶Cirep_serializationt | |
| Cireps_containert | |
| ▶Cirept | Base class for tree-like data structures with sharing |
| Cdt | |
| Cis_name_equalt | |
| Cis_predecessor_oft | |
| Cis_threaded_domaint | |
| Cis_threadedt | |
| Cis_virtual_name_equalt | |
| 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 |
| Cjar_filet | |
| Cjar_poolt | |
| Cjava_bytecode_convert_classt | |
| ▶Cjava_bytecode_convert_methodt | |
| Cblock_tree_nodet | |
| Cconverted_instructiont | |
| Cholet | |
| Clocal_variable_with_holest | |
| Cvariablet | |
| Cjava_bytecode_languaget | |
| ▶Cjava_bytecode_parse_treet | |
| ▶Cannotationt | |
| Celement_value_pairt | |
| Cclasst | |
| Cfieldt | |
| Cinstructiont | |
| Cmembert | |
| ▶Cmethodt | |
| Cexceptiont | |
| Clocal_variablet | |
| Cstack_map_table_entryt | |
| Cverification_type_infot | |
| ▶Cjava_bytecode_parsert | |
| Cbytecodet | |
| Cpool_entryt | |
| Cjava_bytecode_typecheckt | |
| Cjava_bytecode_vtable_factoryt | |
| Cjava_class_loader_limitt | |
| ▶Cjava_class_loadert | |
| ▶Cjar_map_entryt | |
| Centryt | |
| Cjava_object_factoryt | |
| Cjsil_builtin_code_typet | |
| Cjsil_convertt | |
| Cjsil_declarationt | |
| Cjsil_languaget | |
| Cjsil_parse_treet | |
| Cjsil_parsert | |
| Cjsil_spec_code_typet | |
| Cjsil_typecheckt | |
| Cjsil_union_typet | |
| Cjson_arrayt | |
| Cjson_falset | |
| Cjson_irept | |
| Cjson_nullt | |
| Cjson_numbert | |
| Cjson_objectt | |
| Cjson_parsert | |
| Cjson_stringt | |
| Cjson_truet | |
| Cjsont | |
| Ck_inductiont | |
| Clanguage_entryt | |
| Clanguage_filest | |
| Clanguage_filet | |
| Clanguage_modulet | |
| Clanguage_uit | |
| Clanguagest | |
| Clanguaget | |
| Cld_cmdlinet | |
| Clet_exprt | A let expression |
| Clinear_recurrencet | |
| ▶Clinkingt | |
| Cadjust_type_infot | |
| Clispexprt | |
| Clispsymbolt | |
| Cliteral_exprt | |
| Cliteralt | |
| Cloc_reft | |
| ▶Clocal_bitvector_analysist | |
| Cflagst | |
| Cloc_infot | |
| ▶Clocal_cfgt | |
| Cnodet | |
| Clocal_may_alias_factoryt | |
| ▶Clocal_may_aliast | |
| Cloc_infot | |
| Clocalst | |
| ▶Clocst | |
| Cfunction_entryt | |
| Cloct | |
| Cloop_accelerationt | |
| Clshr_exprt | Logical right shift |
| Cmain_function_resultt | |
| 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 | |
| Cmini_bdd_applyt | |
| ▶Cmini_bdd_mgrt | |
| Creverse_keyt | |
| Cvar_table_entryt | |
| Cmini_bdd_nodet | |
| Cmini_bddt | |
| Cminisat_prooft | |
| Cminus_exprt | Binary minus |
| Cmip_vart | |
| Cmm2cppt | |
| Cmm_parsert | |
| Cmmcc_parse_optionst | |
| Cmod_exprt | Binary modulo |
| ▶Cmonomialt | |
| Ctermt | |
| Cms_cl_cmdlinet | |
| Cms_cl_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_array | |
| Cmz_zip_internal_state_tag | |
| Cmz_zip_writer_add_state | |
| 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 |
| Cnot_exprt | Boolean negation |
| Cnotequal_exprt | Inequality |
| Cnull_message_handlert | |
| Cnull_pointer_exprt | The null pointer constant |
| Cnullptr_exceptiont | |
| Cnumbering | |
| Cobject_descriptor_exprt | Split an expression into a base object and a (byte) offset |
| 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_options_baset | |
| CParser | |
| Cparsert | |
| ▶Cpartial_order_concurrencyt | |
| Ca_rect | |
| Cpath_accelerationt | |
| Cpath_acceleratort | |
| Cpath_enumeratort | |
| Cpath_nodet | |
| Cpath_replayt | |
| ▶Cpath_searcht | |
| Cloc_datat | |
| Cproperty_entryt | |
| Cpath_symex_historyt | |
| ▶Cpath_symex_statet | |
| Cframet | |
| Cthreadt | |
| Cvar_statet | |
| Cpath_symex_step_reft | |
| Cpath_symex_stept | |
| Cpath_symext | |
| Cpatternt | |
| Cpbs_dimacs_cnft | |
| Cpipe_streamt | |
| Cplus_exprt | The plus expression |
| Cpointer_arithmetict | |
| ▶Cpointer_logict | |
| Cpointert | |
| Cpointer_typet | The pointer type |
| Cpoints_tot | |
| ▶Cpolynomial_acceleratort | |
| Cpolynomial_array_assignment | |
| Cpolynomialt | |
| 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_assignmentt | TO_BE_DOCUMENTED |
| Cprop_conv_solvert | TO_BE_DOCUMENTED |
| ▶Cprop_conv_storet | |
| Cconstraintst | |
| Cconstraintt | |
| Cprop_convt | |
| ▶Cprop_minimizet | Computes a satisfying assignment of minimal cost according to a const function using incremental SAT |
| Cobjectivet | |
| Cprop_wrappert | |
| 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 | |
| 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 | |
| Cslicer_entryt | |
| Creaching_definitions_analysist | |
| Creaching_definitiont | |
| Creal_typet | Unbounded, signed real numbers |
| Crecursion_countert | |
| Cref_expr_set_dt | |
| Cref_expr_sett | |
| ▶Creference_counting | |
| Cdt | |
| Creference_typet | The reference type |
| Crefined_string_typet | |
| Crem_exprt | Remainder of division |
| Cremove_asmt | |
| Cremove_const_function_pointerst | |
| Cremove_exceptionst | |
| Cremove_function_pointerst | |
| Cremove_instanceoft | |
| Cremove_returnst | |
| Cremove_static_init_loopst | |
| ▶Cremove_virtual_functionst | |
| Cfunctiont | |
| Crename_symbolt | |
| Creplace_symbol_extt | |
| Creplace_symbolt | |
| Creplication_exprt | Bit-vector replication |
| Cresolution_prooft | |
| 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 | |
| Csafe_pointer | |
| 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_glucose_baset | |
| Csatcheck_glucose_no_simplifiert | |
| Csatcheck_glucose_simplifiert | |
| Csatcheck_limmatt | |
| Csatcheck_lingelingt | |
| Csatcheck_minisat1_baset | |
| Csatcheck_minisat1_coret | |
| Csatcheck_minisat1_prooft | |
| Csatcheck_minisat1t | |
| Csatcheck_minisat2_baset | |
| Csatcheck_minisat_no_simplifiert | |
| Csatcheck_minisat_simplifiert | |
| Csatcheck_picosatt | |
| Csatcheck_precosatt | |
| Csatcheck_smvsat_coret | |
| ▶Csatcheck_smvsat_interpolatort | |
| Centryt | |
| Csatcheck_smvsatt | |
| Csatcheck_zchaff_baset | |
| Csatcheck_zchafft | |
| Csatcheck_zcoret | |
| Csave_scopet | |
| Cscratch_programt | |
| ▶Cshared_bufferst | |
| Ccfg_visitort | |
| Cvarst | |
| ▶Csharing_mapt | |
| Cdelta_view_itemt | |
| ▶Csharing_nodet | |
| Cdt | |
| Cshift_exprt | A base class for shift operators |
| Cshl_exprt | Left shift |
| Cshow_goto_functions_jsont | |
| Cshow_goto_functions_xmlt | |
| Cside_effect_expr_catcht | A side effect that pushes/pops a catch handler |
| 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 |
| Csimple_insertiont | |
| Csimplify_exprt | |
| Cslicing_criteriont | |
| ▶Csmt1_convt | |
| Cidentifiert | |
| ▶Csmt1_dect | Decision procedure interface for various SMT 1.x solvers |
| Cvaluet | |
| Csmt1_propt | |
| Csmt1_temp_filet | |
| ▶Csmt2_convt | |
| Cidentifiert | |
| Clet_visitort | |
| Csmt2_symbolt | |
| Csmt2_dect | Decision procedure interface for various SMT 2.x solvers |
| Csmt2_parsert | |
| Csmt2_propt | |
| Csmt2_stringstreamt | |
| Csmt2_temp_filet | |
| Csmt2irept | |
| Csorted_vector | |
| Csource_locationt | |
| Csparse_bitvector_analysist | |
| Cssa_exprt | Expression providing an SSA-renamed symbol of expressions |
| Cstatic_analysis_baset | |
| Cstatic_analysist | |
| Cstatic_analyzert | |
| Cstream_message_handlert | |
| Cstring_abstractiont | |
| Cstring_constantt | |
| Cstring_constraint_generatort | |
| Cstring_constraintt | |
| Cstring_containert | |
| Cstring_exprt | |
| Cstring_hash | |
| Cstring_instrumentationt | |
| Cstring_not_contains_constraintt | |
| Cstring_ptr_hash | |
| Cstring_ptrt | |
| Cstring_refinementt | |
| Cstring_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 | |
| Csubsumed_patht | |
| Csymbol_exprt | Expression to hold a symbol (variable) |
| Csymbol_factoryt | |
| 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_parse_optionst | |
| Csymex_slice_by_tracet | |
| Csymex_slicet | |
| ▶Csymex_target_equationt | |
| CSSA_stept | |
| ▶Csymex_targett | |
| Csourcet | |
| Csyntactic_difft | |
| Ctag_typet | A generic tag-based type |
| Ctaint_analysist | |
| ▶Ctaint_parse_treet | |
| Crulet | |
| Ctarget_to_loc_mapt | |
| Ctdefl_compressor | |
| Ctdefl_output_buffer | |
| Ctdefl_sym_freq | |
| Ctemp_dirt | |
| Ctemp_working_dirt | |
| Ctemplate_mapt | |
| Ctemplate_parametert | |
| Ctemplate_typet | |
| Ctemporary_filet | |
| Ctime_periodt | |
| Ctimert | |
| Ctinfl_decompressor_tag | |
| Ctinfl_huff_table | |
| Cto_be_merged_irep_hash | |
| Cto_be_merged_irept | |
| Ctrace_automatont | |
| Ctranst | A transition system, consisting of state invariant, initial state predicate, and transition predicate |
| 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 | |
| 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 |
| Cunified_difft | |
| Cuninitialized_domaint | |
| Cuninitializedt | |
| Cunion_exprt | Union constructor from single element |
| Cunion_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 |
| Cupdate_exprt | Operator to update elements in structs and arrays |
| Cvalue_set_analysis_fit | |
| Cvalue_set_analysis_fivrnst | |
| Cvalue_set_analysis_fivrt | |
| Cvalue_set_analysist | |
| ▶Cvalue_set_dereferencet | TO_BE_DOCUMENTED |
| Cvaluet | |
| Cvalue_set_domain_fit | |
| Cvalue_set_domain_fivrnst | |
| Cvalue_set_domain_fivrt | |
| Cvalue_set_domaint | |
| ▶Cvalue_set_fit | |
| Centryt | |
| Cobject_map_dt | |
| Cobjectt | |
| ▶Cvalue_set_fivrnst | |
| Centryt | |
| ▶Cobject_map_dt | |
| Cvalidity_ranget | |
| Cobjectt | |
| ▶Cvalue_set_fivrt | |
| Centryt | |
| ▶Cobject_map_dt | |
| Cvalidity_ranget | |
| Cobjectt | |
| Cvalue_setst | |
| ▶Cvalue_sett | |
| Centryt | |
| Cobject_map_dt | |
| Cobjectt | |
| ▶Cvar_mapt | |
| Cvar_infot | |
| 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 | |
| Cwith_exprt | Operator to update elements in structs and arrays |
| Cxml_edget | |
| Cxml_goto_function_convertt | |
| Cxml_goto_program_convertt | |
| Cxml_graph_nodet | |
| Cxml_interfacet | |
| ▶Cxml_irep_convertt | |
| Cirep_content_eq | |
| Cirep_full_hash | |
| Cireps_containert | |
| Cul_eq | |
| Cul_hash | |
| Cxml_parse_treet | |
| Cxml_parsert | |
| Cxml_symbol_convertt | |
| Cxmlt | |
| Cyy_buffer_state | |
| Cyy_trans_info | |
| Cyyalloc | |
| CYYSTYPE | |
| Czero_initializert | |
1.8.14