mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

ML API bug fixes

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-02-15 12:54:05 +00:00
parent 18c0a3bfaf
commit 62cae4186b
2 changed files with 15 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

6
scripts/update_api.py
View file

@ -1456,11 +1456,11 @@ def mk_z3native_stubs_c(ml_dir): # C interface
ml_wrapper.write(' ') ml_wrapper.write(' ')
if result != VOID: if result != VOID:
ts = type2str(result) ts = type2str(result)
ml_wrapper.write('result = caml_alloc(%s, 0);\n' % ret_size)
if ml_has_plus_type(ts): if ml_has_plus_type(ts):
ml_wrapper.write(' %s z3rv_m = ' % ts) ml_wrapper.write('%s z3rv_m = ' % ts)
else: else:
ml_wrapper.write(' %s z3rv = ' % ts) ml_wrapper.write('result = caml_alloc(%s, 0);\n ' % ret_size)
ml_wrapper.write('%s z3rv = ' % ts)
elif len(op) != 0: elif len(op) != 0:
ml_wrapper.write('result = caml_alloc(%s, 0);\n ' % ret_size) ml_wrapper.write('result = caml_alloc(%s, 0);\n ' % ret_size)

22
src/api/ml/z3native_stubs.c.pre
View file

@ -79,14 +79,14 @@ static struct custom_operations default_custom_ops = {
typedef struct { typedef struct {
Z3_context ctx; Z3_context ctx;
unsigned long ast_count; unsigned long obj_count;
} Z3_context_plus; } Z3_context_plus;
Z3_context_plus Z3_context_plus_mk(Z3_context c) { Z3_context_plus Z3_context_plus_mk(Z3_context c) {
Z3_context_plus r; Z3_context_plus r;
r.ctx = c; r.ctx = c;
r.ast_count = 0; r.obj_count = 0;
printf("ctx++\n"); //printf("ctx++\n");
return r; return r;
} }
@ -96,8 +96,8 @@ Z3_context Z3_context_plus_raw(Z3_context_plus * cp) {
void Z3_context_finalize(value v) { void Z3_context_finalize(value v) {
Z3_context_plus * cp = (Z3_context_plus*)Data_custom_val(v); Z3_context_plus * cp = (Z3_context_plus*)Data_custom_val(v);
printf("ctx--; cnt=%lu\n", cp->ast_count); // printf("ctx--; cnt=%lu\n", cp->obj_count);
if (cp->ast_count == 0) if (cp->obj_count == 0)
Z3_del_context(cp->ctx); Z3_del_context(cp->ctx);
else else
printf("Leaking the context; context_plus pointers now invalid. \n"); printf("Leaking the context; context_plus pointers now invalid. \n");
@ -122,7 +122,7 @@ typedef struct {
} Z3_symbol_plus; } Z3_symbol_plus;
Z3_symbol_plus Z3_symbol_plus_mk(Z3_context_plus * cp, Z3_symbol s) { Z3_symbol_plus Z3_symbol_plus_mk(Z3_context_plus * cp, Z3_symbol s) {
Z3_symbol_plus r; Z3_symbol_plus r;
r.cp = cp; r.cp = cp;
r.s = s; r.s = s;
return r; return r;
@ -156,9 +156,9 @@ Z3_ast_plus Z3_ast_plus_mk(Z3_context_plus * cp, Z3_ast a) {
Z3_ast_plus r; Z3_ast_plus r;
r.cp = cp; r.cp = cp;
r.a = a; r.a = a;
printf("++\n"); //printf("++\n");
cp->obj_count++;
Z3_inc_ref(cp->ctx, a); Z3_inc_ref(cp->ctx, a);
cp->ast_count++;
return r; return r;
} }
@ -167,10 +167,10 @@ Z3_ast Z3_ast_plus_raw(Z3_ast_plus * ap) {
} }
void Z3_ast_finalize(value v) { void Z3_ast_finalize(value v) {
printf("--\n"); //printf("--\n");
Z3_ast_plus * ap = (Z3_ast_plus*)(Data_custom_val(v)); Z3_ast_plus * ap = (Z3_ast_plus*)(Data_custom_val(v));
Z3_dec_ref(ap->cp->ctx, ap->a); Z3_dec_ref(ap->cp->ctx, ap->a);
ap->cp->ast_count--; ap->cp->obj_count--;
} }
int Z3_ast_compare(value v1, value v2) { int Z3_ast_compare(value v1, value v2) {
@ -321,6 +321,7 @@ MK_CTX_OF(rcf_num)
Z3_ ## X ## _plus r; \ Z3_ ## X ## _plus r; \
r.cp = cp; \ r.cp = cp; \
r.p = p; \ r.p = p; \
r.cp->obj_count++; \
Z3_ ## X ## _inc_ref(cp->ctx, p); \ Z3_ ## X ## _inc_ref(cp->ctx, p); \
return r; \ return r; \
} \ } \
@ -332,6 +333,7 @@ MK_CTX_OF(rcf_num)
void Z3_ ## X ## _finalize(value v) { \ void Z3_ ## X ## _finalize(value v) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \ Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \
Z3_ ## X ## _dec_ref(pp->cp->ctx, pp->p); \ Z3_ ## X ## _dec_ref(pp->cp->ctx, pp->p); \
pp->cp->obj_count--; \
} \ } \
\ \
static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \ static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \