Skip to content

Commit 6c626c7

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #843 from allredj/test-gen-string-fix-245
Implement StringBuffer methods
2 parents 64c8bdf + 6b24ec7 commit 6c626c7

File tree

2 files changed

+153
-3
lines changed

2 files changed

+153
-3
lines changed

‎src/goto-programs/string_refine_preprocess.cpp

+148-3
Original file line numberDiff line numberDiff line change
@@ -123,6 +123,44 @@ bool string_refine_preprocesst::is_java_string_builder_pointer_type(
123123

124124
/*******************************************************************\
125125
126+
Function: string_refine_preprocesst::is_java_string_buffer_type
127+
128+
Inputs: a type
129+
130+
Outputs: Boolean telling whether the type is that of java string buffer
131+
132+
\*******************************************************************/
133+
134+
bool string_refine_preprocesst::is_java_string_buffer_type(const typet &type)
135+
{
136+
return check_java_type(type, "java.lang.StringBuffer");
137+
}
138+
139+
/*******************************************************************\
140+
141+
Function: string_refine_preprocesst::is_java_string_buffer_pointer_type
142+
143+
Inputs: a type
144+
145+
Outputs: Boolean telling whether the type is that of java StringBuffer
146+
pointers
147+
148+
\*******************************************************************/
149+
150+
bool string_refine_preprocesst::is_java_string_buffer_pointer_type(
151+
const typet &type)
152+
{
153+
if(type.id()==ID_pointer)
154+
{
155+
const pointer_typet &pt=to_pointer_type(type);
156+
const typet &subtype=pt.subtype();
157+
return is_java_string_buffer_type(subtype);
158+
}
159+
return false;
160+
}
161+
162+
/*******************************************************************\
163+
126164
Function: string_refine_preprocesst::is_java_char_sequence_type
127165
128166
Inputs: a type
@@ -315,9 +353,7 @@ Function: string_refine_preprocesst::get_data_and_length_type_of_string
315353
void string_refine_preprocesst::get_data_and_length_type_of_string(
316354
const exprt &expr, typet &data_type, typet &length_type)
317355
{
318-
assert(is_java_string_type(expr.type()) ||
319-
is_java_string_builder_type(expr.type()) ||
320-
is_java_char_sequence_type(expr.type()));
356+
assert(implements_java_char_sequence(pointer_typet(expr.type())));
321357
typet object_type=ns.follow(expr.type());
322358
const struct_typet &struct_type=to_struct_type(object_type);
323359
for(const auto &component : struct_type.components())
@@ -1345,6 +1381,115 @@ void string_refine_preprocesst::initialize_string_function_table()
13451381
// Not supported "java.lang.StringBuilder.trimToSize"
13461382
// TODO clean irep ids from insert_char_array etc...
13471383

1384+
// StringBuffer library
1385+
string_function_calls
1386+
["java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"]=
1387+
ID_cprover_string_copy_func;
1388+
string_function_calls["java::java.lang.StringBuffer.<init>:()V"]=
1389+
ID_cprover_string_empty_string_func;
1390+
1391+
side_effect_functions
1392+
["java::java.lang.StringBuffer.append:(Z)Ljava/lang/StringBuffer;"]=
1393+
ID_cprover_string_concat_bool_func;
1394+
side_effect_functions
1395+
["java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
1396+
ID_cprover_string_concat_char_func;
1397+
side_effect_functions
1398+
["java::java.lang.StringBuffer.append:([C)"
1399+
"Ljava/lang/StringBuffer;"]=
1400+
ID_cprover_string_concat_func;
1401+
// Not supported: "java.lang.StringBuffer.append:([CII)"
1402+
// Not supported: "java.lang.StringBuffer.append:(LCharSequence;)"
1403+
side_effect_functions
1404+
["java::java.lang.StringBuffer.append:(D)Ljava/lang/StringBuffer;"]=
1405+
ID_cprover_string_concat_double_func;
1406+
side_effect_functions
1407+
["java::java.lang.StringBuffer.append:(F)Ljava/lang/StringBuffer;"]=
1408+
ID_cprover_string_concat_float_func;
1409+
side_effect_functions
1410+
["java::java.lang.StringBuffer.append:(I)Ljava/lang/StringBuffer;"]=
1411+
ID_cprover_string_concat_int_func;
1412+
side_effect_functions
1413+
["java::java.lang.StringBuffer.append:(J)Ljava/lang/StringBuffer;"]=
1414+
ID_cprover_string_concat_long_func;
1415+
// Not supported: "java.lang.StringBuffer.append:(LObject;)"
1416+
side_effect_functions
1417+
["java::java.lang.StringBuffer.append:(Ljava/lang/String;)"
1418+
"Ljava/lang/StringBuffer;"]=
1419+
ID_cprover_string_concat_func;
1420+
side_effect_functions
1421+
["java::java.lang.StringBuffer.appendCodePoint:(I)"
1422+
"Ljava/lang/StringBuffer;"]=
1423+
ID_cprover_string_concat_code_point_func;
1424+
// Not supported: "java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)"
1425+
// Not supported: "java.lang.StringBuffer.capacity:()"
1426+
string_functions["java::java.lang.StringBuffer.charAt:(I)C"]=
1427+
ID_cprover_string_char_at_func;
1428+
string_functions["java::java.lang.StringBuffer.codePointAt:(I)I"]=
1429+
ID_cprover_string_code_point_at_func;
1430+
string_functions["java::java.lang.StringBuffer.codePointBefore:(I)I"]=
1431+
ID_cprover_string_code_point_before_func;
1432+
string_functions["java::java.lang.StringBuffer.codePointCount:(II)I"]=
1433+
ID_cprover_string_code_point_count_func;
1434+
side_effect_functions
1435+
["java::java.lang.StringBuffer.delete:(II)Ljava/lang/StringBuffer;"]=
1436+
ID_cprover_string_delete_func;
1437+
side_effect_functions
1438+
["java::java.lang.StringBuffer.deleteCharAt:(I)Ljava/lang/StringBuffer;"]=
1439+
ID_cprover_string_delete_char_at_func;
1440+
// Not supported: "java.lang.StringBuffer.ensureCapacity:()"
1441+
// Not supported: "java.lang.StringBuffer.getChars:()"
1442+
// Not supported: "java.lang.StringBuffer.indexOf:()"
1443+
side_effect_functions
1444+
["java::java.lang.StringBuffer.insert:(IZ)Ljava/lang/StringBuffer;"]=
1445+
ID_cprover_string_insert_bool_func;
1446+
side_effect_functions
1447+
["java::java.lang.StringBuffer.insert:(IC)Ljava/lang/StringBuffer;"]=
1448+
ID_cprover_string_insert_char_func;
1449+
side_effect_functions
1450+
["java::java.lang.StringBuffer.insert:(I[C)Ljava/lang/StringBuffer;"]=
1451+
ID_cprover_string_insert_func;
1452+
side_effect_functions
1453+
["java::java.lang.StringBuffer.insert:(I[CII)Ljava/lang/StringBuffer;"]=
1454+
ID_cprover_string_insert_func;
1455+
// Not supported "java.lang.StringBuffer.insert:(ILCharSequence;)"
1456+
// Not supported "java.lang.StringBuffer.insert:(ILCharSequence;II)"
1457+
// Not supported "java.lang.StringBuffer.insert:(ID)"
1458+
// Not supported "java.lang.StringBuffer.insert:(IF)"
1459+
side_effect_functions
1460+
["java::java.lang.StringBuffer.insert:(II)Ljava/lang/StringBuffer;"]=
1461+
ID_cprover_string_insert_int_func;
1462+
side_effect_functions
1463+
["java::java.lang.StringBuffer.insert:(IJ)Ljava/lang/StringBuffer;"]=
1464+
ID_cprover_string_insert_long_func;
1465+
// Not supported "java.lang.StringBuffer.insert:(ILObject;)"
1466+
side_effect_functions
1467+
["java::java.lang.StringBuffer.insert:(ILjava/lang/String;)"
1468+
"Ljava/lang/StringBuffer;"]=
1469+
ID_cprover_string_insert_func;
1470+
// Not supported "java.lang.StringBuffer.lastIndexOf"
1471+
string_functions["java::java.lang.StringBuffer.length:()I"]=
1472+
ID_cprover_string_length_func;
1473+
// Not supported "java.lang.StringBuffer.offsetByCodePoints"
1474+
// Not supported "java.lang.StringBuffer.replace"
1475+
// Not supported "java.lang.StringBuffer.reverse"
1476+
side_effect_functions["java::java.lang.StringBuffer.setCharAt:(IC)V"]=
1477+
ID_cprover_string_char_set_func;
1478+
side_effect_functions
1479+
["java::java.lang.StringBuffer.setLength:(I)V"]=
1480+
ID_cprover_string_set_length_func;
1481+
// Not supported "java.lang.StringBuffer.subSequence"
1482+
string_functions
1483+
["java::java.lang.StringBuffer.substring:(II)Ljava/lang/String;"]=
1484+
ID_cprover_string_substring_func;
1485+
string_functions
1486+
["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
1487+
ID_cprover_string_substring_func;
1488+
string_functions
1489+
["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"]=
1490+
ID_cprover_string_copy_func;
1491+
// Not supported "java.lang.StringBuffer.trimToSize"
1492+
13481493
// Other libraries
13491494
string_functions["java::java.lang.CharSequence.charAt:(I)C"]=
13501495
ID_cprover_string_char_at_func;

‎src/goto-programs/string_refine_preprocess.h

+5
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,10 @@ class string_refine_preprocesst:public messaget
5353

5454
static bool is_java_string_builder_pointer_type(const typet &type);
5555

56+
static bool is_java_string_buffer_type(const typet &type);
57+
58+
static bool is_java_string_buffer_pointer_type(const typet &type);
59+
5660
static bool is_java_char_sequence_type(const typet &type);
5761

5862
static bool is_java_char_sequence_pointer_type(const typet &type);
@@ -66,6 +70,7 @@ class string_refine_preprocesst:public messaget
6670
return
6771
is_java_char_sequence_pointer_type(type) ||
6872
is_java_string_builder_pointer_type(type) ||
73+
is_java_string_buffer_pointer_type(type) ||
6974
is_java_string_pointer_type(type);
7075
}
7176

0 commit comments

Comments
 (0)