Skip to content

Commit 6b24ec7

Browse files
romainbrenguierJoel Allred
romainbrenguier
authored and
Joel Allred
committed
Implement StringBuffer methods
Addresses issue diffblue/test-gen#245. This adds preprocessing for StringBuffer methods
1 parent 21eeb29 commit 6b24ec7

File tree

2 files changed

+153
-3
lines changed

2 files changed

+153
-3
lines changed

‎src/goto-programs/string_refine_preprocess.cpp

Lines changed: 148 additions & 3 deletions
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())
@@ -1351,6 +1387,115 @@ void string_refine_preprocesst::initialize_string_function_table()
13511387
// Not supported "java.lang.StringBuilder.trimToSize"
13521388
// TODO clean irep ids from insert_char_array etc...
13531389

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

‎src/goto-programs/string_refine_preprocess.h

Lines changed: 5 additions & 0 deletions
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)