Address majority of second round review comments

Author: NlightNFotis

cpp_api/api.cpp

@@ -16,26 +16,10 @@
 
 extern configt config;
 
-// Default initialise the api_dependencies object
-cbmc_api::api_dependenciest::api_dependenciest()
-  : // We don't print anything to the console as part of the API
-    message_handler(new null_message_handlert()),
-    // We create a default options object which we are going to
-    // customise later.
-    options(new optionst())
-{
-}
-
-cbmc_api::api_dependenciest::api_dependenciest(const optionst options)
-  : // We don't print anything to the console as part of the API
-    message_handler(new null_message_handlert()),
-    options(util_make_unique<optionst>(options))
-{
-}
-
-cbmc_api::api_dependenciest::~api_dependenciest() = default;
-
-cbmc_api::cbmc_api() : dependencies(new api_dependenciest())
+cprover_api::cprover_api()
+  : message_handler(
+      util_make_unique<null_message_handlert>(null_message_handlert{})),
+    options(util_make_unique<optionst>(optionst{}))
 {
   // Needed to initialise the language options correctly
   cmdlinet cmdline;
@@ -45,8 +29,10 @@ cbmc_api::cbmc_api() : dependencies(new api_dependenciest())
   register_language(new_ansi_c_language);
 }
 
-cbmc_api::cbmc_api(const api_optionst &options)
-  : dependencies(new api_dependenciest(options.to_engine_options()))
+cprover_api::cprover_api(const api_optionst &options)
+  : message_handler(
+      util_make_unique<null_message_handlert>(null_message_handlert{})),
+    options(options.to_engine_options())
 {
   // Needed to initialise the language options correctly
   cmdlinet cmdline;
@@ -56,10 +42,10 @@ cbmc_api::cbmc_api(const api_optionst &options)
   register_language(new_ansi_c_language);
 }
 
-cbmc_api::~cbmc_api() = default;
+cprover_api::~cprover_api() = default;
 
-void cbmc_api::load_model_from_files(const std::vector<std::string> &files)
+void cprover_api::load_model_from_files(const std::vector<std::string> &files)
 {
-  model = util_make_unique<goto_modelt>(initialize_goto_model(
-    files, *dependencies->message_handler, *dependencies->options));
+  model = util_make_unique<goto_modelt>(
+    initialize_goto_model(files, *message_handler, *options));
 }

cpp_api/api.h

@@ -1,3 +1,6 @@
+#ifndef CPROVER_API_API_H
+#define CPROVER_API_API_H
+
 #include <memory>
 #include <vector>
 
@@ -10,12 +13,12 @@ class optionst;
 
 // An object in the pattern of Session Facade - owning all of the memory
 // the API is using and being responsible for the management of that.
-struct cbmc_api
+struct cprover_api
 {
   // Initialising constructor
-  explicit cbmc_api();
-  cbmc_api(const api_optionst &options);
-  ~cbmc_api();
+  cprover_api();
+  explicit cprover_api(const api_optionst &options);
+  ~cprover_api(); // default constructed in the .cpp file
 
   /// Load a goto_model from a given vector of filenames.
   /// \param files: A vector<string> containing the filenames to be loaded
@@ -24,17 +27,9 @@ struct cbmc_api
   void load_model_from_files(const std::vector<std::string> &files);
 
 private:
-  // A struct containing the API dependencies (some of them, at least)
-  struct api_dependenciest
-  {
-    explicit api_dependenciest();
-    api_dependenciest(const optionst options);
-    ~api_dependenciest();
-  
-    std::unique_ptr<message_handlert> message_handler;
-    std::unique_ptr<optionst> options;
-  };
-  
   std::unique_ptr<goto_modelt> model;
-  std::unique_ptr<api_dependenciest> dependencies;
+  std::unique_ptr<message_handlert> message_handler;
+  std::unique_ptr<optionst> options;
 };
+
+#endif

cpp_api/call_bmc.cpp

@@ -19,7 +19,7 @@ int main(int argc, char *argv[])
         auto api_options = api_optionst::create().simplify(false);
 
         // Initialise API dependencies and global configuration in one step.
-        cbmc_api api(api_options);
+        cprover_api api(api_options);
 
         // Demonstrate the loading of a goto-model from the command line arguments
         api.load_model_from_files(arguments);
@@ -30,5 +30,3 @@ int main(int argc, char *argv[])
         std::cout << e.what() << std::endl;
     }
 }
-
-

cpp_api/options.cpp

@@ -1,5 +1,6 @@
 #include "options.h"
 
+#include <util/make_unique.h>
 #include <util/options.h>
 
 api_optionst api_optionst::create()
@@ -13,9 +14,9 @@ api_optionst &api_optionst::simplify(bool on)
   return *this;
 }
 
-optionst api_optionst::to_engine_options() const
+std::unique_ptr<optionst> api_optionst::to_engine_options() const
 {
   optionst engine_options;
   engine_options.set_option("simplify", simplify_enabled);
-  return engine_options;
+  return util_make_unique<optionst>(engine_options);
 }

cpp_api/options.h

@@ -1,4 +1,7 @@
-#pragma once
+#ifndef CPROVER_API_OPTIONS_H
+#define CPROVER_API_OPTIONS_H
+
+#include <memory>
 
 class optionst;
 
@@ -11,10 +14,11 @@ class api_optionst
   api_optionst() = default;
 
 public:
-  ~api_optionst() = default;
   static api_optionst create();
 
   api_optionst &simplify(bool on);
 
-  optionst to_engine_options() const;
+  std::unique_ptr<optionst> to_engine_options() const;
 };
+
+#endif