Skip to content

Commit f025c91

Browse files
committed
[FIXUP] Appease linter
1 parent d39d57d commit f025c91

File tree

7 files changed

+48
-32
lines changed

7 files changed

+48
-32
lines changed
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
ansi-c
2+
langapi
3+
goto-programs
Lines changed: 25 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
// Author: Fotis Koutoulakis for Diffblue Ltd.
2+
13
// Test file to try loading a GOTO-model into memory and running a sample verification run on it.
24
#include <util/exception_utils.h>
35

@@ -9,24 +11,27 @@
911

1012
int main(int argc, char *argv[])
1113
{
12-
try {
13-
std::cout << "Hello from API stub" << std::endl;
14-
15-
// Convert argv to vector of strings for initialize_goto_model
16-
std::vector<std::string> arguments(argv + 1, argv + argc);
17-
18-
// Create API options object, to pass to initialiser of API object.
19-
auto api_options = api_optionst::create().simplify(false);
20-
21-
// Initialise API dependencies and global configuration in one step.
22-
cprover_api api(api_options);
23-
24-
// Demonstrate the loading of a goto-model from the command line arguments
25-
api.load_model_from_files(arguments);
26-
27-
std::cout << "Successfully initialised goto_model" << std::endl;
28-
return 0;
29-
} catch (const invalid_command_line_argument_exceptiont &e) {
30-
std::cout << e.what() << std::endl;
31-
}
14+
try
15+
{
16+
std::cout << "Hello from API stub" << std::endl;
17+
18+
// Convert argv to vector of strings for initialize_goto_model
19+
std::vector<std::string> arguments(argv + 1, argv + argc);
20+
21+
// Create API options object, to pass to initialiser of API object.
22+
auto api_options = api_optionst::create().simplify(false);
23+
24+
// Initialise API dependencies and global configuration in one step.
25+
api_sessiont api(api_options);
26+
27+
// Demonstrate the loading of a goto-model from the command line arguments
28+
api.load_model_from_files(arguments);
29+
30+
std::cout << "Successfully initialised goto_model" << std::endl;
31+
return 0;
32+
}
33+
catch (const invalid_command_line_argument_exceptiont &e)
34+
{
35+
std::cout << e.what() << std::endl;
36+
}
3237
}

cprover-cpp-api/regression/model_loading/load_basic_c_file/test.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@
22

33
int main(int argc, char *argv[])
44
{
5-
int a[] = {0, 1, 2, 3, 4};
6-
assert(a[4] != 4);
5+
int a[] = {0, 1, 2, 3, 4};
6+
assert(a[4] != 4);
77
}

cprover-cpp-api/src/api.cpp

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
// Author: Fotis Koutoulakis for Diffblue Ltd.
2+
13
#include "api.h"
24

35
#include <util/cmdline.h>
@@ -12,12 +14,12 @@
1214
#include <langapi/mode.h>
1315

1416
#include <memory>
15-
#include <vector>
1617
#include <string>
18+
#include <vector>
1719

1820
extern configt config;
1921

20-
cprover_api::cprover_api()
22+
api_sessiont::api_sessiont()
2123
: message_handler(
2224
util_make_unique<null_message_handlert>(null_message_handlert{})),
2325
options(util_make_unique<optionst>(optionst{}))
@@ -30,7 +32,7 @@ cprover_api::cprover_api()
3032
register_language(new_ansi_c_language);
3133
}
3234

33-
cprover_api::cprover_api(const api_optionst &options)
35+
api_sessiont::api_sessiont(const api_optionst &options)
3436
: message_handler(
3537
util_make_unique<null_message_handlert>(null_message_handlert{})),
3638
options(options.to_engine_options())
@@ -43,9 +45,9 @@ cprover_api::cprover_api(const api_optionst &options)
4345
register_language(new_ansi_c_language);
4446
}
4547

46-
cprover_api::~cprover_api() = default;
48+
api_sessiont::~api_sessiont() = default;
4749

48-
void cprover_api::load_model_from_files(const std::vector<std::string> &files)
50+
void api_sessiont::load_model_from_files(const std::vector<std::string> &files)
4951
{
5052
model = util_make_unique<goto_modelt>(
5153
initialize_goto_model(files, *message_handler, *options));

cprover-cpp-api/src/api.h

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,11 @@
1+
// Author: Fotis Koutoulakis for Diffblue Ltd.
2+
13
#ifndef CPROVER_API_API_H
24
#define CPROVER_API_API_H
35

46
#include <memory>
5-
#include <vector>
67
#include <string>
8+
#include <vector>
79

810
// Forward declaration of API dependencies
911
class goto_modelt;
@@ -14,12 +16,12 @@ class optionst;
1416

1517
// An object in the pattern of Session Facade - owning all of the memory
1618
// the API is using and being responsible for the management of that.
17-
struct cprover_api
19+
struct api_sessiont
1820
{
1921
// Initialising constructor
20-
cprover_api();
21-
explicit cprover_api(const api_optionst &options);
22-
~cprover_api(); // default constructed in the .cpp file
22+
api_sessiont();
23+
explicit api_sessiont(const api_optionst &options);
24+
~api_sessiont(); // default constructed in the .cpp file
2325

2426
/// Load a goto_model from a given vector of filenames.
2527
/// \param files: A vector<string> containing the filenames to be loaded

cprover-cpp-api/src/options.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
// Author: Fotis Koutoulakis for Diffblue Ltd.
2+
13
#include "options.h"
24

35
#include <util/make_unique.h>

cprover-cpp-api/src/options.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
// Author: Fotis Koutoulakis for Diffblue Ltd.
2+
13
#ifndef CPROVER_API_OPTIONS_H
24
#define CPROVER_API_OPTIONS_H
35

0 commit comments

Comments
 (0)