Skip to content

Make CMake generation of cprover_library.inc match with Makefile #5234

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

Conversation

hannes-steffenhagen-diffblue
Copy link
Contributor

Before it appended the converter input at configure time, meaning if you changed
any of the model *.c files it’d actually not notice the change unless you ran
CMake again. This version will pick up such changes, and also matches what we
have in the current Makefile.

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

COMMAND converter < ${converter_input_path} > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
DEPENDS converter ${converter_input_path}
)
COMMAND cat ${ansi_c_library_sources} | $<TARGET_FILE:converter> > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
Copy link
Contributor

Choose a reason for hiding this comment

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

Any particular reason for using cat here, rather than just stdin redirection from the file?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

@chrisr-diffblue Because it’s a list of files, not just one.

Copy link
Contributor

Choose a reason for hiding this comment

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

Doh, of course.... :-)

Copy link
Contributor

@chrisr-diffblue chrisr-diffblue left a comment

Choose a reason for hiding this comment

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

Good catch, thanks. One minor query, but nothing particularly blocking.

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue force-pushed the fix/cmake-ansi-c-library-converter branch from ecab714 to 0c29c8d Compare February 14, 2020 14:20
Before it appended the converter input at configure time, meaning if you changed
any of the model *.c files it’d actually not notice the change unless you ran
CMake again. This version will pick up such changes, and also matches what we
have in the current Makefile.
@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue force-pushed the fix/cmake-ansi-c-library-converter branch from 0c29c8d to 711b52e Compare February 14, 2020 14:21
@codecov-io
Copy link

Codecov Report

Merging #5234 into develop will decrease coverage by 35.51%.
The diff coverage is n/a.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop   #5234       +/-   ##
===========================================
- Coverage    67.42%   31.9%   -35.52%     
===========================================
  Files         1162     910      -252     
  Lines        95606   79415    -16191     
===========================================
- Hits         64459   25336    -39123     
- Misses       31147   54079    +22932
Flag Coverage Δ
#cproversmt2 ?
#regression ?
#unit 31.9% <ø> (ø) ⬆️
Impacted Files Coverage Δ
src/cpp/cpp_typecheck_virtual_table.cpp 0% <0%> (-100%) ⬇️
src/cpp/cpp_name.cpp 0% <0%> (-100%) ⬇️
src/cpp/cpp_enum_type.h 0% <0%> (-100%) ⬇️
src/goto-checker/witness_provider.h 0% <0%> (-100%) ⬇️
src/goto-checker/single_path_symex_only_checker.h 0% <0%> (-100%) ⬇️
src/util/irep_serialization.h 0% <0%> (-100%) ⬇️
src/solvers/smt2/smt2_dec.h 0% <0%> (-100%) ⬇️
src/goto-symex/symex_dereference_state.h 0% <0%> (-100%) ⬇️
src/solvers/smt2/letify.cpp 0% <0%> (-100%) ⬇️
src/cpp/cpp_token.h 0% <0%> (-100%) ⬇️
... and 880 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 0fbabca...711b52e. Read the comment docs.

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue merged commit 13c9a17 into diffblue:develop Feb 17, 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.

5 participants