CBMC
java_primitive_type_infot Struct Reference

Return type for get_java_primitive_type_info. More...

#include <java_utils.h>

+ Collaboration diagram for java_primitive_type_infot:

Public Attributes

const irep_idt boxed_type_name
 Name, including java:: prefix, of the corresponding boxed type. More...
 
const irep_idt boxed_type_factory_method
 Full identifier of the boxed type's factory method that takes the corresponding primitive as its sole argument. More...
 
const irep_idt unboxing_function_name
 Full identifier of the most general boxed-type method that yields this type. More...
 

Detailed Description

Return type for get_java_primitive_type_info.

Definition at line 32 of file java_utils.h.

Member Data Documentation

◆ boxed_type_factory_method

const irep_idt java_primitive_type_infot::boxed_type_factory_method

Full identifier of the boxed type's factory method that takes the corresponding primitive as its sole argument.

Definition at line 38 of file java_utils.h.

◆ boxed_type_name

const irep_idt java_primitive_type_infot::boxed_type_name

Name, including java:: prefix, of the corresponding boxed type.

Definition at line 35 of file java_utils.h.

◆ unboxing_function_name

const irep_idt java_primitive_type_infot::unboxing_function_name

Full identifier of the most general boxed-type method that yields this type.

For most primitives that means the corresponding method on java.lang.Number; for Character and Boolean it means the method on their specific boxed type.

Definition at line 43 of file java_utils.h.


The documentation for this struct was generated from the following file: