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 | |
►Cabstract_goto_modelt | Abstract interface to eager or lazy GOTO models |
Cgoto_modelt | |
Clazy_goto_modelt | A GOTO model that produces function bodies on demand |
Cwrapper_goto_modelt | Class providing the abstract GOTO model interface onto an unrelated symbol table and goto_functionst |
Cacceleratet | |
Cacceleration_utilst | |
Clinkingt::adjust_type_infot | |
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 |
►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 | This is a may analysis (i.e |
►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 | The interface offered by a domain, allows code to manipulate domains without knowing their exact type |
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 | Because the class is inherited from ai_domain_baset , its instance represents an element of a domain of the reaching definitions abstract interpretation analysis |
Cuninitialized_domaint | |
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 | |
Carray_poolt | Correspondance between arrays and pointers string representations |
Cautomatont | |
Clocal_safe_pointerst::base_type_comparet | Comparator that regards base_type_eq expressions as equal, and otherwise uses the natural (operator<) ordering on irept |
Cbase_type_eqt | |
►Cstd::basic_string< Char > | STL class |
►Cstd::string | STL class |
Clispsymbolt | |
Cbdd_exprt | TO_BE_DOCUMENTED |
Ccover_basic_blockst::block_infot | |
Cjava_bytecode_convert_methodt::block_tree_nodet | |
Cboolbv_mapt | |
Cboolbv_widtht | |
Cgoto_convertt::break_continue_targetst | |
Cgoto_convertt::break_switch_targetst | |
Cstring_dependenciest::builtin_function_nodet | A builtin function node contains a builtin function call |
Cbv_arithmetict | |
Cconfigt::bv_encodingt | |
Cbv_spect | |
Cbv_utilst | |
Cbytecode_infot | |
Cjava_bytecode_parsert::bytecodet | |
Cc_storage_spect | |
►Cc_typecastt | |
Ccpp_typecastt | |
Ccall_checkt< Base, T > | |
Ccall_grapht | A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection |
Ccheck_call_sequencet::call_stack_entryt | |
Ccall_validate_fullt< Base, T > | |
Ccall_validatet< Base, T > | |
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_methods_neededt | |
Cclass_hierarchyt | Non-graph-based representation of the class hierarchy |
Cmethod_bytecodet::class_method_and_bytecodet | Pair of class id and methodt |
Cjava_class_loader_baset::classpath_entryt | An entry in the classpath |
Cjava_bytecode_parse_treet::classt | |
Cclauset | |
Cescape_domaint::cleanupt | |
►Ccmdlinet | |
Cfree_form_cmdlinet | An implementation of cmdlinet to be used in tests |
►Cgoto_cc_cmdlinet | |
Carmcc_cmdlinet | |
Cas86_cmdlinet | |
Cas_cmdlinet | |
Cbcc_cmdlinet | |
Cgcc_cmdlinet | |
Cld_cmdlinet | |
Cms_cl_cmdlinet | |
Cms_link_cmdlinet | |
Ccode_contractst | |
Cmessaget::commandt | |
Cconcat_iteratort< first_iteratort, second_iteratort > | On increment, increments a first iterator and when the corresponding end iterator is reached, starts to increment a second one |
Cconcurrency_instrumentationt | |
Cgoto_checkt::conditiont | |
Ccone_of_influencet | |
►Cbv_refinementt::configt | |
►Cbv_refinementt::infot | |
Cstring_refinementt::infot | String_refinementt constructor arguments |
►Cstring_refinementt::configt | |
Cstring_refinementt::infot | String_refinementt constructor arguments |
Cconfigt | Globally accessible architectural configuration |
►Cconst_expr_visitort | |
Cfind_qvar_visitort | |
Csmall_mapt< T, Ind, Num >::const_iterator | Const iterator |
Cconst_target_hash | |
Csmall_mapt< T, Ind, Num >::const_value_iterator | Const value iterator |
Cconversion_dependenciest | This is structure is here to facilitate passing arguments to the conversion functions |
Cci_lazy_methodst::convert_method_resultt | |
Cjava_bytecode_convert_methodt::converted_instructiont | |
Ccopy_on_write_pointeet< Num > | A helper class to store use-counts of copy-on-write objects |
Ccopy_on_writet< T > | A utility class for writing types with copy-on-write behaviour (like irep) |
Ccounterexample_beautificationt | |
►Ccover_blocks_baset | |
Ccover_basic_blocks_javat | |
Ccover_basic_blockst | |
Ccover_configt | |
►Ccover_instrumenter_baset | Base class for goto program coverage instrumenters |
Ccover_assertion_instrumentert | Assertion coverage instrumenter |
Ccover_branch_instrumentert | Branch coverage instrumenter |
Ccover_condition_instrumentert | Condition coverage instrumenter |
Ccover_cover_instrumentert | __CPROVER_cover coverage instrumenter |
Ccover_decision_instrumentert | Decision coverage instrumenter |
Ccover_location_instrumentert | Basic block coverage instrumenter |
Ccover_mcdc_instrumentert | MC/DC coverage instrumenter |
Ccover_path_instrumentert | Path coverage instrumenter |
Ccover_instrumenterst | A collection of instrumenters to be run |
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_exception_baset | Base class for exceptions thrown in the cprover project |
Canalysis_exceptiont | Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an error) |
Cdeserialization_exceptiont | Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes |
Cincorrect_goto_program_exceptiont | Thrown when a goto program that's being processed is in an invalid format, for example passing the wrong number of arguments to functions |
Cincorrect_source_program_exceptiont | |
Cinvalid_command_line_argument_exceptiont | Thrown when users pass incorrect command line arguments, for example passing no files to analysis or setting two mutually exclusive flags |
Cinvalid_source_file_exceptiont | Thrown when we can't handle something in an input source file |
Csmt2_tokenizert::smt2_errort | |
Csystem_exceptiont | Thrown when some external system fails unexpectedly |
Cunsupported_operation_exceptiont | Thrown when we encounter an instruction, parameters to an instruction etc |
Cuser_input_error_exceptiont | |
Ccprover_library_entryt | |
Cevent_grapht::critical_cyclet | |
Cdata | |
Cdata_dpt | |
Cdatat | |
Cevent_grapht::critical_cyclet::delayt | |
Csharing_mapt< keyT, valueT, hashT, equalT >::delta_view_itemt | |
Cdep_edget | |
Cdepth_iterator_baset< depth_iterator_t > | Depth first search iterator base - iterates over supplied expression and all its operands recursively |
►Cdepth_iterator_baset< const_depth_iteratort > | |
Cconst_depth_iteratort | |
►Cdepth_iterator_baset< const_unique_depth_iteratort > | |
Cconst_unique_depth_iteratort | |
►Cdepth_iterator_baset< depth_iteratort > | |
Cdepth_iteratort | |
Cdepth_iterator_expr_statet | Helper class for depth_iterator_baset |
►Cdereference_callbackt | Base class for pointer value set analysis |
Cgoto_program_dereferencet | Wrapper for functions removing dereferences in expressions contained in a goto program |
Csymex_dereference_statet | |
Cdereferencet | Wrapper for a function which dereference a pointer-expression |
Cdesignatort | |
Cdiagnostics_helpert< T > | Helper to give us some diagnostic in a usable form on assertion failure |
Cdiagnostics_helpert< char * > | |
Cdiagnostics_helpert< char[N]> | |
Cdiagnostics_helpert< dstringt > | |
Cdiagnostics_helpert< irep_pretty_diagnosticst > | |
Cdiagnostics_helpert< source_locationt > | |
Cdiagnostics_helpert< std::string > | |
Cdirtyt | |
Cdisjunctive_polynomial_accelerationt | |
Cdispatch_table_entryt | |
Cdocument_propertiest::doc_claimt | |
Cdocument_propertiest | |
Cdoes_remove_constt | |
►Cdomain_baset | |
Cvalue_set_domain_templatet< VST > | |
Cdott | |
Cdstring_hash | |
Cdstringt | dstringt has one field, an unsigned integer no which is an index into a static table of strings |
Cirept::dt | |
Cdump_ct | |
Ccall_grapht::edge_with_callsitest | Edge of the directed graph representation of this call graph |
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 |
Cbv_endianness_mapt | Map bytes according to the configured endianness |
Ccfg_baset< T, P, I >::entry_mapt | |
Cvalue_sett::entryt | Represents a row of a value_sett |
Cvalue_set_fit::entryt | |
Cvalue_set_fivrt::entryt | |
Cvalue_set_fivrnst::entryt | |
Cboolbv_widtht::entryt | |
Cinv_object_storet::entryt | |
Crw_set_baset::entryt | |
Cclass_hierarchyt::entryt | |
Cdesignatort::entryt | |
Cenumerating_loop_accelerationt | |
Cprintf_formattert::eol_exceptiont | |
Cmessaget::eomt | |
Cequation_symbol_mappingt | Maps equation to expressions contained in them and conversely expressions to equations that contain them |
Cevent_grapht | |
►Cstd::exception | STL class |
Crequire_goto_statements::no_decl_found_exceptiont | |
►Cstd::logic_error | STL class |
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 |
Cunsupported_java_class_signature_exceptiont | An exception that is raised for unsupported class signature |
►Cstd::runtime_error | STL class |
Cbitvector_conversion_exceptiont | |
Cequation_conversion_exceptiont | |
►Cflatten_byte_extract_exceptiont | |
Cnon_byte_alignedt | |
Cnon_const_array_sizet | |
Cnon_const_byte_extraction_sizet | |
Cnon_constant_widtht | |
Cgenerate_function_bodies_errort | |
Cjava_bytecode_parse_treet::methodt::exceptiont | |
Cexpanding_vectort< T > | |
Cexpanding_vectort< variablest > | |
Crequire_parse_tree::expected_instructiont | |
Crequire_type::expected_type_argumentt | |
Cexpr2c_configurationt | Used for configuring the behaviour of expr2c and type2c |
►Cexpr2ct | |
Cexpr2cppt | |
Cexpr2javat | |
Cexpr2jsilt | |
Cdetail::expr_dynamic_cast_return_typet< Ret, T > | |
Cexpr_initializert< nondet > | |
Cdetail::expr_try_dynamic_cast_return_typet< Ret, T > | |
►Cexpr_visitort | |
Csmt2_convt::let_visitort | |
►Cfalse_type | |
Cdetail::always_falset< T > | |
Cfile | |
Cfilter_iteratort< iteratort > | Iterator which only stops at elements for which some given function f is true |
Cfixed_keys_map_wrappert< mapt > | |
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_containert< T > | The below enables convenient syntax for feeding objects into streams, via stream << format(o) |
Cformat_elementt | |
Cformat_specifiert | |
►Cformat_spect | |
Cformat_constantt | |
Cformat_textt | |
Cformat_tokent | |
Cgoto_symex_statet::framet | |
Cfreert | A functor wrapping std::free |
Cfull_slicert | |
Cinterpretert::function_assignments_contextt | |
Cinterpretert::function_assignmentt | |
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 |
Cfunctionst::function_infot | |
Cfunction_modifiest | |
Cfunctionst | |
Cgcc_versiont | |
►Cgenerate_function_bodiest | Base class for replace_function_body implementations |
Cassert_false_generate_function_bodiest | |
Cassert_false_then_assume_false_generate_function_bodiest | |
Cassume_false_generate_function_bodiest | |
Chavoc_generate_function_bodiest | |
Cgeneric_parameter_specialization_map_keyst | |
Cgoal_filterst | A collection of goal filters to be applied in conjunction |
Ccover_goalst::goalt | |
Cbmc_all_propertiest::goalt | |
Cbmc_covert::goalt | |
Cgoto_checkt | |
►Cgoto_difft | |
Cjava_syntactic_difft | |
Csyntactic_difft | |
Cgoto_functionst | A collection of goto functions |
Cgoto_functiont | A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers) |
Cgoto_inlinet::goto_inline_logt::goto_inline_log_infot | |
Cgoto_inlinet::goto_inline_logt | |
Cgoto_model_functiont | Interface providing access to a single function in a GOTO model, plus its associated symbol table |
Cgoto_null_checkt | Return structure for get_null_checked_expr and get_conditional_checked_expr |
Cgoto_program2codet | |
►Cgoto_programt | A generic container class for the GOTO intermediate representation of one function |
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< edge_with_callsitest > | |
Ccall_grapht::function_nodet | Node of the directed graph representation of this call graph |
►Cgraph_nodet< empty_edget > | |
Cabstract_eventt | |
Ccfg_base_nodet< T, I > | |
Cclass_hierarchy_graph_nodet | Class hierarchy graph node: simply contains a class identifier |
►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, java_bytecode_convert_methodt::method_offsett > > | |
Cprocedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett > | |
►Cgrapht< class_hierarchy_graph_nodet > | |
Cclass_hierarchy_grapht | Class hierarchy, represented using grapht and therefore suitable for use with generic graph algorithms |
►Cgrapht< dep_nodet > | |
Cdependence_grapht | |
►Cgrapht< function_nodet > | |
Ccall_grapht::directed_grapht | Directed graph representation of this call graph |
►Cgrapht< xml_graph_nodet > | |
Cgraphmlt | |
Cstd::hash< dstringt > | Default hash function of dstringt for use with STL containers |
Cstd::hash< string_not_contains_constraintt > | |
Chavoc_loopst | |
Cjava_bytecode_convert_methodt::holet | |
Csmt2_convt::identifiert | |
Cidentifiert | |
Csmt2_parsert::idt | |
Cieee_float_spect | |
Cieee_floatt | |
Cincremental_dirtyt | Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly once |
Cindex_set_pairt | |
Cindicator_maskt< T, B, U > | |
Cindicator_maskt< T, B, std::integral_constant< T, 0 > > | |
Cinfix_opt | |
Cinflate_state | |
Cresolve_inherited_componentt::inherited_componentt | |
Cinode | |
Cbmc_covert::goalt::instancet | |
Ccpp_typecheckt::instantiation_levelt | |
Ccpp_typecheckt::instantiationt | |
Cjava_bytecode_parse_treet::instructiont | |
Cgoto_programt::instructiont | This class represents an instruction in the GOTO intermediate representation |
►Cinstrumentert | |
Cinstrumenter_pensievet | |
Cinterval_templatet< T > | |
Cinv_object_storet | |
►Cinvariant_failedt | A logic error, augmented with a distinguished field to hold a backtrace |
Cbad_cast_exceptiont | |
Cinvariant_with_diagnostics_failedt | A class that includes diagnostic information related to an invariant violation |
Cnullptr_exceptiont | |
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 |
Cmessaget::mstreamt | |
Cirep_hash_container_baset::irep_entryt | |
Cirep_full_eq | |
Cirep_full_hash | |
Cirep_hash | |
►Cirep_hash_container_baset | |
Cirep_full_hash_containert | |
Cirep_hash_containert | |
Cirep_hash_mapt< Key, T > | |
Cirep_pretty_diagnosticst | |
Cirep_serializationt | |
Cirep_serializationt::ireps_containert | |
►Cirept | Base class for tree-like data structures with sharing |
Cc_enum_typet::c_enum_membert | |
Ccode_push_catcht::exception_list_entryt | |
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 | |
Carray_string_exprt | |
►Cbinary_exprt | A base class for binary expressions |
►Cbinary_predicate_exprt | A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two arguments |
►Cbinary_relation_exprt | A base class for relations, i.e., binary predicates |
Cequal_exprt | Equality |
Cieee_float_equal_exprt | IEEE-floating-point equality |
Cieee_float_notequal_exprt | IEEE floating-point disequality |
Cnotequal_exprt | Disequality |
Cextractbit_exprt | Extracts a single bit of a bit-vector operand |
►Cquantifier_exprt | A base class for quantifier expressions |
Cexists_exprt | An exists expression |
Cforall_exprt | A forall expression |
Cbyte_extract_exprt | TO_BE_DOCUMENTED |
Ccomplex_exprt | Complex constructor from a pair of numbers |
Cdiv_exprt | Division |
Cdynamic_object_exprt | Representation of heap-allocated objects |
Cfactorial_power_exprt | Falling factorial power |
Cfloatbv_typecast_exprt | Semantic type conversion from/to floating-point formats |
Cfunction_application_exprt | Application of (mathematical) function |
Cimplies_exprt | Boolean implication |
Cindex_exprt | Array index operator |
Cminus_exprt | Binary minus |
Cmod_exprt | Modulo |
Cobject_descriptor_exprt | Split an expression into a base object and a (byte) offset |
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 |
Ccode_typet::parametert | |
►Ccodet | Data structure for representing an arbitrary statement in a program |
Ccode_asmt | codet representation of an inline assembler statement |
Ccode_assertt | A non-fatal assertion, which checks a condition then permits execution to continue |
Ccode_assignt | A codet representing an assignment in the program |
Ccode_assumet | An assumption, which must hold in subsequent code |
Ccode_blockt | A codet representing sequential composition of program statements |
Ccode_breakt | codet representation of a break statement (within a for or while loop) |
Ccode_continuet | codet representation of a continue statement (within a for or while loop) |
Ccode_deadt | A codet representing the removal of a local variable going out of scope |
Ccode_declt | A codet representing the declaration of a local variable |
Ccode_dowhilet | codet representation of a do while statement |
Ccode_expressiont | codet representation of an expression statement |
Ccode_fort | codet representation of a for statement |
Ccode_function_callt | codet representation of a function call statement |
Ccode_gotot | codet representation of a goto statement |
Ccode_ifthenelset | codet representation of an if-then-else statement |
Ccode_labelt | codet representation of a label for branch targets |
Ccode_landingpadt | A statement that catches an exception, assigning the exception in flight to an expression (e.g |
Ccode_pop_catcht | Pops an exception handler from the stack of active handlers (i.e |
Ccode_push_catcht | Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 .. |
Ccode_returnt | codet representation of a "return from a function" statement |
Ccode_skipt | A codet representing a skip statement |
Ccode_switch_caset | codet representation of a switch-case, i.e. a case statement within a switch |
Ccode_switcht | codet representing a switch statement |
Ccode_try_catcht | codet representation of a try/catch block |
Ccode_whilet | codet representing a while statement |
►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 | |
Cextractbits_exprt | Extracts a sub-range of a bit-vector operand |
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 |
Cguardt | |
Cieee_float_op_exprt | IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2) |
Cindex_designatort | |
Cjsil_declarationt | |
Cmember_designatort | |
►Cmulti_ary_exprt | A base class for multi-ary expressions Associativity is not specified |
Cand_exprt | Boolean AND |
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 |
Cbitand_exprt | Bit-wise AND |
Cbitor_exprt | Bit-wise OR |
Cbitxor_exprt | Bit-wise XOR |
Cconcatenation_exprt | Concatenation of bit-vector operands |
Ccond_exprt | This is a parametric version of an if-expression: it returns the value of the first case (using the ordering of the operands) whose condition evaluates to true |
Cmult_exprt | Binary multiplication Associativity is not specified |
Cor_exprt | Boolean OR |
Cplus_exprt | The plus expression Associativity is not specified |
►Cstruct_exprt | Struct constructor from list of elements |
Crefined_string_exprt | |
Cvector_exprt | Vector constructor from list of elements |
Cxor_exprt | Boolean XOR |
►Cnullary_exprt | An expression without operands |
Cansi_c_declaratort | |
Cinfinity_exprt | An expression denoting infinity |
Cnil_exprt | The NIL expression |
Cnondet_symbol_exprt | Expression to hold a nondeterministic choice |
Csmt2_convt::smt2_symbolt | |
Cstring_constantt | |
►Csymbol_exprt | Expression to hold a symbol (variable) |
Cdecorated_symbol_exprt | Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_local |
Cssa_exprt | Expression providing an SSA-renamed symbol of expressions |
Ctype_exprt | An expression denoting a type |
►Cpredicate_exprt | A 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_function_callt | A side_effect_exprt representation of a function call side effect |
Cside_effect_expr_nondett | A side_effect_exprt that returns a non-deterministically chosen value |
Cside_effect_expr_throwt | A side_effect_exprt representation of a side effect that throws an exception |
Cstruct_typet::baset | Base class or struct that a class or struct inherits from |
Cstruct_union_typet::componentt | |
Ctemplate_parametert | |
►Cternary_exprt | An expression with three operands |
Cbyte_update_exprt | TO_BE_DOCUMENTED |
Cif_exprt | The trinary if-then-else operator |
Clet_exprt | A let expression |
Ctranst | Transition system, consisting of state invariant, initial state predicate, and transition predicate |
Cupdate_exprt | Operator to update elements in structs and arrays |
►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 |
Cbswap_exprt | The byte swap expression |
Ccomplex_imag_exprt | Imaginary part of the expression describing a complex number |
Ccomplex_real_exprt | Real part of the expression describing a complex number |
Cdereference_exprt | Operator to dereference a pointer |
Cmember_exprt | Extract member of struct or union |
Cnot_exprt | Boolean negation |
Cpopcount_exprt | The popcount (counting the number of bits set to 1) expression |
Ctypecast_exprt | Semantic type conversion |
Cunary_minus_exprt | The unary minus expression |
Cunary_plus_exprt | The unary plus expression |
►Cunary_predicate_exprt | A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argument |
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 Predicate is true if _op is negative, false otherwise |
Cunion_exprt | Union constructor from single element |
Cwith_exprt | Operator to update elements in structs and arrays |
Cjava_annotationt | |
Cjava_annotationt::valuet | |
Cmerged_irept | |
Csource_locationt | |
Cto_be_merged_irept | |
►Ctypet | The type of an expression, extends irept |
Cannotated_typet | |
►Cbitvector_typet | Base class of fixed-width bit-vector types |
Cbv_typet | Fixed-width bit-vector without numerical interpretation |
Cc_bit_field_typet | Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they have a subtype) |
Cc_bool_typet | The C/C++ Booleans |
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 These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they have a subtype) |
►Creference_typet | The reference type |
Cjava_generic_parametert | Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T> |
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) |
Csignedbv_typet | Fixed-width bit-vector with two's complement interpretation |
Cunsignedbv_typet | Fixed-width bit-vector with unsigned binary interpretation |
Cbool_typet | The Boolean type |
►Ccode_typet | Base type of functions |
Cjava_method_typet | |
Cjsil_builtin_code_typet | |
Cjsil_spec_code_typet | |
Ccpp_enum_typet | |
►Cempty_typet | The empty type |
Cvoid_typet | The void type, the same as empty_typet |
Cenumeration_typet | An enumeration type, i.e., a type with elements (not to be confused with C enums) |
Cinteger_typet | Unbounded, signed integers (mathematical integers, not bitvectors) |
Cnatural_typet | Natural numbers including zero (mathematical integers, not bitvectors) |
Cnil_typet | The NIL type, i.e., an invalid type, no value |
Crange_typet | A type for subranges of integers |
Crational_typet | Unbounded, signed rational numbers |
Creal_typet | Unbounded, signed real numbers |
Cstring_typet | String type |
►Cstruct_union_typet | Base type for structs and unions |
►Cstruct_typet | Structure type, corresponds to C style structs |
►Cclass_typet | Class type |
►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_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 |
Crefined_string_typet | |
►Cunion_typet | The union type |
Cjsil_union_typet | |
Csymbol_typet | A reference into the symbol table |
►Ctag_typet | A tag-based type, i.e., typet with an identifier |
Cc_enum_tag_typet | C enum tag type, i.e., c_enum_typet with an identifier |
►Cstruct_tag_typet | A struct tag type, i.e., struct_typet with an identifier |
Cjava_generic_struct_tag_typet | Type for a generic symbol, extends struct_tag_typet with a vector of java generic types |
Cunion_tag_typet | A union tag type, i.e., union_typet with an identifier |
Ctemplate_typet | |
►Ctype_with_subtypest | Type with multiple subtypes |
Cmathematical_function_typet | A type for mathematical functions (do not confuse with functions/methods in code) |
Cmerged_typet | Holds a combination of types |
►Ctype_with_subtypet | Type with a single subtype |
Carray_typet | Arrays with given size |
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 | The vector type |
Ctypedef_typet | A typedef |
►Cis_constantt | Determine whether an expression is constant |
Cgoto_symex_is_constantt | |
Cis_predecessor_oft | |
Cis_threadedt | |
Csymbol_table_baset::iteratort | |
Cjar_filet | Class representing a .jar archive |
Cjar_poolt | A chache for jar_filet objects, by file name |
Cjava_bytecode_parse_treet | |
Cjava_object_factoryt | |
Cjava_simple_method_stubst | |
Cconfigt::javat | |
Cjsil_parse_treet | |
Cjson_irept | |
►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_stream_arrayt | Provides methods for streaming JSON arrays |
Cjson_stream_objectt | Provides methods for streaming JSON objects |
►Cjsont | |
Cjson_arrayt | |
Cjson_falset | |
Cjson_nullt | |
Cjson_numbert | |
Cjson_objectt | |
Cjson_stringt | |
Cjson_truet | |
Ck_inductiont | |
Cjava_bytecode_parse_treet::classt::lambda_method_handlet | |
Clanguage_entryt | |
Clanguage_filet | |
Clanguage_modulet | |
Carrayst::lazy_constraintt | |
Clazy_goto_functions_mapt | Provides a wrapper for a map of lazily loaded goto_functiont |
Cgoto_convertt::leave_targett | |
Csmt2_convt::let_count_idt | |
Cdocument_propertiest::linet | |
Cliteralt | |
Clocal_may_aliast::loc_infot | |
Clocal_bitvector_analysist | |
Clocal_cfgt | |
Clocal_may_alias_factoryt | |
Clocal_may_aliast | |
Clocal_safe_pointerst | A very simple, cheap analysis to determine when dereference operations are trivially guarded by a check against a null pointer access |
Cjava_bytecode_convert_methodt::local_variable_with_holest | |
Cjava_bytecode_parse_treet::methodt::local_variablet | |
Clocalst | |
Cgoto_symex_statet::framet::loop_infot | |
Cfault_localizationt::lpointt | |
Cmain_function_resultt | |
Cboolbv_mapt::map_bitt | |
Cboolbv_mapt::map_entryt | |
Cmap_iteratort< iteratort, outputt > | Iterator which applies some given function f after each increment and returns its result on dereference |
Ccpp_typecheck_resolvet::matcht | |
►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 | |
►Cconsole_message_handlert | |
Cgcc_message_handlert | |
Cnull_message_handlert | |
Csmt2_message_handlert | |
►Cstream_message_handlert | |
Ccerr_message_handlert | |
Ccout_message_handlert | |
Cui_message_handlert | |
►Cmessaget | Class that provides messages with a built-in verbosity 'level' |
Cansi_c_convert_typet | |
►Cbmc_all_propertiest | |
Cfault_localizationt | |
Cbmc_covert | |
Cbv_minimizet | |
Ccbmc_parse_optionst | |
Ccharacter_refine_preprocesst | |
Cci_lazy_methodst | |
Ccompilet | |
Ccover_goalst | Try to cover some given set of goals incrementally |
►Cdecision_proceduret | |
►Cprop_convt | |
►Cprop_conv_solvert | TO_BE_DOCUMENTED |
►Cequalityt | |
►Carrayst | |
►Cboolbvt | |
►Cbv_pointerst | |
Cbv_dimacst | |
Cbv_minimizing_dect | |
►Cbv_refinementt | |
Cstring_refinementt | |
►Csmt2_convt | |
Csmt2_dect | Decision procedure interface for various SMT 2.x solvers |
►Cfunction_filter_baset | Base class for filtering functions |
Cinclude_pattern_filtert | Filters functions that match the provided pattern |
Cinternal_functions_filtert | Filters out CPROVER internal functions |
Ctrivial_functions_filtert | Filters out trivial functions |
►Cgoal_filter_baset | Base class for filtering goals |
Cinternal_goals_filtert | Filters out goals with source locations considered internal |
Cgoto_analyzer_parse_optionst | |
►Cgoto_cc_modet | |
Carmcc_modet | |
Cas_modet | |
Ccw_modet | |
Cgcc_modet | |
Cld_modet | |
Cms_cl_modet | |
Cms_link_modet | |
►Cgoto_convertt | |
Cgoto_convert_functionst | |
Cgoto_inlinet | |
Cgoto_instrument_parse_optionst | |
Chavoc_generate_function_bodiest | |
Cinterpretert | |
Cjanalyzer_parse_optionst | |
Cjava_bytecode_convert_classt | |
Cjava_bytecode_convert_methodt | |
Cjava_bytecode_instrumentt | |
►Cjava_class_loader_baset | Base class for maintaining classpath |
Cjava_class_loadert | Class responsible to load .class files |
Cjava_class_loader_limitt | Class representing a filter for class file loading |
Cjava_string_library_preprocesst | |
Cjbmc_parse_optionst | |
Cjsil_convertt | |
Clanguage_filest | |
►Clanguage_uit | |
►Cgoto_diff_languagest | |
Cgoto_diff_parse_optionst | |
►Cjdiff_languagest | |
Cjdiff_parse_optionst | |
►Clanguaget | |
Cansi_c_languaget | |
Ccpp_languaget | |
Cjava_bytecode_languaget | |
Cjsil_languaget | |
Cjson_symtab_languaget | |
Clinker_script_merget | Synthesise definitions of symbols that are defined in linker scripts |
►Cparsert | |
Cansi_c_parsert | |
Cassembler_parsert | |
Ccpp_parsert | |
Cjava_bytecode_parsert | |
Cjsil_parsert | |
Cjson_parsert | |
►Csmt2_tokenizert | |
►Csmt2_parsert | |
Csmt2_solvert | |
Csmt2irept | |
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 |
►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_zcoret | |
►Csatcheck_zchaff_baset | |
Csatcheck_zchafft | |
►Ccnf_solvert | |
►Csatcheck_booleforce_baset | |
Csatcheck_booleforce_coret | |
Csatcheck_booleforcet | |
Csatcheck_cadicalt | |
Csatcheck_glucose_baset< T > | |
►Csatcheck_glucose_baset< Glucose::SimpSolver > | |
Csatcheck_glucose_simplifiert | |
►Csatcheck_glucose_baset< Glucose::Solver > | |
Csatcheck_glucose_no_simplifiert | |
Csatcheck_ipasirt | Interface for generic SAT solver interface IPASIR |
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 | |
Cdimacs_cnf_dumpt | |
Crebuild_goto_start_function_baset< maybe_lazy_goto_modelt > | |
Cremove_const_function_pointerst | |
Cremove_java_newt | |
►Csafety_checkert | |
►Cbmct | Bounded model checking or path exploration for goto-programs |
Cpath_explorert | Symbolic execution from a saved branch point |
Cstring_abstractiont | |
Cstring_instrumentationt | |
Ctaint_analysist | |
►Ctypecheckt | |
►Cc_typecheck_baset | |
Cansi_c_typecheckt | |
Ccpp_typecheckt | |
Cjava_bytecode_typecheckt | |
Cjsil_typecheckt | |
Clinkingt | |
Ccpp_typecheckt::method_bodyt | |
Cmethod_bytecodet | |
Cmini_bdd_applyt | |
Cmini_bdd_mgrt | |
Cmini_bdd_nodet | |
Cmini_bddt | |
Cmonomialt | |
Cms_cl_versiont | |
Cmz_stream_s | |
►Cmz_zip_archive | |
Cmz_zip_archive_statet | |
Cmz_zip_archive_file_stat | |
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 | |
Csmt2_parsert::named_termt | |
►Cnamespace_baset | Basic interface for a namespace |
►Cnamespacet | A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in them |
Cc_typecheck_baset | |
Cmulti_namespacet | A multi namespace is essentially a namespace, with a list of namespaces |
Cnatural_loops_templatet< P, T > | Main driver for working out if a class (normally goto_programt) has any natural loops |
►Cnatural_loops_templatet< const goto_programt, goto_programt::const_targett > | |
Cnatural_loopst | A concretized version of natural_loops_templatet<const goto_programt, goto_programt::const_targett> |
Cnatural_loops_templatet< goto_programt, goto_programt::targett > | |
Cnew_scopet | |
Cstring_dependenciest::node_hash | Hash function for nodes |
Cunsigned_union_find::nodet | |
Ccfg_dominators_templatet< P, T, post_dom >::nodet | |
Cstring_dependenciest::nodet | |
Clocal_cfgt::nodet | |
Cnondet_instruction_infot | Holds information about any discovered nondet methods, with extreme type- safety |
Cnum_bitst< N > | |
Cnum_bitst< 0 > | |
Cnum_bitst< 1 > | |
Cnumeric_castt< Target, typename > | 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_factory_parameterst | |
Cc_object_factory_parameterst | |
Cjava_object_factory_parameterst | |
Cobject_idt | |
Cvalue_sett::object_map_dt | Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances) |
Cvalue_set_fivrt::object_map_dt | |
Cvalue_set_fivrnst::object_map_dt | |
Cvalue_set_fit::object_map_dt | |
Cprop_minimizet::objectivet | |
►Ccover_goalst::observert | |
Cbmc_all_propertiest | |
Cbmc_covert | |
Coperator_entryt | |
Coptionst | |
Ccmdlinet::optiont | |
Cosx_fat_readert | |
Coverflow_instrumentert | |
Cparameter_assignmentst | |
Cparse_floatt | |
►Cparse_options_baset | |
Ccbmc_parse_optionst | |
Cgoto_analyzer_parse_optionst | |
Cgoto_diff_parse_optionst | |
Cgoto_instrument_parse_optionst | |
Cjanalyzer_parse_optionst | |
Cjbmc_parse_optionst | |
Cjdiff_parse_optionst | |
CParser | |
Cpath_acceleratort | |
►Cpath_enumeratort | |
Call_paths_enumeratort | |
Csat_path_enumeratort | |
Cpath_nodet | |
►Cpath_storaget | Storage for symbolic execution paths to be resumed later |
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_strategy_choosert | Factory and information for path_storaget |
Cpath_storaget::patht | Information saved at a conditional goto to resume execution |
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 |
Cpointee_address_equalt | Functor to check whether iterators from different collections point at the same object |
Cpointer_arithmetict | |
Crequire_goto_statements::pointer_assignment_locationt | |
Cirep_hash_container_baset::pointer_hasht | |
Cpointer_logict | |
Cpointer_logict::pointert | |
Cpoints_tot | |
Cpolynomial_acceleratort | |
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 | |
Cproperty_checkert::property_statust | |
►Cqualifierst | |
►Cc_qualifierst | |
Cjava_qualifierst | |
Cqdimacs_cnft::quantifiert | |
Cboolbvt::quantifiert | |
►Crange_domain_baset | |
Cguarded_range_domaint | |
Crange_domaint | |
Cranget< iteratort > | A range is a pair of a begin and an end iterators |
Crationalt | |
Creachability_slicert | |
Creaching_definitiont | Identifies a GOTO instruction where a given variable is defined (i.e |
Crecursion_set_entryt | Recursion-set entry owner class |
Cref_expr_set_dt | |
Creference_counting< T > | |
Creference_counting< object_map_dt > | |
►Creference_counting< ref_expr_set_dt > | |
Cref_expr_sett | |
Cremove_asmt | |
Cremove_calls_no_bodyt | |
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_returnst | |
Cremove_virtual_functionst | |
Crename_symbolt | |
Creplace_callst | |
►Creplace_symbolt | Replace expression or type symbols by an expression or type, respectively |
Ccasting_replace_symbolt | |
►Cunchecked_replace_symbolt | |
Caddress_of_aware_replace_symbolt | Replace symbols with constants while maintaining syntactically valid expressions |
Creplacement_predicatet | Patterns of expressions that should be replaced |
Cresolution_prooft< T > | |
Cresolution_prooft< clauset > | |
Cresolve_inherited_componentt | |
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 | |
Csaj_tablet | Produce canonical ordering for associative and commutative binary operators |
Csave_scopet | |
Creachability_slicert::search_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 |
Cselect_pointer_typet | |
Caddress_of_aware_replace_symbolt::set_require_lvalue_and_backupt | |
Cshared_bufferst | |
Cconcurrency_instrumentationt::shared_vart | |
Csharing_mapt< keyT, valueT, hashT, equalT >::sharing_map_statst | Stats about sharing between several sharing map instances |
Csharing_mapt< keyT, valueT, hashT, equalT > | A map implemented as a tree where subtrees can be shared between different maps |
►Csharing_node_baset | |
Csharing_node_innert< keyT, valueT, equalT > | |
Csharing_node_innert< key_type, mapped_type > | |
Csharing_node_leaft< keyT, valueT, equalT > | |
Cshow_goto_functions_jsont | |
Cshow_goto_functions_xmlt | |
Csmt2_parsert::signature_with_parameter_idst | |
Csimplify_exprt | |
Creachability_slicert::slicer_entryt | |
►Cslicing_criteriont | |
Cassert_criteriont | |
Cin_function_criteriont | |
Cproperties_criteriont | |
Csmall_mapt< T, Ind, Num > | Map from small integers to values |
Csmall_mapt< innert > | |
Csmall_shared_pointeet< Num > | A helper class to store use-counts of objects held by small shared pointers |
►Csmall_shared_pointeet< unsigned > | |
Cd_leaft< keyT, valueT, equalT > | |
Csmall_shared_ptrt< T > | 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_ptrt< d_leaft< keyT, valueT, equalT > > | |
►Csmall_shared_two_way_pointeet< Num > | |
Cd_containert< keyT, valueT, equalT > | |
Cd_internalt< keyT, valueT, equalT > | |
Csmall_shared_two_way_ptrt< U, V > | This class is similar to small_shared_ptrt and boost's intrusive_ptr |
Csmall_shared_two_way_ptrt< d_internalt< key_type, mapped_type, equalT >, d_containert< key_type, mapped_type, equalT > > | |
Csmall_shared_two_way_ptrt< d_internalt< keyT, valueT, equalT >, d_containert< keyT, valueT, equalT > > | |
Csmt2_format_containert< T > | |
►Csmt2_stringstreamt | |
Csmt2_dect | Decision procedure interface for various SMT 2.x solvers |
Csolver_factoryt | |
Csolver_factoryt::solvert | |
Csymex_targett::sourcet | Identifies source in the context of symbolic execution |
►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 |
Cinterval_sparse_arrayt | Represents arrays by the indexes up to which the value remains the same |
Csparse_bitvector_analysist< V > | An instance of this class provides an assignment of unique numeric ID to each inserted reaching_definitiont instance |
►Csparse_bitvector_analysist< reaching_definitiont > | |
Creaching_definitions_analysist | |
Csparse_vectort< T > | |
Csparse_vectort< memory_cellt > | |
Csymex_target_equationt::SSA_stept | Single SSA step in the equation |
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< VSDT > | |
Cvalue_set_analysis_templatet< VSDT > | |
Cstatic_verifier_resultt | |
Cclauset::stept | |
Cstring_axiomst | |
►Cstring_builtin_functiont | Base class for string functions that are built in the solver |
Cstring_builtin_function_with_no_evalt | Functions that are not yet supported in this class but are supported by string_constraint_generatort |
►Cstring_creation_builtin_functiont | String creation from other types |
Cstring_of_int_builtin_functiont | String creation from integer types |
►Cstring_insertion_builtin_functiont | String inserting a string into another one |
Cstring_concatenation_builtin_functiont | |
Cstring_test_builtin_functiont | String test |
►Cstring_transformation_builtin_functiont | String builtin_function transforming one string into another |
Cstring_concat_char_builtin_functiont | Adding a character at the end of a string |
Cstring_set_char_builtin_functiont | Setting a character at a particular position of a string |
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_constraint_generatort | |
Cstring_constraintst | Collection of constraints of different types: existential formulas, universal formulas, and "not contains" (universal with one alternation) |
Cstring_constraintt | |
Cstring_containert | |
Cstring_dependenciest | Keep track of dependencies between strings |
Cstring_hash | |
Cstring_dependenciest::string_nodet | A string node points to builtin_function on which it depends |
Cstring_not_contains_constraintt | Constraints to encode non containement of strings |
Cstring_ptr_hash | |
Cstring_ptrt | |
►Cstructured_pool_entryt | |
Cbase_ref_infot | |
Cclass_infot | Corresponds to the CONSTANT_Class_info Structure Described in Java 8 specification 4.4.1 |
Cmethod_handle_infot | |
Cname_and_type_infot | Corresponds to the CONSTANT_NameAndType_info Structure Described in Java 8 specification 4.4.6 |
Cstub_global_initializer_factoryt | |
Csubsumed_patht | |
Csymbol_factoryt | |
Csymbol_generatort | Generation of fresh symbols of a given type |
►Csymbol_table_baset | The symbol table base class interface |
Cjournalling_symbol_tablet | A symbol table wrapper that records which entries have been updated/removed |
Csymbol_table_buildert | Author: Diffblue Ltd |
Csymbol_tablet | The symbol table |
►Csymbolt | Symbol table entry |
Cauxiliary_symbolt | Internally generated symbol table entry |
Cparameter_symbolt | Symbol table entry of function parameter |
Ctype_symbolt | Symbol table entry describing a data type |
Csymex_configt | Configuration of the symbolic execution |
Csymex_coveraget | |
Csymex_nondet_generatort | Functor generating fresh nondet symbols |
►Csymex_renaming_levelt | Wrapper for a current_names map, which maps each identifier to an SSA expression and a counter |
Csymex_level0t | Functor to set the level 0 renaming of SSA expressions |
Csymex_level1t | Functor to set the level 1 renaming of SSA expressions |
Csymex_level2t | Functor to set the level 2 renaming of SSA expressions |
Csymex_slice_by_tracet | |
Csymex_slicet | |
►Csymex_targett | The interface of the target container for symbolic execution to record its symbolic steps into |
Csymex_target_equationt | Inheriting the interface of symex_targett this class represents the SSA form of the input program as a list of SSA_stept |
Csystem_library_symbolst | |
►CT | |
Ccfg_base_nodet< T, I > | |
Creference_counting< T >::dt | |
Ctaint_parse_treet | |
Cgoto_convertt::targetst | |
Cgrapht< N >::tarjant | |
Ctdefl_compressor | |
Ctdefl_output_buffer | |
Ctdefl_sym_freq | |
Ctemp_dirt | |
Ctemplate_mapt | |
Ctemplate_numberingt< Map > | |
Ctemplate_numberingt< dstringt > | |
Ctemplate_numberingt< dstringt, dstring_hash > | |
Ctemplate_numberingt< exprt > | |
Ctemplate_numberingt< exprt, irep_hash > | |
Ctemplate_numberingt< irep_idt > | |
Ctemplate_numberingt< irep_idt, irep_id_hash > | |
Ctemplate_numberingt< packedt, vector_hasht > | |
Ctemplate_numberingt< T > | |
Ctemporary_filet | |
Cmonomialt::termt | |
Cbmc_covert::testt | |
Cconcurrency_instrumentationt::thread_local_vart | |
Cgoto_symex_statet::threadt | |
Cgoto_convertt::throw_targett | |
►Ctimestampert | Timestamp class hierarchy |
Cmonotonic_timestampert | |
Cwall_clock_timestampert | |
Ctinfl_decompressor_tag | |
Ctinfl_huff_table | |
Cto_be_merged_irep_hash | |
Ctrace_automatont | |
Ctrace_optionst | |
Ctvt | |
Cdump_ct::typedef_infot | |
Cequalityt::typestructt | |
Cuncaught_exceptions_analysist | Computes in exceptions_map an overapproximation of the exceptions thrown by each method |
Cuncaught_exceptions_domaint | |
Cunified_difft | |
Cuninitializedt | |
Cunion_find< T > | |
Cunion_find< exprt > | |
Cunion_find< irep_idt > | |
Cunion_find_replacet | Similar interface to union-find for expressions, with a function for replacing sub-expressions by their result for find |
►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 | |
Cunwindsett | |
Cvalue_set_fivrnst::object_map_dt::validity_ranget | |
Cvalue_set_fivrt::object_map_dt::validity_ranget | |
Cvalue_set_dereferencet | Wrapper for a function dereferencing pointer expressions using a value set |
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_analysis_templatet< VSDT > | |
Cvalue_sett | State type in value_set_domaint, used in value-set analysis and goto-symex |
Cconstant_propagator_domaint::valuest | |
Cvalue_set_dereferencet::valuet | Return value for build_reference_to ; see that method for documentation |
Cmini_bdd_mgrt::var_table_entryt | |
Cjava_bytecode_convert_methodt::variablet | |
Cshared_bufferst::varst | |
►Cstd::vector< T > | STL class |
Clispexprt | |
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_interfacet | |
Ccbmc_parse_optionst | |
Cxml_parse_treet | |
Cxmlt | |
Cyy_buffer_state | |
Cyy_trans_info | |
Cyyalloc | |
CYYSTYPE | |