| ►Ndetail | |
| Cexpr_try_dynamic_cast_return_typet | |
| Cexpr_dynamic_cast_return_typet | |
| Calways_falset | |
| ►Nrequire_goto_statements | |
| Cpointer_assignment_locationt | |
| Cno_decl_found_exceptiont | |
| ►Nrequire_parse_tree | |
| Cexpected_instructiont | |
| ►Nrequire_type | |
| Cexpected_type_argumentt | |
| ►Nstd | STL namespace |
| Chash< solver_hardnesst::hardness_ssa_keyt > | |
| Chash< string_not_contains_constraintt > | |
| Chash< dstringt > | Default hash function of dstringt for use with STL containers |
| Chash<::symbol_exprt > | |
| C__CPROVER_cegis_instructiont | |
| C__CPROVER_contracts_car_set_t | A set of __CPROVER_contracts_car_t |
| C__CPROVER_contracts_car_t | A conditionally writable range of bytes |
| C__CPROVER_contracts_obj_set_t | A set of pointers |
| C__CPROVER_contracts_write_set_t | Runtime representation of a write set |
| C__CPROVER_jsa_abstract_heap | |
| C__CPROVER_jsa_abstract_node | Abstract nodes may assume any of a set of pre-defined values (value_ref to abstract_ranget) |
| C__CPROVER_jsa_abstract_range | Set of pre-defined, possible values for abstract nodes |
| C__CPROVER_jsa_concrete_node | Concrete node with explicit value |
| C__CPROVER_jsa_iterator | Iterators point to a node and give the relative index within that node |
| C__CPROVER_pipet | |
| C_rw_set_loct | |
| Cabs_exprt | Absolute value |
| Cabstract_aggregate_objectt | |
| Cabstract_aggregate_tag | |
| Cabstract_environmentt | |
| Cabstract_equalert | |
| Cabstract_eventt | |
| Cabstract_goto_modelt | Abstract interface to eager or lazy GOTO models |
| Cabstract_hashert | |
| Cabstract_object_sett | |
| Cabstract_object_statisticst | |
| ►Cabstract_objectt | |
| Cabstract_object_visitort | Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstract_object_pointert |
| Ccombine_result | Clones the first parameter and merges it with the second |
| Cabstract_pointer_objectt | |
| Cabstract_pointer_tag | |
| Cabstract_value_objectt | |
| Cabstract_value_tag | |
| 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 |
| 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++.. |
| Cai_baset | This is the basic interface of the abstract interpreter with default implementations of the core functionality |
| Cai_domain_baset | The interface offered by a domain, allows code to manipulate domains without knowing their exact type |
| Cai_domain_factory_baset | |
| Cai_domain_factory_default_constructort | |
| Cai_domain_factory_location_constructort | |
| Cai_domain_factoryt | |
| ►Cai_history_baset | A history object is an abstraction / representation of the control-flow part of a set of traces |
| Ccompare_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 |
| 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 | An easy factory implementation for histories that don't need parameters |
| Cai_recursive_interproceduralt | |
| Cai_storage_baset | This is the basic interface for storing domains |
| Cai_three_way_merget | |
| Cait | 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) |
| Call_paths_enumeratort | |
| Call_properties_verifier_with_fault_localizationt | Requires an incremental goto checker that is a goto_trace_providert and fault_localization_providert |
| Call_properties_verifier_with_trace_storaget | |
| Call_properties_verifiert | |
| Callocate_exprt | |
| Callocate_objectst | |
| Callocate_state_exprt | |
| Calready_typechecked_exprt | |
| Calready_typechecked_typet | |
| Calternatives_enumeratort | Enumerators that enumerates expressions in the union of enumerated expressions of sub-enumerators |
| Canalysis_exceptiont | Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an error) |
| Cancestry_resultt | Result of an attempt to find ancestor information about two nodes |
| Cand_exprt | Boolean AND |
| Cannotated_pointer_constant_exprt | Pointer-typed bitvector constant annotated with the pointer expression that the bitvector is the numeric representation of |
| 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 | |
| Capi_message_handlert | |
| Capi_messaget | |
| Capi_optionst | |
| Capi_session_implementationt | |
| Capi_sessiont | |
| Carmcc_cmdlinet | |
| Carmcc_modet | |
| Carray_aggregate_typet | |
| Carray_comprehension_exprt | Expression to define a mapping from an argument (index) to elements |
| 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 | |
| Cascii_encoding_targett | |
| Cashr_exprt | Arithmetic right shift |
| Cassembler_parsert | |
| Cassert_criteriont | |
| Cassert_false_generate_function_bodiest | |
| Cassert_false_then_assume_false_generate_function_bodiest | |
| Cassignmentt | Assignment from the rhs value to the lhs variable |
| Cassume_false_generate_function_bodiest | |
| Cat_scope_exitt | |
| Cautomatont | |
| Cauxiliary_symbolt | Internally generated symbol table entryThis is a symbol generated as part of translation to or modification of the intermediate representation |
| Caxiomst | |
| Cbad_cast_exceptiont | |
| Cbase_ref_infot | |
| Cbcc_cmdlinet | |
| 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 |
| Cbinary_exprt | A base class for binary expressions |
| Cbinary_functional_enumeratort | Enumerator that enumerates binary functional expressions |
| Cbinary_overflow_exprt | A Boolean expression returning true, iff operation kind would result in an overflow when applied to operands lhs and rhs |
| 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 |
| Cbinding_exprt | A base class for variable bindings (quantifiers, let, lambda) |
| Cbit_cast_exprt | Reinterpret the bits of an expression of type S as an expression of type T where S and T have the same size |
| Cbitand_exprt | Bit-wise AND |
| Cbitnot_exprt | Bit-wise negation of bit-vectors |
| Cbitor_exprt | Bit-wise OR |
| Cbitreverse_exprt | Reverse the order of bits in a bit-vector |
| Cbitvector_typet | Base class of fixed-width bit-vector types |
| Cbitxnor_exprt | Bit-wise XNOR |
| Cbitxor_exprt | Bit-wise XOR |
| Cbool_typet | The Boolean type |
| ►Cboolbv_mapt | |
| Cmap_entryt | |
| ►Cboolbv_widtht | |
| Cdefined_entryt | |
| Cmembert | |
| ►Cboolbvt | |
| Cquantifiert | |
| Cboundst | |
| Cbswap_exprt | The byte swap expression |
| Cbuild_declaration_hops_inputst | |
| Cbv_arithmetict | |
| Cbv_dimacst | |
| Cbv_endianness_mapt | Map bytes according to the configured endianness |
| Cbv_minimizet | |
| Cbv_minimizing_dect | |
| ►Cbv_pointers_widet | |
| Cpostponedt | |
| ►Cbv_pointerst | |
| Cpostponedt | |
| ►Cbv_refinementt | |
| Capproximationt | |
| Cconfigt | |
| Cinfot | |
| Cbv_spect | |
| Cbv_typet | Fixed-width bit-vector without numerical interpretation |
| Cbv_utilst | |
| Cbyte_extract_exprt | Expression of type type extracted from some object op starting at position offset (given in number of bytes) |
| Cbyte_update_exprt | Expression corresponding to op() where the bytes starting at position offset (given in number of bytes) have been updated with value |
| 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_declarationt | |
| ►Cc_definest | This class maintains a representation of one assignment to the preprocessor macros in a C program |
| Cdefinet | |
| 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_test_input_generatort | |
| Cc_typecastt | |
| Cc_typecheck_baset | |
| ►Cc_wranglert | |
| Cassertiont | |
| Cfunction_contract_clauset | |
| Cfunctiont | |
| Cloop_contract_clauset | |
| Cobjectt | |
| 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_stack_history_factoryt | |
| ►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 |
| Ccall_stack_entryt | |
| Ccall_stackt | |
| Ccall_validate_fullt | |
| Ccall_validatet | |
| Ccan_forward_propagatet | Determine whether an expression is constant |
| Ccar_exprt | Class that represents a normalized conditional address range, with: |
| Ccasting_replace_symbolt | A variant of replace_symbolt that does not require types to match, but instead inserts type casts as needed when replacing one symbol by another |
| Ccbmc_invariants_should_throwt | Helper to enable invariant throwing as above bounded to an object lifetime: |
| Ccbmc_parse_optionst | |
| Ccegis_evaluatort | Evaluator for checking if an expression is consistent with a given set of test cases (positive examples and negative examples) |
| Ccegis_verifiert | Verifier that take a goto program as input, and output formatted counterexamples for counterexample-guided-synthesis |
| Ccerr_message_handlert | |
| Ccext | Formatted counterexample |
| 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 | Dominator graph |
| Cnodet | |
| Ccfg_infot | Stores information about a goto function computed from its CFG |
| Ccfg_instruction_to_dense_integert | 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 |
| Cchange_impactt | |
| Ccharacter_refine_preprocesst | |
| ►Ccheck_call_sequencet | |
| Ccall_stack_entryt | |
| Cstate_hash | |
| Cstatet | |
| Cci_lazy_methods_neededt | |
| ►Cci_lazy_methodst | |
| Cconvert_method_resultt | |
| Ccl_message_handlert | |
| 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_method_descriptor_exprt | An expression describing a method on a class |
| Cclass_typet | Class type |
| Cclause_hardness_collectort | |
| ►Cclauset | |
| Cstept | |
| Ccleanert | Class that allows to clean expressions of side effects and to generate havoc_slice expressions |
| ►Ccmdlinet | |
| ►Coption_namest | |
| Coption_names_iteratort | |
| Coptiont | |
| Ccnf_clause_list_assignmentt | |
| Ccnf_clause_listt | |
| Ccnf_solvert | |
| Ccnft | |
| Ccode_asm_gcct | codet representation of an inline assembler statement, for the gcc flavor |
| 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 goto_instruction_codet representing an assignment in the program |
| Ccode_assumet | An assumption, which must hold in subsequent code |
| Ccode_blockt | A codet representing sequential composition of program statements |
| Ccode_breakt | codet representation of a break statement (within a for or while loop) |
| Ccode_continuet | codet representation of a continue statement (within a for or while loop) |
| Ccode_contractst | |
| Ccode_deadt | A goto_instruction_codet representing the removal of a local variable going out of scope |
| Ccode_declt | A goto_instruction_codet representing the declaration of a local variable |
| Ccode_dowhilet | codet representation of a do while statement |
| Ccode_expressiont | codet representation of an expression statement |
| Ccode_fort | codet representation of a for statement |
| Ccode_frontend_assignt | A codet representing an assignment in the program |
| Ccode_frontend_declt | A codet representing the declaration of a local variable |
| Ccode_frontend_returnt | codet representation of a "return from a function" statement |
| Ccode_function_bodyt | This class is used to interface between a language frontend and goto-convert – it communicates the identifiers of the parameters of a function or method |
| Ccode_function_callt | goto_instruction_codet representation of a function call statement |
| Ccode_gcc_switch_case_ranget | codet representation of a switch-case, i.e. a case statement within a switch |
| Ccode_gotot | codet representation of a goto statement |
| Ccode_ifthenelset | codet representation of an if-then-else statement |
| Ccode_inputt | A goto_instruction_codet representing the declaration that an input of a particular description has a value which corresponds to the value of a given expression (or expressions) |
| Ccode_labelt | codet representation of a label for branch targets |
| Ccode_landingpadt | A statement that catches an exception, assigning the exception in flight to an expression (e.g |
| Ccode_outputt | A goto_instruction_codet representing the declaration that an output of a particular description has a value which corresponds to the value of a given expression (or expressions) |
| Ccode_pop_catcht | Pops an exception handler from the stack of active handlers (i.e |
| ►Ccode_push_catcht | Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 .. |
| Cexception_list_entryt | |
| Ccode_returnt | goto_instruction_codet representation of a "return from a
function" statement |
| Ccode_skipt | A codet representing a skip statement |
| Ccode_switch_caset | codet representation of a switch-case, i.e. a case statement within a switch |
| Ccode_switcht | codet representing a switch statement |
| Ccode_try_catcht | codet representation of a try/catch block |
| ►Ccode_typet | Base type of functions |
| Cparametert | |
| Ccode_whilet | codet representing a while statement |
| Ccode_with_contract_typet | |
| 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 |
| Ccodet | Data structure for representing an arbitrary statement in a program |
| Ccompare_base_name_and_descriptort | |
| 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 |
| Ccomplexity_limitert | Symex complexity module |
| 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 | Base class for concurrency-aware abstract interpretation |
| ►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 |
| Cconditional_target_exprt | Class that represents a single conditional target |
| Cconditional_target_group_exprt | A class for an expression that represents a conditional target or a list of targets sharing a common condition in an assigns clause |
| Ccone_of_influencet | |
| ►Cconfigt | Globally accessible architectural configuration |
| Cansi_ct | |
| Cbv_encodingt | |
| Ccppt | |
| Cjavat | |
| Cverilogt | |
| Cconflict_providert | |
| Cconsole_message_handlert | |
| ►Cconsolet | |
| Credirectt | |
| Cconst_depth_iteratort | |
| Cconst_expr_visitort | |
| Cconst_target_hash | |
| Cconst_unique_depth_iteratort | |
| Cconstant_abstract_valuet | |
| Cconstant_exprt | A constant literal expression |
| Cconstant_index_ranget | |
| Cconstant_interval_exprt | Represents an interval of values |
| Cconstant_pointer_abstract_objectt | |
| Cconstant_propagator_ait | |
| Cconstant_propagator_can_forward_propagatet | |
| ►Cconstant_propagator_domaint | |
| Cvaluest | |
| Cconstants_evaluator | |
| Cconstructor_oft | A type of functor which wraps around the set of constructors of a type |
| Ccontainer_encoding_targett | |
| Ccontext_abstract_objectt | |
| Ccontract_clausest | |
| Ccontracts_wranglert | |
| 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) |
| Ccount_leading_zeros_exprt | The count leading zeros (counting the number of zero bits starting from the most-significant bit) expression |
| Ccount_trailing_zeros_exprt | The count trailing zeros (counting the number of zero bits starting from the least-significant bit) expression |
| Ccounterexample_beautificationt | |
| Ccout_message_handlert | |
| Ccover_assertion_instrumentert | Assertion coverage instrumenter |
| Ccover_assume_instrumentert | |
| 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_goals_verifier_with_trace_storaget | |
| ►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 | |
| Ccprover_parse_optionst | |
| Ccrangler_parse_optionst | |
| Ccscannert | |
| Ccstrlen_exprt | An expression, akin to ISO C's strlen, that denotes the length of a zero-terminated string that starts at the given address |
| Cctokenitt | |
| Cctokent | |
| Ccustom_bitvector_analysist | |
| ►Ccustom_bitvector_domaint | |
| Cvectorst | |
| Ccw_modet | |
| Cd_containert | |
| Cd_internalt | |
| Cd_leaft | |
| ►Cdata_dependency_contextt | |
| Clocation_ordert | |
| Cdata_dpt | |
| Cdatat | |
| Cdeallocate_state_exprt | |
| Cdecision_procedure_objectt | Information the decision procedure holds about each object |
| Cdecision_proceduret | An interface for a decision procedure for satisfiability problems |
| Cdecorated_symbol_exprt | Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_local |
| Cdefault_trace_stept | |
| ►Cdense_integer_mapt | 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 |
| Citerator_templatet | |
| Cdep_edget | |
| 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 |
| 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 |
| Cdeserialization_exceptiont | Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes |
| ►Cdesignatort | |
| Centryt | |
| Cdestructor_and_idt | Result of a tree query holding both destructor codet and the ID of the node that held it |
| Cdestructt | |
| Cdestructt< 0, pointee_baset, Ts... > | |
| Cdfcc_cfg_infot | Computes natural loops, enforces normal form conditions, computes the nesting graph, tags each instruction of the function with the loop ID of the innermost loop and loop instruction type |
| Cdfcc_contract_clauses_codegent | Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that build write sets or havoc write sets |
| Cdfcc_contract_functionst | Generates GOTO functions modelling a contract assigns and frees clauses |
| Cdfcc_contract_handlert | A contract is represented by a function declaration or definition with contract clauses attached to its signature: |
| Cdfcc_instrument_loopt | This class applies the loop contract transformation to a loop in a goto function |
| Cdfcc_instrumentt | This class instruments GOTO functions or instruction sequences for frame condition checking and loop contracts |
| Cdfcc_is_freeablet | Rewrites calls to is_freeable and was_freed predicates in goto programs encoding pre and post conditions |
| Cdfcc_is_fresht | Rewrites calls to is_fresh predicates into calls to the library implementation |
| Cdfcc_libraryt | Class interface to library types and functions defined in cprover_contracts.c |
| Cdfcc_lift_memory_predicatest | |
| Cdfcc_loop_infot | Describes a single loop for the purpose of DFCC loop contract instrumentation |
| Cdfcc_loop_nesting_graph_nodet | A graph node that stores information about a natural loop |
| Cdfcc_obeys_contractt | Rewrites calls to obeys_contract predicates into calls to the library implementation |
| Cdfcc_pointer_in_ranget | Rewrites calls to pointer_in_range predicates into calls to the library implementation |
| Cdfcc_spec_functionst | This class rewrites GOTO functions that use the built-ins: |
| Cdfcc_swap_and_wrapt | |
| Cdfcc_utilst | |
| Cdfcc_wrapper_programt | Generates the body of a wrapper function from a contract specified using requires, assigns, frees, ensures, clauses attached to a function symbol |
| Cdfcct | Entry point into the contracts transformation |
| Cdiagnostics_helpert | 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 | 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 | |
| Cdiv_exprt | Division |
| Cdjb_manglert | Mangle identifiers by hashing their working directory with djb2 hash |
| ►Cdocument_propertiest | |
| Cdoc_claimt | |
| Clinet | |
| Cdoes_remove_constt | |
| Cdott | |
| Cdstring_hash | |
| Cdstringt | dstringt has one field, an unsigned integer no which is an index into a static table of strings |
| Cdump_c_configurationt | Used for configuring the behaviour of dump_c |
| ►Cdump_ct | |
| Ctypedef_infot | |
| Cdynamic_object_exprt | Representation of heap-allocated objects |
| Celement_address_exprt | Operator to return the address of an array element relative to a base address |
| CElf32_Ehdr | |
| CElf32_Shdr | |
| CElf64_Ehdr | |
| CElf64_Shdr | |
| Celf_readert | |
| Cempty_cfg_nodet | |
| Cempty_edget | |
| Cempty_index_ranget | |
| Cempty_typet | The empty type |
| Cempty_union_exprt | Union constructor to support unions without any member (a GCC/Clang feature) |
| Cempty_value_ranget | |
| Cencoding_targett | |
| Cendianness_map_widet | |
| Cendianness_mapt | Maps a big-endian offset to a little-endian offset |
| Center_scope_state_exprt | |
| Cenum_is_in_range_exprt | A Boolean expression returning true, iff the value of an enum-typed symbol equals one of the enum's declared values |
| Cenumerating_loop_accelerationt | |
| Cenumeration_typet | An enumeration type, i.e., a type with elements (not to be confused with C enums) |
| Cenumerative_loop_contracts_synthesizert | Enumerative loop contracts synthesizers |
| Cenumerator_baset | A base class for expression enumerators |
| Cenumerator_factoryt | Factory for enumerator that can be used to represent a tree grammar |
| Cequal_exprt | Equality |
| ►Cequalityt | |
| Ctypestructt | |
| Cequation_symbol_mappingt | Maps equation to expressions contained in them and conversely expressions to equations that contain them |
| Cescape_analysist | |
| ►Cescape_domaint | |
| Ccleanupt | |
| Ceuclidean_mod_exprt | Boute's Euclidean definition of Modulo – to match SMT-LIB2 |
| Ceval_index_resultt | |
| Cevaluate_exprt | |
| ►Cevent_grapht | |
| ►Ccritical_cyclet | |
| Cdelayt | |
| Cgraph_conc_explorert | |
| Cgraph_explorert | |
| Cgraph_pensieve_explorert | |
| Cexists_exprt | An exists expression |
| Cexit_scope_state_exprt | |
| Cexpanding_vectort | |
| Cexpr2c_configurationt | Used for configuring the behaviour of expr2c and type2c |
| Cexpr2cppt | |
| Cexpr2ct | |
| Cexpr2javat | |
| Cexpr2stlt | Class for saving the internal state of the conversion process |
| Cexpr_initializert | |
| Cexpr_protectedt | Base class for all expressions |
| Cexpr_queryt | Wrapper for std::optional<exprt> with useful method for queries to be used in unit tests |
| Cexpr_skeletont | Expression in which some part is missing and can be substituted for another expression |
| Cexpr_visitort | |
| Cexprt | Base class for all expressions |
| Cexternal_satt | |
| 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 |
| Cfat_header_prefixt | |
| Cfault_localization_providert | An implementation of incremental_goto_checkert may implement this interface to provide fault localization information |
| Cfault_location_infot | |
| Cfield_address_exprt | Operator to return the address of a field relative to a base address |
| Cfield_sensitive_ssa_exprt | |
| Cfield_sensitivityt | Control granularity of object accesses |
| 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_filtert | |
| Cfile_name_manglert | Mangle identifiers by including their filename |
| Cfilter_iteratort | Iterator which only stops at elements for which some given function f is true |
| Cfind_first_set_exprt | Returns one plus the index of the least-significant one bit, or zero if the operand is zero |
| Cfind_is_fresh_calls_visitort | Predicate to be used with the exprt::visit() function |
| Cfixed_keys_map_wrappert | |
| Cfixedbv_spect | |
| Cfixedbv_typet | Fixed-width bit-vector with signed fixed-point interpretation |
| Cfixedbvt | |
| Cflag_overridet | Allows to: |
| 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_expr_configt | |
| Cformat_specifiert | Field names follow the OpenJDK implementation: http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/9b8c96f96a0f/src/share/classes/java/util/Formatter.java#l2569 |
| Cformat_spect | |
| Cformat_textt | |
| Cformat_tokent | |
| Cforward_list_as_mapt | Implementation of map-like interface using a forward list |
| Cframe_reft | |
| ►Cframet | Stack frames – these are used for function calls and for exceptions |
| Cactive_loop_infot | |
| Cimplicationt | |
| Cloop_infot | |
| Cfree_form_cmdlinet | An implementation of cmdlinet to be used in tests |
| Cfreert | A functor wrapping std::free |
| Cfrequency_mapt | |
| ►Cfull_array_abstract_objectt | |
| Cmp_integer_hasht | |
| ►Cfull_slicert | |
| Ccfg_nodet | |
| Cfull_struct_abstract_objectt | |
| Cfunction_application_exprt | Application of (mathematical) function |
| Cfunction_assignst | |
| Cfunction_binding_visitort | |
| ►Cfunction_call_harness_generatort | Function harness generator that for a specified goto-function generates a harness that sets up its arguments and calls it |
| Cimplt | This contains implementation details of function call harness generator to avoid leaking them out into the header |
| Cfunction_cfg_infot | |
| 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_itt_hasht | |
| Cfunction_loc_pair_hasht | |
| Cfunction_loc_pairt | |
| Cfunction_name_manglert | Mangles the names in an entire program and its symbol table |
| Cfunction_pointer_restrictionst | |
| Cfunctions_in_scope_visitort | Predicate to be used with the exprt::visit() function |
| ►Cfunctionst | |
| Cfunction_infot | |
| Cfunctiont | |
| Cgcc_cmdlinet | |
| Cgcc_message_handlert | |
| Cgcc_modet | |
| Cgcc_versiont | |
| ►Cgdb_apit | Interface for running and querying GDB |
| Cmemory_addresst | Memory address imbued with the explicit boolean data indicating if the address is null or not |
| Cpointer_valuet | Data associated with the value of a pointer, i.e |
| Cgdb_interaction_exceptiont | |
| ►Cgdb_value_extractort | Interface for extracting values from GDB (building on gdb_apit) |
| Cmemory_scopet | |
| Cgenerate_function_bodies_errort | |
| Cgenerate_function_bodiest | Base class for replace_function_body implementations |
| Cgeneric_parameter_specialization_map_keyst | |
| ►Cgeneric_parameter_specialization_mapt | Author: Diffblue Ltd |
| Ccontainer_paramt | The index of the container and the type parameter inside that container |
| Cprintert | A wrapper for a generic_parameter_specialization_mapt and a namespacet that can be output to a stream |
| Cget_typet | Get the type with the given index in the parameter pack |
| Cget_virtual_calleest | |
| 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_bmc_parse_optionst | |
| ►Cgoto_cc_cmdlinet | |
| Cargt | |
| Cgoto_cc_modet | |
| ►Cgoto_check_ct | |
| Cconditiont | |
| Cgoto_convert_functionst | |
| ►Cgoto_convertt | |
| Cbreak_continue_targetst | |
| Cbreak_switch_targetst | |
| Cclean_expr_resultt | |
| Cleave_targett | |
| Ctargetst | |
| Cthrow_targett | |
| Cgoto_diff_parse_optionst | |
| Cgoto_difft | |
| Cgoto_functionst | A collection of goto functions |
| Cgoto_functiont | A goto function, consisting of function body (see body) and parameter identifiers (see parameter_identifiers) |
| Cgoto_harness_generator_factoryt | Helper to select harness type by name |
| Cgoto_harness_generatort | |
| ►Cgoto_harness_parse_optionst | |
| Cgoto_harness_configt | |
| ►Cgoto_inlinet | |
| ►Cgoto_inline_logt | |
| Cgoto_inline_log_infot | |
| Cgoto_inspect_parse_optionst | |
| Cgoto_instrument_parse_optionst | |
| Cgoto_model_functiont | Interface providing access to a single function in a GOTO model, plus its associated symbol table |
| Cgoto_model_validation_optionst | |
| Cgoto_modelt | |
| Cgoto_null_checkt | Return structure for get_null_checked_expr and get_conditional_checked_expr |
| ►Cgoto_program2codet | |
| Ccaset | |
| Cgoto_program_cfg_infot | For a goto program |
| ►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 |
| Ctarget_less_than | A total order over targett and const_targett |
| Cgoto_statet | Container for data that varies per program point, e.g |
| Cgoto_symex_can_forward_propagatet | |
| Cgoto_symex_fault_localizert | |
| ►Cgoto_symex_property_decidert | Provides management of goal variables that encode properties |
| Cgoalt | |
| ►Cgoto_symex_statet | Central data structure: state |
| Cthreadt | |
| Cgoto_symext | The main class for the forward symbolic simulator |
| Cgoto_synthesizer_parse_optionst | |
| Cgoto_trace_providert | An implementation of incremental_goto_checkert may implement this interface to provide goto traces |
| Cgoto_trace_stept | Step of the trace of a GOTO program |
| Cgoto_trace_storaget | |
| Cgoto_tracet | Trace of a GOTO program |
| ►Cgoto_unwindt | |
| Cunwind_logt | |
| Cgoto_verifiert | An implementation of goto_verifiert checks all properties in a goto model |
| Cgraph_nodet | This class represents a node in a directed graph |
| ►Cgraphml_witnesst | |
| Cpair_hash | |
| Cgraphmlt | |
| ►Cgrapht | A generic directed graph with a parametric node type |
| Ctarjant | |
| Cgreater_than_exprt | Binary greater than operator expression |
| Cgreater_than_or_equal_exprt | Binary greater than or equal operator expression |
| 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 | |
| Cguarded_range_domaint | |
| Chardness_collectort | |
| Chavoc_assigns_clause_targetst | Class to generate havocking instructions for target expressions of a function contract's assign clause (replacement) |
| Chavoc_assigns_targetst | A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_object expressions |
| Chavoc_generate_function_bodiest | |
| Chavoc_if_validt | A class that overrides the low-level havocing functions in the base utility class, to havoc only when expressions point to valid memory, i.e |
| Chavoc_loopst | |
| Chavoc_utils_can_forward_propagatet | A class containing utility functions for havocing expressions |
| Chavoc_utilst | |
| ►Chelp_formattert | |
| Cstatet | |
| Chistory_exprt | A class for an expression that indicates a history variable |
| Chistory_sensitive_storaget | |
| Cidentifiert | |
| Cidentity_functort | Identity functor. When we use C++20 this can be replaced with std::identity |
| 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 |
| 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 |
| 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 |
| Cresultt | |
| Cindeterminate_index_ranget | |
| Cindex_designatort | |
| Cindex_exprt | Array index operator |
| Cindex_range_implementationt | |
| Cindex_range_iteratort | |
| Cindex_ranget | |
| Cindex_set_pairt | |
| Cinductiveness_resultt | |
| Cinfinity_exprt | An expression denoting infinity |
| Cinfix_opt | |
| Cinflate_state | |
| Cinitial_state_exprt | |
| Cinlining_decoratort | Decorator for a message_handlert used during function inlining that collect names of GOTO functions creating warnings and allows to turn inlining warnings into hard errors |
| Cinsert_final_assert_falset | |
| ►Cinstrument_spec_assignst | A class that generates instrumentation for assigns clause checking |
| Clocation_intervalt | Represents an interval of source locations covered by the static local variable search |
| Cinstrumenter_pensievet | |
| ►Cinstrumentert | |
| Ccfg_visitort | |
| Cinteger_bitvector_typet | Fixed-width bit-vector representing a signed or unsigned integer |
| 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 | |
| Cinterval_abstract_valuet | |
| Cinterval_domaint | |
| Cinterval_evaluator | |
| Cinterval_index_ranget | |
| Cinterval_sparse_arrayt | Represents arrays by the indexes up to which the value remains the same |
| Cinterval_templatet | |
| 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 | |
| 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_function_contract_pair_exceptiont | Exception thrown for bad function/contract specification pairs passed on the CLI |
| Cinvalid_input_exceptiont | Thrown when user-provided input cannot be processed |
| Cinvalid_restriction_exceptiont | |
| 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_failure_containingt | |
| Cinvariant_propagationt | |
| Cinvariant_set_domain_factoryt | Pass the necessary arguments to the invariant_set_domaint's when constructed |
| 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 | There are a large number of kinds of tree structured or tree-like data in CPROVER |
| Cis_compile_time_constantt | Architecturally similar to can_forward_propagatet, but specialized for what is a constexpr, i.e., an expression that can be fully evaluated at compile time |
| Cis_cstring_exprt | A predicate that indicates that a zero-terminated string starts at the given address |
| Cis_dynamic_object_exprt | Evaluates to true if the operand is a pointer to a dynamic object |
| Cis_fresh_baset | |
| Cis_fresh_enforcet | |
| Cis_fresh_replacet | |
| Cis_invalid_pointer_exprt | |
| 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_boxed_type_infot | Return type for get_boxed_type_info_by_name |
| Cjava_bytecode_convert_classt | |
| ►Cjava_bytecode_convert_methodt | |
| Cblock_tree_nodet | |
| Cconverted_instructiont | |
| Cholet | |
| Clocal_variable_with_holest | |
| ►Cmethod_with_amapt | |
| Ctarget_less_than | |
| Cvariablet | |
| Cjava_bytecode_instrumentt | |
| Cjava_bytecode_language_optionst | |
| 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 | |
| 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 | |
| Ccomponentt | |
| Cjava_lambda_method_handlet | Represents a lambda call to a method |
| Cmethodt | |
| 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_parameter_tagt | Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T> |
| Cjava_generic_parametert | Reference that points to a java_generic_parameter_tagt |
| 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) |
| Cjava_generic_typet | Reference that points to a java_generic_struct_tag_typet |
| 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_instanceof_exprt | |
| Cjava_method_typet | |
| Cjava_multi_path_symex_checkert | |
| Cjava_multi_path_symex_only_checkert | |
| Cjava_object_factory_parameterst | |
| Cjava_object_factoryt | |
| Cjava_primitive_type_infot | Return type for get_java_primitive_type_info |
| Cjava_qualifierst | |
| Cjava_reference_typet | This is a specialization of reference_typet |
| Cjava_simple_method_stubst | |
| Cjava_single_path_symex_checkert | |
| Cjava_single_path_symex_only_checkert | |
| Cjava_string_library_preprocesst | |
| Cjava_string_literal_exprt | |
| Cjava_syntactic_difft | |
| Cjbmc_parse_optionst | |
| Cjdiff_parse_optionst | |
| 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 |
| 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 | |
| Clabelt | |
| Clambda_exprt | A (mathematical) lambda expression |
| Clanguage_entryt | |
| Clanguage_filest | |
| Clanguage_filet | |
| Clanguage_modulet | |
| Clanguaget | |
| 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 |
| 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 |
| Clazyt | |
| Cld_cmdlinet | |
| Cld_modet | |
| Cleaf_enumeratort | Enumerator that enumerates leaf expressions from a given list |
| Cleft_and_right_valuest | |
| Cless_than_exprt | Binary less than operator expression |
| Cless_than_or_equal_exprt | Binary less than or equal operator expression |
| Clet_exprt | A let expression |
| ►Cletifyt | Introduce LET for common subexpressions |
| Clet_count_idt | |
| Clevenshtein_automatont | Simple automaton that can detect whether a string can be transformed into another with a limited number of deletions, insertions or substitutions |
| Clexical_loops_templatet | Main driver for working out if a class (normally goto_programt) has any lexical loops |
| 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 |
| Clinked_loop_analysist | |
| Clinker_script_merget | Synthesise definitions of symbols that are defined in linker scripts |
| Clinking_diagnosticst | |
| ►Clinkingt | |
| Cadjust_type_infot | |
| Clispexprt | |
| Clispsymbolt | |
| Cliteral_exprt | |
| Cliteral_vector_exprt | |
| Cliteralt | |
| Clive_object_exprt | A predicate that indicates that the object pointed to is live |
| Cliveness_contextt | General implementation of an abstract_objectt which tracks the last written locations for a given abstract_objectt |
| ►Clocal_bitvector_analysist | |
| Cflagst | |
| ►Clocal_cfgt | |
| Cnodet | |
| Clocal_control_flow_decisiont | Records all local control-flow decisions up to a limit of number of histories per location |
| Clocal_control_flow_history_factoryt | |
| Clocal_control_flow_historyt | 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 |
| 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 |
| Ctype_comparet | Comparator that regards type-equal expressions as equal, and otherwise uses the natural (operator<) ordering on irept |
| Clocalst | |
| Clocation_number_less_thant | |
| Clocation_sensitive_storaget | The most conventional storage; one domain per location |
| Clocation_update_visitort | |
| Cloop_analysist | |
| Cloop_cfg_infot | |
| Cloop_contract_configt | Loop contract configurations |
| Cloop_contracts_clauset | |
| Cloop_contracts_synthesizer_baset | A base class for loop contracts synthesizers |
| Cloop_idt | Loop id used to identify loops |
| Cloop_templatet | A loop, specified as a set of instructions |
| Cloop_with_parent_analysis_templatet | |
| 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) |
| Cmax_value_exprt | +∞ upper bound for intervals |
| Cmember_designatort | |
| Cmember_exprt | Extract member of struct or union |
| Cmemory_analyzer_parse_optionst | |
| Cmemory_model_baset | |
| Cmemory_model_psot | |
| Cmemory_model_sct | |
| Cmemory_model_tsot | |
| Cmemory_sizet | |
| ►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 |
| Centry_goto_locationt | User provided goto location: function name and (maybe) location number; the structure wraps this option with a parser |
| Centry_locationt | Wraps the information needed to identify the entry point |
| Centry_source_locationt | User provided source location: file name and line number; the structure wraps this option with a parser |
| Cpreordert | Simple structure for linearising posets |
| Csource_location_matcht | Wraps the information for source location match candidates |
| Cmerge_full_irept | |
| Cmerge_irept | |
| Cmerge_location_update_visitort | |
| 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 | |
| Cmin_value_exprt | -∞ upper bound for intervals |
| Cmini_bdd_applyt | |
| ►Cmini_bdd_mgrt | |
| Creverse_keyt | |
| Cvar_table_entryt | |
| Cmini_bdd_nodet | |
| Cmini_bddt | |
| Cmini_c_parsert | |
| Cminisat_prooft | |
| Cminus_exprt | Binary minus |
| Cminus_overflow_exprt | |
| 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 |
| Cmixd | |
| Cmixf | |
| Cmixl | |
| Cmm_iot | |
| Cmod_exprt | Modulo defined as lhs-(rhs * truncate(lhs/rhs)) |
| ►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 |
| Cmult_overflow_exprt | |
| 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 |
| 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 |
| Cmulti_path_symex_only_checkert | |
| 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 |
| Cnamed_term_exprt | Expression that introduces a new symbol that is equal to the operand |
| 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 | |
| ►Cnfat | Very simple NFA implementation Not super performant, but should be good enough for our purposes |
| Cstatet | A state is a set of possibly active transitions |
| Ctransitiont | |
| Cnil_exprt | The NIL expression |
| Cno_unique_unimplemented_method_exceptiont | |
| Cnon_leaf_enumeratort | Non-leaf enumerator enumerates expressions of form f(a_1, a_2, ..., a_n) where a_i's are sub-expressions enumerated by sub-enumerators |
| Cnon_sharing_treet | Base class for tree-like data structures without sharing |
| Cnondet_instruction_infot | Holds information about any discovered nondet methods, with extreme type- safety |
| Cnondet_padding_exprt | This expression serves as a placeholder for the bits which have non deterministic value in a larger bit vector |
| Cnondet_symbol_exprt | Expression to hold a nondeterministic choice |
| Cnondet_volatilet | |
| 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 | |
| Cnumberingt | |
| 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_address_exprt | Operator to return the address of an object |
| 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_descriptor_exprt | Split an expression into a base object and a (byte) offset |
| Cobject_factory_parameterst | |
| Cobject_idt | |
| Cobject_size_exprt | Expression for finding the size (in bytes) of the object a pointer points to |
| Coffset_entryt | |
| Conehot0_exprt | A Boolean expression returning true iff the given operand consists of exactly one '0' and '1' otherwise |
| Conehot_exprt | A Boolean expression returning true iff the given operand consists of exactly one '1' and '0' otherwise |
| Coperator_entryt | |
| Coptionst | |
| Cor_exprt | Boolean OR |
| Cosx_fat_readert | |
| ►Cosx_mach_o_readert | |
| Csectiont | |
| Coverflow_instrumentert | |
| Coverflow_result_exprt | An expression returning both the result of the arithmetic operation under wrap-around semantics as well as a Boolean to signify overflow |
| Cparameter_assignmentst | |
| Cparameter_symbolt | Symbol table entry of function parameterThis is a symbol generated as part of type checking |
| Cparse_floatt | |
| Cparse_options_baset | |
| CParser | |
| Cparsert | |
| ►Cpartial_order_concurrencyt | Base class for implementing memory models via additional constraints for SSA equations |
| Ca_rect | |
| Cpath_acceleratort | |
| Cpath_enumeratort | |
| 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 |
| 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 | |
| Cpiped_processt | |
| Cplus_exprt | The plus expression Associativity is not specified |
| Cplus_overflow_exprt | |
| Cpointee_address_equalt | Functor to check whether iterators from different collections point at the same object |
| Cpointer_arithmetict | |
| Cpointer_in_range_exprt | Pointer_in_range(a, b, c) evaluates to true iff same_object(a, b, c) ∧ r_ok(a, offset(c)-offset(a)) ∧ a<=b ∧ b<=c Note that the last inequality is weak, i.e., b may be equal to c |
| ►Cpointer_logict | |
| Cpointert | |
| Cpointer_object_exprt | A numerical identifier for the object a pointer points to |
| Cpointer_offset_exprt | The offset (in bytes) of a pointer relative to the object |
| 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 |
| Cprefix_filtert | Provides filtering of strings vai inclusion/exclusion lists of prefixes |
| 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 | |
| Cprop_convt | |
| ►Cprop_minimizet | Computes a satisfying assignment of minimal cost according to a const function using incremental SAT |
| Cobjectivet | |
| Cproperties_criteriont | |
| Cproperty_infot | |
| ►Cpropertyt | |
| Ctrace_statet | |
| Ctrace_updatet | |
| Cprophecy_pointer_in_range_exprt | Pointer_in_range (see pointer_in_range_exprt) with prophecy expressions to encode whether a pointer refers to a deallocated or out-of-scope object |
| Cprophecy_r_ok_exprt | A predicate that indicates that an address range is ok to read |
| Cprophecy_r_or_w_ok_exprt | A base class for a predicate that indicates that an address range is ok to read or write or both |
| Cprophecy_w_ok_exprt | A predicate that indicates that an address range is ok to write |
| 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 | |
| Cquantifier_exprt | A base class for quantifier expressions |
| Cr_ok_exprt | A predicate that indicates that an address range is ok to read |
| Cr_or_w_ok_exprt | A base class for a predicate that indicates that an address range is ok to read or write or both |
| Crange_domain_baset | |
| Crange_domaint | |
| Crange_spect | Data type to describe upper and lower bounds of the range of bits that a read or write access may affect |
| 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_domain_factoryt | This ensures that all domains are constructed with the appropriate pointer back to the analysis engine itself |
| 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 |
| Creallocate_exprt | |
| Creallocate_state_exprt | |
| Crecursion_set_entryt | Recursion-set entry owner class |
| Crecursive_enumerator_placeholdert | Placeholders for actual enumerators, which represent nonterminals |
| Crecursive_initialization_configt | |
| ►Crecursive_initializationt | Class for generating initialisation code for compound structures |
| Cconstructor_keyt | |
| Cref_count_ift | Used in tree_nodet for activating or not reference counting |
| Cref_count_ift< true > | |
| Cref_expr_set_dt | |
| Cref_expr_sett | |
| Creference_allocationt | Allocation code which contains a reference |
| ►Creference_counting | |
| Cdt | |
| Creference_typet | The reference type |
| Crefined_string_exprt | |
| Crefined_string_typet | |
| 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 | |
| Crenamedt | Wrapper for expressions or types which have been renamed up to a given level |
| Creplace_callst | |
| Creplace_history_parametert | |
| Creplace_symbolt | Replace a symbol expression by a given expression |
| Creplacement_predicatet | Patterns of expressions that should be replaced |
| Creplication_exprt | Bit-vector replication |
| Cresolution_prooft | |
| ►Cresolve_inherited_componentt | |
| Cinherited_componentt | |
| Cresponse_or_errort | Holds either a valid parsed response or response sub-tree of type |
| 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_cadical_baset | |
| Csatcheck_cadical_no_preprocessingt | |
| Csatcheck_cadical_preprocessingt | |
| 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 | |
| Csaturating_minus_exprt | Saturating subtraction expression |
| Csaturating_plus_exprt | The saturating plus expression |
| Csave_scopet | |
| ►Cscope_treet | Tree to keep track of the destructors generated along each branch of a function |
| Cdeclaration_statet | |
| Cscope_nodet | |
| Cscratch_program_symext | |
| Cscratch_programt | |
| Cselect_pointer_typet | |
| Cseparate_exprt | A predicate that indicates that the objects pointed to are distinct |
| Csese_region_analysist | |
| Cshadow_memory_field_definitionst | The shadow memory field definitions |
| ►Cshadow_memory_statet | The state maintained by the shadow memory instrumentation during symbolic execution |
| Cshadowed_addresst | |
| Cshadow_memoryt | The shadow memory instrumentation performed during symbolic execution |
| ►Cshared_bufferst | |
| Ccfg_visitort | |
| Cvarst | |
| ►Csharing_mapt | A map implemented as a tree where subtrees can be shared between different maps |
| Cdelta_view_itemt | |
| Cfalset | |
| Cnoop_value_comparatort | |
| Creal_value_comparatort | |
| Csharing_map_statst | Stats about sharing between several sharing map instances |
| Csharing_nodet | |
| Csharing_treet | Base class for tree-like data structures with sharing |
| Cshift_exprt | A base class for shift and rotate operators |
| Cshl_exprt | Left shift |
| Cshl_overflow_exprt | |
| Cshow_goto_functions_jsont | |
| Cshow_goto_functions_xmlt | |
| Cshuffle_vector_exprt | Shuffle elements of one or two vectors, modelled after Clang's __builtin_shufflevector |
| Cside_effect_expr_assignt | A side_effect_exprt that performs an assignment |
| Cside_effect_expr_function_callt | A side_effect_exprt representation of a function call side effect |
| Cside_effect_expr_nondett | A side_effect_exprt that returns a non-deterministically chosen value |
| Cside_effect_expr_overflowt | A Boolean expression returning true, iff the result of performing operation kind on operands a and b in infinite-precision arithmetic cannot be represented in the type of the object that result points to (or the type of result, if it is not a pointer) |
| Cside_effect_expr_statement_expressiont | A side_effect_exprt that contains a statement |
| Cside_effect_expr_throwt | A side_effect_exprt representation of a side effect that throws an exception |
| 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 |
| Csimple_entryt | |
| ►Csimplify_exprt | |
| Cresultt | |
| Csingle_function_filtert | |
| 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 |
| Csingle_path_symex_only_checkert | Uses goto-symex to generate a symex_target_equationt for each path |
| Csingle_value_index_ranget | |
| Csingle_value_value_ranget | |
| Cslicing_criteriont | |
| ►Csmall_mapt | Map from small integers to values |
| Cconst_iterator | Const iterator |
| Cconst_value_iterator | Const value iterator |
| Csmall_shared_n_way_pointee_baset | |
| Csmall_shared_n_way_ptrt | This class is similar to small_shared_ptrt and boost's intrusive_ptr |
| 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 |
| ►Csmt2_convt | |
| Cidentifiert | |
| Csmt2_symbolt | |
| Csmt2_dect | Decision procedure interface for various SMT 2.x solvers |
| Csmt2_encoding_targett | |
| Csmt2_format_containert | |
| ►Csmt2_incremental_decision_proceduret | |
| Csequencet | Generators of sequences of uniquely identifying numbers used for naming SMT functions introduced by the decision procedure |
| Csmt2_message_handlert | |
| Csmt2_parser_error_containingt | |
| Csmt2_parser_test_resultt | |
| ►Csmt2_parsert | |
| Cidt | |
| Cnamed_termt | |
| Csignature_with_parameter_idst | |
| Csmt2_solvert | |
| Csmt2_stringstreamt | |
| ►Csmt2_tokenizert | |
| Csmt2_errort | |
| Csmt2irept | |
| Csmt_array_sortt | |
| ►Csmt_array_theoryt | |
| Cselectt | |
| Cstoret | |
| Csmt_assert_commandt | |
| Csmt_base_solver_processt | |
| Csmt_bit_vector_constant_termt | |
| Csmt_bit_vector_sortt | |
| ►Csmt_bit_vector_theoryt | |
| Caddt | |
| Candt | |
| Carithmetic_shift_rightt | |
| Ccomparet | |
| Cconcatt | |
| Cextractt | |
| Clogical_shift_rightt | |
| Cmultiplyt | |
| Cnandt | |
| Cnegatet | |
| Cnort | |
| Cnott | |
| Cort | |
| Crepeatt | |
| Crotate_leftt | |
| Crotate_rightt | |
| Cshift_leftt | |
| Csign_extendt | |
| Csigned_dividet | |
| Csigned_greater_than_or_equalt | |
| Csigned_greater_thant | |
| Csigned_less_than_or_equalt | |
| Csigned_less_thant | |
| Csigned_remaindert | |
| Csubtractt | |
| Cunsigned_dividet | |
| Cunsigned_greater_than_or_equalt | |
| Cunsigned_greater_thant | |
| Cunsigned_less_than_or_equalt | |
| Cunsigned_less_thant | |
| Cunsigned_remaindert | |
| Cxnort | |
| Cxort | |
| Czero_extendt | |
| Csmt_bool_literal_termt | |
| Csmt_bool_sortt | |
| Csmt_check_sat_commandt | |
| ►Csmt_check_sat_response_kindt | |
| Cstorert | Class for adding the ability to up and down cast smt_check_sat_response_kindt to and from irept |
| Csmt_check_sat_responset | |
| Csmt_command_const_downcast_visitort | |
| Csmt_command_functiont | A function generated from a command |
| Csmt_command_to_string_convertert | |
| Csmt_commandt | |
| ►Csmt_core_theoryt | |
| Candt | |
| Cdistinctt | |
| Cequalt | |
| Cif_then_elset | |
| Cimpliest | |
| Cnott | |
| Cort | |
| Cxort | |
| Csmt_declare_function_commandt | |
| Csmt_define_function_commandt | |
| Csmt_error_responset | |
| Csmt_exists_termt | |
| Csmt_exit_commandt | |
| Csmt_forall_termt | |
| ►Csmt_function_application_termt | |
| Cfactoryt | |
| Chas_indicest | |
| Chas_indicest< functiont, std::void_t< decltype(std::declval< functiont >().indices())> > | |
| Csmt_get_value_commandt | |
| ►Csmt_get_value_responset | |
| Cvaluation_pairt | |
| Csmt_identifier_termt | Stores identifiers in unescaped and unquoted form |
| Csmt_incremental_dry_run_solvert | Class for an incremental SMT solver used in combination with --outfile argument where the solver is never run |
| Csmt_index_const_downcast_visitort | |
| Csmt_index_output_visitort | |
| ►Csmt_indext | For implementation of indexed identifiers |
| Cstorert | Class for adding the ability to up and down cast smt_indext to and from irept |
| Csmt_is_dynamic_objectt | Specifics of how the dynamic object status lookup is implemented in SMT terms |
| Csmt_logic_const_downcast_visitort | |
| Csmt_logic_to_string_convertert | |
| ►Csmt_logict | |
| Cstorert | Class for adding the ability to up and down cast smt_logict to and from irept |
| Csmt_numeral_indext | |
| Csmt_object_sizet | Specifics of how the object size lookup is implemented in SMT terms |
| Csmt_option_const_downcast_visitort | |
| Csmt_option_produce_modelst | |
| Csmt_option_to_string_convertert | |
| ►Csmt_optiont | |
| Cstorert | Class for adding the ability to up and down cast smt_optiont to and from irept |
| Csmt_piped_solver_processt | |
| Csmt_pop_commandt | |
| Csmt_push_commandt | |
| Csmt_responset | |
| Csmt_sat_responset | |
| Csmt_set_logic_commandt | |
| Csmt_set_option_commandt | |
| Csmt_sort_const_downcast_visitort | |
| Csmt_sort_output_visitort | |
| ►Csmt_sortt | |
| Cstorert | Class for adding the ability to up and down cast smt_sortt to and from irept |
| Csmt_success_responset | |
| Csmt_symbol_indext | |
| Csmt_term_const_downcast_visitort | |
| Csmt_term_to_string_convertert | |
| ►Csmt_termt | |
| Cstorert | Class for adding the ability to up and down cast smt_termt to and from irept |
| Csmt_unknown_responset | |
| Csmt_unsat_responset | |
| Csmt_unsupported_responset | |
| ►Csolver_factoryt | |
| Csolvert | |
| ►Csolver_hardnesst | A structure that facilitates collecting the complexity statistics from a decision procedure |
| Cassertion_statst | |
| Chardness_ssa_keyt | |
| Csat_hardnesst | |
| Csolver_optionst | |
| Csolver_progresst | |
| Csolver_resource_limitst | |
| Csort_based_cast_to_bit_vector_convertert | |
| Csort_based_literal_convertert | |
| Csorted_variablest | |
| Csource_linest | |
| 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_assignment_stept | |
| Cssa_exprt | Expression providing an SSA-renamed symbol of expressions |
| CSSA_stept | Single SSA step in the equation |
| Cstack_decision_proceduret | |
| Cstate_cstrlen_exprt | |
| Cstate_encoding_smt2_convt | |
| Cstate_encodingt | |
| Cstate_is_cstring_exprt | |
| Cstate_is_dynamic_object_exprt | |
| Cstate_is_sentinel_dll_exprt | |
| Cstate_live_object_exprt | |
| Cstate_object_size_exprt | |
| Cstate_ok_exprt | |
| Cstate_type_compatible_exprt | |
| Cstate_typet | |
| Cstate_writeable_object_exprt | |
| Cstatement_list_languaget | Implements the language interface for the Statement List language |
| ►Cstatement_list_parse_treet | Intermediate representation of a parsed Statement List file before converting it into a goto program |
| Cfunction_blockt | Structure for a simple function block in Statement List |
| Cfunctiont | Structure for a simple function in Statement List |
| Cinstructiont | Represents a regular Statement List instruction which consists out of one or more codet tokens |
| Cnetworkt | Representation of a network in Siemens TIA |
| Ctia_modulet | Base element of all modules in the Totally Integrated Automation (TIA) portal by Siemens |
| Cvar_declarationt | Struct for a single variable declaration in Statement List |
| Cstatement_list_parsert | Responsible for starting the parse process and to translate the result into a statement_list_parse_treet |
| ►Cstatement_list_typecheckt | Class for encapsulating the current state of the type check |
| Cnesting_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 |
| Cstl_jump_locationt | Holds information about the properties of a jump instruction |
| Cstl_label_locationt | Holds information about the instruction and the nesting depth to which a label points |
| Cstatic_verifier_resultt | The result of verifying a single assertion As well as the status of the assertion (see above), it also contains the location (source_location and function_id) and the set of histories in which the assertion is unknown or false, so that more detailed post-processing or error output can be done |
| Cstop_on_fail_verifier_with_fault_localizationt | 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 | Stops when the first failing property is found |
| Cstream_message_handlert | |
| Cstring_abstractiont | Replace all uses of char * by a struct that carries that string, and also the underlying allocation and the C string length |
| Cstring_axiomst | |
| Cstring_builtin_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 | |
| Cparseint_argumentst | Argument block for parseInt and cousins, common to parseInt itself and CProverString.isValidInt |
| Cstring_constraintst | Collection of constraints of different types: existential formulas, universal formulas, and "not contains" (universal with one alternation) |
| Cstring_constraintt | |
| Cstring_container_statisticst | Has estimated statistics about string container (estimated because this only uses public information, which disregards any internal control structures that might be in use) |
| Cstring_containert | |
| Cstring_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_format_builtin_functiont | Built-in function for String.format() |
| 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_aggregate_typet | |
| Cstruct_encodingt | Encodes struct types/values into non-struct expressions/types |
| Cstruct_exprt | Struct constructor from list of elements |
| Cstruct_or_union_tag_typet | A struct or union tag type |
| Cstruct_tag_typet | A struct tag type, i.e., struct_typet with an identifier |
| ►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_data_entryt | |
| Cstructured_datat | A way of representing nested key/value data |
| 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 |
| Csymbolt | Symbol table entry |
| Csymex_assignt | Functor for symex assignment |
| Csymex_bmc_incremental_one_loopt | |
| Csymex_bmct | |
| 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 | |
| Ccoverage_infot | |
| 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 |
| 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_target_equationt | Inheriting the interface of symex_targett this class represents the SSA form of the input program as a list of SSA_stept |
| ►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 |
| Csymtab2gb_parse_optionst | |
| 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 | |
| Ctake_time_resourcet | |
| Ctdefl_compressor | |
| Ctdefl_output_buffer | |
| Ctdefl_sym_freq | |
| Ctemp_dirt | |
| Ctemplate_mapt | |
| Ctemplate_parameter_symbol_typet | Template parameter symbol that is a type |
| Ctemplate_parametert | |
| Ctemplate_typet | |
| Ctemporary_filet | |
| Cternary_exprt | An expression with three operands |
| Ctest_inputst | |
| Ctimestampert | Timestamp class hierarchy |
| Ctinfl_decompressor_tag | |
| Ctinfl_huff_table | |
| Cto_be_merged_irep_hash | |
| Cto_be_merged_irept | |
| Ctrace_automatont | |
| Ctrace_map_storaget | |
| Ctrace_optionst | Options for printing the trace using show_goto_trace |
| Ctranst | Transition system, consisting of state invariant, initial state predicate, and transition predicate |
| Ctree_nodet | A node with data in a tree, it contains: |
| Ctrivial_functions_filtert | Filters out trivial functions |
| Ctrue_exprt | The Boolean constant true |
| Ctuple_exprt | |
| Ctvt | |
| Ctwo_value_array_abstract_objectt | |
| Ctwo_value_pointer_abstract_objectt | |
| Ctwo_value_struct_abstract_objectt | |
| Ctwo_value_union_abstract_objectt | |
| Ctype_exprt | An expression denoting a type |
| Ctype_symbolt | Symbol table entry describing a data typeThis is a symbol generated as part of type checking |
| Ctype_with_subtypest | Type with multiple subtypes |
| Ctype_with_subtypet | Type with a single subtype |
| Ctypecast_exprt | Semantic type conversion |
| ►Ctypecheckt | |
| Cerrort | |
| 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_minus_overflow_exprt | A Boolean expression returning true, iff negation would result in an overflow when applied to the (single) operand |
| Cunary_overflow_exprt | A Boolean expression returning true, iff operation kind would result in an overflow when applied to the (single) operand |
| 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 | |
| Cuninitialized_typet | |
| Cuninitializedt | |
| Cunion_aggregate_typet | |
| 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_bit_exprt | Replaces a sub-range of a bit-vector operand |
| Cupdate_bits_exprt | Replaces a sub-range of a bit-vector operand |
| Cupdate_exprt | Operator to update elements in structs and arrays |
| Cupdate_state_exprt | |
| Cuser_input_error_exceptiont | |
| Cvalue_expr_from_smt_factoryt | |
| Cvalue_range_implementationt | |
| Cvalue_range_iteratort | |
| Cvalue_ranget | |
| Cvalue_set_abstract_objectt | |
| Cvalue_set_analysis_fit | |
| Cvalue_set_analysis_templatet | 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_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_templatet | This is the domain for a value set analysis |
| Cvalue_set_evaluator | |
| ►Cvalue_set_fit | |
| Centryt | |
| Cobject_map_dt | |
| Cvalue_set_index_ranget | |
| Cvalue_set_pointer_abstract_objectt | |
| Cvalue_set_tag | |
| Cvalue_set_value_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 |
| Cvariable_sensitivity_dependence_domain_factoryt | This ensures that all domains are constructed with the node ID that links them to the graph part of the dependency graph |
| ►Cvariable_sensitivity_dependence_domaint | |
| Cdependency_ordert | |
| Cvariable_sensitivity_dependence_grapht | |
| Cvariable_sensitivity_domain_factoryt | |
| Cvariable_sensitivity_domaint | |
| Cvariable_sensitivity_object_factoryt | |
| Cvector_exprt | Vector constructor from list of elements |
| Cvector_typet | The vector type |
| ►Cverification_resultt | |
| Cverification_result_implt | |
| Cvisited_nodet | A node type with an extra bit |
| Cvs_dep_edget | |
| Cvs_dep_nodet | |
| Cvsd_configt | |
| Cw_guardst | |
| Cw_ok_exprt | A predicate that indicates that an address range is ok to write |
| Cwall_clock_timestampert | |
| Cwidened_ranget | |
| Cwith_exprt | Operator to update elements in structs and arrays |
| Cwitness_providert | An implementation of incremental_goto_checkert may implement this interface to provide GraphML witnesses |
| Cworkt | |
| Cwrapper_goto_modelt | Class providing the abstract GOTO model interface onto an unrelated symbol table and goto_functionst |
| Cwrite_location_contextt | General implementation of an abstract_objectt which tracks the last written locations for a given abstract_objectt |
| Cwrite_stack_entryt | |
| Cwrite_stackt | |
| Cwriteable_object_exprt | A predicate that indicates that the object pointed to is writeable |
| Cxml_edget | |
| Cxml_graph_nodet | |
| Cxml_parse_treet | |
| Cxml_parsert | |
| Cxmlt | |
| Cxor_exprt | Boolean XOR |
| Czero_extend_exprt | Zero extension The operand is converted to the given type by either a) truncating if the new type is shorter, or b) padding with most-significant zero bits if the new type is larger, or c) reinterprets the operand as the given type if their widths match |
| Czip_iteratort | Zip two ranges to make a range of pairs |
1.9.1