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 | |