From 6889767c9adcb4fd3e6d6be31695d3f68dfbb0c0 Mon Sep 17 00:00:00 2001
From: "Martin R. Neuhaeusser" <post@marneu.com>
Date: Tue, 19 Apr 2016 10:04:49 +0200
Subject: [PATCH 1/2] Fix bug in OCaml API where double values have been
wrapped incorrectly.
This patch fixes a segmentation fault that occurs due to incorrect
wrapping of double values in the OCaml API.
---
scripts/update_api.py | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/scripts/update_api.py b/scripts/update_api.py
index 09a10f6cf..16ec1e81e 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -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:
From 436113896d8699ca49af485285f07c1328958b23 Mon Sep 17 00:00:00 2001
From: "Martin R. Neuhaeusser" <post@marneu.com>
Date: Tue, 19 Apr 2016 12:51:16 +0200
Subject: [PATCH 2/2] Fix typo in OCaml bindings
---
scripts/update_api.py | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/scripts/update_api.py b/scripts/update_api.py
index 16ec1e81e..a06f1fbb1 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -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 ')