cprover
java_types.cpp File Reference
#include "java_types.h"
#include <cassert>
#include <cctype>
#include <util/std_types.h>
#include <util/c_types.h>
#include <util/std_expr.h>
#include <util/ieee_float.h>
Include dependency graph for java_types.cpp:

Go to the source code of this file.

Functions

typet java_int_type ()
 
typet java_void_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 ()
 
reference_typet java_array_type (const char subtype)
 
bool is_reference_type (const char t)
 
typet java_type_from_char (char t)
 
typet java_bytecode_promotion (const typet &type)
 Java does not support byte/short return types. These are always promoted. More...
 
exprt java_bytecode_promotion (const exprt &expr)
 Java does not support byte/short return types. These are always promoted. More...
 
typet java_type_from_string (const std::string &src)
 
char java_char_from_type (const typet &type)
 
static std::string slash_to_dot (const std::string &src)
 
symbol_typet java_classname (const std::string &id)
 

Function Documentation

§ is_reference_type()

bool is_reference_type ( const 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 type)

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 expr)

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 &  id)

§ 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()

§ java_void_type()

typet java_void_type ( )

Definition at line 24 of file java_types.cpp.

Referenced by java_type_from_string().

§ slash_to_dot()

static std::string slash_to_dot ( const std::string &  src)
static

Definition at line 285 of file java_types.cpp.

Referenced by java_classname().