Skip to content

Commit c1894ab

Browse files
danpoedanpoe
committed
Group CProverString operations in initialize_conversion_table()
In the initialization of the conversion table, CProverString operations are grouped together for better readability.
1 parent c9284ae commit c1894ab

File tree

1 file changed

+74
-71
lines changed

1 file changed

+74
-71
lines changed

‎jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 74 additions & 71 deletions
Original file line numberDiff line numberDiff line change
@@ -1475,6 +1475,80 @@ void java_string_library_preprocesst::initialize_conversion_table()
14751475
// Methods that are not supported here should ultimately have Java models
14761476
// provided for them in the class-path.
14771477

1478+
// CProverString library
1479+
cprover_equivalent_to_java_assign_and_return_function
1480+
["java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/"
1481+
"lang/CharSequence;II)"
1482+
"Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1483+
// CProverString.charAt differs from the Java String.charAt in that no
1484+
// exception is raised for the out of bounds case.
1485+
cprover_equivalent_to_java_function
1486+
["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"]=
1487+
ID_cprover_string_char_at_func;
1488+
cprover_equivalent_to_java_function
1489+
["java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
1490+
ID_cprover_string_char_at_func;
1491+
cprover_equivalent_to_java_function
1492+
["java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
1493+
ID_cprover_string_code_point_at_func;
1494+
cprover_equivalent_to_java_function
1495+
["java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
1496+
ID_cprover_string_code_point_before_func;
1497+
cprover_equivalent_to_java_function
1498+
["java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
1499+
ID_cprover_string_code_point_count_func;
1500+
cprover_equivalent_to_java_assign_and_return_function
1501+
["java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/"
1502+
"lang/StringBuffer;"] = ID_cprover_string_delete_func;
1503+
cprover_equivalent_to_java_assign_and_return_function
1504+
["java::org.cprover.CProverString.delete:(Ljava/lang/"
1505+
"StringBuilder;II)Ljava/lang/StringBuilder;"] =
1506+
ID_cprover_string_delete_func;
1507+
cprover_equivalent_to_java_assign_and_return_function
1508+
["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1509+
"StringBufferI)Ljava/lang/StringBuffer;"] =
1510+
ID_cprover_string_delete_char_at_func;
1511+
cprover_equivalent_to_java_assign_and_return_function
1512+
["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1513+
"StringBuilder;I)Ljava/lang/StringBuilder;"] =
1514+
ID_cprover_string_delete_char_at_func;
1515+
1516+
std::string format_signature = "java::org.cprover.CProverString.format:(";
1517+
for(std::size_t i = 0; i < MAX_FORMAT_ARGS + 1; ++i)
1518+
format_signature += "Ljava/lang/String;";
1519+
format_signature += ")Ljava/lang/String;";
1520+
cprover_equivalent_to_java_string_returning_function[format_signature] =
1521+
ID_cprover_string_format_func;
1522+
1523+
cprover_equivalent_to_java_assign_and_return_function
1524+
["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
1525+
"lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
1526+
cprover_equivalent_to_java_function
1527+
["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
1528+
"String;II)I"] = ID_cprover_string_offset_by_code_point_func;
1529+
cprover_equivalent_to_java_assign_function
1530+
["java::org.cprover.CProverString.setCharAt:(Ljava/lang/String;IC)V"] =
1531+
ID_cprover_string_char_set_func;
1532+
cprover_equivalent_to_java_assign_function
1533+
["java::org.cprover.CProverString.setLength:(Ljava/lang/String;I)V"] =
1534+
ID_cprover_string_set_length_func;
1535+
cprover_equivalent_to_java_string_returning_function
1536+
["java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
1537+
"lang/CharSequence;"] = ID_cprover_string_substring_func;
1538+
// CProverString.substring differs from the Java String.substring in that no
1539+
// exception is raised for the out of bounds case.
1540+
cprover_equivalent_to_java_string_returning_function
1541+
["java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
1542+
"Ljava/lang/String;"]=
1543+
ID_cprover_string_substring_func;
1544+
cprover_equivalent_to_java_string_returning_function
1545+
["java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
1546+
"Ljava/lang/String;"]=
1547+
ID_cprover_string_substring_func;
1548+
cprover_equivalent_to_java_string_returning_function
1549+
["java::org.cprover.CProverString.substring:(Ljava/Lang/"
1550+
"StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
1551+
14781552
// String library
14791553
conversion_table["java::java.lang.String.<init>:(Ljava/lang/String;)V"] =
14801554
std::bind(
@@ -1496,20 +1570,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
14961570
["java::java.lang.String.<init>:()V"]=
14971571
ID_cprover_string_empty_string_func;
14981572

1499-
// CProverString.charAt differs from the Java String.charAt in that no
1500-
// exception is raised for the out of bounds case.
1501-
cprover_equivalent_to_java_function
1502-
["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"]=
1503-
ID_cprover_string_char_at_func;
1504-
cprover_equivalent_to_java_function
1505-
["java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
1506-
ID_cprover_string_code_point_at_func;
1507-
cprover_equivalent_to_java_function
1508-
["java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
1509-
ID_cprover_string_code_point_before_func;
1510-
cprover_equivalent_to_java_function
1511-
["java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
1512-
ID_cprover_string_code_point_count_func;
15131573
cprover_equivalent_to_java_function
15141574
["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
15151575
ID_cprover_string_compare_to_func;
@@ -1526,13 +1586,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
15261586
["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
15271587
ID_cprover_string_equals_ignore_case_func;
15281588

1529-
std::string format_signature = "java::org.cprover.CProverString.format:(";
1530-
for(std::size_t i = 0; i < MAX_FORMAT_ARGS + 1; ++i)
1531-
format_signature += "Ljava/lang/String;";
1532-
format_signature += ")Ljava/lang/String;";
1533-
cprover_equivalent_to_java_string_returning_function[format_signature] =
1534-
ID_cprover_string_format_func;
1535-
15361589
cprover_equivalent_to_java_function
15371590
["java::java.lang.String.indexOf:(I)I"]=
15381591
ID_cprover_string_index_of_func;
@@ -1567,9 +1620,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
15671620
std::placeholders::_2,
15681621
std::placeholders::_3,
15691622
std::placeholders::_4);
1570-
cprover_equivalent_to_java_function
1571-
["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
1572-
"String;II)I"] = ID_cprover_string_offset_by_code_point_func;
15731623
cprover_equivalent_to_java_string_returning_function
15741624
["java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
15751625
ID_cprover_string_replace_func;
@@ -1582,19 +1632,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
15821632
cprover_equivalent_to_java_function
15831633
["java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
15841634
ID_cprover_string_startswith_func;
1585-
cprover_equivalent_to_java_string_returning_function
1586-
["java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
1587-
"lang/CharSequence;"] = ID_cprover_string_substring_func;
1588-
// CProverString.substring differs from the Java String.substring in that no
1589-
// exception is raised for the out of bounds case.
1590-
cprover_equivalent_to_java_string_returning_function
1591-
["java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
1592-
"Ljava/lang/String;"]=
1593-
ID_cprover_string_substring_func;
1594-
cprover_equivalent_to_java_string_returning_function
1595-
["java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
1596-
"Ljava/lang/String;"]=
1597-
ID_cprover_string_substring_func;
15981635
cprover_equivalent_to_java_string_returning_function
15991636
["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
16001637
ID_cprover_string_to_lower_case_func;
@@ -1649,10 +1686,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
16491686
cprover_equivalent_to_java_assign_and_return_function
16501687
["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
16511688
ID_cprover_string_concat_char_func;
1652-
cprover_equivalent_to_java_assign_and_return_function
1653-
["java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/"
1654-
"lang/CharSequence;II)"
1655-
"Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
16561689
cprover_equivalent_to_java_assign_and_return_function
16571690
["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
16581691
"Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
@@ -1675,17 +1708,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
16751708
cprover_equivalent_to_java_function
16761709
["java::java.lang.StringBuilder.codePointCount:(II)I"]=
16771710
ID_cprover_string_code_point_count_func;
1678-
cprover_equivalent_to_java_assign_and_return_function
1679-
["java::org.cprover.CProverString.delete:(Ljava/lang/"
1680-
"StringBuilder;II)Ljava/lang/StringBuilder;"] =
1681-
ID_cprover_string_delete_func;
1682-
cprover_equivalent_to_java_assign_and_return_function
1683-
["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1684-
"StringBuilder;I)Ljava/lang/StringBuilder;"] =
1685-
ID_cprover_string_delete_char_at_func;
1686-
cprover_equivalent_to_java_assign_and_return_function
1687-
["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
1688-
"lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
16891711
conversion_table["java::java.lang.StringBuilder.length:()I"] = std::bind(
16901712
&java_string_library_preprocesst::make_string_length_code,
16911713
this,
@@ -1744,9 +1766,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
17441766
["java::java.lang.StringBuffer.appendCodePoint:(I)"
17451767
"Ljava/lang/StringBuffer;"]=
17461768
ID_cprover_string_concat_code_point_func;
1747-
cprover_equivalent_to_java_function
1748-
["java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
1749-
ID_cprover_string_char_at_func;
17501769
cprover_equivalent_to_java_function
17511770
["java::java.lang.StringBuffer.codePointAt:(I)I"]=
17521771
ID_cprover_string_code_point_at_func;
@@ -1756,28 +1775,12 @@ void java_string_library_preprocesst::initialize_conversion_table()
17561775
cprover_equivalent_to_java_function
17571776
["java::java.lang.StringBuffer.codePointCount:(II)I"]=
17581777
ID_cprover_string_code_point_count_func;
1759-
cprover_equivalent_to_java_assign_and_return_function
1760-
["java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/"
1761-
"lang/StringBuffer;"] = ID_cprover_string_delete_func;
1762-
cprover_equivalent_to_java_assign_and_return_function
1763-
["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1764-
"StringBufferI)Ljava/lang/StringBuffer;"] =
1765-
ID_cprover_string_delete_char_at_func;
17661778
conversion_table
17671779
["java::java.lang.StringBuffer.length:()I"]=
17681780
conversion_table["java::java.lang.String.length:()I"];
1769-
cprover_equivalent_to_java_assign_function
1770-
["java::org.cprover.CProverString.setCharAt:(Ljava/lang/String;IC)V"] =
1771-
ID_cprover_string_char_set_func;
1772-
cprover_equivalent_to_java_assign_function
1773-
["java::org.cprover.CProverString.setLength:(Ljava/lang/String;I)V"] =
1774-
ID_cprover_string_set_length_func;
17751781
cprover_equivalent_to_java_string_returning_function
17761782
["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
17771783
ID_cprover_string_substring_func;
1778-
cprover_equivalent_to_java_string_returning_function
1779-
["java::org.cprover.CProverString.substring:(Ljava/Lang/"
1780-
"StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
17811784
conversion_table
17821785
["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
17831786
&java_string_library_preprocesst::make_copy_string_code,

0 commit comments

Comments
 (0)