mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 03:46:17 +00:00
Code Activity

Added filenames to error messages for when we have more than one file.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-01-09 14:51:01 +00:00
parent 00a50eea7f
commit 090a331d79
2 changed files with 101 additions and 96 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/parsers/smt2/smt2parser.cpp
View file

@ -109,7 +109,6 @@ namespace smt2 {
typedef std::pair<symbol, expr*> named_expr; typedef std::pair<symbol, expr*> named_expr;
named_expr m_last_named_expr; named_expr m_last_named_expr;
ast_manager & m() const { return m_ctx.m(); } ast_manager & m() const { return m_ctx.m(); }
pdecl_manager & pm() const { return m_ctx.pm(); } pdecl_manager & pm() const { return m_ctx.pm(); }
sexpr_manager & sm() const { return m_ctx.sm(); } sexpr_manager & sm() const { return m_ctx.sm(); }
@ -402,6 +401,9 @@ namespace smt2 {
void check_int_or_float(char const * msg) { if (!curr_is_int() && !curr_is_float()) throw parser_exception(msg); } void check_int_or_float(char const * msg) { if (!curr_is_int() && !curr_is_float()) throw parser_exception(msg); }
void check_float(char const * msg) { if (!curr_is_float()) throw parser_exception(msg); } void check_float(char const * msg) { if (!curr_is_float()) throw parser_exception(msg); }
char const * m_current_file;
void set_current_file(char const * s) { m_current_file = s; }
void error(unsigned line, unsigned pos, char const * msg) { void error(unsigned line, unsigned pos, char const * msg) {
m_ctx.set_cancel(false); m_ctx.set_cancel(false);
if (use_vs_format()) { if (use_vs_format()) {
@ -410,7 +412,9 @@ namespace smt2 {
m_ctx.diagnostic_stream() << std::endl; m_ctx.diagnostic_stream() << std::endl;
} }
else { else {
m_ctx.regular_stream() << "(error \"line " << line << " column " << pos << ": " << escaped(msg, true) << "\")" << std::endl; m_ctx.regular_stream() << "(error \"";
if (m_current_file) m_ctx.regular_stream() << m_current_file << ": ";
m_ctx.regular_stream()<< "line " << line << " column " << pos << ": " << escaped(msg, true) << "\")" << std::endl;
} }
if (m_ctx.exit_on_error()) { if (m_ctx.exit_on_error()) {
exit(1); exit(1);
@ -2558,7 +2562,7 @@ namespace smt2 {
} }
public: public:
parser(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & p): parser(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & p, char const * filename=0):
m_ctx(ctx), m_ctx(ctx),
m_params(p), m_params(p),
m_scanner(ctx, is, interactive), m_scanner(ctx, is, interactive),
@ -2598,7 +2602,8 @@ namespace smt2 {
m_define_fun_rec("define-fun-rec"), m_define_fun_rec("define-fun-rec"),
m_define_funs_rec("define-funs-rec"), m_define_funs_rec("define-funs-rec"),
m_underscore("_"), m_underscore("_"),
m_num_open_paren(0) { m_num_open_paren(0),
m_current_file(filename) {
// the following assertion does not hold if ctx was already attached to an AST manager before the parser object is created. // the following assertion does not hold if ctx was already attached to an AST manager before the parser object is created.
// SASSERT(!m_ctx.has_manager()); // SASSERT(!m_ctx.has_manager());
@ -2705,8 +2710,8 @@ namespace smt2 {
}; };
}; };
bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps) { bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps, char const * filename) {
smt2::parser p(ctx, is, interactive, ps); smt2::parser p(ctx, is, interactive, ps, filename);
return p(); return p();
} }

2
src/parsers/smt2/smt2parser.h
View file

@ -21,6 +21,6 @@ Revision History:
#include"cmd_context.h" #include"cmd_context.h"
bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive = false, params_ref const & p = params_ref()); bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive = false, params_ref const & p = params_ref(), char const * filename = 0);
#endif #endif