diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 5a5dbc3a4..4082bb2b8 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1351,10 +1351,14 @@ class MLComponent(Component): api_src = get_component(API_COMPONENT).to_src_dir for f in filter(lambda f: f.endswith('.ml'), os.listdir(self.src_dir)): out.write('%s/%s: %s/%s\n' % (sub_dir,f,src_dir,f)) - out.write('\t%s %s/%s %s/%s\n' % (CP_CMD,src_dir,f,sub_dir,f)) + str = '\t%s %s/%s %s/%s\n' % (CP_CMD,src_dir,f,sub_dir,f) + if IS_WINDOWS: str = str.replace('/','\\') + out.write(str) for f in filter(lambda f: f.endswith('.c'), os.listdir(self.src_dir)): out.write('%s/%s: %s/%s\n' % (sub_dir,f,src_dir,f)) - out.write('\t%s %s/%s %s/%s\n' % (CP_CMD,src_dir,f,sub_dir,f)) + str = '\t%s %s/%s %s/%s\n' % (CP_CMD,src_dir,f,sub_dir,f) + if IS_WINDOWS: str = str.replace('/','\\') + out.write(str) modules = ["z3enums", "z3native", "z3"] # dependencies in this order! prev = '' for m in modules: diff --git a/scripts/update_api.py b/scripts/update_api.py index 6e9c14355..e5c66dd39 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1169,9 +1169,11 @@ def mk_ml(): ml_i.write('\n') ml_native.write('external is_null : ptr -> bool\n = "n_is_null"\n\n') ml_native.write('external mk_null : unit -> ptr\n = "n_mk_null"\n\n') + ml_native.write('external set_internal_error_handler : ptr -> unit\n = "n_set_internal_error_handler"\n\n') ml_native.write('exception Exception of string\n\n') ml_i.write('val is_null : ptr -> bool\n') ml_i.write('val mk_null : unit -> ptr\n') + ml_i.write('val set_internal_error_handler : ptr -> unit\n\n') ml_i.write('exception Exception of string\n\n') # ML declarations @@ -1329,6 +1331,16 @@ def mk_ml(): ml_wrapper.write(' memcpy( Data_custom_val(result), &z3_result, sizeof(void*));\n') ml_wrapper.write(' CAMLreturn (result);\n') ml_wrapper.write('}\n\n') + ml_wrapper.write('void MLErrorHandler(Z3_context c, Z3_error_code e)\n') + ml_wrapper.write('{\n') + ml_wrapper.write(' // Internal do-nothing error handler. This is required to avoid that Z3 calls exit()\n') + ml_wrapper.write(' // upon errors, but the actual error handling is done by throwing exceptions in the\n') + ml_wrapper.write(' // wrappers below.\n') + ml_wrapper.write('}\n\n') + ml_wrapper.write('void n_set_internal_error_handler(Z3_context c)\n') + ml_wrapper.write('{\n') + ml_wrapper.write(' Z3_set_error_handler(c, MLErrorHandler);\n') + ml_wrapper.write('}\n\n') for name, result, params in _dotnet_decls: ip = inparams(params) op = outparams(params) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 651102bc8..45faae468 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -135,16 +135,12 @@ struct let v = Z3native.mk_context_rc cfg in Z3native.del_config(cfg) ; Z3native.set_ast_print_mode v (int_of_ast_print_mode PRINT_SMTLIB2_COMPLIANT) ; + Z3native.set_internal_error_handler v ; (* Printf.printf "Installing finalizer on context \n" ; *) let res = { m_n_ctx = v; m_n_obj_cnt = 0 } in let f = fun o -> dispose_context o in Gc.finalise f res; res - (* CMW: Install error handler here! - m_n_err_handler = new Z3native.error_handler(NativeErrorHandler); keep reference so it doesn't get collected. - Z3native.set_error_handler(m_ctx, m_n_err_handler); - GC.SuppressFinalize(this); - *) let context_add1 ctx = ignore (ctx.m_n_obj_cnt = ctx.m_n_obj_cnt + 1) let context_sub1 ctx = ignore (ctx.m_n_obj_cnt = ctx.m_n_obj_cnt - 1)