cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
Here is a list of all file members with links to the files 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 -
s1 :
bytecode_info.h
s2 :
bytecode_info.h
s4 :
bytecode_info.h
s8 :
bytecode_info.h
safe_string2size_t() :
string2int.cpp
,
string2int.h
safe_string2unsigned() :
string2int.cpp
,
string2int.h
saj_table :
simplify_utils.cpp
same_address() :
may_alias.cpp
same_object() :
pointer_predicates.cpp
,
pointer_predicates.h
same_source_line() :
cover_basic_blocks.cpp
SCOPE_SEPARATOR :
expr2statement_list.cpp
send_function_definition() :
smt2_incremental_decision_procedure.cpp
sentinel_dll_member() :
sentinel_dll.cpp
sentinel_dll_next() :
sentinel_dll.cpp
,
sentinel_dll.h
sentinel_dll_prev() :
sentinel_dll.cpp
,
sentinel_dll.h
set_class_identifier() :
class_identifier.cpp
,
class_identifier.h
set_contains() :
value_set_abstract_object.cpp
set_declaring_class() :
java_utils.cpp
,
java_utils.h
set_has_extremes() :
value_set_abstract_object.cpp
set_internal_dynamic_object() :
build_goto_trace.cpp
set_predicate_fn :
value_set_abstract_object.cpp
set_properties() :
set_properties.cpp
,
set_properties.h
SET_RETURN_VALUE :
goto_program.h
set_up_custom_entry_point() :
initialize_goto_model.cpp
,
initialize_goto_model.h
setup_frames() :
solver_types.cpp
,
solver_types.h
SHADOW_MEMORY_FIELD_DECL :
shadow_memory.h
SHADOW_MEMORY_GET_FIELD :
shadow_memory.h
SHADOW_MEMORY_GLOBAL_SCOPE :
shadow_memory.h
SHADOW_MEMORY_LOCAL_SCOPE :
shadow_memory.h
shadow_memory_log_get_field() :
shadow_memory_util.cpp
,
shadow_memory_util.h
shadow_memory_log_set_field() :
shadow_memory_util.cpp
,
shadow_memory_util.h
shadow_memory_log_text_and_expr() :
shadow_memory_util.cpp
,
shadow_memory_util.h
shadow_memory_log_value_set() :
shadow_memory_util.cpp
,
shadow_memory_util.h
shadow_memory_log_value_set_match() :
shadow_memory_util.cpp
,
shadow_memory_util.h
SHADOW_MEMORY_PREFIX :
shadow_memory.h
SHADOW_MEMORY_SET_FIELD :
shadow_memory.h
SHADOW_MEMORY_SYMBOL_PREFIX :
shadow_memory.h
SHARING :
irep.h
SHARING_MAPT :
sharing_map.h
SHARING_MAPT2 :
sharing_map.h
SHARING_MAPT3 :
sharing_map.h
SHARING_MAPT4 :
sharing_map.h
sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::bits :
sharing_map.h
sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::chunk :
sharing_map.h
sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::dummy_level :
sharing_map.h
sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::levels :
sharing_map.h
sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::mask :
sharing_map.h
SHARING_MAPTV :
sharing_map.h
sharing_ptrt :
abstract_object.h
sharing_treet< derivedt, named_subtreest >::empty_d :
irep.h
shell_quote() :
run.cpp
,
run.h
shl_overflow_result() :
boolbv_overflow.cpp
should_init_symbol() :
java_entry_point.cpp
should_use_local_definition_for() :
value_set_dereference.cpp
show_assignment() :
counterexample_found.cpp
,
counterexample_found.h
show_byte_op_plain() :
show_program.cpp
show_byte_ops() :
show_program.cpp
,
show_program.h
show_byte_ops_json() :
show_program.cpp
show_byte_ops_plain() :
show_program.cpp
show_byte_ops_xml() :
show_program.cpp
show_call_sequences() :
call_sequences.cpp
,
call_sequences.h
show_class_hierarchy() :
class_hierarchy.cpp
,
class_hierarchy.h
show_compact_goto_trace() :
goto_trace.cpp
show_full_goto_trace() :
goto_trace.cpp
show_functions_with_loops() :
cprover_parse_options.cpp
show_goto_functions() :
cprover_parse_options.cpp
,
show_goto_functions.cpp
,
show_goto_functions.h
show_goto_stack_trace() :
goto_trace.cpp
show_goto_trace() :
goto_trace.cpp
,
goto_trace.h
show_lexical_loops() :
lexical_loops.h
show_location() :
show_on_source.cpp
show_locations() :
show_locations.cpp
,
show_locations.h
show_loop_ids() :
loop_ids.cpp
,
loop_ids.h
show_loop_ids_json() :
loop_ids.cpp
show_loops() :
loop_analysis.h
show_natural_loops() :
natural_loops.h
show_on_source() :
show_on_source.cpp
,
show_on_source.h
show_path_strategies() :
path_storage.cpp
,
path_storage.h
show_program() :
show_program.cpp
,
show_program.h
show_properties() :
show_properties.cpp
,
show_properties.h
show_properties_json() :
show_properties.cpp
show_ssa_step_plain() :
show_program.cpp
show_state_header() :
goto_trace.cpp
show_step() :
show_program.cpp
show_symbol_table() :
show_symbol_table.cpp
,
show_symbol_table.h
show_symbol_table_brief() :
show_symbol_table.cpp
,
show_symbol_table.h
show_symbol_table_brief_json_ui() :
show_symbol_table.cpp
show_symbol_table_brief_plain() :
show_symbol_table.cpp
show_symbol_table_json_ui() :
show_symbol_table.cpp
show_symbol_table_plain() :
show_symbol_table.cpp
show_symbol_table_xml_ui() :
show_symbol_table.cpp
show_trace() :
report_traces.cpp
show_uninitialized() :
uninitialized.cpp
,
uninitialized.h
show_value_sets() :
show_value_sets.cpp
,
show_value_sets.h
show_vcc() :
show_vcc.cpp
,
show_vcc.h
show_vcc_json() :
show_vcc.cpp
show_vcc_plain() :
show_vcc.cpp
sign_of_expr() :
cover_instrument_mcdc.cpp
signal_catcher() :
signal_catcher.cpp
,
signal_catcher.h
signed_char_type() :
c_types.cpp
,
c_types.h
signed_int_type() :
c_types.cpp
,
c_types.h
signed_long_int_type() :
c_types.cpp
,
c_types.h
signed_long_long_int_type() :
c_types.cpp
,
c_types.h
signed_poly_type() :
util.cpp
,
util.h
signed_short_int_type() :
c_types.cpp
,
c_types.h
signed_size_type() :
c_types.cpp
,
c_types.h
simple_prooft :
resolution_proof.h
simple_slice() :
slice.cpp
,
slice.h
simplify() :
simplify_expr.cpp
,
simplify_expr.h
simplify_allocate() :
simplify_state_expr.cpp
simplify_cstrlen_expr() :
simplify_state_expr.cpp
simplify_evaluate_allocate_state() :
simplify_state_expr.cpp
simplify_evaluate_deallocate_state() :
simplify_state_expr.cpp
simplify_evaluate_enter_scope_state() :
simplify_state_expr.cpp
simplify_evaluate_exit_scope_state() :
simplify_state_expr.cpp
simplify_evaluate_update() :
simplify_state_expr.cpp
simplify_expr() :
simplify_expr.cpp
,
simplify_expr.h
simplify_gotos() :
utils.cpp
,
utils.h
simplify_is_cstring_expr() :
simplify_state_expr.cpp
simplify_is_dynamic_object_expr() :
simplify_state_expr.cpp
simplify_is_sentinel_dll_expr() :
simplify_state_expr.cpp
simplify_json_expr() :
json_expr.cpp
simplify_live_object_expr() :
simplify_state_expr.cpp
simplify_object_expression() :
simplify_state_expr.cpp
simplify_object_expression_rec() :
simplify_state_expr.cpp
simplify_object_size_expr() :
simplify_state_expr.cpp
simplify_ok_expr() :
simplify_state_expr.cpp
simplify_pointer_object_expr() :
simplify_state_expr.cpp
simplify_pointer_offset_expr() :
simplify_state_expr.cpp
simplify_state_expr() :
propagate.h
,
simplify_state_expr.cpp
,
simplify_state_expr.h
simplify_state_expr_node() :
propagate.h
,
simplify_state_expr.cpp
,
simplify_state_expr.h
simplify_string_char_at() :
simplify_expr.cpp
simplify_string_compare_to() :
simplify_expr.cpp
simplify_string_contains() :
simplify_expr.cpp
simplify_string_endswith() :
simplify_expr.cpp
simplify_string_equals_ignore_case() :
simplify_expr.cpp
simplify_string_index_of() :
simplify_expr.cpp
simplify_string_is_empty() :
simplify_expr.cpp
simplify_string_startswith() :
simplify_expr.cpp
simplify_sum() :
string_refinement.cpp
simplify_vsd_expr() :
abstract_environment.h
simplify_writeable_object_expr() :
simplify_state_expr.cpp
simplifying_not() :
state_encoding.cpp
,
horn_encoding.cpp
SINCE :
deprecate.h
size_of_expr() :
pointer_offset_size.cpp
,
pointer_offset_size.h
size_type() :
c_types.cpp
,
c_types.h
SKIP :
goto_program.h
skip_loops() :
skip_loops.cpp
,
skip_loops.h
skip_typecast() :
expr_util.cpp
,
expr_util.h
slash_to_dot() :
java_types.cpp
slice() :
bmc_util.cpp
,
bmc_util.h
,
slice.cpp
,
slice.h
slice_global_inits() :
slice_global_inits.cpp
,
slice_global_inits.h
slice_op_to_deref() :
dfcc_root_object.cpp
SM_ASSERT :
sharing_map.h
smt2_format() :
smt2_format.h
smt2_format_rec() :
smt2_format.cpp
,
smt2_format.h
smt2_parser_success() :
smt2irep.cpp
,
smt2irep.h
SMT2_TODO :
smt2_conv.cpp
smt2irep() :
smt2irep.cpp
,
smt2irep.h
,
smt2irep.cpp
,
smt2irep.h
smt_object_mapt :
object_tracking.h
smt_to_smt2_string() :
smt_to_smt2_string.cpp
,
smt_to_smt2_string.h
SN_ASSERT :
sharing_node.h
SN_ASSERT_USE :
sharing_node.h
SN_PTR_TYPE_ARGS :
sharing_node.h
SN_SHARE_KEYS :
sharing_node.h
SN_SMALL_MAP :
sharing_node.h
SN_TYPE_ARGS :
sharing_node.h
SN_TYPE_PAR_DECL :
sharing_node.h
SN_TYPE_PAR_DEF :
sharing_node.h
solver() :
solver.cpp
,
solver.h
,
smt2_solver.cpp
solver_resultt :
solver.h
solver_to_interrupt :
satcheck_minisat2.cpp
sort_and_join() :
simplify_utils.cpp
,
simplify_utils.h
SORT_ID :
smt_sorts.cpp
,
smt_sorts.h
sort_operands() :
simplify_utils.cpp
,
simplify_utils.h
splice_call() :
splice_call.cpp
,
splice_call.h
split_string() :
string_utils.cpp
,
string_utils.h
ssa_step_matches_failing_property() :
bmc_util.cpp
,
bmc_util.h
ssa_step_predicatet :
build_goto_trace.h
stack_and_not_dirty() :
may_alias.cpp
,
may_alias.h
stack_depth() :
stack_depth.cpp
,
stack_depth.h
stack_expr :
parser.h
stack_type :
parser.h
START_THREAD :
goto_program.h
state_encoding() :
state_encoding.cpp
,
state_encoding.h
,
horn_encoding.cpp
state_encoding_formatt :
state_encoding.h
state_encoding_solver() :
state_encoding.cpp
,
state_encoding.h
state_expr() :
state.h
,
horn_encoding.cpp
state_location() :
goto_trace.cpp
state_predicate_type() :
state.h
,
horn_encoding.cpp
state_sett :
trace_automaton.h
statement_list_entry_point() :
statement_list_entry_point.cpp
,
statement_list_entry_point.h
STATEMENT_LIST_PTR_WIDTH :
statement_list_typecheck.cpp
statement_list_typecheck() :
statement_list_typecheck.cpp
,
statement_list_typecheck.h
statet :
trace_automaton.h
static_lifetime_init() :
static_lifetime_init.cpp
,
static_lifetime_init.h
static_reachable_functions() :
unreachable_instructions.cpp
,
unreachable_instructions.h
static_show_domain() :
static_show_domain.cpp
,
static_show_domain.h
static_simplifier() :
static_simplifier.cpp
,
static_simplifier.h
static_unreachable_functions() :
unreachable_instructions.cpp
,
unreachable_instructions.h
static_unreachable_instructions() :
unreachable_instructions.cpp
,
unreachable_instructions.h
static_verifier() :
static_verifier.cpp
,
static_verifier.h
static_verifier_console() :
static_verifier.cpp
static_verifier_json() :
static_verifier.cpp
static_verifier_text() :
static_verifier.cpp
static_verifier_xml() :
static_verifier.cpp
stdio_redirection() :
run.cpp
STL_DINT_MAX_VALUE :
convert_dint_literal.cpp
STL_DINT_MIN_VALUE :
convert_dint_literal.cpp
STL_DINT_WIDTH :
statement_list_types.h
STL_INT_MAX_VALUE :
convert_int_literal.cpp
STL_INT_MIN_VALUE :
convert_int_literal.cpp
STL_INT_WIDTH :
statement_list_types.h
strictly_below() :
interval_union.cpp
string2integer() :
mp_arith.cpp
,
mp_arith.h
string2optional() :
string2int.h
string2optional_base() :
string2int.h
string2optional_int() :
string2int.cpp
,
string2int.h
string2optional_size_t() :
string2int.cpp
,
string2int.h
string2optional_unsigned() :
string2int.cpp
,
string2int.h
string_abstraction() :
string_abstraction.cpp
,
string_abstraction.h
string_from_ns() :
config.cpp
string_identifiers_resolution_from_equations() :
string_refinement.cpp
,
string_refinement.h
string_instrumentation() :
string_instrumentation.cpp
,
string_instrumentation.h
string_length_type() :
java_string_library_preprocess.cpp
string_of_array() :
string_refinement.cpp
string_refinement_invariantt :
string_refinement_invariant.h
STRING_REFINEMENT_MAX_CHAR_WIDTH :
magic.h
strip_first_field_from_suffix() :
value_set.cpp
strip_java_namespace_prefix() :
java_utils.cpp
,
java_utils.h
strip_member_element() :
may_be_same_object.cpp
strip_string() :
string_utils.cpp
,
string_utils.h
STRUCT_INSENSITIVE :
variable_sensitivity_configuration.h
struct_member_ptr_comparison_expr() :
constant_pointer_abstract_object.cpp
STRUCT_SENSITIVE :
variable_sensitivity_configuration.h
sub_expression_mapt :
convert_expr_to_smt.cpp
substitute() :
miniBDD.cpp
,
miniBDD.h
substitute_array_access() :
string_refinement.cpp
,
string_refinement.h
substitute_array_access_in_place() :
string_refinement.cpp
substitute_array_lists() :
string_refinement.cpp
,
string_refinement.h
substitute_identifiers() :
smt2_incremental_decision_procedure.cpp
substitute_rec() :
wp.cpp
substitute_symbols() :
substitute_symbols.cpp
,
substitute_symbols.h
substitute_symbols_rec() :
substitute_symbols.cpp
substitutiont :
polynomial.h
subsumed_pathst :
subsumed.h
subtype_expr() :
remove_instanceof.cpp
suffix_starts_with_field() :
value_set.cpp
sum_expr() :
simplify_expr_int.cpp
sum_overflows() :
string_constraint_generator.h
,
string_constraint_generator_main.cpp
swap_map() :
dfcc_library.cpp
switch_to_thread() :
symex_main.cpp
SYM_SWAP1 :
symbol.cpp
SYM_SWAP2 :
symbol.cpp
symbol_base_mapt :
symbol_table_base.h
symbol_exists() :
dfcc_utils.cpp
symbol_from_json() :
json_symbol.cpp
,
json_symbol.h
symbol_kindt :
find_symbols.cpp
symbol_module_mapt :
symbol_table_base.h
symbol_numbert :
type2name.cpp
symbol_ptr_comparison_expr() :
constant_pointer_abstract_object.cpp
symbol_sett :
slice.h
symbol_table_from_json() :
json_symbol_table.cpp
,
json_symbol_table.h
symbolptr_listt :
get_module.cpp
SYMEX_DYNAMIC_PREFIX :
pointer_predicates.h
symex_level0() :
renaming_level.cpp
,
renaming_level.h
symex_renaming_levelt :
renaming_level.h
symex_transition() :
goto_symex.h
,
symex_main.cpp
symmetric_operations :
abstract_environment.cpp
SYMTAB2GB_GOTO_FUNCTIONS_OPT :
symtab2gb_parse_options.h
SYMTAB2GB_OPTIONS :
symtab2gb_parse_options.h
SYMTAB2GB_OUT_FILE_OPT :
symtab2gb_parse_options.h
synthetic_class_symbol() :
lambda_synthesis.cpp
synthetic_method_typet :
synthetic_methods_map.h
synthetic_methods_mapt :
synthetic_methods_map.h
Generated by
1.17.0