@@ -1391,6 +1391,11 @@ void java_string_library_preprocesst::initialize_conversion_table()
13911391 " java.lang.CharSequence" ,
13921392 " java.lang.StringBuffer" };
13931393
1394+ // The following list of function is organized by libraries, with
1395+ // constructors first and then methods in alphabetic order.
1396+ // Methods that are not supported here should ultimately have Java models
1397+ // provided for them in the class-path.
1398+
13941399 // String library
13951400 conversion_table
13961401 [" java::java.lang.String.<init>:(Ljava/lang/String;)V" ]=
@@ -1576,32 +1581,31 @@ void java_string_library_preprocesst::initialize_conversion_table()
15761581 [" java::java.lang.StringBuilder.<init>:()V" ]=
15771582 ID_cprover_string_empty_string_func;
15781583
1579- cprover_equivalent_to_java_assign_and_return_function
1580- [" java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;" ]=
1581- ID_cprover_string_concat_bool_func;
15821584 cprover_equivalent_to_java_assign_and_return_function
15831585 [" java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;" ]=
15841586 ID_cprover_string_concat_char_func;
15851587 cprover_equivalent_to_java_assign_and_return_function
15861588 [" java::java.lang.StringBuilder.append:([C)"
15871589 " Ljava/lang/StringBuilder;" ]=
15881590 ID_cprover_string_concat_func;
1589- cprover_equivalent_to_java_assign_and_return_function
1590- [" java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;II)"
1591- " Ljava/lang/StringBuilder;" ]=
1592- ID_cprover_string_concat_func;
1593- cprover_equivalent_to_java_assign_and_return_function
1594- [" java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
1595- " Ljava/lang/StringBuilder;" ]=
1596- ID_cprover_string_concat_func;
1597-
15981591 cprover_equivalent_to_java_assign_and_return_function
15991592 [" java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;" ]=
16001593 ID_cprover_string_concat_double_func;
16011594 cprover_equivalent_to_java_assign_and_return_function
1602- [" java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
1603- " Ljava/lang/StringBuilder;" ]=
1604- ID_cprover_string_concat_func;
1595+ [" java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;II)"
1596+ " Ljava/lang/StringBuilder;" ]=
1597+ ID_cprover_string_concat_func;
1598+ cprover_equivalent_to_java_assign_and_return_function
1599+ [" java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
1600+ " Ljava/lang/StringBuilder;" ]=
1601+ ID_cprover_string_concat_func;
1602+ cprover_equivalent_to_java_assign_and_return_function
1603+ [" java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
1604+ " Ljava/lang/StringBuilder;" ]=
1605+ ID_cprover_string_concat_func;
1606+ cprover_equivalent_to_java_assign_and_return_function
1607+ [" java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;" ]=
1608+ ID_cprover_string_concat_bool_func;
16051609 cprover_equivalent_to_java_assign_and_return_function
16061610 [" java::java.lang.StringBuilder.appendCodePoint:(I)"
16071611 " Ljava/lang/StringBuilder;" ]=
@@ -1625,17 +1629,17 @@ void java_string_library_preprocesst::initialize_conversion_table()
16251629 [" java::java.lang.StringBuilder.deleteCharAt:(I)Ljava/lang/StringBuilder;" ]=
16261630 ID_cprover_string_delete_char_at_func;
16271631 cprover_equivalent_to_java_assign_and_return_function
1628- [" java::java.lang.StringBuilder.insert:(IZ)Ljava/lang/StringBuilder;" ]=
1629- ID_cprover_string_insert_bool_func;
1630- cprover_equivalent_to_java_assign_and_return_function
1631- [" java::java.lang.StringBuilder.insert:(IC)Ljava/lang/StringBuilder;" ]=
1632- ID_cprover_string_insert_char_func;
1632+ [" java::java.lang.StringBuilder.insert:(IC)Ljava/lang/StringBuilder;" ]=
1633+ ID_cprover_string_insert_char_func;
16331634 cprover_equivalent_to_java_assign_and_return_function
16341635 [" java::java.lang.StringBuilder.insert:(I[C)Ljava/lang/StringBuilder;" ]=
16351636 ID_cprover_string_insert_func;
16361637 cprover_equivalent_to_java_assign_and_return_function
16371638 [" java::java.lang.StringBuilder.insert:(I[CII)Ljava/lang/StringBuilder;" ]=
16381639 ID_cprover_string_insert_func;
1640+ cprover_equivalent_to_java_assign_and_return_function
1641+ [" java::java.lang.StringBuilder.insert:(IZ)Ljava/lang/StringBuilder;" ]=
1642+ ID_cprover_string_insert_bool_func;
16391643 cprover_equivalent_to_java_assign_and_return_function
16401644 [" java::java.lang.StringBuilder.insert:(II)Ljava/lang/StringBuilder;" ]=
16411645 ID_cprover_string_insert_int_func;
@@ -1648,7 +1652,12 @@ void java_string_library_preprocesst::initialize_conversion_table()
16481652 ID_cprover_string_insert_func;
16491653 conversion_table
16501654 [" java::java.lang.StringBuilder.length:()I" ]=
1651- conversion_table[" java::java.lang.String.length:()I" ];
1655+ std::bind (
1656+ &java_string_library_preprocesst::make_string_length_code,
1657+ this ,
1658+ std::placeholders::_1,
1659+ std::placeholders::_2,
1660+ std::placeholders::_3);
16521661 cprover_equivalent_to_java_assign_function
16531662 [" java::java.lang.StringBuilder.setCharAt:(IC)V" ]=
16541663 ID_cprover_string_char_set_func;
@@ -1683,9 +1692,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
16831692 [" java::java.lang.StringBuffer.<init>:()V" ]=
16841693 ID_cprover_string_empty_string_func;
16851694
1686- cprover_equivalent_to_java_assign_and_return_function
1687- [" java::java.lang.StringBuffer.append:(Z)Ljava/lang/StringBuffer;" ]=
1688- ID_cprover_string_concat_bool_func;
16891695 cprover_equivalent_to_java_assign_and_return_function
16901696 [" java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;" ]=
16911697 ID_cprover_string_concat_char_func;
@@ -1709,6 +1715,9 @@ void java_string_library_preprocesst::initialize_conversion_table()
17091715 [" java::java.lang.StringBuffer.append:(Ljava/lang/String;)"
17101716 " Ljava/lang/StringBuffer;" ]=
17111717 ID_cprover_string_concat_func;
1718+ cprover_equivalent_to_java_assign_and_return_function
1719+ [" java::java.lang.StringBuffer.append:(Z)Ljava/lang/StringBuffer;" ]=
1720+ ID_cprover_string_concat_bool_func;
17121721 cprover_equivalent_to_java_assign_and_return_function
17131722 [" java::java.lang.StringBuffer.appendCodePoint:(I)"
17141723 " Ljava/lang/StringBuffer;" ]=
@@ -1731,9 +1740,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
17311740 cprover_equivalent_to_java_assign_and_return_function
17321741 [" java::java.lang.StringBuffer.deleteCharAt:(I)Ljava/lang/StringBuffer;" ]=
17331742 ID_cprover_string_delete_char_at_func;
1734- cprover_equivalent_to_java_assign_and_return_function
1735- [" java::java.lang.StringBuffer.insert:(IZ)Ljava/lang/StringBuffer;" ]=
1736- ID_cprover_string_insert_bool_func;
17371743 cprover_equivalent_to_java_assign_and_return_function
17381744 [" java::java.lang.StringBuffer.insert:(IC)Ljava/lang/StringBuffer;" ]=
17391745 ID_cprover_string_insert_char_func;
@@ -1753,6 +1759,9 @@ void java_string_library_preprocesst::initialize_conversion_table()
17531759 [" java::java.lang.StringBuffer.insert:(ILjava/lang/String;)"
17541760 " Ljava/lang/StringBuffer;" ]=
17551761 ID_cprover_string_insert_func;
1762+ cprover_equivalent_to_java_assign_and_return_function
1763+ [" java::java.lang.StringBuffer.insert:(IZ)Ljava/lang/StringBuffer;" ]=
1764+ ID_cprover_string_insert_bool_func;
17561765 conversion_table
17571766 [" java::java.lang.StringBuffer.length:()I" ]=
17581767 conversion_table[" java::java.lang.String.length:()I" ];
@@ -1763,10 +1772,10 @@ void java_string_library_preprocesst::initialize_conversion_table()
17631772 [" java::java.lang.StringBuffer.setLength:(I)V" ]=
17641773 ID_cprover_string_set_length_func;
17651774 cprover_equivalent_to_java_string_returning_function
1766- [" java::java.lang.StringBuffer.substring:(II )Ljava/lang/String;" ]=
1775+ [" java::java.lang.StringBuffer.substring:(I )Ljava/lang/String;" ]=
17671776 ID_cprover_string_substring_func;
17681777 cprover_equivalent_to_java_string_returning_function
1769- [" java::java.lang.StringBuffer.substring:(I )Ljava/lang/String;" ]=
1778+ [" java::java.lang.StringBuffer.substring:(II )Ljava/lang/String;" ]=
17701779 ID_cprover_string_substring_func;
17711780 conversion_table
17721781 [" java::java.lang.StringBuffer.toString:()Ljava/lang/String;" ]=
@@ -1802,12 +1811,12 @@ void java_string_library_preprocesst::initialize_conversion_table()
18021811 std::placeholders::_1,
18031812 std::placeholders::_2,
18041813 std::placeholders::_3);
1805- cprover_equivalent_to_java_string_returning_function
1806- [" java::java.lang.Integer.toHexString:(I)Ljava/lang/String;" ]=
1807- ID_cprover_string_of_int_hex_func;
18081814 cprover_equivalent_to_java_function
18091815 [" java::java.lang.Integer.parseInt:(Ljava/lang/String;)I" ]=
18101816 ID_cprover_string_parse_int_func;
1817+ cprover_equivalent_to_java_string_returning_function
1818+ [" java::java.lang.Integer.toHexString:(I)Ljava/lang/String;" ]=
1819+ ID_cprover_string_of_int_hex_func;
18111820 cprover_equivalent_to_java_string_returning_function
18121821 [" java::java.lang.Integer.toString:(I)Ljava/lang/String;" ]=
18131822 ID_cprover_string_of_int_func;
0 commit comments