Use faster character version of rfind

NathanJPhillips · NathanJPhillips · commit 753ef165251c · 2019-07-24T18:38:33.000+01:00
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -1158,7 +1158,7 @@ void mark_java_implicitly_generic_class_type(
   // the order from the outer-most inwards
   std::vector<java_generic_parametert> implicit_generic_type_parameters;
   std::string::size_type outer_class_delimiter =
-    qualified_class_name.rfind("$");
+    qualified_class_name.rfind('$');
   while(outer_class_delimiter != std::string::npos)
   {
     std::string outer_class_name =
@@ -1178,7 +1178,7 @@ void mark_java_implicitly_generic_class_type(
           outer_generic_type_parameters.begin(),
           outer_generic_type_parameters.end());
       }
-      outer_class_delimiter = outer_class_name.rfind("$");
+      outer_class_delimiter = outer_class_name.rfind('$');
     }
     else
     {

Original file line number	Diff line number	Diff line change
`@@ -1158,7 +1158,7 @@ void mark_java_implicitly_generic_class_type(`
`1158`	`1158`	`// the order from the outer-most inwards`
`1159`	`1159`	`std::vector<java_generic_parametert> implicit_generic_type_parameters;`
`1160`	`1160`	`std::string::size_type outer_class_delimiter =`
`1161`		`- qualified_class_name.rfind("$");`
	`1161`	`+ qualified_class_name.rfind('$');`
`1162`	`1162`	`while(outer_class_delimiter != std::string::npos)`
`1163`	`1163`	`{`
`1164`	`1164`	`std::string outer_class_name =`
`@@ -1178,7 +1178,7 @@ void mark_java_implicitly_generic_class_type(`
`1178`	`1178`	`outer_generic_type_parameters.begin(),`
`1179`	`1179`	`outer_generic_type_parameters.end());`
`1180`	`1180`	`}`
`1181`		`- outer_class_delimiter = outer_class_name.rfind("$");`
	`1181`	`+ outer_class_delimiter = outer_class_name.rfind('$');`
`1182`	`1182`	`}`
`1183`	`1183`	`else`
`1184`	`1184`	`{`