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. | |
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.
Enumerator | |
---|---|
STATIC_INITIALIZER_WRAPPER | A static initializer wrapper (code of the form |
USER_SPECIFIED_STATIC_INITIALIZER | Only exists if the If a given type has an entry in the file given by this option, the "user specified static initializer" contains a sequence of assignments from static field expressions to values read from the file. Otherwise, this function simply calls the regular clinit. |
STUB_CLASS_STATIC_INITIALIZER | A generated (synthetic) static initializer function for a stub type. Because we don't have the bytecode for a stub type (by definition), we generate a static initializer function to initialize its static fields. |
INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR | A generated constructor for a class capturing the parameters of an invokedynamic instruction. |
INVOKEDYNAMIC_METHOD | A generated method for a class capturing the parameters of an invokedynamic instruction. |
CREATE_ARRAY_WITH_TYPE | Our internal implementation of CProver.createArrayWithType, which needs to access internal type-id fields. |
Definition at line 27 of file synthetic_methods_map.h.