mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

override n_mk_config in ml bindings to catch exception path

Browse source
This commit is contained in:
Nicola Mometto 2018-11-27 12:15:57 +00:00
parent 29a28f544d
commit 21158d87e3
2 changed files with 26 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -448,3 +448,21 @@ CAMLprim value DLL_PUBLIC n_set_internal_error_handler(value ctx_v)
Z3_set_error_handler(ctx_p->ctx, MLErrorHandler);
CAMLreturn(Val_unit);
}
CAMLprim DLL_PUBLIC value n_mk_config() {
CAMLparam0();
CAMLlocal1(result);
Z3_config z3rv;
/* invoke Z3 function */
z3rv = Z3_mk_config();
if (z3rv == NULL) {
caml_raise_with_string(*caml_named_value("Z3EXCEPTION"), "internal error");
}
/* construct simple return value */
result = caml_alloc_custom(&default_custom_ops, sizeof(Z3_config), 0, 1); *(Z3_config*)Data_custom_val(result) = z3rv;
/* cleanup and return */
CAMLreturn(result);
}