mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Fixes for error handling in ml api

Browse source
This commit is contained in:
Josh Berdine 2012-12-04 03:23:10 +00:00 committed by Leonardo de Moura
parent ae5f96895d
commit 949317ccfc
2 changed files with 12 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/ml/add_error_checking.V3.sed
View file

@ -1,2 +1,2 @@
# Customize error handling for contexts created in ML: # Customize error handling for contexts created in ML:
s/Z3_API Z3_mk_context(\(.*\))/Z3_API Z3_mk_context(\1) quote(dealloc,\"Z3_set_error_handler(_res, caml_z3_error_handler);\")/g s/Z3_API Z3_mk_context(\(.*\))/Z3_API Z3_mk_context(\1) quote(dealloc,\"Z3_set_error_handler(_res, (void*)caml_z3_error_handler);\")/g

19
src/api/ml/error_handling.idl
View file

@ -53,6 +53,12 @@ Author:
#endif #endif
// The V3 API uses a single handler irregardless of UNSAFE_ERRORS
quote(c,"
/* All contexts share the same handler */
static value caml_z3_error_handler = 0;
");
#ifdef SAFE_ERRORS #ifdef SAFE_ERRORS
quote(mlmli," quote(mlmli,"
@ -64,7 +70,7 @@ quote(mlmli,"
exception Error of context * error_code exception Error of context * error_code
"); ");
quote(ml," quote(ml,"
/* Register dynamically-generated exception tag for use from C */ (* Register dynamically-generated exception tag for use from C *)
let _ = Callback.register_exception \"Z3.Error\" (Error (Obj.magic None, OK)) let _ = Callback.register_exception \"Z3.Error\" (Error (Obj.magic None, OK))
"); ");
@ -108,7 +114,7 @@ quote(mlmli,"
exception Error of context * error_code exception Error of context * error_code
"); ");
quote(ml," quote(ml,"
/* Register dynamically-generated exception tag for use from C */ (* Register dynamically-generated exception tag for use from C *)
let _ = Callback.register_exception \"Z3.Error\" (Error (Obj.magic None, OK)) let _ = Callback.register_exception \"Z3.Error\" (Error (Obj.magic None, OK))
"); ");
@ -116,9 +122,6 @@ quote(c,"
/* Error checking routine that does nothing */ /* Error checking routine that does nothing */
void check_error_code(Z3_context c) {} void check_error_code(Z3_context c) {}
/* All contexts share the same handler */
static value caml_error_handler = 0;
static void error_handler_static (Z3_context c, Z3_error_code e) static void error_handler_static (Z3_context c, Z3_error_code e)
{ {
static struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL }; static struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };
@ -126,8 +129,8 @@ static void error_handler_static (Z3_context c, Z3_error_code e)
value ctx_err[2]; value ctx_err[2];
ctx_err[0] = c2ml_Z3_context(&c); ctx_err[0] = c2ml_Z3_context(&c);
ctx_err[1] = camlidl_c2ml_z3_Z3_error_code(&e, &_ctxs); ctx_err[1] = camlidl_c2ml_z3_Z3_error_code(&e, &_ctxs);
if (caml_error_handler) { if (caml_z3_error_handler) {
caml_callback2(caml_error_handler, ctx_err[0], ctx_err[1]); caml_callback2(caml_z3_error_handler, ctx_err[0], ctx_err[1]);
} else { } else {
/* if no handler set, raise OCaml Error exception */ /* if no handler set, raise OCaml Error exception */
exn_tag = caml_named_value(\"Z3.Error\"); exn_tag = caml_named_value(\"Z3.Error\");
@ -141,7 +144,7 @@ static void error_handler_static (Z3_context c, Z3_error_code e)
void ml2c_Z3_error_handler (value ml_handler, void* c_handler) void ml2c_Z3_error_handler (value ml_handler, void* c_handler)
{ {
caml_error_handler = ml_handler; caml_z3_error_handler = ml_handler;
c_handler = (void*)error_handler_static; c_handler = (void*)error_handler_static;
} }