First iteration of C++ CBMC API #7274

NlightNFotis · 2022-10-27T13:25:53Z

This is the first iteration of a C++ CBMC API.

It includes:

A testing binary, called api-binary-driver, for use to validate this first iteration by exercising the API in the form of a regression test.
The API exposed as a C++ library, in src/libcprover-cpp, which is built and exposed as libcprover-api-cpp.a by CMake and CPack.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

thomasspriggs · 2022-10-31T11:17:59Z

Shouldn't this PR be setting up codeowners?

thomasspriggs · 2022-10-31T12:09:58Z

I currently get the following error when attempting to build locally -

CMake Error at cpp_api/CMakeLists.txt:3 (target_link_libraries):
  Cannot specify link libraries for target "bmc_api" which is not built by
  this project.

thomasspriggs · 2022-10-31T12:14:28Z

cpp_api/call_bmc.cpp

@@ -0,0 +1,40 @@
+// Test file to try loading a GOTO-model into memory and running a sample verification run on it.


Is there a reason we aren't using catch for this test?
Shouldn't tests be in a separate directory from the implementation?

There's no reason why we can't have unit tests, but for a first iteration I planned to use this as a binary driver for a regression test, which I thought might be easier.

It's important to think about testing from the start, both unit and regression tests, and rust integration tests.

cpp_api/api.h

thomasspriggs · 2022-10-31T15:46:33Z

cpp_api/api.h

+
+// A struct containing the API dependencies (some of them, at least)
+struct api_depst {
+    message_handlert *msg_handler;


We should define a new STL based type for message handling rather than exposing the implementation details of message_handlert. I am thinking along the lines of a new api_messaget and corresponding std::function<void(const api_messaget &)> message_handler.

cpp_api/api.h

NlightNFotis · 2022-11-01T14:46:35Z

@NlightNFotis We need to add a readme.md file explaining some of the rationale behind the choices made here.

peterschrammel · 2022-11-01T15:28:49Z

CMakeLists.txt

@@ -215,6 +216,8 @@ cprover_default_properties(
    cbmc
    cbmc-lib
    cpp
+    api_bin
+    bmc_api


_ does not follow the current naming convention for modules.
Suggestion: cprover-api

peterschrammel · 2022-11-01T15:29:45Z

cpp_api/api.cpp

+
+#include "api.h"
+
+api_depst api_deps;


I hope these are temporary. We definitely don't want to have globals. Also see below wrt sessions.

cpp_api/api.h

peterschrammel · 2022-11-01T15:34:08Z

cpp_api/call_bmc.cpp

@@ -0,0 +1,40 @@
+// Test file to try loading a GOTO-model into memory and running a sample verification run on it.


It's important to think about testing from the start, both unit and regression tests, and rust integration tests.

peterschrammel · 2022-11-01T15:42:41Z

cpp_api/api.cpp

+api_depst api_deps;
+extern configt config;
+
+void initialize() {


I remember that we discussed about introducing a session object to encapsulate all the memory owned by the library so that the client has control about the session/memory lifetime.

codecov · 2022-11-22T11:26:21Z

Codecov Report

Base: 78.35% // Head: 78.36% // Increases project coverage by +0.00% 🎉

Coverage data is based on head (f025c91) compared to base (ead3518).
Patch coverage: 75.00% of modified lines in pull request are covered.

❗ Current head f025c91 differs from pull request most recent head d0ab60c. Consider uploading reports for the commit d0ab60c to get more accurate results

Additional details and impacted files

@@            Coverage Diff            @@
##           develop    #7274    +/-   ##
=========================================
  Coverage    78.35%   78.36%            
=========================================
  Files         1645     1651     +6     
  Lines       190208   190009   -199     
=========================================
- Hits        149040   148896   -144     
+ Misses       41168    41113    -55

Impacted Files	Coverage Δ
cprover-cpp-api/src/api.cpp	`61.11% <61.11%> (ø)`
cprover-cpp-api/regression/call_bmc.cpp	`75.00% <75.00%> (ø)`
cprover-cpp-api/src/api.h	`100.00% <100.00%> (ø)`
cprover-cpp-api/src/options.cpp	`100.00% <100.00%> (ø)`
src/cpp/cpp_item.h	`64.15% <0.00%> (-7.55%)`	⬇️
...instrument/contracts/dynamic-frames/dfcc_utils.cpp	`90.38% <0.00%> (-5.39%)`	⬇️
src/cpp/cpp_typecheck_namespace.cpp	`53.48% <0.00%> (-3.96%)`	⬇️
src/goto-programs/goto_convert_exceptions.cpp	`51.78% <0.00%> (-1.67%)`	⬇️
src/cpp/cpp_typecheck_enum_type.cpp	`77.19% <0.00%> (-1.32%)`	⬇️
src/statement-list/statement_list_entry_point.cpp	`83.87% <0.00%> (-1.28%)`	⬇️
... and 181 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

peterschrammel · 2022-11-23T16:03:54Z

CMakeLists.txt

@@ -206,6 +206,7 @@ option(WITH_MEMORY_ANALYZER
 add_subdirectory(src)
 add_subdirectory(regression)
 add_subdirectory(unit)
+add_subdirectory(cpp_api)


cpp_api, cprover_api, cprover_api_cpp, cbmc_api, api-... The naming is very inconsistent. We need to settle on a single name that is used throughout. I'd say let's go with cprover-api-cpp.

The cpp_api is the directory name, which I've left for now because while I'm playing around with the rust part, I was thinking of renaming the folder into api/cpp and move the rust bit into api/rust.

I guess this also refers to the class name, which I can look into naming more appropriately.

thomasspriggs · 2022-11-23T17:42:03Z

cpp_api/api.cpp

+// 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()),


🚫 Unique pointers should be constructed via util_make_unique rather than directly using new like this.

thomasspriggs · 2022-11-23T17:46:35Z

cpp_api/api.h

+  // Initialising constructor
+  explicit cbmc_api();
+  cbmc_api(const api_optionst &options);
+  ~cbmc_api();


I suggest that we put a comment on this destructor in the header file, noting that it is defaulted in the .cpp file for compatibility with implementing the "pointer to implementation" pattern with unique_ptr. This saves checking the .cpp file to work this out, as the prospect of a hand-written destructor implementation can be concerning.

cpp_api/api.h

cpp_api/options.h

cpp_api/call_bmc.cpp

thomasspriggs · 2022-11-23T18:35:37Z

cpp_api/options.h

+
+class optionst;
+
+class api_optionst


At what stage does validation of the supplied options happen? The singular bool option defined now doesn't really need validating. But I foresee a need to report errors if options are specified which don't make sense in combination, or to report warnings if a deprecated option is used.

cpp_api/options.h

NlightNFotis · 2022-11-24T11:26:53Z

cpp_api/call_bmc.cpp

+        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);


Unique pointer to constant instance makes more sense.

regression/cprover-api-cpp/CMakeLists.txt

TGWDB

Looks ok (minor changes proposed, but nothing to block on).

TGWDB · 2022-11-30T11:13:54Z

cprover-cpp-api/readme.md

+This folder includes the interface and the implementation of a new C++-based
+API for the CProver libraries. The aim is for this to be able to be used by
+clients to drive all of the verification pipeline without the need to invoke
+any of the associated tools.


This [folder/directory] includes the interface and implementation of a C++-based API for the CProver libraries. This allows direct linking to key CProver functionality via C++ function calls. This (will eventually) allow the use of all aspects of the CProver verification pipeline via direct function calls and deprecate the need for invoking separate tools/programs.

TGWDB · 2022-11-30T11:17:10Z

cprover-cpp-api/src/api.cpp

+  // Initialise C language mode
+  register_language(new_ansi_c_language);


For a first implementation this is ok I think, but do we want to force/hard-code that the language is C?

This is indeed not ideal, but for a first implementation we need to have at least one language mode bootstrapped, and none other than C seem to fit in this particular scenario.

What I can do is potentially add a todo comment to make this configurable in the future.

TGWDB · 2022-11-30T11:19:21Z

cprover-cpp-api/src/options.cpp

+  return api_optionst{};
+}
+
+api_optionst &api_optionst::simplify(bool on)


on -> enable_simplify ?

TGWDB · 2022-11-30T11:51:05Z

CODEOWNERS

@@ -38,7 +38,7 @@
 /jbmc/src/java_bytecode/ @romainbrenguier @peterschrammel
 /src/analyses/ @martin-cs @peterschrammel @chris-ryder
 /src/pointer-analysis/ @martin-cs @peterschrammel @chris-ryder
-
+/cpp_api/ @diffblue/diffblue-opensource


Let's make this explicit with people rather than simply the team

thomasspriggs

I am still not sure I understand where we are planning to perform error checking on the options. Lets hypothetically say that we add the object-bits option to the API at some point in the future. This option is required to be positive and less than the number of bits configured for the pointer width. It is currently checked in the parse_object_bits_encoding function which is used by the command line entry points. How would the error state/string be communicated to users of the new API in the case where an invalid value was set for this option? Which of the new API functions will trigger the validation currently performed by parse_object_bits_encoding to be carried out?

thomasspriggs · 2022-11-24T11:56:30Z

cpp_api/options.h

+
+class optionst;
+
+class api_optionst


I suggest that we declare all classes (and structs) which are part of the API as final. If users of the API inherit from these classes then it could cause surprising maintenance issues later on. I think this has been prevented for this particular optionst class by making the constructor private. But marking the class as final would be more definitive.

thomasspriggs · 2022-11-24T12:02:04Z

cpp_api/api.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


🤔 Should the name of this object include the word "session" given that it was added it response to Peter's comment asking for a session object?

🤔 Maybe it would also make sense to use the letters "api" a little like a namespace. So this would become something like api_sessiont to match the naming of api_optionst. If the letters "api" are being used mainly to avoid naming clashes with things that are inside cbmc and excluded from the API, then I think it is confusing for them to be used as the end of some names and at the start of others.

thomasspriggs · 2022-11-24T12:21:42Z

cpp_api/api.h

+    std::unique_ptr<optionst> options;
+  };
+
+  std::unique_ptr<goto_modelt> model;


💡 We can actually reduce the number of internal classes which are forward declared in this file. We could have something like an api_session_implementationt struct and a single line std::unique_ptr<api_session_implementationt> implementation; in the header file, with the corresponding implementation of the class/struct in the .cpp for the api_sessiont class. The fields inside that class can then be values (or unique pointers) as we wish because the .cpp file includes the implementation headers. The advantage of this is are -

Improved compile times. Because the definition of the api_session_implementationt would be in the .cpp we can change what fields this contains and only recompile one file + relink, rather than having to recompile every file that includes the API header.

Reduced naming clashes. Forward declaring the message_handlert / optionst / goto_modelt means that users of the API don't need to include the headers defining these classes, but these names could still clash with the names of other unrelated classes of the same names in code bases consuming our api.

This comment is just an idea. So possibly something for a follow-up PR if we think it is worth-while.

A worthwhile idea, for sure, but given the in-flux nature of the API (given the rust work being concurrent, requiring changes to the C++ side to facilitate it) I would rather not make any significant structural changes to it right now - at least not until both the C++ side and the Rust side take more concrete form.

.gitignore

thomasspriggs · 2022-11-30T11:58:09Z

cprover-cpp-api/src/api.h

@@ -0,0 +1,36 @@
+#ifndef CPROVER_API_API_H
+#define CPROVER_API_API_H


I suggest moving these files into a src/libcprover/ sub directory -

api.h

api.cpp

options.h

options.cpp

Then the work on the rust side of the API could go in a separate src/cprover-rust/ directory.

Yes, this should all be inside /src

thomasspriggs · 2022-11-30T12:57:58Z

cprover-cpp-api/src/api.h

+  // Initialising constructor
+  cprover_api();
+  explicit cprover_api(const api_optionst &options);
+  ~cprover_api(); // default constructed in the .cpp file


This would read better to me if the word constructed were to be replaced with definition.

NlightNFotis · 2022-12-05T16:08:43Z

I am still not sure I understand where we are planning to perform error checking on the options. Lets hypothetically say that we add the object-bits option to the API at some point in the future. This option is required to be positive and less than the number of bits configured for the pointer width. It is currently checked in the parse_object_bits_encoding function which is used by the command line entry points. How would the error state/string be communicated to users of the new API in the case where an invalid value was set for this option? Which of the new API functions will trigger the validation currently performed by parse_object_bits_encoding to be carried out?

There's currently no designation for a particular function on the API options to do the error checking, but the vision is that there can be a new function called (for example) validate_options that goes through a dispatch table map<optiont, validation_funct> that has contains all of the options set by the user along with particular validation function they depend on, and have it being called.

With regards to communication of this, for now there's no such infrastructure (for simplicity's sake on this first iteration), but the way I picture it is demanding the validation_funct signature to return a Result<String> type, of either Ok or Error<String> type, containing a textual description of the particular error that occurred during validation. Any preexisting functions that don't conform to this interface could be adapted by a new function that dispatches to the preexisting function, translating any results back into a form that conforms to the new interface.

peterschrammel · 2022-12-05T17:06:40Z

CODEOWNERS

@@ -38,7 +38,7 @@
 /jbmc/src/java_bytecode/ @romainbrenguier @peterschrammel
 /src/analyses/ @martin-cs @peterschrammel @chris-ryder
 /src/pointer-analysis/ @martin-cs @peterschrammel @chris-ryder
-
+/cpp_api/ @NlightNFotis @thomasspriggs @esteffin @TGWDB @peterschrammel


Needs to match the actual name

danielsn · 2022-12-05T20:36:05Z

cprover-cpp-api/regression/CMakeLists.txt

@@ -0,0 +1,39 @@
+file(GLOB_RECURSE api_sources "../src/*.cpp" "../src/*.h")


Is this really the best way to find the files?

danielsn · 2022-12-05T20:37:05Z

cprover-cpp-api/regression/call_bmc.cpp

+    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);


Why hardcoded to false

This is a sample configuration option - this only set as false in the API binary driver that we use for testing.

This is to be initialised as needed by the users of the API.

(This is a single option for now, while we set up the scaffold for further work - we intend to expand this with way more options).

danielsn · 2022-12-05T20:37:40Z

cprover-cpp-api/regression/call_bmc.cpp

+    // 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.


What dependencies are being initialized here?

danielsn · 2022-12-05T20:38:40Z

cprover-cpp-api/regression/call_bmc.cpp

+    api_sessiont api(api_options);
+
+    // Demonstrate the loading of a goto-model from the command line arguments
+    api.load_model_from_files(arguments);


Can this fail? How are error conditions handled here?

Yes. As an example, if the filename passed doesn't exist it throws an exception.

danielsn · 2022-12-05T20:39:29Z

cprover-cpp-api/regression/call_bmc.cpp

+    // Demonstrate the loading of a goto-model from the command line arguments
+    api.load_model_from_files(arguments);
+
+    std::cout << "Successfully initialised goto_model" << std::endl;


Where do we actually call bmc? Looks like we load the model, but then I don't see BMC being called?

The actual call to the BMC will follow up later - I have some code for that but it had some wrinkles that I need to iron. Will probably come up as another PR.

danielsn · 2022-12-05T20:40:10Z

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

+int main(int argc, char *argv[])
+{
+  int a[] = {0, 1, 2, 3, 4};
+  assert(a[4] != 4);


This is expected to fail, correct?

It doesn't matter - we want to make sure a particular string (that shows up if everything works wrt model loading) is present in the output.

danielsn · 2022-12-05T20:40:56Z

cprover-cpp-api/src/api.cpp

+    options(util_make_unique<optionst>(optionst{}))
+{
+  // Needed to initialise the language options correctly
+  cmdlinet cmdline;


Is this the CBMC commandline? Doesn't that make a weird dependency?

Yes - hence why it's handled internally :)

danielsn · 2022-12-05T20:42:11Z

cprover-cpp-api/src/api.h

+#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.


When is this memory released? When the object drops?

Yes - this owns unique pointers to all of its dependencies, so as soon as the object gets out of scope all of the memory the object uses should be released.

danielsn · 2022-12-05T20:43:21Z

cprover-cpp-api/src/api.h

+  /// \param files: A vector<string> containing the filenames to be loaded
+  /// \param options: An options object, to be passed on to analysis or
+  /// transformation passes.
+  void load_model_from_files(const std::vector<std::string> &files);


If this fails, what happens? Throws an exception?

Yes - which bubbles up to the call stack.

The test driver we have is doing the exception handling at this point - we are in the process of researching how to best expose this to Rust.

This also adds a regression testing binary driver under `regression/libcprover-cpp/call_bmc.cpp`, for testing the API. The library being built is `lib/libcprover-api-cpp.a`.

tautschnig

I'm obviously too late to the party, but I'd please ask for some follow-up cleanup to happen.

tautschnig · 2022-12-07T21:25:38Z

CMakeLists.txt

@@ -215,6 +215,7 @@ cprover_default_properties(
    cbmc
    cbmc-lib
    cpp
+    cprover-api-cpp


Why does this not match the directory name?

tautschnig · 2022-12-07T21:26:20Z

regression/libcprover-cpp/CMakeLists.txt

+    # TODO: Should be fixed for the proper include form.
+    ${CMAKE_CURRENT_SOURCE_DIR}/../src/libcprover-cpp/)


Where is this tracked/when will it be fixed?

tautschnig · 2022-12-07T21:27:08Z

regression/libcprover-cpp/CMakeLists.txt

+macro(add_test_pl_profile name cmdline flag profile)
+    add_test(
+        NAME "${name}-${profile}"
+        COMMAND perl ${test_pl_path} -e -p -c "${cmdline}" ${flag} ${ARGN}
+        WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
+    )
+    set_tests_properties("${name}-${profile}" PROPERTIES
+        LABELS "${profile};CBMC"
+    )
+endmacro(add_test_pl_profile)


Why do you need a new one and cannot re-use the existing one?

tautschnig · 2022-12-07T21:27:58Z

regression/libcprover-cpp/CMakeLists.txt

+# For the best possible utilisation of multiple cores when
+# running tests in parallel, it is important that these directories are
+# listed with decreasing runtimes (i.e. longest running at the top)
+add_subdirectory(model_loading)


Will we actually get parallelisation within parallel runs here?

tautschnig · 2022-12-07T21:31:38Z

src/libcprover-cpp/api.cpp

+#include <string>
+#include <vector>
+
+extern configt config;


You are including config.h, this is redundant.

tautschnig · 2022-12-07T21:36:31Z

src/libcprover-cpp/api.h

+class optionst;
+
+#include "options.h"


One of these should be removed.

tautschnig · 2022-12-07T21:38:17Z

src/libcprover-cpp/api.h

+private:
+  std::unique_ptr<goto_modelt> model;
+  std::unique_ptr<message_handlert> message_handler;
+  std::unique_ptr<optionst> options;


I suggest you use PIMPL here: have a single pointer to the actual implementation, and completely hide internals like class message_handlert from the API header file.

tautschnig · 2022-12-07T21:40:37Z

src/libcprover-cpp/options.cpp

+// Author: Fotis Koutoulakis for Diffblue Ltd.
+
+#include "options.h"
+
+#include <util/make_unique.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;
+}
+
+std::unique_ptr<optionst> api_optionst::to_engine_options() const
+{
+  optionst engine_options;
+  engine_options.set_option("simplify", simplify_enabled);
+  return util_make_unique<optionst>(engine_options);
+}


Couldn't this file please be called api_options.h to avoid confusion?

tautschnig · 2022-12-07T21:41:25Z

src/libcprover-cpp/options.h

+  // Private interface methods
+  api_optionst() = default;


I'm not sure this comment is helpful?

tautschnig · 2022-12-07T21:42:24Z

src/libcprover-cpp/options.h

+public:
+  static api_optionst create();
+
+  api_optionst &simplify(bool on);
+
+  std::unique_ptr<optionst> to_engine_options() const;


These strictly need comments. This is supposed to be an API to be used, after all.

NlightNFotis · 2022-12-07T22:51:58Z

@tautschnig Hi Michael, I've made a note of all of your comments and I will raise a PR with them addressed as soon as I can.

NlightNFotis self-assigned this Oct 27, 2022

NlightNFotis force-pushed the kani_api_cpp branch from 428ea04 to 5f51ce6 Compare October 27, 2022 13:51

thomasspriggs reviewed Oct 31, 2022

View reviewed changes

peterschrammel reviewed Nov 1, 2022

View reviewed changes

feliperodri mentioned this pull request Nov 2, 2022

Proposal of Interface between Kani/CProver tools #7042

Closed

feliperodri added aws Kani labels Nov 8, 2022

NlightNFotis force-pushed the kani_api_cpp branch from f0ac9f0 to a1058d6 Compare November 21, 2022 17:24

NlightNFotis force-pushed the kani_api_cpp branch from ae6c9e2 to 21ddf34 Compare November 23, 2022 15:13

NlightNFotis marked this pull request as ready for review November 23, 2022 15:19

NlightNFotis requested review from a team, kroening, tautschnig and chris-ryder as code owners November 23, 2022 15:19

NlightNFotis changed the title ~~First draft of C++ CBMC API~~ First iteration of C++ CBMC API Nov 23, 2022

peterschrammel reviewed Nov 23, 2022

View reviewed changes

thomasspriggs reviewed Nov 23, 2022

View reviewed changes

cpp_api/api.h Outdated Show resolved Hide resolved

thomasspriggs reviewed Nov 23, 2022

View reviewed changes

cpp_api/options.h Outdated Show resolved Hide resolved

thomasspriggs reviewed Nov 23, 2022

View reviewed changes

cpp_api/call_bmc.cpp Outdated Show resolved Hide resolved

thomasspriggs reviewed Nov 23, 2022

View reviewed changes

NlightNFotis commented Nov 24, 2022

View reviewed changes

cpp_api/options.h Outdated Show resolved Hide resolved

NlightNFotis commented Nov 24, 2022

View reviewed changes

cpp_api/options.h Outdated Show resolved Hide resolved

NlightNFotis commented Nov 24, 2022

View reviewed changes

regression/cprover-api-cpp/CMakeLists.txt Outdated Show resolved Hide resolved

NlightNFotis force-pushed the kani_api_cpp branch 3 times, most recently from c2ab3ff to a888249 Compare November 29, 2022 14:49

TGWDB approved these changes Nov 30, 2022

View reviewed changes

TGWDB reviewed Nov 30, 2022

View reviewed changes

thomasspriggs reviewed Nov 30, 2022

View reviewed changes

NlightNFotis mentioned this pull request Dec 2, 2022

Expose CProver API version tag through to Rust API #7410

Merged

7 tasks

NlightNFotis force-pushed the kani_api_cpp branch from f025c91 to 16b5d7c Compare December 5, 2022 17:05

peterschrammel reviewed Dec 5, 2022

View reviewed changes

danielsn reviewed Dec 5, 2022

View reviewed changes

NlightNFotis force-pushed the kani_api_cpp branch 3 times, most recently from b1f3f83 to 1cbf707 Compare December 6, 2022 18:06

Add first version of a C++ API for CBMC.

d0ab60c

This also adds a regression testing binary driver under `regression/libcprover-cpp/call_bmc.cpp`, for testing the API. The library being built is `lib/libcprover-api-cpp.a`.

NlightNFotis force-pushed the kani_api_cpp branch from 1cbf707 to d0ab60c Compare December 6, 2022 18:12

peterschrammel approved these changes Dec 6, 2022

View reviewed changes

thomasspriggs approved these changes Dec 7, 2022

View reviewed changes

thomasspriggs merged commit f5525c6 into diffblue:develop Dec 7, 2022

NlightNFotis deleted the kani_api_cpp branch December 7, 2022 11:58

NlightNFotis restored the kani_api_cpp branch December 7, 2022 15:22

NlightNFotis deleted the kani_api_cpp branch December 7, 2022 15:23

tautschnig reviewed Dec 7, 2022

View reviewed changes

		@@ -0,0 +1,40 @@
		// Test file to try loading a GOTO-model into memory and running a sample verification run on it.

		// Initialise C language mode
		register_language(new_ansi_c_language);

		@@ -0,0 +1,36 @@
		#ifndef CPROVER_API_API_H
		#define CPROVER_API_API_H

		@@ -0,0 +1,39 @@
		file(GLOB_RECURSE api_sources "../src/.cpp" "../src/.h")

		# TODO: Should be fixed for the proper include form.
		${CMAKE_CURRENT_SOURCE_DIR}/../src/libcprover-cpp/)

First iteration of C++ CBMC API #7274

First iteration of C++ CBMC API #7274

Conversation

NlightNFotis commented Oct 27, 2022 • edited Loading

thomasspriggs commented Oct 31, 2022

thomasspriggs commented Oct 31, 2022

Choose a reason for hiding this comment

NlightNFotis Nov 1, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NlightNFotis commented Nov 1, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

codecov bot commented Nov 22, 2022 • edited Loading

Codecov Report

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

TGWDB left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thomasspriggs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NlightNFotis commented Dec 5, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NlightNFotis commented Dec 7, 2022

NlightNFotis commented Oct 27, 2022 •

edited

Loading

NlightNFotis Nov 1, 2022 •

edited

Loading

codecov bot commented Nov 22, 2022 •

edited

Loading