diff --git a/scripts/mk_util.py b/scripts/mk_util.py index bd8889fb5..7466158e6 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -298,13 +298,15 @@ def test_fpmath(cc): t = TempFile('tstsse.cpp') t.add('int main() { return 42; }\n') t.commit() - if exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-mfpmath=sse -msse -msse2']) == 0: + # -Werror is needed because some versions of clang warn about unrecognized + # -m flags. + if exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-mfpmath=sse -msse -msse2']) == 0: FPMATH_FLAGS="-mfpmath=sse -msse -msse2" return "SSE2-GCC" - elif exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-msse -msse2']) == 0: + elif exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-msse -msse2']) == 0: FPMATH_FLAGS="-msse -msse2" return "SSE2-CLANG" - elif exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-mfpu=vfp -mfloat-abi=hard']) == 0: + elif exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-mfpu=vfp -mfloat-abi=hard']) == 0: FPMATH_FLAGS="-mfpu=vfp -mfloat-abi=hard" return "ARM-VFP" else: @@ -2528,7 +2530,8 @@ def mk_config(): check_ar() CXX = find_cxx_compiler() CC = find_c_compiler() - SLIBEXTRAFLAGS = '' + SLITEXTRAFLAGS = '' +# SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so.0' % LDFLAGS EXE_EXT = '' LIB_EXT = '.a' if GPROF: diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp index a2682fc35..e898f2720 100644 --- a/src/api/z3_replayer.cpp +++ b/src/api/z3_replayer.cpp @@ -36,7 +36,7 @@ void throw_invalid_reference() { struct z3_replayer::imp { z3_replayer & m_owner; std::istream & m_stream; - signed char m_curr; // current char; + int m_curr; // current char; int m_line; // line svector m_string; symbol m_id; @@ -158,7 +158,7 @@ struct z3_replayer::imp { } } - signed char curr() const { return m_curr; } + int curr() const { return m_curr; } void new_line() { m_line++; } void next() { m_curr = m_stream.get(); } @@ -168,7 +168,7 @@ struct z3_replayer::imp { m_string.reset(); next(); while (true) { - signed char c = curr(); + int c = curr(); if (c == EOF) { throw z3_replayer_exception("unexpected end of file"); } @@ -229,7 +229,7 @@ struct z3_replayer::imp { } m_int64 = 0; while (true) { - char c = curr(); + int c = curr(); if ('0' <= c && c <= '9') { m_int64 = 10*m_int64 + (c - '0'); next(); @@ -247,7 +247,7 @@ struct z3_replayer::imp { throw z3_replayer_exception("invalid unsigned"); m_uint64 = 0; while (true) { - char c = curr(); + int c = curr(); if ('0' <= c && c <= '9') { m_uint64 = 10*m_uint64 + (c - '0'); next(); @@ -303,7 +303,7 @@ struct z3_replayer::imp { unsigned pos = 0; m_ptr = 0; while (true) { - char c = curr(); + int c = curr(); if ('0' <= c && c <= '9') { m_ptr = m_ptr * 16 + (c - '0'); } @@ -325,7 +325,7 @@ struct z3_replayer::imp { void skip_blank() { while (true) { - char c = curr(); + int c = curr(); if (c == '\n') { new_line(); next(); @@ -413,7 +413,7 @@ struct z3_replayer::imp { } }); skip_blank(); - char c = curr(); + int c = curr(); if (c == EOF) return; switch (c) { diff --git a/src/parsers/util/scanner.cpp b/src/parsers/util/scanner.cpp index c0947fa24..926085a78 100644 --- a/src/parsers/util/scanner.cpp +++ b/src/parsers/util/scanner.cpp @@ -18,7 +18,7 @@ Revision History: --*/ #include "parsers/util/scanner.h" -inline signed char scanner::read_char() { +inline int scanner::read_char() { if (m_is_interactive) { ++m_pos; return m_stream.get(); @@ -58,7 +58,7 @@ inline bool scanner::state_ok() { void scanner::comment(char delimiter) { while(state_ok()) { - signed char ch = read_char(); + int ch = read_char(); if ('\n' == ch) { ++m_line; } @@ -68,7 +68,7 @@ void scanner::comment(char delimiter) { } } -scanner::token scanner::read_symbol(signed char ch) { +scanner::token scanner::read_symbol(int ch) { bool escape = false; if (m_smt2) m_string.pop_back(); // remove leading '|' @@ -94,7 +94,7 @@ scanner::token scanner::read_symbol(signed char ch) { scanner::token scanner::read_id(char first_char) { - signed char ch; + int ch; m_string.reset(); m_params.reset(); m_string.push_back(first_char); @@ -159,7 +159,7 @@ bool scanner::read_params() { unsigned param_num = 0; while (state_ok()) { - signed char ch = read_char(); + int ch = read_char(); switch (m_normalized[(unsigned char) ch]) { case '0': param_num = 10*param_num + (ch - '0'); @@ -208,7 +208,7 @@ scanner::token scanner::read_number(char first_char, bool is_pos) { m_state = INT_TOKEN; while (true) { - signed char ch = read_char(); + int ch = read_char(); if (m_normalized[(unsigned char) ch] == '0') { m_number = rational(10)*m_number + rational(ch - '0'); if (m_state == FLOAT_TOKEN) { @@ -236,7 +236,7 @@ scanner::token scanner::read_string(char delimiter, token result) { m_string.reset(); m_params.reset(); while (true) { - signed char ch = read_char(); + int ch = read_char(); if (!state_ok()) { return m_state; @@ -265,7 +265,7 @@ scanner::token scanner::read_string(char delimiter, token result) { scanner::token scanner::read_bv_literal() { TRACE("scanner", tout << "read_bv_literal\n";); if (m_bv_token) { - signed char ch = read_char(); + int ch = read_char(); if (ch == 'x') { ch = read_char(); m_number = rational(0); @@ -315,7 +315,7 @@ scanner::token scanner::read_bv_literal() { } else { // hack for the old parser - signed char ch = read_char(); + int ch = read_char(); bool is_hex = false; m_state = ID_TOKEN; @@ -449,7 +449,7 @@ scanner::scanner(std::istream& stream, std::ostream& err, bool smt2, bool bv_tok scanner::token scanner::scan() { while (state_ok()) { - signed char ch = read_char(); + int ch = read_char(); switch (m_normalized[(unsigned char) ch]) { case ' ': break; diff --git a/src/parsers/util/scanner.h b/src/parsers/util/scanner.h index 2871eb901..2a59451b9 100644 --- a/src/parsers/util/scanner.h +++ b/src/parsers/util/scanner.h @@ -76,8 +76,8 @@ private: bool m_smt2; bool m_bv_token; - signed char read_char(); - token read_symbol(signed char ch); + int read_char(); + token read_symbol(int ch); void unread_char(); void comment(char delimiter); token read_id(char first_char);