CBMC
|
Synthetic methods are particular methods internally generated by the Java frontend, including thunks to ensure static initializers are run once and initializers created for unknown / stub types. More...
Go to the source code of this file.
Typedefs | |
typedef std::unordered_map< irep_idt, synthetic_method_typet > | synthetic_methods_mapt |
Maps method names on to a synthetic method kind. More... | |
Enumerations | |
enum class | synthetic_method_typet { STATIC_INITIALIZER_WRAPPER , USER_SPECIFIED_STATIC_INITIALIZER , STUB_CLASS_STATIC_INITIALIZER , INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR , INVOKEDYNAMIC_METHOD , CREATE_ARRAY_WITH_TYPE } |
Synthetic method kinds. More... | |
Synthetic methods are particular methods internally generated by the Java frontend, including thunks to ensure static initializers are run once and initializers created for unknown / stub types.
Compare normal methods, which are translated from Java bytecode. This file provides an enumeration specifying the kind of a particular synthetic method and a common type of a map giving a collection of synthetic methods. Functions stubs and array.clone() functions are also generated by the Java frontend but are not recorded using this framework, but may be in future.
Definition in file synthetic_methods_map.h.
typedef std::unordered_map<irep_idt, synthetic_method_typet> synthetic_methods_mapt |
Maps method names on to a synthetic method kind.
Definition at line 57 of file synthetic_methods_map.h.
|
strong |
Synthetic method kinds.
Definition at line 27 of file synthetic_methods_map.h.