Skip to content

Conversation

TGWDB
Copy link
Contributor

@TGWDB TGWDB commented Apr 22, 2021

This fixes various details to ensure that make under Cywin can build
cbmc.

This is just some small fixes that appear to stop cbmc from being built using make and Cygwin.

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

This fixes various details to ensure that make under Cywin can build
cbmc.
@codecov
Copy link

codecov bot commented Apr 22, 2021

Codecov Report

Merging #6048 (c8f9e2c) into develop (7663a57) will decrease coverage by 0.39%.
The diff coverage is 58.18%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #6048      +/-   ##
===========================================
- Coverage    74.30%   73.90%   -0.40%     
===========================================
  Files         1444     1444              
  Lines       157453   157448       -5     
===========================================
- Hits        116995   116368     -627     
- Misses       40458    41080     +622     
Impacted Files Coverage Δ
src/solvers/smt2/smt2_conv.h 100.00% <ø> (ø)
src/util/invariant.cpp 81.63% <ø> (ø)
src/util/run.cpp 74.78% <ø> (ø)
src/ansi-c/c_typecheck_initializer.cpp 64.98% <44.44%> (-9.60%) ⬇️
src/solvers/smt2/smt2_conv.cpp 60.38% <52.94%> (ø)
src/solvers/smt2/smt2_solver.cpp 83.11% <65.51%> (ø)
src/ansi-c/gcc_types.cpp 41.86% <0.00%> (-46.52%) ⬇️
src/solvers/prop/prop.cpp 42.85% <0.00%> (-42.86%) ⬇️
src/ansi-c/ansi_c_entry_point.cpp 63.55% <0.00%> (-23.84%) ⬇️
src/util/parse_options.cpp 57.57% <0.00%> (-22.23%) ⬇️
... and 72 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 2fdf995...c8f9e2c. Read the comment docs.

Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

I'd prefer some more clarity in the commit message, and the failing Visual Studio builds suggest that these "small changes" aren't that small at all (the changes to run.cpp seem quite wrong, actually).

@@ -448,43 +448,10 @@ int run(
#endif
}

#ifndef _WIN32
Copy link
Collaborator

Choose a reason for hiding this comment

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

This change doesn't look like "just a small change" at all?

@TGWDB
Copy link
Contributor Author

TGWDB commented Apr 23, 2021

I'd prefer some more clarity in the commit message, and the failing Visual Studio builds suggest that these "small changes" aren't that small at all (the changes to run.cpp seem quite wrong, actually).

I'll comment directly here, then update the commit message(s) at the end if this makes it through review.

The Windows builds are all currently failing due to some CI problem, not related to this PR (that said, I created this PR to get the results from CI, so there is a chance there could be a problem).

There are three changes here:

  1. Remove the static linking in the Cygwin build since this causes the build to fail (this was also suggested in the Makefile for Cygwin anyway).
  2. Update and link the missing dependencies and fix the use of SYMBOL_INFO that appears to have been wrong for some time and not detected/tested.
  3. Change the ifdef statements related to Cygwin (_WIN32) in run.cpp. Note that this appears to be a large change, but the root of the change is that Cygwin build does not call the shell_quote function. This causes the build to fail since the -Werror flag makes this an error. Rather than create a dummy call to this function, I chose to simply change the ifdef code to not include the function. This also meant deleting code inside the function that was inside an ifdef for building in Cygwin.

I hope this clarifies and that CI can be fixed and a proper CI test done.

@tautschnig
Copy link
Collaborator

I'd prefer some more clarity in the commit message, and the failing Visual Studio builds suggest that these "small changes" aren't that small at all (the changes to run.cpp seem quite wrong, actually).

I'll comment directly here, then update the commit message(s) at the end if this makes it through review.

Thank you!

The Windows builds are all currently failing due to some CI problem, not related to this PR (that said, I created this PR to get the results from CI, so there is a chance there could be a problem).

My apologies for not digging deeper and wrongly attributing these failures to your changes!

There are three changes here:

1. Remove the `static` linking in the Cygwin build since this causes the build to fail (this was also suggested in the `Makefile` for Cygwin anyway).

Yes, this one seemed less surprising,

2. Update and link the missing dependencies and fix the use of `SYMBOL_INFO` that appears to have been wrong for some time and not detected/tested.

and that change looked good.

3. Change the `ifdef` statements related to Cygwin (`_WIN32`) in `run.cpp`. Note that this appears to be a large change, but the root of the change is that Cygwin build does not call the `shell_quote` function. This causes the build to fail since the `-Werror` flag makes this an error. Rather than create a dummy call to this function, I chose to simply change the `ifdef` code to not include the function. This also meant deleting code inside the function that was inside an `ifdef` for building in Cygwin.

This one I'm still not very clear about. _WIN32 is more than Cygwin, this is all Windows builds. I am surprised to hear that shell_quote wasn't being invoked at all, it seemed rather important to do the work it is doing (proper escaping). Looking at the code base you are of course right, but it seems we have another problem to solve: shell_quote exists twice, once in util/ and once in ansi-c. These are byte-by-byte the same, so one of them ought to be removed. This might fix the problem as the function would then actually be used?

@tautschnig
Copy link
Collaborator

@TGWDB See #6054 for the fix of Windows builds in CI.

TGWDB added 2 commits April 26, 2021 10:57
This fixes various details to ensure that make under Cywin can build
cbmc.
@TGWDB
Copy link
Contributor Author

TGWDB commented May 7, 2021

Closing this PR as it mixes different things. The fix needed for general WIN32 build is now #6091.

@TGWDB TGWDB closed this May 7, 2021
@TGWDB TGWDB mentioned this pull request May 7, 2021
7 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants