File tree Expand file tree Collapse file tree 1 file changed +18
-0
lines changed Expand file tree Collapse file tree 1 file changed +18
-0
lines changed Original file line number Diff line number Diff line change
1
+ # The CPROVER C++ API
2
+
3
+ This folder includes the interface and the implementation of a new C++-based
4
+ API for the CProver libraries. The aim is for this to be able to be used by
5
+ clients to drive all of the verification pipeline without the need to invoke
6
+ any of the associated tools.
7
+
8
+ ## Implementation
9
+
10
+ The major part of the implementation of the API is in [ ` api.cpp ` ] ( api.cpp ) .
11
+ To use the API as it stands, you need to include the header [ ` api.h ` ] ( api.h )
12
+ in your program, and link against the resultant shared-object from the CProver
13
+ build process (` libcprover-api.a ` ).
14
+
15
+ ## Example
16
+
17
+ An example for driving the API in its current form is in the file [ ` call_bmc.cpp ` ] ( call_bmc.cpp ) ,
18
+ which we are also using as a binary driver for testing the API.
You can’t perform that action at this time.
0 commit comments