- a -

abstract_nodes : __CPROVER_jsa_abstract_heap
abstract_ranges : __CPROVER_jsa_abstract_heap
abstract_state : variable_sensitivity_domaint
abstraction_types_map : string_abstractiont
accelerate_limit : acceleratet
accelerated_paths : disjunctive_polynomial_accelerationt , sat_path_enumeratort
accelerator : subsumed_patht
accept_states : automatont
accounted_flags : scope_treet::declaration_statet
accumulator : statement_list_typecheckt
active : index_range_iteratort , value_range_iteratort
active_loops : framet
add : smt_bit_vector_theoryt
addr_of_contract_write_set : dfcc_wrapper_programt
addr_of_ensures_write_set : dfcc_wrapper_programt
addr_of_is_fresh_set : dfcc_wrapper_programt
addr_of_requires_write_set : dfcc_wrapper_programt
addr_of_write_set_var : dfcc_loop_infot
address : gdb_apit::pointer_valuet , java_bytecode_parse_treet::instructiont , propertyt::trace_updatet , shadow_memory_statet::shadowed_addresst
address_fields : shadow_memory_statet
address_map : partial_order_concurrencyt
address_of_exprs : axiomst
address_string : gdb_apit::memory_addresst
address_taken : axiomst , remove_function_pointerst
adjust_function : goto_inlinet
adler : mz_stream_s
affected_by_delay_set : shared_bufferst
alias : c_storage_spect
aliases : escape_domaint , global_may_alias_domaint , local_may_aliast::loc_infot
aligned : ansi_c_convert_typet
aligning : help_formattert::statet
alignment : ansi_c_convert_typet , configt::ansi_ct
all_in_lexical_loop_form : lexical_loops_templatet< P, T, C >
all_nondet : nondet_volatilet
all_rounding_modes : constants_evaluator
allocate_objects : gdb_value_extractort , java_object_factoryt , object_creation_infot , symbol_factoryt
allocated : __CPROVER_contracts_write_set_t
allocated_memory : gdb_apit
allocations : goto_check_ct
allow_allocate : __CPROVER_contracts_write_set_t
allow_deallocate : __CPROVER_contracts_write_set_t
allow_pointer_unsoundness : symex_configt
allow_recursive_calls : dfcct
alphabet : trace_automatont
already_typechecked : java_bytecode_typecheckt
always_flush : console_message_handlert , ui_message_handlert
annotation : state_encodingt
annotations : java_bytecode_parse_treet::classt , java_bytecode_parse_treet::membert , java_qualifierst
anon_count : new_scopet
anon_counter : ansi_c_scopet , cpp_typecheckt
ansi_c : configt
ansi_c_parser : cpp_token_buffert
ansi_c_scanner_state : cpp_token_buffert
any_superclass_has_clinit_method : java_bytecode_convert_methodt
appends : java_bytecode_parse_treet::methodt::stack_map_table_entryt
applications : functionst::function_infot
apply_loop_contracts : loop_contract_configt
approximations : bv_refinementt
arbitrary : nfat< T >::transitiont
arch : configt::ansi_ct
arch_map : gcc_modet
arg : goto_cc_cmdlinet::argt , string_creation_builtin_functiont
argc : cprover_parse_optionst
args : cmdlinet , gdb_apit , java_bytecode_parse_treet::instructiont , string_builtin_function_with_no_evalt , string_insertion_builtin_functiont , string_test_builtin_functiont
argument_count : symex_target_equationt
arguments_may_be_equal : recursive_initialization_configt
argv : cprover_parse_optionst
arithmetic_shift_right : smt_bit_vector_theoryt
arity : non_leaf_enumeratort
array : acceleration_utilst::polynomial_array_assignmentt , jsont , polynomial_acceleratort::polynomial_array_assignment
array_abstract_type : vsd_configt
array_comprehension_args : arrayst
array_constraint_count : arrayst
array_equalities : arrayst
array_length : object_creation_referencet
array_name_to_associated_array_size_variable : recursive_initialization_configt
array_option_mappings : vsd_configt
array_option_size_mappings : vsd_configt
array_pool : string_builtin_functiont , string_constraint_generatort
array_sequence : smt2_incremental_decision_proceduret
array_symbol : concurrency_instrumentationt::shared_vart , concurrency_instrumentationt::thread_local_vart
arrays : arrayst
arrays_of_pointers : array_poolt
asm_block_following : ansi_c_parsert , cpp_parsert
asm_label : c_storage_spect
asm_label_map : c_typecheck_baset
assert_ensures_ctx : __CPROVER_contracts_write_set_t
assert_no_exceptions_thrown : java_bytecode_convert_methodt , java_bytecode_language_optionst
assert_requires_ctx : __CPROVER_contracts_write_set_t
assert_uncaught_exceptions : java_bytecode_language_optionst
assertion : goto_check_ct::conditiont
assertion_stats : solver_hardnesst
assertions : c_wranglert::functiont , goto_check_ct
assign_location : liveness_contextt
assignable_builtin_names : dfcc_libraryt
assigned : pbs_dimacs_cnft
assignment : cnf_clause_list_assignmentt , qbf_qube_coret
assignment_type : goto_trace_stept , SSA_stept , symex_assignt
assignments : gdb_value_extractort
assigns : contract_clausest , dfcc_loop_infot , havoc_utils_can_forward_propagatet , havoc_utilst , loop_contracts_clauset
assigns_map : cegis_verifiert , enumerative_loop_contracts_synthesizert
assume_ensures_ctx : __CPROVER_contracts_write_set_t
assume_inputs_integral : java_object_factory_parameterst
assume_inputs_interval : java_object_factory_parameterst
assume_inputs_non_null : java_bytecode_language_optionst
assume_non_null : java_simple_method_stubst
assume_requires_ctx : __CPROVER_contracts_write_set_t
assumption_stack : prop_conv_solvert
assumptions : smt2_convt
atomic_section_counter : goto_symext
atomic_section_id : goto_statet , goto_symex_statet::threadt , SSA_stept
attribute_bootstrapmethods_read : java_bytecode_parse_treet::classt
attributes : xmlt
auxiliaries : framet
auxiliaries_set : framet
avail_in : mz_stream_s
avail_out : mz_stream_s
available : single_value_index_ranget , single_value_value_ranget
axioms : string_refinementt