Skip to content

Commit 760d1ca

Browse files
committed
Lazy goto model: implement abstract_goto_modelt
This enables it to be used interchangeably with goto_modelt, with the first user being bmct (specificially the symex-and-solve process)
1 parent a4f5d77 commit 760d1ca

File tree

1 file changed

+28
-17
lines changed

1 file changed

+28
-17
lines changed

src/goto-programs/lazy_goto_model.h

Lines changed: 28 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -8,31 +8,20 @@
88

99
#include <langapi/language_file.h>
1010

11+
#include "abstract_goto_model.h"
1112
#include "goto_model.h"
1213
#include "lazy_goto_functions_map.h"
1314
#include "goto_convert_functions.h"
1415

1516
class cmdlinet;
1617
class optionst;
1718

18-
/// Interface for a provider of function definitions to report whether or not it
19-
/// can provide a definition (function body) for a given function ID.
20-
struct can_produce_functiont
21-
{
22-
/// Determines if this function provider can produce a body for the given
23-
/// function
24-
/// \param id: function ID to query
25-
/// \return true if we can produce a function body, or false if we would leave
26-
/// it a bodyless stub.
27-
virtual bool can_produce_function(const irep_idt &id) const = 0;
28-
};
29-
3019
/// Model that holds partially loaded map of functions
31-
class lazy_goto_modelt : public can_produce_functiont
20+
class lazy_goto_modelt : public abstract_goto_modelt
3221
{
3322
public:
3423
typedef std::function<
35-
void(goto_model_functiont &function, const can_produce_functiont &)>
24+
void(goto_model_functiont &function, const abstract_goto_modelt &)>
3625
post_process_functiont;
3726
typedef std::function<bool(goto_modelt &goto_model)> post_process_functionst;
3827

@@ -65,8 +54,8 @@ class lazy_goto_modelt : public can_produce_functiont
6554
{
6655
return lazy_goto_modelt(
6756
[&handler, &options]
68-
(goto_model_functiont &fun, const can_produce_functiont &cpf) { // NOLINT(*)
69-
handler.process_goto_function(fun, cpf, options);
57+
(goto_model_functiont &fun, const abstract_goto_modelt &model) { // NOLINT(*)
58+
handler.process_goto_function(fun, model, options);
7059
},
7160
[&handler, &options] (goto_modelt &goto_model) -> bool { // NOLINT(*)
7261
return handler.process_goto_functions(goto_model, options);
@@ -100,7 +89,29 @@ class lazy_goto_modelt : public can_produce_functiont
10089
return std::move(model.goto_model);
10190
}
10291

103-
virtual bool can_produce_function(const irep_idt &id) const;
92+
// Implement the abstract_goto_modelt interface:
93+
94+
/// Accessor to retrieve the internal goto_functionst.
95+
/// Use with care; concurrent use of get_goto_function will have side-effects
96+
/// on this map which may surprise users, including invalidating any iterators
97+
/// they have stored.
98+
const goto_functionst &get_goto_functions() const override
99+
{
100+
return goto_model->goto_functions;
101+
}
102+
103+
const symbol_tablet &get_symbol_table() const override
104+
{
105+
return symbol_table;
106+
}
107+
108+
bool can_produce_function(const irep_idt &id) const override;
109+
110+
const goto_functionst::goto_functiont &get_goto_function(const irep_idt &id)
111+
override
112+
{
113+
return goto_functions.at(id);
114+
}
104115

105116
private:
106117
std::unique_ptr<goto_modelt> goto_model;

0 commit comments

Comments
 (0)