cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
Here is a list of all variables with links to the classes they belong to:
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
- s -
s :
help_formattert
,
java_bytecode_parsert::pool_entryt
,
postconditiont
,
preconditiont
,
string_ptrt
s0 :
string_not_contains_constraintt
s1 :
string_not_contains_constraintt
S_BITS :
small_mapt< T, Ind, Num >
safe_pointers :
path_storaget
sat_hardness :
solver_hardnesst::assertion_statst
satcheck :
bv_minimizing_dect
,
scratch_programt
satchecker :
scratch_programt
saved_scope :
cpp_save_scopet
saved_target :
goto_symex_statet
scc_count :
grapht< N >::tarjant
scc_stack :
grapht< N >::tarjant
SCIENTIFIC :
format_specifiert
SCIENTIFIC_UPPER :
format_specifiert
scope :
cpp_declarator_convertert
scope_counter :
boolbvt
scope_graph :
scope_treet
scope_ptr :
save_scopet
scope_stack :
goto_convertt::targetst
scopes :
ansi_c_parsert
scores :
fault_location_infot
second :
event_grapht::critical_cyclet::delayt
second_begin :
concat_iteratort< first_iteratort, second_iteratort >
,
zip_iteratort< first_iteratort, second_iteratort, same_size >
second_end :
zip_iteratort< first_iteratort, second_iteratort, same_size >
secondary_scopes :
cpp_idt
section :
c_storage_spect
sections :
osx_mach_o_readert
seen :
memory_snapshot_harness_generatort::preordert< Key >
seen_instances :
string_refinementt
seen_locations :
flow_insensitive_analysis_baset
seen_modes :
compilet
select :
smt_array_theoryt
selection_specs :
recursive_initialization_configt
self_loops_to_assumptions :
symex_configt
sequence :
check_call_sequencet
sese_regions :
sese_region_analysist
set_matcher :
java_class_loader_limitt
set_of_cycles :
instrumentert
set_of_cycles_per_SCC :
instrumentert
set_reads :
rw_set_with_trackt
set_to_new :
linkingt::adjust_type_infot
set_values :
smt2_convt
sets_fc_false :
statement_list_typecheckt::stl_jump_locationt
sh_addr :
Elf32_Shdr
,
Elf64_Shdr
sh_addralign :
Elf32_Shdr
,
Elf64_Shdr
sh_entsize :
Elf32_Shdr
,
Elf64_Shdr
sh_flags :
Elf32_Shdr
,
Elf64_Shdr
sh_info :
Elf32_Shdr
,
Elf64_Shdr
sh_link :
Elf32_Shdr
,
Elf64_Shdr
sh_name :
Elf32_Shdr
,
Elf64_Shdr
sh_offset :
Elf32_Shdr
,
Elf64_Shdr
sh_size :
Elf32_Shdr
,
Elf64_Shdr
sh_type :
Elf32_Shdr
,
Elf64_Shdr
shadow :
shadow_memory_statet::shadowed_addresst
shadow_memory :
goto_symex_statet
,
goto_symext
,
symex_assignt
shared_buffers :
shared_bufferst::cfg_visitort
shared_vars :
concurrency_instrumentationt
shift_left :
smt_bit_vector_theoryt
short_cnt :
ansi_c_convert_typet
short_int_width :
configt::ansi_ct
shorthands :
expr2ct
should_lift_clinit_calls :
java_bytecode_language_optionst
should_pause_symex :
goto_symext
should_simplify :
field_sensitivityt
should_track_value :
constant_propagator_ait
show :
interpretert
show_code :
trace_optionst
show_function_calls :
trace_optionst
show_points_to_sets :
symex_configt
show_symex_steps :
symex_configt
si_byte_symbol :
memory_sizet
si_gibibyte_symbol :
memory_sizet
si_kibibyte_symbol :
memory_sizet
si_mebibyte_symbol :
memory_sizet
side_effects :
goto_convertt::clean_expr_resultt
sign :
float_bvt::unpacked_floatt
,
float_utilst::unpacked_floatt
sign_flag :
ieee_float_valuet
signature :
java_bytecode_parse_treet::classt
,
java_bytecode_parse_treet::membert
,
java_bytecode_parse_treet::methodt::local_variablet
signed_cnt :
ansi_c_convert_typet
signed_divide :
smt_bit_vector_theoryt
signed_greater_than :
smt_bit_vector_theoryt
signed_greater_than_or_equal :
smt_bit_vector_theoryt
signed_less_than :
smt_bit_vector_theoryt
signed_less_than_or_equal :
smt_bit_vector_theoryt
signed_remainder :
smt_bit_vector_theoryt
significand :
parse_floatt
simple_entry :
simple_entryt
simple_invalid_pointer_model :
configt::ansi_ct
simplify_enabled :
api_optionst
simplify_opt :
symex_configt
single_precision_constant :
configt::ansi_ct
single_width :
configt::ansi_ct
size :
__CPROVER_contracts_car_t
,
__CPROVER_jsa_abstract_range
,
data
,
decision_procedure_objectt
,
designatort::entryt
,
osx_mach_o_readert::sectiont
sizeof_nesting :
expr2ct
skeleton :
expr_skeletont
skip_instructions :
java_bytecode_parsert
skip_tracked :
event_grapht::graph_explorert
slots_for_parameters :
java_bytecode_convert_methodt
smt2_conv :
smt2_encoding_targett
smt2_identifiers :
smt2_convt
smt2_tokenizer :
smt2_parsert
smt_get_value_responset :
smt_get_value_responset::valuation_pairt
smt_or_messages :
response_or_errort< smtt >
solver :
goto_symex_fault_localizert
,
goto_symex_property_decidert
,
satcheck_cadical_baset
,
satcheck_glucose_baset< T >
,
satcheck_ipasirt
,
satcheck_lingelingt
,
satcheck_minisat1_baset
,
satcheck_minisat2_baset< T >
,
satcheck_zchaff_baset
,
smt2_convt
,
smt2_solvert
solver_binary_or_empty :
smt2_dect
solver_cmd :
external_satt
solver_hardness :
hardness_collectort
solver_process :
smt2_incremental_decision_proceduret
sorts :
smt2_parsert
source :
goto_symex_statet
,
java_bytecode_convert_methodt::converted_instructiont
,
SSA_stept
source_files :
c_wranglert
,
compilet
source_lines :
cover_basic_blockst::block_infot
source_location :
abstract_eventt
,
allocate_objectst
,
ansi_c_convert_typet
,
cover_basic_blockst::block_infot
,
cpp_typecheck_resolvet
,
cpp_typecheckt::instantiationt
,
encoding_targett
,
flag_overridet
,
framet
,
havoc_assigns_clause_targetst
,
incorrect_goto_program_exceptiont
,
invalid_source_file_exceptiont
,
java_bytecode_parse_treet::instructiont
,
java_bytecode_parse_treet::methodt
,
messaget::mstreamt
,
propertyt
,
static_verifier_resultt
spec :
bv_arithmetict
,
fixedbvt
,
float_utilst
,
ieee_float_valuet
spec_assigns_function_id :
dfcc_contract_functionst
spec_assigns_havoc_function_id :
dfcc_contract_functionst
spec_frees_function_id :
dfcc_contract_functionst
spec_functions :
dfcc_contract_functionst
,
dfcc_contract_handlert
,
dfcc_instrument_loopt
,
dfcc_instrumentt
,
dfcc_swap_and_wrapt
,
dfcct
specialization_args :
cpp_typecheck_resolvet::matcht
specialized :
dfcc_libraryt
squolem :
qbf_squolem_coret
,
qbf_squolemt
ssa_expression :
solver_hardnesst::assertion_statst
,
solver_hardnesst::hardness_ssa_keyt
ssa_full_lhs :
SSA_stept
ssa_function_arguments :
SSA_stept
ssa_lhs :
SSA_stept
ssa_rhs :
SSA_stept
SSA_step :
postconditiont
,
preconditiont
SSA_steps :
symex_target_equationt
st :
instrument_spec_assignst
stack :
java_bytecode_convert_methodt::converted_instructiont
,
java_bytecode_convert_methodt
,
java_bytecode_parse_treet::methodt::stack_map_table_entryt
,
json_parsert
,
parsert
,
write_stackt
,
xml_parsert
stack_caught :
uncaught_exceptions_domaint
stack_map_table :
java_bytecode_parse_treet::methodt
stack_pointer :
interpretert
stack_trace :
trace_optionst
start :
propertyt
start_function :
aggressive_slicert
start_instruction :
memory_snapshot_harness_generatort::entry_locationt
start_pc :
java_bytecode_convert_methodt::holet
,
java_bytecode_convert_methodt::variablet
,
java_bytecode_parse_treet::methodt::exceptiont
,
java_bytecode_parse_treet::methodt::local_variablet
state :
flow_insensitive_analysist< T >
,
path_storaget::patht
,
symex_assignt
,
symex_bmc_incremental_one_loopt
,
symex_dereference_statet
state_fkt_declared :
smt2_convt
state_map :
location_sensitive_storaget
state_prefix :
state_encodingt
states :
check_call_sequencet
static_values_json :
java_bytecode_language_optionst
statistics :
flow_insensitive_analysis_baset
status :
cnf_solvert
,
cover_goalst::goalt
,
main_function_resultt
,
property_infot
,
propertyt
,
satcheck_zchaff_baset
,
smt2_solvert
,
static_verifier_resultt
stdin_file :
goto_cc_cmdlinet
step :
conversion_dependenciest
step_case :
k_inductiont
step_nr :
goto_trace_stept
step_number :
default_trace_stept
steps :
clauset
,
goto_tracet
,
interpretert
stl_labels :
statement_list_typecheckt
stop :
propertyt
storage :
ai_baset
store :
smt_array_theoryt
str :
string_constraint_generatort::parseint_argumentst
STRING :
format_specifiert
string :
api_messaget
,
gdb_apit::pointer_valuet
string_abstraction :
configt::ansi_ct
string_args :
string_builtin_function_with_no_evalt
string_count :
string_container_statisticst
string_input_values :
object_factory_parameterst
string_list :
string_containert
string_literal :
ansi_c_parsert
string_map :
irep_serializationt::ireps_containert
string_nodes :
string_dependenciest
string_numbering :
boolbvt
string_preprocess :
java_bytecode_convert_classt
,
java_bytecode_convert_methodt
,
java_bytecode_languaget
string_printable :
object_factory_parameterst
string_refinement_enabled :
java_bytecode_language_optionst
,
java_bytecode_typecheckt
string_res :
string_builtin_function_with_no_evalt
string_rev_map :
irep_serializationt::ireps_containert
string_struct :
string_abstractiont
string_table_offset :
elf_readert
string_types :
java_string_library_preprocesst
STRING_UPPER :
format_specifiert
string_vector :
string_containert
strings_in_equation :
equation_symbol_mappingt
strings_memory_usage :
string_container_statisticst
stringstream :
smt2_stringstreamt
struct_abstract_type :
vsd_configt
struct_encoding :
smt2_incremental_decision_proceduret
struct_option_mappings :
vsd_configt
stub :
c_wranglert::functiont
stub_global_initializer_factory :
java_bytecode_languaget
stub_globals_by_class :
stub_global_initializer_factoryt
stub_objects_are_not_null :
jbmc_parse_optionst
style :
format_spect
sub :
cpp_idt
,
tree_nodet< treet, named_subtreest, sharing >
sub_enumerators :
alternatives_enumeratort
,
non_leaf_enumeratort
subgraph_nr :
grapht< N >::tarjant
subgraphscount :
dott
subsumed :
acceleratet
,
subsumed_patht
subtract :
smt_bit_vector_theoryt
subtype :
designatort::entryt
succ :
symex_coveraget::coverage_infot
successors :
java_bytecode_convert_methodt::converted_instructiont
,
local_cfgt::nodet
suffix :
cpp_idt
,
goto_convertt::targetst
,
value_set_fit::entryt
,
value_sett::entryt
summarized :
code_contractst
super_class :
java_bytecode_parse_treet::classt
support_float16 :
cpp_parsert
support_float16_type :
cpp_typecheckt
swap_and_wrap :
dfcct
switch_op_type :
c_typecheck_baset
sym_suffix :
string_abstractiont
symbol :
framet
symbol_base_map :
symbol_table_baset
symbol_count :
symbol_generatort
symbol_expr :
dispatch_table_entryt
,
java_bytecode_convert_methodt::variablet
,
rw_set_baset::entryt
symbol_mode :
allocate_objectst
symbol_module_map :
symbol_table_baset
symbol_resolve :
string_refinementt
symbol_table :
acceleratet
,
acceleration_utilst
,
allocate_objectst
,
c_typecheck_baset
,
ci_lazy_methods_neededt
,
code_contractst
,
concurrency_instrumentationt
,
contracts_wranglert
,
disjunctive_polynomial_accelerationt
,
enumerating_loop_accelerationt
,
function_call_harness_generatort::implt
,
gdb_value_extractort
,
get_virtual_calleest
,
goto_convertt
,
goto_model_functiont
,
goto_modelt
,
goto_program2codet
,
goto_symex_statet
,
interpretert
,
java_bytecode_convert_classt
,
java_bytecode_convert_methodt
,
java_bytecode_instrumentt
,
java_bytecode_typecheckt
,
java_object_factoryt
,
java_simple_method_stubst
,
lazy_goto_functions_mapt
,
lazy_goto_modelt
,
object_creation_infot
,
overflow_instrumentert
,
parameter_assignmentst
,
polynomial_acceleratort
,
remove_asmt
,
remove_const_function_pointerst
,
remove_exceptionst
,
remove_function_pointerst
,
remove_instanceoft
,
remove_java_newt
,
remove_returnst
,
remove_virtual_functionst
,
resolve_inherited_componentt
,
sat_path_enumeratort
,
scratch_programt
,
shared_bufferst::cfg_visitort
,
shared_bufferst
,
statement_list_typecheckt
,
string_instrumentationt
,
symbol_factoryt
,
uninitializedt
,
w_guardst
,
wrapper_goto_modelt
symbol_table1 :
namespacet
symbol_table2 :
namespacet
symbol_table_list :
multi_namespacet
symbols :
prop_conv_solvert
,
symbol_table_baset
symbols_created :
allocate_objectst
symex :
multi_path_symex_only_checkert
,
scratch_programt
,
single_loop_incremental_symex_checkert
symex_assign :
shadow_memoryt
symex_config :
goto_symext
,
symex_assignt
symex_coverage :
symex_bmct
symex_initialized :
single_path_symex_checkert
symex_runtime :
single_path_symex_only_checkert
symex_state :
scratch_programt
symex_symbol_table :
multi_path_symex_only_checkert
,
scratch_programt
,
single_loop_incremental_symex_checkert
,
single_path_symex_only_checkert
symex_target :
goto_symex_statet
synthetic_methods :
ci_lazy_methodst
,
java_bytecode_languaget
system_headers :
dump_ct
,
goto_program2codet
system_library_map :
system_library_symbolst
system_symbols :
dump_ct
Generated by
1.17.0