Hello Guys,
I have built z3 with python3 scripts/mk_make.py --ml --prefix=/home/user/.local/bin/
I get following error in the build process.
Can anyone help me with this?
ERROR: Leftover object files:
File libz3.so in z3-4.7.1/z3rel/build has suffix .so
Exiting due to hygiene violations.
Compilation unsuccessful after building 0 targets (0 cached) in 00:00:01.
real 0m1.507s
user 0m1.437s
sys 0m0.057s
user@user-pc:~/src/VeriSmart-public$ ./_build/s
sanitize.sh src/
user@user-pc:~/src/VeriSmart-public$ ./_build/sanitize.sh
user@user-pc:~/src/VeriSmart-public$ ./build
+ ocamlfind ocamlopt -linkpkg -thread -package batteries -package str -package Z3 -package yojson -package ocamlgraph -I src/util -I src/frontend -I src/pre -I src/vlang -I src/checker -I src/exploit -I src/pre/interval -I src/verify -I src src/util/options.cmx src/util/vocab.cmx src/frontend/lang.cmx src/pre/funcMap.cmx src/pre/makeCfg.cmx src/util/profiler.cmx src/pre/path.cmx src/vlang/vlang.cmx src/checker/query.cmx src/exploit/preprocessExploit.cmx src/pre/callGraph.cmx src/pre/funcDefUse.cmx src/pre/interval/bTaint.cmx src/pre/interval/gTaint.cmx src/pre/interval/itv.cmx src/pre/interval/itvDom.cmx src/pre/structMap.cmx src/pre/global.cmx src/pre/interval/itvSem2.cmx src/pre/interval/itvAnalysis2.cmx src/verify/simplification.cmx src/vlang/semantics.cmx src/vlang/z3Interface.cmx src/checker/assertion.cmx src/verify/invMap.cmx src/verify/report.cmx src/checker/destruct.cmx src/checker/leaking.cmx src/checker/overflow.cmx src/pre/patternAnalysis.cmx src/checker/reEntrancy.cmx src/checker/collectQuery.cmx src/checker/txOrigin.cmx src/checker/collectQuery2.cmx src/exploit/transaction.cmx src/exploit/execTran.cmx src/exploit/feature.cmx src/exploit/opt.cmx src/exploit/reportExploit.cmx src/exploit/exploitUtils.cmx src/exploit/prob.cmx src/exploit/exploit.cmx src/util/json.cmx src/frontend/translator.cmx src/frontend/preprocess.cmx src/frontend/preprocess2.cmx src/pre/inline.cmx src/pre/interval/itvSem.cmx src/pre/interval/itvAnalysis.cmx src/util/solc.cmx src/verify/component.cmx src/verify/model.cmx src/verify/specMap.cmx src/verify/tactic.cmx src/verify/template.cmx src/verify/transNonLinear.cmx src/verify/transformPredicate.cmx src/verify/verifyUtils.cmx src/verify/synthesizer.cmx src/verify/verifier.cmx src/main.cmx -o src/main.native
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `Z3_simplifier_finalize':
z3native_stubs.c:(.text+0x1049): undefined reference to `Z3_simplifier_dec_ref'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `Z3_simplifier_plus_mk':
z3native_stubs.c:(.text+0x3bff): undefined reference to `Z3_simplifier_inc_ref'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_mk_type_variable':
z3native_stubs.c:(.text+0x83d8): undefined reference to `Z3_mk_type_variable'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_constructor_num_fields':
z3native_stubs.c:(.text+0xa749): undefined reference to `Z3_constructor_num_fields'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_mk_real_int64':
z3native_stubs.c:(.text+0x17fe9): undefined reference to `Z3_mk_real_int64'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_get_quantifier_skolem_id':
z3native_stubs.c:(.text+0x2b626): undefined reference to `Z3_get_quantifier_skolem_id'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_get_quantifier_id':
z3native_stubs.c:(.text+0x2b7a6): undefined reference to `Z3_get_quantifier_id'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_mk_simplifier':
z3native_stubs.c:(.text+0x36cf4): undefined reference to `Z3_mk_simplifier'
/usr/bin/ld: z3native_stubs.c:(.text+0x36d2b): undefined reference to `Z3_simplifier_inc_ref'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_simplifier_inc_ref':
z3native_stubs.c:(.text+0x36e87): undefined reference to `Z3_simplifier_inc_ref'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_simplifier_dec_ref':
z3native_stubs.c:(.text+0x36fd4): undefined reference to `Z3_simplifier_dec_ref'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_solver_add_simplifier':
z3native_stubs.c:(.text+0x37119): undefined reference to `Z3_solver_add_simplifier'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_simplifier_and_then':
z3native_stubs.c:(.text+0x372c9): undefined reference to `Z3_simplifier_and_then'
/usr/bin/ld: z3native_stubs.c:(.text+0x37300): undefined reference to `Z3_simplifier_inc_ref'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_simplifier_using_params':
z3native_stubs.c:(.text+0x37479): undefined reference to `Z3_simplifier_using_params'
/usr/bin/ld: z3native_stubs.c:(.text+0x374b0): undefined reference to `Z3_simplifier_inc_ref'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_get_num_simplifiers':
z3native_stubs.c:(.text+0x375d4): undefined reference to `Z3_get_num_simplifiers'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_get_simplifier_name':
z3native_stubs.c:(.text+0x37728): undefined reference to `Z3_get_simplifier_name'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_simplifier_get_help':
z3native_stubs.c:(.text+0x37879): undefined reference to `Z3_simplifier_get_help'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_simplifier_get_param_descrs':
z3native_stubs.c:(.text+0x379c8): undefined reference to `Z3_simplifier_get_param_descrs'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_simplifier_get_descr':
z3native_stubs.c:(.text+0x37b55): undefined reference to `Z3_simplifier_get_descr'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_rcf_is_rational':
z3native_stubs.c:(.text+0x46129): undefined reference to `Z3_rcf_is_rational'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_rcf_is_algebraic':
z3native_stubs.c:(.text+0x46289): undefined reference to `Z3_rcf_is_algebraic'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_rcf_is_infinitesimal':
z3native_stubs.c:(.text+0x463e9): undefined reference to `Z3_rcf_is_infinitesimal'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_rcf_is_transcendental':
z3native_stubs.c:(.text+0x46549): undefined reference to `Z3_rcf_is_transcendental'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_rcf_extension_index':
z3native_stubs.c:(.text+0x466a9): undefined reference to `Z3_rcf_extension_index'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_rcf_transcendental_name':
z3native_stubs.c:(.text+0x467f6): undefined reference to `Z3_rcf_transcendental_name'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_rcf_infinitesimal_name':
z3native_stubs.c:(.text+0x46976): undefined reference to `Z3_rcf_infinitesimal_name'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_rcf_num_coefficients':
z3native_stubs.c:(.text+0x46af9): undefined reference to `Z3_rcf_num_coefficients'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_rcf_coefficient':
z3native_stubs.c:(.text+0x46c66): undefined reference to `Z3_rcf_coefficient'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_rcf_interval':
z3native_stubs.c:(.text+0x46f2c): undefined reference to `Z3_rcf_interval'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_rcf_num_sign_conditions':
z3native_stubs.c:(.text+0x471e9): undefined reference to `Z3_rcf_num_sign_conditions'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_rcf_sign_condition_sign':
z3native_stubs.c:(.text+0x47359): undefined reference to `Z3_rcf_sign_condition_sign'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_rcf_num_sign_condition_coefficients':
z3native_stubs.c:(.text+0x474c9): undefined reference to `Z3_rcf_num_sign_condition_coefficients'
/usr/bin/ld: /home/user/.opam/ocaml-base-compiler/lib/Z3/libz3ml.a(z3native_stubs.o): in function `n_rcf_sign_condition_coefficient':
z3native_stubs.c:(.text+0x47663): undefined reference to `Z3_rcf_sign_condition_coefficient'
collect2: error: ld returned 1 exit status
File "caml_startup", line 1:
Error: Error during linking (exit code 1)
Command exited with code 2.
Compilation unsuccessful after building 184 targets (183 cached) in 00:00:02.
real 0m2.123s
user 0m1.857s
sys 0m0.268s
user@user-pc:~/src/VeriSmart-public$
Hello Guys,
I have built z3 with
python3 scripts/mk_make.py --ml --prefix=/home/user/.local/bin/I get following error in the build process.
Can anyone help me with this?