From e1f412092ff24c89a59191b6c7efd6209a7c9b42 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 23 Apr 2018 16:23:48 +0000 Subject: [PATCH] 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. --- regression/cbmc-java/virtual7/test.desc | 4 ++-- src/goto-programs/remove_virtual_functions.cpp | 11 ++++++++--- 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/regression/cbmc-java/virtual7/test.desc b/regression/cbmc-java/virtual7/test.desc index 7d23df44236..900469e7dcf 100644 --- a/regression/cbmc-java/virtual7/test.desc +++ b/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 diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index f3b53c57a9b..86e19e7de81 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/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; + } }); }