Add a regression test exercising the API binary driver and its model loading capacity

Author: NlightNFotis

regression/CMakeLists.txt

@@ -37,6 +37,7 @@ add_subdirectory(cbmc-concurrency)
 add_subdirectory(cbmc-cover)
 add_subdirectory(cbmc-incr-oneloop)
 add_subdirectory(cbmc-incr-smt2)
+add_subdirectory(cprover-api-cpp)
 add_subdirectory(cbmc-incr)
 add_subdirectory(cbmc-output-file)
 add_subdirectory(cbmc-with-incr)

regression/cprover-api-cpp/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:api-binary-driver>"
+)

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

@@ -0,0 +1,7 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+    int a[] = {0, 1, 2, 3, 4};
+    assert(a[4] != 4);
+}

regression/cprover-api-cpp/model_loading/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.c
+
+^EXIT=0$
+^SIGNAL=0$
+Successfully initialised goto_model
+--
+--