mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

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

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-06-02 17:22:08 -07:00
parent 6fdef691e5
commit 51b75a132c
4 changed files with 27 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
scripts/mk_util.py
View file

@ -298,13 +298,15 @@ def test_fpmath(cc):
t = TempFile('tstsse.cpp') t = TempFile('tstsse.cpp')
t.add('int main() { return 42; }\n') t.add('int main() { return 42; }\n')
t.commit() 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" FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
return "SSE2-GCC" 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" FPMATH_FLAGS="-msse -msse2"
return "SSE2-CLANG" 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" FPMATH_FLAGS="-mfpu=vfp -mfloat-abi=hard"
return "ARM-VFP" return "ARM-VFP"
else: else:
@ -2528,7 +2530,8 @@ def mk_config():
check_ar() check_ar()
CXX = find_cxx_compiler() CXX = find_cxx_compiler()
CC = find_c_compiler() CC = find_c_compiler()
SLIBEXTRAFLAGS = '' SLITEXTRAFLAGS = ''
# SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so.0' % LDFLAGS
EXE_EXT = '' EXE_EXT = ''
LIB_EXT = '.a' LIB_EXT = '.a'
if GPROF: if GPROF:

16
src/api/z3_replayer.cpp
View file

@ -36,7 +36,7 @@ void throw_invalid_reference() {
struct z3_replayer::imp { struct z3_replayer::imp {
z3_replayer & m_owner; z3_replayer & m_owner;
std::istream & m_stream; std::istream & m_stream;
signed char m_curr; // current char; int m_curr; // current char;
int m_line; // line int m_line; // line
svector<char> m_string; svector<char> m_string;
symbol m_id; 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 new_line() { m_line++; }
void next() { m_curr = m_stream.get(); } void next() { m_curr = m_stream.get(); }
@ -168,7 +168,7 @@ struct z3_replayer::imp {
m_string.reset(); m_string.reset();
next(); next();
while (true) { while (true) {
signed char c = curr(); int c = curr();
if (c == EOF) { if (c == EOF) {
throw z3_replayer_exception("unexpected end of file"); throw z3_replayer_exception("unexpected end of file");
} }
@ -229,7 +229,7 @@ struct z3_replayer::imp {
} }
m_int64 = 0; m_int64 = 0;
while (true) { while (true) {
char c = curr(); int c = curr();
if ('0' <= c && c <= '9') { if ('0' <= c && c <= '9') {
m_int64 = 10*m_int64 + (c - '0'); m_int64 = 10*m_int64 + (c - '0');
next(); next();
@ -247,7 +247,7 @@ struct z3_replayer::imp {
throw z3_replayer_exception("invalid unsigned"); throw z3_replayer_exception("invalid unsigned");
m_uint64 = 0; m_uint64 = 0;
while (true) { while (true) {
char c = curr(); int c = curr();
if ('0' <= c && c <= '9') { if ('0' <= c && c <= '9') {
m_uint64 = 10*m_uint64 + (c - '0'); m_uint64 = 10*m_uint64 + (c - '0');
next(); next();
@ -303,7 +303,7 @@ struct z3_replayer::imp {
unsigned pos = 0; unsigned pos = 0;
m_ptr = 0; m_ptr = 0;
while (true) { while (true) {
char c = curr(); int c = curr();
if ('0' <= c && c <= '9') { if ('0' <= c && c <= '9') {
m_ptr = m_ptr * 16 + (c - '0'); m_ptr = m_ptr * 16 + (c - '0');
} }
@ -325,7 +325,7 @@ struct z3_replayer::imp {
void skip_blank() { void skip_blank() {
while (true) { while (true) {
char c = curr(); int c = curr();
if (c == '\n') { if (c == '\n') {
new_line(); new_line();
next(); next();
@ -413,7 +413,7 @@ struct z3_replayer::imp {
} }
}); });
skip_blank(); skip_blank();
char c = curr(); int c = curr();
if (c == EOF) if (c == EOF)
return; return;
switch (c) { switch (c) {

20
src/parsers/util/scanner.cpp
View file

@ -18,7 +18,7 @@ Revision History:
--*/ --*/
#include "parsers/util/scanner.h" #include "parsers/util/scanner.h"
inline signed char scanner::read_char() { inline int scanner::read_char() {
if (m_is_interactive) { if (m_is_interactive) {
++m_pos; ++m_pos;
return m_stream.get(); return m_stream.get();
@ -58,7 +58,7 @@ inline bool scanner::state_ok() {
void scanner::comment(char delimiter) { void scanner::comment(char delimiter) {
while(state_ok()) { while(state_ok()) {
signed char ch = read_char(); int ch = read_char();
if ('\n' == ch) { if ('\n' == ch) {
++m_line; ++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; bool escape = false;
if (m_smt2) if (m_smt2)
m_string.pop_back(); // remove leading '|' 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) { scanner::token scanner::read_id(char first_char) {
signed char ch; int ch;
m_string.reset(); m_string.reset();
m_params.reset(); m_params.reset();
m_string.push_back(first_char); m_string.push_back(first_char);
@ -159,7 +159,7 @@ bool scanner::read_params() {
unsigned param_num = 0; unsigned param_num = 0;
while (state_ok()) { while (state_ok()) {
signed char ch = read_char(); int ch = read_char();
switch (m_normalized[(unsigned char) ch]) { switch (m_normalized[(unsigned char) ch]) {
case '0': case '0':
param_num = 10*param_num + (ch - '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; m_state = INT_TOKEN;
while (true) { while (true) {
signed char ch = read_char(); int ch = read_char();
if (m_normalized[(unsigned char) ch] == '0') { if (m_normalized[(unsigned char) ch] == '0') {
m_number = rational(10)*m_number + rational(ch - '0'); m_number = rational(10)*m_number + rational(ch - '0');
if (m_state == FLOAT_TOKEN) { if (m_state == FLOAT_TOKEN) {
@ -236,7 +236,7 @@ scanner::token scanner::read_string(char delimiter, token result) {
m_string.reset(); m_string.reset();
m_params.reset(); m_params.reset();
while (true) { while (true) {
signed char ch = read_char(); int ch = read_char();
if (!state_ok()) { if (!state_ok()) {
return m_state; return m_state;
@ -265,7 +265,7 @@ scanner::token scanner::read_string(char delimiter, token result) {
scanner::token scanner::read_bv_literal() { scanner::token scanner::read_bv_literal() {
TRACE("scanner", tout << "read_bv_literal\n";); TRACE("scanner", tout << "read_bv_literal\n";);
if (m_bv_token) { if (m_bv_token) {
signed char ch = read_char(); int ch = read_char();
if (ch == 'x') { if (ch == 'x') {
ch = read_char(); ch = read_char();
m_number = rational(0); m_number = rational(0);
@ -315,7 +315,7 @@ scanner::token scanner::read_bv_literal() {
} }
else { else {
// hack for the old parser // hack for the old parser
signed char ch = read_char(); int ch = read_char();
bool is_hex = false; bool is_hex = false;
m_state = ID_TOKEN; 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() { scanner::token scanner::scan() {
while (state_ok()) { while (state_ok()) {
signed char ch = read_char(); int ch = read_char();
switch (m_normalized[(unsigned char) ch]) { switch (m_normalized[(unsigned char) ch]) {
case ' ': case ' ':
break; break;

4
src/parsers/util/scanner.h
View file

@ -76,8 +76,8 @@ private:
bool m_smt2; bool m_smt2;
bool m_bv_token; bool m_bv_token;
signed char read_char(); int read_char();
token read_symbol(signed char ch); token read_symbol(int ch);
void unread_char(); void unread_char();
void comment(char delimiter); void comment(char delimiter);
token read_id(char first_char); token read_id(char first_char);