cprover
java_types.h File Reference
#include <util/type.h>
#include <util/std_types.h>
Include dependency graph for java_types.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

typet java_int_type ()
 
typet java_long_type ()
 
typet java_short_type ()
 
typet java_byte_type ()
 
typet java_char_type ()
 
typet java_float_type ()
 
typet java_double_type ()
 
typet java_boolean_type ()
 
reference_typet java_reference_type (const typet &subtype)
 
reference_typet java_lang_object_type ()
 
symbol_typet java_classname (const std::string &)
 
reference_typet java_array_type (const char subtype)
 
bool is_reference_type (char t)
 
typet java_type_from_char (char t)
 
typet java_type_from_string (const std::string &)
 
char java_char_from_type (const typet &type)
 
typet java_bytecode_promotion (const typet &)
 Java does not support byte/short return types. These are always promoted. More...
 
exprt java_bytecode_promotion (const exprt &)
 Java does not support byte/short return types. These are always promoted. More...
 

Function Documentation

◆ is_reference_type()

bool is_reference_type ( char  t)

Definition at line 106 of file java_types.cpp.

◆ java_array_type()

◆ java_boolean_type()

◆ java_byte_type()

◆ java_bytecode_promotion() [1/2]

typet java_bytecode_promotion ( const typet )

Java does not support byte/short return types. These are always promoted.

Definition at line 130 of file java_types.cpp.

References java_boolean_type(), java_byte_type(), java_char_type(), java_int_type(), and java_short_type().

Referenced by java_bytecode_convert_methodt::convert_instructions(), and java_bytecode_promotion().

◆ java_bytecode_promotion() [2/2]

exprt java_bytecode_promotion ( const exprt )

Java does not support byte/short return types. These are always promoted.

Definition at line 142 of file java_types.cpp.

References java_bytecode_promotion(), and exprt::type().

◆ java_char_from_type()

◆ java_char_type()

◆ java_classname()

symbol_typet java_classname ( const std::string &  )

◆ java_double_type()

◆ java_float_type()

◆ java_int_type()

◆ java_lang_object_type()

reference_typet java_lang_object_type ( )

Definition at line 72 of file java_types.cpp.

References java_reference_type().

◆ java_long_type()

◆ java_reference_type()

◆ java_short_type()

◆ java_type_from_char()

◆ java_type_from_string()