mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

C API: fixed mk_context/mk_context_rc exception behaviour

Browse source 
Adjusted .NET/Java APIs accordingly.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-02-08 18:54:44 +00:00
parent 2e2fa84d40
commit 91402f2060
5 changed files with 33 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
examples/java/JavaExample.java
View file

@ -2155,7 +2155,7 @@ class JavaExample
// But you cannot mix numerals of different sorts // But you cannot mix numerals of different sorts
// even if the size of their domains are the same: // even if the size of their domains are the same:
// System.out.println(ctx.mkEq(s1, t1)); // System.out.println(ctx.mkEq(s1, t1));
} }
public static void main(String[] args) public static void main(String[] args)
{ {
@ -2226,7 +2226,7 @@ class JavaExample
Context ctx = new Context(cfg); Context ctx = new Context(cfg);
p.quantifierExample3(ctx); p.quantifierExample3(ctx);
p.quantifierExample4(ctx); p.quantifierExample4(ctx);
} }
Log.close(); Log.close();
if (Log.isOpen()) if (Log.isOpen())

35
scripts/update_api.py
View file

@ -395,8 +395,7 @@ def mk_dotnet():
dotnet.write(' public delegate void Z3_error_handler(Z3_context c, Z3_error_code e);\n\n') dotnet.write(' public delegate void Z3_error_handler(Z3_context c, Z3_error_code e);\n\n')
dotnet.write(' public unsafe class LIB\n') dotnet.write(' public unsafe class LIB\n')
dotnet.write(' {\n') dotnet.write(' {\n')
dotnet.write(' ' dotnet.write(' const string Z3_DLL_NAME = \"libz3.dll\";\n'
' const string Z3_DLL_NAME = \"libz3.dll\";\n'
' \n'); ' \n');
dotnet.write(' [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n') dotnet.write(' [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n')
dotnet.write(' public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);\n\n') dotnet.write(' public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);\n\n')
@ -420,7 +419,8 @@ def mk_dotnet():
dotnet.write(' }\n') dotnet.write(' }\n')
DotnetUnwrapped = [ 'Z3_del_context' ] NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ]
Unwrapped = [ 'Z3_del_context' ]
def mk_dotnet_wrappers(): def mk_dotnet_wrappers():
global Type2Str global Type2Str
@ -469,11 +469,15 @@ def mk_dotnet_wrappers():
dotnet.write('a%d' % i) dotnet.write('a%d' % i)
i = i + 1 i = i + 1
dotnet.write(');\n'); dotnet.write(');\n');
if name not in DotnetUnwrapped: if name not in Unwrapped:
if len(params) > 0 and param_type(params[0]) == CONTEXT: if name in NULLWrapped:
dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n") dotnet.write(" if (r == IntPtr.Zero)\n")
dotnet.write(" if (err != Z3_error_code.Z3_OK)\n") dotnet.write(" throw new Z3Exception(\"Object allocation failed.\");\n")
dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n") else:
if len(params) > 0 and param_type(params[0]) == CONTEXT:
dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n")
dotnet.write(" if (err != Z3_error_code.Z3_OK)\n")
dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n")
if result == STRING: if result == STRING:
dotnet.write(" return Marshal.PtrToStringAnsi(r);\n") dotnet.write(" return Marshal.PtrToStringAnsi(r);\n")
elif result != VOID: elif result != VOID:
@ -550,7 +554,7 @@ def mk_java():
java_native.write('%s a%d' % (param2java(param), i)) java_native.write('%s a%d' % (param2java(param), i))
i = i + 1 i = i + 1
java_native.write(')') java_native.write(')')
if len(params) > 0 and param_type(params[0]) == CONTEXT: if (len(params) > 0 and param_type(params[0]) == CONTEXT) or name in NULLWrapped:
java_native.write(' throws Z3Exception') java_native.write(' throws Z3Exception')
java_native.write('\n') java_native.write('\n')
java_native.write(' {\n') java_native.write(' {\n')
@ -568,10 +572,15 @@ def mk_java():
java_native.write('a%d' % i) java_native.write('a%d' % i)
i = i + 1 i = i + 1
java_native.write(');\n') java_native.write(');\n')
if len(params) > 0 and param_type(params[0]) == CONTEXT: if name not in Unwrapped:
java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n') if name in NULLWrapped:
java_native.write(' if (err != Z3_error_code.Z3_OK)\n') java_native.write(" if (res == 0)\n")
java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n') java_native.write(" throw new Z3Exception(\"Object allocation failed.\");\n")
else:
if len(params) > 0 and param_type(params[0]) == CONTEXT:
java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n')
java_native.write(' if (err != Z3_error_code.Z3_OK)\n')
java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n')
if result != VOID: if result != VOID:
java_native.write(' return res;\n') java_native.write(' return res;\n')
java_native.write(' }\n\n') java_native.write(' }\n\n')

4
src/api/api_context.cpp
View file

@ -419,17 +419,21 @@ namespace api {
extern "C" { extern "C" {
Z3_context Z3_API Z3_mk_context(Z3_config c) { Z3_context Z3_API Z3_mk_context(Z3_config c) {
Z3_TRY;
LOG_Z3_mk_context(c); LOG_Z3_mk_context(c);
memory::initialize(UINT_MAX); memory::initialize(UINT_MAX);
Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), false)); Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), false));
RETURN_Z3(r); RETURN_Z3(r);
Z3_CATCH_RETURN_NO_HANDLE(0);
} }
Z3_context Z3_API Z3_mk_context_rc(Z3_config c) { Z3_context Z3_API Z3_mk_context_rc(Z3_config c) {
Z3_TRY;
LOG_Z3_mk_context_rc(c); LOG_Z3_mk_context_rc(c);
memory::initialize(UINT_MAX); memory::initialize(UINT_MAX);
Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), true)); Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), true));
RETURN_Z3(r); RETURN_Z3(r);
Z3_CATCH_RETURN_NO_HANDLE(0);
} }
void Z3_API Z3_del_context(Z3_context c) { void Z3_API Z3_del_context(Z3_context c) {

1
src/api/api_util.h
View file

@ -26,6 +26,7 @@ Revision History:
#define Z3_CATCH_CORE(CODE) } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); CODE } #define Z3_CATCH_CORE(CODE) } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); CODE }
#define Z3_CATCH Z3_CATCH_CORE(return;) #define Z3_CATCH Z3_CATCH_CORE(return;)
#define Z3_CATCH_RETURN(VAL) Z3_CATCH_CORE(return VAL;) #define Z3_CATCH_RETURN(VAL) Z3_CATCH_CORE(return VAL;)
#define Z3_CATCH_RETURN_NO_HANDLE(VAL) } catch (z3_exception &) { return VAL; }
#define CHECK_REF_COUNT(a) (reinterpret_cast<ast const*>(a)->get_ref_count() > 0) #define CHECK_REF_COUNT(a) (reinterpret_cast<ast const*>(a)->get_ref_count() > 0)
#define VALIDATE(a) SASSERT(!a || CHECK_REF_COUNT(a)) #define VALIDATE(a) SASSERT(!a || CHECK_REF_COUNT(a))

8
src/api/java/Context.java
View file

@ -3053,10 +3053,10 @@ public class Context extends IDisposable
// OK. // OK.
} }
m_ctx = 0; m_ctx = 0;
} else }
/* re-queue the finalizer */ /*
/* BUG: DRQ's need to be taken over too! */ else
new Context(m_ctx, m_refCount); CMW: re-queue the finalizer? */
} }
/** /**