mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
9bb0c882fa
when --staticlib is enabled, the linker will still choose to dynamically link upon encountering `-lz3` when generating an executable through OCaml. The interaction between the underlying C linker and OCaml make it very hard to choose the static version instead. The present patch works around this issue by copying `libz3.a` to `libz3-static.a`, and using `-lz3-static` instead: the static version is chosen since no dynamic one is found. One can get back to dynamically linking by compiling without `--staticlib`, or switching back to `-lz3`, but will in the latter case run into the same problem with specifying the option; if that needs to be made easier, we could provide two versions of the `cm(x)a` which differ only by their linking options. One last solution would be to remove `lz3` altogether from the linking options included in the cm(x)a, requiring either `-lz3` or `-lz3-static` to be specified at link time. Simpler and most flexible, but requires an update of all users that link with the Z3 ml api... |
||
|---|---|---|
| .. | ||
| mk_consts_files.py | ||
| mk_copyright.py | ||
| mk_def_file.py | ||
| mk_exception.py | ||
| mk_genfile_common.py | ||
| mk_gparams_register_modules_cpp.py | ||
| mk_install_tactic_cpp.py | ||
| mk_make.py | ||
| mk_mem_initializer_cpp.py | ||
| mk_nuget_release.py | ||
| mk_pat_db.py | ||
| mk_project.py | ||
| mk_unix_dist.py | ||
| mk_util.py | ||
| mk_win_dist.py | ||
| pyg2hpp.py | ||
| README | ||
| trackall.sh | ||
| update_api.py | ||
| update_header_guards.py | ||
| update_include.py | ||
| vsts-mac.sh | ||
| vsts-vs2013.cmd | ||
| vsts-vs2017.cmd | ||
Instructions for updating external Z3 API ----------------------------------------- The python "macros": def_Type() and def_API() are used to add new types and function definitions to the Z3 API. The .h files provided to `mk_bindings(API_files)` contain these definitions. See src\api\z3_api.h for many examples. The bindings for .Net and Python are generated when mk_make.py is invoked.