C__CPROVER_jsa_abstract_heap | |
C__CPROVER_jsa_abstract_node | Abstract nodes may assume any of a set of pre-defined values (value_ref to abstract_ranget) |
C__CPROVER_jsa_abstract_range | Set of pre-defined, possible values for abstract nodes |
C__CPROVER_jsa_concrete_node | Concrete node with explicit value |
C__CPROVER_jsa_iterator | Iterators point to a node and give the relative index within that node |
C__CPROVER_pipet | |
Cpartial_order_concurrencyt::a_rect | |
►Cabstract_goto_modelt | Abstract interface to eager or lazy GOTO models |
Cgoto_modelt | |
Clazy_goto_modelt | A GOTO model that produces function bodies on demand |
Cwrapper_goto_modelt | Class providing the abstract GOTO model interface onto an unrelated symbol table and goto_functionst |
Cacceleratet | |
Cacceleration_utilst | |
Cframet::active_loop_infot | |
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< 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< domainT > | Base class for concurrency-aware abstract interpretation |
►Cait< constant_propagator_domaint > | |
Cconstant_propagator_ait | |
►Cait< custom_bitvector_domaint > | |
Ccustom_bitvector_analysist | |
►Cait< dep_graph_domaint > | |
Cdependence_grapht | |
►Cait< escape_domaint > | |
Cescape_analysist | |
►Cait< global_may_alias_domaint > | |
Cglobal_may_alias_analysist | This is a may analysis (i.e |
►Cait< invariant_set_domaint > | |
Cinvariant_propagationt | |
►Cait< rd_range_domaint > | |
►Cconcurrency_aware_ait< rd_range_domaint > | |
Creaching_definitions_analysist | |
Cait< uninitialized_domaint > | |
►Cai_domain_baset | The interface offered by a domain, allows code to manipulate domains without knowing their exact type |
Cconstant_propagator_domaint | |
Ccustom_bitvector_domaint | |
Cdep_graph_domaint | |
Cescape_domaint | |
Cglobal_may_alias_domaint | |
Cinterval_domaint | |
Cinvariant_set_domaint | |
Cis_threaded_domaint | |
Crd_range_domaint | Because the class is inherited from ai_domain_baset , its instance represents an element of a domain of the reaching definitions abstract interpretation analysis |
Cuninitialized_domaint | |
►Cai_domain_factory_baset | |
►Cai_domain_factoryt< domainT > | |
Cai_domain_factory_default_constructort< domainT > | |
►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< 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_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 |
Cjava_bytecode_parse_treet::annotationt | |
Cansi_c_identifiert | |
Cansi_c_parse_treet | |
Cansi_c_scopet | |
Cconfigt::ansi_ct | |
Cbv_refinementt::approximationt | |
Cgoto_cc_cmdlinet::argt | |
Carrayst::array_equalityt | |
Carray_poolt | Correspondance between arrays and pointers string representations |
Csolver_hardnesst::assertion_statst | |
Cassignmentt | Assignment from the rhs value to the lhs variable |
Cautomatont | |
Cbase_type_eqt | |
►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_managert | Manager for BDD creation |
Cbdd_nodet | Low level access to the structure of the BDD, read-only |
Cbddt | Logical operations on BDDs |
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 | |
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_storage_spect | |
Cc_test_input_generatort | |
►Cc_typecastt | |
Ccpp_typecastt | |
Ccall_checkt< Base, T > | |
Ccall_grapht | A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection |
Ccall_stack_historyt::call_stack_entryt | |
Ccheck_call_sequencet::call_stack_entryt | |
Ccall_validate_fullt< Base, T > | |
Ccall_validatet< Base, T > | |
Cgoto_program2codet::caset | |
Ccbmc_invariants_should_throwt | Helper to enable invariant throwing as above bounded to an object lifetime: |
Ccfg_dominators_templatet< P, T, post_dom > | Dominator graph |
Ccfg_dominators_templatet< const goto_programt, goto_programt::const_targett, false > | |
Ccfg_dominators_templatet< goto_programt, goto_programt::targett, false > | |
Ccfg_dominators_templatet< P, T, false > | |
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 | |
Cclass_hierarchyt | Non-graph-based representation of the class hierarchy |
Cmethod_bytecodet::class_method_and_bytecodet | Pair of class id and methodt |
Cjava_class_loader_baset::classpath_entryt | An entry in the classpath |
Cjava_bytecode_parse_treet::classt | |
Cclauset | |
Cescape_domaint::cleanupt | |
►Ccmdlinet | |
Cfree_form_cmdlinet | An implementation of cmdlinet to be used in tests |
►Cgoto_cc_cmdlinet | |
Carmcc_cmdlinet | |
Cas86_cmdlinet | |
Cas_cmdlinet | |
Cbcc_cmdlinet | |
Cgcc_cmdlinet | |
Cld_cmdlinet | |
Cms_cl_cmdlinet | |
Cms_link_cmdlinet | |
Ccode_contractst | |
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 |
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 |
Ccomplexity_limitert | Symex complexity module |
►Ccomponentt | |
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 |
Cconcurrency_instrumentationt | |
Cgoto_checkt::conditiont | |
Ccone_of_influencet | |
►Cbv_refinementt::configt | |
►Cbv_refinementt::infot | |
Cstring_refinementt::infot | String_refinementt constructor arguments |
►Cstring_refinementt::configt | |
Cstring_refinementt::infot | String_refinementt constructor arguments |
Cconfigt | Globally accessible architectural configuration |
►Cconflict_providert | |
►Cprop_conv_solvert | |
►Cequalityt | |
►Carrayst | |
►Cboolbvt | |
►Cbv_pointerst | |
Cbv_dimacst | |
Cbv_minimizing_dect | |
►Cbv_refinementt | |
Cstring_refinementt | |
►Cconst_expr_visitort | |
Creturn_value_visitort | Predicate to be used with the exprt::visit() function |
Csmall_mapt< T, Ind, Num >::const_iterator | Const iterator |
Cconst_target_hash | |
Csmall_mapt< T, Ind, Num >::const_value_iterator | Const value iterator |
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 |
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_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 |
Cfunction_pointer_restrictionst::invalid_restriction_exceptiont | |
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 |
Cincorrect_source_program_exceptiont | |
Cinvalid_command_line_argument_exceptiont | Thrown when users pass incorrect command line arguments, for example passing no files to analysis or setting two mutually exclusive flags |
Cinvalid_source_file_exceptiont | Thrown when we can't handle something in an input source file |
Csmt2_tokenizert::smt2_errort | |
Csystem_exceptiont | Thrown when some external system fails unexpectedly |
Cunsupported_operation_exceptiont | Thrown when we encounter an instruction, parameters to an instruction etc |
Cuser_input_error_exceptiont | |
Ccprover_library_entryt | |
Cevent_grapht::critical_cyclet | |
Cdata | |
Cdata_dpt | |
Cdatat | |
►Cdecision_proceduret | |
►Cstack_decision_proceduret | |
►Cprop_convt | |
Cprop_conv_solvert | |
►Csmt2_convt | |
Csmt2_dect | Decision procedure interface for various SMT 2.x solvers |
Cdefault_trace_stept | |
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 | |
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 |
Cdestructor_treet | Tree to keep track of the destructors generated along each branch of a function |
Cdestructt< I, pointee_baset, Ts > | |
Cdestructt< 0, pointee_baset, Ts... > | |
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 | |
Cdjb_manglert | Mangle identifiers by hashing their working directory with djb2 hash |
Cdocument_propertiest::doc_claimt | |
Cdocument_propertiest | |
Cdoes_remove_constt | |
►Cdomain_baset | |
Cvalue_set_domain_templatet< VST > | This is the domain for a value set analysis |
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 | |
►Cendianness_mapt | Maps a big-endian offset to a little-endian offset |
Cbv_endianness_mapt | Map bytes according to the configured endianness |
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 |
Cinv_object_storet::entryt | |
Crw_set_baset::entryt | |
Cclass_hierarchyt::entryt | |
Cdesignatort::entryt | |
Cvalue_sett::entryt | Represents a row of a value_sett |
Cvalue_set_fit::entryt | |
Cvalue_set_fivrt::entryt | |
Cvalue_set_fivrnst::entryt | |
Cboolbv_widtht::entryt | |
Cenumerating_loop_accelerationt | |
Cprintf_formattert::eol_exceptiont | |
Cmessaget::eomt | |
Cequation_symbol_mappingt | Maps equation to expressions contained in them and conversely expressions to equations that contain them |
Cevent_grapht | |
►Cstd::exception | STL class |
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 | |
Cexpr2jsilt | |
Cexpr2stlt | Class for saving the internal state of the conversion process |
Cdetail::expr_dynamic_cast_return_typet< Ret, T > | |
Cexpr_initializert< nondet > | |
Cexpr_queryt< T > | Wrapper for optionalt<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 | |
►Cfalse_type | |
Cdetail::always_falset< T > | |
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 | |
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 |
Cfixed_keys_map_wrappert< mapt > | |
Cfixedbv_spect | |
Cfixedbvt | |
Cflag_resett | Set a Boolean flag to a new value (via set_flag ) and restore the previous value when the entire object goes out of scope |
Clocal_bitvector_analysist::flagst | |
Cfloat_bvt | |
►Cfloat_utilst | |
Cfloat_approximationt | |
►Cflow_insensitive_abstract_domain_baset | |
Cvalue_set_domain_fit | |
Cvalue_set_domain_fivrnst | |
Cvalue_set_domain_fivrt | |
►Cflow_insensitive_analysis_baset | |
Cflow_insensitive_analysist< T > | |
►Cflow_insensitive_analysist< value_set_domain_fit > | |
Cvalue_set_analysis_fit | |
►Cflow_insensitive_analysist< value_set_domain_fivrnst > | |
Cvalue_set_analysis_fivrnst | |
►Cflow_insensitive_analysist< value_set_domain_fivrt > | |
Cvalue_set_analysis_fivrt | |
Cformat_containert< T > | The below enables convenient syntax for feeding objects into streams, via stream << format(o) |
Cformat_elementt | |
Cformat_specifiert | 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 |
Cframet | Stack frames – these are used for function calls and for exceptions |
Cfreert | A functor wrapping std::free |
Cfull_slicert | |
Cinterpretert::function_assignments_contextt | |
Cinterpretert::function_assignmentt | |
Cfunction_filterst | A collection of function filters to be applied in conjunction |
Cfunction_indicest | Helper class that maintains a map from function name to grapht node index and adds nodes to the graph on demand |
Cfunctionst::function_infot | |
Cfunction_modifiest | |
Cfunction_name_manglert< MangleFun > | Mangles the names in an entire program and its symbol table |
Cfunction_pointer_restrictionst | |
Cfunctionst | |
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_filterst | A collection of goal filters to be applied in conjunction |
Ccover_goalst::goalt | |
Cgoto_symex_property_decidert::goalt | |
Cgoto_checkt | |
►Cgoto_difft | |
Cjava_syntactic_difft | |
Csyntactic_difft | |
Cgoto_functionst | A collection of goto functions |
Cgoto_functiont | A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers) |
Cgoto_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_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 |
►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 |
Cvisited_nodet< E > | A node type with an extra bit |
►Cgraph_nodet< dep_edget > | |
Cdep_nodet | |
►Cgraph_nodet< edge_with_callsitest > | |
Ccall_grapht::function_nodet | Node of the directed graph representation of this call graph |
►Cgraph_nodet< empty_edget > | |
Cabstract_eventt | |
Ccfg_base_nodet< T, I > | |
Cclass_hierarchy_graph_nodet | Class hierarchy graph node: simply contains a class identifier |
Cdestructor_treet::destructor_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< nodet, goto_programt::const_targett > > | |
►Ccfg_baset< nodet, const goto_programt, goto_programt::const_targett > | |
Cprocedure_local_cfg_baset< nodet, const goto_programt, goto_programt::const_targett > | |
►Cgrapht< cfg_base_nodet< nodet, goto_programt::targett > > | |
►Ccfg_baset< nodet, goto_programt, goto_programt::targett > | |
Cprocedure_local_cfg_baset< nodet, goto_programt, goto_programt::targett > | |
►Cgrapht< cfg_base_nodet< nodet, T > > | |
►Ccfg_baset< nodet, P, T > | |
Cprocedure_local_cfg_baset< nodet, P, T > | |
►Cgrapht< cfg_base_nodet< slicer_entryt, goto_programt::const_targett > > | |
Ccfg_baset< slicer_entryt > | |
►Cgrapht< cfg_base_nodet< T, goto_programt::const_targett > > | |
Ccfg_baset< T, P, I > | A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO program |
►Ccfg_baset< T, const goto_programt, goto_programt::const_targett > | |
Cconcurrent_cfg_baset< T, P, I > | |
►Cconcurrent_cfg_baset< T, const goto_programt, goto_programt::const_targett > | |
Cprocedure_local_concurrent_cfg_baset< T, P, I > | |
Cprocedure_local_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 > | |
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< destructor_treet::destructor_nodet > | |
►Cgrapht< function_nodet > | |
Ccall_grapht::directed_grapht | Directed graph representation of this call graph |
►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 | |
Cprop_conv_solvert | |
Csatcheck_minisat2_baset< T > | |
►Csatcheck_minisat2_baset< Minisat::SimpSolver > | |
Csatcheck_minisat_simplifiert | |
►Csatcheck_minisat2_baset< Minisat::Solver > | |
Csatcheck_minisat_no_simplifiert | |
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 > | |
Chavoc_loopst | |
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 | |
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_set_pairt | |
Cinfix_opt | |
Cinflate_state | |
Cresolve_inherited_componentt::inherited_componentt | |
Cinode | |
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 |
►Cinstrumentert | |
Cinstrumenter_pensievet | |
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_constantt | Determine whether an expression is constant |
Cconstant_propagator_is_constantt | |
Cgoto_symex_is_constantt | |
Cis_predecessor_oft | |
Cis_threadedt | |
►Citerator | |
Ccmdlinet::option_namest::option_names_iteratort | |
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_language_optionst | |
Cjava_bytecode_parse_treet | |
Cjava_object_factoryt | |
Cjava_primitive_type_infot | Return type for get_java_primitive_type_info |
Cjava_simple_method_stubst | |
Cconfigt::javat | |
Cjsil_parse_treet | |
Cjson_irept | |
►Cjson_streamt | This class provides a facility for streaming JSON objects directly to the output instead of waiting for the object to be fully formed in memory and then print it (as done using jsont ) |
Cjson_stream_arrayt | Provides methods for streaming JSON arrays |
Cjson_stream_objectt | Provides methods for streaming JSON objects |
►Cjsont | |
Cjson_arrayt | |
Cjson_falset | |
Cjson_nullt | |
Cjson_numbert | |
Cjson_objectt | |
Cjson_stringt | |
Cjson_truet | |
Ck_inductiont | |
Clabelt | |
Cjava_bytecode_parse_treet::classt::lambda_method_handlet | |
Clanguage_entryt | |
Clanguage_filet | |
Clanguage_modulet | |
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 | |
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 | |
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 | |
►Cloop_analysist< T > | |
Clexical_loops_templatet< P, T > | Main driver for working out if a class (normally goto_programt) has any lexical loops |
Clinked_loop_analysist< T > | |
Cnatural_loops_templatet< P, T > | Main driver for working out if a class (normally goto_programt) has any natural loops |
►Cloop_analysist< goto_programt::const_targett > | |
►Cnatural_loops_templatet< const goto_programt, goto_programt::const_targett > | |
Cnatural_loopst | A concretized version of natural_loops_templatet<const goto_programt, goto_programt::const_targett> |
►Cloop_analysist< goto_programt::targett > | |
Cnatural_loops_templatet< goto_programt, goto_programt::targett > | |
Cframet::loop_infot | |
►Cloop_templatet< T > | A loop, specified as a set of instructions |
Cloop_with_parent_analysis_templatet< T > | |
Cmain_function_resultt | |
Cboolbv_mapt::map_bitt | |
Cboolbv_mapt::map_entryt | |
Cmap_iteratort< iteratort, outputt > | Iterator which applies some given function f after each increment and returns its result on dereference |
►CMatcherBase | |
Cinvariant_failure_containingt | Author: Diffblue Ltd |
Ccpp_typecheck_resolvet::matcht | |
►Cjava_bytecode_parse_treet::membert | |
Cjava_bytecode_parse_treet::fieldt | |
Cjava_bytecode_parse_treet::methodt | |
Cboolbv_widtht::membert | |
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 | |
Cmerge_full_irept | |
Cmerge_irept | |
Cmerged_irep_hash | |
Cmerged_irepst | |
►Cmessage_handlert | |
►Cconsole_message_handlert | |
Ccl_message_handlert | |
Cgcc_message_handlert | |
Cnull_message_handlert | |
Csmt2_message_handlert | |
►Cstream_message_handlert | |
Ccerr_message_handlert | |
Ccout_message_handlert | |
Cui_message_handlert | |
►Cmessaget | Class that provides messages with a built-in verbosity 'level' |
►Cansi_c_convert_typet | |
Ccpp_convert_typet | |
Cci_lazy_methodst | |
Ccompilet | |
►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 |
►Cgoal_filter_baset | Base class for filtering goals |
Cinternal_goals_filtert | Filters out goals with source locations considered internal |
►Cgoto_cc_modet | |
Carmcc_modet | |
Cas_modet | |
Ccw_modet | |
Cgcc_modet | |
Cld_modet | |
Cms_cl_modet | |
Cms_link_modet | |
►Cgoto_convertt | |
Cgoto_convert_functionst | |
Cgoto_inlinet | |
Cinterpretert | |
Cjava_bytecode_convert_classt | |
Cjava_bytecode_convert_methodt | |
Cjava_bytecode_instrumentt | |
►Cjava_class_loader_baset | Base class for maintaining classpath |
Cjava_class_loadert | Class responsible to load .class files |
Cjava_class_loader_limitt | Class representing a filter for class file loading |
Cjava_string_library_preprocesst | |
Cjsil_convertt | |
Clanguage_filest | |
►Clanguaget | |
Cansi_c_languaget | |
Ccpp_languaget | |
Cjava_bytecode_languaget | |
Cjsil_languaget | |
Cjson_symtab_languaget | |
Cstatement_list_languaget | Implements the language interface for the Statement List language |
Clinker_script_merget | Synthesise definitions of symbols that are defined in linker scripts |
►Cparsert | |
Cansi_c_parsert | |
Cassembler_parsert | |
Ccpp_parsert | |
Cjava_bytecode_parsert | |
Cjsil_parsert | |
Cjson_parsert | |
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 | |
Cpreprocessort | |
Cremove_const_function_pointerst | |
Cremove_java_newt | |
Csafety_checkert | |
Csmt2_dect | Decision procedure interface for various SMT 2.x solvers |
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_instrumentationt | |
►Ctypecheckt | |
►Cc_typecheck_baset | |
Cansi_c_typecheckt | |
Ccpp_typecheckt | |
Cjava_bytecode_typecheckt | |
Cjsil_typecheckt | |
Clinkingt | |
Cstatement_list_typecheckt | Class for encapsulating the current state of the type check |
Ccpp_typecheckt::method_bodyt | |
Cmethod_bytecodet | |
►Cmethodt | |
Cjava_class_typet::methodt | |
Cmini_bdd_applyt | |
Cmini_bdd_mgrt | |
Cmini_bdd_nodet | |
Cmini_bddt | |
Cmonomialt | |
Cms_cl_versiont | |
Cmz_stream_s | |
►Cmz_zip_archive | |
Cmz_zip_archive_statet | |
Cmz_zip_archive_file_stat | |
Cmz_zip_archivet | Thin object-oriented wrapper around the MZ Zip library Zip file reader and extractor |
Cmz_zip_array | |
Cmz_zip_internal_state_tag | |
Cmz_zip_writer_add_state | |
Csmt2_parsert::named_termt | |
►Cnamespace_baset | Basic interface for a namespace |
►Cnamespacet | A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in them |
Cc_typecheck_baset | |
Cmulti_namespacet | A multi namespace is essentially a namespace, with a list of namespaces |
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 |
Clocal_cfgt::nodet | |
Cunsigned_union_find::nodet | |
Ccfg_dominators_templatet< P, T, post_dom >::nodet | |
Cstring_dependenciest::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 | |
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 | |
Cvalue_set_fivrt::object_map_dt | |
Cvalue_set_fivrnst::object_map_dt | |
Cprop_minimizet::objectivet | |
Ccover_goalst::observert | |
Coperator_entryt | |
Ccmdlinet::option_namest | |
Coptionst | |
Ccmdlinet::optiont | |
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 | |
Cgoto_analyzer_parse_optionst | |
Cgoto_diff_parse_optionst | |
Cgoto_harness_parse_optionst | |
Cgoto_instrument_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 | |
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 |
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_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 | |
►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_booleforce_baset | |
Csatcheck_booleforce_coret | |
Csatcheck_booleforcet | |
Csatcheck_cadicalt | |
Csatcheck_glucose_baset< T > | |
►Csatcheck_glucose_baset< Glucose::SimpSolver > | |
Csatcheck_glucose_simplifiert | |
►Csatcheck_glucose_baset< Glucose::Solver > | |
Csatcheck_glucose_no_simplifiert | |
Csatcheck_ipasirt | Interface for generic SAT solver interface IPASIR |
Csatcheck_lingelingt | |
►Csatcheck_minisat1_baset | |
►Csatcheck_minisat1t | |
►Csatcheck_minisat1_prooft | |
Csatcheck_minisat1_coret | |
Csatcheck_minisat2_baset< T > | |
Csatcheck_minisat2_baset< Minisat::SimpSolver > | |
Csatcheck_minisat2_baset< Minisat::Solver > | |
Csatcheck_picosatt | |
Cdimacs_cnf_dumpt | |
►Cqualifierst | |
►Cc_qualifierst | |
Cjava_qualifierst | |
Cboolbvt::quantifiert | |
Cqdimacs_cnft::quantifiert | |
►Crange_domain_baset | |
Cguarded_range_domaint | |
Crange_domaint | |
Cranget< iteratort > | A range is a pair of a begin and an end iterators |
Crationalt | |
Creachability_slicert | |
Creaching_definitiont | Identifies a GOTO instruction where a given variable is defined (i.e |
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 |
Cref_count_ift< enabled > | Used in tree_nodet for activating or not reference counting |
►Cref_count_ift< sharing > | |
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_exceptionst | Lowers high-level exception descriptions into low-level operations suitable for symex and other analyses that don't understand the THROW or CATCH GOTO instructions |
Cremove_function_pointerst | |
Cremove_instanceoft | |
Cremove_returnst | |
Cremove_virtual_functionst | |
Crename_symbolt | |
Creplace_callst | |
►Creplace_symbolt | Replace expression or type symbols by an expression or type, respectively |
Ccasting_replace_symbolt | |
►Cunchecked_replace_symbolt | |
Caddress_of_aware_replace_symbolt | Replace symbols with constants while maintaining syntactically valid expressions |
Creplacement_predicatet | Patterns of expressions that should be replaced |
Cresolution_prooft< T > | |
Cresolution_prooft< clauset > | |
Cresolve_inherited_componentt | |
Crestrictt | |
Csimplify_exprt::resultt< T > | |
Cincremental_goto_checkert::resultt | |
Cmini_bdd_mgrt::reverse_keyt | |
Cfloat_utilst::rounding_mode_bitst | |
Cfloat_bvt::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 | |
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 | |
Csese_region_analysist | |
Caddress_of_aware_replace_symbolt::set_require_lvalue_and_backupt | |
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, exprt > | |
Csharing_mapt< irep_idt, entryt > | |
Csharing_mapt< irep_idt, std::pair< ssa_exprt, std::size_t > > | |
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, std::map< irep_namet, 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 | |
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 codet representing an assignment in the program |
Ccode_assumet | An assumption, which must hold in subsequent code |
Ccode_blockt | A codet representing sequential composition of program statements |
Ccode_breakt | codet representation of a break statement (within a for or while loop) |
Ccode_continuet | codet representation of a continue statement (within a for or while loop) |
Ccode_deadt | A codet representing the removal of a local variable going out of scope |
Ccode_declt | A codet representing the declaration of a local variable |
Ccode_dowhilet | codet representation of a do while statement |
Ccode_expressiont | codet representation of an expression statement |
Ccode_fort | codet representation of a for statement |
Ccode_function_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 | 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 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 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 | 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 |
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 |
Carray_comprehension_exprt | Expression to define a mapping from an argument (index) to elements |
►Cbinary_predicate_exprt | A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two arguments |
►Cbinary_relation_exprt | A base class for relations, i.e., binary predicates whose two operands have the same type |
Cequal_exprt | Equality |
Cieee_float_equal_exprt | IEEE-floating-point equality |
Cieee_float_notequal_exprt | IEEE floating-point disequality |
Cnotequal_exprt | Disequality |
Cextractbit_exprt | Extracts a single bit of a bit-vector operand |
Cjava_instanceof_exprt | |
►Cbinding_exprt | A base class for variable bindings (quantifiers, let, lambda) |
►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 | |
Cdiv_exprt | Division |
Cdynamic_object_exprt | Representation of heap-allocated objects |
Cfactorial_power_exprt | Falling factorial power |
Cfloatbv_typecast_exprt | Semantic type conversion from/to floating-point formats |
Cfunction_application_exprt | Application of (mathematical) function |
Cimplies_exprt | Boolean implication |
Cindex_exprt | Array index operator |
Clet_exprt | A let expression |
Cminus_exprt | Binary minus |
Cmod_exprt | Modulo |
Cobject_descriptor_exprt | Split an expression into a base object and a (byte) offset |
Cpower_exprt | Exponentiation |
Crem_exprt | Remainder of division |
Creplication_exprt | Bit-vector replication |
►Cshift_exprt | A base class for shift operators |
Cashr_exprt | Arithmetic right shift |
Clshr_exprt | Logical right shift |
Cshl_exprt | Left shift |
►Cconstant_exprt | A constant literal expression |
Cfalse_exprt | The Boolean constant false |
Cgoto_trace_constant_pointer_exprt | Variety of constant expression only used in the context of a GOTO trace, to give both the numeric value and the symbolic value of a pointer, e.g |
Cnull_pointer_exprt | The null pointer constant |
Ctrue_exprt | The Boolean constant true |
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 |
Cbitxor_exprt | Bit-wise XOR |
Cconcatenation_exprt | Concatenation of bit-vector operands |
Ccond_exprt | This is a parametric version of an if-expression: it returns the value of the first case (using the ordering of the operands) whose condition evaluates to true |
Cmult_exprt | Binary multiplication Associativity is not specified |
Cor_exprt | Boolean OR |
Cplus_exprt | The plus expression Associativity is not specified |
►Cstruct_exprt | Struct constructor from list of elements |
Crefined_string_exprt | |
Ctuple_exprt | |
Cvector_exprt | Vector constructor from list of elements |
Cxor_exprt | Boolean XOR |
►Cnullary_exprt | An expression without operands |
Cansi_c_declaratort | |
Cclass_method_descriptor_exprt | An expression describing a method on a class |
Cinfinity_exprt | An expression denoting infinity |
Cnil_exprt | The NIL expression |
Cnondet_symbol_exprt | Expression to hold a nondeterministic choice |
Csmt2_convt::smt2_symbolt | |
Cstring_constantt | |
►Csymbol_exprt | Expression to hold a symbol (variable) |
Cdecorated_symbol_exprt | Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_local |
Cssa_exprt | Expression providing an SSA-renamed symbol of expressions |
Ctype_exprt | An expression denoting a type |
►Cpredicate_exprt | A base class for expressions that are predicates, i.e., Boolean-typed |
Cliteral_exprt | |
►Cternary_exprt | An expression with three operands |
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 |
Ctranst | Transition system, consisting of state invariant, initial state predicate, and transition predicate |
Cupdate_exprt | Operator to update elements in structs and arrays |
►Cunary_exprt | Generic base class for unary expressions |
Cabs_exprt | Absolute value |
Caddress_of_exprt | Operator to return the address of an object |
Carray_of_exprt | Array constructor from single element |
Cbitnot_exprt | Bit-wise negation of bit-vectors |
Cbswap_exprt | The byte swap expression |
Ccomplex_imag_exprt | Imaginary part of the expression describing a complex number |
Ccomplex_real_exprt | Real part of the expression describing a complex number |
Cdereference_exprt | Operator to dereference a pointer |
Cmember_exprt | Extract member of struct or union |
Cnot_exprt | Boolean negation |
Cpopcount_exprt | The popcount (counting the number of bits set to 1) expression |
Ctypecast_exprt | Semantic type conversion |
Cunary_minus_exprt | The unary minus expression |
Cunary_plus_exprt | The unary plus expression |
►Cunary_predicate_exprt | A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argument |
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 |
Csign_exprt | Sign of an expression Predicate is true if _op is negative, false otherwise |
Cunion_exprt | Union constructor from single element |
Cwith_exprt | Operator to update elements in structs and arrays |
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 | |
Cjsil_declarationt | |
Cmax_exprt | +∞ upper bound for intervals |
Cmin_exprt | -∞ upper bound for intervals |
►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_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 | |
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 |
Cjava_method_typet | |
Cjsil_builtin_code_typet | |
Cjsil_spec_code_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 |
Cstring_typet | String type |
►Cstruct_union_typet | Base type for structs and unions |
►Cstruct_typet | Structure type, corresponds to C style structs |
►Cclass_typet | Class type |
►Cjava_class_typet | |
Cjava_generic_class_typet | Class to hold a class with generics, extends the java class type with a vector of java generic type parameters (also called type variables) |
Cjava_implicitly_generic_class_typet | Type to hold a Java class that is implicitly generic, e.g., an inner class of a generic outer class or a derived class of a generic base class |
Crefined_string_typet | |
►Cunion_typet | The union type |
Cjsil_union_typet | |
►Ctag_typet | A tag-based type, i.e., typet with an identifier |
Cc_enum_tag_typet | C enum tag type, i.e., c_enum_typet with an identifier |
►Cstruct_tag_typet | A struct tag type, i.e., struct_typet with an identifier |
Cjava_generic_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 | |
Cshow_goto_functions_jsont | |
Cshow_goto_functions_xmlt | |
Csmt2_parsert::signature_with_parameter_idst | |
Csimplify_exprt | |
Creachability_slicert::slicer_entryt | |
►Cslicing_criteriont | |
Cassert_criteriont | |
Cin_function_criteriont | |
Cproperties_criteriont | |
Csmall_mapt< T, Ind, Num > | Map from small integers to values |
Csmall_mapt< innert > | |
►Csmall_shared_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< key_type, mapped_type, equalT >, d_leaft< key_type, mapped_type, equalT >, d_internalt< key_type, mapped_type, equalT > > | |
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_format_containert< T > | |
►Csmt2_parsert | |
Csmt2_solvert | |
►Csmt2_stringstreamt | |
Csmt2_dect | Decision procedure interface for various SMT 2.x solvers |
►Csmt2_tokenizert | |
Csmt2irept | |
Csolver_factoryt | |
Csolver_hardnesst | A structure that facilitates collecting the complexity statistics from a decision procedure |
►Csolver_resource_limitst | |
Cprop_conv_solvert | |
Csolver_factoryt::solvert | |
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 | |
Ccheck_call_sequencet::state_hash | |
Cstatement_list_parse_treet | Intermediate representation of a parsed Statement List file before converting it into a goto program |
Cnfat< T >::statet | A state is a set of possibly active transitions |
Ccheck_call_sequencet::statet | |
►Cstatic_analysis_baset | |
►Cstatic_analysist< T > | |
Cconcurrency_aware_static_analysist< T > | |
►Cstatic_analysist< 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 |
Cstatic_verifier_resultt | |
Cclauset::stept | |
Cstring_axiomst | |
►Cstring_builtin_functiont | Base class for string functions that are built in the solver |
Cstring_builtin_function_with_no_evalt | Functions that are not yet supported in this class but are supported by string_constraint_generatort |
►Cstring_creation_builtin_functiont | String creation from other types |
Cstring_of_int_builtin_functiont | String creation from integer types |
Cstring_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_containert | |
Cstring_dependenciest | Keep track of dependencies between strings |
Cstring_hash | |
Cstring_dependenciest::string_nodet | A string node points to builtin_function on which it depends |
Cstring_not_contains_constraintt | Constraints to encode non containement of strings |
Cstring_ptr_hash | |
Cstring_ptrt | |
Cstructured_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 | |
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 | |
Cgoto_convertt::targetst | |
Cgrapht< N >::tarjant | |
Ctdefl_compressor | |
Ctdefl_output_buffer | |
Ctdefl_sym_freq | |
Ctemp_dirt | |
Ctemplate_mapt | |
Ctemplate_numberingt< Map > | |
Ctemplate_numberingt< dstringt > | |
Ctemplate_numberingt< dstringt, dstring_hash > | |
Ctemplate_numberingt< exprt > | |
Ctemplate_numberingt< exprt, irep_hash > | |
Ctemplate_numberingt< irep_idt > | |
Ctemplate_numberingt< irep_idt, irep_id_hash > | |
Ctemplate_numberingt< packedt, vector_hasht > | |
Ctemplate_numberingt< T > | |
Ctemporary_filet | |
Cmonomialt::termt | |
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 |
Cnfat< T >::transitiont | |
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_find< T > | |
Cunion_find< exprt > | |
Cunion_find< irep_idt > | |
Cunion_find_replacet | Similar interface to union-find for expressions, with a function for replacing sub-expressions by their result for find |
►Cfloat_utilst::unpacked_floatt | |
Cfloat_utilst::biased_floatt | |
Cfloat_utilst::unbiased_floatt | |
►Cfloat_bvt::unpacked_floatt | |
Cfloat_bvt::biased_floatt | |
Cfloat_bvt::unbiased_floatt | |
Cunsigned_union_find | |
Cgoto_unwindt::unwind_logt | |
Cunwindsett | |
Cvalue_set_fivrnst::object_map_dt::validity_ranget | |
Cvalue_set_fivrt::object_map_dt::validity_ranget | |
Cvalue_set_dereferencet | Wrapper for a function dereferencing pointer expressions using a value set |
Cvalue_set_fit | |
Cvalue_set_fivrnst | |
Cvalue_set_fivrt | |
►Cvalue_setst | |
Cvalue_set_analysis_fit | |
Cvalue_set_analysis_fivrnst | |
Cvalue_set_analysis_fivrt | |
Cvalue_set_analysis_templatet< VSDT > | 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 | |
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 | |
Cjava_bytecode_parse_treet::methodt::verification_type_infot | |
Cconfigt::verilogt | |
Cw_guardst | |
►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 |
Cxml_edget | |
Cxml_parse_treet | |
Cxmlt | |
Czip_iteratort< first_iteratort, second_iteratort, same_size > | Zip two ranges to make a range of pairs |