Make virtual function resolution independent of string table entry ordering

The program generated by virtual-function removal depended on where 'B', 'C',
'D', 'E' appear in the string table as there are multiple semantically
equivalent resolutions of virtual functions.

Author: tautschnig

regression/cbmc-java/virtual7/test.desc

@@ -3,6 +3,6 @@ test.class
 --show-goto-functions --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
-IF.*"java::C".*THEN GOTO
-IF.*"java::D".*THEN GOTO
+IF.*"java::B".*THEN GOTO
+IF.*"java::E".*THEN GOTO
 IF.*"java::A".*THEN GOTO

src/goto-programs/remove_virtual_functions.cpp

@@ -445,10 +445,15 @@ void remove_virtual_functionst::get_functions(
         has_prefix(
           id2string(b.symbol_expr.get_identifier()), "java::java.lang.Object"))
         return true;
-      else if(a.symbol_expr.get_identifier() == b.symbol_expr.get_identifier())
-        return a.class_id < b.class_id;
       else
-        return a.symbol_expr.get_identifier() < b.symbol_expr.get_identifier();
+      {
+        int cmp = a.symbol_expr.get_identifier().compare(
+          b.symbol_expr.get_identifier());
+        if(cmp == 0)
+          return a.class_id < b.class_id;
+        else
+          return cmp < 0;
+      }
     });
 }