Skip to content

Add brackets to resolve ambiguity#927

Merged
kroening merged 2 commits intodiffblue:masterfrom
NathanJPhillips:bugfix/mini_bdd-operators
May 17, 2017
Merged

Add brackets to resolve ambiguity#927
kroening merged 2 commits intodiffblue:masterfrom
NathanJPhillips:bugfix/mini_bdd-operators

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