Static analysis cleanup and open issues

[daniel-j-h]

I used LLVM's (3.6) static analyzer and clang's (3.6) Weverything flag in order to check the source.

There are minor issues I could fix myself, e.g. undefined behavior when doing 1 << 31.
(Interestingly this is not UB anymore in C++14, see: http://stackoverflow.com/q/26331035)

This increment looks suspicious, as it is dead code:

z3/src/ast/used_vars.cpp

Lines 106 to 112 in d01c349

	unsigned r = 0;
	unsigned num = m_found_vars.size();
	for (unsigned i = 0; i < num; i++) {
	if (m_found_vars[i])
	return r++;
	}
	return r;

Clarify operator precedence: && trumps ||: Is this correct?

z3/src/ast/fpa/fpa2bv_converter.cpp

Lines 1883 to 1884 in d01c349

	m_bv_util.get_bv_size(args[0]) == 3 &&
	m_arith_util.is_int(args[1]) ||

Undefined behavior in reinterpret_cast's, one example is this, but there are more:

z3/src/util/hwf.cpp

Line 161 in d01c349

uint64 r = (RAW(s.value) & 0x800FFFFFFFFFFFFFull) | ((exp + 1023) << 52);

"dereference of type 'const uint64 *' (aka 'const unsigned long long *') that was reinterpret_cast from type 'double *' has undefined behavior"

-Wundefined-reinterpret-cast finds those.

This loop is executed only a single time. Always. Is this correct?

z3/src/util/prime_generator.cpp

Line 70 in d01c349

break;

Note: based on the comment by wintersteiger in #11 this pull request is against the unstable branch.

Would you please be so kind and take a look at those issues -- maybe if you have the time do a static analysis and Weverything build yourself and check the left over warnings.

Thanks,
Daniel

[wintersteiger]

Thanks for the patches, those all look good to me. I've moved some of the other issues into separate issues to be looked at later.

[wintersteiger]

@daniel-j-h if it's not too much trouble, could I get you to sign a CLA before we merge this?

[daniel-j-h]

@wintersteiger signed.

[wintersteiger]

Sorry for the premature closure of this. I'm now merging it into master.

[msftclas]

Hi @daniel-j-h, I'm your friendly neighborhood Microsoft Pull Request Bot (You can call me MSBOT). Thanks for your contribution!
You've already signed the contribution license agreement. Thanks!

The agreement was validated by Microsoft and real humans are currently evaluating your PR.

TTYL, MSBOT;

[wintersteiger]

Merged into master as of 6749c19