mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

update C-example that fails to not use longjumps. Issue #1297

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-10 12:06:19 -07:00
parent 7f693186a0
commit 09ea370ea3
2 changed files with 32 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
examples/c/test_capi.c
View file

@ -65,6 +65,15 @@ void throw_z3_error(Z3_context c, Z3_error_code e)
longjmp(g_catch_buffer, e);
}
/**
\brief Error handling that depends on checking an error code on the context.
*/
void nothrow_z3_error(Z3_context c, Z3_error_code e) {
// no-op
}
/**
\brief Create a logical context.
@ -1592,18 +1601,16 @@ void error_code_example1()
void error_code_example2() {
Z3_config cfg;
Z3_context ctx = NULL;
int r;
Z3_error_code e;
printf("\nerror_code_example2\n");
LOG_MSG("error_code_example2");
/* low tech try&catch */
r = setjmp(g_catch_buffer);
if (r == 0) {
if (1) {
Z3_ast x, y, app;
cfg = Z3_mk_config();
ctx = mk_context_custom(cfg, throw_z3_error);
ctx = mk_context_custom(cfg, nothrow_z3_error);
Z3_del_config(cfg);
x = mk_int_var(ctx, "x");
@ -1611,11 +1618,14 @@ void error_code_example2() {
printf("before Z3_mk_iff\n");
/* the next call will produce an error */
app = Z3_mk_iff(ctx, x, y);
e = Z3_get_error_code(ctx);
if (e != Z3_OK) goto err;
unreachable();
Z3_del_context(ctx);
}
else {
printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, (Z3_error_code)r));
err:
printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, e));
if (ctx != NULL) {
Z3_del_context(ctx);
}
@ -1781,15 +1791,14 @@ void parser_example5() {
Z3_config cfg;
Z3_context ctx = NULL;
Z3_solver s = NULL;
int r;
Z3_error_code e;
printf("\nparser_example5\n");
LOG_MSG("parser_example5");
r = setjmp(g_catch_buffer);
if (r == 0) {
if (1) {
cfg = Z3_mk_config();
ctx = mk_context_custom(cfg, throw_z3_error);
ctx = mk_context_custom(cfg, nothrow_z3_error);
s = mk_solver(ctx);
Z3_del_config(cfg);
@ -1798,12 +1807,15 @@ void parser_example5() {
"(benchmark tst :extrafuns ((x Int (y Int)) :formula (> x y) :formula (> x 0))",
0, 0, 0,
0, 0, 0);
e = Z3_get_error_code(ctx);
if (e != Z3_OK) goto err;
unreachable();
del_solver(ctx, s);
Z3_del_context(ctx);
}
else {
printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, (Z3_error_code)r));
err:
printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, e));
if (ctx != NULL) {
printf("Error message: '%s'.\n",Z3_get_smtlib_error(ctx));
del_solver(ctx, s);
@ -2639,6 +2651,7 @@ void smt2parser_example() {
ctx = mk_context();
fs = Z3_parse_smtlib2_string(ctx, "(declare-fun a () (_ BitVec 8)) (assert (bvuge a #x10)) (assert (bvule a #xf0))", 0, 0, 0, 0, 0, 0);
printf("formulas: %s\n", Z3_ast_to_string(ctx, fs));
Z3_del_context(ctx);
}

16
src/api/api_parsers.cpp
View file

@ -56,20 +56,20 @@ extern "C" {
Z3_func_decl const decls[]) {
Z3_TRY;
LOG_Z3_parse_smtlib_string(c, str, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
std::ostringstream outs;
std::ostringstream* outs = alloc(std::ostringstream);
bool ok = false;
RESET_ERROR_CODE();
init_smtlib_parser(c, num_sorts, sort_names, sorts, num_decls, decl_names, decls);
mk_c(c)->m_smtlib_parser->set_error_stream(outs);
mk_c(c)->m_smtlib_parser->set_error_stream(*outs);
try {
ok = mk_c(c)->m_smtlib_parser->parse_string(str);
}
catch (...) {
ok = false;
}
mk_c(c)->m_smtlib_error_buffer = outs.str();
outs.clear();
mk_c(c)->m_smtlib_error_buffer = outs->str();
dealloc(outs);
if (!ok) {
mk_c(c)->reset_parser();
SET_ERROR_CODE(Z3_PARSER_ERROR);
@ -89,17 +89,17 @@ extern "C" {
LOG_Z3_parse_smtlib_file(c, file_name, num_sorts, sort_names, types, num_decls, decl_names, decls);
bool ok = false;
RESET_ERROR_CODE();
std::ostringstream outs;
std::ostringstream* outs = alloc(std::ostringstream);
init_smtlib_parser(c, num_sorts, sort_names, types, num_decls, decl_names, decls);
mk_c(c)->m_smtlib_parser->set_error_stream(outs);
mk_c(c)->m_smtlib_parser->set_error_stream(*outs);
try {
ok = mk_c(c)->m_smtlib_parser->parse_file(file_name);
}
catch(...) {
ok = false;
}
mk_c(c)->m_smtlib_error_buffer = outs.str();
outs.clear();
mk_c(c)->m_smtlib_error_buffer = outs->str();
dealloc(outs);
if (!ok) {
mk_c(c)->reset_parser();
SET_ERROR_CODE(Z3_PARSER_ERROR);