Skip to content

Commit a95e8dc

Browse files
romainbrenguierromainbrenguier
committed
Removing comments on non-supported functions in string preprocessing
We remove comments about non-supported method as models may be provided for the ones that are not supported internally. Ultimately all the methods that are not supported internally should have models provided for them.
1 parent b0b21bb commit a95e8dc

File tree

1 file changed

+0
-61
lines changed

1 file changed

+0
-61
lines changed

‎src/java_bytecode/java_string_library_preprocess.cpp

-61
Original file line numberDiff line numberDiff line change
@@ -1417,7 +1417,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
14171417
cprover_equivalent_to_java_constructor
14181418
["java::java.lang.String.<init>:()V"]=
14191419
ID_cprover_string_empty_string_func;
1420-
// Not supported java.lang.String.<init>:(Ljava/lang/StringBuffer;)
14211420

14221421
cprover_equivalent_to_java_function
14231422
["java::java.lang.String.charAt:(I)C"]=
@@ -1434,7 +1433,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
14341433
cprover_equivalent_to_java_function
14351434
["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
14361435
ID_cprover_string_compare_to_func;
1437-
// Not supported "java.lang.String.contentEquals"
14381436
cprover_equivalent_to_java_string_returning_function
14391437
["java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
14401438
ID_cprover_string_concat_func;
@@ -1461,9 +1459,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
14611459
cprover_equivalent_to_java_function
14621460
["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
14631461
ID_cprover_string_equals_ignore_case_func;
1464-
// Not supported "java.lang.String.format"
1465-
// Not supported "java.lang.String.getBytes"
1466-
// Not supported "java.lang.String.getChars"
14671462
cprover_equivalent_to_java_function
14681463
["java::java.lang.String.hashCode:()I"]=
14691464
ID_cprover_string_hash_code_func;
@@ -1505,18 +1500,12 @@ void java_string_library_preprocesst::initialize_conversion_table()
15051500
std::placeholders::_1,
15061501
std::placeholders::_2,
15071502
std::placeholders::_3);
1508-
// Not supported "java.lang.String.matches"
15091503
cprover_equivalent_to_java_function
15101504
["java::java.lang.String.offsetByCodePoints:(II)I"]=
15111505
ID_cprover_string_offset_by_code_point_func;
1512-
// Not supported "java.lang.String.regionMatches"
15131506
cprover_equivalent_to_java_string_returning_function
15141507
["java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
15151508
ID_cprover_string_replace_func;
1516-
// Not supported "java.lang.String.replace:(LCharSequence;LCharSequence)"
1517-
// Not supported "java.lang.String.replaceAll"
1518-
// Not supported "java.lang.String.replaceFirst"
1519-
// Not supported "java.lang.String.split"
15201509
cprover_equivalent_to_java_function
15211510
["java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
15221511
ID_cprover_string_startswith_func;
@@ -1543,12 +1532,9 @@ void java_string_library_preprocesst::initialize_conversion_table()
15431532
cprover_equivalent_to_java_string_returning_function
15441533
["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
15451534
ID_cprover_string_to_lower_case_func;
1546-
// Not supported "java.lang.String.toLowerCase:(Locale)"
1547-
// Not supported "java.lang.String.toString:()"
15481535
cprover_equivalent_to_java_string_returning_function
15491536
["java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
15501537
ID_cprover_string_to_upper_case_func;
1551-
// Not supported "java.lang.String.toUpperCase:(Locale)"
15521538
cprover_equivalent_to_java_string_returning_function
15531539
["java::java.lang.String.trim:()Ljava/lang/String;"]=
15541540
ID_cprover_string_trim_func;
@@ -1576,7 +1562,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
15761562
cprover_equivalent_to_java_string_returning_function
15771563
["java::java.lang.String.valueOf:(J)Ljava/lang/String;"]=
15781564
ID_cprover_string_of_long_func;
1579-
// Not supported "java.lang.String.valueOf:(LObject;)"
15801565

15811566
// StringBuilder library
15821567
conversion_table
@@ -1601,8 +1586,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
16011586
["java::java.lang.StringBuilder.append:([C)"
16021587
"Ljava/lang/StringBuilder;"]=
16031588
ID_cprover_string_concat_func;
1604-
// Not supported: "java.lang.StringBuilder.append:([CII)"
1605-
16061589
cprover_equivalent_to_java_assign_and_return_function
16071590
["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;II)"
16081591
"Ljava/lang/StringBuilder;"]=
@@ -1615,14 +1598,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
16151598
cprover_equivalent_to_java_assign_and_return_function
16161599
["java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"]=
16171600
ID_cprover_string_concat_double_func;
1618-
// Not supported: "java.lang.StringBuilder.append:"
1619-
// "(F)Ljava/lang/StringBuilder;"
1620-
// Not supported: "java.lang.StringBuilder.append:(I)"
1621-
// "Ljava/lang/StringBuilder;"
1622-
// Not supported: "java.lang.StringBuilder.append:(J)"
1623-
// "Ljava/lang/StringBuilder;"
1624-
// Not supported: "java.lang.StringBuilder.append:"
1625-
// "(Ljava/lang/Object;)Ljava/lang/StringBuilder;"
16261601
cprover_equivalent_to_java_assign_and_return_function
16271602
["java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
16281603
"Ljava/lang/StringBuilder;"]=
@@ -1631,8 +1606,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
16311606
["java::java.lang.StringBuilder.appendCodePoint:(I)"
16321607
"Ljava/lang/StringBuilder;"]=
16331608
ID_cprover_string_concat_code_point_func;
1634-
// Not supported: "java.lang.StringBuilder.append:(Ljava/lang/StringBuffer;)"
1635-
// Not supported: "java.lang.StringBuilder.capacity:()"
16361609
cprover_equivalent_to_java_function
16371610
["java::java.lang.StringBuilder.charAt:(I)C"]=
16381611
ID_cprover_string_char_at_func;
@@ -1651,9 +1624,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
16511624
cprover_equivalent_to_java_assign_and_return_function
16521625
["java::java.lang.StringBuilder.deleteCharAt:(I)Ljava/lang/StringBuilder;"]=
16531626
ID_cprover_string_delete_char_at_func;
1654-
// Not supported: "java.lang.StringBuilder.ensureCapacity:()"
1655-
// Not supported: "java.lang.StringBuilder.getChars:()"
1656-
// Not supported: "java.lang.StringBuilder.indexOf:()"
16571627
cprover_equivalent_to_java_assign_and_return_function
16581628
["java::java.lang.StringBuilder.insert:(IZ)Ljava/lang/StringBuilder;"]=
16591629
ID_cprover_string_insert_bool_func;
@@ -1666,35 +1636,25 @@ void java_string_library_preprocesst::initialize_conversion_table()
16661636
cprover_equivalent_to_java_assign_and_return_function
16671637
["java::java.lang.StringBuilder.insert:(I[CII)Ljava/lang/StringBuilder;"]=
16681638
ID_cprover_string_insert_func;
1669-
// Not supported "java.lang.StringBuilder.insert:(ILCharSequence;)"
1670-
// Not supported "java.lang.StringBuilder.insert:(ILCharSequence;II)"
1671-
// Not supported "java.lang.StringBuilder.insert:(ID)"
1672-
// Not supported "java.lang.StringBuilder.insert:(IF)"
16731639
cprover_equivalent_to_java_assign_and_return_function
16741640
["java::java.lang.StringBuilder.insert:(II)Ljava/lang/StringBuilder;"]=
16751641
ID_cprover_string_insert_int_func;
16761642
cprover_equivalent_to_java_assign_and_return_function
16771643
["java::java.lang.StringBuilder.insert:(IJ)Ljava/lang/StringBuilder;"]=
16781644
ID_cprover_string_insert_long_func;
1679-
// Not supported "java.lang.StringBuilder.insert:(ILObject;)"
16801645
cprover_equivalent_to_java_assign_and_return_function
16811646
["java::java.lang.StringBuilder.insert:(ILjava/lang/String;)"
16821647
"Ljava/lang/StringBuilder;"]=
16831648
ID_cprover_string_insert_func;
1684-
// Not supported "java.lang.StringBuilder.lastIndexOf"
16851649
conversion_table
16861650
["java::java.lang.StringBuilder.length:()I"]=
16871651
conversion_table["java::java.lang.String.length:()I"];
1688-
// Not supported "java.lang.StringBuilder.offsetByCodePoints"
1689-
// Not supported "java.lang.StringBuilder.replace"
1690-
// Not supported "java.lang.StringBuilder.reverse"
16911652
cprover_equivalent_to_java_assign_function
16921653
["java::java.lang.StringBuilder.setCharAt:(IC)V"]=
16931654
ID_cprover_string_char_set_func;
16941655
cprover_equivalent_to_java_assign_function
16951656
["java::java.lang.StringBuilder.setLength:(I)V"]=
16961657
ID_cprover_string_set_length_func;
1697-
// Not supported "java.lang.StringBuilder.subSequence"
16981658
cprover_equivalent_to_java_string_returning_function
16991659
["java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
17001660
ID_cprover_string_substring_func;
@@ -1709,8 +1669,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
17091669
std::placeholders::_1,
17101670
std::placeholders::_2,
17111671
std::placeholders::_3);
1712-
// Not supported "java.lang.StringBuilder.trimToSize"
1713-
// TODO clean irep ids from insert_char_array etc...
17141672

17151673
// StringBuffer library
17161674
conversion_table
@@ -1735,8 +1693,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
17351693
["java::java.lang.StringBuffer.append:([C)"
17361694
"Ljava/lang/StringBuffer;"]=
17371695
ID_cprover_string_concat_func;
1738-
// Not supported: "java.lang.StringBuffer.append:([CII)"
1739-
// Not supported: "java.lang.StringBuffer.append:(LCharSequence;)"
17401696
cprover_equivalent_to_java_assign_and_return_function
17411697
["java::java.lang.StringBuffer.append:(D)Ljava/lang/StringBuffer;"]=
17421698
ID_cprover_string_concat_double_func;
@@ -1749,7 +1705,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
17491705
cprover_equivalent_to_java_assign_and_return_function
17501706
["java::java.lang.StringBuffer.append:(J)Ljava/lang/StringBuffer;"]=
17511707
ID_cprover_string_concat_long_func;
1752-
// Not supported: "java.lang.StringBuffer.append:(LObject;)"
17531708
cprover_equivalent_to_java_assign_and_return_function
17541709
["java::java.lang.StringBuffer.append:(Ljava/lang/String;)"
17551710
"Ljava/lang/StringBuffer;"]=
@@ -1758,8 +1713,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
17581713
["java::java.lang.StringBuffer.appendCodePoint:(I)"
17591714
"Ljava/lang/StringBuffer;"]=
17601715
ID_cprover_string_concat_code_point_func;
1761-
// Not supported: "java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)"
1762-
// Not supported: "java.lang.StringBuffer.capacity:()"
17631716
cprover_equivalent_to_java_function
17641717
["java::java.lang.StringBuffer.charAt:(I)C"]=
17651718
ID_cprover_string_char_at_func;
@@ -1778,9 +1731,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
17781731
cprover_equivalent_to_java_assign_and_return_function
17791732
["java::java.lang.StringBuffer.deleteCharAt:(I)Ljava/lang/StringBuffer;"]=
17801733
ID_cprover_string_delete_char_at_func;
1781-
// Not supported: "java.lang.StringBuffer.ensureCapacity:()"
1782-
// Not supported: "java.lang.StringBuffer.getChars:()"
1783-
// Not supported: "java.lang.StringBuffer.indexOf:()"
17841734
cprover_equivalent_to_java_assign_and_return_function
17851735
["java::java.lang.StringBuffer.insert:(IZ)Ljava/lang/StringBuffer;"]=
17861736
ID_cprover_string_insert_bool_func;
@@ -1793,35 +1743,25 @@ void java_string_library_preprocesst::initialize_conversion_table()
17931743
cprover_equivalent_to_java_assign_and_return_function
17941744
["java::java.lang.StringBuffer.insert:(I[CII)Ljava/lang/StringBuffer;"]=
17951745
ID_cprover_string_insert_func;
1796-
// Not supported "java.lang.StringBuffer.insert:(ILCharSequence;)"
1797-
// Not supported "java.lang.StringBuffer.insert:(ILCharSequence;II)"
1798-
// Not supported "java.lang.StringBuffer.insert:(ID)"
1799-
// Not supported "java.lang.StringBuffer.insert:(IF)"
18001746
cprover_equivalent_to_java_assign_and_return_function
18011747
["java::java.lang.StringBuffer.insert:(II)Ljava/lang/StringBuffer;"]=
18021748
ID_cprover_string_insert_int_func;
18031749
cprover_equivalent_to_java_assign_and_return_function
18041750
["java::java.lang.StringBuffer.insert:(IJ)Ljava/lang/StringBuffer;"]=
18051751
ID_cprover_string_insert_long_func;
1806-
// Not supported "java.lang.StringBuffer.insert:(ILObject;)"
18071752
cprover_equivalent_to_java_assign_and_return_function
18081753
["java::java.lang.StringBuffer.insert:(ILjava/lang/String;)"
18091754
"Ljava/lang/StringBuffer;"]=
18101755
ID_cprover_string_insert_func;
1811-
// Not supported "java.lang.StringBuffer.lastIndexOf"
18121756
conversion_table
18131757
["java::java.lang.StringBuffer.length:()I"]=
18141758
conversion_table["java::java.lang.String.length:()I"];
1815-
// Not supported "java.lang.StringBuffer.offsetByCodePoints"
1816-
// Not supported "java.lang.StringBuffer.replace"
1817-
// Not supported "java.lang.StringBuffer.reverse"
18181759
cprover_equivalent_to_java_assign_function
18191760
["java::java.lang.StringBuffer.setCharAt:(IC)V"]=
18201761
ID_cprover_string_char_set_func;
18211762
cprover_equivalent_to_java_assign_function
18221763
["java::java.lang.StringBuffer.setLength:(I)V"]=
18231764
ID_cprover_string_set_length_func;
1824-
// Not supported "java.lang.StringBuffer.subSequence"
18251765
cprover_equivalent_to_java_string_returning_function
18261766
["java::java.lang.StringBuffer.substring:(II)Ljava/lang/String;"]=
18271767
ID_cprover_string_substring_func;
@@ -1836,7 +1776,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
18361776
std::placeholders::_1,
18371777
std::placeholders::_2,
18381778
std::placeholders::_3);
1839-
// Not supported "java.lang.StringBuffer.trimToSize"
18401779

18411780
// CharSequence library
18421781
cprover_equivalent_to_java_function

0 commit comments

Comments
 (0)