Attachment 204797 Details for Bug 238284 – Eliminate compile warnings on ARM64

[patch] Eliminate compile warnings on ARM64

z3.patch (text/plain), 7.49 KB, created by John F. Carr on 2019-06-03 08:14:37 UTC

(hide)

Description:

Filename:

MIME Type:

Creator: John F. Carr

Created: 2019-06-03 08:14:37 UTC

Size: 7.49 KB

patch

obsolete

>--- scripts/mk_util.py.orig	2018-12-20 13:32:36.000000000 -0500
>+++ scripts/mk_util.py	2019-06-02 19:28:10.923010000 -0400
>@@ -50,7 +50,7 @@
> CSC_COMPILERS=['csc', 'mcs']
> JAVAC=None
> JAR=None
>-PYTHON_PACKAGE_DIR=distutils.sysconfig.get_python_lib()
>+PYTHON_PACKAGE_DIR=distutils.sysconfig.get_python_lib(prefix=getenv("PREFIX", None))
> BUILD_DIR='build'
> REV_BUILD_DIR='..'
> SRC_DIR='src'
>@@ -298,13 +298,15 @@
>     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:
>@@ -2767,7 +2769,7 @@
>         check_ar()
>         CXX = find_cxx_compiler()
>         CC  = find_c_compiler()
>-        SLIBEXTRAFLAGS = ''
>+        SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so.0' % LDFLAGS
>         EXE_EXT = ''
>         LIB_EXT = '.a'
>         if GPROF:
>--- src/api/z3_replayer.cpp.orig	2018-12-20 13:32:36.000000000 -0500
>+++ src/api/z3_replayer.cpp	2019-06-02 19:17:53.537786000 -0400
>@@ -36,7 +36,7 @@
> struct z3_replayer::imp {
>     z3_replayer &            m_owner;
>     std::istream &           m_stream;
>-    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 @@
>         }
>     }
> 
>-    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 @@
>         m_string.reset();
>         next();
>         while (true) {
>-            char c = curr();
>+            int c = curr();
>             if (c == EOF) {
>                 throw z3_replayer_exception("unexpected end of file");
>             }
>@@ -229,7 +229,7 @@
>         }
>         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 @@
>             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 @@
>         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 @@
> 
>     void skip_blank() {
>         while (true) {
>-            char c = curr();
>+            int c = curr();
>             if (c == '\n') {
>                 new_line();
>                 next();
>@@ -413,7 +413,7 @@
>                 }
>             });
>             skip_blank();
>-            char c = curr();
>+            int c = curr();
>             if (c == EOF)
>                 return;
>             switch (c) {
>--- src/parsers/util/scanner.cpp.orig	2018-12-20 13:32:36.000000000 -0500
>+++ src/parsers/util/scanner.cpp	2019-06-02 19:11:12.370387000 -0400
>@@ -18,7 +18,7 @@
> --*/
> #include "parsers/util/scanner.h"
> 
>-inline char scanner::read_char() {
>+inline int scanner::read_char() {
>     if (m_is_interactive) {
>         ++m_pos;
>         return m_stream.get();
>@@ -58,17 +58,17 @@
> 
> void scanner::comment(char delimiter) {
>     while(state_ok()) {
>-        char ch = read_char();
>+        int ch = read_char();
>         if ('\n' == ch) {
>             ++m_line;
>         }
>-        if (delimiter == ch || -1 == ch) {
>+        if (delimiter == ch || EOF == ch) {
>             return;
>         }
>     }        
> }
> 
>-scanner::token scanner::read_symbol(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_id(char first_char) {
>-    char ch;
>+    int ch;
>     m_string.reset();
>     m_params.reset();
>     m_string.push_back(first_char);
>@@ -159,7 +159,7 @@
>     unsigned param_num = 0;
>     
>     while (state_ok()) {
>-        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 @@
>     m_state = INT_TOKEN;
>     
>     while (true) {
>-        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 @@
>     m_string.reset();
>     m_params.reset();
>     while (true) {
>-        char ch = read_char();
>+        int ch = read_char();
>         
>         if (!state_ok()) {
>             return m_state;
>@@ -265,7 +265,7 @@
> scanner::token scanner::read_bv_literal() {
>     TRACE("scanner", tout << "read_bv_literal\n";);
>     if (m_bv_token) {
>-        char ch     = read_char();
>+        int ch     = read_char();
>         if (ch == 'x') {
>             ch = read_char();
>             m_number  = rational(0);
>@@ -315,7 +315,7 @@
>     }
>     else {
>         // hack for the old parser
>-        char ch     = read_char();
>+        int ch      = read_char();
>         bool is_hex = false;
>         
>         m_state = ID_TOKEN;
>@@ -449,7 +449,7 @@
> 
> scanner::token scanner::scan() {
>     while (state_ok()) {
>-        char ch = read_char();        
>+        int ch = read_char();        
>         switch (m_normalized[(unsigned char) ch]) {
>         case ' ':
>             break;
>--- src/parsers/util/scanner.h.orig	2018-12-20 13:32:36.000000000 -0500
>+++ src/parsers/util/scanner.h	2019-06-02 19:19:59.921462000 -0400
>@@ -71,13 +71,13 @@
>     buffer<char>       m_buffer;
>     unsigned           m_bpos;
>     unsigned           m_bend;
>-    char               m_last_char;
>+    int                m_last_char;
>     bool               m_is_interactive;
>     bool               m_smt2;
>     bool               m_bv_token;
> 
>-    char read_char();
>-    token read_symbol(char ch);
>+    int read_char();
>+    token read_symbol(int ch);
>     void unread_char();
>     void comment(char delimiter);
>     token read_id(char first_char);
>--- src/smt/mam.cpp.orig	2018-12-20 13:32:36.000000000 -0500
>+++ src/smt/mam.cpp	2019-06-02 19:13:30.199562000 -0400
>@@ -79,7 +79,7 @@
>     //
>     // ------------------------------------
>     class label_hasher {
>-        svector<char>               m_lbl2hash;        // cache: lbl_id -> hash
>+        svector<signed char> m_lbl2hash;        // cache: lbl_id -> hash
> 
>         void mk_lbl_hash(unsigned lbl_id) {
>             unsigned a = 17;

Actions: View | Diff

Attachments on bug 238284: 204797