Skip to content

Fix CMake build on Windows #5437

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.

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

Conversation

NlightNFotis
Copy link
Contributor

Attempting to build cbmc with cmake on Visual Studio 2019/Win 10 fails.

This PR introduces some needed changes to two CMakeLists.txt files to make
it work.

  • 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.

Without them being required, a new build where
the binaries of the two programs are not found
fails late and with confusing error messages.

This makes the build fail fast and early, at
the point where the error is produced (where
the binaries have failed to have been found).
The CMakeLists.txt was performing a `cp` command
directly, which while it was not an issue on linux,
if you build on Windows with cmake, it fails the
build because the equivalent command is `copy`.

I made it so we use the portable interface of
the CMake binary to perform the copy across all
targets, so it's portable.
@codecov
Copy link

codecov bot commented Jul 29, 2020

Codecov Report

Merging #5437 into develop will not change coverage.
The diff coverage is n/a.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #5437   +/-   ##
========================================
  Coverage    68.21%   68.21%           
========================================
  Files         1178     1178           
  Lines        97561    97561           
========================================
  Hits         66554    66554           
  Misses       31007    31007           
Flag Coverage Δ
#cproversmt2 42.77% <ø> (ø)
#regression 65.38% <ø> (ø)
#unit 32.26% <ø> (ø)

Flags with carried forward coverage won't be shown. Click here to find out more.


Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update b45ff46...715c7b2. Read the comment docs.

1 similar comment
@codecov
Copy link

codecov bot commented Jul 29, 2020

Codecov Report

Merging #5437 into develop will not change coverage.
The diff coverage is n/a.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #5437   +/-   ##
========================================
  Coverage    68.21%   68.21%           
========================================
  Files         1178     1178           
  Lines        97561    97561           
========================================
  Hits         66554    66554           
  Misses       31007    31007           
Flag Coverage Δ
#cproversmt2 42.77% <ø> (ø)
#regression 65.38% <ø> (ø)
#unit 32.26% <ø> (ø)

Flags with carried forward coverage won't be shown. Click here to find out more.


Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update b45ff46...715c7b2. Read the comment docs.

@@ -1,7 +1,7 @@
project(CBMC)

find_package(BISON)
find_package(FLEX)
find_package(BISON REQUIRED)

Choose a reason for hiding this comment

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

👍 it's a non-optional dependency and absolutely should be marked as REQUIRED

@@ -4,7 +4,7 @@ add_subdirectory(unit)

add_custom_target(java-models-library ALL
COMMAND mvn --quiet -Dmaven.test.skip=true package
COMMAND cp target/core-models.jar ${CMAKE_CURRENT_SOURCE_DIR}/src/java_bytecode/library/
COMMAND ${CMAKE_COMMAND} -E copy target/core-models.jar ${CMAKE_CURRENT_SOURCE_DIR}/src/java_bytecode/library/

Choose a reason for hiding this comment

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

Yep, we should avoid using unix-y commands in our... commands.

I'd recommend putting all the variable stuff in " quotes as well... I don't actually know off the top of my head how CMake handles variable expansions with whitespace in them.

Copy link
Contributor

Choose a reason for hiding this comment

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

It's no worse than the current situation so I'm happy for this to be merged as is - but It probably is worth trying a build on a checkout of CBMC that has spaces in its file path. On Mac/Windows it's not that uncommon for this to happen.

@@ -4,7 +4,7 @@ add_subdirectory(unit)

add_custom_target(java-models-library ALL
COMMAND mvn --quiet -Dmaven.test.skip=true package

Choose a reason for hiding this comment

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

Not an action for this PR, but we should also avoid hardcoding the maven executable. By adding a configuration for this we could support cases where people want to build with ~/.local/bin/maven-experimental or whatever.

@@ -4,7 +4,7 @@ add_subdirectory(unit)

add_custom_target(java-models-library ALL
COMMAND mvn --quiet -Dmaven.test.skip=true package
COMMAND cp target/core-models.jar ${CMAKE_CURRENT_SOURCE_DIR}/src/java_bytecode/library/
COMMAND ${CMAKE_COMMAND} -E copy target/core-models.jar ${CMAKE_CURRENT_SOURCE_DIR}/src/java_bytecode/library/
Copy link
Contributor

Choose a reason for hiding this comment

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

It's no worse than the current situation so I'm happy for this to be merged as is - but It probably is worth trying a build on a checkout of CBMC that has spaces in its file path. On Mac/Windows it's not that uncommon for this to happen.

@NlightNFotis NlightNFotis merged commit c82daba into diffblue:develop Jul 31, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants