| C__CPROVER_cegis_instructiont | |
| C__CPROVER_contracts_car_set_t | A set of __CPROVER_contracts_car_t |
| C__CPROVER_contracts_car_t | A conditionally writable range of bytes |
| C__CPROVER_contracts_obj_set_t | A set of pointers |
| C__CPROVER_contracts_write_set_t | Runtime representation of a write set |
| 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_aggregate_tag | |
| ►Cabstract_aggregate_objectt< two_value_struct_abstract_objectt, struct_aggregate_typet > | |
| Ctwo_value_struct_abstract_objectt | |
| ►Cabstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet > | |
| Cfull_struct_abstract_objectt | |
| ►Cabstract_aggregate_objectt< two_value_array_abstract_objectt, array_aggregate_typet > | |
| Ctwo_value_array_abstract_objectt | |
| ►Cabstract_aggregate_objectt< two_value_union_abstract_objectt, union_aggregate_typet > | |
| Ctwo_value_union_abstract_objectt | |
| ►Cabstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet > | |
| Cfull_array_abstract_objectt | |
| Cabstract_aggregate_objectt< aggregate_typet, aggregate_traitst > | |
| Cabstract_environmentt | |
| Cabstract_equalert | |
| ►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 |
| Cabstract_hashert | |
| Cabstract_object_sett | |
| Cabstract_object_statisticst | |
| ►Cabstract_objectt::abstract_object_visitort | Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstract_object_pointert |
| Clocation_update_visitort | |
| Cmerge_location_update_visitort | |
| ►Cabstract_pointer_tag | |
| ►Cabstract_pointer_objectt | |
| Cconstant_pointer_abstract_objectt | |
| Ctwo_value_pointer_abstract_objectt | |
| Cvalue_set_pointer_abstract_objectt | |
| ►Cabstract_value_tag | |
| ►Cabstract_value_objectt | |
| Cconstant_abstract_valuet | |
| Cinterval_abstract_valuet | |
| Cvalue_set_abstract_objectt | |
| Cacceleratet | |
| Cacceleration_utilst | |
| Cframet::active_loop_infot | |
| Csmt_bit_vector_theoryt::addt | |
| 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 | This is the basic interface of the abstract interpreter with default implementations of the core functionality |
| ►Cai_recursive_interproceduralt | |
| ►Cait< escape_domaint > | |
| Cescape_analysist | |
| ►Cait< invariant_set_domaint > | |
| Cinvariant_propagationt | |
| ►Cait< global_may_alias_domaint > | |
| Cglobal_may_alias_analysist | This is a may analysis (i.e |
| ►Cait< constant_propagator_domaint > | |
| Cconstant_propagator_ait | |
| Cait< uninitialized_domaint > | |
| ►Cait< custom_bitvector_domaint > | |
| Ccustom_bitvector_analysist | |
| ►Cait< VSDT > | |
| Cvalue_set_analysis_templatet< VSDT > | This template class implements a data-flow analysis which keeps track of what values different variables might have at different points in the program |
| ►Cait< dep_graph_domaint > | |
| Cdependence_grapht | |
| ►Cai_three_way_merget | |
| Cvariable_sensitivity_dependence_grapht | |
| ►Cait< domainT > | Ait supplies three of the four components needed: an abstract interpreter (in this case handling function calls via recursion), a history factory (using the simplest possible history objects) and storage (one domain per location) |
| ►Cconcurrency_aware_ait< rd_range_domaint > | |
| Creaching_definitions_analysist | |
| Cconcurrency_aware_ait< domainT > | Base class for concurrency-aware abstract interpretation |
| ►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 | |
| Cvalue_set_domain_templatet< VST > | This is the domain for a value set analysis |
| ►Cvariable_sensitivity_domaint | |
| Cvariable_sensitivity_dependence_domaint | |
| ►Cai_domain_factory_baset | |
| ►Cai_domain_factoryt< invariant_set_domaint > | |
| Cinvariant_set_domain_factoryt | Pass the necessary arguments to the invariant_set_domaint's when constructed |
| ►Cai_domain_factoryt< rd_range_domaint > | |
| Crd_range_domain_factoryt | This ensures that all domains are constructed with the appropriate pointer back to the analysis engine itself |
| ►Cai_domain_factoryt< variable_sensitivity_domaint > | |
| Cvariable_sensitivity_domain_factoryt | |
| ►Cai_domain_factoryt< variable_sensitivity_dependence_domaint > | |
| Cvariable_sensitivity_dependence_domain_factoryt | This ensures that all domains are constructed with the node ID that links them to the graph part of the dependency graph |
| ►Cai_domain_factoryt< dep_graph_domaint > | |
| Cdep_graph_domain_factoryt | This ensures that all domains are constructed with the node ID that links them to the graph part of the dependency graph |
| ►Cai_domain_factoryt< domainT > | |
| Cai_domain_factory_default_constructort< domainT > | |
| Cai_domain_factory_location_constructort< domainT > | |
| ►Cai_history_baset | A history object is an abstraction / representation of the control-flow part of a set of traces |
| Cahistoricalt | The common case of history is to only care about where you are now, not how you got there! Invariants are not checkable due to C++.. |
| Ccall_stack_historyt | Records the call stack Care must be taken when using this on recursive code; it will need the domain to be capable of limiting the recursion |
| Clocal_control_flow_historyt< track_forward_jumps, track_backward_jumps > | Whether we track forwards and / or backwards jumps is compile-time fixed as it does not need to be variable and because there may be a lot of history objects created |
| ►Cai_history_factory_baset | As more detailed histories can get complex (for example, nested loops or deep, mutually recursive call stacks) they often need some user controls or limits |
| Cai_history_factory_default_constructort< traceT > | An easy factory implementation for histories that don't need parameters |
| Ccall_stack_history_factoryt | |
| Clocal_control_flow_history_factoryt | |
| ►Cai_storage_baset | This is the basic interface for storing domains |
| ►Ctrace_map_storaget | |
| Chistory_sensitive_storaget | |
| Clocation_sensitive_storaget | The most conventional storage; one domain per location |
| Callocate_objectst | |
| Cancestry_resultt | Result of an attempt to find ancestor information about two nodes |
| Csmt_bit_vector_theoryt::andt | |
| Csmt_core_theoryt::andt | |
| Cjava_bytecode_parse_treet::annotationt | |
| ►Cansi_c_convert_typet | |
| Ccpp_convert_typet | |
| Cansi_c_identifiert | |
| Cansi_c_parse_treet | |
| Cansi_c_scopet | |
| Cconfigt::ansi_ct | |
| Capi_messaget | |
| Capi_optionst | |
| Capi_session_implementationt | |
| Capi_sessiont | |
| Cbv_refinementt::approximationt | |
| Cgoto_cc_cmdlinet::argt | |
| Csmt_bit_vector_theoryt::arithmetic_shift_rightt | |
| Carray_aggregate_typet | |
| Carrayst::array_equalityt | |
| Carray_poolt | Correspondance between arrays and pointers string representations |
| Csolver_hardnesst::assertion_statst | |
| Cc_wranglert::assertiont | |
| Cassignmentt | Assignment from the rhs value to the lhs variable |
| Cat_scope_exitt< functiont > | |
| Cautomatont | |
| Caxiomst | |
| ►Cstd::basic_string< Char > | STL class |
| ►Cstd::string | STL class |
| Clispsymbolt | |
| Cbdd_exprt | Conversion between exprt and bbdt This encapsulate a bdd_managert, thus BDDs created with this class should only be combined with BDDs created using the same instance of bdd_exprt |
| Cbdd_nodet | Low level access to the structure of the BDD, read-only |
| Ccover_basic_blockst::block_infot | |
| Cjava_bytecode_convert_methodt::block_tree_nodet | |
| Cboolbv_mapt | |
| Cboolbv_widtht | |
| Cboundst | |
| Cgoto_convertt::break_continue_targetst | |
| Cgoto_convertt::break_switch_targetst | |
| Cbuild_declaration_hops_inputst | |
| Cstring_dependenciest::builtin_function_nodet | A builtin function node contains a builtin function call |
| Cbv_arithmetict | |
| Cconfigt::bv_encodingt | |
| Cbv_minimizet | |
| Cbv_spect | |
| Cbv_utilst | |
| Cbytecode_infot | |
| Cc_declarationt | |
| Cc_definest | This class maintains a representation of one assignment to the preprocessor macros in a C program |
| ►Cc_qualifierst | |
| Cjava_qualifierst | |
| Cc_storage_spect | |
| Cc_test_input_generatort | |
| ►Cc_typecastt | |
| Ccpp_typecastt | |
| Cc_wranglert | |
| Ccall_checkt< Base, T > | |
| Ccall_grapht | A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection |
| Ccall_stack_historyt::call_stack_entryt | |
| Ccheck_call_sequencet::call_stack_entryt | |
| Ccall_validate_fullt< Base, T > | |
| Ccall_validatet< Base, T > | |
| ►Ccan_forward_propagatet | Determine whether an expression is constant |
| Cconstant_propagator_can_forward_propagatet | |
| Cgoto_symex_can_forward_propagatet | |
| Chavoc_utils_can_forward_propagatet | A class containing utility functions for havocing expressions |
| Cgoto_program2codet::caset | |
| Ccbmc_invariants_should_throwt | Helper to enable invariant throwing as above bounded to an object lifetime: |
| Ccegis_evaluatort | Evaluator for checking if an expression is consistent with a given set of test cases (positive examples and negative examples) |
| Ccegis_verifiert | Verifier that take a goto program as input, and output formatted counterexamples for counterexample-guided-synthesis |
| Ccext | Formatted counterexample |
| Ccfg_dominators_templatet< P, T, post_dom > | Dominator graph |
| Ccfg_dominators_templatet< P, T, false > | |
| ►Ccfg_infot | Stores information about a goto function computed from its CFG |
| Cfunction_cfg_infot | |
| Cgoto_program_cfg_infot | For a goto program |
| Cloop_cfg_infot | |
| Ccfg_instruction_to_dense_integert< T > | Functor to convert cfg nodes into dense integers, used by cfg_baset |
| Ccfg_instruction_to_dense_integert< goto_programt::const_targett > | GOTO-instruction to location number functor |
| Cfull_slicert::cfg_nodet | |
| Cinstrumentert::cfg_visitort | |
| Cshared_bufferst::cfg_visitort | |
| Cchange_impactt | |
| Ccharacter_refine_preprocesst | |
| Ccheck_call_sequencet | |
| Cci_lazy_methods_neededt | |
| Cci_lazy_methodst | |
| 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 | |
| ►Cclause_hardness_collectort | |
| Csolver_hardnesst | A structure that facilitates collecting the complexity statistics from a decision procedure |
| Cclauset | |
| Cgoto_convertt::clean_expr_resultt | |
| 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 | |
| Ccode_with_references_listt | Wrapper around a list of shared pointer to code_with_referencest objects, which provides a nicer interface |
| ►Ccode_with_referencest | Base class for code which can contain references which can get replaced before generating actual codet |
| Ccode_without_referencest | Code that should not contain reference |
| Creference_allocationt | Allocation code which contains a reference |
| Cabstract_objectt::combine_result | Clones the first parameter and merges it with the second |
| Cmessaget::commandt | |
| Ccompare_base_name_and_descriptort | |
| Cai_history_baset::compare_historyt | In a number of places we need to work with sets of histories so that these (a) make use of the immutability and sharing and (b) ownership can be transfered if necessary, we use shared pointers rather than references |
| Csmt_bit_vector_theoryt::comparet | |
| Ccompilet | |
| Ccomplexity_limitert | Symex complexity module |
| ►Cclass_typet::componentt | |
| Cjava_class_typet::componentt | |
| 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 |
| Csmt_bit_vector_theoryt::concatt | |
| Cconcurrency_instrumentationt | |
| Cgoto_check_ct::conditiont | |
| Ccone_of_influencet | |
| ►Cbv_refinementt::configt | |
| ►Cbv_refinementt::infot | |
| Cstring_refinementt::infot | String_refinementt constructor arguments |
| Cconfigt | Globally accessible architectural configuration |
| ►Cstring_refinementt::configt | |
| Cstring_refinementt::infot | String_refinementt constructor arguments |
| ►Cconflict_providert | |
| ►Cprop_conv_solvert | |
| ►Cequalityt | |
| ►Carrayst | |
| ►Cboolbvt | |
| Cbv_pointers_widet | |
| ►Cbv_pointerst | |
| Cbv_dimacst | |
| Cbv_minimizing_dect | |
| ►Cbv_refinementt | |
| Cstring_refinementt | |
| Cconsolet | |
| ►Cconst_expr_visitort | |
| Cfunction_binding_visitort | |
| Csmall_mapt< T, Ind, Num >::const_iterator | Const iterator |
| Cconst_target_hash | |
| Csmall_mapt< T, Ind, Num >::const_value_iterator | Const value iterator |
| Cconstants_evaluator | |
| Crecursive_initializationt::constructor_keyt | |
| Cconstructor_oft< constructedt > | A type of functor which wraps around the set of constructors of a type |
| Cgeneric_parameter_specialization_mapt::container_paramt | The index of the container and the type parameter inside that container |
| Ccontract_clausest | |
| Ccontracts_wranglert | |
| 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_goalst | Try to cover some given set of goals incrementally |
| ►Ccover_instrumenter_baset | Base class for goto program coverage instrumenters |
| Ccover_assertion_instrumentert | Assertion coverage instrumenter |
| Ccover_assume_instrumentert | |
| 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_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 |
| Cgdb_interaction_exceptiont | |
| 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 |
| 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_function_contract_pair_exceptiont | Exception thrown for bad function/contract specification pairs passed on the CLI |
| ►Cinvalid_input_exceptiont | Thrown when user-provided input cannot be processed |
| Cinvalid_source_file_exceptiont | Thrown when we can't handle something in an input source file |
| Cinvalid_restriction_exceptiont | |
| 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 | |
| Ccprover_parse_optionst | |
| Cevent_grapht::critical_cyclet | |
| Ccscannert | |
| Cctokenitt | |
| Cctokent | |
| Cdata_dpt | |
| Cdatat | |
| Cdecision_procedure_objectt | Information the decision procedure holds about each object |
| ►Cdecision_proceduret | An interface for a decision procedure for satisfiability problems |
| ►Cstack_decision_proceduret | |
| ►Cprop_convt | |
| Cprop_conv_solvert | |
| ►Csmt2_convt | |
| Csmt2_dect | Decision procedure interface for various SMT 2.x solvers |
| Cstate_encoding_smt2_convt | |
| Csmt2_incremental_decision_proceduret | |
| Cscope_treet::declaration_statet | |
| Cdefault_trace_stept | |
| Cboolbv_widtht::defined_entryt | |
| Cc_definest::definet | |
| Cevent_grapht::critical_cyclet::delayt | |
| Csharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::delta_view_itemt | |
| Cdense_integer_mapt< K, V, KeyToDenseInteger > | A map type that is backed by a vector, which relies on the ability to (a) see the keys that might be used in advance of their usage, and (b) map those keys onto a dense range of integers |
| Cdense_integer_mapt< goto_programt::const_targett, entryt, cfg_instruction_to_dense_integert< goto_programt::const_targett > > | |
| Cdep_edget | |
| Cvariable_sensitivity_dependence_domaint::dependency_ordert | |
| 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 | Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value sets (from goto-symex's working value set) and retrieve or create failed symbols on demand |
| Cdesignatort | |
| Cdestructor_and_idt | Result of a tree query holding both destructor codet and the ID of the node that held it |
| Cdestructt< I, pointee_baset, Ts > | |
| Cdestructt< 0, pointee_baset, Ts... > | |
| Cdfcc_cfg_infot | Computes natural loops, enforces normal form conditions, computes the nesting graph, tags each instruction of the function with the loop ID of the innermost loop and loop instruction type |
| Cdfcc_contract_clauses_codegent | Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that build write sets or havoc write sets |
| Cdfcc_contract_functionst | Generates GOTO functions modelling a contract assigns and frees clauses |
| Cdfcc_contract_handlert | A contract is represented by a function declaration or definition with contract clauses attached to its signature: |
| Cdfcc_instrument_loopt | This class applies the loop contract transformation to a loop in a goto function |
| Cdfcc_instrumentt | This class instruments GOTO functions or instruction sequences for frame condition checking and loop contracts |
| Cdfcc_is_freeablet | Rewrites calls to is_freeable and was_freed predicates in goto programs encoding pre and post conditions |
| Cdfcc_is_fresht | Rewrites calls to is_fresh predicates into calls to the library implementation |
| Cdfcc_libraryt | Class interface to library types and functions defined in cprover_contracts.c |
| Cdfcc_lift_memory_predicatest | |
| Cdfcc_loop_infot | Describes a single loop for the purpose of DFCC loop contract instrumentation |
| Cdfcc_obeys_contractt | Rewrites calls to obeys_contract predicates into calls to the library implementation |
| Cdfcc_pointer_in_ranget | Rewrites calls to pointer_in_range predicates into calls to the library implementation |
| Cdfcc_spec_functionst | This class rewrites GOTO functions that use the built-ins: |
| Cdfcc_swap_and_wrapt | |
| Cdfcc_utilst | |
| Cdfcc_wrapper_programt | Generates the body of a wrapper function from a contract specified using requires, assigns, frees, ensures, clauses attached to a function symbol |
| Cdfcct | Entry point into the contracts transformation |
| 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 | Dirty variables are ones which have their address taken so we can't reliably work out where they may be assigned and are also considered shared state in the presence of multi-threading |
| Cdisjunctive_polynomial_accelerationt | |
| Cdispatch_table_entryt | |
| Csmt_core_theoryt::distinctt | |
| Cdjb_manglert | Mangle identifiers by hashing their working directory with djb2 hash |
| Cdocument_propertiest::doc_claimt | |
| Cdocument_propertiest | |
| Cdoes_remove_constt | |
| Cdott | |
| Cdstring_hash | |
| Cdstringt | dstringt has one field, an unsigned integer no which is an index into a static table of strings |
| Cdump_c_configurationt | Used for configuring the behaviour of dump_c |
| 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 | |
| ►Cstd::enable_shared_from_this | |
| ►Cabstract_objectt | |
| Cabstract_aggregate_objectt< two_value_struct_abstract_objectt, struct_aggregate_typet > | |
| Cabstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet > | |
| Cabstract_aggregate_objectt< two_value_array_abstract_objectt, array_aggregate_typet > | |
| Cabstract_aggregate_objectt< two_value_union_abstract_objectt, union_aggregate_typet > | |
| Cabstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet > | |
| Cabstract_aggregate_objectt< aggregate_typet, aggregate_traitst > | |
| Cabstract_pointer_objectt | |
| Cabstract_value_objectt | |
| ►Ccontext_abstract_objectt | |
| ►Cwrite_location_contextt | General implementation of an abstract_objectt which tracks the last written locations for a given abstract_objectt |
| Cdata_dependency_contextt | |
| Cliveness_contextt | General implementation of an abstract_objectt which tracks the last written locations for a given abstract_objectt |
| ►Cencoding_targett | |
| Cascii_encoding_targett | |
| Cascii_encoding_targett | |
| Ccontainer_encoding_targett | |
| Ccontainer_encoding_targett | |
| Csmt2_encoding_targett | |
| Csmt2_encoding_targett | |
| ►Cendianness_mapt | Maps a big-endian offset to a little-endian offset |
| Cbv_endianness_mapt | Map bytes according to the configured endianness |
| Cendianness_map_widet | |
| Cmemory_snapshot_harness_generatort::entry_goto_locationt | User provided goto location: function name and (maybe) location number; the structure wraps this option with a parser |
| Cmemory_snapshot_harness_generatort::entry_locationt | Wraps the information needed to identify the entry point |
| Ccfg_baset< T, P, I >::entry_mapt | |
| Cmemory_snapshot_harness_generatort::entry_source_locationt | User provided source location: file name and line number; the structure wraps this option with a parser |
| Cclass_hierarchyt::entryt | |
| Cdesignatort::entryt | |
| Cinv_object_storet::entryt | |
| Crw_set_baset::entryt | |
| Cvalue_set_fit::entryt | |
| Cvalue_sett::entryt | Represents a row of a value_sett |
| Cenumerating_loop_accelerationt | |
| ►Cenumerator_baset | A base class for expression enumerators |
| Calternatives_enumeratort | Enumerators that enumerates expressions in the union of enumerated expressions of sub-enumerators |
| Cleaf_enumeratort | Enumerator that enumerates leaf expressions from a given list |
| ►Cnon_leaf_enumeratort | Non-leaf enumerator enumerates expressions of form f(a_1, a_2, ..., a_n) where a_i's are sub-expressions enumerated by sub-enumerators |
| Cbinary_functional_enumeratort | Enumerator that enumerates binary functional expressions |
| Crecursive_enumerator_placeholdert | Placeholders for actual enumerators, which represent nonterminals |
| Cenumerator_factoryt | Factory for enumerator that can be used to represent a tree grammar |
| Cprintf_formattert::eol_exceptiont | |
| Cmessaget::eomt | |
| Csmt_core_theoryt::equalt | |
| Cequation_symbol_mappingt | Maps equation to expressions contained in them and conversely expressions to equations that contain them |
| Ctypecheckt::errort | |
| Ceval_index_resultt | |
| Cevent_grapht | |
| ►Cstd::exception | STL class |
| Cno_unique_unimplemented_method_exceptiont | |
| 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 |
| 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 | |
| Cexpr2stlt | Class for saving the internal state of the conversion process |
| Cdetail::expr_dynamic_cast_return_typet< Ret, T > | |
| Cexpr_initializert | |
| Cexpr_queryt< T > | Wrapper for std::optional<exprt> with useful method for queries to be used in unit tests |
| Cexpr_skeletont | Expression in which some part is missing and can be substituted for another expression |
| Cdetail::expr_try_dynamic_cast_return_typet< Ret, T > | |
| Cexpr_visitort | |
| Csmt_bit_vector_theoryt::extractt | |
| Csmt_function_application_termt::factoryt< functiont > | |
| Csmt_function_application_termt::factoryt< smt_array_theoryt::selectt > | |
| Csmt_function_application_termt::factoryt< smt_array_theoryt::storet > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::addt > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::andt > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::arithmetic_shift_rightt > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::comparet > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::concatt > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::logical_shift_rightt > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::multiplyt > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::nandt > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::negatet > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::nort > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::nott > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::ort > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::shift_leftt > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_dividet > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_greater_than_or_equalt > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_greater_thant > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_less_than_or_equalt > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_less_thant > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_remaindert > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::subtractt > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_dividet > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_greater_than_or_equalt > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_greater_thant > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_less_than_or_equalt > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_less_thant > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_remaindert > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::xnort > | |
| Csmt_function_application_termt::factoryt< smt_bit_vector_theoryt::xort > | |
| Csmt_function_application_termt::factoryt< smt_command_functiont > | |
| Csmt_function_application_termt::factoryt< smt_core_theoryt::andt > | |
| Csmt_function_application_termt::factoryt< smt_core_theoryt::distinctt > | |
| Csmt_function_application_termt::factoryt< smt_core_theoryt::equalt > | |
| Csmt_function_application_termt::factoryt< smt_core_theoryt::if_then_elset > | |
| Csmt_function_application_termt::factoryt< smt_core_theoryt::impliest > | |
| Csmt_function_application_termt::factoryt< smt_core_theoryt::nott > | |
| Csmt_function_application_termt::factoryt< smt_core_theoryt::ort > | |
| Csmt_function_application_termt::factoryt< smt_core_theoryt::xort > | |
| ►Cstd::false_type | |
| Cdetail::always_falset< T > | |
| Csmt_function_application_termt::has_indicest< functiont, class > | |
| Csharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::falset | |
| Cfat_header_prefixt | |
| ►Cfault_localization_providert | An implementation of incremental_goto_checkert may implement this interface to provide fault localization information |
| ►Cmulti_path_symex_checkert | Performs a multi-path symbolic execution using goto-symex and calls a SAT/SMT solver to check the status of the properties |
| Cjava_multi_path_symex_checkert | |
| Cfault_location_infot | |
| Cfield_sensitivityt | Control granularity of object accesses |
| Cfile_name_manglert | Mangle identifiers by including their filename |
| Cfilter_iteratort< iteratort > | Iterator which only stops at elements for which some given function f is true |
| Cfind_is_fresh_calls_visitort | Predicate to be used with the exprt::visit() function |
| Cfixed_keys_map_wrappert< mapt > | |
| Cfixedbv_spect | |
| Cfixedbvt | |
| Cflag_overridet | Allows to: |
| Clocal_bitvector_analysist::flagst | |
| Cfloat_bvt | |
| ►Cfloat_utilst | |
| Cfloat_approximationt | |
| ►Cflow_insensitive_abstract_domain_baset | |
| Cvalue_set_domain_fit | |
| ►Cflow_insensitive_analysis_baset | |
| ►Cflow_insensitive_analysist< value_set_domain_fit > | |
| Cvalue_set_analysis_fit | |
| Cflow_insensitive_analysist< T > | |
| Cformat_containert< T > | The below enables convenient syntax for feeding objects into streams, via stream << format(o) |
| Cformat_elementt | |
| Cformat_expr_configt | |
| Cformat_specifiert | Field names follow the OpenJDK implementation: http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/9b8c96f96a0f/src/share/classes/java/util/Formatter.java#l2569 |
| ►Cformat_spect | |
| Cformat_constantt | |
| Cformat_textt | |
| Cformat_tokent | |
| ►Cstd::forward_list< T > | STL class |
| Cforward_list_as_mapt< keyt, mappedt > | Implementation of map-like interface using a forward list |
| Cframe_reft | |
| Cframet | Stack frames – these are used for function calls and for exceptions |
| Cfreert | A functor wrapping std::free |
| Cfrequency_mapt | |
| Cfull_slicert | |
| Cinterpretert::function_assignments_contextt | |
| Cinterpretert::function_assignmentt | |
| Cfunction_assignst | |
| Cc_wranglert::function_contract_clauset | |
| ►Cfunction_filter_baset | Base class for filtering functions |
| Cfile_filtert | |
| Cinclude_pattern_filtert | Filters functions that match the provided pattern |
| Cinternal_functions_filtert | Filters out CPROVER internal functions |
| Csingle_function_filtert | |
| Ctrivial_functions_filtert | Filters out trivial functions |
| Cfunction_filterst | A collection of function filters to be applied in conjunction |
| Cfunction_indicest | Helper class that maintains a map from function name to grapht node index and adds nodes to the graph on demand |
| Cfunctionst::function_infot | |
| Cfunction_itt_hasht | |
| Cfunction_loc_pair_hasht | |
| Cfunction_loc_pairt | |
| Cfunction_name_manglert< MangleFun > | Mangles the names in an entire program and its symbol table |
| Cfunction_pointer_restrictionst | |
| Cfunctions_in_scope_visitort | Predicate to be used with the exprt::visit() function |
| Cfunctionst | |
| Cc_wranglert::functiont | |
| Cfunctiont | |
| Cgcc_versiont | |
| Cgdb_apit | Interface for running and querying GDB |
| Cgdb_value_extractort | Interface for extracting values from GDB (building on gdb_apit) |
| ►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 | |
| Cgeneric_parameter_specialization_mapt | Author: Diffblue Ltd |
| Cget_typet< I, Ts > | Get the type with the given index in the parameter pack |
| Cget_virtual_calleest | |
| ►Cgoal_filter_baset | Base class for filtering goals |
| Cinternal_goals_filtert | Filters out goals with source locations considered internal |
| Cgoal_filterst | A collection of goal filters to be applied in conjunction |
| Ccover_goalst::goalt | |
| Cgoto_symex_property_decidert::goalt | |
| ►Cgoto_cc_modet | |
| Carmcc_modet | |
| Cas_modet | |
| Ccw_modet | |
| Cgcc_modet | |
| Cld_modet | |
| Cms_cl_modet | |
| Cms_link_modet | |
| Cgoto_check_ct | |
| ►Cgoto_difft | |
| Cjava_syntactic_difft | |
| Csyntactic_difft | |
| Cgoto_functionst | A collection of goto functions |
| Cgoto_functiont | A goto function, consisting of function body (see body) and parameter identifiers (see parameter_identifiers) |
| Cgoto_harness_parse_optionst::goto_harness_configt | |
| Cgoto_harness_generator_factoryt | Helper to select harness type by name |
| ►Cgoto_harness_generatort | |
| Cfunction_call_harness_generatort | Function harness generator that for a specified goto-function generates a harness that sets up its arguments and calls it |
| Cmemory_snapshot_harness_generatort | Generates a harness which first assigns global variables with values from a given memory snapshot and then calls a specified function |
| Cgoto_inlinet::goto_inline_logt::goto_inline_log_infot | |
| Cgoto_inlinet::goto_inline_logt | |
| Cgoto_inlinet | |
| Cgoto_model_functiont | Interface providing access to a single function in a GOTO model, plus its associated symbol table |
| Cgoto_model_validation_optionst | |
| 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_statet | Container for data that varies per program point, e.g |
| Cgoto_symex_statet | Central data structure: state |
| Cgoto_symex_fault_localizert | |
| Cgoto_symex_property_decidert | Provides management of goal variables that encode properties |
| ►Cgoto_symext | The main class for the forward symbolic simulator |
| Cscratch_program_symext | |
| ►Csymex_bmct | |
| Csymex_bmc_incremental_one_loopt | |
| ►Cgoto_trace_providert | An implementation of incremental_goto_checkert may implement this interface to provide goto traces |
| Cmulti_path_symex_checkert | Performs a multi-path symbolic execution using goto-symex and calls a SAT/SMT solver to check the status of the properties |
| Csingle_loop_incremental_symex_checkert | Performs a multi-path symbolic execution using goto-symex that incrementally unwinds a given loop and calls a SAT/SMT solver to check the status of the properties after each iteration |
| ►Csingle_path_symex_checkert | Uses goto-symex to symbolically execute each path in the goto model and calls a solver to find property violations |
| Cjava_single_path_symex_checkert | |
| Cgoto_trace_stept | Step of the trace of a GOTO program |
| Cgoto_trace_storaget | |
| Cgoto_tracet | Trace of a GOTO program |
| Cgoto_unwindt | |
| ►Cgoto_verifiert | An implementation of goto_verifiert checks all properties in a goto model |
| Call_properties_verifier_with_fault_localizationt< incremental_goto_checkerT > | Requires an incremental goto checker that is a goto_trace_providert and fault_localization_providert |
| Call_properties_verifier_with_trace_storaget< incremental_goto_checkerT > | |
| Call_properties_verifiert< incremental_goto_checkerT > | |
| Ccover_goals_verifier_with_trace_storaget< incremental_goto_checkerT > | |
| Cstop_on_fail_verifier_with_fault_localizationt< incremental_goto_checkerT > | Stops when the first failing property is found and localizes the fault Requires an incremental goto checker that is a goto_trace_providert and fault_localization_providert |
| Cstop_on_fail_verifiert< incremental_goto_checkerT > | Stops when the first failing property is found |
| ►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 |
| ►Cgraph_nodet< dep_edget > | |
| Cdep_nodet | |
| ►Cgraph_nodet< E > | |
| Cvisited_nodet< E > | A node type with an extra bit |
| ►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 |
| Cdfcc_loop_nesting_graph_nodet | A graph node that stores information about a natural loop |
| Cscope_treet::scope_nodet | |
| ►Cgraph_nodet< vs_dep_edget > | |
| Cvs_dep_nodet | |
| ►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< slicer_entryt, goto_programt::const_targett > > | |
| Ccfg_baset< slicer_entryt > | |
| ►Cgrapht< cfg_base_nodet< T, goto_programt::const_targett > > | |
| ►Ccfg_baset< T, const goto_programt, goto_programt::const_targett > | |
| ►Cconcurrent_cfg_baset< T, const goto_programt, goto_programt::const_targett > | |
| Cprocedure_local_concurrent_cfg_baset< T, P, I > | |
| ►Cprocedure_local_cfg_baset< T, const goto_programt, goto_programt::const_targett > | |
| Cprocedure_local_concurrent_cfg_baset< T, P, I > | |
| Cconcurrent_cfg_baset< T, P, I > | |
| Cprocedure_local_cfg_baset< T, P, I > | |
| ►Ccfg_baset< T, P, I > | A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO program |
| Cprocedure_local_cfg_baset< nodet, P, T > | |
| Cgrapht< cfg_base_nodet< T, 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< scope_treet::scope_nodet > | |
| ►Cgrapht< vs_dep_nodet > | |
| Cvariable_sensitivity_dependence_grapht | |
| ►Cgrapht< xml_graph_nodet > | |
| Cgraphmlt | |
| Cguard_bddt | |
| Cguard_expr_managert | This is unused by this implementation of guards, but can be used by other implementations of the same interface |
| Cguard_exprt | |
| ►Chardness_collectort | |
| ►Csatcheck_glucose_baset< Glucose::Solver > | |
| Csatcheck_glucose_no_simplifiert | |
| ►Csatcheck_glucose_baset< Glucose::SimpSolver > | |
| Csatcheck_glucose_simplifiert | |
| ►Csatcheck_minisat2_baset< Minisat::SimpSolver > | |
| Csatcheck_minisat_simplifiert | |
| ►Csatcheck_minisat2_baset< Minisat::Solver > | |
| Csatcheck_minisat_no_simplifiert | |
| ►Csatcheck_cadical_baset | |
| Csatcheck_cadical_no_preprocessingt | |
| Csatcheck_cadical_preprocessingt | |
| Csatcheck_glucose_baset< T > | |
| Csatcheck_ipasirt | Interface for generic SAT solver interface IPASIR |
| Csatcheck_minisat2_baset< T > | |
| Csolver_hardnesst::hardness_ssa_keyt | |
| Cstd::hash< dstringt > | Default hash function of dstringt for use with STL containers |
| Cstd::hash< solver_hardnesst::hardness_ssa_keyt > | |
| Cstd::hash< string_not_contains_constraintt > | |
| Cstd::hash<::symbol_exprt > | |
| Chavoc_loopst | |
| ►Chavoc_utilst | |
| ►Chavoc_if_validt | A class that overrides the low-level havocing functions in the base utility class, to havoc only when expressions point to valid memory, i.e |
| Chavoc_assigns_targetst | A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_object expressions |
| Chelp_formattert | |
| Cjava_bytecode_convert_methodt::holet | |
| Cidentifiert | |
| Csmt2_convt::identifiert | |
| Cidentity_functort | Identity functor. When we use C++20 this can be replaced with std::identity |
| Csmt2_parsert::idt | |
| Cieee_float_spect | |
| Cieee_floatt | |
| Csmt_core_theoryt::if_then_elset | |
| Cframet::implicationt | |
| Csmt_core_theoryt::impliest | |
| Cfunction_call_harness_generatort::implt | This contains implementation details of function call harness generator to avoid leaking them out into the header |
| Cincremental_dirtyt | Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly once |
| ►Cincremental_goto_checkert | An implementation of incremental_goto_checkert provides functionality for checking a set of properties and returning counterexamples one by one to the caller |
| ►Cmulti_path_symex_only_checkert | |
| Cjava_multi_path_symex_only_checkert | |
| Cmulti_path_symex_checkert | Performs a multi-path symbolic execution using goto-symex and calls a SAT/SMT solver to check the status of the properties |
| Csingle_loop_incremental_symex_checkert | Performs a multi-path symbolic execution using goto-symex that incrementally unwinds a given loop and calls a SAT/SMT solver to check the status of the properties after each iteration |
| ►Csingle_path_symex_only_checkert | Uses goto-symex to generate a symex_target_equationt for each path |
| Cjava_single_path_symex_only_checkert | |
| Csingle_path_symex_checkert | Uses goto-symex to symbolically execute each path in the goto model and calls a solver to find property violations |
| ►Cindex_range_implementationt | |
| Cempty_index_ranget | |
| Cinterval_index_ranget | |
| ►Csingle_value_index_ranget | |
| Cconstant_index_ranget | |
| Cindeterminate_index_ranget | |
| Cvalue_set_index_ranget | |
| Cindex_range_iteratort | |
| Cindex_ranget | |
| Cindex_set_pairt | |
| Cinductiveness_resultt | |
| Cinfix_opt | |
| Cinflate_state | |
| Cresolve_inherited_componentt::inherited_componentt | |
| Cinsert_final_assert_falset | |
| Ccpp_typecheckt::instantiation_levelt | |
| Ccpp_typecheckt::instantiationt | |
| Cgoto_programt::instructiont | This class represents an instruction in the GOTO intermediate representation |
| Cjava_bytecode_parse_treet::instructiont | |
| Cstatement_list_parse_treet::instructiont | Represents a regular Statement List instruction which consists out of one or more codet tokens |
| ►Cinstrument_spec_assignst | A class that generates instrumentation for assigns clause checking |
| Chavoc_assigns_clause_targetst | Class to generate havocking instructions for target expressions of a function contract's assign clause (replacement) |
| ►Cinstrumentert | |
| Cinstrumenter_pensievet | |
| Cinterpretert | |
| Cinterval | |
| Cinterval_evaluator | |
| Cinterval_templatet< T > | |
| Cinterval_uniont | Represents a set of integers by a union of intervals, which are stored in increasing order for efficient union and intersection (linear time in both cases) |
| 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 | |
| Cis_compile_time_constantt | Architecturally similar to can_forward_propagatet, but specialized for what is a constexpr, i.e., an expression that can be fully evaluated at compile time |
| ►Cis_fresh_baset | |
| Cis_fresh_enforcet | |
| Cis_fresh_replacet | |
| Cis_predecessor_oft | |
| Cis_threadedt | |
| Cdense_integer_mapt< K, V, KeyToDenseInteger >::iterator_templatet< UnderlyingIterator, UnderlyingValue > | |
| Csymbol_table_baset::iteratort | |
| Cjar_filet | Class representing a .jar archive |
| Cjar_poolt | A chache for jar_filet objects, by file name |
| Cjava_boxed_type_infot | Return type for get_boxed_type_info_by_name |
| Cjava_bytecode_convert_classt | |
| Cjava_bytecode_convert_methodt | |
| Cjava_bytecode_instrumentt | |
| Cjava_bytecode_language_optionst | |
| Cjava_bytecode_parse_treet | |
| ►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_object_factoryt | |
| Cjava_primitive_type_infot | Return type for get_java_primitive_type_info |
| Cjava_simple_method_stubst | |
| Cjava_string_library_preprocesst | |
| Cconfigt::javat | |
| 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 | |
| Clabelt | |
| Cjava_bytecode_parse_treet::classt::lambda_method_handlet | |
| Clanguage_entryt | |
| Clanguage_filest | |
| Clanguage_filet | |
| Clanguage_modulet | |
| ►Clanguaget | |
| Cansi_c_languaget | |
| Ccpp_languaget | |
| Cjava_bytecode_languaget | |
| Cjson_symtab_languaget | |
| Cstatement_list_languaget | Implements the language interface for the Statement List language |
| Clazy_class_to_declared_symbols_mapt | Map classes to the symbols they declare but is only computed once it is needed and the map is then kept |
| Carrayst::lazy_constraintt | |
| Clazy_goto_functions_mapt | Provides a wrapper for a map of lazily loaded goto_functiont |
| Clazyt< valuet > | |
| Cgoto_convertt::leave_targett | |
| Cleft_and_right_valuest | |
| Cletifyt::let_count_idt | |
| Cletifyt | Introduce LET for common subexpressions |
| Clevenshtein_automatont | Simple automaton that can detect whether a string can be transformed into another with a limited number of deletions, insertions or substitutions |
| Clinear_functiont | Canonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given by constant_coefficient 2 and coefficients: x -> 2, y -> -1 |
| Cdocument_propertiest::linet | |
| Clinker_script_merget | Synthesise definitions of symbols that are defined in linker scripts |
| Clinking_diagnosticst | |
| Clinkingt | |
| Cliteralt | |
| Clocal_may_aliast::loc_infot | |
| Clocal_bitvector_analysist | |
| Clocal_cfgt | |
| Clocal_control_flow_decisiont | Records all local control-flow decisions up to a limit of number of histories per location |
| 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 | |
| Cinstrument_spec_assignst::location_intervalt | Represents an interval of source locations covered by the static local variable search |
| Clocation_number_less_thant | |
| Cdata_dependency_contextt::location_ordert | |
| Csmt_bit_vector_theoryt::logical_shift_rightt | |
| ►Cloop_analysist< T, C > | |
| ►Cnatural_loops_templatet< const goto_programt, goto_programt::const_targett, goto_programt::target_less_than > | |
| Cnatural_loopst | A concretized version of natural_loops_templatet<const goto_programt, goto_programt::const_targett> |
| Cnatural_loops_templatet< goto_programt, goto_programt::targett, goto_programt::target_less_than > | |
| Clexical_loops_templatet< P, T, C > | Main driver for working out if a class (normally goto_programt) has any lexical loops |
| Clinked_loop_analysist< T, C > | |
| Cnatural_loops_templatet< P, T, C > | Main driver for working out if a class (normally goto_programt) has any natural loops |
| Cc_wranglert::loop_contract_clauset | |
| Cloop_contract_configt | Loop contract configurations |
| Cloop_contracts_clauset | |
| ►Cloop_contracts_synthesizer_baset | A base class for loop contracts synthesizers |
| Cenumerative_loop_contracts_synthesizert | Enumerative loop contracts synthesizers |
| Cloop_idt | Loop id used to identify loops |
| Cframet::loop_infot | |
| ►Cloop_templatet< T, C > | A loop, specified as a set of instructions |
| Cloop_with_parent_analysis_templatet< T, C > | |
| Cloop_templatet< goto_programt::targett, goto_programt::instructiont::target_less_than > | |
| Cmain_function_resultt | |
| Cboolbv_mapt::map_entryt | |
| Cmap_iteratort< iteratort, outputt > | Iterator which applies some given function f after each increment and returns its result on dereference |
| ►CCatch::MatcherBase | |
| Cinvariant_failure_containingt | |
| Csmt2_parser_error_containingt | |
| Ccpp_typecheck_resolvet::matcht | |
| Cboolbv_widtht::membert | |
| ►Cjava_bytecode_parse_treet::membert | |
| Cjava_bytecode_parse_treet::fieldt | |
| Cjava_bytecode_parse_treet::methodt | |
| Cgdb_apit::memory_addresst | Memory address imbued with the explicit boolean data indicating if the address is null or not |
| Cinterpretert::memory_cellt | |
| Cgdb_value_extractort::memory_scopet | |
| Cmemory_sizet | |
| Cmerge_full_irept | |
| Cmerge_irept | |
| Cmerged_irep_hash | |
| Cmerged_irepst | |
| ►Cmessage_handlert | |
| Capi_message_handlert | |
| ►Cconsole_message_handlert | |
| Ccl_message_handlert | |
| Cgcc_message_handlert | |
| Cinlining_decoratort | Decorator for a message_handlert used during function inlining that collect names of GOTO functions creating warnings and allows to turn inlining warnings into hard errors |
| 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' |
| ►Cgoto_convertt | |
| Ccleanert | Class that allows to clean expressions of side effects and to generate havoc_slice expressions |
| Cgoto_convert_functionst | |
| Cpreprocessort | |
| Csafety_checkert | |
| ►Ctypecheckt | |
| ►Cc_typecheck_baset | |
| Cansi_c_typecheckt | |
| Ccpp_typecheckt | |
| Cjava_bytecode_typecheckt | |
| Cstatement_list_typecheckt | Class for encapsulating the current state of the type check |
| Ccpp_typecheckt::method_bodyt | |
| Cmethod_bytecodet | |
| Cjava_bytecode_convert_methodt::method_with_amapt | |
| ►Cclass_typet::methodt | |
| Cjava_class_typet::methodt | |
| Cmini_bdd_applyt | |
| ►Cmini_bdd_mgrt | |
| Cbdd_managert | Manager for BDD creation |
| Cmini_bdd_nodet | |
| ►Cmini_bddt | |
| Cbddt | Logical operations on BDDs |
| Cmini_c_parsert | |
| Cmixd | |
| Cmixf | |
| Cmixl | |
| Cmm_iot | |
| Cmonomialt | |
| Cfull_array_abstract_objectt::mp_integer_hasht | |
| Cms_cl_versiont | |
| Csmt_bit_vector_theoryt::multiplyt | |
| 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 |
| Csmt_bit_vector_theoryt::nandt | |
| Csmt_bit_vector_theoryt::negatet | |
| Cstatement_list_typecheckt::nesting_stack_entryt | Every time branching occurs inside of a boolean expression string in STL, the current value of the RLO and OR bits are saved and put on a separate stack |
| Cstatement_list_parse_treet::networkt | Representation of a network in Siemens TIA |
| Cnew_scopet | |
| Cnfat< T > | Very simple NFA implementation Not super performant, but should be good enough for our purposes |
| Cnfat< char > | |
| Cstring_dependenciest::node_hash | Hash function for nodes |
| Ccfg_dominators_templatet< P, T, post_dom >::nodet | |
| Clocal_cfgt::nodet | |
| Cstring_dependenciest::nodet | |
| Cunsigned_union_find::nodet | |
| Cnon_sharing_treet< derivedt, named_subtreest > | Base class for tree-like data structures without sharing |
| Cnondet_instruction_infot | Holds information about any discovered nondet methods, with extreme type- safety |
| Cnondet_volatilet | |
| Csharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::noop_value_comparatort | |
| Csmt_bit_vector_theoryt::nort | |
| Csmt_bit_vector_theoryt::nott | |
| Csmt_core_theoryt::nott | |
| Cnumberingt< keyt, hasht > | |
| Cnumberingt< dstringt > | |
| Cnumberingt< exprt, irep_hash > | |
| Cnumberingt< irep_idt > | |
| Cnumberingt< packedt, irep_hash_container_baset::vector_hasht > | |
| Cnumberingt< T, std::hash< T > > | |
| 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_creation_infot | Values passed around between most functions of the recursive deterministic assignment algorithm entered from assign_from_json |
| Cobject_creation_referencet | Information to store when several references point to the same Java object |
| ►Cobject_factory_parameterst | |
| Cc_object_factory_parameterst | |
| Cjava_object_factory_parameterst | |
| Cobject_idt | |
| Cvalue_set_fit::object_map_dt | |
| Cprop_minimizet::objectivet | |
| Cc_wranglert::objectt | |
| Ccover_goalst::observert | |
| Coperator_entryt | |
| Ccmdlinet::option_namest::option_names_iteratort | |
| Ccmdlinet::option_namest | |
| Coptionst | |
| Ccmdlinet::optiont | |
| Csmt_bit_vector_theoryt::ort | |
| Csmt_core_theoryt::ort | |
| Cosx_fat_readert | |
| Cosx_mach_o_readert | |
| Coverflow_instrumentert | |
| Cgraphml_witnesst::pair_hash< S, T > | |
| Cparameter_assignmentst | |
| Cparse_floatt | |
| ►Cparse_options_baset | |
| Ccbmc_parse_optionst | |
| Ccrangler_parse_optionst | |
| Cgoto_analyzer_parse_optionst | |
| Cgoto_bmc_parse_optionst | |
| Cgoto_diff_parse_optionst | |
| Cgoto_harness_parse_optionst | |
| Cgoto_inspect_parse_optionst | |
| Cgoto_instrument_parse_optionst | |
| Cgoto_synthesizer_parse_optionst | |
| Cjanalyzer_parse_optionst | |
| Cjbmc_parse_optionst | |
| Cjdiff_parse_optionst | |
| Cmemory_analyzer_parse_optionst | |
| Csymtab2gb_parse_optionst | |
| Cstring_constraint_generatort::parseint_argumentst | Argument block for parseInt and cousins, common to parseInt itself and CProverString.isValidInt |
| CParser | |
| ►Cparsert | |
| Cansi_c_parsert | |
| Cassembler_parsert | |
| Ccpp_parsert | |
| Cjava_bytecode_parsert | |
| Cjson_parsert | |
| Cstatement_list_parsert | Responsible for starting the parse process and to translate the result into a statement_list_parse_treet |
| Cxml_parsert | |
| ►Cpartial_order_concurrencyt | Base class for implementing memory models via additional constraints for SSA equations |
| ►Cmemory_model_baset | |
| ►Cmemory_model_sct | |
| ►Cmemory_model_tsot | |
| Cmemory_model_psot | |
| 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_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 |
| Cpiped_processt | |
| 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 | |
| Cgdb_apit::pointer_valuet | Data associated with the value of a pointer, i.e |
| 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_pointers_widet::postponedt | |
| Cbv_pointerst::postponedt | |
| Cpreconditiont | |
| Cprefix_filtert | Provides filtering of strings vai inclusion/exclusion lists of prefixes |
| Cmemory_snapshot_harness_generatort::preordert< Key > | Simple structure for linearising posets |
| Cgeneric_parameter_specialization_mapt::printert | A wrapper for a generic_parameter_specialization_mapt and a namespacet that can be output to a stream |
| Cprintf_formattert | |
| ►CProofTraverser | |
| Cminisat_prooft | |
| Cprop_minimizet | Computes a satisfying assignment of minimal cost according to a const function using incremental SAT |
| Cproperty_infot | |
| Cpropertyt | |
| ►Cpropt | TO_BE_DOCUMENTED |
| ►Ccnft | |
| ►Ccnf_clause_listt | |
| ►Ccnf_clause_list_assignmentt | |
| Cexternal_satt | |
| ►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_glucose_baset< Glucose::Solver > | |
| Csatcheck_glucose_baset< Glucose::SimpSolver > | |
| Csatcheck_minisat2_baset< Minisat::SimpSolver > | |
| Csatcheck_minisat2_baset< Minisat::Solver > | |
| ►Csatcheck_booleforce_baset | |
| Csatcheck_booleforce_coret | |
| Csatcheck_booleforcet | |
| Csatcheck_cadical_baset | |
| Csatcheck_glucose_baset< T > | |
| 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_picosatt | |
| Cdimacs_cnf_dumpt | |
| Cboolbvt::quantifiert | |
| Cqdimacs_cnft::quantifiert | |
| ►Crange_domain_baset | |
| Cguarded_range_domaint | |
| Crange_domaint | |
| Crange_spect | Data type to describe upper and lower bounds of the range of bits that a read or write access may affect |
| 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 |
| Csharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::real_value_comparatort | |
| Crecursion_set_entryt | Recursion-set entry owner class |
| Crecursive_initialization_configt | |
| Crecursive_initializationt | Class for generating initialisation code for compound structures |
| Cconsolet::redirectt | |
| ►Cref_count_ift< enabled > | Used in tree_nodet for activating or not reference counting |
| Ctree_nodet< derivedt, named_subtreest, false > | |
| ►Cref_count_ift< true > | |
| Ctree_nodet< treet, named_subtreest, sharing > | A node with data in a tree, it contains: |
| Cref_expr_set_dt | |
| Creference_counting< T, empty > | |
| Creference_counting< object_map_dt > | |
| Creference_counting< object_map_dt, empty_object_map > | |
| ►Creference_counting< ref_expr_set_dt > | |
| Cref_expr_sett | |
| Cremove_asmt | |
| Cremove_calls_no_bodyt | |
| Cremove_const_function_pointerst | |
| Cremove_exceptionst | Lowers high-level exception descriptions into low-level operations suitable for symex and other analyses that don't understand the THROW or CATCH GOTO instructions |
| Cremove_function_pointerst | |
| Cremove_instanceoft | |
| Cremove_java_newt | |
| Cremove_returnst | |
| Cremove_virtual_functionst | |
| Crename_symbolt | |
| Csmt_bit_vector_theoryt::repeatt | |
| Creplace_callst | |
| Creplace_history_parametert | |
| ►Creplace_symbolt | Replace a symbol expression by a given expression |
| Ccasting_replace_symbolt | A variant of replace_symbolt that does not require types to match, but instead inserts type casts as needed when replacing one symbol by another |
| ►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 | |
| Cresponse_or_errort< smtt > | Holds either a valid parsed response or response sub-tree of type |
| Crestrictt | |
| Cincremental_goto_checkert::resultt | |
| Csimplify_exprt::resultt< T > | |
| Cmini_bdd_mgrt::reverse_keyt | |
| Csmt_bit_vector_theoryt::rotate_leftt | |
| Csmt_bit_vector_theoryt::rotate_rightt | |
| 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 |
| Csolver_hardnesst::sat_hardnesst | |
| Csave_scopet | |
| Cscope_treet | Tree to keep track of the destructors generated along each branch of a function |
| 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 |
| Cosx_mach_o_readert::sectiont | |
| Cselect_pointer_typet | |
| Csmt_array_theoryt::selectt | |
| Csmt2_incremental_decision_proceduret::sequencet | Generators of sequences of uniquely identifying numbers used for naming SMT functions introduced by the decision procedure |
| Csese_region_analysist | |
| Caddress_of_aware_replace_symbolt::set_require_lvalue_and_backupt | |
| Cshadow_memory_field_definitionst | The shadow memory field definitions |
| Cshadow_memory_statet | The state maintained by the shadow memory instrumentation during symbolic execution |
| Cshadow_memoryt | The shadow memory instrumentation performed during symbolic execution |
| Cshadow_memory_statet::shadowed_addresst | |
| Cshared_bufferst | |
| Cconcurrency_instrumentationt::shared_vart | |
| Csharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::sharing_map_statst | Stats about sharing between several sharing map instances |
| Csharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT > | A map implemented as a tree where subtrees can be shared between different maps |
| Csharing_mapt< dstringt, abstract_object_pointert > | |
| Csharing_mapt< dstringt, exprt > | |
| Csharing_mapt< exprt, symbol_exprt, false, irep_hash > | |
| Csharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash > | |
| Csharing_mapt< irep_idt, entryt > | |
| Csharing_mapt< irep_idt, std::pair< ssa_exprt, std::size_t > > | |
| Csharing_mapt< mp_integer, abstract_object_pointert, false, mp_integer_hasht > | |
| Csharing_nodet< keyT, valueT, equalT > | |
| Csharing_nodet< key_type, mapped_type > | |
| Csharing_treet< derivedt, named_subtreest > | Base class for tree-like data structures with sharing |
| ►Csharing_treet< irept, forward_list_as_mapt< irep_idt, irept > > | |
| ►Cirept | There are a large number of kinds of tree structured or tree-like data in CPROVER |
| 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 | |
| Ccar_exprt | Class that represents a normalized conditional address range, with: |
| Ccode_typet::parametert | |
| ►Ccodet | Data structure for representing an arbitrary statement in a program |
| ►Ccode_asmt | codet representation of an inline assembler statement |
| Ccode_asm_gcct | codet representation of an inline assembler statement, for the gcc flavor |
| Ccode_assertt | A non-fatal assertion, which checks a condition then permits execution to continue |
| Ccode_assignt | A goto_instruction_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 goto_instruction_codet representing the removal of a local variable going out of scope |
| Ccode_declt | A goto_instruction_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_frontend_assignt | A codet representing an assignment in the program |
| Ccode_frontend_declt | A codet representing the declaration of a local variable |
| Ccode_frontend_returnt | codet representation of a "return from a function" statement |
| Ccode_function_bodyt | This class is used to interface between a language frontend and goto-convert – it communicates the identifiers of the parameters of a function or method |
| Ccode_function_callt | goto_instruction_codet representation of a function call statement |
| Ccode_gcc_switch_case_ranget | codet representation of a switch-case, i.e. a case statement within a switch |
| Ccode_gotot | codet representation of a goto statement |
| Ccode_ifthenelset | codet representation of an if-then-else statement |
| Ccode_inputt | A goto_instruction_codet representing the declaration that an input of a particular description has a value which corresponds to the value of a given expression (or expressions) |
| 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_outputt | A goto_instruction_codet representing the declaration that an output of a particular description has a value which corresponds to the value of a given expression (or expressions) |
| 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 | goto_instruction_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 |
| Cconditional_target_exprt | Class that represents a single conditional target |
| Cconditional_target_group_exprt | A class for an expression that represents a conditional target or a list of targets sharing a common condition in an assigns clause |
| Ccpp_declarationt | |
| Ccpp_declaratort | |
| Ccpp_linkage_spect | |
| Ccpp_namespace_spect | |
| ►Cexpr_protectedt | Base class for all expressions |
| Calready_typechecked_exprt | |
| ►Cbinary_exprt | A base class for binary expressions |
| Callocate_exprt | |
| Callocate_state_exprt | |
| ►Cbinary_predicate_exprt | A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two arguments |
| ►Cbinary_overflow_exprt | A Boolean expression returning true, iff operation kind would result in an overflow when applied to operands lhs and rhs |
| Cminus_overflow_exprt | |
| Cmult_overflow_exprt | |
| Cplus_overflow_exprt | |
| Cshl_overflow_exprt | |
| ►Cbinary_relation_exprt | A base class for relations, i.e., binary predicates whose two operands have the same type |
| Cequal_exprt | Equality |
| Cgreater_than_exprt | Binary greater than operator expression |
| Cgreater_than_or_equal_exprt | Binary greater than or equal operator expression |
| Cieee_float_equal_exprt | IEEE-floating-point equality |
| Cieee_float_notequal_exprt | IEEE floating-point disequality |
| Cless_than_exprt | Binary less than operator expression |
| Cless_than_or_equal_exprt | Binary less than or equal operator expression |
| Cnotequal_exprt | Disequality |
| Cextractbit_exprt | Extracts a single bit of a bit-vector operand |
| Cjava_instanceof_exprt | |
| ►Cr_or_w_ok_exprt | A base class for a predicate that indicates that an address range is ok to read or write or both |
| Cr_ok_exprt | A predicate that indicates that an address range is ok to read |
| Cw_ok_exprt | A predicate that indicates that an address range is ok to write |
| Cstate_is_cstring_exprt | |
| Cstate_is_dynamic_object_exprt | |
| Cstate_live_object_exprt | |
| Cstate_writeable_object_exprt | |
| ►Cbinding_exprt | A base class for variable bindings (quantifiers, let, lambda) |
| Carray_comprehension_exprt | Expression to define a mapping from an argument (index) to elements |
| Clambda_exprt | A (mathematical) lambda expression |
| ►Cquantifier_exprt | A base class for quantifier expressions |
| Cexists_exprt | An exists expression |
| Cforall_exprt | A forall expression |
| Cbyte_extract_exprt | Expression of type type extracted from some object op starting at position offset (given in number of bytes) |
| Ccomplex_exprt | Complex constructor from a pair of numbers |
| Cconstant_interval_exprt | Represents an interval of values |
| Ccpp_static_assertt | |
| Cdeallocate_state_exprt | |
| Cdiv_exprt | Division |
| Cdynamic_object_exprt | Representation of heap-allocated objects |
| Celement_address_exprt | Operator to return the address of an array element relative to a base address |
| Center_scope_state_exprt | |
| Ceuclidean_mod_exprt | Boute's Euclidean definition of Modulo – to match SMT-LIB2 |
| Cevaluate_exprt | |
| Cevaluate_exprt | |
| Cexit_scope_state_exprt | |
| 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 |
| Clet_exprt | A let expression |
| Cminus_exprt | Binary minus |
| Cmod_exprt | Modulo defined as lhs-(rhs * truncate(lhs/rhs)) |
| Cnamed_term_exprt | Expression that introduces a new symbol that is equal to the operand |
| Cobject_descriptor_exprt | Split an expression into a base object and a (byte) offset |
| Cpower_exprt | Exponentiation |
| Creplication_exprt | Bit-vector replication |
| Csaturating_minus_exprt | Saturating subtraction expression |
| Csaturating_plus_exprt | The saturating plus expression |
| ►Cshift_exprt | A base class for shift and rotate operators |
| Cashr_exprt | Arithmetic right shift |
| Clshr_exprt | Logical right shift |
| Cshl_exprt | Left shift |
| Cstate_cstrlen_exprt | |
| Cstate_object_size_exprt | |
| Cstate_type_compatible_exprt | |
| Cextractbits_exprt | Extracts a sub-range of a bit-vector operand |
| Cindex_designatort | |
| 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 |
| Cbitxnor_exprt | Bit-wise XNOR |
| 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 |
| Cseparate_exprt | A predicate that indicates that the objects pointed to are distinct |
| Cshuffle_vector_exprt | Shuffle elements of one or two vectors, modelled after Clang's __builtin_shufflevector |
| Cstate_is_sentinel_dll_exprt | |
| ►Cstruct_exprt | Struct constructor from list of elements |
| Crefined_string_exprt | |
| Ctuple_exprt | |
| Cvector_exprt | Vector constructor from list of elements |
| Cxor_exprt | Boolean XOR |
| Cnondet_padding_exprt | This expression serves as a placeholder for the bits which have non deterministic value in a larger bit vector |
| ►Cnullary_exprt | An expression without operands |
| Cansi_c_declaratort | |
| Cclass_method_descriptor_exprt | An expression describing a method on a class |
| ►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 |
| Cempty_union_exprt | Union constructor to support unions without any member (a GCC/Clang feature) |
| Cinfinity_exprt | An expression denoting infinity |
| Cliteral_vector_exprt | |
| Cmax_value_exprt | +∞ upper bound for intervals |
| Cmin_value_exprt | -∞ upper bound for intervals |
| Cnil_exprt | The NIL expression |
| Cnondet_symbol_exprt | Expression to hold a nondeterministic choice |
| Cobject_address_exprt | Operator to return the address of an object |
| 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 |
| Coverflow_result_exprt | An expression returning both the result of the arithmetic operation under wrap-around semantics as well as a Boolean to signify overflow |
| ►Cpredicate_exprt | A base class for expressions that are predicates, i.e., Boolean-typed |
| Cliteral_exprt | |
| Cprophecy_pointer_in_range_exprt | Pointer_in_range (see pointer_in_range_exprt) with prophecy expressions to encode whether a pointer refers to a deallocated or out-of-scope object |
| ►Cprophecy_r_or_w_ok_exprt | A base class for a predicate that indicates that an address range is ok to read or write or both |
| Cprophecy_r_ok_exprt | A predicate that indicates that an address range is ok to read |
| Cprophecy_w_ok_exprt | A predicate that indicates that an address range is ok to write |
| ►Cternary_exprt | An expression with three operands |
| Callocate_exprt | |
| Cbyte_update_exprt | Expression corresponding to op() where the bytes starting at position offset (given in number of bytes) have been updated with value |
| Cieee_float_op_exprt | IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2) |
| Cif_exprt | The trinary if-then-else operator |
| Cpointer_in_range_exprt | Pointer_in_range(a, b, c) evaluates to true iff same_object(a, b, c) ∧ r_ok(a, offset(c)-offset(a)) ∧ a<=b ∧ b<=c Note that the last inequality is weak, i.e., b may be equal to c |
| Creallocate_exprt | |
| Creallocate_state_exprt | |
| Cstate_ok_exprt | |
| Ctranst | Transition system, consisting of state invariant, initial state predicate, and transition predicate |
| Cupdate_exprt | Operator to update elements in structs and arrays |
| Cupdate_state_exprt | |
| Cupdate_state_exprt | |
| ►Cunary_exprt | Generic base class for unary expressions |
| Cabs_exprt | Absolute value |
| Caddress_of_exprt | Operator to return the address of an object |
| Cannotated_pointer_constant_exprt | Pointer-typed bitvector constant annotated with the pointer expression that the bitvector is the numeric representation of |
| Carray_of_exprt | Array constructor from single element |
| Cbit_cast_exprt | Reinterpret the bits of an expression of type S as an expression of type T where S and T have the same size |
| Cbitnot_exprt | Bit-wise negation of bit-vectors |
| Cbitreverse_exprt | Reverse the order of bits in a bit-vector |
| 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 |
| Ccount_leading_zeros_exprt | The count leading zeros (counting the number of zero bits starting from the most-significant bit) expression |
| Ccount_trailing_zeros_exprt | The count trailing zeros (counting the number of zero bits starting from the least-significant bit) expression |
| Ccstrlen_exprt | An expression, akin to ISO C's strlen, that denotes the length of a zero-terminated string that starts at the given address |
| Cdereference_exprt | Operator to dereference a pointer |
| Cfield_address_exprt | Operator to return the address of a field relative to a base address |
| Cfind_first_set_exprt | Returns one plus the index of the least-significant one bit, or zero if the operand is zero |
| Chistory_exprt | A class for an expression that indicates a history variable |
| Cmember_exprt | Extract member of struct or union |
| Cnot_exprt | Boolean negation |
| Cobject_size_exprt | Expression for finding the size (in bytes) of the object a pointer points to |
| Cpointer_object_exprt | A numerical identifier for the object a pointer points to |
| Cpointer_offset_exprt | The offset (in bytes) of a pointer relative to the object |
| 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 |
| Cenum_is_in_range_exprt | A Boolean expression returning true, iff the value of an enum-typed symbol equals one of the enum's declared values |
| Cinitial_state_exprt | |
| Cis_cstring_exprt | A predicate that indicates that a zero-terminated string starts at the given address |
| Cis_dynamic_object_exprt | Evaluates to true if the operand is a pointer to a dynamic object |
| Cis_invalid_pointer_exprt | |
| 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 |
| Clive_object_exprt | A predicate that indicates that the object pointed to is live |
| Conehot0_exprt | A Boolean expression returning true iff the given operand consists of exactly one '0' and '1' otherwise |
| Conehot_exprt | A Boolean expression returning true iff the given operand consists of exactly one '1' and '0' otherwise |
| Csign_exprt | Sign of an expression Predicate is true if _op is negative, false otherwise |
| ►Cunary_overflow_exprt | A Boolean expression returning true, iff operation kind would result in an overflow when applied to the (single) operand |
| Cunary_minus_overflow_exprt | A Boolean expression returning true, iff negation would result in an overflow when applied to the (single) operand |
| Cwriteable_object_exprt | A predicate that indicates that the object pointed to is writeable |
| Cunion_exprt | Union constructor from single element |
| Czero_extend_exprt | Zero extension The operand is converted to the given type by either a) truncating if the new type is shorter, or b) padding with most-significant zero bits if the new type is larger, or c) reinterprets the operand as the given type if their widths match |
| Cupdate_bit_exprt | Replaces a sub-range of a bit-vector operand |
| Cupdate_bits_exprt | Replaces a sub-range of a bit-vector operand |
| Cwith_exprt | Operator to update elements in structs and arrays |
| Cfield_sensitive_ssa_exprt | |
| 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 |
| Cjava_string_literal_exprt | |
| ►Cside_effect_exprt | An expression containing a side effect |
| Cside_effect_expr_assignt | A side_effect_exprt that performs an assignment |
| 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_overflowt | A Boolean expression returning true, iff the result of performing operation kind on operands a and b in infinite-precision arithmetic cannot be represented in the type of the object that result points to (or the type of result, if it is not a pointer) |
| Cside_effect_expr_statement_expressiont | A side_effect_exprt that contains a statement |
| 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 | |
| Cjava_annotationt | |
| Cjava_annotationt::valuet | |
| Cjava_class_typet::java_lambda_method_handlet | Represents a lambda call to a method |
| Cmerged_irept | |
| ►Csmt_check_sat_response_kindt | |
| Csmt_sat_responset | |
| Csmt_unknown_responset | |
| Csmt_unsat_responset | |
| ►Csmt_commandt | |
| Csmt_assert_commandt | |
| Csmt_check_sat_commandt | |
| Csmt_declare_function_commandt | |
| Csmt_define_function_commandt | |
| Csmt_exit_commandt | |
| Csmt_get_value_commandt | |
| Csmt_pop_commandt | |
| Csmt_push_commandt | |
| Csmt_set_logic_commandt | |
| Csmt_set_option_commandt | |
| Csmt_get_value_responset::valuation_pairt | |
| ►Csmt_indext | For implementation of indexed identifiers |
| Csmt_numeral_indext | |
| Csmt_symbol_indext | |
| Csmt_logict | |
| ►Csmt_optiont | |
| Csmt_option_produce_modelst | |
| ►Csmt_responset | |
| Csmt_check_sat_responset | |
| Csmt_error_responset | |
| Csmt_get_value_responset | |
| Csmt_success_responset | |
| Csmt_unsupported_responset | |
| ►Csmt_sortt | |
| Csmt_array_sortt | |
| Csmt_bit_vector_sortt | |
| Csmt_bool_sortt | |
| ►Csmt_termt | |
| Csmt_bit_vector_constant_termt | |
| Csmt_bool_literal_termt | |
| Csmt_exists_termt | |
| Csmt_forall_termt | |
| Csmt_function_application_termt | |
| Csmt_identifier_termt | Stores identifiers in unescaped and unquoted form |
| 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 |
| ►Cinteger_bitvector_typet | Fixed-width bit-vector representing a signed or unsigned integer |
| Csignedbv_typet | Fixed-width bit-vector with two's complement interpretation |
| Cunsignedbv_typet | Fixed-width bit-vector with unsigned binary 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 | Reference that points to a java_generic_parameter_tagt |
| Cjava_generic_typet | Reference that points to a java_generic_struct_tag_typet |
| Cjava_reference_typet | This is a specialization of reference_typet |
| Cbool_typet | The Boolean type |
| ►Ccode_typet | Base type of functions |
| Ccode_with_contract_typet | |
| Cjava_method_typet | |
| Ccpp_enum_typet | |
| Cempty_typet | The empty type |
| 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) |
| Crange_typet | A type for subranges of integers |
| Crational_typet | Unbounded, signed rational numbers |
| Creal_typet | Unbounded, signed real numbers |
| Cstate_typet | |
| Cstate_typet | |
| 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 |
| ►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_or_union_tag_typet | A struct or union tag type |
| ►Cstruct_tag_typet | A struct tag type, i.e., struct_typet with an identifier |
| Cjava_generic_parameter_tagt | Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T> |
| Cjava_generic_struct_tag_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) |
| Cunion_tag_typet | A union tag type, i.e., union_typet with an identifier |
| Ctemplate_parameter_symbol_typet | Template parameter symbol that is a type |
| 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 |
| Calready_typechecked_typet | |
| Carray_typet | Arrays with given size |
| Cc_enum_typet | The type of C enums |
| Ccomplex_typet | Complex numbers made of pair of given subtype |
| Cvector_typet | The vector type |
| Ctypedef_typet | A typedef |
| Cuninitialized_typet | |
| Csmt_bit_vector_theoryt::shift_leftt | |
| Cshow_goto_functions_jsont | |
| Cshow_goto_functions_xmlt | |
| Csmt_bit_vector_theoryt::sign_extendt | |
| Csmt2_parsert::signature_with_parameter_idst | |
| Csmt_bit_vector_theoryt::signed_dividet | |
| Csmt_bit_vector_theoryt::signed_greater_than_or_equalt | |
| Csmt_bit_vector_theoryt::signed_greater_thant | |
| Csmt_bit_vector_theoryt::signed_less_than_or_equalt | |
| Csmt_bit_vector_theoryt::signed_less_thant | |
| Csmt_bit_vector_theoryt::signed_remaindert | |
| 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_n_way_pointee_baset< N, Num > | |
| Cd_containert< keyT, valueT, equalT > | |
| Cd_internalt< keyT, valueT, equalT > | |
| Cd_leaft< keyT, valueT, equalT > | |
| Csmall_shared_n_way_ptrt< Ts > | This class is similar to small_shared_ptrt and boost's intrusive_ptr |
| Csmall_shared_n_way_ptrt< d_containert< keyT, valueT, equalT >, d_leaft< keyT, valueT, equalT >, d_internalt< keyT, valueT, equalT > > | |
| Csmall_shared_pointeet< Num > | A helper class to store use-counts of objects held by small shared pointers |
| 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 |
| Csmt2_tokenizert::smt2_errort | |
| Csmt2_format_containert< T > | |
| Csmt2_parser_test_resultt | |
| ►Csmt2_parsert | |
| Csmt2_solvert | |
| ►Csmt2_stringstreamt | |
| Csmt2_dect | Decision procedure interface for various SMT 2.x solvers |
| ►Csmt2_tokenizert | |
| Csmt2irept | |
| Csmt_array_theoryt | |
| ►Csmt_base_solver_processt | |
| Csmt_incremental_dry_run_solvert | Class for an incremental SMT solver used in combination with --outfile argument where the solver is never run |
| Csmt_piped_solver_processt | |
| Csmt_bit_vector_theoryt | |
| ►Csmt_command_const_downcast_visitort | |
| Csmt_command_to_string_convertert | |
| Csmt_command_functiont | A function generated from a command |
| Csmt_core_theoryt | |
| ►Csmt_index_const_downcast_visitort | |
| Csmt_index_output_visitort | |
| Csmt_is_dynamic_objectt | Specifics of how the dynamic object status lookup is implemented in SMT terms |
| ►Csmt_logic_const_downcast_visitort | |
| Csmt_logic_to_string_convertert | |
| Csmt_object_sizet | Specifics of how the object size lookup is implemented in SMT terms |
| ►Csmt_option_const_downcast_visitort | |
| Csmt_option_to_string_convertert | |
| ►Csmt_sort_const_downcast_visitort | |
| Csmt_sort_output_visitort | |
| Csort_based_cast_to_bit_vector_convertert | |
| Csort_based_literal_convertert | |
| ►Csmt_term_const_downcast_visitort | |
| Csmt_term_to_string_convertert | |
| Cvalue_expr_from_smt_factoryt | |
| Csolver_factoryt | |
| Csolver_optionst | |
| Csolver_progresst | |
| ►Csolver_resource_limitst | |
| Cprop_conv_solvert | |
| Csolver_factoryt::solvert | |
| Csorted_variablest | |
| Csource_linest | |
| Cmemory_snapshot_harness_generatort::source_location_matcht | Wraps the information for source location match candidates |
| 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 > | |
| ►CSSA_stept | Single SSA step in the equation |
| CSSA_assignment_stept | |
| Cinterpretert::stack_framet | |
| Cjava_bytecode_parse_treet::methodt::stack_map_table_entryt | |
| Cstate_encodingt | |
| Ccheck_call_sequencet::state_hash | |
| Cstatement_list_parse_treet | Intermediate representation of a parsed Statement List file before converting it into a goto program |
| Ccheck_call_sequencet::statet | |
| Chelp_formattert::statet | |
| Cnfat< T >::statet | A state is a set of possibly active transitions |
| Cstatic_verifier_resultt | The result of verifying a single assertion As well as the status of the assertion (see above), it also contains the location (source_location and function_id) and the set of histories in which the assertion is unknown or false, so that more detailed post-processing or error output can be done |
| Cclauset::stept | |
| Cstatement_list_typecheckt::stl_jump_locationt | Holds information about the properties of a jump instruction |
| Cstatement_list_typecheckt::stl_label_locationt | Holds information about the instruction and the nesting depth to which a label points |
| Csmt_check_sat_response_kindt::storert< derivedt > | Class for adding the ability to up and down cast smt_check_sat_response_kindt to and from irept |
| Csmt_indext::storert< derivedt > | Class for adding the ability to up and down cast smt_indext to and from irept |
| Csmt_logict::storert< derivedt > | Class for adding the ability to up and down cast smt_logict to and from irept |
| Csmt_optiont::storert< derivedt > | Class for adding the ability to up and down cast smt_optiont to and from irept |
| Csmt_sortt::storert< derivedt > | Class for adding the ability to up and down cast smt_sortt to and from irept |
| ►Csmt_termt::storert< derivedt > | Class for adding the ability to up and down cast smt_termt to and from irept |
| Csmt_declare_function_commandt | |
| ►Csmt_termt::storert< smt_assert_commandt > | |
| Csmt_assert_commandt | |
| Csmt_get_value_commandt | |
| ►Csmt_check_sat_response_kindt::storert< smt_check_sat_responset > | |
| Csmt_check_sat_responset | |
| ►Csmt_sortt::storert< smt_declare_function_commandt > | |
| Csmt_declare_function_commandt | |
| ►Csmt_termt::storert< smt_define_function_commandt > | |
| Csmt_define_function_commandt | |
| ►Csmt_termt::storert< smt_get_value_responset > | |
| Csmt_get_value_responset | |
| ►Csmt_indext::storert< smt_identifier_termt > | |
| Csmt_identifier_termt | Stores identifiers in unescaped and unquoted form |
| ►Csmt_logict::storert< smt_set_logic_commandt > | |
| Csmt_set_logic_commandt | |
| ►Csmt_optiont::storert< smt_set_option_commandt > | |
| Csmt_set_option_commandt | |
| ►Csmt_sortt::storert< smt_termt > | |
| Csmt_termt | |
| ►Csmt_termt::storert< valuation_pairt > | |
| Csmt_get_value_responset::valuation_pairt | |
| Csmt_array_theoryt::storet | |
| Cstring_abstractiont | Replace all uses of char * by a struct that carries that string, and also the underlying allocation and the C string length |
| 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_format_builtin_functiont | Built-in function for String.format() |
| ►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_container_statisticst | Has estimated statistics about string container (estimated because this only uses public information, which disregards any internal control structures that might be in use) |
| Cstring_containert | |
| Cstring_dependenciest | Keep track of dependencies between strings |
| Cstring_hash | |
| Cstring_instrumentationt | |
| 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 | |
| Cstruct_aggregate_typet | |
| Cstruct_encodingt | Encodes struct types/values into non-struct expressions/types |
| Cstructured_data_entryt | |
| Cstructured_datat | A way of representing nested key/value data |
| ►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 | |
| Csmt_bit_vector_theoryt::subtractt | |
| 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/removedA caller can pass a journalling_symbol_tablet into a callee that is expected to mutate it somehow, then after it has run inspect the recording table's journal to determine what has changed more cheaply than examining every symbol |
| Csymbol_table_buildert | Author: Diffblue Ltd |
| Csymbol_tablet | The symbol table |
| ►Csymbolt | Symbol table entry |
| 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_assignt | Functor for symex assignment |
| Csymex_complexity_limit_exceeded_actiont | Default heuristic transformation that cancels branches when complexity has been breached |
| Csymex_configt | Configuration used for a symbolic execution |
| Csymex_coveraget | |
| 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_nondet_generatort | Functor generating fresh nondet symbols |
| 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, empty >::dt | |
| Ctaint_analysist | |
| Ctaint_parse_treet | |
| Ctake_time_resourcet | |
| Cgoto_programt::instructiont::target_less_than | A total order over targett and const_targett |
| Cjava_bytecode_convert_methodt::method_with_amapt::target_less_than | |
| Cgoto_convertt::targetst | |
| Cgrapht< N >::tarjant | |
| Ctdefl_compressor | |
| Ctdefl_output_buffer | |
| Ctdefl_sym_freq | |
| Ctemp_dirt | |
| Ctemplate_mapt | |
| Ctemporary_filet | |
| Cmonomialt::termt | |
| Ctest_inputst | |
| Cconcurrency_instrumentationt::thread_local_vart | |
| Cgoto_symex_statet::threadt | |
| Cgoto_convertt::throw_targett | |
| ►Cstatement_list_parse_treet::tia_modulet | Base element of all modules in the Totally Integrated Automation (TIA) portal by Siemens |
| Cstatement_list_parse_treet::function_blockt | Structure for a simple function block in Statement List |
| Cstatement_list_parse_treet::functiont | Structure for a simple function in Statement List |
| ►Ctimestampert | Timestamp class hierarchy |
| Cmonotonic_timestampert | |
| Cwall_clock_timestampert | |
| Ctinfl_decompressor_tag | |
| Ctinfl_huff_table | |
| Cto_be_merged_irep_hash | |
| Ctrace_automatont | |
| Ctrace_optionst | Options for printing the trace using show_goto_trace |
| Cpropertyt::trace_statet | |
| Cpropertyt::trace_updatet | |
| Cnfat< T >::transitiont | |
| ►Cstd::true_type | |
| Csmt_function_application_termt::has_indicest< functiont, std::void_t< decltype(std::declval< functiont >().indices())> > | |
| Ctvt | |
| Clocal_safe_pointerst::type_comparet | Comparator that regards type-equal expressions as equal, and otherwise uses the natural (operator<) ordering on irept |
| 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 | |
| ►Cunderlyingt | |
| Crenamedt< underlyingt, level > | Wrapper for expressions or types which have been renamed up to a given level |
| Cunified_difft | |
| Cuninitializedt | |
| Cunion_aggregate_typet | |
| Cunion_find< T, hasht > | |
| Cunion_find< exprt, irep_hash > | |
| 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_bvt::unpacked_floatt | |
| Cfloat_bvt::biased_floatt | |
| Cfloat_bvt::unbiased_floatt | |
| ►Cfloat_utilst::unpacked_floatt | |
| Cfloat_utilst::biased_floatt | |
| Cfloat_utilst::unbiased_floatt | |
| Csmt_bit_vector_theoryt::unsigned_dividet | |
| Csmt_bit_vector_theoryt::unsigned_greater_than_or_equalt | |
| Csmt_bit_vector_theoryt::unsigned_greater_thant | |
| Csmt_bit_vector_theoryt::unsigned_less_than_or_equalt | |
| Csmt_bit_vector_theoryt::unsigned_less_thant | |
| Csmt_bit_vector_theoryt::unsigned_remaindert | |
| Cunsigned_union_find | |
| Cgoto_unwindt::unwind_logt | |
| Cunwindsett | |
| ►Cvalue_range_implementationt | |
| Cempty_value_ranget | |
| Csingle_value_value_ranget | |
| Cvalue_set_value_ranget | |
| Cvalue_range_iteratort | |
| Cvalue_ranget | |
| Cvalue_set_dereferencet | Wrapper for a function dereferencing pointer expressions using a value set |
| Cvalue_set_evaluator | |
| Cvalue_set_fit | |
| ►Cvalue_set_tag | |
| Cvalue_set_abstract_objectt | |
| Cvalue_set_pointer_abstract_objectt | |
| ►Cvalue_setst | |
| Cvalue_set_analysis_fit | |
| Cvalue_set_analysis_templatet< VSDT > | This template class implements a data-flow analysis which keeps track of what values different variables might have at different points in the program |
| 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 |
| Cstatement_list_parse_treet::var_declarationt | Struct for a single variable declaration in Statement List |
| Cmini_bdd_mgrt::var_table_entryt | |
| Cvariable_sensitivity_object_factoryt | |
| Cjava_bytecode_convert_methodt::variablet | |
| Cshared_bufferst::varst | |
| ►Cstd::vector< T > | STL class |
| Ccall_stackt | |
| Clispexprt | |
| Cirep_hash_container_baset::vector_hasht | |
| Ccustom_bitvector_domaint::vectorst | |
| Cverification_resultt::verification_result_implt | |
| Cverification_resultt | |
| Cjava_bytecode_parse_treet::methodt::verification_type_infot | |
| Cconfigt::verilogt | |
| Cvs_dep_edget | |
| Cvsd_configt | |
| Cw_guardst | |
| Cwidened_ranget | |
| ►Cwitness_providert | An implementation of incremental_goto_checkert may implement this interface to provide GraphML witnesses |
| Cmulti_path_symex_checkert | Performs a multi-path symbolic execution using goto-symex and calls a SAT/SMT solver to check the status of the properties |
| Csingle_loop_incremental_symex_checkert | Performs a multi-path symbolic execution using goto-symex that incrementally unwinds a given loop and calls a SAT/SMT solver to check the status of the properties after each iteration |
| Csingle_path_symex_checkert | Uses goto-symex to symbolically execute each path in the goto model and calls a solver to find property violations |
| Cworkt | |
| ►Cwrite_stack_entryt | |
| Coffset_entryt | |
| Csimple_entryt | |
| Cwrite_stackt | |
| Cxml_edget | |
| Cxml_parse_treet | |
| Cxmlt | |
| Csmt_bit_vector_theoryt::xnort | |
| Csmt_bit_vector_theoryt::xort | |
| Csmt_core_theoryt::xort | |
| Csmt_bit_vector_theoryt::zero_extendt | |
| Czip_iteratort< first_iteratort, second_iteratort, same_size > | Zip two ranges to make a range of pairs |
1.9.1