Skip to content

Commit 6850b84

Browse files
committed
Refactor API class to follow Session Facade pattern and own the memory of the API
1 parent c8f3442 commit 6850b84

File tree

3 files changed

+69
-56
lines changed

3 files changed

+69
-56
lines changed

cpp_api/api.cpp

Lines changed: 33 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -1,36 +1,46 @@
1-
#include <ansi-c/ansi_c_language.h>
1+
#include "api.h"
2+
3+
#include <util/cmdline.h>
4+
#include <util/config.h>
5+
#include <util/message.h>
6+
#include <util/options.h>
27

38
#include <goto-programs/goto_model.h>
49
#include <goto-programs/initialize_goto_model.h>
510

11+
#include <ansi-c/ansi_c_language.h>
612
#include <langapi/mode.h>
713

8-
#include <util/cmdline.h>
9-
#include <util/message.h>
10-
#include <util/options.h>
11-
12-
#include "api.h"
14+
#include <memory>
1315

14-
api_depst api_deps;
1516
extern configt config;
1617

17-
void initialize() {
18-
// Initialise a null-message handler (we don't print anything in the API)
19-
api_deps.msg_handler = new null_message_handlert();
20-
// Initialise default options
21-
api_deps.opts = new optionst();
22-
// Needed to initialise the language options correctly
23-
cmdlinet cmdline;
24-
// config is global in config.cpp
25-
config.set(cmdline);
26-
// Initialise C language mode
27-
register_language(new_ansi_c_language);
18+
// Default initialise the api_dependencies object
19+
cbmc_api::api_dependenciest::api_dependenciest()
20+
: // We don't print anything to the console as part of the API
21+
message_handler(new null_message_handlert()),
22+
// We create a default options object which we are going to
23+
// customise later.
24+
options(new optionst())
25+
{
2826
}
2927

30-
goto_modelt load_model_from_files(
31-
const std::vector<std::string> &files,
32-
const optionst &options)
28+
cbmc_api::api_dependenciest::~api_dependenciest() = default;
29+
30+
cbmc_api::cbmc_api() : dependencies(new api_dependenciest())
31+
{
32+
// Needed to initialise the language options correctly
33+
cmdlinet cmdline;
34+
// config is global in config.cpp
35+
config.set(cmdline);
36+
// Initialise C language mode
37+
register_language(new_ansi_c_language);
38+
}
39+
40+
cbmc_api::~cbmc_api() = default;
41+
42+
void cbmc_api::load_model_from_files(const std::vector<std::string> &files)
3343
{
34-
// This could be nested inside a try/catch, but for now let's leave it alone.
35-
return initialize_goto_model(files, *api_deps.msg_handler, options);
44+
model = util_make_unique<goto_modelt>(initialize_goto_model(
45+
files, *dependencies->message_handler, *dependencies->options));
3646
}

cpp_api/api.h

Lines changed: 31 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,37 @@
1+
#include <memory>
12
#include <vector>
23

3-
#include <goto-programs/goto_model.h>
4+
// Forward declaration of API dependencies
5+
class goto_modelt;
6+
class message_handlert;
7+
class optionst;
48

5-
#include <util/message.h>
6-
#include <util/options.h>
7-
#include <util/config.h>
89

9-
// A struct containing the API dependencies (some of them, at least)
10-
struct api_depst {
11-
message_handlert *msg_handler;
12-
optionst *opts;
13-
};
10+
// An object in the pattern of Session Facade - owning all of the memory
11+
// the API is using and being responsible for the management of that.
12+
struct cbmc_api
13+
{
14+
// Initialising constructor
15+
explicit cbmc_api();
16+
~cbmc_api();
1417

15-
/// Initialise API dependencies
16-
void initialize();
18+
/// Load a goto_model from a given vector of filenames.
19+
/// \param files: A vector<string> containing the filenames to be loaded
20+
/// \param options: An options object, to be passed on to analysis or
21+
/// transformation passes.
22+
void load_model_from_files(const std::vector<std::string> &files);
1723

18-
/// Load a goto_model from a given vector of filenames.
19-
/// \param files: A vector<string> containing the filenames to be loaded
20-
/// \param options: An options object, to be passed on to analysis or transformation
21-
/// passes.
22-
goto_modelt load_model_from_files(
23-
const std::vector<std::string> &files,
24-
const optionst &options);
24+
private:
25+
// A struct containing the API dependencies (some of them, at least)
26+
struct api_dependenciest
27+
{
28+
api_dependenciest();
29+
~api_dependenciest();
30+
31+
std::unique_ptr<message_handlert> message_handler;
32+
std::unique_ptr<optionst> options;
33+
};
34+
35+
std::unique_ptr<goto_modelt> model;
36+
std::unique_ptr<api_dependenciest> dependencies;
37+
};

cpp_api/call_bmc.cpp

Lines changed: 5 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -2,21 +2,10 @@
22
#include <iostream>
33
#include <vector>
44

5-
#include <ansi-c/ansi_c_language.h>
6-
7-
#include <langapi/mode.h>
8-
9-
#include <goto-programs/goto_model.h>
10-
#include <goto-programs/initialize_goto_model.h>
11-
12-
#include <util/config.h>
13-
#include <util/cmdline.h>
14-
#include <util/message.h>
5+
#include <util/exception_utils.h>
156

167
#include "api.h"
178

18-
extern api_depst api_deps;
19-
209
int main(int argc, char *argv[])
2110
{
2211
try {
@@ -26,13 +15,14 @@ int main(int argc, char *argv[])
2615
std::vector<std::string> arguments(argv + 1, argv + argc);
2716

2817
// Initialise API dependencies and global configuration in one step.
29-
initialize();
18+
cbmc_api api;
3019

31-
auto model = load_model_from_files(arguments, *api_deps.opts);
20+
// Demonstrate the loading of a goto-model from the command line arguments
21+
api.load_model_from_files(arguments);
3222

3323
std::cout << "Successfully initialised goto_model" << std::endl;
3424
return 0;
35-
} catch (invalid_command_line_argument_exceptiont e) {
25+
} catch (const invalid_command_line_argument_exceptiont &e) {
3626
std::cout << e.what() << std::endl;
3727
}
3828
}

0 commit comments

Comments
 (0)