mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 05:11:21 +00:00
Code Activity

Merge pull request #1969 from Bronsa/master

Browse source 
Catch and print exceptions in Z3_mk_config
This commit is contained in:
Nikolaj Bjorner 2018-11-27 10:43:43 -08:00 • committed by GitHub
commit c5f280ae6e
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 37 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
scripts/update_api.py
View file

@ -1335,6 +1335,10 @@ z3_long_funs = frozenset([
'Z3_simplify_ex', 'Z3_simplify_ex',
]) ])
z3_ml_overrides = frozenset([
'Z3_mk_config'
])
def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface
ml_wrapperf = os.path.join(ml_output_dir, 'z3native_stubs.c') ml_wrapperf = os.path.join(ml_output_dir, 'z3native_stubs.c')
ml_wrapper = open(ml_wrapperf, 'w') ml_wrapper = open(ml_wrapperf, 'w')
@ -1346,6 +1350,10 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface
ml_pref.close() ml_pref.close()
for name, result, params in _dotnet_decls: for name, result, params in _dotnet_decls:
if name in z3_ml_overrides:
continue
ip = inparams(params) ip = inparams(params)
op = outparams(params) op = outparams(params)
ap = arrayparams(params) ap = arrayparams(params)

15
src/api/api_config_params.cpp
View file

@ -68,10 +68,17 @@ extern "C" {
} }
Z3_config Z3_API Z3_mk_config(void) { Z3_config Z3_API Z3_mk_config(void) {
memory::initialize(UINT_MAX); try {
LOG_Z3_mk_config(); memory::initialize(UINT_MAX);
Z3_config r = reinterpret_cast<Z3_config>(alloc(context_params)); LOG_Z3_mk_config();
RETURN_Z3(r); Z3_config r = reinterpret_cast<Z3_config>(alloc(context_params));
RETURN_Z3(r);
} catch (z3_exception & ex) {
// The error handler is only available for contexts
// Just throw a warning.
warning_msg("%s", ex.msg());
return nullptr;
}
} }
void Z3_API Z3_del_config(Z3_config c) { void Z3_API Z3_del_config(Z3_config c) {

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); Z3_set_error_handler(ctx_p->ctx, MLErrorHandler);
CAMLreturn(Val_unit); 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);
}