Add libcprover unit test

Author: thomasspriggs

CMakeLists.txt

@@ -240,6 +240,7 @@ cprover_default_properties(
     json
     json-symtab-language
     langapi
+    lib-unit
     linking
     pointer-analysis
     solvers

unit/CMakeLists.txt

@@ -12,6 +12,7 @@ endif()
 file(GLOB_RECURSE sources "*.cpp" "*.h")
 
 file(GLOB_RECURSE testing_utils "testing-utils/*.cpp" "testing-utils/*.h")
+file(GLOB_RECURSE libcprover_sources "libcprover-cpp/*.cpp" "libcprover-cpp/*.h")
 
 if(NOT WITH_MEMORY_ANALYZER)
     file(GLOB_RECURSE memory_analyzer_sources "memory-analyzer/*.cpp")
@@ -62,9 +63,13 @@ list(REMOVE_ITEM sources
 
     # Intended to fail to compile
     ${CMAKE_CURRENT_SOURCE_DIR}/util/expr_cast/expr_undefined_casts.cpp
+
+    # Built into separate binary
+    ${libcprover_sources}
 )
 
 add_subdirectory(testing-utils)
+add_subdirectory(libcprover-cpp)
 
 add_executable(unit ${sources})
 target_include_directories(unit

unit/count_tests.py

@@ -56,6 +56,9 @@ def tests_in_file(file_path):
 def count_tests_in_directory(directory_path, exclude_files):
     test_count = 0
     for root, sub_directories, files in os.walk("."):
+        # Excluded from count as built into separate binary.
+        if root.endswith("libcprover-cpp"):
+            continue
         for file_name in files:
             if any(file_name == excluded_file for excluded_file in exclude_files):
                 continue

unit/libcprover-cpp/CMakeLists.txt

@@ -0,0 +1,19 @@
+
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+
+add_executable(lib-unit ${sources})
+target_include_directories(lib-unit
+    PUBLIC
+    ${CBMC_SOURCE_DIR}/libcprover-cpp
+)
+target_link_libraries(lib-unit
+    cprover-api-cpp
+)
+
+add_test(
+    NAME lib-unit
+    COMMAND $<TARGET_FILE:lib-unit>
+    WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+)
+
+set_tests_properties(lib-unit PROPERTIES LABELS "CORE;CBMC")

unit/libcprover-cpp/api.cpp

@@ -0,0 +1,88 @@
+// Author: Diffblue Ltd.
+
+// Note that this test should not include any headers which are internal to
+// cbmc. API headers (and STL/catch) should be included only. This is in order
+// to confirm that the API can be used without reference to cmbc internals.
+
+#include <libcprover-cpp/api.h>
+
+#include <algorithm>
+#include <sstream>
+#include <string>
+#include <vector>
+
+#include "../catch/catch.hpp"
+
+class contains_in_ordert final
+  : public Catch::MatcherBase<std::vector<std::string>>
+{
+public:
+  contains_in_ordert(std::initializer_list<std::string> expected);
+  bool match(const std::vector<std::string> &actual) const override;
+
+protected:
+  std::string describe() const override;
+
+private:
+  std::vector<std::string> expected;
+};
+
+contains_in_ordert::contains_in_ordert(
+  std::initializer_list<std::string> expected)
+  : expected{
+      std::make_move_iterator(expected.begin()),
+      std::make_move_iterator(expected.end())}
+{
+}
+
+bool contains_in_ordert::match(const std::vector<std::string> &actual) const
+{
+  auto begin_search = actual.begin();
+  for(const auto &expected_item : expected)
+  {
+    auto find_result = std::find(begin_search, actual.end(), expected_item);
+    if(find_result == actual.end())
+      return false;
+    else
+      begin_search = ++find_result;
+  }
+  return true;
+}
+
+std::string contains_in_ordert::describe() const
+{
+  std::stringstream description;
+  description << "contains these strings in order ";
+  description << '"' << *expected.begin() << '"';
+  for(auto iterator = std::next(expected.begin()); iterator != expected.end();
+      ++iterator)
+  {
+    description << ", \"" << *iterator << '"';
+  }
+  return description.str();
+}
+
+TEST_CASE("Test loading model from file.", "[core][libcprover-cpp]")
+{
+  api_sessiont api(api_optionst::create());
+
+  std::vector<std::string> output;
+  // This lambda needs to be non-capturing in order for it to be convertible
+  // to a function pointer, to pass to the API.
+  const auto write_output =
+    [](const api_messaget &message, api_call_back_contextt context) {
+      std::vector<std::string> &output =
+        *static_cast<std::vector<std::string> *>(context);
+      output.emplace_back(api_message_get_string(message));
+    };
+
+  api.set_message_callback(write_output, &output);
+  api.load_model_from_files({"test.c"});
+  CHECK_THAT(
+    output,
+    (contains_in_ordert{
+      "Parsing test.c",
+      "Converting",
+      "Type-checking test",
+      "Generating GOTO Program"}));
+}

unit/libcprover-cpp/lib_unit_tests.cpp

@@ -0,0 +1,4 @@
+// Author: Diffblue Ltd.
+
+#define CATCH_CONFIG_MAIN
+#include "../catch/catch.hpp"

unit/libcprover-cpp/module_dependencies.txt

@@ -0,0 +1,2 @@
+../catch
+libcprover-cpp

unit/libcprover-cpp/test.c

@@ -0,0 +1,9 @@
+// Input file to test reading through API, not for compiling!
+
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  int a[] = {0, 1, 2, 3, 4};
+  assert(a[4] != 4);
+}