Add an options object for the API

Author: NlightNFotis

cpp_api/CMakeLists.txt

@@ -1,9 +1,9 @@
 # This step builds a binary driving the API (to be used for testing)
-add_executable(api-binary-driver call_bmc.cpp api.cpp)
+add_executable(api-binary-driver call_bmc.cpp api.cpp options.cpp)
 target_link_libraries(api-binary-driver goto-programs util langapi ansi-c)
 
 # This step builds the API in the form of a statically linked library (libcprover-api.a)
-add_library(cprover-api api.cpp)
+add_library(cprover-api api.cpp options.cpp)
 target_link_libraries(cprover-api goto-programs util langapi ansi-c)
 
 install(TARGETS cprover-api RUNTIME DESTINATION lib)

cpp_api/api.cpp

@@ -12,6 +12,7 @@
 #include <langapi/mode.h>
 
 #include <memory>
+#include <options.h>
 
 extern configt config;
 
@@ -25,6 +26,13 @@ cbmc_api::api_dependenciest::api_dependenciest()
 {
 }
 
+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())
@@ -37,6 +45,17 @@ 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()))
+{
+  // Needed to initialise the language options correctly
+  cmdlinet cmdline;
+  // config is global in config.cpp
+  config.set(cmdline);
+  // Initialise C language mode
+  register_language(new_ansi_c_language);
+}
+
 cbmc_api::~cbmc_api() = default;
 
 void cbmc_api::load_model_from_files(const std::vector<std::string> &files)

cpp_api/api.h

@@ -6,13 +6,15 @@ class goto_modelt;
 class message_handlert;
 class optionst;
 
+#include "options.h"
 
 // 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
 {
   // Initialising constructor
   explicit cbmc_api();
+  cbmc_api(const api_optionst &options);
   ~cbmc_api();
 
   /// Load a goto_model from a given vector of filenames.
@@ -25,7 +27,8 @@ struct cbmc_api
   // A struct containing the API dependencies (some of them, at least)
   struct api_dependenciest
   {
-    api_dependenciest();
+    explicit api_dependenciest();
+    api_dependenciest(const optionst options);
     ~api_dependenciest();
 
     std::unique_ptr<message_handlert> message_handler;

cpp_api/call_bmc.cpp

@@ -1,10 +1,11 @@
 // Test file to try loading a GOTO-model into memory and running a sample verification run on it.
-#include <iostream>
-#include <vector>
-
 #include <util/exception_utils.h>
 
 #include "api.h"
+#include "options.h"
+
+#include <iostream>
+#include <vector>
 
 int main(int argc, char *argv[])
 {
@@ -14,8 +15,11 @@ int main(int argc, char *argv[])
         // Convert argv to vector of strings for initialize_goto_model
         std::vector<std::string> arguments(argv + 1, argv + argc);
 
+        // Create API options object, to pass to initialiser of API object.
+        auto api_options = api_optionst::create().simplify(false);
+
         // Initialise API dependencies and global configuration in one step.
-        cbmc_api api;
+        cbmc_api api(api_options);
 
         // Demonstrate the loading of a goto-model from the command line arguments
         api.load_model_from_files(arguments);

cpp_api/options.cpp

@@ -0,0 +1,21 @@
+#include "options.h"
+
+#include <util/options.h>
+
+api_optionst api_optionst::create()
+{
+  return api_optionst{};
+}
+
+api_optionst &api_optionst::simplify(bool on)
+{
+  simplify_enabled = on;
+  return *this;
+}
+
+optionst api_optionst::to_engine_options() const
+{
+  optionst engine_options;
+  engine_options.set_option("simplify", simplify_enabled);
+  return engine_options;
+}

cpp_api/options.h

@@ -0,0 +1,20 @@
+#pragma once
+
+class optionst;
+
+class api_optionst
+{
+  // Options for the verification engine
+  bool simplify_enabled;
+
+  // Private interface methods
+  api_optionst() = default;
+
+public:
+  ~api_optionst() = default;
+  static api_optionst create();
+
+  api_optionst &simplify(bool on);
+
+  optionst to_engine_options() const;
+};