mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Merge pull request #5 from martin-neuhaeusser/cwinter

Browse source 
Fix bug in OCaml API where double values have been wrapped incorrectly.
This commit is contained in:
Christoph M. Wintersteiger 2016-05-03 11:45:36 +01:00
parent 1b9a1d5c64 436113896d
commit 126e44dbd8
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
scripts/update_api.py
View file

@ -1179,7 +1179,7 @@ def ml_set_wrap(t, d, n):
elif t == INT64 or t == UINT64:
return d + ' = Val_long(' + n + ');'
elif t == DOUBLE:
return 'Store_double_val(' + d + ', ' + n + ');'
return d + '= caml_copy_double(' + n + ');'
elif t == STRING:
return d + ' = caml_copy_string((const char*) ' + n + ');'
else:
@ -1364,11 +1364,11 @@ def mk_z3native_stubs_c(ml_dir): # C interface
ts = type2str(t)
ml_wrapper.write(' _iter = a' + str(i) + ';\n')
ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) {\n' % param_array_capacity_pos(param))
ml_wrapper.write(' assert(iter != Val_emptylist);\n')
ml_wrapper.write(' assert(_iter != Val_emptylist);\n')
ml_wrapper.write(' _a%s[_i] = %s;\n' % (i, ml_unwrap(t, ts, 'Field(_iter, 0)')))
ml_wrapper.write(' _iter = Field(_iter, 1);\n')
ml_wrapper.write(' }\n')
ml_wrapper.write(' assert(iter == Val_emptylist);\n\n')
ml_wrapper.write(' assert(_iter == Val_emptylist);\n\n')
i = i + 1
ml_wrapper.write('\n /* invoke Z3 function */\n ')