CBMC
Toggle main menu visibility
Main Page
Related Pages
Namespaces
Namespace List
Namespace Members
All
a
c
d
e
f
g
j
l
m
r
t
w
Functions
a
c
d
f
g
r
t
w
Typedefs
Enumerations
Classes
Class List
Class Hierarchy
Class Members
All
_
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
~
Functions
_
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
~
Variables
_
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
Typedefs
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
Enumerations
a
b
c
d
e
f
g
i
k
l
m
o
p
r
s
t
u
v
w
Enumerator
a
b
c
d
e
f
h
i
k
l
m
n
o
p
q
r
s
t
u
v
Related Symbols
b
c
d
e
g
i
j
m
n
o
s
t
u
v
Files
File List
File Members
All
_
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
Functions
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
r
s
t
u
v
w
x
y
z
Variables
_
a
b
c
d
e
f
g
i
l
m
n
o
p
r
s
t
u
w
y
Typedefs
_
a
b
c
d
e
f
g
h
i
j
l
m
n
o
p
r
s
t
u
v
w
Enumerations
_
a
b
c
d
f
g
i
l
m
p
r
s
t
u
v
w
Enumerator
_
a
c
d
e
f
g
h
i
l
m
n
o
p
r
s
t
u
v
w
Macros
_
a
b
c
d
e
f
g
h
i
j
l
m
n
o
p
q
r
s
t
u
v
w
x
y
•
All
Classes
Namespaces
Files
Functions
Variables
Typedefs
Enumerations
Enumerator
Friends
Macros
Modules
Pages
Loading...
Searching...
No Matches
Here is a list of all macros with links to the files they belong to:
- c -
CALL_ON_CODE :
validate_code.cpp
CALL_ON_EXPR :
validate_expressions.cpp
CALL_ON_TYPE :
validate_types.cpp
CBMC_NORETURN :
invariant.h
CBMC_OPTIONS :
cbmc_parse_options.h
CHARACTER_FOR_UNKNOWN :
string_builtin_function.h
CHECK_RETURN :
invariant.h
CHECK_RETURN_STRUCTURED :
invariant.h
CHECK_RETURN_WITH_DIAGNOSTICS :
invariant.h
CHECK_RETURN_WITH_IREP :
invariant_utils.h
CLONE :
abstract_object.h
COMMAND_ID :
smt_commands.cpp
,
smt_commands.h
COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT :
common_harness_generator_options.h
COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT :
common_harness_generator_options.h
COMMON_HARNESS_GENERATOR_HELP :
common_harness_generator_options.h
COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT :
common_harness_generator_options.h
COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT :
common_harness_generator_options.h
COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT :
common_harness_generator_options.h
COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT :
common_harness_generator_options.h
COMMON_HARNESS_GENERATOR_OPTIONS :
common_harness_generator_options.h
COMPACT_CARRY :
bv_utils.cpp
COMPACT_ITE :
cnf.cpp
COMPACT_LT_OR_LE :
bv_utils.cpp
COMPACT_OBJECT_SIZE_EQ :
bv_pointers.cpp
CONSTANT_Class :
java_bytecode_parser.cpp
CONSTANT_Double :
java_bytecode_parser.cpp
CONSTANT_Fieldref :
java_bytecode_parser.cpp
CONSTANT_Float :
java_bytecode_parser.cpp
CONSTANT_Integer :
java_bytecode_parser.cpp
CONSTANT_InterfaceMethodref :
java_bytecode_parser.cpp
CONSTANT_InvokeDynamic :
java_bytecode_parser.cpp
CONSTANT_Long :
java_bytecode_parser.cpp
CONSTANT_MethodHandle :
java_bytecode_parser.cpp
CONSTANT_Methodref :
java_bytecode_parser.cpp
CONSTANT_MethodType :
java_bytecode_parser.cpp
CONSTANT_NameAndType :
java_bytecode_parser.cpp
CONSTANT_String :
java_bytecode_parser.cpp
CONSTANT_Utf8 :
java_bytecode_parser.cpp
CONTRACTS_PREFIX :
dfcc_library.cpp
CPROVER_ASSERT :
statement_list_typecheck.cpp
CPROVER_ASSUME :
statement_list_typecheck.cpp
CPROVER_EXIT_CONVERSION_FAILED :
exit_codes.h
CPROVER_EXIT_EXCEPTION :
exit_codes.h
CPROVER_EXIT_INCORRECT_TASK :
exit_codes.h
CPROVER_EXIT_INTERNAL_ERROR :
exit_codes.h
CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY :
exit_codes.h
CPROVER_EXIT_PARSE_ERROR :
exit_codes.h
CPROVER_EXIT_PREPROCESSOR_TEST_FAILED :
exit_codes.h
CPROVER_EXIT_SET_PROPERTIES_FAILED :
exit_codes.h
CPROVER_EXIT_SUCCESS :
exit_codes.h
CPROVER_EXIT_USAGE_ERROR :
exit_codes.h
CPROVER_EXIT_VERIFICATION_INCONCLUSIVE :
exit_codes.h
CPROVER_EXIT_VERIFICATION_SAFE :
exit_codes.h
CPROVER_EXIT_VERIFICATION_UNSAFE :
exit_codes.h
CPROVER_FAT_CIGAM :
osx_fat_reader.cpp
CPROVER_FAT_MAGIC :
osx_fat_reader.cpp
CPROVER_FKT_PREFIX :
cprover_prefix.h
CPROVER_HIDE :
statement_list_entry_point.cpp
CPROVER_MH_CIGAM :
osx_fat_reader.cpp
CPROVER_MH_CIGAM_64 :
osx_fat_reader.cpp
CPROVER_MH_MAGIC :
osx_fat_reader.cpp
CPROVER_MH_MAGIC_64 :
osx_fat_reader.cpp
CPROVER_OPTIONS :
cprover_parse_options.h
CPROVER_PREFIX :
cprover_prefix.h
CPROVER_TEMP_RLO :
statement_list_typecheck.cpp
CURRENT_FUNCTION_NAME :
invariant.h
Generated by
1.9.8
1.9.8