79 std::string subtype_str;
83 case 'b': subtype_str=
"byte";
break;
84 case 'f': subtype_str=
"float";
break;
85 case 'd': subtype_str=
"double";
break;
86 case 'i': subtype_str=
"int";
break;
87 case 'c': subtype_str=
"char";
break;
88 case 's': subtype_str=
"short";
break;
89 case 'z': subtype_str=
"boolean";
break;
90 case 'v': subtype_str=
"void";
break;
91 case 'j': subtype_str=
"long";
break;
92 case 'l': subtype_str=
"long";
break;
93 case 'a': subtype_str=
"reference";
break;
94 default: assert(
false);
97 irep_idt class_name=
"array["+subtype_str+
"]";
100 symbol_type.
set(ID_C_base_name, class_name);
125 default: assert(
false);
return nil_typet();
146 if(new_type==expr.
type())
161 std::size_t e_pos=src.rfind(
')');
162 if(e_pos==std::string::npos)
170 for(std::size_t i=1; i<src.size() && src[i]!=
')'; i++)
189 std::string sub_str=src.substr(start, i-start+1);
192 if(param.
type().
id()==ID_symbol)
207 char subtype_letter=src[1];
210 if(subtype_letter==
'L' ||
214 tmp.
subtype().
set(ID_C_element_type, subtype);
231 if(src[src.size()-1]!=
';')
233 std::string class_name=src.substr(1, src.size()-2);
235 for(
unsigned i=0; i<class_name.size(); i++)
236 if(class_name[i]==
'/')
239 std::string identifier=
"java::"+class_name;
243 result.
subtype().
set(ID_C_base_name, class_name);
268 else if(
id==ID_unsignedbv)
270 else if(
id==ID_floatbv)
278 else if(
id==ID_c_bool)
287 std::string result=src;
288 for(std::string::iterator it=result.begin(); it!=result.end(); it++)
296 if(!
id.empty() &&
id[0]==
'[')
299 std::string class_name=id;
302 irep_idt identifier=
"java::"+class_name;
304 symbol_type.
set(ID_C_base_name, class_name);
The type of an expression.
Fixed-width bit-vector with unsigned binary interpretation.
const std::string & id2string(const irep_idt &d)
typet java_boolean_type()
reference_typet java_reference_type(const typet &subtype)
reference_typet java_array_type(const char subtype)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
reference_typet java_lang_object_type()
static ieee_float_spect double_precision()
class floatbv_typet to_type() const
const irep_idt & id() const
typet java_type_from_string(const std::string &src)
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
A reference into the symbol table.
reference_typet reference_type(const typet &subtype)
Fixed-width bit-vector with two's complement interpretation.
typet java_type_from_char(char t)
API to expression classes.
static ieee_float_spect single_precision()
bool is_reference_type(const char t)
std::size_t get_width() const
const reference_typet & to_reference_type(const typet &type)
Cast a generic typet to a reference_typet.
static std::string slash_to_dot(const std::string &src)
Base class for all expressions.
const parameterst & parameters() const
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
typet java_bytecode_promotion(const typet &type)
Java does not support byte/short return types. These are always promoted.
const typet & subtype() const
symbol_typet java_classname(const std::string &id)
const irept & find(const irep_namet &name) const
const typet & return_type() const
char java_char_from_type(const typet &type)
void set(const irep_namet &name, const irep_idt &value)