mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-09 07:33:24 +00:00
Code Activity

fix for OCaml API build

Browse source
This commit is contained in:
Yuto Takei 2012-11-20 13:08:40 +09:00
parent 6ae3929a92
commit dcf8291860
4 changed files with 25 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/ml/build-lib.sh Normal file → Executable file
View file

@ -3,7 +3,7 @@
# Script to compile the Z3 OCaml API # Script to compile the Z3 OCaml API
# Expects to find ../lib/libz3{,_dbg}.{a,so,dylib} # Expects to find ../lib/libz3{,_dbg}.{a,so,dylib}
CFLAGS="-ccopt -Wno-discard-qual -ccopt -I../include" CFLAGS="-ccopt -Wno-discard-qual"
XCDBG="-g -ccopt -g $CFLAGS" XCDBG="-g -ccopt -g $CFLAGS"
XCOPT="-ccopt -O3 -ccopt -fomit-frame-pointer $CFLAGS" XCOPT="-ccopt -O3 -ccopt -fomit-frame-pointer $CFLAGS"
@ -26,6 +26,6 @@ ocamlopt -a $XCDBG -cclib -L$PWD/../lib -cclib -lz3_dbg -cclib -lcamlidl -cclib
ocamlopt -a $XCOPT -cclib -L$PWD/../lib -cclib -lz3 -cclib -lcamlidl -cclib -lz3stubs z3.cmx -o z3.cmxa ocamlopt -a $XCOPT -cclib -L$PWD/../lib -cclib -lz3 -cclib -lcamlidl -cclib -lz3stubs z3.cmx -o z3.cmxa
ocamlmktop -o ocamlz3 z3.cma -cclib -L. ocamlmktop -o ocamlz3 z3.cma -ccopt -L. -cclib -lz3 -cclib -lcamlidl
rm z3.cm{o,x} *.o rm z3.cm{o,x} *.o

8
src/api/ml/z3.ml
View file

@ -1219,13 +1219,13 @@ external get_smtlib_sort : context -> int -> sort
external get_smtlib_error : context -> string external get_smtlib_error : context -> string
= "camlidl_z3_Z3_get_smtlib_error" = "camlidl_z3_Z3_get_smtlib_error"
(*
external parse_z3_string : context -> string -> ast external parse_z3_string : context -> string -> ast
= "camlidl_z3_Z3_parse_z3_string" = "camlidl_z3_Z3_parse_z3_string"
external parse_z3_file : context -> string -> ast external parse_z3_file : context -> string -> ast
= "camlidl_z3_Z3_parse_z3_file" = "camlidl_z3_Z3_parse_z3_file"
*)
external set_error : context -> error_code -> unit external set_error : context -> error_code -> unit
= "camlidl_z3_Z3_set_error" = "camlidl_z3_Z3_set_error"
@ -2930,13 +2930,13 @@ external get_smtlib_sort : context -> int -> sort
external get_smtlib_error : context -> string external get_smtlib_error : context -> string
= "camlidl_z3V3_Z3_get_smtlib_error" = "camlidl_z3V3_Z3_get_smtlib_error"
(*
external parse_z3_string : context -> string -> ast external parse_z3_string : context -> string -> ast
= "camlidl_z3_Z3_parse_z3V3_string" = "camlidl_z3_Z3_parse_z3V3_string"
external parse_z3_file : context -> string -> ast external parse_z3_file : context -> string -> ast
= "camlidl_z3_Z3_parse_z3V3_file" = "camlidl_z3_Z3_parse_z3V3_file"
*)
external get_version : unit -> int * int * int * int external get_version : unit -> int * int * int * int
= "camlidl_z3V3_Z3_get_version" = "camlidl_z3V3_Z3_get_version"

7
src/api/ml/z3.mli
View file

@ -4787,7 +4787,6 @@ external get_smtlib_sort : context -> int -> sort
external get_smtlib_error : context -> string external get_smtlib_error : context -> string
= "camlidl_z3_Z3_get_smtlib_error" = "camlidl_z3_Z3_get_smtlib_error"
*)
(** (**
Summary: \[ [ parse_z3_string c str ] \] Summary: \[ [ parse_z3_string c str ] \]
Parse the given string using the Z3 native parser. Parse the given string using the Z3 native parser.
@ -4806,7 +4805,7 @@ external parse_z3_string : context -> string -> ast
*) *)
external parse_z3_file : context -> string -> ast external parse_z3_file : context -> string -> ast
= "camlidl_z3_Z3_parse_z3_file" = "camlidl_z3_Z3_parse_z3_file"
*)
(** (**
{2 {L Error Handling}} {2 {L Error Handling}}
*) *)
@ -10198,7 +10197,7 @@ external get_smtlib_sort : context -> int -> sort
*) *)
external get_smtlib_error : context -> string external get_smtlib_error : context -> string
= "camlidl_z3V3_Z3_get_smtlib_error" = "camlidl_z3V3_Z3_get_smtlib_error"
(*
(** (**
Summary: \[ [ parse_z3_string c str ] \] Summary: \[ [ parse_z3_string c str ] \]
Parse the given string using the Z3 native parser. Parse the given string using the Z3 native parser.
@ -10217,7 +10216,7 @@ external parse_z3_string : context -> string -> ast
*) *)
external parse_z3_file : context -> string -> ast external parse_z3_file : context -> string -> ast
= "camlidl_z3_Z3_parse_z3V3_file" = "camlidl_z3_Z3_parse_z3V3_file"
*)
(** (**
{2 {L Miscellaneous}} {2 {L Miscellaneous}}
*) *)

32
src/api/ml/z3_stubs.c
View file

@ -8169,13 +8169,13 @@ check_error_code(c);
/* end user-supplied deallocation sequence */ /* end user-supplied deallocation sequence */
return _vres; return _vres;
} }
/*
value camlidl_z3_Z3_parse_z3_string( value camlidl_z3_Z3_parse_z3_string(
value _v_c, value _v_c,
value _v_str) value _v_str)
{ {
Z3_context c; /*in*/ Z3_context c; /*in
Z3_string str; /*in*/ Z3_string str; /*in
Z3_ast _res; Z3_ast _res;
value _vres; value _vres;
@ -8186,9 +8186,9 @@ value camlidl_z3_Z3_parse_z3_string(
_res = Z3_parse_z3_string(c, str); _res = Z3_parse_z3_string(c, str);
_vres = camlidl_c2ml_z3_Z3_ast(&_res, _ctx); _vres = camlidl_c2ml_z3_Z3_ast(&_res, _ctx);
camlidl_free(_ctx); camlidl_free(_ctx);
/* begin user-supplied deallocation sequence */ /* begin user-supplied deallocation sequence
check_error_code(c); check_error_code(c);
/* end user-supplied deallocation sequence */ /* end user-supplied deallocation sequence
return _vres; return _vres;
} }
@ -8196,8 +8196,8 @@ value camlidl_z3_Z3_parse_z3_file(
value _v_c, value _v_c,
value _v_file_name) value _v_file_name)
{ {
Z3_context c; /*in*/ Z3_context c; /*in
Z3_string file_name; /*in*/ Z3_string file_name; /*in
Z3_ast _res; Z3_ast _res;
value _vres; value _vres;
@ -8208,12 +8208,12 @@ value camlidl_z3_Z3_parse_z3_file(
_res = Z3_parse_z3_file(c, file_name); _res = Z3_parse_z3_file(c, file_name);
_vres = camlidl_c2ml_z3_Z3_ast(&_res, _ctx); _vres = camlidl_c2ml_z3_Z3_ast(&_res, _ctx);
camlidl_free(_ctx); camlidl_free(_ctx);
/* begin user-supplied deallocation sequence */ /* begin user-supplied deallocation sequence
check_error_code(c); check_error_code(c);
/* end user-supplied deallocation sequence */ /* end user-supplied deallocation sequence
return _vres; return _vres;
} }
*/
value camlidl_z3_Z3_set_error( value camlidl_z3_Z3_set_error(
value _v_c, value _v_c,
value _v_e) value _v_e)
@ -17569,13 +17569,13 @@ value camlidl_z3V3_Z3_get_smtlib_error(
camlidl_free(_ctx); camlidl_free(_ctx);
return _vres; return _vres;
} }
/*
value camlidl_z3_Z3_parse_z3V3_string( value camlidl_z3_Z3_parse_z3V3_string(
value _v_c, value _v_c,
value _v_str) value _v_str)
{ {
Z3_context c; /*in*/ Z3_context c; /*in
Z3_string str; /*in*/ Z3_string str; /*in
Z3_ast _res; Z3_ast _res;
value _vres; value _vres;
@ -17593,8 +17593,8 @@ value camlidl_z3_Z3_parse_z3V3_file(
value _v_c, value _v_c,
value _v_file_name) value _v_file_name)
{ {
Z3_context c; /*in*/ Z3_context c; /*in
Z3_string file_name; /*in*/ Z3_string file_name; /*in
Z3_ast _res; Z3_ast _res;
value _vres; value _vres;
@ -17607,7 +17607,7 @@ value camlidl_z3_Z3_parse_z3V3_file(
camlidl_free(_ctx); camlidl_free(_ctx);
return _vres; return _vres;
} }
*/
value camlidl_z3V3_Z3_get_version(value _unit) value camlidl_z3V3_Z3_get_version(value _unit)
{ {
unsigned int *major; /*out*/ unsigned int *major; /*out*/