=> 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-13-13.3.0 # Produce Ada code that stores the reserved keywords of Why3 /usr/pkg/bin/gmake -f Makefile.gnatprove build /usr/pkg/bin/gmake -C why3 -j gmake[1]: Entering directory '/tmp/lang/spark2014-13/work/spark2014-12db22e854defa9d1c993ef904af1e72330a68ca' gprbuild -p -j0 -P gnatprove.gpr # This script should be run *ONLY* in developer build not in prod gmake[1]: Entering directory '/tmp/lang/spark2014-13/work/spark2014-12db22e854defa9d1c993ef904af1e72330a68ca/why3' gmake[1]: warning: -j0 forced in submake: resetting jobserver mode. # (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_loc.ml cmp -s src/util/mysexplib-dummy.ml src/util/mysexplib.ml || cp src/util/mysexplib-dummy.ml src/util/mysexplib.ml cmp -s src/util/mlmpfr_dummy.ml src/util/mlmpfr_wrapper.ml || cp src/util/mlmpfr_dummy.ml src/util/mlmpfr_wrapper.ml cmp -s src/util/dynlink_new.ml src/util/dynlink_wrapper.ml || cp src/util/dynlink_new.ml src/util/dynlink_wrapper.ml cmp -s src/session/compress_z.ml src/session/compress.ml || cp src/session/compress_z.ml src/session/compress.ml Ocamldep src/gnat/gnat_counterexamples.ml cmp -s src/util/recompat.ml src/util/re.ml || cp src/util/recompat.ml src/util/re.ml Ocamldep src/gnat/gnat_config.ml Ocamldep src/gnat/gnat_expl.ml Ocamldep src/gnat/gnat_report.ml Ocamldep src/gnat/gnat_server.ml Ocamldep src/gnat/gnat_scheduler.ml Ocamldep src/gnat/gnat_main.ml Generate src/util/config.ml Ocamllex src/util/lexlib.mll Menhir src/parser/parser_common.mly Ocamldep src/gnat/gnat_objectives.ml Ocamldep src/gnat/gnat_manual.ml Ocamllex src/util/json_lexer.mll Ocamllex src/parser/lexer.mll Menhir src/util/json_parser.mly Ocamllex src/driver/sexp.mll Menhir src/driver/driver_parser.mly Menhir src/parser/parser_common.mly src/parser/parser.mly Ocamllex src/driver/driver_lexer.mll Ocamllex src/util/rc.mll Ocamllex src/session/strategy_parser.mll Ocamllex src/session/xml.mll /usr/pkg/bin/gmake -C gnat2why AUTOMATED=1 GPRARGS='-XBuild=Production' gmake[1]: Entering directory '/tmp/lang/spark2014-13/work/spark2014-12db22e854defa9d1c993ef904af1e72330a68ca/gnat2why' cmp -s src/tools/why3pp_sexp-dummy.ml src/tools/why3pp_sexp.ml || cp src/tools/why3pp_sexp-dummy.ml src/tools/why3pp_sexp.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_lexer.mli src/trywhy3/json_lexer.mli 27 states, 306 transitions, table size 1386 bytes 117 states, 1396 transitions, table size 6286 bytes 3556 additional bytes used for bindings /usr/pkg/bin/gmake -C ../src/why/xgen gmake[2]: Entering directory '/tmp/lang/spark2014-13/work/spark2014-12db22e854defa9d1c993ef904af1e72330a68ca/src/why/xgen' gprbuild -j0 -p -Phelpers xtree 174 states, 4831 transitions, table size 20368 bytes 9859 additional bytes used for bindings 39 states, 600 transitions, table size 2634 bytes 1338 additional bytes used for bindings Ocamllex plugins/tptp/tptp_lexer.mll Ocamllex plugins/parser/dimacs.mll 52 states, 495 transitions, table size 2292 bytes cp src/util/json_parser.ml src/trywhy3/json_parser.ml cp src/util/json_parser.mli src/trywhy3/json_parser.mli cp src/util/json_lexer.ml src/trywhy3/json_lexer.ml Ocamllex plugins/python/py_lexer.mll 34 states, 1366 transitions, table size 5668 bytes Ocamllex plugins/cfg/cfg_lexer.mll Menhir src/parser/parser_common.mly plugins/cfg/cfg_parser.mly Ocamllex src/tools/why3wc.mll 47 states, 678 transitions, table size 2994 bytes 2153 additional bytes used for bindings Menhir plugins/python/py_parser.mly Menhir plugins/microc/mc_parser.mly Ocamllex plugins/ada_terms/ada_lexer.mll Menhir plugins/ada_terms/ada_parser.mly Ocamllex plugins/microc/mc_lexer.mll Menhir plugins/tptp/tptp_parser.mly Ocamldep src/why3session/why3session_html.ml 48 states, 1889 transitions, table size 7844 bytes 3073 additional bytes used for bindings Ocamldep src/ide/wserver.ml Ocamldep src/tools/why3shell.ml Ocamldep src/why3session/why3session_main.ml Ocamldep src/isabelle-client/isabelle_client_main.ml Ocamllex src/why3doc/doc_lexer.mll Ocamldep src/why3session/why3session_lib.ml Ocamldep src/trywhy3/json_base.ml Ocamldep src/why3session/why3session_info.ml Ocamldep src/ide/why3web.ml Ocamldep src/trywhy3/json_parser.ml Ocamldep src/trywhy3/shortener.ml Ocamldep src/trywhy3/trywhy3.ml Ocamldep src/tools/why3pp_sexp.ml Ocamldep src/trywhy3/worker_proto.ml 77 states, 473 transitions, table size 2354 bytes 1504 additional bytes used for bindings Ocamldep src/trywhy3/json_lexer.ml Ocamldep src/tools/why3pp.ml Ocamldep src/trywhy3/bindings.ml Ocamldep src/trywhy3/why3_worker.ml 101 states, 1563 transitions, table size 6858 bytes 3126 additional bytes used for bindings 34 states, 434 transitions, table size 1940 bytes 1293 additional bytes used for bindings 171 states, 4814 transitions, table size 20282 bytes 9841 additional bytes used for bindings 67 states, 1307 transitions, table size 5630 bytes 1441 additional bytes used for bindings Ocamldep src/why3session/why3session_update.ml Ocamldep src/why3session/why3session_latex.ml Read 3 sample input sentences and 3 error messages. 120 states, 685 transitions, table size 3460 bytes 1763 additional bytes used for bindings 157 states, 3909 transitions, table size 16578 bytes 9757 additional bytes used for bindings 307 states, 15627 transitions, table size 64350 bytes 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/why3prove.ml Ocamldep src/tools/why3replay.ml Ocamldep src/tools/why3extract.ml Ocamldep src/tools/why3execute.ml Ocamldep src/tools/why3wc.ml Ocamldep src/tools/why3show.ml Ocamldep src/tools/why3realize.ml Ocamldep src/tools/why3config.ml Ocamldep src/why3doc/doc_html.ml Ocamldep src/why3doc/doc_lexer.ml Ocamldep src/why3doc/doc_main.ml Ocamldep src/why3doc/doc_def.ml Read 3 sample input sentences and 3 error messages. Ocamldep src/util/mysexplib.ml Ocamldep src/util/config.ml Ocamldep src/util/bigInt.ml Ocamldep src/util/mlmpfr_wrapper.ml Ocamldep src/util/opt.ml Ocamldep src/util/util.ml Ocamldep src/util/cmdline.ml Ocamldep src/util/exthtbl.ml Ocamldep src/util/dynlink_wrapper.ml Ocamldep src/core/decl.ml Ocamldep src/util/warning.ml Ocamldep src/util/json_parser.ml Ocamldep src/driver/driver.ml Ocamldep src/driver/driver_lexer.ml Ocamldep src/util/getopt.ml Ocamldep src/util/lexlib.ml Ocamldep src/util/pqueue.ml Ocamldep src/util/plugin.ml Ocamldep src/core/env.ml Ocamldep src/util/exn_printer.ml Ocamldep src/util/sysutil.ml Ocamldep src/core/ident.ml Ocamldep src/util/strings.ml Ocamldep src/driver/autodetection.ml Ocamldep src/core/ty.ml Ocamldep src/util/extmap.ml Ocamldep src/core/model_parser.ml Ocamldep src/util/wstdlib.ml Ocamldep src/driver/smtv2_model_parser.ml Ocamldep src/extract/compile.ml Ocamldep src/mlw/check_ce.ml Ocamldep src/util/diffmap.ml Ocamldep src/mlw/ity.ml Ocamldep src/mlw/dexpr.ml Ocamldep src/core/term.ml Ocamldep src/core/theory.ml Ocamldep src/util/rc.ml Ocamldep src/util/constant.ml Ocamldep src/util/print_tree.ml Ocamldep src/driver/prove_client.ml Ocamldep src/parser/report.ml Ocamldep src/transform/fold_defs.ml Ocamldep src/parser/mlw_printer.ml Ocamldep src/driver/sexp.ml Ocamldep src/mlw/vc.ml Ocamldep src/transform/eliminate_unknown_types.ml Ocamldep src/transform/abstract_quantifiers.ml Ocamldep src/mlw/eval_match.ml Ocamldep src/session/strategy.ml Ocamldep src/transform/simplify_formula.ml Ocamldep src/extract/pdriver.ml Ocamldep src/extract/ml_printer.ml Ocamldep src/transform/encoding_guards_full.ml Ocamldep src/mlw/expr.ml Ocamldep src/parser/ptree.ml Ocamldep src/util/vector.ml Ocamldep src/util/loc.ml Ocamldep src/transform/eliminate_symbol.ml Ocamldep src/driver/whyconf.ml Ocamldep src/core/pattern.ml Ocamldep src/util/number.ml Ocamldep src/extract/cakeml.ml Ocamldep src/driver/call_provers.ml Ocamldep src/transform/cut.ml Ocamldep src/transform/subst.ml Ocamldep src/core/pretty.ml Ocamldep src/util/extset.ml Ocamldep src/printer/coq.ml Ocamldep src/transform/encoding.ml Ocamldep src/mlw/pinterp_core.ml Ocamldep src/transform/congruence.ml Ocamldep src/util/weakhtbl.ml Ocamldep src/mlw/typeinv.ml Ocamldep src/extract/mlinterp.ml Ocamldep src/util/json_base.ml Ocamldep src/transform/abstraction.ml Ocamldep src/transform/eliminate_if.ml Ocamldep src/parser/lexer.ml Ocamldep plugins/microc/mc_lexer.ml Ocamldep src/session/itp_server.ml Ocamldep src/session/xml.ml Ocamldep src/transform/compute.ml Ocamldep src/mlw/pmodule.ml Ocamldep src/transform/eliminate_unknown_lsymbols.ml Ocamldep src/transform/gnat_trivial.ml Ocamldep src/extract/c.ml Ocamldep src/mlw/pinterp.ml Ocamldep src/transform/reduction_engine.ml Ocamldep src/transform/case.ml Ocamldep src/transform/induction.ml Ocamldep plugins/tptp/tptp_printer.ml Ocamldep src/transform/split_goal.ml Ocamldep src/util/re.ml Ocamldep src/mlw/big_real.ml Ocamldep src/core/dterm.ml Ocamldep plugins/tptp/tptp_parser.ml Ocamldep src/transform/simplify_array.ml Ocamldep src/transform/inlining.ml Ocamldep src/session/termcode.ml Ocamldep src/mlw/pdecl.ml Ocamldep src/printer/alt_ergo.ml Ocamldep src/core/task.ml Ocamldep src/parser/typing.ml Ocamldep src/transform/destruct.ml Ocamldep src/transform/discriminate.ml Ocamldep src/printer/cvc3.ml Ocamldep src/driver/collect_data_model.ml Ocamldep src/printer/simplify.ml Ocamldep src/transform/encoding_tags.ml Ocamldep src/session/server_utils.ml Ocamldep src/transform/ind_itp.ml Ocamldep src/session/compress.ml Ocamldep src/driver/smtv2_model_defs.ml Ocamldep src/printer/isabelle.ml Ocamldep src/transform/eliminate_literal.ml Ocamldep src/printer/pvs.ml Ocamldep src/extract/ocaml.ml Ocamldep src/session/session_itp.ml Ocamldep src/transform/gnat_rewrite.ml Ocamldep src/transform/libencoding.ml Ocamldep src/core/coercion.ml Ocamldep src/transform/gnat_split_disj.ml Ocamldep src/printer/yices.ml Ocamldep src/transform/introduction.ml Ocamldep src/transform/instantiate_predicate.ml Ocamldep src/parser/parser_messages.ml Ocamldep src/transform/reflection.ml Ocamldep src/transform/smoke_detector.ml Ocamldep src/core/parser_tokens.ml Ocamldep src/transform/apply.ml Ocamldep src/printer/gappa.ml Ocamldep plugins/parser/dimacs.ml Ocamldep src/transform/intro_projections_counterexmp.ml Ocamldep src/transform/eliminate_epsilon.ml Ocamldep src/core/trans.ml Ocamldep src/util/pp.ml Ocamldep src/printer/why3printer.ml Ocamldep src/transform/eliminate_let.ml Ocamldep src/transform/remove_unused.ml Ocamldep src/transform/filter_trigger.ml Ocamldep src/transform/eliminate_unused.ml Ocamldep src/session/unix_scheduler.ml Ocamldep src/transform/close_epsilon.ml Ocamldep src/session/json_util.ml Ocamldep src/session/controller_itp.ml Ocamldep plugins/microc/mc_parser.ml Ocamldep src/parser/parser.ml Ocamldep src/parser/ptree_helpers.ml Ocamldep src/transform/eliminate_inductive.ml Ocamldep src/transform/encoding_twin.ml Ocamldep src/transform/encoding_select.ml Ocamldep src/transform/eliminate_definition.ml Ocamldep src/core/printer.ml Ocamldep plugins/python/py_main.ml Ocamldep plugins/cfg/cfg_ast.mli Ocamldep src/extract/mltree.ml Ocamldep plugins/tptp/tptp_lexer.ml Ocamldep src/transform/detect_polymorphism.ml Ocamldep src/transform/induction_pr.ml Ocamldep src/util/debug.ml Ocamldep src/util/hashcons.ml Ocamldep src/transform/encoding_sort.ml Ocamldep src/transform/lift_epsilon.ml Ocamldep src/util/json_lexer.ml Ocamldep src/transform/prop_curry.ml Ocamldep src/transform/intro_vc_vars_counterexmp.ml Ocamldep src/transform/eliminate_quantifiers.ml Ocamldep src/session/itp_communication.ml Ocamldep src/core/keywords.ml Ocamldep src/util/lists.ml Ocamldep src/mlw/rac.ml Ocamldep src/session/strategy_parser.ml Ocamldep plugins/ada_terms/ada_parser.ml Ocamldep src/transform/eliminate_algebraic.ml Ocamldep src/transform/eliminate_unused_hypo.ml Ocamldep src/transform/args_wrapper.ml Ocamldep src/printer/mathematica.ml Ocamldep src/parser/glob.ml Ocamldep src/transform/encoding_tags_full.ml Ocamldep plugins/parser/genequlin.ml Ocamldep src/driver/driver_parser.ml Ocamldep src/transform/rec_logic.ml Ocamldep plugins/gnat_json/gnat_ast.ml Ocamldep src/printer/smtv2.ml Ocamldep src/printer/cntexmp_printer.ml Ocamldep src/transform/gnat_split_conj.ml Ocamldep src/printer/smtv1.ml Ocamldep src/transform/prepare_for_counterexmp.ml Ocamldep src/transform/encoding_guards.ml Ocamldep src/driver/driver_ast.mli Ocamldep plugins/tptp/tptp_typing.ml Ocamldep plugins/cfg/cfg_main.ml Ocamldep src/transform/generic_arg_trans_utils.ml Ocamldep plugins/tptp/tptp_ast.mli Ocamldep plugins/python/py_lexer.ml Ocamldep plugins/gnat_json/gnat_ast_to_ptree.ml Ocamldep plugins/microc/mc_printer.ml Ocamldep plugins/gnat_json/ptree_constructors.ml Ocamldep plugins/cfg/cfg_parser.ml Ocamldep plugins/python/py_ast.mli Ocamldep plugins/cfg/cfg_lexer.ml Ocamldep plugins/microc/mc_main.ml Ocamldep plugins/python/py_parser.ml Ocamldep plugins/ada_terms/ada_main.ml Ocamldep plugins/ada_terms/ada_nametable.ml Ocamldep plugins/ada_terms/ada_lexer.ml Ocamldep plugins/gnat_json/gnat_ast_pretty.ml Ocamldep plugins/microc/mc_ast.mli Ocamldep plugins/cfg/cfg_paths.ml Ocamldep plugins/cfg/cfg_stackify.ml Ocamldep plugins/cfg/stackify.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 /tmp/lang/spark2014-13/work/spark2014-12db22e854defa9d1c993ef904af1e72330a68ca/src/common/semaphores_c.c: In function '__netbsd_sem_name': /tmp/lang/spark2014-13/work/spark2014-12db22e854defa9d1c993ef904af1e72330a68ca/src/common/semaphores_c.c:35:16: warning: implicit declaration of function 'strlen' [-Wimplicit-function-declaration] 35 | size_t len = strlen (name); | ^~~~~~ /tmp/lang/spark2014-13/work/spark2014-12db22e854defa9d1c993ef904af1e72330a68ca/src/common/semaphores_c.c:32:1: note: include '' or provide a declaration of 'strlen' 31 | #include +++ |+#include 32 | /tmp/lang/spark2014-13/work/spark2014-12db22e854defa9d1c993ef904af1e72330a68ca/src/common/semaphores_c.c:35:16: warning: incompatible implicit declaration of built-in function 'strlen' [-Wbuiltin-declaration-mismatch] 35 | size_t len = strlen (name); | ^~~~~~ /tmp/lang/spark2014-13/work/spark2014-12db22e854defa9d1c993ef904af1e72330a68ca/src/common/semaphores_c.c:35:16: note: include '' or provide a declaration of 'strlen' /tmp/lang/spark2014-13/work/spark2014-12db22e854defa9d1c993ef904af1e72330a68ca/src/common/semaphores_c.c:45:3: warning: implicit declaration of function 'strcpy' [-Wimplicit-function-declaration] 45 | strcpy (p, name); | ^~~~~~ /tmp/lang/spark2014-13/work/spark2014-12db22e854defa9d1c993ef904af1e72330a68ca/src/common/semaphores_c.c:45:3: note: include '' or provide a declaration of 'strcpy' /tmp/lang/spark2014-13/work/spark2014-12db22e854defa9d1c993ef904af1e72330a68ca/src/common/semaphores_c.c:45:3: warning: incompatible implicit declaration of built-in function 'strcpy' [-Wbuiltin-declaration-mismatch] /tmp/lang/spark2014-13/work/spark2014-12db22e854defa9d1c993ef904af1e72330a68ca/src/common/semaphores_c.c:45:3: note: include '' or provide a declaration of 'strcpy' [C] colors.c [Ada] named_semaphores.adb Setup [mkdir] object directory for project Helpers Compile [Ada] xtree.adb [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 [Ada] why.ads [Ada] why-sinfo.ads [Ada] xkind_tables.adb [Ada] outputs.adb [Ada] xtree_tables.adb [Ada] cache_client.ads [Ada] filecache_client.adb [Ada] memcache_client.adb [Ada] call.adb [Ada] xtree_classes.adb mkdir lib/plugins 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 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 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 Ocamlc src/util/weakhtbl.mli Ocamlc src/driver/prove_client.mli Ocamlc src/transform/remove_unused.mli Ocamlc src/transform/encoding_twin.mli Ocamlc src/transform/induction.mli Ocamlc src/printer/smtv1.mli Ocamlc plugins/parser/dimacs.mli Ocamlc src/why3session/why3session_main.mli Ocamlc src/util/util.mli Ocamlc src/tools/main.mli Ocamlc src/util/lists.mli Ocamlc plugins/gnat_json/gnat_ast.ml Ocamlc src/util/lexlib.mli Ocamlc src/util/re.ml Ocamlc src/parser/parser_messages.mli Ocamlc src/transform/lift_epsilon.mli Ocamlc src/printer/smtv2.mli [Ada] string_utils.adb Ocamlc plugins/parser/genequlin.mli Ocamlc src/tools/why3config.mli Ocamlc src/tools/why3pp.mli Ocamlc src/tools/why3wc.mli Ocamlc src/util/mysexplib.ml Ocamlc src/util/strings.mli Ocamlc src/util/exthtbl.mli Generate drivers/pvs-realizations.aux Ocamlc src/extract/cakeml.mli Linking src/util/ppx_debug_optim Ocamlc src/printer/pvs.mli Ocamlc src/transform/encoding_select.mli Ocamlc src/printer/simplify.mli Ocamlc src/tools/why3replay.mli Ocamlc src/isabelle-client/isabelle_client_main.mli Ocamlc src/ide/why3web.mli Ocamlc src/printer/yices.mli Ocamlc src/util/cmdline.mli Ocamlc src/transform/encoding_guards_full.mli Ocamlc src/tools/why3prove.mli Ocamlc src/transform/encoding_tags_full.mli findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /usr/pkg/lib/ocaml, /usr/pkg/lib/ocaml/compiler-libs Ocamlc src/transform/instantiate_predicate.mli File "src/util/re.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/gnat/gnat_scheduler.mli Ocamlc plugins/python/py_main.mli Ocamlc src/session/xml.mli Ocamlc src/session/compress.mli Ocamlc src/transform/case.mli Ocamlc src/extract/ocaml.mli Ocamlc src/util/config.mli Ocamlc src/printer/why3printer.mli Ocamlc plugins/microc/mc_main.mli Ocamlc src/tools/why3show.mli Ocamlc src/transform/prop_curry.mli Ocamlc src/transform/encoding_tags.mli Ocamlc plugins/tptp/tptp_printer.mli Ocamlc src/util/mlmpfr_wrapper.mli Ocamlc src/transform/encoding_sort.mli Ocamlc src/transform/eliminate_unknown_lsymbols.mli Ocamlc src/transform/congruence.mli Ocamlc src/session/unix_scheduler.mli Ocamlopt src/util/re.ml Ocamlc src/transform/abstract_quantifiers.mli Ocamlc src/util/lists.ml Ocamlc src/why3doc/doc_main.mli Ocamlc src/transform/simplify_array.mli Ocamlc src/transform/induction_pr.mli Ocamlc src/printer/mathematica.mli Ocamlc src/util/loc.mli Ocamlc src/ide/wserver.mli Ocamlc src/driver/sexp.mli Ocamlc src/why3doc/doc_html.mli Ocamlc src/util/hashcons.mli Ocamlc src/transform/filter_trigger.mli Ocamlc src/tools/why3execute.mli Ocamlc src/why3doc/doc_lexer.mli Ocamlc src/printer/alt_ergo.mli Generate drivers/isabelle-realizations.aux Ocamlc src/util/sysutil.mli Ocamlc src/transform/eliminate_unknown_types.mli Ocamlc src/util/pp.mli Ocamlc src/tools/why3shell.mli Ocamlc src/mlw/big_real.mli Ocamlc src/util/json_base.mli Ocamlc src/driver/smtv2_model_parser.mli Ocamlc src/util/strings.ml Ocamlc src/util/getopt.mli Ocamlc src/transform/encoding_guards.mli Ocamlc src/printer/cvc3.mli Ocamlc src/printer/isabelle.mli Ocamlc src/printer/gappa.mli Ocamlc src/util/print_tree.mli Ocamlc src/tools/why3realize.mli Ocamlc src/transform/eliminate_symbol.mli Ocamlc src/util/vector.mli File "src/util/util.mli", line 126, characters 22-52: 126 | val ansi_color_tags : Format.formatter_tag_functions ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Alert deprecated: Stdlib.Format.formatter_tag_functions Use formatter_stag_functions. Ocamlc src/util/exn_printer.mli Ocamlc src/transform/gnat_split_disj.mli Ocamlc src/tools/why3extract.mli Ocamlc src/util/bigInt.mli Ocamlc src/printer/coq.mli Ocamlc src/parser/parser_messages.ml Ocamlopt src/parser/parser_messages.ml Ocamlc src/extract/c.mli Ocamlopt src/util/lists.ml Ocamlc src/util/opt.mli Ocamlc src/util/dynlink_wrapper.mli File "src/util/mysexplib.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/util/pqueue.mli Ocamlopt src/util/mysexplib.ml Ocamlc src/util/extmap.mli Generate drivers/coq-realizations.aux Ocamlc src/util/weakhtbl.ml Ocamlc src/util/exthtbl.ml Ocamlc src/session/compress.ml Ocamlopt src/util/weakhtbl.ml Ocamlopt src/session/compress.ml Ocamlc src/session/unix_scheduler.ml Ocamlopt src/util/strings.ml Ocamlc src/util/mlmpfr_wrapper.ml Ocamlopt src/session/unix_scheduler.ml Ocamlopt src/util/mlmpfr_wrapper.ml Ocamlopt src/util/exthtbl.ml Ocamlopt src/util/util.ml Ocamlopt src/util/print_tree.ml Ocamlc src/util/dynlink_wrapper.ml Ocamlc src/util/getopt.ml Ocamlc src/util/diffmap.mli Ocamlc src/util/print_tree.ml Ocamlopt src/util/config.ml File "src/ide/wserver.mli", line 71, characters 35-43: 71 | val get_request_and_content : char Stream.t -> string list * string ^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. Ocamlopt src/util/opt.ml Ocamlc src/util/util.ml Ocamlc src/util/hashcons.ml Ocamlc src/util/opt.ml Ocamlc src/driver/prove_client.ml Ocamlc src/util/extset.mli File "src/session/compress_z.ml", line 44, characters 23-33: 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/util/pp.mli", line 122, characters 33-51: 122 | ('b, formatter, unit, string) Pervasives.format4 -> 'b ^^^^^^^^^^^^^^^^^^ 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/util/pp.mli", line 125, characters 33-51: 125 | ('b, formatter, unit, string) Pervasives.format4 -> 'b ^^^^^^^^^^^^^^^^^^ 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 Ocamlc src/util/extmap.ml Ocamlc src/driver/sexp.ml Ocamlc src/util/pqueue.ml Ocamlopt src/util/dynlink_wrapper.ml Ocamlopt src/util/hashcons.ml Ocamlopt src/driver/sexp.ml Ocamlc src/util/json_base.ml Ocamlc src/util/config.ml Ocamlc src/util/exn_printer.ml Ocamlopt src/util/vector.ml Ocamlc src/util/bigInt.ml Ocamlopt src/util/exn_printer.ml Ocamlopt src/gnat/gnat_scheduler.ml Ocamlc src/util/vector.ml Ocamlopt src/util/json_base.ml Ocamlopt src/util/extmap.ml Ocamlc src/util/number.mli Ocamlc src/util/cmdline.ml Ocamlc src/util/json_parser.mli Ocamlc src/mlw/big_real.ml Ocamlopt src/util/bigInt.ml File "src/util/weakhtbl.ml", line 98, characters 13-19: 98 | let iter = H.iter ^^^^^^ Alert old_ephemeron_api: H.iter This function won't be available in 5.0 File "src/util/weakhtbl.ml", line 99, characters 13-19: 99 | let fold = H.fold ^^^^^^ Alert old_ephemeron_api: H.fold This function won't be available in 5.0 File "src/util/weakhtbl.ml", line 101, characters 19-25: 101 | let iterk fn t = H.iter (fun k _ -> fn k) t ^^^^^^ Alert old_ephemeron_api: H.iter This function won't be available in 5.0 File "src/util/weakhtbl.ml", line 102, characters 19-25: 102 | let foldk fn t = H.fold (fun k _ -> fn k) t ^^^^^^ Alert old_ephemeron_api: H.fold This function won't be available in 5.0 Ocamlc src/util/wstdlib.mli Ocamlc src/gnat/gnat_loc.mli Ocamlc src/util/debug.mli 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. Ocamlc src/util/sysutil.ml Ocamlc src/util/pp.ml gcc -Wall -o lib/why3cpulimit src/server/cpulimit-unix.o src/server/cpulimit-win.o Ocamlc src/util/extset.ml Ocamlopt src/util/pp.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. 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/util/constant.mli Ocamlc src/util/warning.mli Ocamlc src/util/json_lexer.mli File "src/session/compress_z.ml", line 44, characters 23-33: 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/util/weakhtbl.ml", line 98, characters 13-19: 98 | let iter = H.iter ^^^^^^ Alert old_ephemeron_api: H.iter This function won't be available in 5.0 File "src/util/weakhtbl.ml", line 99, characters 13-19: 99 | let fold = H.fold ^^^^^^ Alert old_ephemeron_api: H.fold This function won't be available in 5.0 File "src/util/weakhtbl.ml", line 101, characters 19-25: 101 | let iterk fn t = H.iter (fun k _ -> fn k) t ^^^^^^ Alert old_ephemeron_api: H.iter This function won't be available in 5.0 File "src/util/weakhtbl.ml", line 102, characters 19-25: 102 | let foldk fn t = H.fold (fun k _ -> fn k) t ^^^^^^ Alert old_ephemeron_api: H.fold This function won't be available in 5.0 Ocamlc src/util/lexlib.ml Ocamlc src/util/json_parser.ml Ocamlc src/driver/driver_ast.mli Ocamlc src/core/ident.mli Ocamlc src/core/parser_tokens.mli 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. Ocamlopt src/mlw/big_real.ml Ocamlc src/driver/driver_parser.mli Ocamlc src/driver/driver_lexer.mli Ocamlc src/core/parser_tokens.ml Ocamlopt src/util/json_parser.ml [Ada] utils.adb Ocamlc src/util/json_lexer.ml Ocamlc src/util/constant.ml File "plugins/gnat_json/gnat_ast.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/util/warning.ml Ocamlc src/util/diffmap.ml Ocamlopt src/util/cmdline.ml Ocamlc src/util/wstdlib.ml Ocamlc src/util/rc.mli Ocamlopt src/util/pqueue.ml Ocamlc src/driver/driver_lexer.ml Ocamlc src/util/plugin.mli Ocamlc src/util/debug.ml Ocamlc src/util/number.ml Ocamlc src/session/xml.ml Ocamlc src/util/loc.ml File "src/util/constant.ml", line 26, characters 33-51: 26 | let c = if structural then Pervasives.compare k1 k2 else 0 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/util/constant.ml", line 29, characters 33-51: 29 | let c = if structural then Pervasives.compare k1 k2 else 0 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/util/constant.ml", line 32, characters 6-24: 32 | Pervasives.compare c1 c2 ^^^^^^^^^^^^^^^^^^ 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 Ocamlc src/core/ty.mli Ocamlc src/driver/driver_parser.ml Ocamlc src/core/ident.ml Ocamlc src/util/rc.ml Ocamlc src/parser/glob.mli File "src/util/debug.ml", line 121, characters 21-39: 121 | (List.sort Pervasives.compare list); ^^^^^^^^^^^^^^^^^^ 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 src/util/getopt.ml Ocamlopt src/driver/prove_client.ml Ocamlc src/parser/glob.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/loc.ml", line 72, characters 14-32: 72 | let compare = 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 File "src/util/loc.ml", line 73, characters 12-26: 73 | let equal = Pervasives.(=) ^^^^^^^^^^^^^^ 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/util/loc.ml", lines 51-52, characters 0-20: 51 | type expanded_position = string * int * int * int * int 52 | [@@deriving sexp_of] Warning 34 [unused-type-declaration]: unused type expanded_position. File "src/util/loc.ml", line 54, characters 4-20: 54 | let sexp_of_position loc = ^^^^^^^^^^^^^^^^ Warning 32 [unused-value-declaration]: unused value sexp_of_position. Ocamlc src/util/plugin.ml Ocamlopt src/util/sysutil.ml Ocamlopt src/util/json_lexer.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. Ocamlopt src/util/extset.ml Ocamlopt src/util/diffmap.ml File "_none_", line 1: Warning 58 [no-cmx-file]: no cmx file was found in path for module Pp, and its interface was not compiled with -opaque Ocamlc src/core/term.mli Ocamlc src/core/ty.ml Ocamlc src/core/pattern.mli Ocamlc src/transform/close_epsilon.mli Ocamlc src/mlw/ity.mli Ocamlc src/core/term.ml Ocamlc src/printer/cntexmp_printer.mli Ocamlc src/core/decl.mli Ocamlc src/core/coercion.mli Bind [gprbind] xtree.bexch [Ada] xtree.ali [Ada] configuration.adb [Ada] gnat2why_opts.ads Ocamlc src/core/dterm.mli Ocamlc src/core/coercion.ml [Ada] gnat2why_opts-writing.adb Link [link] xtree.adb File "src/core/term.ml", line 281, characters 39-57: 281 | let perv_compare h1 h2 = comp_raise (Pervasives.compare h1 h2) 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 ./xtree 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 '/tmp/lang/spark2014-13/work/spark2014-12db22e854defa9d1c993ef904af1e72330a68ca/src/why/xgen' mkdir -p obj obj-gnat obj-gnat2why obj-tools ../install/bin sed -e "s^@ADAINCLUDE@^/tmp/lang/spark2014-13/work/.buildlink/lib/gcc/x86_64--netbsd/13.4.0/adainclude /usr/pkg/gcc13-gnat/lib/gcc/x86_64--netbsd/13.4.0/adainclude^" \ -e "s^@ADALIB@^/usr/pkg/gcc13-gnat/lib/gcc/x86_64--netbsd/13.4.0/adalib^" \ -e "s^@PREFIX@^/tmp/lang/spark2014-13/work/.buildlink/lib/gcc/x86_64--netbsd/13.4.0/adainclude /usr/pkg/gcc13-gnat/^" \ -e "s^@GNAT1DIR@^/tmp/lang/spark2014-13/work/.buildlink/lib/gcc/x86_64--netbsd/13.4.0/ /usr/pkg/gcc13-gnat/lib/gcc/x86_64--netbsd/13.4.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/pattern.ml Ocamlc src/core/decl.ml Ocamlc src/core/theory.mli Ocamlopt src/util/wstdlib.ml Ocamlc src/printer/cntexmp_printer.ml Ocamlc src/mlw/expr.mli Ocamlopt plugins/gnat_json/gnat_ast.ml Ocamlc plugins/gnat_json/gnat_ast_pretty.mli Ocamlc src/parser/ptree.ml Ocamlc src/mlw/pdecl.mli Ocamlc src/core/task.mli Ocamlc src/transform/detect_polymorphism.mli Ocamlc src/core/theory.ml Ocamlc src/transform/eliminate_literal.mli Ocamlc src/core/env.mli Ocamlopt src/util/debug.ml Ocamlopt src/util/rc.ml Ocamlc src/mlw/eval_match.mli Ocamlc src/mlw/typeinv.mli File "src/parser/ptree.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/mlw/eval_match.ml Ocamlc src/mlw/typeinv.ml Ocamlc src/parser/mlw_printer.mli Ocamlc src/parser/ptree_helpers.mli Ocamlc src/session/termcode.mli Ocamlc src/core/pretty.mli Ocamlc src/core/task.ml File "src/util/debug.ml", line 121, characters 21-39: 121 | (List.sort Pervasives.compare list); ^^^^^^^^^^^^^^^^^^ 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 src/util/loc.ml Ocamlopt src/util/number.ml Ocamlopt src/session/xml.ml Ocamlopt src/util/plugin.ml File "src/util/loc.ml", line 72, characters 14-32: 72 | let compare = 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 File "src/util/loc.ml", line 73, characters 12-26: 73 | let equal = Pervasives.(=) ^^^^^^^^^^^^^^ 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/util/loc.ml", lines 51-52, characters 0-20: 51 | type expanded_position = string * int * int * int * int 52 | [@@deriving sexp_of] Warning 34 [unused-type-declaration]: unused type expanded_position. File "src/util/loc.ml", line 54, characters 4-20: 54 | let sexp_of_position loc = ^^^^^^^^^^^^^^^^ Warning 32 [unused-value-declaration]: unused value sexp_of_position. Ocamlc src/mlw/pmodule.mli Ocamlc src/mlw/expr.ml Ocamlc src/mlw/pdecl.ml Ocamlc src/parser/mlw_printer.ml File "src/core/theory.ml", line 472, characters 4-12: 472 | let print_id fmt id = Ident.print_decoded fmt id.id_string ^^^^^^^^ Warning 32 [unused-value-declaration]: unused value print_id. Ocamlc src/driver/whyconf.mli Ocamlopt src/util/lexlib.ml Ocamlc src/parser/ptree_helpers.ml Ocamlc src/mlw/ity.ml Ocamlopt src/util/warning.ml Ocamlc src/transform/reduction_engine.mli Ocamlopt src/core/ident.ml Ocamlc src/core/dterm.ml Ocamlc src/core/trans.mli Ocamlc src/core/env.ml Ocamlc src/driver/autodetection.mli Ocamlc src/session/strategy.mli Ocamlc src/driver/autodetection.ml Ocamlc src/driver/whyconf.ml Ocamlc src/core/printer.mli Ocamlc src/transform/simplify_formula.mli Ocamlc src/transform/inlining.mli Ocamlc src/transform/eliminate_algebraic.mli Ocamlc src/transform/eliminate_inductive.mli Ocamlc src/transform/subst.mli Ocamlc src/transform/gnat_split_conj.mli Ocamlc src/transform/eliminate_unused.mli Ocamlc src/transform/apply.mli Ocamlc src/transform/eliminate_if.mli Ocamlc src/transform/eliminate_let.mli Ocamlc src/transform/prop_curry.ml Ocamlc src/transform/lift_epsilon.ml Ocamlc src/transform/gnat_rewrite.mli Ocamlc src/transform/smoke_detector.mli Ocamlc src/transform/generic_arg_trans_utils.mli Ocamlc src/core/trans.ml Ocamlc src/transform/split_goal.mli Ocamlc src/transform/simplify_array.ml Ocamlc src/transform/remove_unused.ml Ocamlc src/mlw/vc.mli Ocamlc src/transform/instantiate_predicate.ml Ocamlc src/transform/abstraction.mli Ocamlc src/transform/congruence.ml Ocamlc src/transform/close_epsilon.ml Ocamlc src/transform/detect_polymorphism.ml Ocamlc src/transform/compute.mli Ocamlc src/transform/eliminate_epsilon.mli Ocamlc src/transform/cut.mli Ocamlc src/transform/eliminate_symbol.ml Ocamlc src/transform/args_wrapper.mli Ocamlc src/transform/intro_vc_vars_counterexmp.mli Ocamlc src/transform/eliminate_definition.mli Ocamlc src/transform/rec_logic.ml Ocamlc src/transform/destruct.mli Ocamlc src/transform/intro_projections_counterexmp.mli Ocamlc src/transform/reflection.mli Ocamlc src/transform/prepare_for_counterexmp.mli Ocamlc src/transform/eliminate_unused_hypo.ml Ocamlc src/transform/libencoding.mli Ocamlc src/transform/encoding.mli Ocamlc src/transform/abstract_quantifiers.ml Ocamlc src/session/termcode.ml Ocamlc src/transform/eliminate_quantifiers.ml Ocamlc src/transform/introduction.mli Ocamlc src/transform/eliminate_if.ml Ocamlc src/mlw/pmodule.ml Ocamlc src/mlw/vc.ml Ocamlc src/transform/split_goal.ml Ocamlc src/transform/gnat_split_disj.ml Ocamlc src/printer/pvs.ml Ocamlc src/transform/abstraction.ml Ocamlc src/transform/fold_defs.ml Ocamlc src/transform/eliminate_inductive.ml Ocamlc src/printer/coq.ml Ocamlc src/session/strategy_parser.mli Ocamlc src/transform/eliminate_unused.ml Ocamlc src/mlw/dexpr.mli Ocamlc src/transform/simplify_formula.ml Ocamlc src/core/model_parser.mli Ocamlc src/transform/eliminate_unknown_lsymbols.ml Ocamlc src/transform/eliminate_unknown_types.ml Ocamlc src/transform/encoding_sort.ml Ocamlc src/transform/eliminate_algebraic.ml Ocamlc src/session/strategy.ml Ocamlc src/transform/reduction_engine.ml Ocamlc src/core/printer.ml Ocamlc src/transform/eliminate_let.ml Ocamlc src/mlw/pinterp_core.mli Ocamlc src/transform/generic_arg_trans_utils.ml Ocamlc src/printer/isabelle.ml Ocamlc src/parser/parser.mli Ocamlc src/parser/lexer.mli Ocamlc src/transform/discriminate.mli Ocamlc src/transform/smoke_detector.ml Ocamlc src/printer/mathematica.ml File "src/transform/rec_logic.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. [Ada] assumption_types.adb Ocamlc src/transform/filter_trigger.ml Ocamlc src/extract/mltree.mli Ocamlc src/extract/mlinterp.mli Ocamlc src/transform/gnat_split_conj.ml Ocamlc src/transform/gnat_rewrite.ml Ocamlc src/transform/eliminate_epsilon.ml Ocamlc src/printer/gappa.ml Ocamlopt src/core/parser_tokens.ml File "src/transform/eliminate_unused_hypo.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. File "src/transform/eliminate_quantifiers.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/transform/eliminate_literal.ml Ocamlc src/transform/libencoding.ml Ocamlopt src/util/constant.ml Ocamlc src/transform/encoding_guards_full.ml Ocamlc src/transform/introduction.ml Ocamlc src/transform/encoding_guards.ml Ocamlc src/transform/encoding_twin.ml File "src/transform/fold_defs.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/transform/encoding_tags.ml Ocamlc src/transform/encoding_tags_full.ml Ocamlc src/core/model_parser.ml Ocamlc src/extract/compile.mli Ocamlc src/driver/smtv2_model_defs.mli Ocamlc src/transform/encoding.ml Ocamlc src/session/strategy_parser.ml Ocamlc src/extract/pdriver.mli Ocamlc src/driver/call_provers.mli Ocamlc src/core/keywords.mli Ocamlc src/parser/typing.mli Ocamlc src/printer/smtv1.ml File "src/util/constant.ml", line 26, characters 33-51: 26 | let c = if structural then Pervasives.compare k1 k2 else 0 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 Ocamlc src/transform/ind_itp.mli Ocamlc src/transform/apply.ml Ocamlc src/transform/cut.ml Ocamlc src/transform/discriminate.ml File "src/util/constant.ml", line 29, characters 33-51: 29 | let c = if structural then Pervasives.compare k1 k2 else 0 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/util/constant.ml", line 32, characters 6-24: 32 | Pervasives.compare c1 c2 ^^^^^^^^^^^^^^^^^^ 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 Ocamlc src/transform/gnat_trivial.ml Ocamlc src/transform/intro_vc_vars_counterexmp.ml Ocamlc src/printer/simplify.ml Ocamlc src/transform/compute.ml Ocamlc src/extract/mltree.ml Ocamlc src/transform/encoding_select.ml Ocamlc src/mlw/pinterp_core.ml Ocamlc src/printer/cvc3.ml Ocamlc src/mlw/dexpr.ml Ocamlc src/parser/report.mli Ocamlc src/transform/intro_projections_counterexmp.ml Ocamlc src/printer/yices.ml Ocamlc src/transform/reflection.ml Ocamlc src/transform/subst.ml Ocamlc src/transform/destruct.ml Ocamlc src/transform/case.ml Ocamlc src/extract/pdriver.ml File "src/session/termcode.ml", line 1116, characters 24-42: 1116 | let compare e1 e2 = Pervasives.compare e1.shape e2.shape 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 Ocamlc src/driver/driver.mli Ocamlc src/session/session_itp.mli Ocamlc src/driver/call_provers.ml Ocamlc src/extract/ml_printer.mli Ocamlc src/core/keywords.ml Ocamlc src/mlw/pinterp.mli Ocamlopt src/parser/glob.ml Ocamlopt src/core/ty.ml Ocamlc src/mlw/rac.mli Ocamlopt src/core/keywords.ml Ocamlc src/printer/why3printer.ml Ocamlc src/printer/alt_ergo.ml Ocamlc src/core/pretty.ml Ocamlc src/driver/driver.ml Ocamlc src/transform/inlining.ml Ocamlc src/transform/prepare_for_counterexmp.ml Ocamlc src/transform/eliminate_definition.ml Ocamlc src/printer/smtv2.ml Ocamlopt src/driver/driver_parser.ml File "src/transform/gnat_trivial.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. [Ada] assumptions.adb Ocamlc src/session/controller_itp.mli Ocamlc src/driver/smtv2_model_defs.ml File "src/driver/call_provers.ml", line 472, characters 22-34: 472 | let cmd, use_stdin, on_timelimit = ^^^^^^^^^^^^ Warning 27 [unused-var-strict]: unused variable on_timelimit. Ocamlc src/extract/ml_printer.ml Ocamlc src/extract/mlinterp.ml Ocamlc src/extract/compile.ml Ocamlc src/extract/c.ml Ocamlc src/mlw/pinterp.ml Ocamlc src/driver/collect_data_model.mli Ocamlc src/mlw/check_ce.mli Ocamlc src/extract/cakeml.ml Ocamlc src/transform/induction_pr.ml Ocamlc src/parser/report.ml Ocamlc src/session/session_itp.ml Ocamlc src/extract/ocaml.ml Ocamlc src/transform/induction.ml Ocamlc src/parser/typing.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. Ocamlc src/parser/parser.ml Ocamlc src/mlw/rac.ml Ocamlc src/transform/args_wrapper.ml Ocamlc src/session/itp_communication.mli Ocamlc src/parser/lexer.ml Ocamlc src/transform/ind_itp.ml Ocamlc src/session/controller_itp.ml Ocamlc src/mlw/check_ce.ml File "src/extract/c.ml", line 68, characters 4-22: 68 | | Cfloat of string ^^^^^^^^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Cfloat is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 69, characters 4-21: 69 | | Cchar of string ^^^^^^^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Cchar is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 44, characters 45-56: 44 | and unop = Unot | Ustar | Uaddr | Upreincr | Upostincr | Upredecr | Upostdecr ^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Upostincr is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 44, characters 68-79: 44 | and unop = Unot | Ustar | Uaddr | Upreincr | Upostincr | Upredecr | Upostdecr ^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Upostdecr is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 41, characters 59-64: 41 | and binop = Band | Bor | Beq | Bne | Bassign | Blt | Ble | Bgt | Bge ^^^^^ Warning 37 [unused-constructor]: constructor Bgt is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 29, characters 4-41: 29 | | Tunion of ident * (ident * ty) list ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Tunion is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 92, characters 4-28: 92 | | Dtypedef of ty * ident ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Dtypedef is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 83, characters 21-24: 83 | and include_kind = Sys | Proj (* include <...> vs. include "..." *) ^^^ Warning 37 [unused-constructor]: constructor Sys is never used to build values. (However, this constructor appears in patterns.) [Ada] assumptions-search.adb Ocamlc src/driver/smtv2_model_parser.ml Ocamlc src/driver/collect_data_model.ml File "src/mlw/dexpr.ml", line 1301, characters 4-28: 1301 | let attr_w_unmodified_var_no = ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 32 [unused-value-declaration]: unused value attr_w_unmodified_var_no. Ocamlc src/session/server_utils.mli Ocamlc src/session/itp_server.mli Ocamlc src/session/json_util.mli Ocamlc src/session/itp_communication.ml Ocamlopt src/core/term.ml Ocamlc src/session/json_util.ml File "src/core/term.ml", line 281, characters 39-57: 281 | let perv_compare h1 h2 = comp_raise (Pervasives.compare h1 h2) 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 Ocamlc src/session/server_utils.ml File "src/parser/typing.ml", line 482, characters 32-38: 482 | | Ptree.Tupdate ({ term_loc = e1_loc } as e1, fl) -> ^^^^^^ Warning 27 [unused-var-strict]: unused variable e1_loc. File "src/parser/typing.ml", line 1034, characters 32-38: 1034 | | Ptree.Eupdate ({ expr_loc = e1_loc } as e1, fl) -> ^^^^^^ Warning 27 [unused-var-strict]: unused variable e1_loc. Ocamlc src/session/itp_server.ml Ocamlopt src/driver/driver_lexer.ml Ocamlopt src/core/pattern.ml Ocamlopt src/core/coercion.ml [Ada] platform.adb [Ada] print_table.adb Ocamlopt src/core/decl.ml [Ada] report_database.adb [Ada] spark2014vsn.adb [Ada] vc_kinds.adb Ocamlopt src/core/theory.ml [Ada] hash_cons.adb File "src/core/theory.ml", line 472, characters 4-12: 472 | let print_id fmt id = Ident.print_decoded fmt id.id_string ^^^^^^^^ Warning 32 [unused-value-declaration]: unused value print_id. Ocamlopt src/core/task.ml Ocamlopt src/core/env.ml Ocamlopt src/driver/whyconf.ml Ocamlopt src/transform/reduction_engine.ml Ocamlopt src/core/pretty.ml Ocamlopt src/driver/autodetection.ml Ocamlopt src/session/strategy.ml Ocamlopt src/core/trans.ml Ocamlopt src/mlw/ity.ml Ocamlopt src/core/dterm.ml gprbuild -XBuild=Production -Pgnat2why -j0 -cargs -O2 -I/usr/pkg/include -I/usr/include -Dz_off_t=long -I/usr/pkg/gcc13-gnat/include -I/usr/pkg/gcc13-gnat/lib/gcc/x86_64--netbsd/13.4.0/include -I/usr/pkg/gcc13-gnat/lib/gcc/x86_64--netbsd/13.4.0/adainclude -largs -L/usr/pkg/gcc13-gnat/lib/gcc/x86_64--netbsd/13.4.0 -Wl,-R/usr/pkg/gcc13-gnat/lib/gcc/x86_64--netbsd/13.4.0 -L/usr/pkg/gcc13-gnat/lib -Wl,-R/usr/pkg/gcc13-gnat/lib -L/usr/pkg/lib -L/usr/lib -Wl,-R/usr/lib -Wl,-R/usr/pkg/lib -L/usr/pkg/gcc13-gnat/lib/gcc/x86_64--netbsd/13.4.0/adalib Ocamlopt src/core/printer.ml Ocamlopt src/transform/split_goal.ml Ocamlopt src/transform/remove_unused.ml Ocamlopt src/transform/simplify_formula.ml Ocamlopt src/transform/abstract_quantifiers.ml Ocamlopt src/transform/intro_projections_counterexmp.ml Ocamlopt src/transform/gnat_rewrite.ml Ocamlopt src/transform/eliminate_unused_hypo.ml Ocamlopt src/transform/eliminate_quantifiers.ml Ocamlopt src/transform/congruence.ml Ocamlopt src/transform/rec_logic.ml Ocamlopt src/transform/eliminate_epsilon.ml Ocamlopt src/transform/abstraction.ml Ocamlopt src/transform/generic_arg_trans_utils.ml Ocamlopt src/transform/detect_polymorphism.ml Ocamlopt src/session/strategy_parser.ml Ocamlopt src/transform/close_epsilon.ml Ocamlopt src/transform/eliminate_symbol.ml Ocamlopt src/transform/instantiate_predicate.ml Ocamlopt src/transform/prop_curry.ml Ocamlopt src/transform/eliminate_unused.ml Ocamlopt src/transform/smoke_detector.ml Ocamlopt src/transform/simplify_array.ml Ocamlopt src/transform/eliminate_let.ml Ocamlopt src/session/termcode.ml Ocamlopt src/transform/eliminate_inductive.ml File "src/session/termcode.ml", line 1116, characters 24-42: 1116 | let compare e1 e2 = Pervasives.compare e1.shape e2.shape 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 Ocamlopt src/transform/lift_epsilon.ml Ocamlopt src/mlw/expr.ml Ocamlopt src/printer/cntexmp_printer.ml Linking lib/why3/why3.cmo Ocamlopt src/transform/intro_vc_vars_counterexmp.ml Ocamlopt src/transform/fold_defs.ml Ocamlopt src/transform/eliminate_unknown_types.ml Ocamlopt src/printer/pvs.ml Ocamlopt src/printer/coq.ml Ocamlopt src/transform/eliminate_unknown_lsymbols.ml Ocamlopt src/transform/libencoding.ml Ocamlopt src/printer/isabelle.ml Ocamlopt src/transform/eliminate_algebraic.ml Ocamlopt src/transform/eliminate_if.ml Ocamlopt src/core/model_parser.ml Ocamlopt src/printer/mathematica.ml Ocamlopt src/transform/encoding_sort.ml Ocamlopt src/transform/filter_trigger.ml Ocamlopt src/transform/gnat_split_conj.ml Ocamlopt src/transform/gnat_split_disj.ml Ocamlopt src/transform/encoding.ml Ocamlopt src/transform/eliminate_literal.ml Ocamlopt src/transform/encoding_guards_full.ml Ocamlopt src/transform/encoding_twin.ml Ocamlopt src/transform/encoding_tags_full.ml Ocamlopt src/transform/encoding_guards.ml Ocamlopt src/transform/encoding_tags.ml Compile [Ada] gnat1drv.adb [C] smissing.c Ocamlopt src/driver/call_provers.ml Ocamlopt src/driver/smtv2_model_defs.ml Ocamlopt src/driver/collect_data_model.ml File "src/driver/call_provers.ml", line 472, characters 22-34: 472 | let cmd, use_stdin, on_timelimit = ^^^^^^^^^^^^ Warning 27 [unused-var-strict]: unused variable on_timelimit. Ocamlopt src/driver/smtv2_model_parser.ml Ocamlopt src/driver/driver.ml Ocamlopt src/mlw/pdecl.ml Ocamlopt src/parser/ptree.ml Ocamlopt src/parser/ptree_helpers.ml Ocamlopt src/parser/mlw_printer.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. Ocamlc plugins/python/py_ast.mli Ocamlc src/gnat/gnat_counterexamples.ml Ocamlc plugins/microc/mc_ast.mli Ocamlc plugins/tptp/tptp_ast.mli Ocamlc plugins/ada_terms/ada_parser.mli Ocamlc src/gnat/gnat_expl.mli Ocamlc plugins/gnat_json/ptree_constructors.mli Ocamlc plugins/microc/mc_printer.mli Ocamlc plugins/gnat_json/gnat_ast_to_ptree.mli Ocamlc plugins/ada_terms/ada_nametable.mli Ocamlc src/tools/why3pp_sexp.mli Ocamlc src/why3doc/doc_def.mli Ocamlc src/gnat/gnat_util.mli Ocamlc plugins/cfg/cfg_ast.mli Ocamlc src/why3session/why3session_lib.mli Ocamlc plugins/python/py_parser.mli Ocamlc src/gnat/gnat_config.mli Ocamlopt src/tools/why3pp_sexp.ml Ocamlc plugins/python/py_lexer.mli Ocamlc src/gnat/gnat_report.mli Ocamlc src/gnat/gnat_manual.mli Ocamlc src/why3session/why3session_html.mli Ocamlc src/why3session/why3session_update.mli Ocamlc src/why3session/why3session_info.mli Ocamlc plugins/tptp/tptp_lexer.mli Ocamlc src/why3session/why3session_latex.mli Ocamlc plugins/microc/mc_lexer.mli Ocamlc plugins/tptp/tptp_parser.mli Ocamlc src/gnat/gnat_server.ml Ocamlopt src/mlw/eval_match.ml Ocamlc plugins/microc/mc_parser.mli Ocamlc plugins/tptp/tptp_typing.mli Ocamlc plugins/ada_terms/ada_lexer.ml Ocamlc plugins/cfg/stackify.mli Ocamlc plugins/cfg/cfg_paths.mli Ocamlc plugins/cfg/cfg_main.mli Ocamlc plugins/cfg/cfg_parser.mli Ocamlc plugins/cfg/cfg_lexer.mli File "src/gnat/gnat_counterexamples.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. File "src/gnat/gnat_server.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc plugins/cfg/cfg_stackify.ml Ocamlc src/gnat/gnat_objectives.mli File "plugins/ada_terms/ada_lexer.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. File "plugins/cfg/cfg_stackify.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. 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. Ocamlc src/gnat/gnat_main.ml Ocamlc plugins/ada_terms/ada_main.ml Ocamlopt src/mlw/typeinv.ml File "src/gnat/gnat_main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. [Ada] atree.adb [Ada] back_end.adb [Ada] checks.adb [Ada] comperr.adb File "plugins/ada_terms/ada_main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/mlw/vc.ml [Ada] csets.adb [Ada] debug.adb [Ada] elists.adb [Ada] errout.adb [Ada] exp_cg.adb Ocamlopt src/mlw/pmodule.ml 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 Link [archive] libgnatprove.a [index] libgnatprove.a [link] gnatprove.adb [link] spark_report.adb [link] spark_memcached_wrapper.adb [link] spark_semaphore_wrapper.adb Ocamlopt src/mlw/dexpr.ml Ocamlopt src/mlw/pinterp_core.ml gmake[1]: Leaving directory '/tmp/lang/spark2014-13/work/spark2014-12db22e854defa9d1c993ef904af1e72330a68ca' File "src/mlw/dexpr.ml", line 1301, characters 4-28: 1301 | 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/extract/mltree.ml Ocamlopt src/parser/typing.ml File "src/parser/typing.ml", line 482, characters 32-38: 482 | | Ptree.Tupdate ({ term_loc = e1_loc } as e1, fl) -> ^^^^^^ Warning 27 [unused-var-strict]: unused variable e1_loc. File "src/parser/typing.ml", line 1034, characters 32-38: 1034 | | Ptree.Eupdate ({ expr_loc = e1_loc } as e1, fl) -> ^^^^^^ Warning 27 [unused-var-strict]: unused variable e1_loc. Ocamlopt src/extract/compile.ml Ocamlopt src/extract/pdriver.ml [Ada] fmap.adb Ocamlopt src/extract/ml_printer.ml [Ada] fname.adb [Ada] fname-uf.adb Ocamlopt src/extract/cakeml.ml Ocamlopt src/extract/ocaml.ml Ocamlopt src/mlw/check_ce.ml [Ada] frontend.adb Ocamlopt src/extract/mlinterp.ml Ocamlopt src/extract/c.ml Ocamlopt src/parser/parser.ml File "src/extract/c.ml", line 68, characters 4-22: 68 | | Cfloat of string ^^^^^^^^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Cfloat is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 69, characters 4-21: 69 | | Cchar of string ^^^^^^^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Cchar is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 44, characters 45-56: 44 | and unop = Unot | Ustar | Uaddr | Upreincr | Upostincr | Upredecr | Upostdecr ^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Upostincr is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 44, characters 68-79: 44 | and unop = Unot | Ustar | Uaddr | Upreincr | Upostincr | Upredecr | Upostdecr ^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Upostdecr is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 41, characters 59-64: 41 | and binop = Band | Bor | Beq | Bne | Bassign | Blt | Ble | Bgt | Bge ^^^^^ Warning 37 [unused-constructor]: constructor Bgt is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 29, characters 4-41: 29 | | Tunion of ident * (ident * ty) list ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Tunion is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 92, characters 4-28: 92 | | Dtypedef of ty * ident ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Dtypedef is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 83, characters 21-24: 83 | and include_kind = Sys | Proj (* include <...> vs. include "..." *) ^^^ Warning 37 [unused-constructor]: constructor Sys is never used to build values. (However, this constructor appears in patterns.) [Ada] ghost.adb [Ada] gnatvsn.adb [Ada] inline.adb [Ada] lib.adb [Ada] lib-writ.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/subst.ml Ocamlopt src/transform/cut.ml Ocamlopt src/transform/case.ml Ocamlopt src/transform/ind_itp.ml Ocamlopt src/transform/apply.ml [Ada] lib-xref.adb Ocamlopt src/transform/eliminate_definition.ml Ocamlopt src/transform/discriminate.ml Ocamlopt src/printer/gappa.ml Ocamlopt src/transform/introduction.ml Ocamlopt src/transform/destruct.ml Ocamlopt src/transform/induction.ml Ocamlopt src/transform/induction_pr.ml [Ada] namet.adb Ocamlopt src/transform/reflection.ml Ocamlopt src/printer/why3printer.ml Ocamlopt src/printer/simplify.ml Ocamlopt src/printer/alt_ergo.ml Ocamlopt src/printer/smtv2.ml Ocamlopt src/printer/smtv1.ml Ocamlopt src/printer/cvc3.ml Ocamlopt src/printer/yices.ml Ocamlopt src/transform/encoding_select.ml Ocamlopt src/transform/gnat_trivial.ml Ocamlopt src/transform/prepare_for_counterexmp.ml Ocamlopt src/session/session_itp.ml [Ada] nlists.adb Ocamlopt src/session/controller_itp.ml Ocamlopt src/session/itp_communication.ml Ocamlopt src/session/server_utils.ml Ocamlopt src/session/json_util.ml [Ada] opt.adb [Ada] osint.adb Ocamlopt src/session/itp_server.ml [Ada] osint-c.adb [Ada] output.adb [Ada] par_sco.adb Linking lib/why3/why3.cmx [Ada] prepcomp.adb File "lib/why3/why3.cmx", line 1: Error: File src/util/sysutil.cmx was compiled without access to the .cmx file for module Pp, which was produced by `ocamlopt -for-pack'. Please recompile src/util/sysutil.cmx with the correct `-I' option so that Pp.cmx is found. gmake[1]: *** [Makefile:441: lib/why3/why3.cmx] Error 2 gmake[1]: Leaving directory '/tmp/lang/spark2014-13/work/spark2014-12db22e854defa9d1c993ef904af1e72330a68ca/why3' gmake: *** [Makefile:89: why3] Error 2 gmake: *** Waiting for unfinished jobs.... [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] sdefault.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] alloc.ads [Ada] table.adb [Ada] einfo.adb [Ada] einfo-entities.adb [Ada] einfo-utils.adb [Ada] exp_dbug.adb [Ada] exp_tss.adb [Ada] sem_aux.adb [Ada] sem_disp.adb [Ada] sem_util.adb [Ada] sinfo-utils.adb [Ada] aspects.adb [Ada] seinfo.ads [Ada] krunch.adb [Ada] widechar.adb [Ada] casing.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] sem_warn.adb [Ada] vast.adb [Ada] scans.adb [Ada] stand.ads [Ada] err_vars.ads [Ada] nmake.adb [Ada] sem_res.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] sem_cat.adb [Ada] sem_ch3.adb [Ada] sem_mech.adb [Ada] hostparm.ads [Ada] ali.adb [Ada] gnat_cuda.adb [Ada] lib-util.adb [Ada] exp_ch7.adb [Ada] sem_ch10.adb [Ada] spark_xrefs.adb [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] exp_disp.adb [Ada] impunit.adb [Ada] namet-sp.adb [Ada] sem_dim.adb [Ada] sinfo-cn.adb [Ada] style.adb [Ada] sem_aggr.adb [Ada] contracts.adb [Ada] itypes.adb [Ada] get_targ.adb [Ada] accessibility.adb [Ada] exp_ch3.adb [Ada] sem_case.adb [Ada] sinput-d.adb [Ada] gnat2why_opts-reading.adb [Ada] sem_intr.adb [Ada] strub.adb [Ada] ali-util.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_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-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-inter.adb [Ada] assumption_types.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] layout.adb [Ada] exp_aggr.adb [Ada] exp_atag.adb [Ada] exp_ch9.adb [Ada] exp_intr.adb [Ada] scng.adb [Ada] styleg.adb [Ada] exp_code.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] exp_fixd.adb [Ada] butil.adb [Ada] exp_put_image.adb [Ada] exp_strm.adb [Ada] sem_smem.adb [Ada] sinput-c.adb [Ada] exp_smem.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_refinement.adb [Ada] flow_sanity.adb [Ada] spark_frame_conditions.adb [Ada] flow-analysis-antialiasing.adb [Ada] flow-analysis-sanity.adb [Ada] ce_fuzzer.adb [Ada] ce_parsing.adb [Ada] ce_utils.adb [Ada] ce_values.adb [Ada] ce_display.adb [Ada] gnat2why-expr.adb [Ada] gnat2why-expr-loops.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] 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] spark2014vsn.adb [Ada] why-atree-mutators.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-subprograms-pointers.adb [Ada] why-gen-arrays.adb [Ada] why-gen-hardcoded.adb [Ada] why-gen-scalars.adb [Ada] why-keywords.adb [Ada] why-opaque_ids.ads [Ada] pprint.adb [Ada] why-classes.ads [Ada] why-images.adb [Ada] why-atree-traversal.adb [Ada] hash_cons.adb [Ada] exp_imgv.adb [Ada] exp_sel.adb [Ada] flow-control_flow_graph-utility.adb [Ada] flow_generated_globals-phase_1.adb [Ada] why-unchecked_ids.ads [Ada] gnat2why-expr-loops-exits.adb [Ada] gnat2why-expr-loops-inv.adb [Ada] ce_interval_sets.adb [Ada] ce_pretty_printing.adb [Ada] why-atree-validity.ads [Ada] why-kind_validity.ads [Ada] flow_generated_globals-phase_1-write.adb Bind [gprbind] gnat1drv.bexch [Ada] gnat1drv.ali Link [archive] libgnat2why.a [index] libgnat2why.a [link] gnat1drv.adb gmake[1]: Leaving directory '/tmp/lang/spark2014-13/work/spark2014-12db22e854defa9d1c993ef904af1e72330a68ca/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 in /amd/pkgsrc/CHROOT/P/pkgsrc/lang/spark2014-13 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 in /amd/pkgsrc/CHROOT/P/pkgsrc/lang/spark2014-13