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

API: dont deref already free'd memory on error

Browse source
This commit is contained in:
Nuno Lopes 2020-06-30 15:04:40 +01:00
parent 64f1a759a7
commit 8fda4f904d
7 changed files with 24 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/api/api_context.cpp
View file

@ -147,6 +147,14 @@ namespace api {
}
}
void context::set_error_code(Z3_error_code err, std::string &&opt_msg) {
m_error_code = err;
if (err != Z3_OK) {
m_exception_msg = std::move(opt_msg);
invoke_error_handler(err);
}
}
void context::check_searching() {
if (m_searching) {
set_error_code(Z3_INVALID_USAGE, "cannot use function while searching"); // TBD: error code could be fixed.
@ -287,7 +295,8 @@ namespace api {
buffer << mk_bounded_pp(a->get_arg(i), m(), 3) << " of sort ";
buffer << mk_pp(m().get_sort(a->get_arg(i)), m()) << "\n";
}
warning_msg("%s",buffer.str().c_str());
auto str = buffer.str();
warning_msg("%s", str.c_str());
break;
}
case AST_VAR:

1
src/api/api_context.h
View file

@ -170,6 +170,7 @@ namespace api {
Z3_error_code get_error_code() const { return m_error_code; }
void reset_error_code() { m_error_code = Z3_OK; }
void set_error_code(Z3_error_code err, char const* opt_msg);
void set_error_code(Z3_error_code err, std::string &&opt_msg);
void set_error_handler(Z3_error_handler h) { m_error_handler = h; }
// Sign an error if solver is searching
void check_searching();

4
src/api/api_opt.cpp
View file

@ -358,14 +358,14 @@ extern "C" {
try {
if (!parse_smt2_commands(*ctx.get(), s)) {
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str());
SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str());
return;
}
}
catch (z3_exception& e) {
errstrm << e.msg();
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str());
SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str());
return;
}

8
src/api/api_parsers.cpp
View file

@ -90,14 +90,14 @@ extern "C" {
try {
if (!parse_smt2_commands(*ctx.get(), is)) {
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str());
SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str());
return of_ast_vector(v);
}
}
catch (z3_exception& e) {
errstrm << e.msg();
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str());
SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str());
return of_ast_vector(v);
}
for (expr* e : ctx->tracked_assertions()) {
@ -157,13 +157,13 @@ extern "C" {
ctx->set_diagnostic_stream(ous);
try {
if (!parse_smt2_commands(*ctx.get(), is)) {
SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str().c_str());
SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str());
RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
}
}
catch (z3_exception& e) {
if (ous.str().empty()) ous << e.msg();
SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str().c_str());
SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str());
RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
}
RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));

10
src/api/api_solver.cpp
View file

@ -105,10 +105,10 @@ extern "C" {
m_out.flush();
}
solver2smt2_pp::solver2smt2_pp(ast_manager& m, char const* file):
solver2smt2_pp::solver2smt2_pp(ast_manager& m, const std::string& file):
m_pp_util(m), m_out(file), m_tracked(m) {
if (!m_out) {
throw default_exception("could not open " + std::string(file) + " for output");
throw default_exception("could not open " + file + " for output");
}
}
@ -155,7 +155,7 @@ extern "C" {
solver_params sp(to_solver(s)->m_params);
symbol smt2log = sp.smtlib2_log();
if (smt2log.is_non_empty_string() && !to_solver(s)->m_pp) {
to_solver(s)->m_pp = alloc(solver2smt2_pp, mk_c(c)->m(), smt2log.str().c_str());
to_solver(s)->m_pp = alloc(solver2smt2_pp, mk_c(c)->m(), smt2log.str());
}
}
@ -247,7 +247,7 @@ extern "C" {
if (!parse_smt2_commands(*ctx.get(), is)) {
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str());
SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str());
return;
}
@ -266,7 +266,7 @@ extern "C" {
std::stringstream err;
sat::solver solver(to_solver_ref(s)->get_params(), m.limit());
if (!parse_dimacs(is, err, solver)) {
SET_ERROR_CODE(Z3_PARSER_ERROR, err.str().c_str());
SET_ERROR_CODE(Z3_PARSER_ERROR, err.str());
return;
}
sat2goal s2g;

2
src/api/api_solver.h
View file

@ -28,7 +28,7 @@ struct solver2smt2_pp {
expr_ref_vector m_tracked;
unsigned_vector m_tracked_lim;
solver2smt2_pp(ast_manager& m, char const* file);
solver2smt2_pp(ast_manager& m, const std::string& file);
void assert_expr(expr* e);
void assert_expr(expr* e, expr* t);
void push();

2
src/api/api_tactic.cpp
View file

@ -54,7 +54,7 @@ extern "C" {
if (t == nullptr) {
std::stringstream err;
err << "unknown tactic " << name;
SET_ERROR_CODE(Z3_INVALID_ARG, err.str().c_str());
SET_ERROR_CODE(Z3_INVALID_ARG, err.str());
RETURN_Z3(nullptr);
}
tactic * new_t = t->mk(mk_c(c)->m());