- 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_floatt
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
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 , 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_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 , parsert , propertyt , static_verifier_resultt
spec : bv_arithmetict , fixedbvt , float_utilst , ieee_floatt
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 > , mz_stream_s , 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 : api_messaget
STRING : format_specifiert
string : 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