Feature banner helper by hannes-steffenhagen-diffblue · Pull Request #3920 · diffblue/cbmc

hannes-steffenhagen-diffblue · 2019-01-24T16:20:57Z

This adds a small helper function, to help with writing banners like

**              this             **

which we do for our tools. Also updates all our help messages to use the helper.

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.

smowton · 2019-01-24T16:22:24Z

While you're at it, maybe fix the copyright dates?

NlightNFotis

Looks good to me.

hannes-steffenhagen-diffblue · 2019-01-24T16:27:47Z

@smowton I purposefully avoided messing with the copyright notices in any way because that's an issue I'd rather not deal with, if it was determined that they need changing I'd rather have that done separate from this work

NlightNFotis · 2019-01-24T16:29:46Z

Basically I agree with Hannes on this one: as a PR that just reformats the strings, it should only do just that. Changing the content of the strings, however trivial, in my opinion belongs to another PR.

tautschnig · 2019-01-24T16:29:35Z

src/util/parse_options.cpp

 banner_string(const std::string &front_end, const std::string &version)
 {
+  static_assert(CHAR_BIT == 8,
+                "we do make the fairly safe assumption of 8 bit bytes");


Fair enough, I'll remove it. In this case the worst that can happen is odd numbers in the -bits section anyway 🤷‍♀️

Oh, sorry, I did not necessarily want you to feel compelled to remove it. Was just meaning to say that there is existing work to clean this up.

tautschnig · 2019-01-24T16:30:35Z

unit/Makefile

       util/message.cpp \
       util/optional.cpp \
       util/optional_utils.cpp \
+			 util/parse_options.cpp \


Space vs tabs?

🤦‍♀️

tautschnig · 2019-01-24T16:31:09Z

unit/util/parse_options.cpp

+#include <testing-utils/use_catch.h>
+#include <util/parse_options.h>
+
+TEST_CASE("align_center_with_border", "[core][util]") {


{ on new line?

danpoe

LGTM

martin-cs

Couldn't we use left-pad :-D

hannes-steffenhagen-diffblue · 2019-01-24T17:33:57Z

Slight change: There was a potential underflow bug if the total length of the banner text exceeded the expected total length of the banner. The "fill" now can't be lower than 0.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 55a8e61).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98597198
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

hannes-steffenhagen-diffblue · 2019-01-25T12:08:34Z

test-gen failure appears to be unrelated to this PR

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: b7a33ba).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98634346
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

…to_harness_stub Add stub for new goto-harness tool [depends-on: #3920]

hannes-steffenhagen-diffblue requested review from cesaro, chrisr-diffblue, cristina-david, kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners January 24, 2019 16:20

NlightNFotis approved these changes Jan 24, 2019

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the feature-banner_helper branch from 3bad5ab to 2f7df5d Compare January 24, 2019 16:26

tautschnig approved these changes Jan 24, 2019

View reviewed changes

danpoe approved these changes Jan 24, 2019

View reviewed changes

hannes-steffenhagen-diffblue mentioned this pull request Jan 24, 2019

Add stub for new goto-harness tool [depends-on: #3920] #3875

Merged

7 tasks

hannes-steffenhagen-diffblue force-pushed the feature-banner_helper branch from 2f7df5d to ef956a9 Compare January 24, 2019 16:53

martin-cs approved these changes Jan 24, 2019

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the feature-banner_helper branch from ef956a9 to 8a99323 Compare January 24, 2019 17:32

hannes-steffenhagen-diffblue force-pushed the feature-banner_helper branch from 8a99323 to ea62b6d Compare January 24, 2019 17:35

hannes-steffenhagen-diffblue added 8 commits January 25, 2019 10:29

Add helper function for aligning banners

73118f0

Use align_center_with_border helper in jbmc

887e763

Use align_center_with_border helper in cbmc

bd5ecf5

Use align_center_with_border helper in goto-cc

bd8aa81

Use align_center_with_border helper in goto-diff

21d4f7d

Use align_center_with_border helper in goto-analyzer

e7fc1d5

Use align_center_with_border helper in goto-instrument

aac3f72

Use align_center_with_border helper in jdiff

4dc003e

hannes-steffenhagen-diffblue force-pushed the feature-banner_helper branch from ea62b6d to 55a8e61 Compare January 25, 2019 10:29

tautschnig assigned smowton and peterschrammel Jan 25, 2019

allredj reviewed Jan 25, 2019

View reviewed changes

Use align_center_with_border helper in janalyzer

b7a33ba

hannes-steffenhagen-diffblue force-pushed the feature-banner_helper branch from 55a8e61 to b7a33ba Compare January 25, 2019 15:39

allredj reviewed Jan 25, 2019

View reviewed changes

peterschrammel approved these changes Jan 25, 2019

View reviewed changes

NlightNFotis merged commit f6f7ecd into diffblue:develop Jan 25, 2019

hannes-steffenhagen-diffblue added a commit that referenced this pull request Jan 26, 2019

Merge pull request #3875 from hannes-steffenhagen-diffblue/feature-go…

d3d19f9

…to_harness_stub Add stub for new goto-harness tool [depends-on: #3920]

Conversation

hannes-steffenhagen-diffblue commented Jan 24, 2019

Uh oh!

smowton commented Jan 24, 2019

Uh oh!

NlightNFotis left a comment

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue commented Jan 24, 2019

Uh oh!

NlightNFotis commented Jan 24, 2019

Uh oh!

tautschnig Jan 24, 2019

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Jan 24, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 24, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 24, 2019

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Jan 24, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 24, 2019

Choose a reason for hiding this comment

Uh oh!

danpoe left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue commented Jan 24, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue commented Jan 25, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants