Skip to content

Commit f5525c6

Browse files
Merge pull request #7274 from NlightNFotis/kani_api_cpp
First iteration of C++ CBMC API
2 parents 97ffac6 + d0ab60c commit f5525c6

File tree

16 files changed

+268
-1
lines changed

16 files changed

+268
-1
lines changed

CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -215,6 +215,7 @@ cprover_default_properties(
215215
cbmc
216216
cbmc-lib
217217
cpp
218+
cprover-api-cpp
218219
cprover
219220
cprover-lib
220221
crangler

CODEOWNERS

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@
4444
/jbmc/src/java_bytecode/ @romainbrenguier @peterschrammel
4545
/src/analyses/ @martin-cs @peterschrammel @chris-ryder
4646
/src/pointer-analysis/ @martin-cs @peterschrammel @chris-ryder
47-
47+
/src/libcprover-cpp @NlightNFotis @thomasspriggs @esteffin @TGWDB @peterschrammel
4848

4949
# These files change frequently and changes are medium-risk
5050

regression/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,7 @@ add_subdirectory(goto-interpreter)
8585
add_subdirectory(cbmc-sequentialization)
8686
add_subdirectory(cpp-linter)
8787
add_subdirectory(catch-framework)
88+
add_subdirectory(libcprover-cpp)
8889

8990
if(WITH_MEMORY_ANALYZER)
9091
add_subdirectory(snapshot-harness)
Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
file(GLOB_RECURSE api_sources "../src/libcprover-cpp/*.cpp" "../src/libcprover-cpp/*.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+
cprover_default_properties(api-binary-driver)
6+
target_include_directories(api-binary-driver
7+
PUBLIC
8+
${CBMC_BINARY_DIR}
9+
${CBMC_SOURCE_DIR}
10+
# TODO: Should be fixed for the proper include form.
11+
${CMAKE_CURRENT_SOURCE_DIR}/../src/libcprover-cpp/)
12+
target_link_libraries(api-binary-driver goto-programs util langapi ansi-c cprover-api-cpp)
13+
14+
# Enable test running
15+
set(test_pl_path "${CBMC_SOURCE_DIR}/../regression/test.pl")
16+
17+
macro(add_test_pl_profile name cmdline flag profile)
18+
add_test(
19+
NAME "${name}-${profile}"
20+
COMMAND perl ${test_pl_path} -e -p -c "${cmdline}" ${flag} ${ARGN}
21+
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
22+
)
23+
set_tests_properties("${name}-${profile}" PROPERTIES
24+
LABELS "${profile};CBMC"
25+
)
26+
endmacro(add_test_pl_profile)
27+
28+
macro(add_test_pl_tests cmdline)
29+
get_filename_component(TEST_DIR_NAME ${CMAKE_CURRENT_SOURCE_DIR} NAME)
30+
message(STATUS "Adding tests in directory: ${TEST_DIR_NAME}")
31+
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -C CORE ${ARGN})
32+
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -T THOROUGH ${ARGN})
33+
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -F FUTURE ${ARGN})
34+
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG ${ARGN})
35+
endmacro(add_test_pl_tests)
36+
37+
# For the best possible utilisation of multiple cores when
38+
# running tests in parallel, it is important that these directories are
39+
# listed with decreasing runtimes (i.e. longest running at the top)
40+
add_subdirectory(model_loading)
Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
// Author: Fotis Koutoulakis for Diffblue Ltd.
2+
3+
// Test file to try loading a GOTO-model into memory and running a sample verification run on it.
4+
#include <util/exception_utils.h>
5+
6+
#include <libcprover-cpp/api.h>
7+
#include <libcprover-cpp/options.h>
8+
9+
#include <iostream>
10+
#include <vector>
11+
12+
int main(int argc, char *argv[])
13+
{
14+
try
15+
{
16+
std::cout << "Hello from API stub" << std::endl;
17+
18+
// Convert argv to vector of strings for initialize_goto_model
19+
std::vector<std::string> arguments(argv + 1, argv + argc);
20+
21+
// Create API options object, to pass to initialiser of API object.
22+
auto api_options = api_optionst::create().simplify(false);
23+
24+
// Initialise API dependencies and global configuration in one step.
25+
api_sessiont api(api_options);
26+
27+
// Demonstrate the loading of a goto-model from the command line arguments
28+
api.load_model_from_files(arguments);
29+
30+
std::cout << "Successfully initialised goto_model" << std::endl;
31+
return 0;
32+
}
33+
catch(const invalid_command_line_argument_exceptiont &e)
34+
{
35+
std::cout << e.what() << std::endl;
36+
}
37+
}
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
add_test_pl_tests(
2+
"$<TARGET_FILE:api-binary-driver>"
3+
)
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
#include <assert.h>
2+
3+
int main(int argc, char *argv[])
4+
{
5+
int a[] = {0, 1, 2, 3, 4};
6+
assert(a[4] != 4);
7+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
Successfully initialised goto_model
7+
--
8+
--

src/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -102,6 +102,7 @@ add_subdirectory(jsil)
102102
add_subdirectory(json)
103103
add_subdirectory(json-symtab-language)
104104
add_subdirectory(langapi)
105+
add_subdirectory(libcprover-cpp)
105106
add_subdirectory(linking)
106107
add_subdirectory(pointer-analysis)
107108
add_subdirectory(solvers)

src/libcprover-cpp/CMakeLists.txt

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

0 commit comments

Comments
 (0)