CBMC
synthetic_methods_map.h File Reference

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...

#include <unordered_map>
#include <util/irep.h>
+ Include dependency graph for synthetic_methods_map.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Typedefs

typedef std::unordered_map< irep_idt, synthetic_method_typetsynthetic_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...
 

Detailed Description

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 Documentation

◆ synthetic_methods_mapt

Maps method names on to a synthetic method kind.

Definition at line 57 of file synthetic_methods_map.h.

Enumeration Type Documentation

◆ synthetic_method_typet

Synthetic method kinds.

Enumerator
STATIC_INITIALIZER_WRAPPER 

A static initializer wrapper (code of the form if(!already_run) clinit(); already_run = true;) These are generated for both user and stub types, to ensure the actual static initializer is only run once on any given path.

USER_SPECIFIED_STATIC_INITIALIZER 

Only exists if the --static-values option was used.

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.