cprover
ci_lazy_methods_needed.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Context-insensitive lazy methods container
4
5Author: Chris Smowton, chris.smowton@diffblue.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H
13#define CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H
14
15#include <unordered_set>
16
17#include <util/irep.h>
18
19class namespacet;
20class pointer_typet;
22class symbol_tablet;
23class typet;
24
26{
27public:
29 std::unordered_set<irep_idt> &_callable_methods,
30 std::unordered_set<irep_idt> &_instantiated_classes,
31 const symbol_tablet &_symbol_table,
33 : callable_methods(_callable_methods),
34 instantiated_classes(_instantiated_classes),
35 symbol_table(_symbol_table),
37 {}
38
39 void add_needed_method(const irep_idt &);
40 // Returns true if new
41 bool add_needed_class(const irep_idt &);
42
44
45private:
46 // callable_methods is a vector because it's used as a work-list
47 // which is periodically cleared. It can't be relied upon to
48 // contain all methods that have previously been elaborated.
49 // It should be changed to a set if we develop the need to use
50 // it that way.
51 std::unordered_set<irep_idt> &callable_methods;
52 // instantiated_classes on the other hand is a true set of every class
53 // found so far, so we can use a membership test to avoid
54 // repeatedly exploring a class hierarchy.
55 std::unordered_set<irep_idt> &instantiated_classes;
57
59
60 void add_clinit_call(const irep_idt &class_id);
62
65 const namespacet &ns);
66
67 void gather_field_types(const typet &class_type, const namespacet &ns);
68};
69
70#endif
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
std::unordered_set< irep_idt > & instantiated_classes
void initialize_instantiated_classes_from_pointer(const pointer_typet &pointer_type, const namespacet &ns)
Build up list of methods for types for a specific pointer type.
const select_pointer_typet & pointer_type_selector
void gather_field_types(const typet &class_type, const namespacet &ns)
For a given type, gather all fields referenced by that type.
void add_needed_method(const irep_idt &)
Notes method_symbol_name is referenced from some reachable function, and should therefore be elaborat...
void add_all_needed_classes(const pointer_typet &pointer_type)
Add to the needed classes all classes specified, the replacement type if it will be replaced,...
std::unordered_set< irep_idt > & callable_methods
ci_lazy_methods_neededt(std::unordered_set< irep_idt > &_callable_methods, std::unordered_set< irep_idt > &_instantiated_classes, const symbol_tablet &_symbol_table, const select_pointer_typet &pointer_type_selector)
const symbol_tablet & symbol_table
bool add_needed_class(const irep_idt &)
Notes class class_symbol_name will be instantiated, or a static field belonging to it will be accesse...
void add_cprover_nondet_initialize_if_it_exists(const irep_idt &class_id)
For a given class id, if cproverNondetInitialize exists on it or any of its ancestors then note that ...
void add_clinit_call(const irep_idt &class_id)
For a given class id, note that its static initializer is needed.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
The symbol table.
Definition: symbol_table.h:14
The type of an expression, extends irept.
Definition: type.h:29