Skip to content

Fix CPP models when using CMake Build #5285

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
tautschnig merged 4 commits into from
Apr 4, 2020
Merged

Fix CPP models when using CMake Build #5285

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
7e87db1
Fix over-writing library prologue
petr-bauch Feb 25, 2020
3abc5db
Add test for the new operator
Apr 1, 2020
64f1c3d
Add test verifying that the string abstraction is enabled
Apr 1, 2020
9c5a5c4
Add dependency to cprover_library.inc for the C++ module
Apr 2, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions regression/cbmc-cpp/cpp-new/main.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
#include <cassert>

int main()
{
int *some_data = new int(10);
assert(some_data);
assert(*some_data == 10);
return 0;
}
10 changes: 10 additions & 0 deletions regression/cbmc-cpp/cpp-new/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
main.cpp
--pointer-check
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
--
Ensure that the new operator is implemented.
10 changes: 10 additions & 0 deletions regression/cbmc-library/string-abstraction/test-c-with-string-abstraction.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
test.c
--string-abstraction --show-goto-functions
strlen#return_value = \(.*\)s#strarg->length - POINTER_OFFSET\(s\);
^EXIT=0$
^SIGNAL=0$
--
--
Ensure that the --string-abstraction flag enables the string abstraction
version of string functions
10 changes: 10 additions & 0 deletions regression/cbmc-library/string-abstraction/test-c-without-string-abstraction.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
test.c
--show-goto-functions
IF !\(\(signed int\)s\[\(.*\)len\] != 0\) THEN GOTO 2
^EXIT=0$
^SIGNAL=0$
--
--
Ensure that if the string abstraction flag is not provided, the regular model for
string functions is used (in this case searching for the terminator).
9 changes: 9 additions & 0 deletions regression/cbmc-library/string-abstraction/test.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
#include <assert.h>
#include <stdlib.h>

int main()
{
char *x = malloc(sizeof(char) * 10);
x[8] = '\0';
assert(strlen(x) == 8);
}
4 changes: 3 additions & 1 deletion src/ansi-c/cprover_library.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,9 @@ std::string get_cprover_library_text(
const struct cprover_library_entryt cprover_library[],
const std::string &prologue)
{
std::ostringstream library_text(prologue);
// the default mode is ios_base::out which means subsequent write to the
// stream will overwrite the original content
std::ostringstream library_text(prologue, std::ios_base::ate);

std::size_t count=0;

Expand Down
16 changes: 8 additions & 8 deletions src/cpp/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,14 +1,8 @@
file(GLOB cpp_library_sources "library/*.c")

add_custom_command(OUTPUT converter_input.txt
COMMAND cat ${cpp_library_sources} > converter_input.txt
DEPENDS ${cpp_library_sources}
)

add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
COMMAND ../ansi-c/converter < "converter_input.txt" > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
DEPENDS "converter_input.txt" ../ansi-c/converter
)
COMMAND cat ${cpp_library_sources} | $<TARGET_FILE:converter> > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
DEPENDS converter ${cpp_library_sources})

################################################################################

Expand All @@ -33,6 +27,12 @@ endif()
file(GLOB_RECURSE sources "*.cpp" "*.h")
add_library(cpp ${sources})

set_source_files_properties(
${sources}
PROPERTIES
OBJECT_DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
)
Copy link
Contributor

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue Apr 3, 2020 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should just be add_dependencies(cpp "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc") I think?

Copy link
Contributor Author

@thk123 thk123 Apr 3, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copied from ansi-c, will try updating both.

Copy link
Contributor Author

@thk123 thk123 Apr 3, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This doesn't work:

CMake Error at src/cpp/CMakeLists.txt:30 (add_dependencies):
  The dependency target
  "/home/tkiley/workspace/cbmc/build/debug/src/cpp/cprover_library.inc" of
  target "cpp" does not exist.

You're more than welcome to raise a follow up PR making this nicer, but I'd rather just merge this as is, rather than spend more time on it, since it does fix the problem of the C++ library and macros in the C library not working on CMake.


generic_includes(cpp)

target_link_libraries(cpp util ansi-c)