=> Bootstrap dependency digest>=20211023: found digest-20220214 ===> Skipping vulnerability checks. WARNING: No /usr/pkg/pkgdb/pkg-vulnerabilities file found. WARNING: To fix run: `/usr/sbin/pkg_admin -K /usr/pkg/pkgdb fetch-pkg-vulnerabilities'. ===> Building for spark2014-14-14.2.0nb1 # Produce Ada code that stores the reserved keywords of Why3 /usr/pkg/bin/gmake -f Makefile.gnatprove build PROD=-XBuild=Production /usr/pkg/bin/gmake -C why3 -j # This script should be run *ONLY* in developer build not in prod gmake[1]: Entering directory '/pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/why3' gmake[1]: warning: -j0 forced in submake: resetting jobserver mode. gmake[1]: Entering directory '/pbulk/work/lang/spark2014-14/work/spark2014-fsf-14' gprbuild -p -j0 -P gnatprove.gpr -XBuild=Production -eL -R -cargs -O2 -I/usr/pkg/include -I/usr/include -I/usr/pkg/gcc14-gnat/include -I/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/include -I/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adainclude -largs -Wl,-R'$ORIGIN' -L/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0 -Wl,-R/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0 -L/usr/pkg/gcc14-gnat/lib -Wl,-R/usr/pkg/gcc14-gnat/lib -Wl,-zrelro -L/usr/pkg/lib -Wl,-R/usr/pkg/lib -L/usr/lib -Wl,-R/usr/lib -L/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib -gargs # (gnat2why-nightly) python3 scripts/why3keywords.py why3/src/core/keywords.ml src/why/why-keywords.adb Ocamldep src/gnat/gnat_util.ml Ocamldep src/gnat/gnat_counterexamples.ml Ocamldep src/gnat/gnat_loc.ml Ocamldep src/gnat/gnat_expl.ml Ocamldep src/gnat/gnat_config.ml Ocamldep src/gnat/gnat_scheduler.ml Ocamldep src/gnat/gnat_manual.ml Ocamldep src/gnat/gnat_report.ml Ocamldep src/gnat/gnat_objectives.ml /usr/pkg/bin/gmake -C gnat2why AUTOMATED=1 GPRARGS=-XBuild=Production gmake[1]: Entering directory '/pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/gnat2why' Ocamldep src/gnat/gnat_main.ml cmp -s src/util/mysexplib-real.ml src/util/mysexplib.ml || cp src/util/mysexplib-real.ml src/util/mysexplib.ml Ocamllex src/util/rc.mll Generate src/util/config.ml cmp -s src/util/mlmpfr_dummy.ml src/util/mlmpfr_wrapper.ml || cp src/util/mlmpfr_dummy.ml src/util/mlmpfr_wrapper.ml Ocamllex src/util/json_lexer.mll Menhir src/util/json_parser.mly Ocamllex src/util/lexlib.mll 48 states, 1889 transitions, table size 7844 bytes 3073 additional bytes used for bindings Ocamllex src/parser/lexer.mll Menhir src/parser/parser_common.mly Menhir src/parser/parser_common.mly src/parser/parser.mly 39 states, 600 transitions, table size 2634 bytes 1338 additional bytes used for bindings 52 states, 495 transitions, table size 2292 bytes cmp -s src/session/compress_none.ml src/session/compress.ml || cp src/session/compress_none.ml src/session/compress.ml Menhir src/driver/driver_parser.mly Ocamllex src/driver/sexp.mll Ocamllex src/driver/driver_lexer.mll /usr/pkg/bin/gmake -C ../src/why/xgen gmake[2]: Entering directory '/pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/src/why/xgen' gprbuild -j0 -p -Phelpers xtree cmp -s src/util/recompat.ml src/util/re.ml || cp src/util/recompat.ml src/util/re.ml Ocamllex src/session/xml.mll Ocamllex src/session/strategy_parser.mll 27 states, 306 transitions, table size 1386 bytes 34 states, 1366 transitions, table size 5668 bytes 174 states, 4831 transitions, table size 20368 bytes 9859 additional bytes used for bindings Menhir plugins/tptp/tptp_parser.mly 59 states, 799 transitions, table size 3550 bytes 2611 additional bytes used for bindings 117 states, 1396 transitions, table size 6286 bytes 3556 additional bytes used for bindings Ocamllex plugins/tptp/tptp_lexer.mll Menhir plugins/python/py_parser.mly Menhir plugins/microc/mc_parser.mly Ocamllex plugins/python/py_lexer.mll Ocamllex plugins/microc/mc_lexer.mll 101 states, 1563 transitions, table size 6858 bytes 3126 additional bytes used for bindings 69 states, 1256 transitions, table size 5438 bytes 1453 additional bytes used for bindings Ocamllex plugins/cfg/cfg_lexer.mll 77 states, 473 transitions, table size 2354 bytes 1504 additional bytes used for bindings Menhir src/parser/parser_common.mly plugins/cfg/cfg_parser.mly Ocamllex plugins/parser/dimacs.mll Ocamllex plugins/ada_terms/ada_lexer.mll Menhir plugins/ada_terms/ada_parser.mly 34 states, 434 transitions, table size 1940 bytes 1293 additional bytes used for bindings 157 states, 3909 transitions, table size 16578 bytes 9757 additional bytes used for bindings Ocamllex src/tools/why3wc.mll 173 states, 4796 transitions, table size 20222 bytes 9853 additional bytes used for bindings Ocamldep src/ide/wserver.ml Ocamldep src/why3session/why3session_lib.ml Ocamldep src/ide/why3web.ml Ocamldep src/why3session/why3session_info.ml Ocamldep src/why3session/why3session_latex.ml Ocamldep src/why3session/why3session_html.ml Ocamldep src/why3session/why3session_update.ml Ocamldep src/why3session/why3session_main.ml Ocamldep src/tools/why3shell.ml cmp -s src/tools/why3pp_sexp-real.ml src/tools/why3pp_sexp.ml || cp src/tools/why3pp_sexp-real.ml src/tools/why3pp_sexp.ml Ocamldep src/isabelle-client/isabelle_client_main.ml cp src/util/json_base.ml src/trywhy3/json_base.ml cp src/util/json_base.mli src/trywhy3/json_base.mli cp src/util/json_parser.ml src/trywhy3/json_parser.ml 307 states, 15627 transitions, table size 64350 bytes Ocamllex src/why3doc/doc_lexer.mll cp src/util/json_lexer.ml src/trywhy3/json_lexer.ml cp src/util/json_parser.mli src/trywhy3/json_parser.mli cp src/util/json_lexer.mli src/trywhy3/json_lexer.mli Read 3 sample input sentences and 3 error messages. 120 states, 685 transitions, table size 3460 bytes 1763 additional bytes used for bindings menhir --explain --strict src/parser/parser_common.mly src/parser/parser.mly --base src/parser/parser --compile-errors \ src/parser/handcrafted.messages > src/parser/parser_messages.ml Ocamldep src/tools/main.ml Ocamldep src/tools/why3execute.ml Ocamldep src/tools/why3config.ml Ocamldep src/tools/why3prove.ml Ocamldep src/tools/why3extract.ml Ocamldep src/tools/why3realize.ml Ocamldep src/tools/why3replay.ml Ocamldep src/tools/why3wc.ml Ocamldep src/tools/why3show.ml Read 3 sample input sentences and 3 error messages. Ocamldep src/tools/why3pp_sexp.ml Ocamldep src/why3doc/doc_html.ml Ocamldep src/tools/why3pp.ml Ocamldep src/trywhy3/json_base.ml Ocamldep src/why3doc/doc_def.ml Ocamldep src/why3doc/doc_main.ml Ocamldep src/why3doc/doc_lexer.ml Ocamldep src/trywhy3/json_lexer.ml Ocamldep src/trywhy3/bindings.ml Ocamldep src/trywhy3/json_parser.ml Ocamldep src/trywhy3/trywhy3.ml Ocamldep src/trywhy3/why3_worker.ml Ocamldep src/trywhy3/shortener.ml Ocamldep src/trywhy3/worker_proto.ml Ocamldep src/util/mysexplib.ml Ocamldep src/util/config.ml Ocamldep src/util/bigInt.ml Ocamldep src/util/mlmpfr_wrapper.ml Ocamldep src/util/util.ml Ocamldep src/util/opt.ml Ocamldep src/util/lists.ml Ocamldep src/util/strings.ml Ocamldep src/util/pp.ml Ocamldep src/util/extmap.ml Ocamldep src/util/extset.ml Ocamldep src/util/exthtbl.ml Ocamldep src/util/weakhtbl.ml Ocamldep src/util/diffmap.ml Ocamldep src/util/hashcons.ml Ocamldep src/util/wstdlib.ml Ocamldep src/util/exn_printer.ml Ocamldep src/util/getopt.ml Ocamldep src/util/json_base.ml Ocamldep src/util/json_lexer.ml Ocamldep src/util/debug.ml Ocamldep src/util/loc.ml Ocamldep src/util/lexlib.ml Ocamldep src/util/cmdline.ml Ocamldep src/util/sysutil.ml Ocamldep src/util/rc.ml Ocamldep src/util/print_tree.ml Ocamldep src/util/plugin.ml Ocamldep src/util/json_parser.ml Ocamldep src/util/vector.ml Ocamldep src/util/constant.ml Ocamldep src/util/number.ml Ocamldep src/util/pqueue.ml Ocamldep src/core/term.ml Ocamldep src/util/re.ml Ocamldep src/core/ty.ml Ocamldep src/core/ident.ml Ocamldep src/core/decl.ml Ocamldep src/core/pattern.ml Ocamldep src/core/coercion.ml Ocamldep src/core/theory.ml Ocamldep src/core/parser_tokens.ml Ocamldep src/core/task.ml Ocamldep src/core/pretty.ml Ocamldep src/core/dterm.ml Ocamldep src/core/env.ml Ocamldep src/core/trans.ml Ocamldep src/core/keywords.ml Ocamldep src/core/printer.ml Ocamldep src/core/model_parser.ml Ocamldep src/driver/whyconf.ml Ocamldep src/driver/call_provers.ml Ocamldep src/driver/prove_client.ml Ocamldep src/driver/driver_parser.ml Ocamldep src/driver/driver_lexer.ml Ocamldep src/driver/driver.ml Ocamldep src/driver/autodetection.ml Ocamldep src/driver/smtv2_model_defs.ml Ocamldep src/driver/sexp.ml Ocamldep src/driver/smtv2_model_parser.ml Ocamldep src/mlw/expr.ml Ocamldep src/mlw/pdecl.ml Ocamldep src/mlw/ity.ml Ocamldep src/mlw/eval_match.ml Ocamldep src/mlw/vc.ml Ocamldep src/mlw/typeinv.ml Ocamldep src/mlw/pmodule.ml Ocamldep src/mlw/dexpr.ml Ocamldep src/mlw/big_real.ml Ocamldep src/mlw/pinterp_core.ml Ocamldep src/mlw/rac.ml Ocamldep src/mlw/pinterp.ml Ocamldep src/mlw/check_ce.ml Ocamldep src/transform/encoding_sort.ml Ocamldep src/parser/sexp_parser.ml Ocamldep src/parser/lexer.ml Ocamldep src/transform/eliminate_unknown_lsymbols.ml Ocamldep src/transform/encoding_select.ml Ocamldep src/transform/remove_unused.ml Ocamldep src/transform/simplify_array.ml Ocamldep src/transform/smoke_detector.ml Ocamldep src/transform/prop_curry.ml Ocamldep src/transform/instantiate_predicate.ml Ocamldep src/transform/eliminate_literal.ml Ocamldep src/transform/libencoding.ml Ocamldep src/transform/generic_arg_trans_utils.ml Ocamldep src/extract/cakeml.ml Ocamldep src/transform/args_wrapper.ml Ocamldep src/transform/subst.ml Ocamldep src/transform/eliminate_definition.ml Ocamldep src/transform/introduction.ml Ocamldep src/transform/apply.ml Ocamldep src/transform/eliminate_symbol.ml Ocamldep src/transform/detect_polymorphism.ml Ocamldep src/transform/ind_itp.ml Ocamldep src/parser/parser.ml Ocamldep src/transform/encoding_guards.ml Ocamldep src/transform/close_epsilon.ml Ocamldep src/transform/encoding.ml Ocamldep src/parser/ptree_helpers.ml Ocamldep src/transform/abstract_quantifiers.ml Ocamldep src/transform/congruence.ml Ocamldep src/transform/eliminate_epsilon.ml Ocamldep src/transform/encoding_guards_full.ml Ocamldep src/transform/abstraction.ml Ocamldep src/parser/glob.ml Ocamldep src/transform/cut.ml Ocamldep src/transform/eliminate_unused.ml Ocamldep src/transform/filter_trigger.ml Ocamldep src/transform/rec_logic.ml Ocamldep src/transform/eliminate_gnatprove_guard_epsilon.ml Ocamldep src/extract/mlinterp.ml Ocamldep src/transform/eliminate_let.ml Ocamldep src/transform/encoding_tags.ml Ocamldep src/transform/case.ml Ocamldep src/parser/mlw_printer.ml Ocamldep src/transform/eliminate_inductive.ml Ocamldep src/transform/lift_epsilon.ml Ocamldep src/extract/mltree.ml Ocamldep src/extract/ocaml.ml Ocamldep src/transform/eliminate_algebraic.ml Ocamldep src/transform/encoding_tags_full.ml Ocamldep src/transform/reduction_engine.ml Ocamldep src/transform/inlining.ml Ocamldep src/parser/report.ml Ocamldep src/transform/eliminate_unknown_types.ml Ocamldep src/transform/encoding_twin.ml Ocamldep src/parser/typing.ml Ocamldep src/parser/ptree.ml Ocamldep src/extract/compile.ml Ocamldep src/transform/eliminate_if.ml Ocamldep src/transform/split_goal.ml Ocamldep src/transform/discriminate.ml Ocamldep src/extract/ml_printer.ml Ocamldep src/transform/intro_projections_counterexmp.ml Ocamldep src/transform/compute.ml Ocamldep src/transform/destruct.ml Ocamldep src/transform/fold_defs.ml Ocamldep src/extract/c.ml Ocamldep src/transform/gnat_rewrite.ml Ocamldep src/transform/eliminate_quantifiers.ml Ocamldep src/extract/pdriver.ml Ocamldep src/parser/parser_messages.ml Ocamldep src/transform/simplify_formula.ml Ocamldep src/transform/gnat_split_disj.ml Ocamldep src/transform/gnat_split_conj.ml Ocamldep src/transform/gnat_trivial.ml Ocamldep src/transform/eliminate_unused_hypo.ml Ocamldep src/transform/induction.ml Ocamldep src/transform/induction_pr.ml Ocamldep src/transform/prepare_for_counterexmp.ml Ocamldep src/transform/intro_vc_vars_counterexmp.ml Ocamldep src/transform/reflection.ml Ocamldep src/transform/keep_only_arithmetic.ml Ocamldep src/printer/alt_ergo.ml Ocamldep src/printer/cntexmp_printer.ml Ocamldep src/printer/why3printer.ml Ocamldep src/printer/smtv2.ml Ocamldep src/printer/coq.ml Ocamldep src/printer/smtv1.ml Ocamldep src/printer/pvs.ml Ocamldep src/printer/isabelle.ml Ocamldep src/printer/simplify.ml Ocamldep src/printer/gappa.ml Ocamldep src/printer/cvc3.ml Ocamldep src/printer/yices.ml Ocamldep src/printer/mathematica.ml Ocamldep src/session/compress.ml Ocamldep src/session/xml.ml Ocamldep src/session/termcode.ml Ocamldep src/session/session_itp.ml Ocamldep src/session/strategy_parser.ml Ocamldep src/session/strategy.ml Ocamldep src/session/controller_itp.ml Ocamldep src/session/server_utils.ml Ocamldep src/session/itp_communication.ml Ocamldep src/session/json_util.ml Ocamldep src/session/itp_server.ml Ocamldep src/session/unix_scheduler.ml Ocamldep src/driver/driver_ast.mli Ocamldep plugins/parser/genequlin.ml Ocamldep plugins/parser/dimacs.ml Ocamldep plugins/tptp/tptp_parser.ml Ocamldep plugins/tptp/tptp_typing.ml Ocamldep plugins/tptp/tptp_printer.ml Ocamldep plugins/python/py_lexer.ml Ocamldep plugins/python/py_parser.ml Ocamldep plugins/tptp/tptp_lexer.ml Ocamldep plugins/python/py_main.ml Ocamldep plugins/microc/mc_parser.ml Ocamldep plugins/microc/mc_lexer.ml Ocamldep plugins/microc/mc_printer.ml Ocamldep plugins/microc/mc_main.ml Ocamldep plugins/cfg/cfg_parser.ml Ocamldep plugins/cfg/cfg_lexer.ml Ocamldep plugins/cfg/stackify.ml Ocamldep plugins/cfg/cfg_main.ml Ocamldep plugins/cfg/subregion_analysis.ml Ocamldep plugins/cfg/cfg_paths.ml Ocamldep plugins/cfg/cfg_stackify.ml Ocamldep plugins/ada_terms/ada_nametable.ml Ocamldep plugins/gnat_json/ptree_constructors.ml Ocamldep plugins/ada_terms/ada_lexer.ml Ocamldep plugins/gnat_json/gnat_ast_to_ptree.ml Ocamldep plugins/python/py_ast.mli Ocamldep plugins/tptp/tptp_ast.mli Ocamldep plugins/microc/mc_ast.mli Ocamldep plugins/cfg/cfg_ast.mli Ocamldep plugins/ada_terms/ada_parser.ml Ocamldep plugins/ada_terms/ada_main.ml Ocamldep plugins/gnat_json/gnat_ast.ml Ocamldep plugins/gnat_json/gnat_ast_pretty.ml Setup [mkdir] object directory for project GNATprove [mkdir] exec directory for project GNATprove Compile [Ada] gnatprove.adb [Ada] spark_report.adb [Ada] spark_memcached_wrapper.adb [Ada] spark_semaphore_wrapper.adb [C] semaphores_c.c [C] colors.c mkdir lib/plugins Ocamlc src/util/util.mli Ocamlc src/util/mlmpfr_wrapper.mli Ocamlc src/util/mysexplib.ml Ocamlc src/util/config.mli Ocamlc src/util/opt.mli Ocamlc src/util/bigInt.mli Ocamlc src/util/strings.mli Ocamlc src/util/lists.mli Ocamlc src/util/pp.mli Setup [mkdir] object directory for project Helpers Ocamlc src/util/extmap.mli Ocamlc src/util/weakhtbl.mli Ocamlc src/util/exthtbl.mli Compile [Ada] xtree.adb Ocamlc src/util/exn_printer.mli Ocamlc src/util/getopt.mli Ocamlc src/util/json_base.mli Ocamlc src/util/lexlib.mli Ocamlc src/util/hashcons.mli Ocamlc src/util/print_tree.mli Ocamlc src/util/cmdline.mli Ocamlc src/util/sysutil.mli Ocamlc src/util/vector.mli Ocamlc src/util/pqueue.mli Ocamlc src/util/re.ml Ocamlc src/driver/prove_client.mli Ocamlc src/driver/sexp.mli Ocamlc src/extract/c.mli Linking src/util/ppx_debug_optim Ocamlc src/mlw/big_real.mli Ocamlc src/driver/smtv2_model_parser.mli Ocamlc src/extract/ocaml.mli Ocamlc src/extract/cakeml.mli Ocamlc src/parser/parser_messages.mli findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /usr/pkg/lib/ocaml, /usr/pkg/lib/ocaml/compiler-libs File "src/util/re.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/transform/remove_unused.mli Ocamlc src/transform/abstract_quantifiers.mli [Ada] templates.adb [Ada] xkind_checks.adb [Ada] xkind_conversions.adb [Ada] xkind_decls.adb [Ada] xkind_ids.adb [Ada] xtree_accessors.adb [Ada] xtree_builders.adb [Ada] xtree_checks.adb [Ada] xtree_children_checks.adb [Ada] xtree_decls.adb [Ada] xtree_mutators.adb [Ada] xtree_sinfo.adb [Ada] xtree_traversal.adb [Ada] xtree_why_ast.adb Ocamlc src/transform/eliminate_symbol.mli Ocamlc src/transform/eliminate_unknown_lsymbols.mli Ocamlc src/transform/eliminate_unknown_types.mli Ocamlc src/transform/encoding_select.mli Ocamlc src/transform/encoding_guards_full.mli Ocamlc src/transform/encoding_guards.mli Ocamlc src/transform/encoding_tags.mli Ocamlc src/transform/encoding_tags_full.mli Ocamlc src/transform/simplify_array.mli Ocamlc src/transform/encoding_twin.mli [Ada] named_semaphores.adb Ocamlc src/transform/encoding_sort.mli Ocamlc src/transform/filter_trigger.mli Ocamlc src/transform/eliminate_gnatprove_guard_epsilon.mli Ocamlc src/transform/instantiate_predicate.mli [Ada] why.ads [Ada] why-sinfo.ads [Ada] xkind_tables.adb [Ada] outputs.adb Ocamlc src/transform/prop_curry.mli Ocamlc src/transform/lift_epsilon.mli Ocamlc src/transform/case.mli [Ada] xtree_classes.adb [Ada] xtree_tables.adb Ocamlc src/transform/congruence.mli Ocamlc src/transform/gnat_split_disj.mli Ocamlc src/transform/induction.mli Ocamlc src/transform/induction_pr.mli Ocamlc src/transform/keep_only_arithmetic.mli Ocamlc src/printer/alt_ergo.mli Ocamlc src/printer/smtv1.mli Ocamlc src/printer/why3printer.mli Ocamlc src/printer/smtv2.mli Ocamlc src/printer/coq.mli Ocamlc src/printer/pvs.mli Ocamlc src/printer/isabelle.mli Ocamlc src/printer/simplify.mli Ocamlc src/printer/gappa.mli Ocamlc src/printer/cvc3.mli Ocamlc src/printer/yices.mli Ocamlc src/printer/mathematica.mli Ocamlc src/session/compress.mli Ocamlc src/session/xml.mli Ocamlc src/util/config.ml Ocamlc src/session/unix_scheduler.mli Ocamlc src/util/util.ml Ocamlc src/util/bigInt.ml Ocamlc src/util/opt.ml Ocamlc src/util/lists.ml Ocamlc src/util/strings.ml Ocamlc src/util/exthtbl.ml Ocamlc src/util/pp.ml Ocamlc src/util/extmap.ml Ocamlc src/util/weakhtbl.ml Ocamlc src/util/hashcons.ml Ocamlc src/util/exn_printer.ml Ocamlc src/util/getopt.ml Ocamlc src/util/print_tree.ml Ocamlc src/util/json_base.ml Ocamlc src/util/cmdline.ml Ocamlc src/util/sysutil.ml Ocamlc src/util/vector.ml Ocamlc src/driver/prove_client.ml Ocamlc plugins/parser/genequlin.mli Ocamlc plugins/parser/dimacs.mli Ocamlc plugins/tptp/tptp_printer.mli Ocamlc plugins/microc/mc_main.mli Ocamlc plugins/python/py_main.mli Ocamlc plugins/cfg/cfg_stackify.mli Ocamlc plugins/gnat_json/gnat_ast.ml Ocamlc src/tools/main.mli Ocamlc src/tools/why3config.mli Ocamlc src/tools/why3execute.mli Ocamlc src/tools/why3extract.mli Ocamlc src/tools/why3realize.mli Ocamlc src/tools/why3prove.mli Ocamlc src/tools/why3show.mli Ocamlc src/tools/why3wc.mli Ocamlc src/tools/why3replay.mli Ocamlc src/gnat/gnat_scheduler.mli Ocamlc src/ide/wserver.mli Ocamlc src/ide/why3web.mli Ocamlc src/tools/why3shell.mli Ocamlc src/why3session/why3session_main.mli Ocamlc src/isabelle-client/isabelle_client_main.mli Ocamlc src/why3doc/doc_html.mli Ocamlc src/tools/why3pp.mli gcc -Wall -O -g -o src/server/logging.o -c src/server/logging.c gcc -Wall -O -g -o src/server/arraylist.o -c src/server/arraylist.c gcc -Wall -O -g -o src/server/options.o -c src/server/options.c gcc -Wall -O -g -o src/server/queue.o -c src/server/queue.c gcc -Wall -O -g -o src/server/readbuf.o -c src/server/readbuf.c gcc -Wall -O -g -o src/server/request.o -c src/server/request.c gcc -Wall -O -g -o src/server/proc.o -c src/server/proc.c gcc -Wall -O -g -o src/server/writebuf.o -c src/server/writebuf.c Ocamlc src/why3doc/doc_lexer.mli gcc -Wall -O -g -o src/server/server-unix.o -c src/server/server-unix.c gcc -Wall -O -g -o src/server/server-win.o -c src/server/server-win.c Ocamlc src/why3doc/doc_main.mli gcc -Wall -O -g -o src/server/cpulimit-unix.o -c src/server/cpulimit-unix.c gcc -Wall -O -g -o src/server/cpulimit-win.o -c src/server/cpulimit-win.c Generate drivers/coq-realizations.aux Generate drivers/pvs-realizations.aux Generate drivers/isabelle-realizations.aux Ocamlopt src/util/mysexplib.ml Ocamlopt src/util/config.ml Ocamlopt src/util/util.ml Ocamlopt src/util/lists.ml Ocamlopt src/util/opt.ml Ocamlopt src/util/strings.ml Ocamlopt src/util/extmap.ml Ocamlc src/util/extset.mli Ocamlopt src/util/exthtbl.ml Ocamlopt src/util/weakhtbl.ml Ocamlc src/util/diffmap.mli Ocamlopt src/util/hashcons.ml Ocamlopt src/util/exn_printer.ml Ocamlc src/util/json_parser.mli Ocamlopt src/util/print_tree.ml Ocamlc src/util/debug.mli Ocamlopt src/util/json_base.ml Ocamlc src/util/loc.mli Ocamlc src/util/number.mli Ocamlopt src/util/re.ml Ocamlopt src/driver/sexp.ml Ocamlopt src/util/vector.ml Ocamlc src/driver/sexp.ml Ocamlc src/parser/parser_messages.ml Ocamlopt src/parser/parser_messages.ml Ocamlopt src/util/mlmpfr_wrapper.ml Ocamlc src/mlw/big_real.ml Ocamlc src/util/mlmpfr_wrapper.ml gcc -Wall -o lib/why3cpulimit src/server/cpulimit-unix.o src/server/cpulimit-win.o Ocamlopt src/session/compress.ml Ocamlc src/session/compress.ml Ocamlc src/util/pqueue.ml gcc -Wall -o lib/why3server src/server/logging.o src/server/arraylist.o src/server/options.o src/server/queue.o src/server/readbuf.o src/server/request.o src/server/proc.o src/server/writebuf.o src/server/server-unix.o src/server/server-win.o File "src/util/vector.ml", line 22, characters 22-30: 22 | let create ?capacity:(capacity: (int) option) ~dummy:(dummy: 'a) : 'a t = ^^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. [Ada] cache_client.ads [Ada] filecache_client.adb [Ada] memcache_client.adb Ocamlopt src/util/cmdline.ml Ocamlc src/session/unix_scheduler.ml Ocamlopt src/session/unix_scheduler.ml Ocamlc src/util/diffmap.ml Ocamlopt src/mlw/big_real.ml Ocamlopt src/util/diffmap.ml Ocamlopt src/util/getopt.ml Ocamlopt src/driver/prove_client.ml File "plugins/gnat_json/gnat_ast.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/util/constant.mli Ocamlc src/driver/smtv2_model_defs.mli Ocamlopt src/util/pp.ml Ocamlc src/util/json_lexer.mli Ocamlc src/util/json_parser.ml Ocamlc src/util/extset.ml Ocamlc src/util/wstdlib.mli Ocamlc src/gnat/gnat_loc.mli [Ada] utils.adb Ocamlc src/core/ident.mli Ocamlc src/core/parser_tokens.mli Ocamlc src/driver/driver_ast.mli Ocamlc src/util/lexlib.ml Ocamlopt src/gnat/gnat_scheduler.ml Ocamlopt src/util/bigInt.ml File "src/driver/prove_client.ml", line 116, characters 21-27: 116 | let connect_internal libdir = ^^^^^^ Warning 27 [unused-var-strict]: unused variable libdir. Ocamlc src/util/number.ml Ocamlc src/session/xml.ml Ocamlc src/util/plugin.mli Ocamlc src/util/constant.ml File "src/util/vector.ml", line 22, characters 22-30: 22 | let create ?capacity:(capacity: (int) option) ~dummy:(dummy: 'a) : 'a t = ^^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. Ocamlc src/driver/driver_parser.mli File "src/driver/prove_client.ml", line 116, characters 21-27: 116 | let connect_internal libdir = ^^^^^^ Warning 27 [unused-var-strict]: unused variable libdir. Ocamlc src/driver/smtv2_model_defs.ml Ocamlc src/util/rc.mli Ocamlc src/util/wstdlib.ml Ocamlc src/util/debug.ml Ocamlc src/util/loc.ml File "src/gnat/gnat_scheduler.ml", line 10, characters 15-19: 10 | let idle ~(prio:int) f = ^^^^ Warning 27 [unused-var-strict]: unused variable prio. File "src/gnat/gnat_scheduler.ml", line 16, characters 17-19: 16 | let timeout ~ms f = timeout_handler := Some f ^^ Warning 27 [unused-var-strict]: unused variable ms. Ocamlopt src/util/extset.ml Ocamlopt src/util/sysutil.ml Ocamlc src/util/json_lexer.ml Ocamlc src/util/plugin.ml Bind [gprbind] xtree.bexch [Ada] xtree.ali Ocamlc src/core/parser_tokens.ml Ocamlopt src/util/json_parser.ml Ocamlc src/core/ty.mli Ocamlc src/parser/glob.mli Ocamlc src/core/ident.ml Ocamlopt src/util/pqueue.ml Ocamlc src/driver/driver_parser.ml [Ada] call.adb Ocamlc src/util/rc.ml Ocamlc src/parser/glob.ml Link [link] xtree.adb Ocamlopt src/util/wstdlib.ml Ocamlopt plugins/gnat_json/gnat_ast.ml Ocamlc plugins/gnat_json/gnat_ast_pretty.mli Ocamlc src/core/term.mli Ocamlc src/core/ty.ml ./xtree Ocamlopt src/util/json_lexer.ml cp why-classes.ads why-atree.ads why-atree-accessors.ads why-atree-builders.ads why-atree-builders.adb why-atree-mutators.ads why-atree-mutators.adb why-atree-traversal.ads why-atree-traversal.adb why-atree-traversal_stub.ads why-atree-traversal_stub.adb why-atree-treepr.ads why-atree-treepr.adb why-atree-validity.ads why-conversions.ads why-ids.ads why-kind_validity.ads why-opaque_ids.ads why-unchecked_ids.ads why-atree-to_json.adb ../ gmake[2]: Leaving directory '/pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/src/why/xgen' mkdir -p obj obj-gnat obj-gnat2why obj-tools ../install/bin sed -e "s^@ADAINCLUDE@^/pbulk/work/lang/spark2014-14/work/.buildlink/lib/gcc/x86_64--netbsd/14.3.0/adainclude /usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adainclude^" \ -e "s^@ADALIB@^/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib^" \ -e "s^@PREFIX@^/pbulk/work/lang/spark2014-14/work/.buildlink/lib/gcc/x86_64--netbsd/14.3.0/adainclude /usr/pkg/gcc14-gnat/^" \ -e "s^@GNAT1DIR@^/pbulk/work/lang/spark2014-14/work/.buildlink/lib/gcc/x86_64--netbsd/14.3.0/ /usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adainclude^" \ sdefault.adb.in > obj/sdefault.adb cp -f gnat_src/ada_get_targ.adb obj/get_targ.adb for f in gnat1drv.adb ;\ do \ cp -pf gnat_src/$f obj-gnat2why; \ done cp -pf gnat_src/libgnat/s-rident.ads obj-gnat for f in `cd gnat_src; ls gen_il*.ad? xutil.ad? *-tmpl xsnamest.adb`; \ do \ cp -p gnat_src/$f obj-tools; \ done cd obj-tools && gprbuild -q xsnamest && ./xsnamest && \ mv snames.ns ../obj/snames.ads && mv snames.nb ../obj/snames.adb && \ gprbuild -q -j0 gen_il-main.adb -cargs -I../obj && ./gen_il-main && \ mv nmake.adb nmake.ads seinfo.ads sinfo-nodes.ads sinfo-nodes.adb einfo-entities.ads einfo-entities.adb ../obj Ocamlc src/core/decl.mli Ocamlc src/core/pattern.mli Ocamlc src/core/coercion.mli Ocamlc src/mlw/ity.mli Ocamlc src/transform/close_epsilon.mli Ocamlc src/printer/cntexmp_printer.mli Ocamlc src/core/term.ml Ocamlopt src/util/debug.ml Ocamlopt src/util/rc.ml Ocamlc src/core/pattern.ml Ocamlc src/core/dterm.mli Ocamlc src/core/coercion.ml Ocamlc src/core/theory.mli Ocamlc src/core/decl.ml Ocamlopt src/util/plugin.ml Ocamlopt src/util/loc.ml Ocamlopt src/util/number.ml Ocamlopt src/session/xml.ml Ocamlc src/mlw/expr.mli Ocamlc src/printer/cntexmp_printer.ml Ocamlc src/core/env.mli Ocamlc src/core/task.mli Ocamlc src/transform/detect_polymorphism.mli Ocamlc src/transform/eliminate_literal.mli Ocamlc src/core/theory.ml Ocamlopt src/util/lexlib.ml Ocamlopt src/core/ident.ml Ocamlc src/session/termcode.mli Ocamlc src/core/pretty.mli Ocamlc src/core/task.ml Ocamlc src/driver/whyconf.mli Ocamlc src/core/trans.mli Ocamlc src/core/env.ml Ocamlc src/transform/reduction_engine.mli Ocamlopt src/core/parser_tokens.ml Ocamlopt src/util/constant.ml Ocamlopt src/driver/smtv2_model_defs.ml Ocamlc src/parser/ptree.ml Ocamlc src/mlw/pdecl.mli Ocamlc src/driver/driver_lexer.mli File "src/core/theory.ml", line 505, characters 4-12: 505 | let print_id fmt id = Ident.print_decoded fmt id.id_string ^^^^^^^^ Warning 32 [unused-value-declaration]: unused value print_id. File "src/core/theory.ml", line 507, characters 4-23: 507 | let warn_axiom_abstract = ^^^^^^^^^^^^^^^^^^^ Warning 32 [unused-value-declaration]: unused value warn_axiom_abstract. Ocamlc src/driver/autodetection.mli Ocamlc src/session/strategy.mli Ocamlc src/driver/whyconf.ml Ocamlc src/core/dterm.ml Ocamlc src/mlw/ity.ml Ocamlc src/mlw/expr.ml Ocamlc src/transform/reduction_engine.ml Ocamlc src/transform/abstract_quantifiers.ml Ocamlc src/transform/detect_polymorphism.ml Ocamlc src/transform/eliminate_symbol.ml Ocamlc src/transform/simplify_array.ml Ocamlc src/transform/remove_unused.ml Ocamlc src/transform/lift_epsilon.ml Ocamlc src/transform/eliminate_gnatprove_guard_epsilon.ml Ocamlc src/transform/close_epsilon.ml Ocamlc src/transform/instantiate_predicate.ml Ocamlc src/transform/prop_curry.ml Ocamlc src/transform/keep_only_arithmetic.ml Ocamlc src/transform/congruence.ml Ocamlc src/session/termcode.ml Ocamlc src/session/strategy.ml Ocamlc src/core/printer.mli Ocamlc src/mlw/pmodule.mli Ocamlopt src/core/ty.ml Ocamlopt src/driver/driver_parser.ml Ocamlc src/mlw/typeinv.mli Ocamlc src/mlw/eval_match.mli Ocamlc src/mlw/vc.mli Ocamlc src/transform/inlining.mli Ocamlc src/transform/simplify_formula.mli Ocamlc src/transform/split_goal.mli Ocamlopt src/parser/glob.ml Ocamlc src/transform/compute.mli Ocamlc src/transform/eliminate_definition.mli Ocamlc src/transform/eliminate_let.mli Ocamlc src/transform/eliminate_quantifiers.ml Ocamlc src/transform/eliminate_if.mli Ocamlc src/transform/libencoding.mli Ocamlc src/transform/eliminate_algebraic.mli [Ada] string_utils.adb Ocamlc src/transform/eliminate_inductive.mli Ocamlc src/transform/encoding.mli Ocamlc src/transform/abstraction.mli Ocamlc src/transform/eliminate_epsilon.mli Ocamlc src/transform/smoke_detector.mli Ocamlc src/transform/generic_arg_trans_utils.mli Ocamlc src/transform/intro_projections_counterexmp.mli Ocamlc src/transform/apply.mli Ocamlc src/transform/introduction.mli Ocamlc src/transform/subst.mli Ocamlc src/transform/destruct.mli Ocamlc src/transform/rec_logic.ml Ocamlc src/transform/cut.mli Ocamlc src/transform/gnat_rewrite.mli File "src/transform/eliminate_quantifiers.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/transform/eliminate_unused.mli Ocamlc src/transform/gnat_split_conj.mli Ocamlc src/transform/eliminate_unused_hypo.ml Ocamlc src/transform/intro_vc_vars_counterexmp.mli Ocamlc src/transform/prepare_for_counterexmp.mli Ocamlc src/transform/reflection.mli Ocamlc src/session/strategy_parser.mli File "src/transform/rec_logic.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/core/trans.ml Ocamlc src/driver/driver_lexer.ml Ocamlc src/core/printer.ml Ocamlc src/mlw/pdecl.ml Ocamlc src/mlw/typeinv.ml Ocamlc src/mlw/eval_match.ml Ocamlc src/mlw/vc.ml Ocamlc src/mlw/pmodule.ml Ocamlc src/transform/simplify_formula.ml Ocamlc src/transform/split_goal.ml Ocamlc src/transform/eliminate_unknown_types.ml Ocamlc src/transform/eliminate_unknown_lsymbols.ml Ocamlc src/transform/eliminate_inductive.ml Ocamlc src/transform/eliminate_let.ml Ocamlc src/transform/libencoding.ml Ocamlc src/transform/eliminate_if.ml Ocamlc src/transform/eliminate_algebraic.ml Ocamlc src/transform/encoding.ml Ocamlc src/transform/encoding_guards_full.ml Ocamlc src/transform/encoding_tags_full.ml Ocamlc src/transform/encoding_guards.ml Ocamlc src/transform/encoding_tags.ml Ocamlc src/transform/encoding_twin.ml Ocamlc src/driver/autodetection.ml Ocamlc src/transform/encoding_sort.ml Ocamlc src/transform/filter_trigger.ml Ocamlc src/transform/eliminate_epsilon.ml Ocamlc src/transform/abstraction.ml Ocamlc src/transform/eliminate_literal.ml Ocamlc src/transform/introduction.ml Ocamlc src/transform/generic_arg_trans_utils.ml Ocamlc src/transform/gnat_split_disj.ml Ocamlc src/printer/coq.ml Ocamlc src/transform/intro_projections_counterexmp.ml Ocamlc src/transform/smoke_detector.ml Ocamlc src/printer/mathematica.ml Ocamlc src/parser/parser.mli Ocamlc src/core/model_parser.mli Ocamlc src/mlw/dexpr.mli Ocamlc src/mlw/pinterp_core.mli Ocamlc src/extract/mltree.mli Ocamlc src/extract/mlinterp.mli Ocamlc src/parser/ptree_helpers.mli Ocamlc src/parser/lexer.mli Ocamlc src/parser/mlw_printer.mli Ocamlc src/transform/args_wrapper.mli Ocamlc src/transform/discriminate.mli Ocamlc src/transform/fold_defs.ml Ocamlc src/printer/pvs.ml Ocamlc src/printer/isabelle.ml Ocamlc src/printer/gappa.ml Ocamlc src/session/strategy_parser.ml Ocamlc src/transform/eliminate_unused.ml Ocamlc src/transform/gnat_rewrite.ml Ocamlc src/transform/gnat_split_conj.ml Ocamlc src/transform/intro_vc_vars_counterexmp.ml File "src/transform/eliminate_unused_hypo.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/core/term.ml Ocamlc src/parser/mlw_printer.ml Ocamlc src/mlw/pinterp.mli Ocamlc src/mlw/pinterp_core.ml Ocamlc src/extract/compile.mli Ocamlc src/extract/pdriver.mli Ocamlc src/mlw/pinterp.ml Ocamlc src/core/keywords.mli Ocamlc src/parser/report.mli File "src/transform/fold_defs.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/extract/ml_printer.mli Ocamlc src/transform/ind_itp.mli Ocamlc src/transform/gnat_trivial.ml Ocamlc src/transform/compute.ml Ocamlc src/transform/apply.ml Ocamlc src/transform/subst.ml Ocamlc src/transform/destruct.ml Ocamlc src/transform/cut.ml Ocamlc src/transform/case.ml Ocamlc src/parser/ptree_helpers.ml Ocamlc src/transform/reflection.ml Ocamlc src/extract/compile.ml Ocamlc src/extract/mlinterp.ml Ocamlc src/transform/discriminate.ml Ocamlc src/printer/smtv1.ml Ocamlc src/printer/simplify.ml Ocamlc src/transform/encoding_select.ml Ocamlc src/printer/cvc3.ml Ocamlc src/printer/yices.ml Ocamlc src/parser/typing.mli Ocamlc src/extract/mltree.ml Ocamlc src/extract/c.ml Ocamlc src/mlw/dexpr.ml File "src/transform/gnat_trivial.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/extract/ml_printer.ml Ocamlc src/extract/ocaml.ml Ocamlc src/extract/cakeml.ml Ocamlc src/parser/report.ml Ocamlc src/driver/call_provers.mli Ocamlc src/driver/smtv2_model_parser.ml Ocamlc src/core/model_parser.ml Ocamlopt src/core/keywords.ml Ocamlc src/core/keywords.ml Ocamlc src/core/pretty.ml Ocamlc src/printer/why3printer.ml Ocamlc src/transform/ind_itp.ml Ocamlc src/transform/induction_pr.ml Ocamlc src/transform/induction.ml Ocamlc src/mlw/check_ce.mli Ocamlc src/driver/call_provers.ml Ocamlc src/session/session_itp.mli Ocamlc src/driver/driver.mli Ocamlc src/extract/pdriver.ml Ocamlc src/mlw/rac.mli Ocamlc src/driver/driver.ml Ocamlc src/transform/inlining.ml Ocamlc src/transform/eliminate_definition.ml Ocamlc src/transform/prepare_for_counterexmp.ml Ocamlc src/printer/alt_ergo.ml Ocamlc src/printer/smtv2.ml Ocamlopt src/core/coercion.ml Ocamlopt src/core/pattern.ml Ocamlc src/mlw/check_ce.ml Ocamlc src/mlw/rac.ml File "src/transform/inlining.ml", line 93, characters 27-51: 93 | let t ~use_meta ~in_goal ?(only_top_in_goal=in_goal) ~notls ~notdef = ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. File "src/driver/call_provers.ml", line 485, characters 22-34: 485 | let cmd, use_stdin, on_timelimit = ^^^^^^^^^^^^ Warning 27 [unused-var-strict]: unused variable on_timelimit. Ocamlc src/session/controller_itp.mli Ocamlc src/session/session_itp.ml Ocamlc src/parser/sexp_parser.ml Ocamlc src/parser/typing.ml Ocamlc src/parser/parser.ml Ocamlc src/parser/lexer.ml Ocamlc src/transform/args_wrapper.ml Ocamlopt src/core/decl.ml [Ada] assumption_types.adb [Ada] assumptions.adb [Ada] assumptions-search.adb [Ada] platform.adb [Ada] print_table.adb [Ada] report_database.adb [Ada] spark2014vsn.adb [Ada] vc_kinds.adb File "src/mlw/dexpr.ml", line 1304, characters 4-28: 1304 | let attr_w_unmodified_var_no = ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 32 [unused-value-declaration]: unused value attr_w_unmodified_var_no. Ocamlc src/session/itp_communication.mli Ocamlc src/session/controller_itp.ml File "src/parser/sexp_parser.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/session/itp_server.mli Ocamlc src/session/json_util.mli Ocamlc src/session/server_utils.mli Ocamlc src/session/itp_communication.ml File "src/parser/typing.ml", line 477, characters 32-38: 477 | | Ptree.Tupdate ({ term_loc = e1_loc } as e1, fl) -> ^^^^^^ Warning 27 [unused-var-strict]: unused variable e1_loc. File "src/parser/typing.ml", line 1035, characters 32-38: 1035 | | Ptree.Eupdate ({ expr_loc = e1_loc } as e1, fl) -> ^^^^^^ Warning 27 [unused-var-strict]: unused variable e1_loc. Ocamlc src/session/json_util.ml Ocamlc src/session/server_utils.ml Ocamlc src/session/itp_server.ml Ocamlopt src/core/theory.ml File "src/core/theory.ml", line 505, characters 4-12: 505 | let print_id fmt id = Ident.print_decoded fmt id.id_string ^^^^^^^^ Warning 32 [unused-value-declaration]: unused value print_id. File "src/core/theory.ml", line 507, characters 4-23: 507 | let warn_axiom_abstract = ^^^^^^^^^^^^^^^^^^^ Warning 32 [unused-value-declaration]: unused value warn_axiom_abstract. Ocamlopt src/core/env.ml Ocamlopt src/core/task.ml Ocamlopt src/core/pretty.ml Ocamlopt src/driver/whyconf.ml Ocamlopt src/transform/reduction_engine.ml Linking lib/why3/why3.cmo Ocamlopt src/session/strategy.ml Ocamlopt src/driver/autodetection.ml Ocamlopt src/driver/driver_lexer.ml Ocamlopt src/core/dterm.ml Ocamlopt src/mlw/ity.ml Ocamlopt src/core/trans.ml Ocamlc plugins/tptp/tptp_ast.mli Ocamlc plugins/python/py_ast.mli Ocamlc plugins/microc/mc_printer.mli Ocamlc plugins/cfg/cfg_ast.mli Ocamlc plugins/microc/mc_ast.mli Ocamlc plugins/cfg/subregion_analysis.mli Ocamlc plugins/ada_terms/ada_nametable.mli Ocamlc plugins/ada_terms/ada_parser.mli Ocamlc plugins/gnat_json/ptree_constructors.mli Ocamlc src/gnat/gnat_util.mli Ocamlc plugins/gnat_json/gnat_ast_to_ptree.mli Ocamlc src/gnat/gnat_expl.mli Ocamlc src/gnat/gnat_counterexamples.ml Ocamlc src/why3session/why3session_lib.mli Ocamlc src/tools/why3pp_sexp.mli Ocamlc src/why3doc/doc_def.mli Ocamlc plugins/python/py_lexer.mli Ocamlc plugins/python/py_parser.mli Ocamlc src/gnat/gnat_config.mli Ocamlc src/gnat/gnat_manual.mli Ocamlc src/gnat/gnat_report.mli Ocamlc plugins/microc/mc_parser.mli Ocamlc plugins/microc/mc_lexer.mli Ocamlc src/why3session/why3session_info.mli Ocamlc src/why3session/why3session_latex.mli Ocamlc src/why3session/why3session_html.mli Ocamlc src/why3session/why3session_update.mli Ocamlc plugins/ada_terms/ada_lexer.ml Ocamlc plugins/tptp/tptp_typing.mli Ocamlc plugins/tptp/tptp_parser.mli Ocamlc plugins/tptp/tptp_lexer.mli Ocamlc src/gnat/gnat_objectives.mli Ocamlopt src/core/printer.ml Ocamlopt src/transform/simplify_formula.ml Ocamlopt src/transform/split_goal.ml Ocamlopt src/transform/remove_unused.ml Ocamlopt src/transform/detect_polymorphism.ml Ocamlopt src/transform/abstract_quantifiers.ml Ocamlopt src/transform/eliminate_quantifiers.ml Ocamlopt src/transform/eliminate_let.ml Ocamlopt src/transform/eliminate_symbol.ml Ocamlopt src/transform/libencoding.ml Ocamlopt src/transform/eliminate_if.ml Ocamlopt src/transform/simplify_array.ml Ocamlopt src/transform/abstraction.ml Ocamlopt src/transform/close_epsilon.ml Ocamlopt src/transform/eliminate_gnatprove_guard_epsilon.ml Ocamlopt src/transform/eliminate_epsilon.ml Ocamlopt src/transform/instantiate_predicate.ml Ocamlopt src/transform/intro_projections_counterexmp.ml Ocamlopt src/transform/smoke_detector.ml Ocamlopt src/transform/prop_curry.ml Ocamlopt src/transform/generic_arg_trans_utils.ml Ocamlopt src/transform/congruence.ml Ocamlopt src/transform/rec_logic.ml Ocamlopt src/transform/gnat_rewrite.ml Ocamlopt src/transform/eliminate_unused.ml Ocamlopt src/transform/eliminate_unused_hypo.ml Ocamlopt src/transform/keep_only_arithmetic.ml Ocamlopt src/session/termcode.ml Ocamlopt src/session/strategy_parser.ml Ocamlc plugins/cfg/cfg_parser.mli Ocamlc plugins/cfg/cfg_lexer.mli Ocamlc plugins/cfg/cfg_paths.mli Ocamlc plugins/cfg/cfg_main.mli File "plugins/ada_terms/ada_lexer.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc plugins/cfg/stackify.mli Ocamlopt src/printer/cntexmp_printer.ml Ocamlopt src/mlw/expr.ml Ocamlc plugins/ada_terms/ada_main.ml File "src/gnat/gnat_objectives.mli", line 128, characters 13-14: 128 | module Make (S: Controller_itp.Scheduler) : sig ^ Warning 67 [unused-functor-parameter]: unused functor parameter S. Ocamlopt src/transform/intro_vc_vars_counterexmp.ml Ocamlopt src/transform/eliminate_inductive.ml Ocamlopt src/transform/lift_epsilon.ml Ocamlopt src/transform/gnat_split_disj.ml Ocamlopt src/transform/gnat_split_conj.ml File "plugins/ada_terms/ada_main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. [Ada] configuration.adb [Ada] gnat2why_opts.ads [Ada] gnat2why_opts-writing.adb File "src/gnat/gnat_counterexamples.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/transform/eliminate_literal.ml Ocamlopt src/transform/encoding.ml Ocamlc src/gnat/gnat_main.ml File "src/gnat/gnat_main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/transform/fold_defs.ml Ocamlopt src/transform/eliminate_unknown_types.ml Ocamlopt src/core/model_parser.ml Ocamlopt src/transform/eliminate_unknown_lsymbols.ml Ocamlopt src/transform/eliminate_algebraic.ml Ocamlopt src/transform/filter_trigger.ml Ocamlopt src/printer/coq.ml Ocamlopt src/printer/isabelle.ml Ocamlopt src/printer/mathematica.ml Ocamlopt src/printer/pvs.ml Ocamlopt src/transform/encoding_guards_full.ml Ocamlopt src/transform/encoding_tags_full.ml Ocamlopt src/transform/encoding_twin.ml [Ada] hash_cons.adb Ocamlopt src/parser/ptree.ml Ocamlopt src/mlw/pdecl.ml Ocamlopt src/transform/encoding_tags.ml Ocamlopt src/transform/encoding_guards.ml Ocamlopt src/transform/encoding_sort.ml Ocamlopt src/driver/call_provers.ml Ocamlopt src/driver/smtv2_model_parser.ml File "src/driver/call_provers.ml", line 485, characters 22-34: 485 | let cmd, use_stdin, on_timelimit = ^^^^^^^^^^^^ Warning 27 [unused-var-strict]: unused variable on_timelimit. Ocamlopt src/driver/driver.ml Ocamlopt src/mlw/eval_match.ml Ocamlopt src/mlw/typeinv.ml Ocamlopt src/transform/inlining.ml File "src/transform/inlining.ml", line 93, characters 27-51: 93 | let t ~use_meta ~in_goal ?(only_top_in_goal=in_goal) ~notls ~notdef = ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. Ocamlopt src/parser/ptree_helpers.ml Ocamlopt src/parser/mlw_printer.ml Ocamlopt src/mlw/vc.ml gprbuild -XBuild=Production -Pgnat2why -eL -R -cargs -O2 -I/usr/pkg/include -I/usr/include -I/usr/pkg/gcc14-gnat/include -I/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/include -I/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adainclude -largs -Wl,-R'$ORIGIN' -L/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0 -Wl,-R/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0 -L/usr/pkg/gcc14-gnat/lib -Wl,-R/usr/pkg/gcc14-gnat/lib -Wl,-zrelro -L/usr/pkg/lib -Wl,-R/usr/pkg/lib -L/usr/lib -Wl,-R/usr/lib -L/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib -gargs Ocamlopt src/mlw/pmodule.ml Compile [Ada] gnat1drv.adb Ocamlopt src/mlw/pinterp_core.ml Ocamlopt src/mlw/dexpr.ml File "src/mlw/dexpr.ml", line 1304, characters 4-28: 1304 | let attr_w_unmodified_var_no = ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 32 [unused-value-declaration]: unused value attr_w_unmodified_var_no. Ocamlopt src/mlw/rac.ml Ocamlopt src/mlw/pinterp.ml Ocamlopt src/parser/typing.ml Ocamlopt src/extract/mltree.ml Ocamlopt src/extract/compile.ml Ocamlopt src/extract/pdriver.ml File "src/parser/typing.ml", line 477, characters 32-38: 477 | | Ptree.Tupdate ({ term_loc = e1_loc } as e1, fl) -> ^^^^^^ Warning 27 [unused-var-strict]: unused variable e1_loc. File "src/parser/typing.ml", line 1035, characters 32-38: 1035 | | Ptree.Eupdate ({ expr_loc = e1_loc } as e1, fl) -> ^^^^^^ Warning 27 [unused-var-strict]: unused variable e1_loc. [C] smissing.c Ocamlopt src/extract/ml_printer.ml [Ada] atree.adb Ocamlopt src/mlw/check_ce.ml Ocamlopt src/extract/ocaml.ml Ocamlopt src/extract/cakeml.ml Ocamlopt src/extract/mlinterp.ml Ocamlopt src/extract/c.ml Ocamlopt src/parser/parser.ml Ocamlopt src/parser/sexp_parser.ml [Ada] back_end.adb Ocamlopt src/parser/report.ml Ocamlopt src/parser/lexer.ml Ocamlopt src/transform/args_wrapper.ml Ocamlopt src/transform/compute.ml Ocamlopt src/transform/case.ml Ocamlopt src/transform/apply.ml Ocamlopt src/transform/subst.ml Ocamlopt src/transform/ind_itp.ml Ocamlopt src/transform/cut.ml Ocamlopt src/transform/eliminate_definition.ml Ocamlopt src/transform/discriminate.ml Ocamlopt src/printer/gappa.ml Ocamlopt src/transform/induction.ml Ocamlopt src/transform/induction_pr.ml [Ada] checks.adb Ocamlopt src/transform/introduction.ml Ocamlopt src/transform/destruct.ml Ocamlopt src/transform/encoding_select.ml Ocamlopt src/printer/smtv1.ml Ocamlopt src/printer/why3printer.ml Ocamlopt src/printer/alt_ergo.ml Ocamlopt src/printer/simplify.ml Ocamlopt src/printer/smtv2.ml Ocamlopt src/printer/cvc3.ml Ocamlopt src/printer/yices.ml Ocamlopt src/transform/reflection.ml Ocamlopt src/transform/prepare_for_counterexmp.ml Ocamlopt src/transform/gnat_trivial.ml Ocamlopt src/session/session_itp.ml Ocamlopt src/session/controller_itp.ml Ocamlopt src/session/itp_communication.ml Ocamlopt src/session/server_utils.ml Ocamlopt src/session/json_util.ml Ocamlopt src/session/itp_server.ml Linking lib/why3/why3.cmx Bind [gprbind] gnatprove.bexch [Ada] gnatprove.ali [gprbind] spark_report.bexch [Ada] spark_report.ali [gprbind] spark_memcached_wrapper.bexch [Ada] spark_memcached_wrapper.ali [gprbind] spark_semaphore_wrapper.bexch [Ada] spark_semaphore_wrapper.ali Ocamlopt plugins/parser/dimacs.ml Ocamlopt plugins/parser/genequlin.ml Ocamlopt plugins/tptp/tptp_parser.ml Ocamlopt plugins/tptp/tptp_typing.ml Ocamlopt plugins/tptp/tptp_printer.ml Ocamlopt plugins/microc/mc_parser.ml Ocamlopt plugins/python/py_parser.ml Ocamlopt plugins/cfg/cfg_paths.ml Ocamlopt plugins/cfg/cfg_parser.ml Ocamlopt plugins/microc/mc_printer.ml Ocamlopt plugins/cfg/subregion_analysis.ml Ocamlopt plugins/cfg/stackify.ml Ocamlopt plugins/ada_terms/ada_nametable.ml Ocamlopt plugins/gnat_json/ptree_constructors.ml Ocamlopt plugins/gnat_json/gnat_ast_pretty.ml Linking lib/why3/why3.cmxa Linking lib/why3/why3.cmxs Ocamlopt src/tools/main.ml Ocamlopt src/tools/why3config.ml Ocamlopt src/tools/why3execute.ml Ocamlopt src/tools/why3prove.ml Ocamlopt src/tools/why3realize.ml Ocamlopt src/tools/why3replay.ml Ocamlopt src/tools/why3extract.ml Ocamlopt src/tools/why3show.ml Ocamlopt src/tools/why3wc.ml Ocamlopt src/gnat/gnat_counterexamples.ml Ocamlopt src/ide/wserver.ml Ocamlopt src/tools/why3shell.ml Ocamlopt src/isabelle-client/isabelle_client_main.ml Ocamlopt src/why3doc/doc_html.ml Ocamlopt src/why3doc/doc_def.ml Ocamlopt src/tools/why3pp_sexp.ml Ocamlopt src/why3session/why3session_lib.ml Ocamlopt src/gnat/gnat_util.ml Ocamlopt src/tools/why3pp.ml Linking bin/why3realize.cmxs Ocamlopt src/ide/why3web.ml Ocamlopt plugins/ada_terms/ada_parser.ml Ocamlopt src/why3doc/doc_lexer.ml Linking bin/why3replay.cmxs Linking lib/plugins/dimacs.cmxs Linking bin/isabelle_client.opt Linking bin/why3wc.cmxs Linking bin/why3show.cmxs Linking bin/why3.opt Linking bin/why3execute.cmxs Linking bin/why3config.cmxs Ocamlopt src/why3session/why3session_info.ml Ocamlopt src/why3session/why3session_latex.ml Ocamlopt src/why3session/why3session_update.ml Ocamlopt src/why3session/why3session_html.ml Linking lib/plugins/genequlin.cmxs Ocamlopt src/gnat/gnat_loc.ml Ocamlopt plugins/gnat_json/gnat_ast_to_ptree.ml Link [archive] libgnatprove.a [index] libgnatprove.a [link] gnatprove.adb [link] spark_report.adb [link] spark_memcached_wrapper.adb [link] spark_semaphore_wrapper.adb /usr/bin/ld: cannot find -liconv: No such file or directory /usr/bin/ld: cannot find -liconv: No such file or directory /usr/bin/ld: cannot find -liconv: No such file or directory collect2: error: ld returned 1 exit status Linking bin/why3shell.cmxs collect2: error: ld returned 1 exit status collect2: error: ld returned 1 exit status Linking bin/why3prove.cmxs /usr/bin/ld: cannot find -liconv: No such file or directory Linking bin/why3pp.cmxs collect2: error: ld returned 1 exit status link of spark_semaphore_wrapper.adb failed failed command was: /pbulk/work/lang/spark2014-14/work/.buildlink/bin/gcc spark_semaphore_wrapper.o b__spark_semaphore_wrapper.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/named_semaphores.o libgnatprove.a /usr/pkg/gcc14-gnat/lib/gpr2.static/libgpr2.a /usr/pkg/gcc14-gnat/lib/gnatcoll_iconv.static/libgnatcoll_iconv.a /usr/pkg/gcc14-gnat/lib/gnatcoll_gmp.static/libgnatcoll_gmp.a /usr/pkg/gcc14-gnat/lib/gnatcoll_projects.static/libgnatcoll_projects.a /usr/pkg/gcc14-gnat/lib/gnatcoll_core.static/libgnatcoll_core.a /usr/pkg/gcc14-gnat/lib/gnatcoll_minimal.static/libgnatcoll_minimal.a /usr/pkg/gcc14-gnat/lib/gpr/static/gpr/libgnatprj.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_schema.static/libxmlada_schema.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_dom.static/libxmlada_dom.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_sax.static/libxmlada_sax.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_input.static/libxmlada_input_sources.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_unicode.static/libxmlada_unicode.a -lrt -liconv -lgmp -Wl,-R$ORIGIN -L/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0 -Wl,-R/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0 -L/usr/pkg/gcc14-gnat/lib -Wl,-R/usr/pkg/gcc14-gnat/lib -Wl,-zrelro -L/usr/pkg/lib -Wl,-R/usr/pkg/lib -L/usr/lib -Wl,-R/usr/lib -L/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib -L/pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/ -L/pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/ -L/usr/pkg/gcc14-gnat/lib/gpr/static/gpr/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_schema.static/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_sax.static/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_unicode.static/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_input.static/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_dom.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_projects.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_minimal.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_core.static/ -L/usr/pkg/gcc14-gnat/lib/gpr2.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_gmp.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_iconv.static/ -L/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib/ -static-libgcc /usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib/libgnat.a -o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/install/bin//spark_semaphore_wrapper link of spark_memcached_wrapper.adb failed failed command was: /pbulk/work/lang/spark2014-14/work/.buildlink/bin/gcc spark_memcached_wrapper.o b__spark_memcached_wrapper.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/cache_client.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/memcache_client.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/string_utils.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/call.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/filecache_client.o libgnatprove.a /usr/pkg/gcc14-gnat/lib/gpr2.static/libgpr2.a /usr/pkg/gcc14-gnat/lib/gnatcoll_iconv.static/libgnatcoll_iconv.a /usr/pkg/gcc14-gnat/lib/gnatcoll_gmp.static/libgnatcoll_gmp.a /usr/pkg/gcc14-gnat/lib/gnatcoll_projects.static/libgnatcoll_projects.a /usr/pkg/gcc14-gnat/lib/gnatcoll_core.static/libgnatcoll_core.a /usr/pkg/gcc14-gnat/lib/gnatcoll_minimal.static/libgnatcoll_minimal.a /usr/pkg/gcc14-gnat/lib/gpr/static/gpr/libgnatprj.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_schema.static/libxmlada_schema.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_dom.static/libxmlada_dom.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_sax.static/libxmlada_sax.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_input.static/libxmlada_input_sources.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_unicode.static/libxmlada_unicode.a -lrt -liconv -lgmp -Wl,-R$ORIGIN -L/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0 -Wl,-R/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0 -L/usr/pkg/gcc14-gnat/lib -Wl,-R/usr/pkg/gcc14-gnat/lib -Wl,-zrelro -L/usr/pkg/lib -Wl,-R/usr/pkg/lib -L/usr/lib -Wl,-R/usr/lib -L/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib -L/pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/ -L/pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/ -L/usr/pkg/gcc14-gnat/lib/gpr/static/gpr/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_schema.static/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_sax.static/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_unicode.static/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_input.static/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_dom.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_projects.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_minimal.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_core.static/ -L/usr/pkg/gcc14-gnat/lib/gpr2.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_gmp.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_iconv.static/ -L/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib/ -static-libgcc /usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib/libgnarl.a /usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib/libgnat.a -pthread -o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/install/bin//spark_memcached_wrapper link of spark_report.adb failed failed command was: /pbulk/work/lang/spark2014-14/work/.buildlink/bin/gcc spark_report.o b__spark_report.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/hash_cons.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/assumption_types.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/assumptions.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/assumptions-search.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/platform.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/print_table.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/spark2014vsn.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/string_utils.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/call.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/vc_kinds.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/report_database.o libgnatprove.a /usr/pkg/gcc14-gnat/lib/gpr2.static/libgpr2.a /usr/pkg/gcc14-gnat/lib/gnatcoll_iconv.static/libgnatcoll_iconv.a /usr/pkg/gcc14-gnat/lib/gnatcoll_gmp.static/libgnatcoll_gmp.a /usr/pkg/gcc14-gnat/lib/gnatcoll_projects.static/libgnatcoll_projects.a /usr/pkg/gcc14-gnat/lib/gnatcoll_core.static/libgnatcoll_core.a /usr/pkg/gcc14-gnat/lib/gnatcoll_minimal.static/libgnatcoll_minimal.a /usr/pkg/gcc14-gnat/lib/gpr/static/gpr/libgnatprj.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_schema.static/libxmlada_schema.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_dom.static/libxmlada_dom.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_sax.static/libxmlada_sax.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_input.static/libxmlada_input_sources.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_unicode.static/libxmlada_unicode.a -lrt -liconv -lgmp -Wl,-R$ORIGIN -L/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0 -Wl,-R/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0 -L/usr/pkg/gcc14-gnat/lib -Wl,-R/usr/pkg/gcc14-gnat/lib -Wl,-zrelro -L/usr/pkg/lib -Wl,-R/usr/pkg/lib -L/usr/lib -Wl,-R/usr/lib -L/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib -L/pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/ -L/pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/ -L/usr/pkg/gcc14-gnat/lib/gpr/static/gpr/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_schema.static/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_sax.static/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_unicode.static/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_input.static/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_dom.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_projects.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_minimal.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_core.static/ -L/usr/pkg/gcc14-gnat/lib/gpr2.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_gmp.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_iconv.static/ -L/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib/ -static-libgcc /usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib/libgnarl.a /usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib/libgnat.a -pthread -o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/install/bin//spark_report link of gnatprove.adb failed failed command was: /pbulk/work/lang/spark2014-14/work/.buildlink/bin/gcc gnatprove.o b__gnatprove.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/gnat2why_opts.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/named_semaphores.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/platform.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/spark2014vsn.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/string_utils.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/call.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/vc_kinds.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/gnat2why_opts-writing.o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/configuration.o libgnatprove.a /usr/pkg/gcc14-gnat/lib/gpr2.static/libgpr2.a /usr/pkg/gcc14-gnat/lib/gnatcoll_iconv.static/libgnatcoll_iconv.a /usr/pkg/gcc14-gnat/lib/gnatcoll_gmp.static/libgnatcoll_gmp.a /usr/pkg/gcc14-gnat/lib/gnatcoll_projects.static/libgnatcoll_projects.a /usr/pkg/gcc14-gnat/lib/gnatcoll_core.static/libgnatcoll_core.a /usr/pkg/gcc14-gnat/lib/gnatcoll_minimal.static/libgnatcoll_minimal.a /usr/pkg/gcc14-gnat/lib/gpr/static/gpr/libgnatprj.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_schema.static/libxmlada_schema.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_dom.static/libxmlada_dom.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_sax.static/libxmlada_sax.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_input.static/libxmlada_input_sources.a /usr/pkg/gcc14-gnat/lib/xmlada/xmlada_unicode.static/libxmlada_unicode.a -lrt -liconv -lgmp -Wl,-R$ORIGIN -L/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0 -Wl,-R/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0 -L/usr/pkg/gcc14-gnat/lib -Wl,-R/usr/pkg/gcc14-gnat/lib -Wl,-zrelro -L/usr/pkg/lib -Wl,-R/usr/pkg/lib -L/usr/lib -Wl,-R/usr/lib -L/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib -L/pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/ -L/pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/obj/ -L/usr/pkg/gcc14-gnat/lib/gpr/static/gpr/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_schema.static/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_sax.static/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_unicode.static/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_input.static/ -L/usr/pkg/gcc14-gnat/lib/xmlada/xmlada_dom.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_projects.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_minimal.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_core.static/ -L/usr/pkg/gcc14-gnat/lib/gpr2.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_gmp.static/ -L/usr/pkg/gcc14-gnat/lib/gnatcoll_iconv.static/ -L/usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib/ -static-libgcc /usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib/libgnarl.a /usr/pkg/gcc14-gnat/lib/gcc/x86_64--netbsd/14.3.0/adalib/libgnat.a -pthread -o /pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/install/bin//gnatprove gprbuild: *** link phase failed gmake[1]: *** [Makefile.gnatprove:9: build] Error 4 gmake[1]: Leaving directory '/pbulk/work/lang/spark2014-14/work/spark2014-fsf-14' gmake: *** [Makefile:182: gnatprove] Error 2 gmake: *** Waiting for unfinished jobs.... Linking bin/why3webserver.cmxs Ocamlopt src/why3doc/doc_main.ml File "src/gnat/gnat_loc.ml", line 45, characters 21-39: 45 | let compare_simple = Pervasives.compare ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlopt plugins/tptp/tptp_lexer.ml Ocamlopt src/why3session/why3session_main.ml Ocamlopt src/gnat/gnat_expl.ml Linking bin/why3doc.cmxs File "src/gnat/gnat_expl.ml", line 165, characters 10-28: 165 | let c = Pervasives.compare a.id b.id in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims File "src/gnat/gnat_expl.ml", line 167, characters 7-25: 167 | else Pervasives.compare a.reason b.reason ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims File "src/gnat/gnat_expl.ml", line 170, characters 2-16: 170 | Pervasives.(=) a.id b.id && Pervasives.(=) a.reason b.reason ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims File "src/gnat/gnat_expl.ml", line 170, characters 30-44: 170 | Pervasives.(=) a.id b.id && Pervasives.(=) a.reason b.reason ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlopt plugins/microc/mc_lexer.ml Ocamlopt src/gnat/gnat_config.ml Linking bin/why3session.cmxs Linking bin/why3extract.cmxs Ocamlopt plugins/microc/mc_main.ml Linking lib/plugins/tptp.cmxs Ocamlopt src/gnat/gnat_manual.ml Ocamlopt src/gnat/gnat_report.ml Ocamlopt plugins/python/py_lexer.ml File "src/gnat/gnat_report.ml", line 116, characters 36-37: 116 | | Some (Check_ce.RAC_not_done s) -> rcd_only_cntexmp_model ^ Warning 27 [unused-var-strict]: unused variable s. File "src/gnat/gnat_report.ml", line 196, characters 41-42: 196 | "timings", Record (List.map (fun (k,(v,n)) -> get_name k, StandardFloat v) l) ^ Warning 27 [unused-var-strict]: unused variable n. Ocamlopt src/gnat/gnat_objectives.ml Linking lib/plugins/gnat_json.cmxs File "src/gnat/gnat_objectives.ml", line 58, characters 2-26: 58 | val close : unit -> unit ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 32 [unused-value-declaration]: unused value close. Linking lib/plugins/microc.cmxs Ocamlopt plugins/python/py_main.ml Ocamlopt plugins/ada_terms/ada_lexer.ml Ocamlopt plugins/ada_terms/ada_main.ml Linking lib/plugins/ada_terms.cmxs [Ada] comperr.adb Ocamlopt src/gnat/gnat_main.ml [Ada] csets.adb [Ada] debug.adb [Ada] elists.adb Linking lib/plugins/python.cmxs [Ada] errout.adb Linking bin/gnatwhy3.opt [Ada] exp_cg.adb Ocamlopt plugins/cfg/cfg_lexer.ml [Ada] fmap.adb Ocamlopt plugins/cfg/cfg_main.ml [Ada] fname.adb Ocamlopt plugins/cfg/cfg_stackify.ml [Ada] fname-uf.adb Linking lib/plugins/cfg.cmxs gmake[1]: Leaving directory '/pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/why3' [Ada] frontend.adb [Ada] ghost.adb [Ada] gnatvsn.adb [Ada] inline.adb [Ada] lib.adb [Ada] lib-writ.adb [Ada] lib-xref.adb [Ada] namet.adb [Ada] nlists.adb [Ada] opt.adb [Ada] osint.adb [Ada] osint-c.adb [Ada] output.adb [Ada] par_sco.adb [Ada] prepcomp.adb [Ada] repinfo.adb [Ada] repinfo-input.adb [Ada] restrict.adb [Ada] rident.ads [Ada] rtsfind.adb [Ada] scos.adb [Ada] sem.adb [Ada] sem_ch12.adb [Ada] sem_ch13.adb [Ada] sem_ch8.adb [Ada] sem_elim.adb [Ada] sem_eval.adb [Ada] sem_prag.adb [Ada] sem_type.adb [Ada] set_targ.adb [Ada] sinfo.adb [Ada] sinfo-nodes.adb [Ada] sinput.adb [Ada] sinput-l.adb [Ada] snames.adb [Ada] sprint.adb [Ada] stringt.adb [Ada] stylesw.adb [Ada] targparm.adb [Ada] tbuild.adb [Ada] treepr.adb [Ada] ttypes.ads [Ada] types.adb [Ada] uintp.adb [Ada] uname.adb [Ada] urealp.adb [Ada] usage.adb [Ada] validsw.adb [Ada] warnsw.adb [Ada] sinfo-utils.adb [Ada] alloc.ads [Ada] einfo.adb [Ada] einfo-entities.adb [Ada] einfo-utils.adb [Ada] seinfo.ads [Ada] table.adb [Ada] adabkend.adb [Ada] backend_utils.adb [Ada] erroutc.adb [Ada] gnat2why.ads [Ada] gnat2why-driver.adb [Ada] gnat2why_args.ads [Ada] gnat2why_opts.ads [Ada] spark_definition.adb [Ada] switch.adb [Ada] switch-c.adb [Ada] eval_fat.adb [Ada] exp_ch11.adb [Ada] exp_ch4.adb [Ada] exp_pakd.adb [Ada] exp_util.adb [Ada] expander.adb [Ada] freeze.adb [Ada] nmake.adb [Ada] sem_aux.adb [Ada] sem_cat.adb [Ada] sem_ch3.adb [Ada] sem_disp.adb [Ada] sem_mech.adb [Ada] sem_res.adb [Ada] sem_util.adb [Ada] sem_warn.adb [Ada] stand.ads [Ada] sdefault.adb [Ada] casing.adb [Ada] scans.adb [Ada] err_vars.ads [Ada] exp_dbug.adb [Ada] exp_tss.adb [Ada] krunch.adb [Ada] widechar.adb [Ada] cstand.adb [Ada] exp_ch6.adb [Ada] exp_unst.adb [Ada] lib-load.adb [Ada] live.adb [Ada] par.adb [Ada] prep.adb [Ada] scil_ll.adb [Ada] scn.adb [Ada] sem_elab.adb [Ada] sem_scil.adb [Ada] vast.adb [Ada] aspects.adb [Ada] exp_ch7.adb [Ada] sem_ch10.adb [Ada] ali.adb [Ada] gnat_cuda.adb [Ada] lib-util.adb [Ada] spark_xrefs.adb [Ada] hostparm.ads [Ada] put_scos.adb [Ada] exp_dist.adb [Ada] sem_ch7.adb [Ada] sem_dist.adb [Ada] debug_a.adb [Ada] exp_spark.adb [Ada] sem_attr.adb [Ada] sem_ch11.adb [Ada] sem_ch2.adb [Ada] sem_ch4.adb [Ada] sem_ch5.adb [Ada] sem_ch6.adb [Ada] sem_ch9.adb [Ada] contracts.adb [Ada] itypes.adb [Ada] sem_dim.adb [Ada] sinfo-cn.adb [Ada] accessibility.adb [Ada] exp_ch3.adb [Ada] exp_disp.adb [Ada] sem_case.adb [Ada] local_restrict.adb [Ada] impunit.adb [Ada] namet-sp.adb [Ada] style.adb [Ada] sem_aggr.adb [Ada] sem_intr.adb [Ada] strub.adb [Ada] get_targ.adb [Ada] sinput-d.adb [Ada] ali-util.adb [Ada] assumption_types.adb [Ada] binderr.adb [Ada] call.adb [Ada] ce_rac.adb [Ada] common_containers.adb [Ada] debug-timing.adb [Ada] flow.adb [Ada] flow-analysis.adb [Ada] flow-analysis-assumptions.adb [Ada] flow_error_messages.adb [Ada] flow_generated_globals.adb [Ada] flow_generated_globals-phase_1.adb [Ada] flow_generated_globals-phase_2.adb [Ada] flow_generated_globals-traversal.adb [Ada] flow_types.adb [Ada] flow_utility.adb [Ada] flow_visibility.adb [Ada] gnat2why-assumptions.adb [Ada] gnat2why-borrow_checker.adb [Ada] gnat2why-data_decomposition.adb [Ada] gnat2why-decls.adb [Ada] gnat2why-error_messages.adb [Ada] gnat2why-subprograms.adb [Ada] gnat2why-tables.adb [Ada] gnat2why-types.adb [Ada] gnat2why-util.adb [Ada] hashing.adb [Ada] outputs.adb [Ada] spark_definition-annotate.adb [Ada] spark_register.adb [Ada] spark_rewrite.adb [Ada] spark_util.adb [Ada] spark_util-hardcoded.adb [Ada] spark_util-subprograms.adb [Ada] spark_util-types.adb [Ada] string_utils.adb [Ada] tempdir.adb [Ada] vc_kinds.adb [Ada] why.ads [Ada] why-atree.ads [Ada] why-atree-modules.adb [Ada] why-atree-tables.adb [Ada] why-atree-to_json.adb [Ada] why-atree-treepr.adb [Ada] why-gen.ads [Ada] why-gen-binders.adb [Ada] why-gen-expr.adb [Ada] why-gen-names.adb [Ada] why-images.adb [Ada] why-inter.adb [Ada] gnat2why_opts-reading.adb [Ada] checked_types.ads [Ada] common_iterators.adb [Ada] flow_dependency_maps.adb [Ada] flow_utility-initialization.adb [Ada] spark_atree.adb [Ada] spark_atree-entities.adb [Ada] spark_definition-violations.adb [Ada] exp_intr.adb [Ada] exp_aggr.adb [Ada] exp_ch9.adb [Ada] exp_fixd.adb [Ada] layout.adb [Ada] exp_attr.adb [Ada] exp_ch12.adb [Ada] exp_ch13.adb [Ada] exp_ch2.adb [Ada] exp_ch5.adb [Ada] exp_ch8.adb [Ada] exp_prag.adb [Ada] sem_smem.adb [Ada] exp_code.adb [Ada] exp_atag.adb [Ada] scng.adb [Ada] styleg.adb [Ada] exp_put_image.adb [Ada] butil.adb [Ada] exp_strm.adb [Ada] exp_smem.adb [Ada] sinput-c.adb [Ada] hash_cons.adb [Ada] ce_fuzzer.adb [Ada] ce_parsing.adb [Ada] ce_utils.adb [Ada] flow_refinement.adb [Ada] ce_values.adb [Ada] assumptions.adb [Ada] flow-control_dependence_graph.adb [Ada] flow-control_flow_graph.adb [Ada] flow-data_dependence_graph.adb [Ada] flow-interprocedural.adb [Ada] flow-program_dependence_graph.adb [Ada] flow-slice.adb [Ada] flow_classwide.adb [Ada] flow_debug.adb [Ada] flow_generated_globals-partial.adb [Ada] flow_sanity.adb [Ada] spark_frame_conditions.adb [Ada] flow-analysis-antialiasing.adb [Ada] flow-analysis-sanity.adb [Ada] ce_display.adb [Ada] gnat2why-expr.adb [Ada] gnat2why-expr-loops.adb [Ada] flow_generated_globals-phase_1-write.adb [Ada] spark2014vsn.adb [Ada] flow_generated_globals-ali_serialization.ads [Ada] flow_generated_globals-phase_2-read.adb [Ada] flow_generated_globals-phase_2-traversal.adb [Ada] flow_generated_globals-phase_2-visibility.adb [Ada] graphs.adb [Ada] why-atree-accessors.ads [Ada] why-atree-builders.adb [Ada] why-gen-decl.adb [Ada] why-gen-pointers.adb [Ada] why-ids.ads [Ada] why-sinfo.ads [Ada] why-types.ads [Ada] why-atree-mutators.adb [Ada] why-gen-arrays.adb [Ada] why-gen-init.adb [Ada] why-gen-progs.adb [Ada] why-gen-records.adb [Ada] why-conversions.ads [Ada] why-gen-terms.adb [Ada] gnat2why-expr-aggregates.adb [Ada] gnat2why-subprograms-pointers.adb [Ada] why-gen-hardcoded.adb [Ada] why-gen-scalars.adb [Ada] why-keywords.adb [Ada] pprint.adb [Ada] why-opaque_ids.ads [Ada] why-classes.ads [Ada] why-atree-traversal.adb [Ada] exp_sel.adb [Ada] exp_imgv.adb [Ada] flow-control_flow_graph-utility.adb [Ada] ce_interval_sets.adb [Ada] ce_pretty_printing.adb [Ada] gnat2why-expr-loops-inv.adb [Ada] why-unchecked_ids.ads [Ada] why-atree-validity.ads [Ada] why-kind_validity.ads Bind [gprbind] gnat1drv.bexch [Ada] gnat1drv.ali Link [archive] libgnat2why.a [index] libgnat2why.a [link] gnat1drv.adb gmake[1]: Leaving directory '/pbulk/work/lang/spark2014-14/work/spark2014-fsf-14/gnat2why' # (The timestamp of) src/why/xgen/gnat_ast.ml is updated every time `make` is called in # `gnat2why`, causing a recompilation of why3 every time because Why3's makefile is # based on timestamps not file content. So we check if anything changed before copying. SOURCE=src/why/xgen/gnat_ast.ml; TARGET=why3/plugins/gnat_json/gnat_ast.ml; \ cmp "$SOURCE" "$TARGET" || cp -pr $SOURCE $TARGET *** Error code 2 Stop. make[1]: stopped making "all" in /usr/pkgsrc/lang/spark2014-14 WARNING: *** Please consider adding c++ to USE_LANGUAGES in the package Makefile. WARNING: *** Please consider adding fortran to USE_LANGUAGES in the package Makefile. *** Error code 1 Stop. make: stopped making "all" in /usr/pkgsrc/lang/spark2014-14