Skip to content

Commit ada16d5

Browse files
committed
Move to a folder format close to the one used by JBMC
1 parent eb74c6c commit ada16d5

File tree

11 files changed

+29
-12
lines changed

11 files changed

+29
-12
lines changed

cpp_api/CMakeLists.txt

Lines changed: 0 additions & 9 deletions
This file was deleted.

cprover-cpp-api/CMakeLists.txt

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
add_subdirectory(regression)
2+
add_subdirectory(src)
3+
add_subdirectory(unit)
4+
5+
install(TARGETS cprover-api RUNTIME DESTINATION lib)

cpp_api/readme.md renamed to cprover-cpp-api/readme.md

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,12 +7,12 @@ any of the associated tools.
77

88
## Implementation
99

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)
10+
The major part of the implementation of the API is in [`api.cpp`](src/api.cpp).
11+
To use the API as it stands, you need to include the header [`api.h`](src/api.h)
1212
in your program, and link against the resultant shared-object from the CProver
1313
build process (`libcprover-api.a`).
1414

1515
## Example
1616

17-
An example for driving the API in its current form is in the file [`call_bmc.cpp`](call_bmc.cpp),
17+
An example for driving the API in its current form is in the file [`call_bmc.cpp`](regression/call_bmc.cpp),
1818
which we are also using as a binary driver for testing the API.
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
file(GLOB_RECURSE api_sources "../src/*.cpp" "../src/*.h")
2+
3+
# This step builds a binary driving the API (to be used for testing)
4+
add_executable(api-binary-driver call_bmc.cpp ${api_sources})
5+
target_include_directories(api-binary-driver
6+
PUBLIC
7+
${CBMC_BINARY_DIR}
8+
${CBMC_SOURCE_DIR}
9+
# TODO: Should be fixed for the proper include form.
10+
${CMAKE_CURRENT_SOURCE_DIR}/../src)
11+
target_link_libraries(api-binary-driver goto-programs util langapi ansi-c)
12+
File renamed without changes.

cprover-cpp-api/src/CMakeLists.txt

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
file(GLOB_RECURSE sources "*.cpp" "*.h")
2+
3+
# This step builds the API in the form of a statically linked library (libcprover-api.a)
4+
add_library(cprover-api ${sources})
5+
target_include_directories(cprover-api
6+
PUBLIC
7+
${CBMC_BINARY_DIR}
8+
${CBMC_SOURCE_DIR})
9+
target_link_libraries(cprover-api goto-programs util langapi ansi-c)
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.

cprover-cpp-api/unit/CMakeLists.txt

Whitespace-only changes.

0 commit comments

Comments
 (0)