mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 00:55:31 +00:00
ML API: Build system and error handling fixes.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
fd2ae5f60e
commit
09aa02759f
3 changed files with 19 additions and 7 deletions
|
@ -1341,10 +1341,14 @@ class MLComponent(Component):
|
|||
api_src = get_component(API_COMPONENT).to_src_dir
|
||||
for f in filter(lambda f: f.endswith('.ml'), os.listdir(self.src_dir)):
|
||||
out.write('%s/%s: %s/%s\n' % (sub_dir,f,src_dir,f))
|
||||
out.write('\t%s %s/%s %s/%s\n' % (CP_CMD,src_dir,f,sub_dir,f))
|
||||
str = '\t%s %s/%s %s/%s\n' % (CP_CMD,src_dir,f,sub_dir,f)
|
||||
if IS_WINDOWS: str = str.replace('/','\\')
|
||||
out.write(str)
|
||||
for f in filter(lambda f: f.endswith('.c'), os.listdir(self.src_dir)):
|
||||
out.write('%s/%s: %s/%s\n' % (sub_dir,f,src_dir,f))
|
||||
out.write('\t%s %s/%s %s/%s\n' % (CP_CMD,src_dir,f,sub_dir,f))
|
||||
str = '\t%s %s/%s %s/%s\n' % (CP_CMD,src_dir,f,sub_dir,f)
|
||||
if IS_WINDOWS: str = str.replace('/','\\')
|
||||
out.write(str)
|
||||
modules = ["z3enums", "z3native", "z3"] # dependencies in this order!
|
||||
prev = ''
|
||||
for m in modules:
|
||||
|
|
|
@ -1169,9 +1169,11 @@ def mk_ml():
|
|||
ml_i.write('\n')
|
||||
ml_native.write('external is_null : ptr -> bool\n = "n_is_null"\n\n')
|
||||
ml_native.write('external mk_null : unit -> ptr\n = "n_mk_null"\n\n')
|
||||
ml_native.write('external set_internal_error_handler : ptr -> unit\n = "n_set_internal_error_handler"\n\n')
|
||||
ml_native.write('exception Exception of string\n\n')
|
||||
ml_i.write('val is_null : ptr -> bool\n')
|
||||
ml_i.write('val mk_null : unit -> ptr\n')
|
||||
ml_i.write('val set_internal_error_handler : ptr -> unit\n\n')
|
||||
ml_i.write('exception Exception of string\n\n')
|
||||
|
||||
# ML declarations
|
||||
|
@ -1329,6 +1331,16 @@ def mk_ml():
|
|||
ml_wrapper.write(' memcpy( Data_custom_val(result), &z3_result, sizeof(void*));\n')
|
||||
ml_wrapper.write(' CAMLreturn (result);\n')
|
||||
ml_wrapper.write('}\n\n')
|
||||
ml_wrapper.write('void MLErrorHandler(Z3_context c, Z3_error_code e)\n')
|
||||
ml_wrapper.write('{\n')
|
||||
ml_wrapper.write(' // Internal do-nothing error handler. This is required to avoid that Z3 calls exit()\n')
|
||||
ml_wrapper.write(' // upon errors, but the actual error handling is done by throwing exceptions in the\n')
|
||||
ml_wrapper.write(' // wrappers below.\n')
|
||||
ml_wrapper.write('}\n\n')
|
||||
ml_wrapper.write('void n_set_internal_error_handler(Z3_context c)\n')
|
||||
ml_wrapper.write('{\n')
|
||||
ml_wrapper.write(' Z3_set_error_handler(c, MLErrorHandler);\n')
|
||||
ml_wrapper.write('}\n\n')
|
||||
for name, result, params in _dotnet_decls:
|
||||
ip = inparams(params)
|
||||
op = outparams(params)
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue