forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request diffblue#2074 from owen-jones-diffblue/owen-jones-…
…diffblue/lazy-methods-no-candidate-callees Deal with virtual function calls with no candidate targets
- Loading branch information
Showing
9 changed files
with
123 additions
and
84 deletions.
There are no files selected for viewing
Binary file added
BIN
+222 Bytes
regression/cbmc-java/lazyloading_no_candidates/Test$factory_intf.class
Binary file not shown.
Binary file not shown.
Binary file not shown.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
public class Test { | ||
|
||
interface factory_intf { | ||
public intf getintf(); | ||
} | ||
|
||
interface intf { | ||
public void f(); | ||
} | ||
|
||
public static void main(factory_intf i) { i.getintf().f(); } | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
CORE symex-driven-lazy-loading-expected-failure | ||
Test.class | ||
--lazy-methods --show-goto-functions --verbosity 10 --function Test.main | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^CI lazy methods: elaborate java::Test\$intf\.f:\(\)V$ | ||
Test\$intf\.f:\(\)V\(\);$ | ||
-- | ||
-- | ||
This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -20,7 +20,7 @@ Author: Chris Smowton, [email protected] | |
void ci_lazy_methods_neededt::add_needed_method( | ||
const irep_idt &method_symbol_name) | ||
{ | ||
callable_methods.push_back(method_symbol_name); | ||
callable_methods.insert(method_symbol_name); | ||
} | ||
|
||
/// Notes class `class_symbol_name` will be instantiated, or a static field | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -14,18 +14,19 @@ Author: Chris Smowton, [email protected] | |
|
||
#include <vector> | ||
#include <set> | ||
#include <unordered_set> | ||
#include <util/symbol_table.h> | ||
|
||
class ci_lazy_methods_neededt | ||
{ | ||
public: | ||
ci_lazy_methods_neededt( | ||
std::vector<irep_idt> &_callable_methods, | ||
std::set<irep_idt> &_instantiated_classes, | ||
symbol_tablet &_symbol_table): | ||
callable_methods(_callable_methods), | ||
instantiated_classes(_instantiated_classes), | ||
symbol_table(_symbol_table) | ||
std::unordered_set<irep_idt> &_callable_methods, | ||
std::unordered_set<irep_idt> &_instantiated_classes, | ||
symbol_tablet &_symbol_table) | ||
: callable_methods(_callable_methods), | ||
instantiated_classes(_instantiated_classes), | ||
symbol_table(_symbol_table) | ||
{} | ||
|
||
void add_needed_method(const irep_idt &); | ||
|
@@ -38,11 +39,11 @@ class ci_lazy_methods_neededt | |
// contain all methods that have previously been elaborated. | ||
// It should be changed to a set if we develop the need to use | ||
// it that way. | ||
std::vector<irep_idt> &callable_methods; | ||
std::unordered_set<irep_idt> &callable_methods; | ||
// instantiated_classes on the other hand is a true set of every class | ||
// found so far, so we can use a membership test to avoid | ||
// repeatedly exploring a class hierarchy. | ||
std::set<irep_idt> &instantiated_classes; | ||
std::unordered_set<irep_idt> &instantiated_classes; | ||
symbol_tablet &symbol_table; | ||
}; | ||
|
||
|