First version of new binary being added.

Author: NlightNFotis

CMakeLists.txt

@@ -206,6 +206,7 @@ option(WITH_MEMORY_ANALYZER
 add_subdirectory(src)
 add_subdirectory(regression)
 add_subdirectory(unit)
+add_subdirectory(cpp_api)
 
 cprover_default_properties(
     analyses
@@ -215,6 +216,7 @@ cprover_default_properties(
     cbmc
     cbmc-lib
     cpp
+    bmc_api
     cprover
     cprover-lib
     crangler

cpp_api/CMakeLists.txt

@@ -0,0 +1,5 @@
+
+
+add_executable(bmc_api call_bmc.cpp)
+
+target_link_libraries(bmc_api goto-programs util langapi ansi-c)

cpp_api/call_bmc.cpp

@@ -0,0 +1,53 @@
+// Test file to try loading a GOTO-model into memory and running a sample verification run on it.
+#include <iostream>
+#include <vector>
+
+#include <ansi-c/ansi_c_language.h>
+
+#include <langapi/mode.h>
+
+#include <goto-programs/goto_model.h>
+#include <goto-programs/initialize_goto_model.h>
+
+#include <util/config.h>
+#include <util/cmdline.h>
+#include <util/message.h>
+#include <util/options.h>
+
+int main(int argc, char *argv[])
+{
+    try {
+        std::cout << "Hello from API stub" << std::endl;
+
+        // Convert argv to vector of strings for initialize_goto_model
+        std::vector<std::string> arguments(argv + 1, argv + argc);
+
+        // Initialise a null-message handler (we don't print anything yet)
+        null_message_handlert null_msg_hnd;
+        // Default options
+        optionst opts;
+        // 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);
+
+        std::cout << "[DEBUG] arguments is ";
+        for (auto opt : arguments) {
+            std::cout << "   [] " << opt << std::endl;
+        }
+
+        // Assume that argv[] is a list of files passed
+        goto_modelt model = initialize_goto_model(arguments, null_msg_hnd, opts);
+
+        std::cout << "Successfully initialised goto_model" << std::endl;
+        return 0;
+    } catch (invalid_command_line_argument_exceptiont e) {
+        std::cout << e.what() << std::endl;
+    }
+}
+
+