CBMC
- _ -
__attribute__ :
gcc.c
,
gcc_builtin_headers_types.h
__builtin_ms_va_list :
gcc_builtin_headers_types.h
__builtin_va_list :
gcc_builtin_headers_types.h
__CPROVER_contracts_car_set_ptr_t :
cprover_contracts.c
__CPROVER_contracts_obj_set_ptr_t :
cprover_contracts.c
__CPROVER_contracts_write_set_ptr_t :
cprover_contracts.c
__CPROVER_jsa__internal_index_t :
jsa.h
__CPROVER_jsa_abstract_heapt :
jsa.h
__CPROVER_jsa_abstract_nodet :
jsa.h
__CPROVER_jsa_abstract_ranget :
jsa.h
__CPROVER_jsa_concrete_nodet :
jsa.h
__CPROVER_jsa_data_t :
jsa.h
__CPROVER_jsa_id_t :
jsa.h
__CPROVER_jsa_index_t :
jsa.h
__CPROVER_jsa_iterator_id_t :
jsa.h
__CPROVER_jsa_iteratort :
jsa.h
__CPROVER_jsa_list_id_t :
jsa.h
__CPROVER_jsa_node_id_t :
jsa.h
__CPROVER_jsa_signed_word_t :
jsa.h
__CPROVER_jsa_word_t :
jsa.h
__CPROVER_mutex_t :
pthread_lib.c
__CPROVER_ssize_t :
cprover.h
__gcc_di :
gcc_builtin_headers_types.h
- a -
abstract_object_pointert :
abstract_object.h
abstract_object_visitedt :
abstract_object.h
abstract_value_pointert :
abstract_value_object.h
address_mapt :
java_local_variable_table.cpp
allocate_local_symbolt :
nondet.h
alternate_casest :
nondet.h
api_call_back_contextt :
api.h
api_message_callbackt :
api.h
array_element_generatort :
java_object_factory.h
assignst :
havoc_utils.h
,
loop_utils.h
assume_function :
abstract_environment.cpp
- b -
build_argumentst :
java_entry_point.h
bvt :
literal.h
Byte :
miniz.h
Bytef :
miniz.h
- c -
c_translation_unitt :
mini_c_parser.h
cfg_dominatorst :
cfg_dominators.h
cfg_post_dominatorst :
cfg_dominators.h
charf :
miniz.h
- d -
d_baset :
sharing_node.h
dead_mapt :
unreachable_instructions.cpp
dfcc_loop_nesting_grapht :
dfcc_loop_nesting_graph.h
dispatch_table_entries_mapt :
remove_virtual_functions.h
dispatch_table_entriest :
remove_virtual_functions.h
- e -
Elf32_Addr :
elf_reader.h
Elf32_Half :
elf_reader.h
Elf32_Off :
elf_reader.h
Elf32_Word :
elf_reader.h
Elf64_Addr :
elf_reader.h
Elf64_Half :
elf_reader.h
Elf64_Off :
elf_reader.h
Elf64_Word :
elf_reader.h
Elf64_Xword :
elf_reader.h
enumeratorst :
expr_enumerator.h
event_idt :
event_graph.h
expr_listt :
acceleration_utils.h
,
expr_enumerator.h
expr_mapt :
acceleration_utils.h
expr_sett :
cone_of_influence.h
,
expr_enumerator.h
- f -
fdt :
run.cpp
filest :
count_eloc.cpp
find_macros_sett :
find_macros.h
find_symbols_sett :
find_symbols.h
format_token_listt :
format_strings.h
frame_mapt :
solver_types.h
function_is_stubt :
remove_returns.h
functionst :
contracts_wrangler.h
- g -
goto_instruction_codet :
goto_instruction_code.h
guard_managert :
guard.h
guardt :
guard.h
- h -
holet :
java_local_variable_table.cpp
- i -
ieee_float_intervalt :
interval_domain.h
index_range_implementation_ptrt :
abstract_value_object.h
innermost_loop_mapt :
sese_regions.cpp
integer_intervalt :
integer_interval.h
intf :
miniz.h
invariant_mapt :
utils.h
irep_id_hash :
irep.h
irep_idt :
verification_result.h
,
irep.h
- j -
java_cfg_dominatorst :
java_local_variable_table.cpp
- l -
language_factoryt :
mode.h
languagest :
mode.cpp
lexical_loopst :
lexical_loops.h
linest :
count_eloc.cpp
llong_t :
mp_arith.cpp
load_extra_methodst :
ci_lazy_methods.h
loc_sett :
fatal_assertions.cpp
local_variable_table_with_holest :
java_local_variable_table.cpp
local_variable_with_holest :
java_local_variable_table.cpp
loop_idst :
skip_loops.cpp
loop_mapt :
skip_loops.cpp
loopt :
loop_utils.h
- m -
method_convertert :
ci_lazy_methods.h
methods_by_name_and_descriptort :
lambda_synthesis.cpp
minimization_listt :
bv_minimize.h
mp_integer :
smt_terms.h
,
mp_arith.h
mz_alloc_func :
miniz.h
mz_bool :
miniz.h
mz_file_read_func :
miniz.h
mz_file_write_func :
miniz.h
mz_free_func :
miniz.h
mz_int16 :
miniz.h
mz_int64 :
miniz.h
mz_realloc_func :
miniz.h
mz_stream :
miniz.h
mz_streamp :
miniz.h
mz_uint :
miniz.h
mz_uint16 :
miniz.h
mz_uint32 :
miniz.h
mz_uint64 :
miniz.h
mz_uint8 :
miniz.h
mz_ulong :
miniz.h
mz_validate_uint16 :
miniz.cpp
mz_validate_uint32 :
miniz.cpp
mz_validate_uint64 :
miniz.cpp
mz_zip_internal_state :
miniz.h
- n -
name_mapt :
graphml.cpp
natural_loops_mutablet :
natural_loops.h
node_indext :
scope_tree.h
- o -
object_id_sett :
object_id.h
object_numberingt :
object_numbering.h
opcodet :
cegis.c
opt :
cegis.c
- p -
partitiont :
expr_enumerator.h
pathst :
path.h
patht :
path.h
polynomialst :
polynomial.h
predecessor_mapt :
java_local_variable_table.cpp
program_relative_instruction_indicest :
sese_regions.cpp
propertiest :
properties.h
,
verification_result.h
propertyt :
report_util.cpp
- r -
replace_mapt :
replace_expr.h
- s -
s1 :
bytecode_info.h
s2 :
bytecode_info.h
s4 :
bytecode_info.h
s8 :
bytecode_info.h
set_predicate_fn :
value_set_abstract_object.cpp
sharing_ptrt :
abstract_object.h
simple_prooft :
resolution_proof.h
smt_object_mapt :
object_tracking.h
ssa_step_predicatet :
build_goto_trace.h
state_sett :
trace_automaton.h
statet :
trace_automaton.h
sub_expression_mapt :
convert_expr_to_smt.cpp
substitutiont :
polynomial.h
subsumed_pathst :
subsumed.h
symbol_base_mapt :
symbol_table_base.h
symbol_module_mapt :
symbol_table_base.h
symbol_numbert :
type2name.cpp
symbol_sett :
slice.h
symbolptr_listt :
get_module.cpp
symex_renaming_levelt :
renaming_level.h
synthetic_methods_mapt :
synthetic_methods_map.h
- t -
tdefl_put_buf_func_ptr :
miniz.h
tinfl_bit_buf_t :
miniz.h
tinfl_decompressor :
miniz.h
tinfl_put_buf_func_ptr :
miniz.h
type_size_mapt :
type_size_mapping.h
- u -
u1 :
bytecode_info.h
u2 :
bytecode_info.h
u4 :
bytecode_info.h
u8 :
bytecode_info.h
uInt :
miniz.h
uIntf :
miniz.h
ullong_t :
mp_arith.cpp
uLong :
miniz.h
uLongf :
miniz.h
uninitialized_analysist :
uninitialized_domain.h
- v -
value_range_implementation_ptrt :
abstract_value_object.h
value_set_analysist :
value_set_analysis.h
value_set_domain_factoryt :
value_set_domain.h
value_set_domaint :
value_set_domain.h
variable_sensitivity_object_factory_ptrt :
abstract_environment.h
,
variable_sensitivity_object_factory.h
variablest :
java_bytecode_convert_method.h
voidp :
miniz.h
voidpc :
miniz.h
voidpf :
miniz.h
- w -
wmm_grapht :
event_graph.h
working_dirst :
count_eloc.cpp
Generated by
1.9.1
1.9.1