Skip to content

Add brackets to resolve ambiguity #927

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
merged 2 commits into from
May 17, 2017

Conversation

NathanJPhillips
Copy link
Contributor

@NathanJPhillips NathanJPhillips commented May 16, 2017

There is an ambiguity in this expression caused by a mix of bit-wise (operator&) and logical (operator!) operators in mini_bdd.
Personally I would change the bit-wise operators to logical operators in mini_bdd but some concern was raised that people may then wrongly expect them to short-circuit, as the Boolean logical operators do. (Overridden logical operators do not short-circuit, as stated here under Restrictions: http://en.cppreference.com/w/cpp/language/operators.)
The other option would be to change the operator! to operator~, but in my opinion this would be moving in the wrong direction and reduce code-clarity.

@NathanJPhillips
Copy link
Contributor Author

@thk123 - could you comment on why this hasn't caused Travis to fail? Are the unit tests built with different settings to the main build so that warnings don't cause errors?

@thk123
Copy link
Contributor

thk123 commented May 16, 2017

@NathanJPhillips So I looked at the travis file and as we suspected, the -Wall -Werror appear to be manually specified only for the make -C src (i.e. not unit *AND* not src/clobber, src/memory-models`...)

I think line 155 should read:

  - COMMAND="make -C unit CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" &&
    eval ${PRE_COMMAND} ${COMMAND}

That is replacing $FLAGS with -Wall -Werror -pedantic -O2 -g since this makes it consistent with the make -C src command on line 146.

The AppVeyor.yml seems to be building consistently.

@NathanJPhillips NathanJPhillips force-pushed the bugfix/mini_bdd-operators branch from 4f321b9 to 31cba6b Compare May 16, 2017 16:38
@NathanJPhillips
Copy link
Contributor Author

OK, I've pushed a commit with Travis updated but without the fix to show that it fails. I'll then push the fix once we've seen the failure.

@NathanJPhillips
Copy link
Contributor Author

NathanJPhillips commented May 17, 2017

Here is the failed build showing the problem: https://travis-ci.org/diffblue/cbmc/builds/232900282
In particular from https://travis-ci.org/diffblue/cbmc/jobs/232900286:

g++-5 -c -MMD -MP -std=c++11 -Wall -Werror -pedantic -O2 -g  -I ../src/ -I. -o miniBDD.o miniBDD.cpp
miniBDD.cpp: In function ‘void test1()’:
miniBDD.cpp:21:26: error: suggest parentheses around operand of ‘!’ or change ‘&’ to ‘&&’ or ‘!’ to ‘~’ [-Werror=parentheses]
   mini_bddt f=(x&y&z)|(!x&!y&z);
                          ^
cc1plus: all warnings being treated as errors

I've now pushed the fix.

@kroening kroening merged commit bd4221c into diffblue:master May 17, 2017
@NathanJPhillips NathanJPhillips deleted the bugfix/mini_bdd-operators branch May 17, 2017 15:58
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.

4 participants