►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< solver_hardnesst::hardness_ssa_keyt > | |
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 |
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_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 |
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_objectst | |
Calready_typechecked_exprt | |
Calready_typechecked_typet | |
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_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_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 | |
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 | |
Cautomatont | |
Cauxiliary_symbolt | Internally generated symbol table entryThis is a symbol generated as part of translation to or modification of the intermediate representation |
Cbad_cast_exceptiont | |
Cbase_ref_infot | |
Cbase_type_eqt | |
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_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) |
Cbitand_exprt | Bit-wise AND |
Cbitnot_exprt | Bit-wise negation of bit-vectors |
Cbitor_exprt | Bit-wise OR |
Cbitvector_typet | Base class of fixed-width bit-vector types |
Cbitxor_exprt | Bit-wise XOR |
Cbool_typet | The Boolean type |
►Cboolbv_mapt | |
Cmap_bitt | |
Cmap_entryt | |
►Cboolbv_widtht | |
Centryt | |
Cmembert | |
►Cboolbvt | |
Cquantifiert | |
Cboundst | |
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 | 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_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 | |
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 | |
Ccasting_replace_symbolt | |
Ccbmc_invariants_should_throwt | Helper to enable invariant throwing as above bounded to an object lifetime: |
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 | Dominator graph |
Cnodet | |
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 |
►Cclauset | |
Cstept | |
►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 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_bodyt | This class is used to interface between a language frontend and goto-convert – it communicates the identifiers of the parameters of a function or method |
Ccode_function_callt | codet representation of a function call statement |
Ccode_gcc_switch_case_ranget | codet representation of a switch-case, i.e. a case statement within a switch |
Ccode_gotot | codet representation of a goto statement |
Ccode_ifthenelset | codet representation of an if-then-else statement |
Ccode_inputt | A codet representing the declaration that an input of a particular description has a value which corresponds to the value of a given expression (or expressions) |
Ccode_labelt | codet representation of a label for branch targets |
Ccode_landingpadt | A statement that catches an exception, assigning the exception in flight to an expression (e.g |
Ccode_outputt | A codet representing the declaration that an output of a particular description has a value which corresponds to the value of a given expression (or expressions) |
Ccode_pop_catcht | Pops an exception handler from the stack of active handlers (i.e |
►Ccode_push_catcht | Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 .. |
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 |
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_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 | |
Cconflict_providert | |
Cconsole_message_handlert | |
Cconst_depth_iteratort | |
Cconst_expr_visitort | |
Cconst_target_hash | |
Cconst_unique_depth_iteratort | |
Cconstant_exprt | A constant literal expression |
Cconstant_interval_exprt | Represents an interval of values |
Cconstant_propagator_ait | |
►Cconstant_propagator_domaint | |
Cvaluest | |
Cconstant_propagator_is_constantt | |
Cconstructor_oft | A type of functor which wraps around the set of constructors of a type |
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_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 | |
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 |
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 |
►Cdestructor_treet | Tree to keep track of the destructors generated along each branch of a function |
Cdestructor_nodet | |
Cdestructt | |
Cdestructt< 0, pointee_baset, Ts... > | |
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 | |
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_c_configurationt | Used for configuring the behaviour of dump_c |
►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_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 | |
Cexpr2stlt | Class for saving the internal state of the conversion process |
Cexpr_initializert | |
Cexpr_protectedt | Base class for all expressions |
Cexpr_queryt | Wrapper for optionalt<exprt> with useful method for queries to be used in unit tests |
Cexpr_skeletont | Expression in which some part is missing and can be substituted for another expression |
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_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 | |
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 |
Cfixed_keys_map_wrappert | |
Cfixedbv_spect | |
Cfixedbv_typet | Fixed-width bit-vector with signed fixed-point interpretation |
Cfixedbvt | |
Cflag_resett | Set a Boolean flag to a new value (via set_flag ) and restore the previous value when the entire object goes out of scope |
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 | 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 |
►Cframet | Stack frames – these are used for function calls and for exceptions |
Cactive_loop_infot | |
Cloop_infot | |
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_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_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 | |
Cfunction_name_manglert | Mangles the names in an entire program and its symbol table |
►Cfunction_pointer_restrictionst | |
Cinvalid_restriction_exceptiont | |
►Cfunctionst | |
Cfunction_infot | |
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_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_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_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_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_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_statet | Container for data that varies per program point, e.g |
Cgoto_symex_fault_localizert | |
Cgoto_symex_is_constantt | |
►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_trace_constant_pointer_exprt | Variety of constant expression only used in the context of a GOTO trace, to give both the numeric value and the symbolic value of a pointer, e.g |
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 | |
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_generate_function_bodiest | |
Chavoc_loopst | |
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 |
Cincorrect_source_program_exceptiont | |
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 | |
Cindex_designatort | |
Cindex_exprt | Array index operator |
Cindex_set_pairt | |
Cinfinity_exprt | An expression denoting infinity |
Cinfix_opt | |
Cinflate_state | |
Cinode | |
Cinsert_final_assert_falset | |
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_domaint | |
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_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 | Author: Diffblue Ltd |
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_constantt | Determine whether an expression is constant |
Cis_dynamic_object_exprt | Evaluates to true if the operand is a pointer to a dynamic object |
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 | |
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 |
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 | |
Clabelt | |
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 | |
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 |
►Clinkingt | |
Cadjust_type_infot | |
Clispexprt | |
Clispsymbolt | |
Cliteral_exprt | |
Cliteralt | |
►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_sensitive_storaget | The most conventional storage; one domain per location |
Cloop_analysist | |
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_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_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 | |
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_exprt | -∞ upper bound for intervals |
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 |
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 |
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_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_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 | |
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_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 | |
Coperator_entryt | |
Coptionst | |
Cor_exprt | Boolean OR |
Cosx_fat_readert | |
►Cosx_mach_o_readert | |
Csectiont | |
Coverflow_instrumentert | |
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 | |
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 |
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 | |
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_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 |
Crecursion_set_entryt | Recursion-set entry owner class |
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 | |
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 | |
Crenamedt | Wrapper for expressions or types which have been renamed up to a given level |
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 | |
Creturn_value_visitort | Predicate to be used with the exprt::visit() function |
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 | |
Csese_region_analysist | |
►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 operators |
Cshl_exprt | Left shift |
Cshow_goto_functions_jsont | |
Cshow_goto_functions_xmlt | |
Cside_effect_expr_assignt | A side_effect_exprt that performs an assignment |
Cside_effect_expr_function_callt | A side_effect_exprt representation of a function call side effect |
Cside_effect_expr_nondett | A side_effect_exprt that returns a non-deterministically chosen value |
Cside_effect_expr_statement_expressiont | A side_effect_exprt that contains a statement |
Cside_effect_expr_throwt | A side_effect_exprt representation of a side effect that throws an exception |
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 | |
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 |
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_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 | |
►Csolver_hardnesst | A structure that facilitates collecting the complexity statistics from a decision procedure |
Cassertion_statst | |
Chardness_ssa_keyt | |
Csat_hardnesst | |
Csolver_resource_limitst | |
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 | |
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 |
Cstatic_analysis_baset | |
Cstatic_analysist | |
Cstatic_verifier_resultt | |
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_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_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_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 | |
Ctdefl_compressor | |
Ctdefl_output_buffer | |
Ctdefl_sym_freq | |
Ctemp_dirt | |
Ctemplate_mapt | |
Ctemplate_numberingt | |
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 | |
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 | |
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 | |
Cuninitialized_typet | |
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 | 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_fivrnst | |
Cvalue_set_domain_fivrt | |
Cvalue_set_domain_templatet | This is the domain for a value set analysis |
►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 |
Cvector_exprt | Vector constructor from list of elements |
Cvector_typet | The vector type |
Cvisited_nodet | A node type with an extra bit |
Cw_guardst | |
Cwall_clock_timestampert | |
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 |
Cwrapper_goto_modelt | Class providing the abstract GOTO model interface onto an unrelated symbol table and goto_functionst |
Cxml_edget | |
Cxml_graph_nodet | |
Cxml_parse_treet | |
Cxml_parsert | |
Cxmlt | |
Cxor_exprt | Boolean XOR |
Czip_iteratort | Zip two ranges to make a range of pairs |