Skip to content

Commit 5851f63

Browse files
romainbrenguierJoel Allred
romainbrenguier
authored and
Joel Allred
committed
Order string functions in alphabetical order
1 parent cb065bf commit 5851f63

File tree

1 file changed

+163
-124
lines changed

1 file changed

+163
-124
lines changed

‎src/goto-programs/string_refine_preprocess.cpp

+163-124
Original file line numberDiff line numberDiff line change
@@ -1116,14 +1116,54 @@ Function: string_refine_preprocesst::initialize_string_function_table
11161116

11171117
void string_refine_preprocesst::initialize_string_function_table()
11181118
{
1119+
// String library
1120+
string_function_calls
1121+
["java::java.lang.String.<init>:(Ljava/lang/String;)V"]=
1122+
ID_cprover_string_copy_func;
1123+
string_function_calls
1124+
["java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"]=
1125+
ID_cprover_string_copy_func;
1126+
string_function_calls["java::java.lang.String.<init>:([C)V"]=
1127+
ID_cprover_string_copy_func;
1128+
string_function_calls["java::java.lang.String.<init>:([CII)V"]=
1129+
ID_cprover_string_copy_func;
1130+
string_function_calls["java::java.lang.String.<init>:()V"]=
1131+
ID_cprover_string_empty_string_func;
1132+
// Not supported java.lang.String.<init>:(Ljava/lang/StringBuffer;)
1133+
1134+
string_functions["java::java.lang.String.charAt:(I)C"]=
1135+
ID_cprover_string_char_at_func;
11191136
string_functions["java::java.lang.String.codePointAt:(I)I"]=
11201137
ID_cprover_string_code_point_at_func;
11211138
string_functions["java::java.lang.String.codePointBefore:(I)I"]=
11221139
ID_cprover_string_code_point_before_func;
11231140
string_functions["java::java.lang.String.codePointCount:(II)I"]=
11241141
ID_cprover_string_code_point_count_func;
1125-
string_functions["java::java.lang.String.offsetByCodePoints:(II)I"]=
1126-
ID_cprover_string_offset_by_code_point_func;
1142+
string_functions["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
1143+
ID_cprover_string_compare_to_func;
1144+
// Not supported "java.lang.String.contentEquals"
1145+
string_functions
1146+
["java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
1147+
ID_cprover_string_concat_func;
1148+
string_functions
1149+
["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
1150+
ID_cprover_string_contains_func;
1151+
string_functions
1152+
["java::java.lang.String.copyValueOf:([CII)Ljava/lang/String;"]=
1153+
ID_cprover_string_copy_func;
1154+
string_functions
1155+
["java::java.lang.String.copyValueOf:([C)Ljava/lang/String;"]=
1156+
ID_cprover_string_copy_func;
1157+
string_functions["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
1158+
ID_cprover_string_endswith_func;
1159+
string_functions["java::java.lang.String.equals:(Ljava/lang/Object;)Z"]=
1160+
ID_cprover_string_equal_func;
1161+
string_functions
1162+
["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
1163+
ID_cprover_string_equals_ignore_case_func;
1164+
// Not supported "java.lang.String.format"
1165+
// Not supported "java.lang.String.getBytes"
1166+
// Not supported "java.lang.String.getChars"
11271167
string_functions["java::java.lang.String.hashCode:()I"]=
11281168
ID_cprover_string_hash_code_func;
11291169
string_functions["java::java.lang.String.indexOf:(I)I"]=
@@ -1134,6 +1174,10 @@ void string_refine_preprocesst::initialize_string_function_table()
11341174
ID_cprover_string_index_of_func;
11351175
string_functions["java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]=
11361176
ID_cprover_string_index_of_func;
1177+
string_functions["java::java.lang.String.intern:()Ljava/lang/String;"]=
1178+
ID_cprover_string_intern_func;
1179+
string_functions["java::java.lang.String.isEmpty:()Z"]=
1180+
ID_cprover_string_is_empty_func;
11371181
string_functions["java::java.lang.String.lastIndexOf:(I)I"]=
11381182
ID_cprover_string_last_index_of_func;
11391183
string_functions["java::java.lang.String.lastIndexOf:(II)I"]=
@@ -1144,188 +1188,182 @@ void string_refine_preprocesst::initialize_string_function_table()
11441188
string_functions
11451189
["java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
11461190
ID_cprover_string_last_index_of_func;
1147-
string_functions
1148-
["java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
1149-
ID_cprover_string_concat_func;
11501191
string_functions["java::java.lang.String.length:()I"]=
11511192
ID_cprover_string_length_func;
1152-
string_functions["java::java.lang.StringBuilder.length:()I"]=
1153-
ID_cprover_string_length_func;
1154-
string_functions["java::java.lang.String.equals:(Ljava/lang/Object;)Z"]=
1155-
ID_cprover_string_equal_func;
1156-
string_functions
1157-
["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
1158-
ID_cprover_string_equals_ignore_case_func;
1193+
// Not supported "java.lang.String.matches"
1194+
string_functions["java::java.lang.String.offsetByCodePoints:(II)I"]=
1195+
ID_cprover_string_offset_by_code_point_func;
1196+
// Not supported "java.lang.String.regionMatches"
1197+
string_functions["java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
1198+
ID_cprover_string_replace_func;
1199+
// Not supported "java.lang.String.replace:(LCharSequence;LCharSequence)"
1200+
// Not supported "java.lang.String.replaceAll"
1201+
// Not supported "java.lang.String.replaceFirst"
1202+
// Not supported "java.lang.String.split"
11591203
string_functions["java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
11601204
ID_cprover_string_startswith_func;
11611205
string_functions
11621206
["java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
11631207
ID_cprover_string_startswith_func;
1164-
string_functions["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
1165-
ID_cprover_string_endswith_func;
1166-
string_functions["java::java.lang.String.substring:(II)Ljava/lang/String;"]=
1167-
ID_cprover_string_substring_func;
1208+
string_functions
1209+
["java::java.lang.String.subSequence:(II)Ljava/lang/CharSequence;"]=
1210+
ID_cprover_string_substring_func;
11681211
string_functions["java::java.lang.String.substring:(II)Ljava/lang/String;"]=
11691212
ID_cprover_string_substring_func;
11701213
string_functions["java::java.lang.String.substring:(I)Ljava/lang/String;"]=
11711214
ID_cprover_string_substring_func;
1172-
string_functions
1173-
["java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
1174-
ID_cprover_string_substring_func;
1175-
string_functions
1176-
["java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
1177-
ID_cprover_string_substring_func;
1178-
string_functions
1179-
["java::java.lang.String.subSequence:(II)Ljava/lang/CharSequence;"]=
1180-
ID_cprover_string_substring_func;
1181-
string_functions["java::java.lang.String.trim:()Ljava/lang/String;"]=
1182-
ID_cprover_string_trim_func;
1215+
// "java.lang.String.toCharArray has a special treatment in the
1216+
// replace_string_calls function
11831217
string_functions["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
11841218
ID_cprover_string_to_lower_case_func;
1219+
// Not supported "java.lang.String.toLowerCase:(Locale)"
1220+
// Not supported "java.lang.String.toString:()"
11851221
string_functions["java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
11861222
ID_cprover_string_to_upper_case_func;
1187-
string_functions["java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
1188-
ID_cprover_string_replace_func;
1189-
string_functions
1190-
["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
1191-
ID_cprover_string_contains_func;
1192-
string_functions["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
1193-
ID_cprover_string_compare_to_func;
1194-
string_functions["java::java.lang.String.intern:()Ljava/lang/String;"]=
1195-
ID_cprover_string_intern_func;
1196-
string_functions["java::java.lang.String.isEmpty:()Z"]=
1197-
ID_cprover_string_is_empty_func;
1198-
string_functions["java::java.lang.String.charAt:(I)C"]=
1199-
ID_cprover_string_char_at_func;
1200-
string_functions["java::java.lang.StringBuilder.charAt:(I)C"]=
1201-
ID_cprover_string_char_at_func;
1202-
string_functions["java::java.lang.CharSequence.charAt:(I)C"]=
1203-
ID_cprover_string_char_at_func;
1204-
string_functions
1205-
["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"]=
1223+
// Not supported "java.lang.String.toUpperCase:(Locale)"
1224+
string_functions["java::java.lang.String.trim:()Ljava/lang/String;"]=
1225+
ID_cprover_string_trim_func;
1226+
string_functions["java::java.lang.String.valueOf:(Z)Ljava/lang/String;"]=
1227+
ID_cprover_string_of_bool_func;
1228+
string_functions["java::java.lang.String.valueOf:(C)Ljava/lang/String;"]=
1229+
ID_cprover_string_of_char_func;
1230+
string_functions["java::java.lang.String.valueOf:([C)Ljava/lang/String;"]=
12061231
ID_cprover_string_copy_func;
1207-
1232+
string_functions["java::java.lang.String.valueOf:([CII)Ljava/lang/String;"]=
1233+
ID_cprover_string_copy_func;
1234+
string_functions["java::java.lang.String.valueOf:(D)Ljava/lang/String;"]=
1235+
ID_cprover_string_of_double_func;
12081236
string_functions["java::java.lang.String.valueOf:(F)Ljava/lang/String;"]=
12091237
ID_cprover_string_of_float_func;
1210-
string_functions["java::java.lang.Float.toString:(F)Ljava/lang/String;"]=
1211-
ID_cprover_string_of_float_func;
1212-
string_functions["java::java.lang.Integer.toString:(I)Ljava/lang/String;"]=
1213-
ID_cprover_string_of_int_func;
12141238
string_functions["java::java.lang.String.valueOf:(I)Ljava/lang/String;"]=
12151239
ID_cprover_string_of_int_func;
1216-
string_functions["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
1217-
ID_cprover_string_of_int_hex_func;
12181240
string_functions["java::java.lang.String.valueOf:(L)Ljava/lang/String;"]=
12191241
ID_cprover_string_of_long_func;
1220-
string_functions["java::java.lang.String.valueOf:(D)Ljava/lang/String;"]=
1221-
ID_cprover_string_of_double_func;
1222-
string_functions["java::java.lang.String.valueOf:(Z)Ljava/lang/String;"]=
1223-
ID_cprover_string_of_bool_func;
1224-
string_functions["java::java.lang.String.valueOf:(C)Ljava/lang/String;"]=
1225-
ID_cprover_string_of_char_func;
1226-
string_functions["java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]=
1227-
ID_cprover_string_parse_int_func;
1242+
// Not supported "java.lang.String.valueOf:(LObject;)"
1243+
1244+
// StringBuilder library
1245+
string_function_calls
1246+
["java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"]=
1247+
ID_cprover_string_copy_func;
1248+
string_function_calls["java::java.lang.StringBuilder.<init>:()V"]=
1249+
ID_cprover_string_empty_string_func;
12281250

1229-
side_effect_functions
1230-
["java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
1231-
"Ljava/lang/StringBuilder;"]=
1232-
ID_cprover_string_concat_func;
1233-
side_effect_functions["java::java.lang.StringBuilder.setCharAt:(IC)V"]=
1234-
ID_cprover_string_char_set_func;
1235-
side_effect_functions
1236-
["java::java.lang.StringBuilder.append:(I)Ljava/lang/StringBuilder;"]=
1237-
ID_cprover_string_concat_int_func;
1238-
side_effect_functions
1239-
["java::java.lang.StringBuilder.append:(J)Ljava/lang/StringBuilder;"]=
1240-
ID_cprover_string_concat_long_func;
12411251
side_effect_functions
12421252
["java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;"]=
12431253
ID_cprover_string_concat_bool_func;
12441254
side_effect_functions
1245-
["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
1246-
ID_cprover_string_concat_char_func;
1255+
["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
1256+
ID_cprover_string_concat_char_func;
1257+
side_effect_functions
1258+
["java::java.lang.StringBuilder.append:([C)"
1259+
"Ljava/lang/StringBuilder;"]=
1260+
ID_cprover_string_concat_func;
1261+
// Not supported: "java.lang.StringBuilder.append:([CII)"
1262+
// Not supported: "java.lang.StringBuilder.append:(LCharSequence;)"
12471263
side_effect_functions
12481264
["java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"]=
12491265
ID_cprover_string_concat_double_func;
12501266
side_effect_functions
12511267
["java::java.lang.StringBuilder.append:(F)Ljava/lang/StringBuilder;"]=
12521268
ID_cprover_string_concat_float_func;
1269+
side_effect_functions
1270+
["java::java.lang.StringBuilder.append:(I)Ljava/lang/StringBuilder;"]=
1271+
ID_cprover_string_concat_int_func;
1272+
side_effect_functions
1273+
["java::java.lang.StringBuilder.append:(J)Ljava/lang/StringBuilder;"]=
1274+
ID_cprover_string_concat_long_func;
1275+
// Not supported: "java.lang.StringBuilder.append:(LObject;)"
1276+
side_effect_functions
1277+
["java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
1278+
"Ljava/lang/StringBuilder;"]=
1279+
ID_cprover_string_concat_func;
12531280
side_effect_functions
12541281
["java::java.lang.StringBuilder.appendCodePoint:(I)"
12551282
"Ljava/lang/StringBuilder;"]=
12561283
ID_cprover_string_concat_code_point_func;
1284+
// Not supported: "java.lang.StringBuilder.append:(Ljava/lang/StringBuffer;)"
1285+
// Not supported: "java.lang.StringBuilder.capacity:()"
1286+
string_functions["java::java.lang.StringBuilder.charAt:(I)C"]=
1287+
ID_cprover_string_char_at_func;
1288+
string_functions["java::java.lang.StringBuilder.codePointAt:(I)I"]=
1289+
ID_cprover_string_code_point_at_func;
1290+
string_functions["java::java.lang.StringBuilder.codePointBefore:(I)I"]=
1291+
ID_cprover_string_code_point_before_func;
1292+
string_functions["java::java.lang.StringBuilder.codePointCount:(II)I"]=
1293+
ID_cprover_string_code_point_count_func;
12571294
side_effect_functions
12581295
["java::java.lang.StringBuilder.delete:(II)Ljava/lang/StringBuilder;"]=
12591296
ID_cprover_string_delete_func;
12601297
side_effect_functions
12611298
["java::java.lang.StringBuilder.deleteCharAt:(I)Ljava/lang/StringBuilder;"]=
12621299
ID_cprover_string_delete_char_at_func;
1300+
// Not supported: "java.lang.StringBuilder.ensureCapacity:()"
1301+
// Not supported: "java.lang.StringBuilder.getChars:()"
1302+
// Not supported: "java.lang.StringBuilder.indexOf:()"
12631303
side_effect_functions
1264-
["java::java.lang.StringBuilder.insert:(ILjava/lang/String;)"
1265-
"Ljava/lang/StringBuilder;"]=
1304+
["java::java.lang.StringBuilder.insert:(IZ)Ljava/lang/StringBuilder;"]=
1305+
ID_cprover_string_insert_bool_func;
1306+
side_effect_functions
1307+
["java::java.lang.StringBuilder.insert:(IC)Ljava/lang/StringBuilder;"]=
1308+
ID_cprover_string_insert_char_func;
1309+
side_effect_functions
1310+
["java::java.lang.StringBuilder.insert:(I[C)Ljava/lang/StringBuilder;"]=
12661311
ID_cprover_string_insert_func;
1312+
side_effect_functions
1313+
["java::java.lang.StringBuilder.insert:(I[CII)Ljava/lang/StringBuilder;"]=
1314+
ID_cprover_string_insert_func;
1315+
// Not supported "java.lang.StringBuilder.insert:(ILCharSequence;)"
1316+
// Not supported "java.lang.StringBuilder.insert:(ILCharSequence;II)"
1317+
// Not supported "java.lang.StringBuilder.insert:(ID)"
1318+
// Not supported "java.lang.StringBuilder.insert:(IF)"
12671319
side_effect_functions
12681320
["java::java.lang.StringBuilder.insert:(II)Ljava/lang/StringBuilder;"]=
12691321
ID_cprover_string_insert_int_func;
12701322
side_effect_functions
12711323
["java::java.lang.StringBuilder.insert:(IJ)Ljava/lang/StringBuilder;"]=
12721324
ID_cprover_string_insert_long_func;
1325+
// Not supported "java.lang.StringBuilder.insert:(ILObject;)"
12731326
side_effect_functions
1274-
["java::java.lang.StringBuilder.insert:(IC)Ljava/lang/StringBuilder;"]=
1275-
ID_cprover_string_insert_char_func;
1276-
side_effect_functions
1277-
["java::java.lang.StringBuilder.insert:(IZ)Ljava/lang/StringBuilder;"]=
1278-
ID_cprover_string_insert_bool_func;
1327+
["java::java.lang.StringBuilder.insert:(ILjava/lang/String;)"
1328+
"Ljava/lang/StringBuilder;"]=
1329+
ID_cprover_string_insert_func;
1330+
// Not supported "java.lang.StringBuilder.lastIndexOf"
1331+
string_functions["java::java.lang.StringBuilder.length:()I"]=
1332+
ID_cprover_string_length_func;
1333+
// Not supported "java.lang.StringBuilder.offsetByCodePoints"
1334+
// Not supported "java.lang.StringBuilder.replace"
1335+
// Not supported "java.lang.StringBuilder.reverse"
1336+
side_effect_functions["java::java.lang.StringBuilder.setCharAt:(IC)V"]=
1337+
ID_cprover_string_char_set_func;
12791338
side_effect_functions
12801339
["java::java.lang.StringBuilder.setLength:(I)V"]=
12811340
ID_cprover_string_set_length_func;
1282-
1283-
1284-
1285-
side_effect_functions
1286-
["java::java.lang.StringBuilder.append:([C)"
1287-
"Ljava/lang/StringBuilder;"]=
1288-
ID_cprover_string_concat_func;
1289-
side_effect_functions
1290-
["java::java.lang.StringBuilder.insert:(I[CII)Ljava/lang/StringBuilder;"]=
1291-
ID_cprover_string_insert_func;
1292-
side_effect_functions
1293-
["java::java.lang.StringBuilder.insert:(I[C)Ljava/lang/StringBuilder;"]=
1294-
ID_cprover_string_insert_func;
1295-
// TODO clean irep ids from insert_char_array etc...
1296-
1297-
string_function_calls
1298-
["java::java.lang.String.<init>:(Ljava/lang/String;)V"]=
1299-
ID_cprover_string_copy_func;
1300-
string_function_calls
1301-
["java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"]=
1302-
ID_cprover_string_copy_func;
1303-
string_function_calls
1304-
["java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"]=
1305-
ID_cprover_string_copy_func;
1306-
string_function_calls["java::java.lang.String.<init>:()V"]=
1307-
ID_cprover_string_empty_string_func;
1308-
string_function_calls["java::java.lang.StringBuilder.<init>:()V"]=
1309-
ID_cprover_string_empty_string_func;
1310-
1311-
string_function_calls["java::java.lang.String.<init>:([C)V"]=
1312-
ID_cprover_string_copy_func;
1313-
string_function_calls["java::java.lang.String.<init>:([CII)V"]=
1314-
ID_cprover_string_copy_func;
1315-
1341+
// Not supported "java.lang.StringBuilder.subSequence"
13161342
string_functions
1317-
["java::java.lang.String.valueOf:([CII)Ljava/lang/String;"]=
1318-
ID_cprover_string_copy_func;
1319-
string_functions
1320-
["java::java.lang.String.valueOf:([C)Ljava/lang/String;"]=
1321-
ID_cprover_string_copy_func;
1343+
["java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
1344+
ID_cprover_string_substring_func;
13221345
string_functions
1323-
["java::java.lang.String.copyValueOf:([CII)Ljava/lang/String;"]=
1324-
ID_cprover_string_copy_func;
1346+
["java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
1347+
ID_cprover_string_substring_func;
13251348
string_functions
1326-
["java::java.lang.String.copyValueOf:([C)Ljava/lang/String;"]=
1349+
["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"]=
13271350
ID_cprover_string_copy_func;
1351+
// Not supported "java.lang.StringBuilder.trimToSize"
1352+
// TODO clean irep ids from insert_char_array etc...
1353+
1354+
// Other libraries
1355+
string_functions["java::java.lang.CharSequence.charAt:(I)C"]=
1356+
ID_cprover_string_char_at_func;
1357+
string_functions["java::java.lang.Float.toString:(F)Ljava/lang/String;"]=
1358+
ID_cprover_string_of_float_func;
1359+
string_functions["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
1360+
ID_cprover_string_of_int_hex_func;
1361+
string_functions["java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]=
1362+
ID_cprover_string_parse_int_func;
1363+
string_functions["java::java.lang.Integer.toString:(I)Ljava/lang/String;"]=
1364+
ID_cprover_string_of_int_func;
13281365

1366+
// C functions
13291367
c_string_functions["__CPROVER_uninterpreted_string_literal_func"]=
13301368
ID_cprover_string_literal_func;
13311369
c_string_functions["__CPROVER_uninterpreted_string_char_at_func"]=
@@ -1357,6 +1395,7 @@ void string_refine_preprocesst::initialize_string_function_table()
13571395
c_string_functions["__CPROVER_uninterpreted_string_of_int_func"]=
13581396
ID_cprover_string_of_int_func;
13591397

1398+
// Signatures
13601399
signatures["java::java.lang.String.equals:(Ljava/lang/Object;)Z"]="SSZ";
13611400
signatures["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
13621401
"SSZ";

0 commit comments

Comments
 (0)