Attachment #204797 for bug #238284

View | Details | Raw Unified | Return to bug 238284
Collapse All | Expand All

Lines 50-56 Link Here

(-)scripts/mk_util.py (-5 / +7 lines)
50	CSC_COMPILERS=['csc', 'mcs']	50	CSC_COMPILERS=['csc', 'mcs']
51	JAVAC=None	51	JAVAC=None
52	JAR=None	52	JAR=None
53	PYTHON_PACKAGE_DIR=distutils.sysconfig.get_python_lib()	53	PYTHON_PACKAGE_DIR=distutils.sysconfig.get_python_lib(prefix=getenv("PREFIX", None))
54	BUILD_DIR='build'	54	BUILD_DIR='build'
55	REV_BUILD_DIR='..'	55	REV_BUILD_DIR='..'
56	SRC_DIR='src'	56	SRC_DIR='src'
Lines 298-310 Link Here
298	t = TempFile('tstsse.cpp')	298	t = TempFile('tstsse.cpp')
299	t.add('int main() { return 42; }\n')	299	t.add('int main() { return 42; }\n')
300	t.commit()	300	t.commit()
301	if exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-mfpmath=sse -msse -msse2']) == 0:	301	# -Werror is needed because some versions of clang warn about unrecognized
		302	# -m flags.
		303	if exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-mfpmath=sse -msse -msse2']) == 0:
302	FPMATH_FLAGS="-mfpmath=sse -msse -msse2"	304	FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
303	return "SSE2-GCC"	305	return "SSE2-GCC"
304	elif exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-msse -msse2']) == 0:	306	elif exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-msse -msse2']) == 0:
305	FPMATH_FLAGS="-msse -msse2"	307	FPMATH_FLAGS="-msse -msse2"
306	return "SSE2-CLANG"	308	return "SSE2-CLANG"
307	elif exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-mfpu=vfp -mfloat-abi=hard']) == 0:	309	elif exec_compiler_cmd([cc, CPPFLAGS, '-Werror', 'tstsse.cpp', LDFLAGS, '-mfpu=vfp -mfloat-abi=hard']) == 0:
308	FPMATH_FLAGS="-mfpu=vfp -mfloat-abi=hard"	310	FPMATH_FLAGS="-mfpu=vfp -mfloat-abi=hard"
309	return "ARM-VFP"	311	return "ARM-VFP"
310	else:	312	else:
Lines 2767-2773 Link Here
2767	check_ar()	2769	check_ar()
2768	CXX = find_cxx_compiler()	2770	CXX = find_cxx_compiler()
2769	CC = find_c_compiler()	2771	CC = find_c_compiler()
2770	SLIBEXTRAFLAGS = ''	2772	SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so.0' % LDFLAGS
2771	EXE_EXT = ''	2773	EXE_EXT = ''
2772	LIB_EXT = '.a'	2774	LIB_EXT = '.a'
2773	if GPROF:	2775	if GPROF:




struct z3_replayer::imp {
    z3_replayer &            m_owner;
    std::istream &           m_stream;
    int                      m_curr;  // current char;
    int                      m_line;  // line
    svector<char>            m_string;
    symbol                   m_id;

        }
    }

    int curr() const { return m_curr; }
    void new_line() { m_line++; }
    void next() { m_curr = m_stream.get(); }


        m_string.reset();
        next();
        while (true) {
            int c = curr();
            if (c == EOF) {
                throw z3_replayer_exception("unexpected end of file");
            }

        }
        m_int64 = 0;
        while (true) {
            int c = curr();
            if ('0' <= c && c <= '9') {
                m_int64 = 10*m_int64 + (c - '0');
                next();

            throw z3_replayer_exception("invalid unsigned");
        m_uint64 = 0;
        while (true) {
            int c = curr();
            if ('0' <= c && c <= '9') {
                m_uint64 = 10*m_uint64 + (c - '0');
                next();

        unsigned pos = 0;
        m_ptr = 0;
        while (true) {
            int c = curr();
            if ('0' <= c && c <= '9') {
                m_ptr = m_ptr * 16 + (c - '0');
            }


    void skip_blank() {
        while (true) {
            int c = curr();
            if (c == '\n') {
                new_line();
                next();

                }
            });
            skip_blank();
            int c = curr();
            if (c == EOF)
                return;
            switch (c) {




--*/
#include "parsers/util/scanner.h"

inline int scanner::read_char() {
    if (m_is_interactive) {
        ++m_pos;
        return m_stream.get();


void scanner::comment(char delimiter) {
    while(state_ok()) {
        int ch = read_char();
        if ('\n' == ch) {
            ++m_line;
        }
        if (delimiter == ch || EOF == ch) {
            return;
        }
    }        
}

scanner::token scanner::read_symbol(int ch) {
    bool escape = false;
    if (m_smt2)
        m_string.pop_back(); // remove leading '|'



scanner::token scanner::read_id(char first_char) {
    int ch;
    m_string.reset();
    m_params.reset();
    m_string.push_back(first_char);

    unsigned param_num = 0;
    
    while (state_ok()) {
        int ch = read_char();
        switch (m_normalized[(unsigned char) ch]) {
        case '0': 
            param_num = 10*param_num + (ch - '0');

    m_state = INT_TOKEN;
    
    while (true) {
        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) {

    m_string.reset();
    m_params.reset();
    while (true) {
        int ch = read_char();
        
        if (!state_ok()) {
            return m_state;

scanner::token scanner::read_bv_literal() {
    TRACE("scanner", tout << "read_bv_literal\n";);
    if (m_bv_token) {
        int ch     = read_char();
        if (ch == 'x') {
            ch = read_char();
            m_number  = rational(0);

    }
    else {
        // hack for the old parser
        int ch      = read_char();
        bool is_hex = false;
        
        m_state = ID_TOKEN;


scanner::token scanner::scan() {
    while (state_ok()) {
        int ch = read_char();        
        switch (m_normalized[(unsigned char) ch]) {
        case ' ':
            break;




    buffer<char>       m_buffer;
    unsigned           m_bpos;
    unsigned           m_bend;
    int                m_last_char;
    bool               m_is_interactive;
    bool               m_smt2;
    bool               m_bv_token;

    int read_char();
    token read_symbol(int ch);
    void unread_char();
    void comment(char delimiter);
    token read_id(char first_char);

Lines 79-85 Link Here

(-)src/smt/mam.cpp (-1 / +1 lines)
79	//	79	//
80	// ------------------------------------	80	// ------------------------------------
81	class label_hasher {	81	class label_hasher {
82	svector<char> m_lbl2hash; // cache: lbl_id -> hash	82	svector<signed char> m_lbl2hash; // cache: lbl_id -> hash
83		83
84	void mk_lbl_hash(unsigned lbl_id) {	84	void mk_lbl_hash(unsigned lbl_id) {
85	unsigned a = 17;	85	unsigned a = 17;

Return to bug 238284

Lines 36-42 Link Here

(-)src/api/z3_replayer.cpp (-8 / +8 lines)
36	struct z3_replayer::imp {	36	struct z3_replayer::imp {
37	z3_replayer & m_owner;	37	z3_replayer & m_owner;
38	std::istream & m_stream;	38	std::istream & m_stream;
39	char m_curr; // current char;	39	int m_curr; // current char;
40	int m_line; // line	40	int m_line; // line
41	svector<char> m_string;	41	svector<char> m_string;
42	symbol m_id;	42	symbol m_id;
Lines 158-164 Link Here
158	}	158	}
159	}	159	}
160		160
161	char curr() const { return m_curr; }	161	int curr() const { return m_curr; }
162	void new_line() { m_line++; }	162	void new_line() { m_line++; }
163	void next() { m_curr = m_stream.get(); }	163	void next() { m_curr = m_stream.get(); }
164		164
Lines 168-174 Link Here
168	m_string.reset();	168	m_string.reset();
169	next();	169	next();
170	while (true) {	170	while (true) {
171	char c = curr();	171	int c = curr();
172	if (c == EOF) {	172	if (c == EOF) {
173	throw z3_replayer_exception("unexpected end of file");	173	throw z3_replayer_exception("unexpected end of file");
174	}	174	}
Lines 229-235 Link Here
229	}	229	}
230	m_int64 = 0;	230	m_int64 = 0;
231	while (true) {	231	while (true) {
232	char c = curr();	232	int c = curr();
233	if ('0' <= c && c <= '9') {	233	if ('0' <= c && c <= '9') {
234	m_int64 = 10*m_int64 + (c - '0');	234	m_int64 = 10*m_int64 + (c - '0');
235	next();	235	next();
Lines 247-253 Link Here
247	throw z3_replayer_exception("invalid unsigned");	247	throw z3_replayer_exception("invalid unsigned");
248	m_uint64 = 0;	248	m_uint64 = 0;
249	while (true) {	249	while (true) {
250	char c = curr();	250	int c = curr();
251	if ('0' <= c && c <= '9') {	251	if ('0' <= c && c <= '9') {
252	m_uint64 = 10*m_uint64 + (c - '0');	252	m_uint64 = 10*m_uint64 + (c - '0');
253	next();	253	next();
Lines 303-309 Link Here
303	unsigned pos = 0;	303	unsigned pos = 0;
304	m_ptr = 0;	304	m_ptr = 0;
305	while (true) {	305	while (true) {
306	char c = curr();	306	int c = curr();
307	if ('0' <= c && c <= '9') {	307	if ('0' <= c && c <= '9') {
308	m_ptr = m_ptr * 16 + (c - '0');	308	m_ptr = m_ptr * 16 + (c - '0');
309	}	309	}
Lines 325-331 Link Here
325		325
326	void skip_blank() {	326	void skip_blank() {
327	while (true) {	327	while (true) {
328	char c = curr();	328	int c = curr();
329	if (c == '\n') {	329	if (c == '\n') {
330	new_line();	330	new_line();
331	next();	331	next();
Lines 413-419 Link Here
413	}	413	}
414	});	414	});
415	skip_blank();	415	skip_blank();
416	char c = curr();	416	int c = curr();
417	if (c == EOF)	417	if (c == EOF)
418	return;	418	return;
419	switch (c) {	419	switch (c) {

Lines 18-24 Link Here

(-)src/parsers/util/scanner.cpp (-11 / +11 lines)
18	--*/	18	--*/
19	#include "parsers/util/scanner.h"	19	#include "parsers/util/scanner.h"
20		20
21	inline char scanner::read_char() {	21	inline int scanner::read_char() {
22	if (m_is_interactive) {	22	if (m_is_interactive) {
23	++m_pos;	23	++m_pos;
24	return m_stream.get();	24	return m_stream.get();
Lines 58-74 Link Here
58		58
59	void scanner::comment(char delimiter) {	59	void scanner::comment(char delimiter) {
60	while(state_ok()) {	60	while(state_ok()) {
61	char ch = read_char();	61	int ch = read_char();
62	if ('\n' == ch) {	62	if ('\n' == ch) {
63	++m_line;	63	++m_line;
64	}	64	}
65	if (delimiter == ch \|\| -1 == ch) {	65	if (delimiter == ch \|\| EOF == ch) {
66	return;	66	return;
67	}	67	}
68	}	68	}
69	}	69	}
70		70
71	scanner::token scanner::read_symbol(char ch) {	71	scanner::token scanner::read_symbol(int ch) {
72	bool escape = false;	72	bool escape = false;
73	if (m_smt2)	73	if (m_smt2)
74	m_string.pop_back(); // remove leading '\|'	74	m_string.pop_back(); // remove leading '\|'
Lines 94-100 Link Here
94		94
95		95
96	scanner::token scanner::read_id(char first_char) {	96	scanner::token scanner::read_id(char first_char) {
97	char ch;	97	int ch;
98	m_string.reset();	98	m_string.reset();
99	m_params.reset();	99	m_params.reset();
100	m_string.push_back(first_char);	100	m_string.push_back(first_char);
Lines 159-165 Link Here
159	unsigned param_num = 0;	159	unsigned param_num = 0;
160		160
161	while (state_ok()) {	161	while (state_ok()) {
162	char ch = read_char();	162	int ch = read_char();
163	switch (m_normalized[(unsigned char) ch]) {	163	switch (m_normalized[(unsigned char) ch]) {
164	case '0':	164	case '0':
165	param_num = 10*param_num + (ch - '0');	165	param_num = 10*param_num + (ch - '0');
Lines 208-214 Link Here
208	m_state = INT_TOKEN;	208	m_state = INT_TOKEN;
209		209
210	while (true) {	210	while (true) {
211	char ch = read_char();	211	int ch = read_char();
212	if (m_normalized[(unsigned char) ch] == '0') {	212	if (m_normalized[(unsigned char) ch] == '0') {
213	m_number = rational(10)*m_number + rational(ch - '0');	213	m_number = rational(10)*m_number + rational(ch - '0');
214	if (m_state == FLOAT_TOKEN) {	214	if (m_state == FLOAT_TOKEN) {
Lines 236-242 Link Here
236	m_string.reset();	236	m_string.reset();
237	m_params.reset();	237	m_params.reset();
238	while (true) {	238	while (true) {
239	char ch = read_char();	239	int ch = read_char();
240		240
241	if (!state_ok()) {	241	if (!state_ok()) {
242	return m_state;	242	return m_state;
Lines 265-271 Link Here
265	scanner::token scanner::read_bv_literal() {	265	scanner::token scanner::read_bv_literal() {
266	TRACE("scanner", tout << "read_bv_literal\n";);	266	TRACE("scanner", tout << "read_bv_literal\n";);
267	if (m_bv_token) {	267	if (m_bv_token) {
268	char ch = read_char();	268	int ch = read_char();
269	if (ch == 'x') {	269	if (ch == 'x') {
270	ch = read_char();	270	ch = read_char();
271	m_number = rational(0);	271	m_number = rational(0);
Lines 315-321 Link Here
315	}	315	}
316	else {	316	else {
317	// hack for the old parser	317	// hack for the old parser
318	char ch = read_char();	318	int ch = read_char();
319	bool is_hex = false;	319	bool is_hex = false;
320		320
321	m_state = ID_TOKEN;	321	m_state = ID_TOKEN;
Lines 449-455 Link Here
449		449
450	scanner::token scanner::scan() {	450	scanner::token scanner::scan() {
451	while (state_ok()) {	451	while (state_ok()) {
452	char ch = read_char();	452	int ch = read_char();
453	switch (m_normalized[(unsigned char) ch]) {	453	switch (m_normalized[(unsigned char) ch]) {
454	case ' ':	454	case ' ':
455	break;	455	break;

Lines 71-83 Link Here

(-)src/parsers/util/scanner.h (-3 / +3 lines)
71	buffer<char> m_buffer;	71	buffer<char> m_buffer;
72	unsigned m_bpos;	72	unsigned m_bpos;
73	unsigned m_bend;	73	unsigned m_bend;
74	char m_last_char;	74	int m_last_char;
75	bool m_is_interactive;	75	bool m_is_interactive;
76	bool m_smt2;	76	bool m_smt2;
77	bool m_bv_token;	77	bool m_bv_token;
78		78
79	char read_char();	79	int read_char();
80	token read_symbol(char ch);	80	token read_symbol(int ch);
81	void unread_char();	81	void unread_char();
82	void comment(char delimiter);	82	void comment(char delimiter);
83	token read_id(char first_char);	83	token read_id(char first_char);