mirror of
https://github.com/Z3Prover/z3
synced 2025-06-11 00:23:25 +00:00
Make C-layer of OCaml bindings C89 compatible.
This patch ensures that the C code generated for the OCaml stubs complies with C89. It is needed to compile Z3 with OCaml support with Visual Studio versions older than VS2013.
This commit is contained in:
martin-neuhaeusser
parent
19f98547f7
commit
f069b1c0e9
2 changed files with 69 additions and 24 deletions
|
|
@ -1324,36 +1324,80 @@ def mk_z3native_stubs_c(ml_dir): # C interface
|
||||||
if len(ap) > 0:
|
if len(ap) > 0:
|
||||||
ml_wrapper.write(' unsigned _i;\n')
|
ml_wrapper.write(' unsigned _i;\n')
|
||||||
|
|
||||||
# declare locals, preprocess arrays, strings, in/out arguments
|
# determine if the function has a context as parameter.
|
||||||
have_context = False
|
have_context = (len(params) > 0) and (param_type(params[0]) == CONTEXT)
|
||||||
|
|
||||||
|
if have_context and name not in Unwrapped:
|
||||||
|
ml_wrapper.write(' Z3_error_code ec;\n')
|
||||||
|
|
||||||
|
if result != VOID:
|
||||||
|
ts = type2str(result)
|
||||||
|
if ml_has_plus_type(ts):
|
||||||
|
pts = ml_plus_type(ts)
|
||||||
|
ml_wrapper.write(' %s z3rv_m;\n' % ts)
|
||||||
|
ml_wrapper.write(' %s z3rv;\n' % pts)
|
||||||
|
else:
|
||||||
|
ml_wrapper.write(' %s z3rv;\n' % ts)
|
||||||
|
|
||||||
|
# declare all required local variables
|
||||||
|
# To comply with C89, we need to first declare the variables and initialize them
|
||||||
|
# only afterwards.
|
||||||
i = 0
|
i = 0
|
||||||
for param in params:
|
for param in params:
|
||||||
if param_type(param) == CONTEXT and i == 0:
|
if param_type(param) == CONTEXT and i == 0:
|
||||||
ml_wrapper.write(' Z3_context_plus ctx_p = *(Z3_context_plus*) Data_custom_val(a' + str(i) + ');\n')
|
ml_wrapper.write(' Z3_context_plus ctx_p;\n')
|
||||||
ml_wrapper.write(' Z3_context _a0 = ctx_p->ctx;\n')
|
ml_wrapper.write(' Z3_context _a0;\n')
|
||||||
have_context = True
|
|
||||||
else:
|
else:
|
||||||
k = param_kind(param)
|
k = param_kind(param)
|
||||||
if k == OUT_ARRAY:
|
if k == OUT_ARRAY:
|
||||||
ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * (_a%s));\n' % (
|
ml_wrapper.write(' %s * _a%s;\n' % (type2str(param_type(param)), i))
|
||||||
type2str(param_type(param)),
|
elif k == OUT_MANAGED_ARRAY:
|
||||||
|
ml_wrapper.write(' %s * _a%s;\n' % (type2str(param_type(param)), i))
|
||||||
|
elif k == IN_ARRAY or k == INOUT_ARRAY:
|
||||||
|
t = param_type(param)
|
||||||
|
ts = type2str(t)
|
||||||
|
ml_wrapper.write(' %s * _a%s;\n' % (ts, i))
|
||||||
|
elif k == IN:
|
||||||
|
t = param_type(param)
|
||||||
|
ml_wrapper.write(' %s _a%s;\n' % (type2str(t), i))
|
||||||
|
elif k == OUT or k == INOUT:
|
||||||
|
t = param_type(param)
|
||||||
|
ml_wrapper.write(' %s _a%s;\n' % (type2str(t), i))
|
||||||
|
ts = type2str(t)
|
||||||
|
if ml_has_plus_type(ts):
|
||||||
|
pts = ml_plus_type(ts)
|
||||||
|
ml_wrapper.write(' %s _a%dp;\n' % (pts, i))
|
||||||
|
i = i + 1
|
||||||
|
|
||||||
|
|
||||||
|
# End of variable declarations in outermost block:
|
||||||
|
# To comply with C89, no variable declarations may occur in the outermost block
|
||||||
|
# from that point onwards (breaks builds with at least VC 2012 and prior)
|
||||||
|
ml_wrapper.write('\n')
|
||||||
|
|
||||||
|
# Declare locals, preprocess arrays, strings, in/out arguments
|
||||||
|
i = 0
|
||||||
|
for param in params:
|
||||||
|
if param_type(param) == CONTEXT and i == 0:
|
||||||
|
ml_wrapper.write(' ctx_p = *(Z3_context_plus*) Data_custom_val(a' + str(i) + ');\n')
|
||||||
|
ml_wrapper.write(' _a0 = ctx_p->ctx;\n')
|
||||||
|
else:
|
||||||
|
k = param_kind(param)
|
||||||
|
if k == OUT_ARRAY:
|
||||||
|
ml_wrapper.write(' _a%s = (%s*) malloc(sizeof(%s) * (_a%s));\n' % (
|
||||||
i,
|
i,
|
||||||
type2str(param_type(param)),
|
type2str(param_type(param)),
|
||||||
type2str(param_type(param)),
|
type2str(param_type(param)),
|
||||||
param_array_capacity_pos(param)))
|
param_array_capacity_pos(param)))
|
||||||
elif k == OUT_MANAGED_ARRAY:
|
elif k == OUT_MANAGED_ARRAY:
|
||||||
ml_wrapper.write(' %s * _a%s = 0;\n' % (type2str(param_type(param)), i))
|
ml_wrapper.write(' _a%s = 0;\n' % i)
|
||||||
elif k == IN_ARRAY or k == INOUT_ARRAY:
|
elif k == IN_ARRAY or k == INOUT_ARRAY:
|
||||||
t = param_type(param)
|
t = param_type(param)
|
||||||
ts = type2str(t)
|
ts = type2str(t)
|
||||||
ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * _a%s);\n' % (ts, i, ts, ts, param_array_capacity_pos(param)))
|
ml_wrapper.write(' _a%s = (%s*) malloc(sizeof(%s) * _a%s);\n' % (i, ts, ts, param_array_capacity_pos(param)))
|
||||||
elif k == IN:
|
elif k == IN:
|
||||||
t = param_type(param)
|
t = param_type(param)
|
||||||
ml_wrapper.write(' %s _a%s = %s;\n' % (type2str(t), i, ml_unwrap(t, type2str(t), 'a' + str(i))))
|
ml_wrapper.write(' _a%s = %s;\n' % (i, ml_unwrap(t, type2str(t), 'a' + str(i))))
|
||||||
elif k == OUT:
|
|
||||||
ml_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i))
|
|
||||||
elif k == INOUT:
|
|
||||||
ml_wrapper.write(' %s _a%s = a%s;\n' % (type2str(param_type(param)), i, i))
|
|
||||||
i = i + 1
|
i = i + 1
|
||||||
|
|
||||||
i = 0
|
i = 0
|
||||||
|
|
@ -1375,9 +1419,9 @@ def mk_z3native_stubs_c(ml_dir): # C interface
|
||||||
if result != VOID:
|
if result != VOID:
|
||||||
ts = type2str(result)
|
ts = type2str(result)
|
||||||
if ml_has_plus_type(ts):
|
if ml_has_plus_type(ts):
|
||||||
ml_wrapper.write('%s z3rv_m = ' % ts)
|
ml_wrapper.write('z3rv_m = ')
|
||||||
else:
|
else:
|
||||||
ml_wrapper.write('%s z3rv = ' % ts)
|
ml_wrapper.write('z3rv = ')
|
||||||
|
|
||||||
# invoke procedure
|
# invoke procedure
|
||||||
ml_wrapper.write('%s(' % name)
|
ml_wrapper.write('%s(' % name)
|
||||||
|
|
@ -1397,8 +1441,8 @@ def mk_z3native_stubs_c(ml_dir): # C interface
|
||||||
ml_wrapper.write(');\n')
|
ml_wrapper.write(');\n')
|
||||||
|
|
||||||
if have_context and name not in Unwrapped:
|
if have_context and name not in Unwrapped:
|
||||||
ml_wrapper.write(' int ec = Z3_get_error_code(ctx_p->ctx);\n')
|
ml_wrapper.write(' ec = Z3_get_error_code(ctx_p->ctx);\n')
|
||||||
ml_wrapper.write(' if (ec != 0) {\n')
|
ml_wrapper.write(' if (ec != Z3_OK) {\n')
|
||||||
ml_wrapper.write(' const char * msg = Z3_get_error_msg(ctx_p->ctx, ec);\n')
|
ml_wrapper.write(' const char * msg = Z3_get_error_msg(ctx_p->ctx, ec);\n')
|
||||||
ml_wrapper.write(' caml_raise_with_string(*caml_named_value("Z3EXCEPTION"), msg);\n')
|
ml_wrapper.write(' caml_raise_with_string(*caml_named_value("Z3EXCEPTION"), msg);\n')
|
||||||
ml_wrapper.write(' }\n')
|
ml_wrapper.write(' }\n')
|
||||||
|
|
@ -1408,9 +1452,9 @@ def mk_z3native_stubs_c(ml_dir): # C interface
|
||||||
if ml_has_plus_type(ts):
|
if ml_has_plus_type(ts):
|
||||||
pts = ml_plus_type(ts)
|
pts = ml_plus_type(ts)
|
||||||
if name in NULLWrapped:
|
if name in NULLWrapped:
|
||||||
ml_wrapper.write(' %s z3rv = %s_mk(z3rv_m);\n' % (pts, pts))
|
ml_wrapper.write(' z3rv = %s_mk(z3rv_m);\n' % pts)
|
||||||
else:
|
else:
|
||||||
ml_wrapper.write(' %s z3rv = %s_mk(ctx_p, (%s) z3rv_m);\n' % (pts, pts, ml_minus_type(ts)))
|
ml_wrapper.write(' z3rv = %s_mk(ctx_p, (%s) z3rv_m);\n' % (pts, ml_minus_type(ts)))
|
||||||
|
|
||||||
# convert output params
|
# convert output params
|
||||||
if len(op) > 0:
|
if len(op) > 0:
|
||||||
|
|
@ -1450,7 +1494,7 @@ def mk_z3native_stubs_c(ml_dir): # C interface
|
||||||
elif is_out_param(p):
|
elif is_out_param(p):
|
||||||
if ml_has_plus_type(ts):
|
if ml_has_plus_type(ts):
|
||||||
pts = ml_plus_type(ts)
|
pts = ml_plus_type(ts)
|
||||||
ml_wrapper.write(' %s _a%dp = %s_mk(ctx_p, (%s) _a%d);\n' % (pts, i, pts, ml_minus_type(ts), i))
|
ml_wrapper.write(' _a%dp = %s_mk(ctx_p, (%s) _a%d);\n' % (i, pts, ml_minus_type(ts), i))
|
||||||
ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, '_a%d_val' % i, '_a%dp' % i))
|
ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, '_a%d_val' % i, '_a%dp' % i))
|
||||||
else:
|
else:
|
||||||
ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, '_a%d_val' % i, '_a%d' % i))
|
ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, '_a%d_val' % i, '_a%d' % i))
|
||||||
|
|
|
||||||
|
|
@ -227,6 +227,7 @@ void Z3_ast_finalize(value v) {
|
||||||
int Z3_ast_compare(value v1, value v2) {
|
int Z3_ast_compare(value v1, value v2) {
|
||||||
Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1);
|
Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1);
|
||||||
Z3_ast_plus * a2 = (Z3_ast_plus*)Data_custom_val(v2);
|
Z3_ast_plus * a2 = (Z3_ast_plus*)Data_custom_val(v2);
|
||||||
|
unsigned id1, id2;
|
||||||
|
|
||||||
/* if the two ASTs belong to different contexts, we take
|
/* if the two ASTs belong to different contexts, we take
|
||||||
their contexts' addresses to order them (arbitrarily, but fixed) */
|
their contexts' addresses to order them (arbitrarily, but fixed) */
|
||||||
|
|
@ -242,8 +243,8 @@ int Z3_ast_compare(value v1, value v2) {
|
||||||
return +1;
|
return +1;
|
||||||
|
|
||||||
/* Comparison according to AST ids. */
|
/* Comparison according to AST ids. */
|
||||||
unsigned id1 = Z3_get_ast_id(a1->cp->ctx, a1->p);
|
id1 = Z3_get_ast_id(a1->cp->ctx, a1->p);
|
||||||
unsigned id2 = Z3_get_ast_id(a2->cp->ctx, a2->p);
|
id2 = Z3_get_ast_id(a2->cp->ctx, a2->p);
|
||||||
if (id1 == id2)
|
if (id1 == id2)
|
||||||
return 0;
|
return 0;
|
||||||
else if (id1 < id2)
|
else if (id1 < id2)
|
||||||
|
|
@ -255,7 +256,7 @@ int Z3_ast_compare(value v1, value v2) {
|
||||||
int Z3_ast_compare_ext(value v1, value v2) {
|
int Z3_ast_compare_ext(value v1, value v2) {
|
||||||
Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1);
|
Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1);
|
||||||
unsigned id1;
|
unsigned id1;
|
||||||
int id2 = Val_int(v2);
|
unsigned id2 = (unsigned)Val_int(v2);
|
||||||
if (a1->p == NULL && id2 == 0)
|
if (a1->p == NULL && id2 == 0)
|
||||||
return 0;
|
return 0;
|
||||||
if (a1->p == NULL)
|
if (a1->p == NULL)
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue