►Ndetail | |
Calways_falset | |
Cexpr_dynamic_cast_return_typet | |
Cexpr_try_dynamic_cast_return_typet | |
►Nrequire_goto_statements | |
Cno_decl_found_exceptiont | |
Cpointer_assignment_locationt | |
►Nrequire_parse_tree | |
Cexpected_instructiont | |
►Nrequire_type | |
Cexpected_type_argumentt | |
►Nstd | STL namespace |
Chash< dstringt > | Default hash function of dstringt for use with STL containers |
Chash< string_not_contains_constraintt > | |
C__CPROVER_jsa_abstract_heap | |
C__CPROVER_jsa_abstract_node | Abstract nodes may assume any of a set of pre-defined values (value_ref to abstract_ranget) |
C__CPROVER_jsa_abstract_range | Set of pre-defined, possible values for abstract nodes |
C__CPROVER_jsa_concrete_node | Concrete node with explicit value |
C__CPROVER_jsa_iterator | Iterators point to a node and give the relative index within that node |
C__CPROVER_pipet | |
C_rw_set_loct | |
Cabs_exprt | Absolute value |
Cabstract_eventt | |
Cabstract_goto_modelt | Abstract interface to eager or lazy GOTO models |
Cacceleratet | |
►Cacceleration_utilst | |
Cpolynomial_array_assignmentt | |
►Caddress_of_aware_replace_symbolt | Replace symbols with constants while maintaining syntactically valid expressions |
Cset_require_lvalue_and_backupt | |
Caddress_of_exprt | Operator to return the address of an object |
Caggressive_slicert | The aggressive slicer removes the body of all the functions except those on the shortest path, those within the call-depth of the shortest path, those given by name as command line argument, and those that contain a given irep_idt snippet If no properties are set by the user, we preserve all functions on the shortest paths to each property |
Cai_baset | The basic interface of an abstract interpreter |
Cai_domain_baset | The interface offered by a domain, allows code to manipulate domains without knowing their exact type |
Cait | |
Call_paths_enumeratort | |
Canalysis_exceptiont | Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an error) |
Cand_exprt | Boolean AND |
Cannotated_typet | |
Cansi_c_convert_typet | |
Cansi_c_declarationt | |
Cansi_c_declaratort | |
Cansi_c_identifiert | |
Cansi_c_languaget | |
Cansi_c_parse_treet | |
Cansi_c_parsert | |
Cansi_c_scopet | |
Cansi_c_typecheckt | |
Carmcc_cmdlinet | |
Carmcc_modet | |
Carray_exprt | Array constructor from list of elements |
Carray_list_exprt | Array constructor from a list of index-element pairs Operands are index/value pairs, alternating |
Carray_of_exprt | Array constructor from single element |
Carray_poolt | Correspondance between arrays and pointers string representations |
Carray_string_exprt | |
Carray_typet | Arrays with given size |
►Carrayst | |
Carray_equalityt | |
Clazy_constraintt | |
Cas86_cmdlinet | |
Cas_cmdlinet | |
Cas_modet | |
Cashr_exprt | Arithmetic right shift |
Cassembler_parsert | |
Cassert_criteriont | |
Cassert_false_generate_function_bodiest | |
Cassert_false_then_assume_false_generate_function_bodiest | |
Cassume_false_generate_function_bodiest | |
Cautomatont | |
Cauxiliary_symbolt | Internally generated symbol table entry |
Cbad_cast_exceptiont | |
Cbase_ref_infot | |
Cbase_type_eqt | |
Cbcc_cmdlinet | |
Cbdd_exprt | TO_BE_DOCUMENTED |
Cbinary_exprt | A base class for binary expressions |
Cbinary_predicate_exprt | A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two arguments |
Cbinary_relation_exprt | A base class for relations, i.e., binary predicates |
Cbitand_exprt | Bit-wise AND |
Cbitnot_exprt | Bit-wise negation of bit-vectors |
Cbitor_exprt | Bit-wise OR |
Cbitvector_conversion_exceptiont | |
Cbitvector_typet | Base class of fixed-width bit-vector types |
Cbitxor_exprt | Bit-wise XOR |
►Cbmc_all_propertiest | |
Cgoalt | |
►Cbmc_covert | |
►Cgoalt | |
Cinstancet | |
Ctestt | |
Cbmct | Bounded model checking or path exploration for goto-programs |
Cbool_typet | The Boolean type |
►Cboolbv_mapt | |
Cmap_bitt | |
Cmap_entryt | |
►Cboolbv_widtht | |
Centryt | |
Cmembert | |
►Cboolbvt | |
Cquantifiert | |
Cbswap_exprt | The byte swap expression |
Cbv_arithmetict | |
Cbv_dimacst | |
Cbv_endianness_mapt | Map bytes according to the configured endianness |
Cbv_minimizet | |
Cbv_minimizing_dect | |
►Cbv_pointerst | |
Cpostponedt | |
►Cbv_refinementt | |
Capproximationt | |
Cconfigt | |
Cinfot | |
Cbv_spect | |
Cbv_typet | Fixed-width bit-vector without numerical interpretation |
Cbv_utilst | |
Cbyte_extract_exprt | TO_BE_DOCUMENTED |
Cbyte_update_exprt | TO_BE_DOCUMENTED |
Cbytecode_infot | |
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 |
Cc_enum_tag_typet | C enum tag type, i.e., c_enum_typet with an identifier |
►Cc_enum_typet | The type of C enums |
Cc_enum_membert | |
Cc_object_factory_parameterst | |
Cc_qualifierst | |
Cc_storage_spect | |
Cc_typecastt | |
Cc_typecheck_baset | |
Ccall_checkt | |
►Ccall_grapht | A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection |
Cdirected_grapht | Directed graph representation of this call graph |
Cedge_with_callsitest | Edge of the directed graph representation of this call graph |
Cfunction_nodet | Node of the directed graph representation of this call graph |
Ccall_validate_fullt | |
Ccall_validatet | |
Ccasting_replace_symbolt | |
Ccbmc_parse_optionst | |
Ccerr_message_handlert | |
Ccfg_base_nodet | |
►Ccfg_baset | A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO program |
Centry_mapt | |
►Ccfg_dominators_templatet | |
Cnodet | |
Cchange_impactt | |
Ccharacter_refine_preprocesst | |
►Ccheck_call_sequencet | |
Ccall_stack_entryt | |
Cstate_hash | |
Cstatet | |
Cci_lazy_methods_neededt | |
►Cci_lazy_methodst | |
Cconvert_method_resultt | |
Cclass_hierarchy_graph_nodet | Class hierarchy graph node: simply contains a class identifier |
Cclass_hierarchy_grapht | Class hierarchy, represented using grapht and therefore suitable for use with generic graph algorithms |
►Cclass_hierarchyt | Non-graph-based representation of the class hierarchy |
Centryt | |
Cclass_infot | Corresponds to the CONSTANT_Class_info Structure Described in Java 8 specification 4.4.1 |
Cclass_typet | Class type |
►Cclauset | |
Cstept | |
►Ccmdlinet | |
Coptiont | |
Ccnf_clause_list_assignmentt | |
Ccnf_clause_listt | |
Ccnf_solvert | |
Ccnft | |
Ccode_asmt | codet representation of an inline assembler statement |
Ccode_assertt | A non-fatal assertion, which checks a condition then permits execution to continue |
Ccode_assignt | A codet representing an assignment in the program |
Ccode_assumet | An assumption, which must hold in subsequent code |
Ccode_blockt | A codet representing sequential composition of program statements |
Ccode_breakt | codet representation of a break statement (within a for or while loop) |
Ccode_continuet | codet representation of a continue statement (within a for or while loop) |
Ccode_contractst | |
Ccode_deadt | A codet representing the removal of a local variable going out of scope |
Ccode_declt | A codet representing the declaration of a local variable |
Ccode_dowhilet | codet representation of a do while statement |
Ccode_expressiont | codet representation of an expression statement |
Ccode_fort | codet representation of a for statement |
Ccode_function_callt | codet representation of a function call statement |
Ccode_gotot | codet representation of a goto statement |
Ccode_ifthenelset | codet representation of an if-then-else statement |
Ccode_labelt | codet representation of a label for branch targets |
Ccode_landingpadt | A statement that catches an exception, assigning the exception in flight to an expression (e.g |
Ccode_pop_catcht | Pops an exception handler from the stack of active handlers (i.e |
►Ccode_push_catcht | Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 .. |
Cexception_list_entryt | |
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_typet | Base type of functions |
Cparametert | |
Ccode_whilet | codet representing a while statement |
Ccodet | Data structure for representing an arbitrary statement in a program |
Ccompilet | |
Ccomplex_exprt | Complex constructor from a pair of numbers |
Ccomplex_imag_exprt | Imaginary part of the expression describing a complex number |
Ccomplex_real_exprt | Real part of the expression describing a complex number |
Ccomplex_typet | Complex numbers made of pair of given subtype |
Cconcat_iteratort | On increment, increments a first iterator and when the corresponding end iterator is reached, starts to increment a second one |
Cconcatenation_exprt | Concatenation of bit-vector operands |
Cconcurrency_aware_ait | |
Cconcurrency_aware_static_analysist | |
►Cconcurrency_instrumentationt | |
Cshared_vart | |
Cthread_local_vart | |
Cconcurrent_cfg_baset | |
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 |
Ccone_of_influencet | |
►Cconfigt | Globally accessible architectural configuration |
Cansi_ct | |
Cbv_encodingt | |
Ccppt | |
Cjavat | |
Cverilogt | |
Cconsole_message_handlert | |
Cconst_depth_iteratort | |
Cconst_expr_visitort | |
Cconst_target_hash | |
Cconst_unique_depth_iteratort | |
Cconstant_exprt | A constant literal expression |
Cconstant_propagator_ait | |
►Cconstant_propagator_domaint | |
Cvaluest | |
Cconversion_dependenciest | This is structure is here to facilitate passing arguments to the conversion functions |
Ccopy_on_write_pointeet | A helper class to store use-counts of copy-on-write objects |
Ccopy_on_writet | A utility class for writing types with copy-on-write behaviour (like irep) |
Ccounterexample_beautificationt | |
Ccout_message_handlert | |
Ccover_assertion_instrumentert | Assertion coverage instrumenter |
Ccover_basic_blocks_javat | |
►Ccover_basic_blockst | |
Cblock_infot | |
Ccover_blocks_baset | |
Ccover_branch_instrumentert | Branch coverage instrumenter |
Ccover_condition_instrumentert | Condition coverage instrumenter |
Ccover_configt | |
Ccover_cover_instrumentert | __CPROVER_cover coverage instrumenter |
Ccover_decision_instrumentert | Decision coverage instrumenter |
►Ccover_goalst | Try to cover some given set of goals incrementally |
Cgoalt | |
Cobservert | |
Ccover_instrumenter_baset | Base class for goto program coverage instrumenters |
Ccover_instrumenterst | A collection of instrumenters to be run |
Ccover_location_instrumentert | Basic block coverage instrumenter |
Ccover_mcdc_instrumentert | MC/DC coverage instrumenter |
Ccover_path_instrumentert | Path coverage instrumenter |
Ccoverage_recordt | |
Ccpp_convert_typet | |
Ccpp_declarationt | |
Ccpp_declarator_convertert | |
Ccpp_declaratort | |
Ccpp_enum_typet | |
Ccpp_idt | |
Ccpp_itemt | |
Ccpp_languaget | |
Ccpp_linkage_spect | |
Ccpp_member_spect | |
Ccpp_namespace_spect | |
►Ccpp_namet | |
Cnamet | |
Ccpp_parse_treet | |
Ccpp_parsert | |
Ccpp_root_scopet | |
Ccpp_save_scopet | |
Ccpp_saved_template_mapt | |
Ccpp_scopest | |
Ccpp_scopet | |
Ccpp_static_assertt | |
Ccpp_storage_spect | |
Ccpp_template_args_baset | |
Ccpp_template_args_non_tct | |
Ccpp_template_args_tct | |
Ccpp_token_buffert | |
Ccpp_tokent | |
Ccpp_typecastt | |
Ccpp_typecheck_fargst | |
►Ccpp_typecheck_resolvet | |
Cmatcht | |
►Ccpp_typecheckt | |
Cinstantiation_levelt | |
Cinstantiationt | |
Cmethod_bodyt | |
Ccpp_usingt | |
Ccprover_exception_baset | Base class for exceptions thrown in the cprover project |
Ccprover_library_entryt | |
Ccustom_bitvector_analysist | |
►Ccustom_bitvector_domaint | |
Cvectorst | |
Ccw_modet | |
Cd_containert | |
Cd_internalt | |
Cd_leaft | |
Cdata | |
Cdata_dpt | |
Cdatat | |
Cdecision_proceduret | |
Cdecorated_symbol_exprt | Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_local |
Cdep_edget | |
Cdep_graph_domaint | |
Cdep_nodet | |
Cdependence_grapht | |
Cdepth_iterator_baset | Depth first search iterator base - iterates over supplied expression and all its operands recursively |
Cdepth_iterator_expr_statet | Helper class for depth_iterator_baset |
Cdepth_iteratort | |
Cdereference_callbackt | Base class for pointer value set analysis |
Cdereference_exprt | Operator to dereference a pointer |
Cdereferencet | Wrapper for a function which dereference a pointer-expression |
Cdeserialization_exceptiont | Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes |
►Cdesignatort | |
Centryt | |
Cdiagnostics_helpert | 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 > | |
Cdimacs_cnf_dumpt | |
Cdimacs_cnft | |
Cdirtyt | |
Cdisjunctive_polynomial_accelerationt | |
Cdispatch_table_entryt | |
Cdiv_exprt | Division |
►Cdocument_propertiest | |
Cdoc_claimt | |
Clinet | |
Cdoes_remove_constt | |
Cdomain_baset | |
Cdott | |
Cdstring_hash | |
Cdstringt | dstringt has one field, an unsigned integer no which is an index into a static table of strings |
►Cdump_ct | |
Ctypedef_infot | |
Cdynamic_object_exprt | Representation of heap-allocated objects |
CElf32_Ehdr | |
CElf32_Shdr | |
CElf64_Ehdr | |
CElf64_Shdr | |
Celf_readert | |
Cempty_cfg_nodet | |
Cempty_edget | |
Cempty_typet | The empty type |
Cendianness_mapt | Maps a big-endian offset to a little-endian offset |
Cenumerating_loop_accelerationt | |
Cenumeration_typet | An enumeration type, i.e., a type with elements (not to be confused with C enums) |
Cequal_exprt | Equality |
►Cequalityt | |
Ctypestructt | |
Cequation_conversion_exceptiont | |
Cequation_symbol_mappingt | Maps equation to expressions contained in them and conversely expressions to equations that contain them |
Cescape_analysist | |
►Cescape_domaint | |
Ccleanupt | |
►Cevent_grapht | |
►Ccritical_cyclet | |
Cdelayt | |
Cgraph_conc_explorert | |
Cgraph_explorert | |
Cgraph_pensieve_explorert | |
Cexists_exprt | An exists expression |
Cexpanding_vectort | |
Cexpr2c_configurationt | Used for configuring the behaviour of expr2c and type2c |
Cexpr2cppt | |
Cexpr2ct | |
Cexpr2javat | |
Cexpr2jsilt | |
Cexpr_initializert | |
Cexpr_visitort | |
Cexprt | Base class for all expressions |
Cextractbit_exprt | Extracts a single bit of a bit-vector operand |
Cextractbits_exprt | Extracts a sub-range of a bit-vector operand |
Cfactorial_power_exprt | Falling factorial power |
Cfalse_exprt | The Boolean constant false |
►Cfault_localizationt | |
Clpointt | |
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 |
Cfile | |
Cfilter_iteratort | Iterator which only stops at elements for which some given function f is true |
Cfind_qvar_visitort | |
Cfixed_keys_map_wrappert | |
Cfixedbv_spect | |
Cfixedbv_typet | Fixed-width bit-vector with signed fixed-point interpretation |
Cfixedbvt | |
Cflatten_byte_extract_exceptiont | |
Cfloat_approximationt | |
►Cfloat_bvt | |
Cbiased_floatt | |
Crounding_mode_bitst | |
Cunbiased_floatt | |
Cunpacked_floatt | |
►Cfloat_utilst | |
Cbiased_floatt | |
Crounding_mode_bitst | |
Cunbiased_floatt | |
Cunpacked_floatt | |
Cfloatbv_typecast_exprt | Semantic type conversion from/to floating-point formats |
Cfloatbv_typet | Fixed-width bit-vector with IEEE floating-point interpretation |
Cflow_insensitive_abstract_domain_baset | |
Cflow_insensitive_analysis_baset | |
Cflow_insensitive_analysist | |
Cforall_exprt | A forall expression |
Cformat_constantt | |
Cformat_containert | The below enables convenient syntax for feeding objects into streams, via stream << format(o) |
Cformat_elementt | |
Cformat_specifiert | |
Cformat_spect | |
Cformat_textt | |
Cformat_tokent | |
Cfree_form_cmdlinet | An implementation of cmdlinet to be used in tests |
Cfreert | A functor wrapping std::free |
►Cfull_slicert | |
Ccfg_nodet | |
Cfunction_application_exprt | Application of (mathematical) function |
Cfunction_filter_baset | Base class for filtering 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 |
Cfunction_modifiest | |
►Cfunctionst | |
Cfunction_infot | |
Cgcc_cmdlinet | |
Cgcc_message_handlert | |
Cgcc_modet | |
Cgcc_versiont | |
Cgenerate_function_bodies_errort | |
Cgenerate_function_bodiest | Base class for replace_function_body implementations |
Cgeneric_parameter_specialization_map_keyst | |
Cglobal_may_alias_analysist | This is a may analysis (i.e |
Cglobal_may_alias_domaint | |
Cgoal_filter_baset | Base class for filtering goals |
Cgoal_filterst | A collection of goal filters to be applied in conjunction |
Cgoto_analyzer_parse_optionst | |
►Cgoto_cc_cmdlinet | |
Cargt | |
Cgoto_cc_modet | |
►Cgoto_checkt | |
Cconditiont | |
Cgoto_convert_functionst | |
►Cgoto_convertt | |
Cbreak_continue_targetst | |
Cbreak_switch_targetst | |
Cleave_targett | |
Ctargetst | |
Cthrow_targett | |
Cgoto_diff_languagest | |
Cgoto_diff_parse_optionst | |
Cgoto_difft | |
Cgoto_functionst | A collection of goto functions |
Cgoto_functiont | A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers) |
►Cgoto_inlinet | |
►Cgoto_inline_logt | |
Cgoto_inline_log_infot | |
Cgoto_instrument_parse_optionst | |
Cgoto_model_functiont | Interface providing access to a single function in a GOTO model, plus its associated symbol table |
Cgoto_modelt | |
Cgoto_null_checkt | Return structure for get_null_checked_expr and get_conditional_checked_expr |
►Cgoto_program2codet | |
Ccaset | |
►Cgoto_program_coverage_recordt | |
Ccoverage_conditiont | |
Ccoverage_linet | |
Cgoto_program_dereferencet | Wrapper for functions removing dereferences in expressions contained in a goto program |
►Cgoto_programt | A generic container class for the GOTO intermediate representation of one function |
Cinstructiont | This class represents an instruction in the GOTO intermediate representation |
Cgoto_symex_is_constantt | |
►Cgoto_symex_statet | |
►Cframet | |
Cloop_infot | |
Cgoto_statet | |
Cthreadt | |
Cgoto_symext | The main class for the forward symbolic simulator |
Cgoto_trace_stept | TO_BE_DOCUMENTED |
Cgoto_tracet | TO_BE_DOCUMENTED |
►Cgoto_unwindt | |
Cunwind_logt | |
Cgraph_nodet | This class represents a node in a directed graph |
Cgraphml_witnesst | |
Cgraphmlt | |
►Cgrapht | A generic directed graph with a parametric node type |
Ctarjant | |
Cguarded_range_domaint | |
Cguardt | |
Chavoc_generate_function_bodiest | |
Chavoc_loopst | |
Cidentifiert | |
Cieee_float_equal_exprt | IEEE-floating-point equality |
Cieee_float_notequal_exprt | IEEE floating-point disequality |
Cieee_float_op_exprt | IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2) |
Cieee_float_spect | |
Cieee_floatt | |
Cif_exprt | The trinary if-then-else operator |
Cimplies_exprt | Boolean implication |
Cin_function_criteriont | |
Cinclude_pattern_filtert | Filters functions that match the provided pattern |
Cincomplete_array_typet | Arrays without size |
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 | |
Cincremental_dirtyt | Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly once |
Cindex_designatort | |
Cindex_exprt | Array index operator |
Cindex_set_pairt | |
Cindicator_maskt | |
Cindicator_maskt< T, B, std::integral_constant< T, 0 > > | |
Cinfinity_exprt | An expression denoting infinity |
Cinfix_opt | |
Cinflate_state | |
Cinode | |
Cinstrumenter_pensievet | |
►Cinstrumentert | |
Ccfg_visitort | |
Cinteger_typet | Unbounded, signed integers (mathematical integers, not bitvectors) |
Cinternal_functions_filtert | Filters out CPROVER internal functions |
Cinternal_goals_filtert | Filters out goals with source locations considered internal |
►Cinterpretert | |
Cfunction_assignments_contextt | |
Cfunction_assignmentt | |
Cmemory_cellt | |
Cstack_framet | |
Cinterval_domaint | |
Cinterval_sparse_arrayt | Represents arrays by the indexes up to which the value remains the same |
Cinterval_templatet | |
►Cinv_object_storet | |
Centryt | |
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 |
Cinvariant_failedt | A logic error, augmented with a distinguished field to hold a backtrace |
Cinvariant_propagationt | |
Cinvariant_set_domaint | |
Cinvariant_sett | |
Cinvariant_with_diagnostics_failedt | A class that includes diagnostic information related to an invariant violation |
Cirep_full_eq | |
Cirep_full_hash | |
Cirep_full_hash_containert | |
Cirep_hash | |
►Cirep_hash_container_baset | |
Cirep_entryt | |
Cpointer_hasht | |
Cvector_hasht | |
Cirep_hash_containert | |
Cirep_hash_mapt | |
Cirep_pretty_diagnosticst | |
►Cirep_serializationt | |
Cireps_containert | |
►Cirept | Base class for tree-like data structures with sharing |
Cdt | |
Cis_constantt | Determine whether an expression is constant |
Cis_predecessor_oft | |
Cis_threaded_domaint | |
Cis_threadedt | |
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 |
Cjanalyzer_parse_optionst | |
Cjar_filet | Class representing a .jar archive |
Cjar_poolt | A chache for jar_filet objects, by file name |
►Cjava_annotationt | |
Cvaluet | |
Cjava_bytecode_convert_classt | |
►Cjava_bytecode_convert_methodt | |
Cblock_tree_nodet | |
Cconverted_instructiont | |
Cholet | |
Clocal_variable_with_holest | |
Cvariablet | |
Cjava_bytecode_instrumentt | |
Cjava_bytecode_languaget | |
►Cjava_bytecode_parse_treet | |
►Cannotationt | |
Celement_value_pairt | |
►Cclasst | |
Clambda_method_handlet | |
Cfieldt | |
Cinstructiont | |
Cmembert | |
►Cmethodt | |
Cexceptiont | |
Clocal_variablet | |
Cstack_map_table_entryt | |
Cverification_type_infot | |
►Cjava_bytecode_parsert | |
Cbytecodet | |
Cpool_entryt | |
Cjava_bytecode_typecheckt | |
►Cjava_class_loader_baset | Base class for maintaining classpath |
Cclasspath_entryt | An entry in the classpath |
Cjava_class_loader_limitt | Class representing a filter for class file loading |
Cjava_class_loadert | Class responsible to load .class files |
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_generic_parametert | Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T> |
Cjava_generic_struct_tag_typet | Type for a generic symbol, extends struct_tag_typet with a vector of java generic types |
Cjava_generic_typet | Class to hold type with generic type arguments, for example java.util.List in either a reference of type List<Integer> or List<T> (here T must have been concretized already to create this object so technically it is an argument rather than parameter/variable, but in the symbol table this still shows as the parameter T) |
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 |
Cjava_method_typet | |
Cjava_object_factory_parameterst | |
Cjava_object_factoryt | |
Cjava_qualifierst | |
Cjava_simple_method_stubst | |
Cjava_string_library_preprocesst | |
Cjava_syntactic_difft | |
Cjbmc_parse_optionst | |
Cjdiff_languagest | |
Cjdiff_parse_optionst | |
Cjournalling_symbol_tablet | A symbol table wrapper that records which entries have been updated/removed |
Cjsil_builtin_code_typet | |
Cjsil_convertt | |
Cjsil_declarationt | |
Cjsil_languaget | |
Cjsil_parse_treet | |
Cjsil_parsert | |
Cjsil_spec_code_typet | |
Cjsil_typecheckt | |
Cjsil_union_typet | |
Cjson_arrayt | |
Cjson_falset | |
Cjson_irept | |
Cjson_nullt | |
Cjson_numbert | |
Cjson_objectt | |
Cjson_parsert | |
Cjson_stream_arrayt | Provides methods for streaming JSON arrays |
Cjson_stream_objectt | Provides methods for streaming JSON objects |
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_stringt | |
Cjson_symtab_languaget | |
Cjson_truet | |
Cjsont | |
Ck_inductiont | |
Clanguage_entryt | |
Clanguage_filest | |
Clanguage_filet | |
Clanguage_modulet | |
Clanguage_uit | |
Clanguaget | |
Clazy_goto_functions_mapt | Provides a wrapper for a map of lazily loaded goto_functiont |
Clazy_goto_modelt | A GOTO model that produces function bodies on demand |
Cld_cmdlinet | |
Cld_modet | |
Clet_exprt | A let expression |
Clinker_script_merget | Synthesise definitions of symbols that are defined in linker scripts |
►Clinkingt | |
Cadjust_type_infot | |
Clispexprt | |
Clispsymbolt | |
Cliteral_exprt | |
Cliteralt | |
►Clocal_bitvector_analysist | |
Cflagst | |
►Clocal_cfgt | |
Cnodet | |
Clocal_may_alias_factoryt | |
►Clocal_may_aliast | |
Cloc_infot | |
►Clocal_safe_pointerst | A very simple, cheap analysis to determine when dereference operations are trivially guarded by a check against a null pointer access |
Cbase_type_comparet | Comparator that regards base_type_eq expressions as equal, and otherwise uses the natural (operator<) ordering on irept |
Clocalst | |
Clshr_exprt | Logical right shift |
Cmain_function_resultt | |
Cmap_iteratort | Iterator which applies some given function f after each increment and returns its result on dereference |
Cmathematical_function_typet | A type for mathematical functions (do not confuse with functions/methods in code) |
Cmember_designatort | |
Cmember_exprt | Extract member of struct or union |
Cmemory_model_baset | |
Cmemory_model_psot | |
Cmemory_model_sct | |
Cmemory_model_tsot | |
Cmerge_full_irept | |
Cmerge_irept | |
Cmerged_irep_hash | |
Cmerged_irepst | |
Cmerged_irept | |
Cmerged_typet | Holds a combination of types |
Cmessage_handlert | |
►Cmessaget | Class that provides messages with a built-in verbosity 'level' |
Ccommandt | |
Ceomt | |
Cmstreamt | |
►Cmethod_bytecodet | |
Cclass_method_and_bytecodet | Pair of class id and methodt |
Cmethod_handle_infot | |
Cmini_bdd_applyt | |
►Cmini_bdd_mgrt | |
Creverse_keyt | |
Cvar_table_entryt | |
Cmini_bdd_nodet | |
Cmini_bddt | |
Cminisat_prooft | |
Cminus_exprt | Binary minus |
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 |
Cmod_exprt | Modulo |
►Cmonomialt | |
Ctermt | |
Cmonotonic_timestampert | |
Cms_cl_cmdlinet | |
Cms_cl_modet | |
Cms_cl_versiont | |
Cms_link_cmdlinet | |
Cms_link_modet | |
Cmult_exprt | Binary multiplication Associativity is not specified |
Cmulti_ary_exprt | A base class for multi-ary expressions Associativity is not specified |
Cmulti_namespacet | A multi namespace is essentially a namespace, with a list of namespaces |
Cmz_stream_s | |
Cmz_zip_archive | |
Cmz_zip_archive_file_stat | |
Cmz_zip_archive_statet | |
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 | |
Cname_and_type_infot | Corresponds to the CONSTANT_NameAndType_info Structure Described in Java 8 specification 4.4.6 |
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 |
Cnatural_loops_templatet | Main driver for working out if a class (normally goto_programt) has any natural loops |
Cnatural_loopst | A concretized version of natural_loops_templatet<const goto_programt, goto_programt::const_targett> |
Cnatural_typet | Natural numbers including zero (mathematical integers, not bitvectors) |
Cnew_scopet | |
Cnil_exprt | The NIL expression |
Cnil_typet | The NIL type, i.e., an invalid type, no value |
Cnon_byte_alignedt | |
Cnon_const_array_sizet | |
Cnon_const_byte_extraction_sizet | |
Cnon_constant_widtht | |
Cnondet_instruction_infot | Holds information about any discovered nondet methods, with extreme type- safety |
Cnondet_symbol_exprt | Expression to hold a nondeterministic choice |
Cnot_exprt | Boolean negation |
Cnotequal_exprt | Disequality |
Cnull_message_handlert | |
Cnull_pointer_exprt | The null pointer constant |
Cnullary_exprt | An expression without operands |
Cnullptr_exceptiont | |
Cnum_bitst | |
Cnum_bitst< 0 > | |
Cnum_bitst< 1 > | |
Cnumeric_castt | 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_descriptor_exprt | Split an expression into a base object and a (byte) offset |
Cobject_factory_parameterst | |
Cobject_idt | |
Coperator_entryt | |
Coptionst | |
Cor_exprt | Boolean OR |
Cosx_fat_readert | |
Coverflow_instrumentert | |
Cparameter_assignmentst | |
Cparameter_symbolt | Symbol table entry of function parameter |
Cparse_floatt | |
Cparse_options_baset | |
CParser | |
Cparsert | |
►Cpartial_order_concurrencyt | |
Ca_rect | |
Cpath_acceleratort | |
Cpath_enumeratort | |
Cpath_explorert | Symbolic execution from a saved branch point |
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_nodet | |
►Cpath_storaget | Storage for symbolic execution paths to be resumed later |
Cpatht | Information saved at a conditional goto to resume execution |
Cpath_strategy_choosert | Factory and information for path_storaget |
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 |
Cpbs_dimacs_cnft | |
Cplus_exprt | The plus expression Associativity is not specified |
Cpointee_address_equalt | Functor to check whether iterators from different collections point at the same object |
Cpointer_arithmetict | |
►Cpointer_logict | |
Cpointert | |
Cpointer_typet | The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they have a subtype) |
Cpoints_tot | |
►Cpolynomial_acceleratort | |
Cpolynomial_array_assignment | |
Cpolynomialt | |
Cpopcount_exprt | The popcount (counting the number of bits set to 1) expression |
Cpostconditiont | |
Cpower_exprt | Exponentiation |
Cpreconditiont | |
Cpredicate_exprt | A base class for expressions that are predicates, i.e., Boolean-typed |
Cpreprocessort | |
►Cprintf_formattert | |
Ceol_exceptiont | |
Cprocedure_local_cfg_baset | |
Cprocedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett > | |
Cprocedure_local_concurrent_cfg_baset | |
Cprop_conv_solvert | TO_BE_DOCUMENTED |
Cprop_convt | |
►Cprop_minimizet | Computes a satisfying assignment of minimal cost according to a const function using incremental SAT |
Cobjectivet | |
Cproperties_criteriont | |
►Cproperty_checkert | |
Cproperty_statust | |
Cpropt | TO_BE_DOCUMENTED |
Cqbf_bdd_certificatet | |
Cqbf_bdd_coret | |
Cqbf_quantort | |
Cqbf_qube_coret | |
Cqbf_qubet | |
Cqbf_skizzo_coret | |
Cqbf_skizzot | |
Cqbf_squolem_coret | |
Cqbf_squolemt | |
►Cqdimacs_cnft | |
Cquantifiert | |
Cqdimacs_coret | |
Cqualifierst | |
Cquantifier_exprt | A base class for quantifier expressions |
Crange_domain_baset | |
Crange_domaint | |
Crange_typet | A type for subranges of integers |
Cranget | A range is a pair of a begin and an end iterators |
Crational_typet | Unbounded, signed rational numbers |
Crationalt | |
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 |
►Creachability_slicert | |
Csearch_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 |
Cslicer_entryt | |
Creaching_definitions_analysist | |
Creaching_definitiont | Identifies a GOTO instruction where a given variable is defined (i.e |
Creal_typet | Unbounded, signed real numbers |
Crebuild_goto_start_function_baset | |
Crecursion_set_entryt | Recursion-set entry owner class |
Cref_expr_set_dt | |
Cref_expr_sett | |
►Creference_counting | |
Cdt | |
Creference_typet | The reference type |
Crefined_string_exprt | |
Crefined_string_typet | |
Crem_exprt | Remainder of division |
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 | |
Creplace_callst | |
Creplace_symbolt | Replace expression or type symbols by an expression or type, respectively |
Creplacement_predicatet | Patterns of expressions that should be replaced |
Creplication_exprt | Bit-vector replication |
Cresolution_prooft | |
►Cresolve_inherited_componentt | |
Cinherited_componentt | |
Crestrictt | |
Crw_guarded_range_set_value_sett | |
Crw_range_set_value_sett | |
Crw_range_sett | |
►Crw_set_baset | |
Centryt | |
Crw_set_functiont | |
Crw_set_loct | |
Crw_set_with_trackt | |
Csafety_checkert | |
Csaj_tablet | Produce canonical ordering for associative and commutative binary operators |
Csat_path_enumeratort | |
Csatcheck_booleforce_baset | |
Csatcheck_booleforce_coret | |
Csatcheck_booleforcet | |
Csatcheck_cadicalt | |
Csatcheck_glucose_baset | |
Csatcheck_glucose_no_simplifiert | |
Csatcheck_glucose_simplifiert | |
Csatcheck_ipasirt | Interface for generic SAT solver interface IPASIR |
Csatcheck_lingelingt | |
Csatcheck_minisat1_baset | |
Csatcheck_minisat1_coret | |
Csatcheck_minisat1_prooft | |
Csatcheck_minisat1t | |
Csatcheck_minisat2_baset | |
Csatcheck_minisat_no_simplifiert | |
Csatcheck_minisat_simplifiert | |
Csatcheck_picosatt | |
Csatcheck_zchaff_baset | |
Csatcheck_zchafft | |
Csatcheck_zcoret | |
Csave_scopet | |
Cscratch_programt | |
Cselect_pointer_typet | |
►Cshared_bufferst | |
Ccfg_visitort | |
Cvarst | |
►Csharing_mapt | A map implemented as a tree where subtrees can be shared between different maps |
Cdelta_view_itemt | |
Csharing_map_statst | Stats about sharing between several sharing map instances |
Csharing_node_baset | |
Csharing_node_innert | |
Csharing_node_leaft | |
Cshift_exprt | A base class for shift operators |
Cshl_exprt | Left shift |
Cshow_goto_functions_jsont | |
Cshow_goto_functions_xmlt | |
Cside_effect_expr_function_callt | A side_effect_exprt representation of a function call side effect |
Cside_effect_expr_nondett | A side_effect_exprt that returns a non-deterministically chosen value |
Cside_effect_expr_throwt | A side_effect_exprt representation of a side effect that throws an exception |
Cside_effect_exprt | An expression containing a side effect |
Csign_exprt | Sign of an expression Predicate is true if _op is negative, false otherwise |
Csignedbv_typet | Fixed-width bit-vector with two's complement interpretation |
Csimplify_exprt | |
Cslicing_criteriont | |
►Csmall_mapt | Map from small integers to values |
Cconst_iterator | Const iterator |
Cconst_value_iterator | Const value iterator |
Csmall_shared_pointeet | A helper class to store use-counts of objects held by small shared pointers |
Csmall_shared_ptrt | This class is really similar to boost's intrusive_pointer, but can be a bit simpler seeing as we're only using it one place |
Csmall_shared_two_way_pointeet | |
Csmall_shared_two_way_ptrt | This class is similar to small_shared_ptrt and boost's intrusive_ptr |
►Csmt2_convt | |
Cidentifiert | |
Clet_count_idt | |
Clet_visitort | |
Csmt2_symbolt | |
Csmt2_dect | Decision procedure interface for various SMT 2.x solvers |
Csmt2_format_containert | |
Csmt2_message_handlert | |
►Csmt2_parsert | |
Cidt | |
Cnamed_termt | |
Csignature_with_parameter_idst | |
Csmt2_solvert | |
Csmt2_stringstreamt | |
►Csmt2_tokenizert | |
Csmt2_errort | |
Csmt2irept | |
►Csolver_factoryt | |
Csolvert | |
Csource_locationt | |
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 |
Csparse_bitvector_analysist | An instance of this class provides an assignment of unique numeric ID to each inserted reaching_definitiont instance |
Csparse_vectort | |
Cssa_exprt | Expression providing an SSA-renamed symbol of expressions |
Cstatic_analysis_baset | |
Cstatic_analysist | |
Cstatic_verifier_resultt | |
Cstream_message_handlert | |
Cstring_abstractiont | |
Cstring_axiomst | |
Cstring_builtin_function_with_no_evalt | Functions that are not yet supported in this class but are supported by string_constraint_generatort |
Cstring_builtin_functiont | Base class for string functions that are built in the solver |
Cstring_concat_char_builtin_functiont | Adding a character at the end of a string |
Cstring_concatenation_builtin_functiont | |
Cstring_constantt | |
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_creation_builtin_functiont | String creation from other types |
►Cstring_dependenciest | Keep track of dependencies between strings |
Cbuiltin_function_nodet | A builtin function node contains a builtin function call |
Cnode_hash | Hash function for nodes |
Cnodet | |
Cstring_nodet | A string node points to builtin_function on which it depends |
Cstring_hash | |
Cstring_insertion_builtin_functiont | String inserting a string into another one |
Cstring_instrumentationt | |
Cstring_not_contains_constraintt | Constraints to encode non containement of strings |
Cstring_of_int_builtin_functiont | String creation from integer types |
Cstring_ptr_hash | |
Cstring_ptrt | |
►Cstring_refinementt | |
Cconfigt | |
Cinfot | String_refinementt constructor arguments |
Cstring_set_char_builtin_functiont | Setting a character at a particular position of a string |
Cstring_test_builtin_functiont | String test |
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_transformation_builtin_functiont | String builtin_function transforming one string into another |
Cstring_typet | String type |
Cstruct_exprt | Struct constructor from list of elements |
Cstruct_tag_typet | A struct tag type, i.e., struct_typet with an identifier |
►Cstruct_typet | Structure type, corresponds to C style structs |
Cbaset | Base class or struct that a class or struct inherits from |
►Cstruct_union_typet | Base type for structs and unions |
Ccomponentt | |
Cstructured_pool_entryt | |
Cstub_global_initializer_factoryt | |
Csubsumed_patht | |
Csymbol_exprt | Expression to hold a symbol (variable) |
Csymbol_factoryt | |
Csymbol_generatort | Generation of fresh symbols of a given type |
►Csymbol_table_baset | The symbol table base class interface |
Citeratort | |
Csymbol_table_buildert | Author: Diffblue Ltd |
Csymbol_tablet | The symbol table |
Csymbol_typet | A reference into the symbol table |
Csymbolt | Symbol table entry |
Csymex_bmct | |
Csymex_configt | Configuration of the symbolic execution |
►Csymex_coveraget | |
Ccoverage_infot | |
Csymex_dereference_statet | |
Csymex_level0t | Functor to set the level 0 renaming of SSA expressions |
Csymex_level1t | Functor to set the level 1 renaming of SSA expressions |
Csymex_level2t | Functor to set the level 2 renaming of SSA expressions |
Csymex_nondet_generatort | Functor generating fresh nondet symbols |
Csymex_renaming_levelt | Wrapper for a current_names map, which maps each identifier to an SSA expression and a counter |
Csymex_slice_by_tracet | |
Csymex_slicet | |
►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 |
CSSA_stept | Single SSA step in the equation |
►Csymex_targett | The interface of the target container for symbolic execution to record its symbolic steps into |
Csourcet | Identifies source in the context of symbolic execution |
Csyntactic_difft | |
Csystem_exceptiont | Thrown when some external system fails unexpectedly |
Csystem_library_symbolst | |
Ctag_typet | A tag-based type, i.e., typet with an identifier |
Ctaint_analysist | |
►Ctaint_parse_treet | |
Crulet | |
Ctdefl_compressor | |
Ctdefl_output_buffer | |
Ctdefl_sym_freq | |
Ctemp_dirt | |
Ctemplate_mapt | |
Ctemplate_numberingt | |
Ctemplate_parametert | |
Ctemplate_typet | |
Ctemporary_filet | |
Cternary_exprt | An expression with three operands |
Ctimestampert | Timestamp class hierarchy |
Ctinfl_decompressor_tag | |
Ctinfl_huff_table | |
Cto_be_merged_irep_hash | |
Cto_be_merged_irept | |
Ctrace_automatont | |
Ctrace_optionst | |
Ctranst | Transition system, consisting of state invariant, initial state predicate, and transition predicate |
Ctrivial_functions_filtert | Filters out trivial functions |
Ctrue_exprt | The Boolean constant true |
Ctvt | |
Ctype_exprt | An expression denoting a type |
Ctype_symbolt | Symbol table entry describing a data type |
Ctype_with_subtypest | Type with multiple subtypes |
Ctype_with_subtypet | Type with a single subtype |
Ctypecast_exprt | Semantic type conversion |
Ctypecheckt | |
Ctypedef_typet | A typedef |
Ctypet | The type of an expression, extends irept |
Cui_message_handlert | |
Cunary_exprt | Generic base class for unary expressions |
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 |
Cuncaught_exceptions_analysist | Computes in exceptions_map an overapproximation of the exceptions thrown by each method |
Cuncaught_exceptions_domaint | |
Cunchecked_replace_symbolt | |
Cunified_difft | |
Cuninitialized_domaint | |
Cuninitializedt | |
Cunion_exprt | Union constructor from single element |
Cunion_find | |
Cunion_find_replacet | Similar interface to union-find for expressions, with a function for replacing sub-expressions by their result for find |
Cunion_tag_typet | A union tag type, i.e., union_typet with an identifier |
Cunion_typet | The union type |
►Cunsigned_union_find | |
Cnodet | |
Cunsignedbv_typet | Fixed-width bit-vector with unsigned binary interpretation |
Cunsupported_java_class_signature_exceptiont | An exception that is raised for unsupported class signature |
Cunsupported_operation_exceptiont | Thrown when we encounter an instruction, parameters to an instruction etc |
Cunwindsett | |
Cupdate_exprt | Operator to update elements in structs and arrays |
Cuser_input_error_exceptiont | |
Cvalue_set_analysis_fit | |
Cvalue_set_analysis_fivrnst | |
Cvalue_set_analysis_fivrt | |
Cvalue_set_analysis_templatet | |
►Cvalue_set_dereferencet | Wrapper for a function dereferencing pointer expressions using a value set |
Cvaluet | Return value for build_reference_to ; see that method for documentation |
Cvalue_set_domain_fit | |
Cvalue_set_domain_fivrnst | |
Cvalue_set_domain_fivrt | |
Cvalue_set_domain_templatet | |
►Cvalue_set_fit | |
Centryt | |
Cobject_map_dt | |
►Cvalue_set_fivrnst | |
Centryt | |
►Cobject_map_dt | |
Cvalidity_ranget | |
►Cvalue_set_fivrt | |
Centryt | |
►Cobject_map_dt | |
Cvalidity_ranget | |
Cvalue_setst | |
►Cvalue_sett | State type in value_set_domaint, used in value-set analysis and goto-symex |
Centryt | Represents a row of a value_sett |
Cobject_map_dt | Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances) |
Cvector_exprt | Vector constructor from list of elements |
Cvector_typet | The vector type |
Cvisited_nodet | A node type with an extra bit |
Cvoid_typet | The void type, the same as empty_typet |
Cw_guardst | |
Cwall_clock_timestampert | |
Cwith_exprt | Operator to update elements in structs and arrays |
Cwrapper_goto_modelt | Class providing the abstract GOTO model interface onto an unrelated symbol table and goto_functionst |
Cxml_edget | |
Cxml_graph_nodet | |
Cxml_interfacet | |
Cxml_parse_treet | |
Cxml_parsert | |
Cxmlt | |
Cxor_exprt | Boolean XOR |
Cyy_buffer_state | |
Cyy_trans_info | |
Cyyalloc | |
CYYSTYPE | |