signed char -> int, update mk_util to catch warnings on fptest, thanks to jfc

NikolajBjorner · NikolajBjorner · commit 51b75a132c05 · 2019-06-02T17:22:36.000-07:00
Signed-off-by: Nikolaj Bjorner &lt;nbjorner@microsoft.com&gt;
diff --git 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
@@ -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<char>            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
@@ -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
@@ -76,8 +76,8 @@ class scanner {
     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);
