diff --git a/scripts/update_api.py b/scripts/update_api.py index 60ec37220..abd347a74 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -494,12 +494,12 @@ def mk_java(): java_native.write(' public static class IntPtr { public int value; }\n') java_native.write(' public static class LongPtr { public long value; }\n') java_native.write(' public static class StringPtr { public String value; }\n') - java_native.write(' public static class errorHandler { public long ptr; }\n') + java_native.write(' public static native void setInternalErrorHandler(long ctx);\n\n') if IS_WINDOWS: java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name) else: java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name[3:]) # We need 3: to extract the prexi 'lib' form the dll_name - java_native.write('\n\n') + java_native.write('\n') for name, result, params in _dotnet_decls: java_native.write(' protected static native %s INTERNAL%s(' % (type2java(result), java_method_name(name))) first = True @@ -553,6 +553,7 @@ def mk_java(): java_native.write(' }\n\n') java_native.write('}\n') java_wrapper = open(java_wrapperf, 'w') + pkg_str = get_component('java').package_name.replace('.', '_') java_wrapper.write('// Automatically generated file\n') java_wrapper.write('#include\n') java_wrapper.write('#include\n') @@ -578,7 +579,17 @@ def mk_java(): java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') java_wrapper.write(' delete [] NEW; \n\n') java_wrapper.write('#endif\n\n') - pkg_str = get_component('java').package_name.replace('.', '_') + java_wrapper.write('void Z3JavaErrorHandler(Z3_context c, Z3_error_code e)\n') + java_wrapper.write('{\n') + java_wrapper.write(' // Internal do-nothing error handler. This is required to avoid that Z3 calls exit()\n') + java_wrapper.write(' // upon errors, but the actual error handling is done by throwing exceptions in the\n') + java_wrapper.write(' // wrappers below.\n') + java_wrapper.write('}\n\n') + java_wrapper.write('JNIEXPORT void JNICALL Java_%s_Native_setInternalErrorHandler(JNIEnv * jenv, jclass cls, long a0)\n' % pkg_str) + java_wrapper.write('{\n') + java_wrapper.write(' Z3_set_error_handler((Z3_context)a0, Z3JavaErrorHandler);\n') + java_wrapper.write('}\n\n') + java_wrapper.write('') for name, result, params in _dotnet_decls: java_wrapper.write('JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name))) i = 0; diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 1d2f800ba..f375ab525 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -38,12 +38,11 @@ public class Context extends IDisposable InitContext(); } - private Context(long ctx, long refCount, Native.errorHandler errh) + private Context(long ctx, long refCount) { super(); this.m_ctx = ctx; this.m_refCount = refCount; - this.m_n_err_handler = errh; } /** @@ -2908,21 +2907,6 @@ public class Context extends IDisposable Native.toggleWarningMessages((enabled) ? true : false); } - // /// - // /// A delegate which is executed when an error is raised. - // /// - // /// - // /// Note that it is possible for memory leaks to occur if error handlers - // /// throw exceptions. - // /// - // public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, - // String errorString); - - // /// - // /// The OnError event. - // /// - // public event ErrorHandler OnError = null; - /** * Update a mutable configuration parameter. The list of all * configuration parameters can be obtained using the Z3 executable: @@ -2950,26 +2934,16 @@ public class Context extends IDisposable } long m_ctx = 0; - Native.errorHandler m_n_err_handler = null; long nCtx() { return m_ctx; } - // void NativeErrorHandler(long ctx, Z3_error_code errorCode) - // { - // // Do-nothing error handler. The wrappers in Z3.Native will throw - // exceptions upon errors. - // } - void InitContext() throws Z3Exception { setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT); - // m_n_err_handler = new Native.errorHandler(NativeErrorHandler); // - // keep reference so it doesn't get collected. - // if (m_n_err_handler != null) Native.setErrorHandler(m_ctx, - // m_n_err_handler); + Native.setInternalErrorHandler(nCtx()); } void CheckContextMatch(Z3Object other) throws Z3Exception @@ -3087,7 +3061,6 @@ public class Context extends IDisposable if (m_refCount == 0) { - m_n_err_handler = null; try { Native.delContext(m_ctx); @@ -3099,7 +3072,7 @@ public class Context extends IDisposable } else /* re-queue the finalizer */ /* BUG: DRQ's need to be taken over too! */ - new Context(m_ctx, m_refCount, m_n_err_handler); + new Context(m_ctx, m_refCount); } /**