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 | |
Cpartial_order_concurrencyt::a_rect | |
Cacceleratet | |
Cacceleration_utilst | |
Clinkingt::adjust_type_infot | |
▶Cai_baset | |
▶Cait< domainT > | |
Cconcurrency_aware_ait< domainT > | |
▶Cait< constant_propagator_domaint > | |
Cconstant_propagator_ait | |
▶Cait< custom_bitvector_domaint > | |
Ccustom_bitvector_analysist | |
▶Cait< dep_graph_domaint > | |
Cdependence_grapht | |
▶Cait< escape_domaint > | |
Cescape_analysist | |
▶Cait< global_may_alias_domaint > | |
Cglobal_may_alias_analysist | |
Cait< interval_domaint > | |
▶Cait< invariant_set_domaint > | |
Cinvariant_propagationt | |
▶Cait< rd_range_domaint > | |
▶Cconcurrency_aware_ait< rd_range_domaint > | |
Creaching_definitions_analysist | |
Cait< uninitialized_domaint > | |
▶Cai_domain_baset | |
Cconstant_propagator_domaint | |
Ccustom_bitvector_domaint | |
Cdep_graph_domaint | |
Cescape_domaint | |
Cglobal_may_alias_domaint | |
Cinterval_domaint | |
Cinvariant_set_domaint | |
Cis_threaded_domaint | |
Crd_range_domaint | |
Cuninitialized_domaint | |
Caig_nodet | |
▶Caigt | |
Caig_plus_constraintst | |
Cjava_bytecode_parse_treet::annotationt | |
Cansi_c_identifiert | |
Cansi_c_parse_treet | |
Cansi_c_scopet | |
Cconfigt::ansi_ct | |
Cbv_refinementt::approximationt | |
Cgoto_cc_cmdlinet::argt | |
Carrayst::array_equalityt | |
Cautomatont | |
Cbase_type_eqt | |
Cbasic_blockst | |
▶Cstd::basic_string< Char > | STL class |
▶Cstd::string | STL class |
Clispsymbolt | |
Cbdd_exprt | TO_BE_DOCUMENTED |
Cjava_bytecode_convert_methodt::block_tree_nodet | |
Cboolbv_mapt | |
Cboolbv_widtht | |
Cgoto_convertt::break_continue_targetst | |
Cgoto_convertt::break_switch_targetst | |
Cbv_arithmetict | |
Cbv_spect | |
Cbv_utilst | |
Cbytecode_infot | |
Cjava_bytecode_parsert::bytecodet | |
Cc_qualifierst | |
Cc_sizeoft | |
Cc_storage_spect | |
▶Cc_typecastt | |
Ccpp_typecastt | |
Ccall_grapht | |
Ccheck_call_sequencet::call_stack_entryt | |
Cgoto_program2codet::caset | |
Ccfg_dominators_templatet< P, T, post_dom > | |
Ccfg_dominators_templatet< const goto_programt, goto_programt::const_targett, false > | |
Ccfg_dominators_templatet< goto_programt, goto_programt::targett, false > | |
Ccfg_dominators_templatet< P, T, false > | |
Cfull_slicert::cfg_nodet | |
Cinstrumentert::cfg_visitort | |
Cshared_bufferst::cfg_visitort | |
Cchange_impactt | |
Ccheck_call_sequencet | |
Cci_lazy_methodst | |
Cclass_hierarchyt | |
Cjava_bytecode_parse_treet::classt | |
Cclauset | |
Cescape_domaint::cleanupt | |
▶Ccmdlinet | |
▶Cgoto_cc_cmdlinet | |
Carmcc_cmdlinet | |
Cas86_cmdlinet | |
Cas_cmdlinet | |
Cbcc_cmdlinet | |
Cgcc_cmdlinet | |
Cld_cmdlinet | |
Cms_cl_cmdlinet | |
Ccode_contractst | |
Cconcurrency_instrumentationt | |
Ccone_of_influencet | |
Cconfigt | Globally accessible architectural configuration |
▶Cconst_expr_visitort | |
Cfind_index_visitort | |
Cfind_qvar_visitort | |
Cconst_function_pointer_propagationt | |
Cconst_graph_visitort | |
Cconst_target_hash_templatet< codeT, guardT > | |
Cprop_conv_storet::constraintst | |
Cprop_conv_storet::constraintt | |
Cjava_bytecode_convert_methodt::converted_instructiont | |
Ccounterexample_beautificationt | |
Cgoto_program_coverage_recordt::coverage_conditiont | |
Csymex_coveraget::coverage_infot | |
Cgoto_program_coverage_recordt::coverage_linet | |
▶Ccoverage_recordt | |
Cgoto_program_coverage_recordt | |
Ccpp_convert_typet | |
Ccpp_declarator_convertert | |
▶Ccpp_idt | |
▶Ccpp_scopet | |
Ccpp_root_scopet | |
Ccpp_parse_treet | |
Ccpp_save_scopet | |
Ccpp_saved_template_mapt | |
Ccpp_scopest | |
Ccpp_token_buffert | |
Ccpp_tokent | |
Ccpp_typecheck_fargst | |
Ccpp_typecheck_resolvet | |
Cconfigt::cppt | |
Ccprover_library_entryt | |
▶Ccvc_temp_filet | |
Ccvc_dect | |
Ccycles_visitort | |
Cdata | |
Cdatat | |
Cevent_grapht::critical_cyclet::delayt | |
Csharing_mapt< keyT, valueT, hashT, predT >::delta_view_itemt | |
Cdep_edget | |
▶Cdereference_callbackt | TO_BE_DOCUMENTED |
Cgoto_program_dereferencet | |
Csymex_dereference_statet | |
Cdereferencet | TO_BE_DOCUMENTED |
Cdesignatort | |
Cdirtyt | |
Cdocument_propertiest::doc_claimt | |
Cdocument_propertiest | |
Cdoes_remove_constt | |
▶Cdomain_baset | |
Cvalue_set_domaint | |
Cdott | |
▶Cdplib_temp_filet | |
Cdplib_dect | |
Cdstring_hash | |
Cdstringt | |
Cirept::dt | |
Csharing_nodet< keyT, valueT, predT, no_sharing >::dt | |
Cdump_ct | |
Cjava_bytecode_parse_treet::annotationt::element_value_pairt | |
CElf32_Ehdr | |
CElf32_Shdr | |
CElf64_Ehdr | |
CElf64_Shdr | |
Celf_readert | |
Cempty_cfg_nodet | |
Cempty_edget | |
Cendianness_mapt | Maps a big-endian offset to a little-endian offset |
Cjava_class_loadert::jar_map_entryt::entryt | |
Cvalue_sett::entryt | |
Cvalue_set_fit::entryt | |
Cvalue_set_fivrt::entryt | |
Cvalue_set_fivrnst::entryt | |
Cboolbv_widtht::entryt | |
Cinv_object_storet::entryt | |
Csatcheck_smvsat_interpolatort::entryt | |
Crw_set_baset::entryt | |
Cclass_hierarchyt::entryt | |
Cdesignatort::entryt | |
Cprintf_formattert::eol_exceptiont | |
Cevent_grapht | |
▶Cstd::exception | STL class |
▶Cerror_baset | |
Cerror_streamt | |
▶Cstd::logic_error | STL class |
▶Cinvariant_failedt | A logic error, augmented with a distinguished field to hold a backtrace |
Cbad_cast_exceptiont | |
Cnullptr_exceptiont | |
Cjava_bytecode_parse_treet::methodt::exceptiont | |
▶Cexpr2ct | |
Cexpr2cppt | |
Cexpr2javat | |
Cexpr2jsilt | |
▶Cexpr_visitort | |
Csmt2_convt::let_visitort | |
▶Cfence_insertert | |
Cfence_assert_insertert | |
Cfence_user_def_insertert | |
Cfile | |
▶Cfine_timet | |
Cabsolute_timet | |
Ctime_periodt | |
Cfixedbv_spect | |
Cfixedbvt | |
Clocal_bitvector_analysist::flagst | |
Cfloat_bvt | |
▶Cfloat_utilst | |
Cfloat_approximationt | |
▶Cflow_insensitive_abstract_domain_baset | |
Cvalue_set_domain_fit | |
Cvalue_set_domain_fivrnst | |
Cvalue_set_domain_fivrt | |
▶Cflow_insensitive_analysis_baset | |
Cflow_insensitive_analysist< T > | |
▶Cflow_insensitive_analysist< value_set_domain_fit > | |
Cvalue_set_analysis_fit | |
▶Cflow_insensitive_analysist< value_set_domain_fivrnst > | |
Cvalue_set_analysis_fivrnst | |
▶Cflow_insensitive_analysist< value_set_domain_fivrt > | |
Cvalue_set_analysis_fivrt | |
▶Cformat_spect | |
Cformat_constantt | |
Cformat_tokent | |
Cpath_symex_statet::framet | |
Cgoto_symex_statet::framet | |
Cfull_slicert | |
Clocst::function_entryt | |
Cfunctionst::function_infot | |
Cfunction_modifiest | |
Cfunctionst | |
Cremove_virtual_functionst::functiont | |
Ccover_goalst::goalt | |
Cbmc_all_propertiest::goalt | |
Cbmc_covert::goalt | |
Cgoto_checkt | |
Cgoto_function_templatet< bodyT > | |
Cgoto_functions_templatet< bodyT > | |
▶Cgoto_functions_templatet< goto_programt > | |
Cgoto_functionst | |
Cgoto_inlinet::goto_inline_logt::goto_inline_log_infot | |
Cgoto_inlinet::goto_inline_logt | |
Cgoto_modelt | |
Cgoto_program2codet | |
Cgoto_program_templatet< codeT, guardT > | A generic container class for the GOTO intermediate representation of one function |
▶Cgoto_program_templatet< codet, exprt > | |
▶Cgoto_programt | A specialization of goto_program_templatet over goto programs in which instructions have codet type |
Cscratch_programt | |
Cgoto_symex_statet::goto_statet | |
Cgoto_symex_statet | |
▶Cgoto_symext | The main class for the forward symbolic simulator |
Csymex_bmct | |
Cgoto_trace_stept | TO_BE_DOCUMENTED |
Cgoto_tracet | TO_BE_DOCUMENTED |
Cgoto_unwindt | |
▶Cevent_grapht::graph_explorert | |
Cevent_grapht::graph_conc_explorert | |
Cevent_grapht::graph_pensieve_explorert | |
▶Cgraph_nodet< E > | This class represents a node in a directed graph |
Cvisited_nodet< E > | A node type with an extra bit |
▶Cgraph_nodet< dep_edget > | |
Cdep_nodet | |
▶Cgraph_nodet< empty_edget > | |
Cabstract_eventt | |
Ccfg_base_nodet< T, I > | |
▶Cgraph_nodet< xml_edget > | |
Cxml_graph_nodet | |
Cgraphml_witnesst | |
Cgrapht< N > | A generic directed graph with a parametric node type |
Cgrapht< abstract_eventt > | |
▶Cgrapht< cfg_base_nodet< cfg_nodet, goto_programt::const_targett > > | |
Ccfg_baset< cfg_nodet > | |
▶Cgrapht< cfg_base_nodet< empty_cfg_nodet, goto_programt::const_targett > > | |
Ccfg_baset< empty_cfg_nodet > | |
▶Cgrapht< cfg_base_nodet< nodet, goto_programt::const_targett > > | |
▶Ccfg_baset< nodet, const goto_programt, goto_programt::const_targett > | |
Cprocedure_local_cfg_baset< nodet, const goto_programt, goto_programt::const_targett > | |
▶Cgrapht< cfg_base_nodet< nodet, goto_programt::targett > > | |
▶Ccfg_baset< nodet, goto_programt, goto_programt::targett > | |
Cprocedure_local_cfg_baset< nodet, goto_programt, goto_programt::targett > | |
▶Cgrapht< cfg_base_nodet< nodet, T > > | |
▶Ccfg_baset< nodet, P, T > | |
Cprocedure_local_cfg_baset< nodet, P, T > | |
▶Cgrapht< cfg_base_nodet< slicer_entryt, goto_programt::const_targett > > | |
Ccfg_baset< slicer_entryt > | |
▶Cgrapht< cfg_base_nodet< T, I > > | |
▶Ccfg_baset< T, P, I > | A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO program |
▶Cconcurrent_cfg_baset< T, P, I > | |
Cprocedure_local_concurrent_cfg_baset< T, P, I > | |
▶Cprocedure_local_cfg_baset< T, P, I > | |
Cprocedure_local_concurrent_cfg_baset< T, P, I > | |
▶Cgrapht< cfg_base_nodet< T, unsigned > > | |
Cprocedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, unsigned > | |
▶Cgrapht< dep_nodet > | |
Cdependence_grapht | |
▶Cgrapht< xml_graph_nodet > | |
Cgraphmlt | |
Cgoto_convertt::guarded_gotot | |
Chavoc_loopst | |
Cjava_bytecode_convert_methodt::holet | |
Ccvc_convt::identifiert | |
Cdplib_convt::identifiert | |
Csmt1_convt::identifiert | |
Csmt2_convt::identifiert | |
Cidentifiert | |
Cieee_float_spect | |
Cieee_floatt | |
Cilpt | |
Cinflate_state | |
Cinode | |
Cbmc_covert::goalt::instancet | |
Ccpp_typecheckt::instantiation_levelt | |
Ccpp_typecheckt::instantiationt | |
Cjava_bytecode_parse_treet::instructiont | |
Cgoto_program_templatet< codeT, guardT >::instructiont | This class represents an instruction in the GOTO intermediate representation |
▶Cinstrumentert | |
Cinstrumenter_pensievet | |
Cinterpretert | |
Cinterval_templatet< T > | |
Cinv_object_storet | |
Cinvariant_sett | |
▶Cstd::ios_base | STL class |
▶Cstd::basic_ios< Char > | STL class |
▶Cstd::basic_ostream< Char > | STL class |
▶Cstd::basic_ostringstream< Char > | STL class |
▶Cstd::ostringstream | STL class |
Cerror_streamt | |
Cmessaget::mstreamt | |
▶Ciostream | |
Cpipe_streamt | |
Cxml_irep_convertt::irep_content_eq | |
Cirep_full_eq | |
Cxml_irep_convertt::irep_full_hash | |
Cirep_full_hash | |
Cirep_hash | |
▶Cirep_hash_container_baset | |
Cirep_full_hash_containert | |
Cirep_hash_containert | |
Cirep_serializationt | |
Cxml_irep_convertt::ireps_containert | |
Cirep_serializationt::ireps_containert | |
▶Cirept | Base class for tree-like data structures with sharing |
Cc_enum_typet::c_enum_membert | |
Ccpp_itemt | |
Ccpp_member_spect | |
Ccpp_namet | |
Ccpp_namet::namet | |
Ccpp_storage_spect | |
▶Ccpp_template_args_baset | |
Ccpp_template_args_non_tct | |
Ccpp_template_args_tct | |
Ccpp_usingt | |
▶Cexprt | Base class for all expressions |
Cansi_c_declarationt | |
Cansi_c_declaratort | |
Carray_exprt | Array constructor from list of elements |
▶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 |
Cequal_exprt | Equality |
Cieee_float_equal_exprt | IEEE-floating-point equality |
Cieee_float_notequal_exprt | IEEE floating-point disequality |
Cnotequal_exprt | Inequality |
Cextractbit_exprt | Extracts a single bit of a bit-vector operand |
Ccomplex_exprt | Complex constructor from a pair of numbers |
Cdiv_exprt | Division (integer and real) |
Cfactorial_power_exprt | Falling factorial power |
Cfloatbv_typecast_exprt | Semantic type conversion from/to floating-point formats |
Cimplies_exprt | Boolean implication |
Cminus_exprt | Binary minus |
Cmod_exprt | Binary modulo |
Cpower_exprt | Exponentiation |
Crem_exprt | Remainder of division |
Creplication_exprt | Bit-vector replication |
▶Cshift_exprt | A base class for shift operators |
Cashr_exprt | Arithmetic right shift |
Clshr_exprt | Logical right shift |
Cshl_exprt | Left shift |
▶Cbyte_extract_exprt | TO_BE_DOCUMENTED |
Cbyte_extract_big_endian_exprt | TO_BE_DOCUMENTED |
Cbyte_extract_little_endian_exprt | TO_BE_DOCUMENTED |
▶Cbyte_update_exprt | TO_BE_DOCUMENTED |
Cbyte_update_big_endian_exprt | TO_BE_DOCUMENTED |
Cbyte_update_little_endian_exprt | TO_BE_DOCUMENTED |
Ccode_typet::parametert | |
▶Ccodet | A statement in a programming language |
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_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_whilet | A ‘while’ instruction |
Cconcatenation_exprt | Concatenation of bit-vector operands |
▶Cconstant_exprt | A constant literal expression |
Cfalse_exprt | The boolean constant false |
Cnull_pointer_exprt | The null pointer constant |
Ctrue_exprt | The boolean constant true |
Ccpp_declarationt | |
Ccpp_declaratort | |
Ccpp_linkage_spect | |
Ccpp_namespace_spect | |
Ccpp_static_assertt | |
Cdereference_exprt | Operator to dereference a pointer |
Cdynamic_object_exprt | TO_BE_DOCUMENTED |
Cexists_exprt | An exists expression |
Cextractbits_exprt | Extracts a sub-range of a bit-vector operand |
Cforall_exprt | A forall expression |
Cfunction_application_exprt | Application of (mathematical) function |
Cguardt | |
Cieee_float_op_exprt | IEEE floating-point operations |
Cif_exprt | The trinary if-then-else operator |
Cindex_designatort | |
Cindex_exprt | Array index operator |
Cinfinity_exprt | An expression denoting infinity |
Cjsil_declarationt | |
Clet_exprt | A let expression |
Cmember_designatort | |
Cmember_exprt | Extract member of struct or union |
▶Cmulti_ary_exprt | A generic base class for multi-ary expressions |
Cand_exprt | Boolean AND |
Cbitand_exprt | Bit-wise AND |
Cbitor_exprt | Bit-wise OR |
Cbitxor_exprt | Bit-wise XOR |
Cmult_exprt | Binary multiplication |
Cor_exprt | Boolean OR |
Cplus_exprt | The plus expression |
Cnil_exprt | The NIL expression |
Cnot_exprt | Boolean negation |
Cobject_descriptor_exprt | Split an expression into a base object and a (byte) offset |
▶Cpredicate_exprt | A generic base class for expressions that are predicates, i.e., boolean-typed |
Cliteral_exprt | |
▶Cside_effect_exprt | An expression containing a side effect |
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 |
Csmt2_convt::smt2_symbolt | |
Cstring_constantt | |
Cstring_constraintt | |
Cstring_not_contains_constraintt | |
▶Cstruct_exprt | Struct constructor from list of elements |
Cstring_exprt | |
Cstruct_union_typet::componentt | |
▶Csymbol_exprt | Expression to hold a symbol (variable) |
Cdecorated_symbol_exprt | Expression to hold a symbol (variable) |
Cssa_exprt | Expression providing an SSA-renamed symbol of expressions |
Ctemplate_parametert | |
Ctranst | A transition system, consisting of state invariant, initial state predicate, and transition predicate |
Ctype_exprt | An expression denoting a type |
Ctypecast_exprt | Semantic type conversion |
▶Cunary_exprt | Generic base class for unary expressions |
Cabs_exprt | Absolute value |
Caddress_of_exprt | Operator to return the address of an object |
Carray_of_exprt | Array constructor from single element |
Cbitnot_exprt | Bit-wise negation of bit-vectors |
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 |
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 |
Csign_exprt | Sign of an expression |
Cunion_exprt | Union constructor from single element |
Cupdate_exprt | Operator to update elements in structs and arrays |
Cvector_exprt | Vector constructor from list of elements |
Cwith_exprt | Operator to update elements in structs and arrays |
Cmerged_irept | |
Csource_locationt | |
Cto_be_merged_irept | |
▶Ctypet | The type of an expression |
Cbool_typet | The proper Booleans |
▶Ccode_typet | Base type of functions |
Cjsil_builtin_code_typet | |
Cjsil_spec_code_typet | |
Ccpp_enum_typet | |
▶Cempty_typet | The empty type |
Cvoid_typet | The void type |
Cenumeration_typet | A generic enumeration type (not to be confused with C enums) |
Cinteger_typet | Unbounded, signed integers |
Cnatural_typet | Natural numbers (which include zero) |
Cnil_typet | The NIL type |
Crange_typet | A type for subranges of integers |
Crational_typet | Unbounded, signed rational numbers |
Creal_typet | Unbounded, signed real numbers |
Cstring_typet | TO_BE_DOCUMENTED |
▶Cstruct_union_typet | Base type of C structs and unions, and C++ classes |
▶Cstruct_typet | Structure type |
Cclass_typet | C++ class type |
Crefined_string_typet | |
▶Cunion_typet | The union type |
Cjsil_union_typet | |
Csymbol_typet | A reference into the symbol table |
▶Ctag_typet | A generic tag-based type |
Cc_enum_tag_typet | An enum tag type |
Cstruct_tag_typet | A struct tag type |
Cunion_tag_typet | A union tag type |
Ctemplate_typet | |
Ctype_with_subtypest | |
▶Ctype_with_subtypet | |
Carray_typet | Arrays with given size |
▶Cbitvector_typet | Base class of bitvector types |
Cbv_typet | Fixed-width bit-vector without numerical interpretation |
Cc_bit_field_typet | Type for c bit fields |
Cc_bool_typet | The C/C++ Booleans |
Cfixedbv_typet | Fixed-width bit-vector with signed fixed-point interpretation |
Cfloatbv_typet | Fixed-width bit-vector with IEEE floating-point interpretation |
▶Cpointer_typet | The pointer type |
Creference_typet | The reference type |
Csignedbv_typet | Fixed-width bit-vector with two's complement interpretation |
Cunsignedbv_typet | Fixed-width bit-vector with unsigned binary interpretation |
Cc_enum_typet | The type of C enums |
Ccomplex_typet | Complex numbers made of pair of given subtype |
Cincomplete_array_typet | Arrays without size |
Cvector_typet | A constant-size array type |
Cis_name_equalt | |
Cis_predecessor_oft | |
Cis_threadedt | |
Cis_virtual_name_equalt | |
Cjava_class_loadert::jar_map_entryt | |
Cjava_bytecode_parse_treet | |
Cjava_bytecode_vtable_factoryt | |
Cjava_object_factoryt | |
Cconfigt::javat | |
Cjsil_parse_treet | |
Cjson_irept | |
▶Cjsont | |
Cjson_arrayt | |
Cjson_falset | |
Cjson_nullt | |
Cjson_numbert | |
Cjson_objectt | |
Cjson_stringt | |
Cjson_truet | |
Ck_inductiont | |
Clanguage_entryt | |
Clanguage_filet | |
Clanguage_modulet | |
Clanguagest | |
Carrayst::lazy_constraintt | |
Cgoto_convertt::leave_targett | |
Clinear_recurrencet | |
Cdocument_propertiest::linet | |
▶Cstd::list< T > | STL class |
Cevent_grapht::critical_cyclet | |
Cformat_token_listt | |
Crange_domaint | |
Cliteralt | |
Cpath_searcht::loc_datat | |
Clocal_bitvector_analysist::loc_infot | |
Clocal_may_aliast::loc_infot | |
Cloc_reft | |
Clocal_bitvector_analysist | |
Clocal_cfgt | |
Clocal_may_alias_factoryt | |
Clocal_may_aliast | |
Cjava_bytecode_convert_methodt::local_variable_with_holest | |
Cjava_bytecode_parse_treet::methodt::local_variablet | |
Clocalst | |
Clocst | |
Cloct | |
▶Cloop_accelerationt | |
Cdisjunctive_polynomial_accelerationt | |
Cenumerating_loop_accelerationt | |
Cgoto_symex_statet::framet::loop_infot | |
Cfault_localizationt::lpointt | |
Cmain_function_resultt | |
▶Cstd::map< K, T > | STL class |
Ccfg_baset< T, P, I >::entry_mapt | |
Cvalue_set_fit::object_map_dt | |
Cvalue_sett::object_map_dt | |
Cboolbv_mapt::map_bitt | |
Cboolbv_mapt::map_entryt | |
Ccpp_typecheck_resolvet::matcht | |
Cmember_offset_iterator | |
▶Cjava_bytecode_parse_treet::membert | |
Cjava_bytecode_parse_treet::fieldt | |
Cjava_bytecode_parse_treet::methodt | |
Cboolbv_widtht::membert | |
Cinterpretert::memory_cellt | |
Cmerge_full_irept | |
Cmerge_irept | |
Cmerged_irep_hash | |
Cmerged_irepst | |
▶Cmessage_handlert | |
Cnull_message_handlert | |
▶Cstream_message_handlert | |
Ccerr_message_handlert | |
Ccout_message_handlert | |
▶Cui_message_handlert | |
Cconsole_message_handlert | |
Cgcc_message_handlert | |
▶Cmessaget | |
Cansi_c_convert_typet | |
▶Cbmc_all_propertiest | |
Cfault_localizationt | |
Cbmc_covert | |
Cbv_minimizet | |
Ccbmc_solverst | |
Ccharacter_refine_preprocesst | |
Ccover_goalst | Try to cover some given set of goals incrementally |
▶Cdecision_proceduret | |
▶Cprop_convt | |
▶Ccvc_convt | |
Ccvc_dect | |
▶Cdplib_convt | |
Cdplib_dect | |
▶Cprop_conv_solvert | TO_BE_DOCUMENTED |
▶Cequalityt | |
▶Carrayst | |
▶Cboolbvt | |
▶Cbv_pointerst | |
▶Cbv_cbmct | |
Ccbmc_dimacst | |
Cbv_minimizing_dect | |
▶Cbv_refinementt | |
Cstring_refinementt | |
Cprop_conv_storet | |
▶Csmt1_convt | |
Csmt1_dect | Decision procedure interface for various SMT 1.x solvers |
▶Csmt2_convt | |
Csmt2_dect | Decision procedure interface for various SMT 2.x solvers |
▶Cgoto_cc_modet | |
Carmcc_modet | |
Cas_modet | |
Ccw_modet | |
Cgcc_modet | |
Cms_cl_modet | |
▶Cgoto_convertt | |
Cgoto_convert_functionst | |
▶Cgoto_difft | |
Csyntactic_difft | |
Cgoto_inlinet | |
Cjar_filet | |
Cjar_poolt | |
Cjava_bytecode_convert_classt | |
Cjava_bytecode_convert_methodt | |
Cjava_class_loader_limitt | |
Cjava_class_loadert | |
Cjsil_convertt | |
Clanguage_filest | |
▶Clanguage_uit | |
Ccbmc_parse_optionst | |
Cclobber_parse_optionst | |
Ccompilet | |
Cgoto_analyzer_parse_optionst | |
▶Cgoto_diff_languagest | |
Cgoto_diff_parse_optionst | |
Cgoto_fence_inserter_parse_optionst | |
Cgoto_instrument_parse_optionst | |
Csymex_parse_optionst | |
▶Clanguaget | |
Cansi_c_languaget | |
Ccpp_languaget | |
Cjava_bytecode_languaget | |
Cjsil_languaget | |
▶Cparsert | |
Cansi_c_parsert | |
Cassembler_parsert | |
Ccpp_parsert | |
Cjava_bytecode_parsert | |
Cjsil_parsert | |
Cjson_parsert | |
Cmm_parsert | |
Cxml_parsert | |
▶Cpartial_order_concurrencyt | |
▶Cmemory_model_baset | |
▶Cmemory_model_sct | |
▶Cmemory_model_tsot | |
Cmemory_model_psot | |
Cpreprocessort | |
Cprop_minimizet | Computes a satisfying assignment of minimal cost according to a const function using incremental SAT |
Cproperty_checkert | |
▶Cpropt | TO_BE_DOCUMENTED |
▶Caig_prop_baset | |
▶Caig_prop_constraintt | |
Caig_prop_solvert | |
▶Ccnft | |
▶Ccnf_clause_listt | |
Ccnf_clause_list_assignmentt | |
▶Cdimacs_cnft | |
Cpbs_dimacs_cnft | |
▶Cqdimacs_cnft | |
Cqbf_quantort | |
Cqbf_qubet | |
Cqbf_skizzot | |
Cqbf_squolemt | |
▶Cqdimacs_coret | |
▶Cqbf_bdd_certificatet | |
Cqbf_bdd_coret | |
Cqbf_skizzo_coret | |
Cqbf_qube_coret | |
Cqbf_squolem_coret | |
Csatcheck_limmatt | |
Csatcheck_zcoret | |
▶Csatcheck_zchaff_baset | |
Csatcheck_zchafft | |
▶Ccnf_solvert | |
▶Csatcheck_booleforce_baset | |
Csatcheck_booleforce_coret | |
Csatcheck_booleforcet | |
Csatcheck_glucose_baset< T > | |
▶Csatcheck_glucose_baset< Glucose::SimpSolver > | |
Csatcheck_glucose_simplifiert | |
▶Csatcheck_glucose_baset< Glucose::Solver > | |
Csatcheck_glucose_no_simplifiert | |
Csatcheck_lingelingt | |
▶Csatcheck_minisat1_baset | |
▶Csatcheck_minisat1t | |
▶Csatcheck_minisat1_prooft | |
Csatcheck_minisat1_coret | |
Csatcheck_minisat2_baset< T > | |
▶Csatcheck_minisat2_baset< Minisat::SimpSolver > | |
Csatcheck_minisat_simplifiert | |
▶Csatcheck_minisat2_baset< Minisat::Solver > | |
Csatcheck_minisat_no_simplifiert | |
Csatcheck_picosatt | |
Csatcheck_precosatt | |
▶Csatcheck_smvsatt | |
Csatcheck_smvsat_coret | |
Csatcheck_smvsat_interpolatort | |
Cdimacs_cnf_dumpt | |
Ccvc_propt | |
Cdplib_propt | |
Cprop_wrappert | |
Csmt1_propt | |
Csmt2_propt | |
Cremove_const_function_pointerst | |
Cremove_function_pointerst | |
▶Csafety_checkert | |
Cbmct | |
Cpath_searcht | |
Cstatic_analyzert | |
Cstring_abstractiont | |
Cstring_instrumentationt | |
Csymex_bmct | |
Ctaint_analysist | |
▶Ctypecheckt | |
▶Cc_typecheck_baset | |
Cansi_c_typecheckt | |
Ccpp_typecheckt | |
Cjava_bytecode_typecheckt | |
Cjsil_typecheckt | |
Clinkingt | |
Czero_initializert | |
Ccpp_typecheckt::method_bodyt | |
Cmini_bdd_applyt | |
Cmini_bdd_mgrt | |
Cmini_bdd_nodet | |
Cmini_bddt | |
Cmip_vart | |
Cmm2cppt | |
Cmonomialt | |
▶Cstd::multimap< K, T > | STL class |
Cguarded_range_domaint | |
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 |
Cc_typecheck_baset | |
Cmulti_namespacet | |
Cnatural_loops_templatet< P, T > | |
▶Cnatural_loops_templatet< const goto_programt, goto_programt::const_targett > | |
Cnatural_loopst | |
Cnatural_loops_templatet< goto_programt, goto_programt::targett > | |
Cnew_scopet | |
Cunsigned_union_find::nodet | |
Ccfg_dominators_templatet< P, T, post_dom >::nodet | |
Clocal_cfgt::nodet | |
Cobject_idt | |
Cvalue_set_fivrt::object_map_dt | |
Cvalue_set_fivrnst::object_map_dt | |
Cprop_minimizet::objectivet | |
Cvalue_sett::objectt | |
Cvalue_set_fivrnst::objectt | |
Cvalue_set_fit::objectt | |
Cvalue_set_fivrt::objectt | |
▶Ccover_goalst::observert | |
Cbmc_all_propertiest | |
Cbmc_covert | |
Coperator_entryt | |
Coptionst | |
Ccmdlinet::optiont | |
Cosx_fat_readert | |
Coverflow_instrumentert | |
Cparameter_assignmentst | |
▶Cparse_options_baset | |
Ccbmc_parse_optionst | |
Cclobber_parse_optionst | |
Cgoto_analyzer_parse_optionst | |
Cgoto_diff_parse_optionst | |
Cgoto_fence_inserter_parse_optionst | |
Cgoto_instrument_parse_optionst | |
Cmmcc_parse_optionst | |
Csymex_parse_optionst | |
CParser | |
▶Cpath_accelerationt | |
Cpolynomial_acceleratort | |
Cpath_acceleratort | |
▶Cpath_enumeratort | |
Call_paths_enumeratort | |
Csat_path_enumeratort | |
Cpath_nodet | |
Cpath_replayt | |
Cpath_symex_historyt | |
Cpath_symex_statet | |
Cpath_symex_step_reft | |
Cpath_symex_stept | |
Cpath_symext | |
Cpatternt | |
Cpointer_arithmetict | |
Cirep_hash_container_baset::pointer_hasht | |
Cpointer_logict | |
Cpointer_logict::pointert | |
Cpoints_tot | |
Cpolynomial_acceleratort::polynomial_array_assignment | |
Cacceleration_utilst::polynomial_array_assignmentt | |
Cpolynomialt | |
Cjava_bytecode_parsert::pool_entryt | |
Cpostconditiont | |
Cbv_pointerst::postponedt | |
Cpreconditiont | |
Cprintf_formattert | |
▶CProofTraverser | |
Cminisat_prooft | |
▶Cprop_assignmentt | TO_BE_DOCUMENTED |
Cpropt | TO_BE_DOCUMENTED |
Cgoto_symex_statet::propagationt | |
Cpath_searcht::property_entryt | |
Cproperty_checkert::property_statust | |
Cboolbvt::quantifiert | |
Cqdimacs_cnft::quantifiert | |
▶Crange_domain_baset | |
Cguarded_range_domaint | |
Crange_domaint | |
Crationalt | |
Creachability_slicert | |
Creaching_definitiont | |
Crecursion_countert | |
Cref_expr_set_dt | |
Creference_counting< T > | |
Creference_counting< object_map_dt > | |
▶Creference_counting< ref_expr_set_dt > | |
Cref_expr_sett | |
Cremove_asmt | |
Cremove_exceptionst | |
Cremove_instanceoft | |
Cremove_returnst | |
Cremove_static_init_loopst | |
Cremove_virtual_functionst | |
Crename_symbolt | |
▶Cgoto_symex_statet::renaming_levelt | |
Cgoto_symex_statet::level0t | |
Cgoto_symex_statet::level1t | |
Cgoto_symex_statet::level2t | |
▶Creplace_symbolt | |
Creplace_symbol_extt | |
Cresolution_prooft< T > | |
Cresolution_prooft< clauset > | |
Crestrictt | |
Cmini_bdd_mgrt::reverse_keyt | |
Cfloat_bvt::rounding_mode_bitst | |
Cfloat_utilst::rounding_mode_bitst | |
Ctaint_parse_treet::rulet | |
▶Crw_range_sett | |
▶Crw_range_set_value_sett | |
Crw_guarded_range_set_value_sett | |
▶Crw_set_baset | |
▶C_rw_set_loct | |
Crw_set_loct | |
Crw_set_with_trackt | |
Crw_set_functiont | |
Csafe_pointer< T > | |
Csafe_pointer< ci_lazy_methodst > | |
Csaj_tablet | Produce canonical ordering for associative and commutative binary operators |
Csave_scopet | |
▶Cstd::set< K > | STL class |
Cconst_function_pointer_propagationt::arg_stackt | |
Cdata_dpt | |
Cshared_bufferst | |
Cconcurrency_instrumentationt::shared_vart | |
Csharing_mapt< keyT, valueT, hashT, predT > | |
Csharing_nodet< keyT, valueT, predT, no_sharing > | |
Csharing_nodet< key_type, mapped_type, key_equal > | |
Cshow_goto_functions_jsont | |
Cshow_goto_functions_xmlt | |
▶Csimple_insertiont | |
▶Cfence_all_sharedt | |
Cfence_all_shared_aegt | |
Cfence_volatilet | |
Csimplify_exprt | |
Creachability_slicert::slicer_entryt | |
▶Cslicing_criteriont | |
Cassert_criteriont | |
Cproperties_criteriont | |
▶Csmt1_temp_filet | |
Csmt1_dect | Decision procedure interface for various SMT 1.x solvers |
▶Csmt2_parsert | |
Csmt2irept | |
▶Csmt2_stringstreamt | |
Csmt2_dect | Decision procedure interface for various SMT 2.x solvers |
Csmt2_temp_filet | |
Ccbmc_solverst::solvert | |
Csorted_vector< K, bNoDuplicates, Pr, A > | |
Csymex_targett::sourcet | |
Csparse_bitvector_analysist< V > | |
▶Csparse_bitvector_analysist< reaching_definitiont > | |
Creaching_definitions_analysist | |
Csymex_target_equationt::SSA_stept | |
Cinterpretert::stack_framet | |
Cjava_bytecode_parse_treet::methodt::stack_map_table_entryt | |
Ccheck_call_sequencet::state_hash | |
Ccheck_call_sequencet::statet | |
▶Cstatic_analysis_baset | |
▶Cstatic_analysist< T > | |
Cconcurrency_aware_static_analysist< T > | |
▶Cstatic_analysist< value_set_domaint > | |
Cvalue_set_analysist | |
Cclauset::stept | |
▶Cstreambuf | |
Cfiledescriptor_streambuft | |
Cstring_constraint_generatort | |
Cstring_containert | |
Cstring_hash | |
Cstring_ptr_hash | |
Cstring_ptrt | |
Csubsumed_patht | |
Csymbol_factoryt | |
Csymbol_tablet | The symbol table |
▶Csymbolt | Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet |
Cauxiliary_symbolt | Internally generated symbol table entryThis is a symbol generated as part of translation to or modification of the intermediate representation |
Cparameter_symbolt | Symbol table entry of function parameterThis is a symbol generated as part of type checking |
Ctype_symbolt | Symbol table entry describing a data typeThis is a symbol generated as part of type checking |
Csymex_coveraget | |
Csymex_slice_by_tracet | |
Csymex_slicet | |
▶Csymex_targett | |
Csymex_target_equationt | |
▶CT | |
Ccfg_base_nodet< T, I > | |
Creference_counting< T >::dt | |
Ctaint_parse_treet | |
Ctarget_to_loc_mapt | |
Cgoto_convertt::targetst | |
Cgrapht< N >::tarjant | |
Ctdefl_compressor | |
Ctdefl_output_buffer | |
Ctdefl_sym_freq | |
▶Ctemp_dirt | |
Ctemp_working_dirt | |
Ctemplate_mapt | |
Ctemporary_filet | |
Cmonomialt::termt | |
Cbmc_covert::testt | |
Cconcurrency_instrumentationt::thread_local_vart | |
Cpath_symex_statet::threadt | |
Cgoto_symex_statet::threadt | |
Cgoto_convertt::throw_targett | |
Ctimert | |
Ctinfl_decompressor_tag | |
Ctinfl_huff_table | |
Cto_be_merged_irep_hash | |
Ctrace_automatont | |
Ctvt | |
Cdump_ct::typedef_infot | |
Cequalityt::typestructt | |
Cxml_irep_convertt::ul_eq | |
Cxml_irep_convertt::ul_hash | |
Cunified_difft | |
Cuninitializedt | |
▶Cfloat_utilst::unpacked_floatt | |
Cfloat_utilst::biased_floatt | |
Cfloat_utilst::unbiased_floatt | |
▶Cfloat_bvt::unpacked_floatt | |
Cfloat_bvt::biased_floatt | |
Cfloat_bvt::unbiased_floatt | |
Cunsigned_union_find | |
Cgoto_unwindt::unwind_logt | |
Cvalue_set_fivrnst::object_map_dt::validity_ranget | |
Cvalue_set_fivrt::object_map_dt::validity_ranget | |
Cvalue_set_dereferencet | TO_BE_DOCUMENTED |
Cvalue_set_fit | |
Cvalue_set_fivrnst | |
Cvalue_set_fivrt | |
▶Cvalue_setst | |
Cvalue_set_analysis_fit | |
Cvalue_set_analysis_fivrnst | |
Cvalue_set_analysis_fivrt | |
Cvalue_set_analysist | |
Cvalue_sett | |
Cconstant_propagator_domaint::valuest | |
Cvalue_set_dereferencet::valuet | |
Csmt1_dect::valuet | |
Cvar_mapt::var_infot | |
Cvar_mapt | |
Cpath_symex_statet::var_statet | |
Cmini_bdd_mgrt::var_table_entryt | |
Cjava_bytecode_convert_methodt::variablet | |
Cshared_bufferst::varst | |
▶Cstd::vector< T > | STL class |
Cexpanding_vectort< T > | |
Cexpanding_vectort< flagst > | |
Cexpanding_vectort< path_searcht::loc_datat > | |
Cexpanding_vectort< variablest > | |
Chash_numbering< T, hash_fkt > | |
Chash_numbering< dstringt, dstring_hash > | |
Chash_numbering< exprt, irep_hash > | |
Chash_numbering< irep_idt, irep_id_hash > | |
Chash_numbering< packedt, vector_hasht > | |
Clispexprt | |
▶Cnumbering< T > | |
Cunion_find< T > | |
Cnumbering< dstringt > | |
▶Cnumbering< exprt > | |
Cunion_find< exprt > | |
▶Cnumbering< irep_idt > | |
Cunion_find< irep_idt > | |
Cirep_hash_container_baset::vector_hasht | |
Ccustom_bitvector_domaint::vectorst | |
Cjava_bytecode_parse_treet::methodt::verification_type_infot | |
Cconfigt::verilogt | |
Cw_guardst | |
Cxml_edget | |
Cxml_goto_function_convertt | |
Cxml_goto_program_convertt | |
▶Cxml_interfacet | |
Ccbmc_parse_optionst | |
Cxml_irep_convertt | |
Cxml_parse_treet | |
Cxml_symbol_convertt | |
Cxmlt | |
Cyy_buffer_state | |
Cyy_trans_info | |
Cyyalloc | |
CYYSTYPE | |