Mock Version: 1.1.4 Mock Version: 1.1.4 ENTER do(['bash', '--login', '-c', 'rpmbuild -bs --target x86_64 --nodeps builddir/build/SPECS/why.spec'], False, '/var/lib/mock/dist-f14-build-904151-132794/root/', None, 86400, True, 0, 419, 419, None, logger=) Executing command: ['bash', '--login', '-c', 'rpmbuild -bs --target x86_64 --nodeps builddir/build/SPECS/why.spec'] warning: Could not canonicalize hostname: x86-14.phx2.fedoraproject.org Building target platforms: x86_64 Building for target x86_64 Wrote: /builddir/build/SRPMS/why-2.26-1.fc14.src.rpm Child returncode was: 0 LEAVE do --> ENTER do(['bash', '--login', '-c', 'rpmbuild -bb --target x86_64 --nodeps builddir/build/SPECS/why.spec'], False, '/var/lib/mock/dist-f14-build-904151-132794/root/', None, 86400, True, 0, 419, 419, None, logger=) Executing command: ['bash', '--login', '-c', 'rpmbuild -bb --target x86_64 --nodeps builddir/build/SPECS/why.spec'] Building target platforms: x86_64 Building for target x86_64 Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.MqMJg6 + umask 022 + cd /builddir/build/BUILD + LANG=C + export LANG + unset DISPLAY + cd /builddir/build/BUILD + rm -rf why-2.26 + /usr/bin/gzip -dc /builddir/build/SOURCES/why-2.26.tar.gz + /bin/tar -xf - + STATUS=0 + '[' 0 -ne 0 ']' + cd why-2.26 + /bin/chmod -Rf a+rX,u+w,g-w,o-w . + echo 'Patch #0 (gwhy-2.26.patch):' Patch #0 (gwhy-2.26.patch): + /bin/cat /builddir/build/SOURCES/gwhy-2.26.patch + /usr/bin/patch -s -p1 --fuzz=0 Patch #1 (why-2.26-Makefile.in.patch): + echo 'Patch #1 (why-2.26-Makefile.in.patch):' + /bin/cat /builddir/build/SOURCES/why-2.26-Makefile.in.patch + /usr/bin/patch -s -p1 --fuzz=0 + cp -p /builddir/build/SOURCES/README.why-gwhy.Fedora /builddir/build/SOURCES/README.why-coq.Fedora /builddir/build/SOURCES/README.why /builddir/build/SOURCES/gwhy.desktop /builddir/build/SOURCES/gwhy-icon.png /builddir/build/SOURCES/min.mlw /builddir/build/SOURCES/min_why.why.result /builddir/build/SOURCES/caduceus.ps /builddir/build/SOURCES/krakatoa.pdf /builddir/build/SOURCES/jessie.desktop /builddir/build/SOURCES/div.pvs /builddir/build/SOURCES/rem.pvs /builddir/build/SOURCES/patch_jessie_pvs ./ + cp -p /usr/share/frama-c/Makefile.dynamic ./frama-c-plugin/ + exit 0 Executing(%build): /bin/sh -e /var/tmp/rpm-tmp.Pf4JjY + umask 022 + cd /builddir/build/BUILD + cd why-2.26 + LANG=C + export LANG + unset DISPLAY + sed -e 's/versions_ok = \["0\.91"\]/versions_ok = ["0.92.1"]/' -i tools/dpConfig.ml + sed -e 's/command = "pvs"/command = "pvs-sbcl"/' -e 's/PVS, (pvs, \["pvs"\]);/PVS, (pvs, ["pvs-sbcl" ; "pvs"]);/' -i tools/dpConfig.ml + sed -e 's/pvs /pvs-sbcl /' -i configure + CFLAGS='-O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic' + export CFLAGS + CXXFLAGS='-O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic' + export CXXFLAGS + FFLAGS='-O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m64 -mtune=generic -I/usr/lib64/gfortran/modules' + export FFLAGS ++ which pvs-sbcl + ./configure --build=x86_64-redhat-linux-gnu --host=x86_64-redhat-linux-gnu --program-prefix= --disable-dependency-tracking --prefix=/usr --exec-prefix=/usr --bindir=/usr/bin --sbindir=/usr/sbin --sysconfdir=/etc --datadir=/usr/share --includedir=/usr/include --libdir=/usr/lib64 --libexecdir=/usr/libexec --localstatedir=/var --sharedstatedir=/var/lib --mandir=/usr/share/man --infodir=/usr/share/info --disable-security_slicing --disable-aorai PVSC=/usr/bin/pvs-sbcl configure: WARNING: unrecognized options: --disable-dependency-tracking, --disable-security_slicing, --disable-aorai checking for ocamlc... ocamlc ocaml version is 3.11.2 ocaml library path is /usr/lib64/ocaml checking OS dependent settings... Unix checking for ocamlopt... ocamlopt checking ocamlopt version... ok checking for ocamlc.opt... ocamlc.opt checking ocamlc.opt version... ok checking for ocamlopt.opt... ocamlopt.opt checking ocamlc.opt version... ok checking for ocamldep... ocamldep checking for ocamldep.opt... ocamldep.opt checking for ocamllex... ocamllex checking for ocamllex.opt... ocamllex.opt checking for ocamlyacc... ocamlyacc checking for ocamldoc... true configure: WARNING: Cannot find ocamldoc checking for /usr/lib64/ocaml/ocamlgraph/graph.cmi... yes checking for /usr/lib64/ocaml/lablgtk2/lablgtk.cma... yes checking for ocamlweb... true checking for frama-c... frama-c checking Frama-c version... Boron-20100401 checking for camlp4o... camlp4o checking camlp4 version... ok checking for coqc... coqc checking for coqdep... coqdep checking Coq version... 8.2pl1 checking Coq floating-point library... no checking Coq Gappa library... no checking for pvs... /usr/bin/pvs-sbcl checking for mizf... no configure: WARNING: Cannot find Mizar. configure: creating ./config.status config.status: creating Makefile config.status: creating bench/bench configure: WARNING: unrecognized options: --disable-dependency-tracking, --disable-security_slicing, --disable-aorai Summary ----------------------------------------- OCaml version : 3.11.2 OCaml library path : /usr/lib64/ocaml OcamlGraph lib : in Ocaml lib, subdir ocamlgraph Verbose make : no Inference of annotations : no Frama-C plugin : yes Frama-C version : Boron-20100401 GWhy : yes Coq support : yes Version : v8 (8.2pl1) Lib : /usr/share/coq Floats : no (Coq library AllFloat.vo not found) Gappa : no (Coq library Gappa_tactic.vo not found) PVS support : yes Bin : /usr/bin/pvs-sbcl Lib : /usr/lib64/pvs/lib Mizar support : no Other provers support : at run-time (use why-config to configure) + sed -e 's/\"\/usr\/share\/coq\"/\$(DESTDIR)\/usr\/share\/coq\//' -i Makefile + make VERBOSEMAKE=yes OCAMLBEST=opt OCAMLOPT=ocamlopt.opt BINDIR=/usr/bin LIBDIR=/usr/lib64 COQVER=v8 ./version.sh ocamllex.opt src/rc.mll 39 states, 1677 transitions, table size 6942 bytes 1933 additional bytes used for bindings ocamllex.opt src/xml.mll 51 states, 1824 transitions, table size 7602 bytes 2541 additional bytes used for bindings ocamllex.opt src/lexer.mll 101 states, 1298 transitions, table size 5798 bytes 4632 additional bytes used for bindings ocamlyacc -v src/parser.mly ocamllex.opt src/linenum.mll 15 states, 323 transitions, table size 1382 bytes 1194 additional bytes used for bindings ocamllex.opt jc/numconst.mll 71 states, 764 transitions, table size 3482 bytes ocamllex.opt jc/jc_lexer.mll 494 states, 28850 transitions, table size 118364 bytes 10182 additional bytes used for bindings ocamlyacc -v jc/jc_parser.mly 1 shift/reduce conflict. if test "no" = "yes" ; then \ echo "# 1 \"jc/jc_annot_inference.ml\"" > jc/jc_ai.ml; \ cat jc/jc_annot_inference.ml >> jc/jc_ai.ml; \ else \ echo "# 1 \"jc/jc_annot_fail.ml\"" > jc/jc_ai.ml; \ cat jc/jc_annot_fail.ml >> jc/jc_ai.ml; \ fi ocamlyacc -v java/java_parser.mly ocamllex.opt java/java_lexer.mll 145 states, 1574 transitions, table size 7166 bytes 3721 additional bytes used for bindings ocamlyacc -v ml/parsing/parser.mly ocamllex.opt ml/parsing/lexer.mll 172 states, 3313 transitions, table size 14284 bytes 2252 additional bytes used for bindings ocamllex.opt ml/parsing/linenum.mll 12 states, 323 transitions, table size 1364 bytes ocamllex.opt c/clexer.mll 317 states, 15579 transitions, table size 64218 bytes 3110 additional bytes used for bindings ocamlyacc -v c/cparser.mly 1 shift/reduce conflict, 24 reduce/reduce conflicts. ocamllex.opt c/cllexer.mll 276 states, 15549 transitions, table size 63852 bytes ocamlyacc -v c/clparser.mly ocamllex.opt c/cpp.mll 105 states, 331 transitions, table size 1954 bytes ocamllex.opt c/cconst.mll 61 states, 574 transitions, table size 2662 bytes ocamllex.opt intf/hilight.mll 43 states, 532 transitions, table size 2386 bytes ocamllex.opt intf/whyhilight.mll 101 states, 6417 transitions, table size 26274 bytes ocamllex.opt intf/tagsplit.mll 9 states, 495 transitions, table size 2034 bytes ocamllex.opt intf/config.mll 14 states, 446 transitions, table size 1868 bytes ocamllex.opt tools/why2html.mll 82 states, 2034 transitions, table size 8628 bytes ocamllex.opt tools/cvcl_split.mll 18 states, 262 transitions, table size 1156 bytes ocamllex.opt tools/simplify_split.mll 38 states, 429 transitions, table size 1944 bytes ocamllex.opt tools/smtlib_split.mll 61 states, 455 transitions, table size 2186 bytes ocamllex.opt tools/rv_split.mll 65 states, 376 transitions, table size 1894 bytes ocamllex.opt tools/zenon_split.mll 37 states, 379 transitions, table size 1738 bytes ocamllex.opt tools/ergo_split.mll 41 states, 2642 transitions, table size 10814 bytes ocamllex.opt tools/simplify_lexer.mll 16 states, 364 transitions, table size 1552 bytes ocamlyacc -v tools/simplify_parser.mly ocamllex.opt tools/toolstat_lex.mll 223 states, 5431 transitions, table size 23062 bytes 11960 additional bytes used for bindings ocamlyacc -v tools/toolstat_pars.mly ocamllex.opt mix/mix_lexer.mll 65 states, 434 transitions, table size 2126 bytes ocamlyacc -v mix/mix_parser.mly rm -f .depend ocamldep.opt -slash -I src -I jc -I c -I java -I intf -I tools -I mix -I ml src/*.ml src/*.mli jc/*.mli jc/*.ml c/*.mli c/*.ml java/*.mli java/*.ml intf/*.ml intf/*.mli tools/*.mli tools/*.ml mix/*.mli mix/*.ml ml/*.ml ml/*.mli > .depend ocamldep.opt -slash -I ml/utils -I ml/parsing -I ml/typing ml/parsing/*.ml ml/parsing/*.mli ml/typing/*.ml ml/typing/*.mli ml/utils/*.ml ml/utils/*.mli >> .depend make -C frama-c-plugin depend make[1]: Entering directory `/builddir/build/BUILD/why-2.26/frama-c-plugin' /usr/share/frama-c/Makefile.dynamic:219: .depend: No such file or directory rm -f ./.depend ocamldep.opt -slash \ -I . -I "/usr/lib64/frama-c" \ ./*.mli ./*.ml \ ./Jessie.mli\ \ \ > ./.depend touch Jessie_DEP chmod a-w ./.depend rm -f ./.depend ocamldep.opt -slash \ -I . -I "/usr/lib64/frama-c" \ ./*.mli ./*.ml \ ./Jessie.mli\ \ \ > ./.depend chmod a-w ./.depend make[1]: Leaving directory `/builddir/build/BUILD/why-2.26/frama-c-plugin' ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/lib.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc src/lib.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/rc.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc src/rc.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/dpConfig.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/dpConfig.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/version.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/ident.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/logic.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/loc.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/effect.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/types.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/cc.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/ptree.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/ast.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/env.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/logic_decl.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/project.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/options.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/options.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/linenum.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/linenum.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc src/loc.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc src/ident.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc src/print_real.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc src/effect.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/pp.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc src/pp.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/option_misc.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc src/option_misc.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/misc.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/misc.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/error.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/parser.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc src/parser.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/lexer.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc src/lexer.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/report.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc src/report.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/env.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/mapenv.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/rename.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/rename.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/explain.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc src/explain.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/util.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/util.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/ltyping.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/ltyping.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/typing.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/typing.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/wp.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/wp.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/fastwp.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/fastwp.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/monadSig.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/monad.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/monad.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/mlize.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/mlize.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/red.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/red.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/log.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/vcg.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/vcg.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/predDefExpansor.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/predDefExpansor.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/encoding_mono_inst.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/encoding_mono_inst.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/encoding_rec.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/encoding_rec.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/encoding_pred.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/encoding_pred.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/encoding_strat.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/encoding_strat.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/encoding_mono.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/monomorph.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/monomorph.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/encoding.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/encoding.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/pvs.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/pvs.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/hol4.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/hol4.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/gappa.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/gappa.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/holl.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/holl.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/harvey.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/harvey.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/simplify.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/simplify.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/regen.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/regen.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/mizar.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/mizar.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/smtlib.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/smtlib.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/coq.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/coq.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/zenon.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/zenon.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/z3.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/z3.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/cvcl.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/cvcl.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/calldp.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/calldp.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/xml.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc src/xml.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc src/project.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/why3.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/why3.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/pretty.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/pretty.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/unionfind.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/theoryreducer.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/theory_filtering.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/hypotheses_filtering.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/dispatcher.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/dispatcher.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/isabelle.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/isabelle.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/ocaml.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/ocaml.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/main.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/why.ml ocamlopt.opt -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -o bin/why.opt unix.cmxa str.cmxa nums.cmxa graph.cmxa src/lib.cmx src/rc.cmx tools/dpConfig.cmx src/version.cmx src/options.cmx src/linenum.cmx src/loc.cmx src/ident.cmx src/print_real.cmx src/effect.cmx src/pp.cmx src/option_misc.cmx src/misc.cmx src/parser.cmx src/lexer.cmx src/report.cmx src/env.cmx src/mapenv.cmx src/rename.cmx src/explain.cmx src/util.cmx src/ltyping.cmx src/typing.cmx src/wp.cmx src/fastwp.cmx src/monad.cmx src/mlize.cmx src/red.cmx src/vcg.cmx src/predDefExpansor.cmx src/encoding_mono_inst.cmx src/encoding_rec.cmx src/encoding_pred.cmx src/encoding_strat.cmx src/encoding_mono.cmx src/monomorph.cmx src/encoding.cmx src/pvs.cmx src/hol4.cmx src/gappa.cmx src/holl.cmx src/harvey.cmx src/simplify.cmx src/regen.cmx src/mizar.cmx src/smtlib.cmx src/coq.cmx src/zenon.cmx src/z3.cmx src/cvcl.cmx tools/calldp.cmx src/xml.cmx src/project.cmx src/why3.cmx src/pretty.cmx src/unionfind.cmx src/theoryreducer.cmx src/theory_filtering.cmx src/hypotheses_filtering.cmx src/dispatcher.cmx src/isabelle.cmx src/ocaml.cmx src/main.cmx src/why.cmx strip bin/why.opt ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/whyConfig.ml ocamlopt.opt -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -o bin/why-config.opt unix.cmxa str.cmxa src/rc.cmx src/version.cmx tools/dpConfig.cmx tools/whyConfig.cmx strip bin/why-config.opt WHYLIB=lib bin/why.opt --no-pervasives -tc lib/why/prelude.why for f in lib/why/bool.why lib/why/integer.why lib/why/real.why lib/why/arrays.why lib/why/jessie.why lib/why/jessie_bitvectors.why lib/why/mybag.why lib/why/mix.why lib/why/floats_common.why lib/why/floats_strict.why lib/why/floats_full.why lib/why/floats_multi_rounding.why ; do \ WHYLIB=lib bin/why.opt -tc $f; \ done ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/output.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc jc/output.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cversion.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/coptions.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/coptions.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cutil.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cutil.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/ctypes.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/ctypes.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cerror.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/creport.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/creport.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/info.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/info.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cconst.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cconst.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/clogic.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cast.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cenv.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cenv.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cltyping.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cltyping.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/ctyping.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/ctyping.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cprint_graph.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cprint_graph.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cgraph.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cgraph.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cinit.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cinit.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cast_misc.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cast_misc.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/clparser.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/clparser.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cllexer.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cparser.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cparser.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/clexer.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cprint.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cprint.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cnorm.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cnorm.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cseparation.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cseparation.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/invariant.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/invariant.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/ceffect.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/ceffect.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cinterp.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cinterp.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cpp.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cpp.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cmake.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cmake.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cabsint.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cptr.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cptr.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/csymbol.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph c/cmain.ml ocamlopt.opt \ -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -o bin/caduceus.opt unix.cmxa str.cmxa graph.cmxa src/lib.cmx src/linenum.cmx src/loc.cmx src/pp.cmx src/option_misc.cmx src/version.cmx jc/output.cmx c/cversion.cmx c/coptions.cmx c/cutil.cmx c/ctypes.cmx c/info.cmx c/creport.cmx c/cconst.cmx c/cenv.cmx c/cltyping.cmx c/ctyping.cmx c/cprint_graph.cmx c/cgraph.cmx c/cinit.cmx c/cast_misc.cmx c/clparser.cmx c/cllexer.cmx c/cparser.cmx c/clexer.cmx c/cprint.cmx c/cnorm.cmx c/cseparation.cmx c/invariant.cmx c/ceffect.cmx c/cinterp.cmx c/cpp.cmx c/cmake.cmx c/cabsint.cmx c/cptr.cmx c/csymbol.cmx c/cmain.cmx strip bin/caduceus.opt ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_env.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_common_options.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc jc/jc_common_options.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc jc/jc_stdlib.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_stdlib.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_envset.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc jc/jc_envset.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc jc/jc_region.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_region.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_ast.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc jc/jc_fenv.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_fenv.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_constructors.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc jc/jc_constructors.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_pervasives.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc jc/jc_pervasives.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_iterators.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc jc/jc_iterators.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_type_var.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc jc/jc_type_var.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc jc/jc_output_misc.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc jc/jc_poutput.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc jc/jc_output.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -for-pack Jc jc/jc_noutput.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_options.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_options.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_name.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_struct_tools.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_struct_tools.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_norm.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_norm.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_typing.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_typing.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/numconst.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/numconst.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_parser.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_parser.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_lexer.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_lexer.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_separation.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_callgraph.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_callgraph.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_effect.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_ai.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_ai.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_interp_misc.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_interp_misc.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_invariants.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_pattern.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_interp.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_interp.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_frame.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_frame.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_make.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_main.ml ocamlopt.opt -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -I atp -o bin/jessie.opt \ unix.cmxa str.cmxa nums.cmxa graph.cmxa src/version.cmx src/lib.cmx src/rc.cmx src/loc.cmx src/ident.cmx src/print_real.cmx src/effect.cmx src/pp.cmx src/option_misc.cmx src/parser.cmx src/lexer.cmx src/report.cmx src/explain.cmx src/xml.cmx src/project.cmx jc/output.cmx jc/jc_common_options.cmx jc/jc_stdlib.cmx jc/jc_envset.cmx jc/jc_region.cmx jc/jc_fenv.cmx jc/jc_constructors.cmx jc/jc_pervasives.cmx jc/jc_iterators.cmx jc/jc_type_var.cmx jc/jc_output_misc.cmx jc/jc_poutput.cmx jc/jc_output.cmx jc/jc_noutput.cmx jc/jc_options.cmx jc/jc_name.cmx jc/jc_struct_tools.cmx jc/jc_norm.cmx jc/jc_typing.cmx jc/numconst.cmx jc/jc_parser.cmx jc/jc_lexer.cmx jc/jc_separation.cmx jc/jc_callgraph.cmx jc/jc_effect.cmx jc/jc_ai.cmx jc/jc_interp_misc.cmx jc/jc_invariants.cmx jc/jc_pattern.cmx jc/jc_interp.cmx jc/jc_frame.cmx jc/jc_make.cmx jc/jc_main.cmx strip bin/jessie.opt ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph java/java_env.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph java/java_options.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph java/java_ast.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph java/java_tast.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph java/java_pervasives.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph java/java_abstract.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph java/java_parser.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph java/java_parser.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph java/java_lexer.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph java/java_syntax.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph java/java_typing.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph java/java_typing.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph java/java_callgraph.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph java/java_callgraph.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph java/java_analysis.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph java/java_interp.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph java/java_main.ml ocamlopt.opt -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -o bin/krakatoa.opt \ unix.cmxa nums.cmxa graph.cmxa src/lib.cmx src/version.cmx src/loc.cmx src/pp.cmx src/option_misc.cmx jc/output.cmx jc/jc_stdlib.cmx jc/jc_envset.cmx jc/jc_common_options.cmx jc/jc_region.cmx jc/jc_fenv.cmx jc/numconst.cmx jc/jc_constructors.cmx jc/jc_pervasives.cmx jc/jc_name.cmx jc/jc_iterators.cmx jc/jc_type_var.cmx jc/jc_output_misc.cmx jc/jc_poutput.cmx jc/jc_output.cmx jc/jc_noutput.cmx java/java_options.cmx java/java_pervasives.cmx java/java_abstract.cmx java/java_parser.cmx java/java_lexer.cmx java/java_syntax.cmx java/java_typing.cmx java/java_callgraph.cmx java/java_analysis.cmx java/java_interp.cmx java/java_main.cmx strip bin/krakatoa.opt coqc -I lib/coq lib/coq/WhyInt.v coqc -I lib/coq lib/coq/WhyArrays.v coqc -I lib/coq lib/coq/WhyBool.v coqc -I lib/coq lib/coq/WhyTuples.v coqc -I lib/coq lib/coq/WhyPermut.v coqc -I lib/coq lib/coq/WhyCoqCompat.v coqc -I lib/coq lib/coq/WhySorted.v coqc -I lib/coq lib/coq/WhyExn.v coqc -I lib/coq lib/coq/WhyLemmas.v coqc -I lib/coq lib/coq/WhyTactics.v coqc -I lib/coq lib/coq/WhyPrelude.v coqc -I lib/coq lib/coq/WhyCM.v coqc -I lib/coq lib/coq/Why.v coqc -I lib/coq lib/coq/WhyReal.v WHYLIB=lib bin/why.opt --dir lib/coq --coq-v8 lib/why/caduceus.why coqc -I lib/coq lib/coq/caduceus_why.v coqc -I lib/coq lib/coq/caduceus_tactics.v coqc -I lib/coq lib/coq/caduceus_lists.v coqc -I lib/coq lib/coq/Caduceus.v WHYLIB=lib bin/why.opt --dir lib/coq --coq-v8 lib/why/jessie.why coqc -I lib/coq lib/coq/jessie_why.v ocamlopt.opt -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -o bin/why2html.opt tools/why2html.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/cvcl_split.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/cvcl_split.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/simplify_split.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/simplify_split.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/smtlib_split.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/zenon_split.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/zenon_split.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/ergo_split.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/ergo_split.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/rv_split.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/dp.ml ocamlopt.opt -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -o bin/why-dp.opt unix.cmxa str.cmxa src/lib.cmx tools/cvcl_split.cmx tools/simplify_split.cmx tools/smtlib_split.cmx tools/zenon_split.cmx tools/ergo_split.cmx tools/rv_split.cmx src/rc.cmx tools/dpConfig.cmx src/version.cmx tools/calldp.cmx tools/dp.cmx cc -o bin/why-cpulimit tools/cpulimit.c ocamlopt.opt -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -o bin/rv_merge.opt tools/rv_merge.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/obfuscator.ml ocamlopt.opt -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -o bin/why-obfuscator.opt nums.cmxa src/pp.cmx src/loc.cmx src/ident.cmx src/parser.cmx src/lexer.cmx src/print_real.cmx tools/obfuscator.cmx ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/simplify_ast.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/simplify_parser.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/simplify_parser.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/simplify_lexer.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/simplify_towhy.ml ocamlopt.opt -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -o bin/simplify2why.opt src/ident.cmx src/pp.cmx tools/simplify_parser.cmx tools/simplify_lexer.cmx tools/simplify_towhy.cmx ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/whystat.ml ocamlopt.opt -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -o bin/why-stat.opt src/pp.cmx src/loc.cmx src/ident.cmx src/parser.cmx src/lexer.cmx tools/whystat.cmx ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/toolstat_types.mli ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/toolstat_pars.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/toolstat_pars.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/toolstat_lex.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph tools/toolstat.ml ocamlopt.opt -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -o bin/tool-stat.opt src/loc.cmx src/pp.cmx tools/toolstat_pars.cmx tools/toolstat_lex.cmx tools/toolstat.cmx ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/colors.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/colors.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/tags.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/tools.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/tagsplit.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/astprinter.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/astnprinter.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/astpprinter.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/model.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/model.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/cache.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/gConfig.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/gConfig.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/hilight.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/whyhilight.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/tags.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/pprinter.mli ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/pprinter.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/preferences.ml ocamlopt.opt -I atp -c -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph intf/stat.ml ocamlopt.opt -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -o bin/gwhy.opt unix.cmxa threads.cmxa nums.cmxa str.cmxa graph.cmxa lablgtk.cmxa gtkThread.cmx src/lib.cmx src/rc.cmx tools/dpConfig.cmx src/version.cmx src/options.cmx src/linenum.cmx src/loc.cmx src/ident.cmx src/print_real.cmx src/effect.cmx src/pp.cmx src/option_misc.cmx src/misc.cmx src/parser.cmx src/lexer.cmx src/report.cmx src/env.cmx src/mapenv.cmx src/rename.cmx src/explain.cmx src/util.cmx src/ltyping.cmx src/typing.cmx src/wp.cmx src/fastwp.cmx src/monad.cmx src/mlize.cmx src/red.cmx src/vcg.cmx src/predDefExpansor.cmx src/encoding_mono_inst.cmx src/encoding_rec.cmx src/encoding_pred.cmx src/encoding_strat.cmx src/encoding_mono.cmx src/monomorph.cmx src/encoding.cmx src/pvs.cmx src/hol4.cmx src/gappa.cmx src/holl.cmx src/harvey.cmx src/simplify.cmx src/regen.cmx src/mizar.cmx src/smtlib.cmx src/coq.cmx src/zenon.cmx src/z3.cmx src/cvcl.cmx tools/calldp.cmx src/xml.cmx src/project.cmx src/why3.cmx src/pretty.cmx src/unionfind.cmx src/theoryreducer.cmx src/theory_filtering.cmx src/hypotheses_filtering.cmx src/dispatcher.cmx src/isabelle.cmx src/ocaml.cmx src/main.cmx intf/colors.cmx intf/tags.cmx intf/tools.cmx intf/tagsplit.cmx intf/astprinter.cmx intf/astnprinter.cmx intf/astpprinter.cmx intf/model.cmx intf/cache.cmx intf/gConfig.cmx intf/hilight.cmx intf/whyhilight.cmx intf/pprinter.cmx intf/preferences.cmx intf/stat.cmx strip bin/gwhy.opt ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/lib.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/rc.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/loc.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/ident.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/print_real.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/effect.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/pp.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/option_misc.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/parser.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/lexer.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/report.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/explain.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/xml.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph src/project.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/output.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_common_options.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_envset.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_constructors.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_pervasives.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_iterators.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_type_var.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_output_misc.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_poutput.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_output.ml ocamlc.opt -I atp -c -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph jc/jc_noutput.ml ocamlc.opt -w Z -warn-error A -dtypes -g -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -pack -o jc/jc.cmo src/ast.cmi src/lib.cmo src/rc.cmo src/loc.cmo src/ident.cmo src/print_real.cmo src/effect.cmo src/pp.cmo src/option_misc.cmo src/parser.cmo src/lexer.cmo src/report.cmo src/explain.cmo src/xml.cmo src/project.cmo jc/output.cmo jc/jc_common_options.cmo jc/jc_stdlib.cmo jc/jc_envset.cmo jc/jc_region.cmo jc/jc_fenv.cmo jc/jc_constructors.cmo jc/jc_pervasives.cmo jc/jc_iterators.cmo jc/jc_type_var.cmo jc/jc_output_misc.cmo jc/jc_poutput.cmo jc/jc_output.cmo jc/jc_noutput.cmo ocamlopt.opt -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -pack -o jc/jc.cmx src/ast.cmi src/lib.cmx src/rc.cmx src/loc.cmx src/ident.cmx src/print_real.cmx src/effect.cmx src/pp.cmx src/option_misc.cmx src/parser.cmx src/lexer.cmx src/report.cmx src/explain.cmx src/xml.cmx src/project.cmx jc/output.cmx jc/jc_common_options.cmx jc/jc_stdlib.cmx jc/jc_envset.cmx jc/jc_region.cmx jc/jc_fenv.cmx jc/jc_constructors.cmx jc/jc_pervasives.cmx jc/jc_iterators.cmx jc/jc_type_var.cmx jc/jc_output_misc.cmx jc/jc_poutput.cmx jc/jc_output.cmx jc/jc_noutput.cmx ocamlopt.opt -w Z -warn-error A -dtypes -I src -I jc -I c -I java -I intf -I tools -I mix -I ml -I +lablgtk2 -I +threads -I +ocamlgraph -thread -o regtest.opt unix.cmxa str.cmxa threads.cmxa tools/regtest.ml make -C frama-c-plugin depend make[1]: Entering directory `/builddir/build/BUILD/why-2.26/frama-c-plugin' rm -f ./.depend ocamldep.opt -slash \ -I . -I "/usr/lib64/frama-c" \ ./*.mli ./*.ml \ ./Jessie.mli\ \ \ > ./.depend chmod a-w ./.depend make[1]: Leaving directory `/builddir/build/BUILD/why-2.26/frama-c-plugin' make -C frama-c-plugin make[1]: Entering directory `/builddir/build/BUILD/why-2.26/frama-c-plugin' ocamlc.opt -c Jessie.mli echo "let jessie_local = false" > jessie_config.ml ocamlc.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc jessie_config.ml ocamlc.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc jessie_options.mli ocamlc.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc jessie_options.ml ocamlc.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc integer.ml ocamlc.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc common.mli ocamlc.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc common.ml ocamlc.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc rewrite.ml ocamlc.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc norm.mli ocamlc.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc norm.ml ocamlc.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc retype.ml ocamlc.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc interp.mli MAKEFLAGS="w" make -C .. -j 1 jc/jc.cmo make[2]: Entering directory `/builddir/build/BUILD/why-2.26' make[2]: `jc/jc.cmo' is up to date. make[2]: Leaving directory `/builddir/build/BUILD/why-2.26' ocamlc.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc interp.ml ocamlc.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc register.ml ocamlc.opt -o Jessie.cmo -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc -pack \ \ ./jessie_config.cmo ./jessie_options.cmo ./integer.cmo ./common.cmo ./rewrite.cmo ./norm.cmo ./retype.cmo ./interp.cmo ./register.cmo ocamlc.opt -o Jessie.cma -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc \ \ -a ./../jc/jc.cmo Jessie.cmo ocamlopt.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc -for-pack Jessie jessie_config.ml ocamlopt.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc -for-pack Jessie jessie_options.ml ocamlopt.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc -for-pack Jessie integer.ml ocamlopt.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc -for-pack Jessie common.ml ocamlopt.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc -for-pack Jessie rewrite.ml ocamlopt.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc -for-pack Jessie norm.ml ocamlopt.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc -for-pack Jessie retype.ml ocamlopt.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc -for-pack Jessie interp.ml ocamlopt.opt -c -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc -for-pack Jessie register.ml ocamlopt.opt -o Jessie.cmx -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc \ -pack \ ./jessie_config.cmx ./jessie_options.cmx ./integer.cmx ./common.cmx ./rewrite.cmx ./norm.cmx ./retype.cmx ./interp.cmx ./register.cmx ocamlopt.opt -o Jessie.cmxs -shared -I . -w Z -warn-error A -annot -g -I "/usr/lib64/frama-c" -I /usr/lib64/frama-c -I ./../src -I ./../jc \ ./../jc/jc.cmx \ Jessie.cmx make[1]: Leaving directory `/builddir/build/BUILD/why-2.26/frama-c-plugin' + strip bin/why-cpulimit + strip bin/caduceus.opt bin/gwhy.opt bin/jessie.opt bin/krakatoa.opt bin/rv_merge.opt bin/simplify2why.opt bin/tool-stat.opt bin/why-config.opt bin/why-dp.opt bin/why-obfuscator.opt bin/why-stat.opt bin/why.opt bin/why2html.opt + exit 0 Executing(%install): /bin/sh -e /var/tmp/rpm-tmp.JbZOsd + umask 022 + cd /builddir/build/BUILD + '[' /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64 '!=' / ']' + rm -rf /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64 ++ dirname /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64 + mkdir -p /builddir/build/BUILDROOT + mkdir /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64 + cd why-2.26 + LANG=C + export LANG + unset DISPLAY + rm -rf /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64 + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64 /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share + sed -e 's/\$(FRAMAC_SHARE)\/Makefile.dynamic/.\/Makefile.dynamic/' -i ./frama-c-plugin/Makefile + sed -e 's/echo/\# echo/' -i ./frama-c-plugin/Makefile.dynamic + sed -e 's/>>/\# >>/' -i ./frama-c-plugin/Makefile.dynamic + make-redir install DESTDIR=/builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64 VERBOSEMAKE=yes OCAMLBEST=opt OCAMLOPT=ocamlopt.opt PVSLIB=/builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/pvs/lib mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin cp -f bin/why.opt /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin/why cp -f bin/why-config.opt /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin/why-config cp -f bin/caduceus.opt /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin/caduceus cp -f bin/jessie.opt /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin/jessie cp -f bin/krakatoa.opt /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin/krakatoa cp -f bin/gwhy.sh /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin/gwhy cp -f bin/why2html.opt /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin/why2html cp -f bin/why-dp.opt /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin/why-dp cp -f bin/why-cpulimit /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin/why-cpulimit cp -f bin/rv_merge.opt /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin/rv_merge cp -f bin/why-obfuscator.opt /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin/why-obfuscator cp -f bin/why-stat.opt /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin/why-stat cp -f bin/tool-stat.opt /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin/tool-stat cp -f bin/simplify2why.opt /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin/simplify2why if test -f bin/gwhy.opt; then \ cp -f bin/gwhy.opt /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin/gwhy-bin; \ fi mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/why/why cp -f lib/why/prelude.why lib/why/bool.why lib/why/integer.why lib/why/real.why lib/why/arrays.why lib/why/jessie.why lib/why/jessie_bitvectors.why lib/why/mybag.why lib/why/mix.why lib/why/floats_common.why lib/why/floats_strict.why lib/why/floats_full.why lib/why/floats_multi_rounding.why /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/why/why mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/caduceus/why mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/jessie cp -f jc/jc.cmo jc/jc.cmx jc/jc.o jc/jc_ast.cmi jc/jc_env.cmi jc/jc.cmi src/lib.cmi src/rc.cmi src/loc.cmi src/ident.cmi src/print_real.cmi src/effect.cmi src/pp.cmi src/option_misc.cmi src/parser.cmi src/lexer.cmi src/report.cmi src/explain.cmi src/xml.cmi src/project.cmi jc/output.cmi jc/jc_common_options.cmi jc/jc_stdlib.cmi jc/jc_envset.cmi jc/jc_region.cmi jc/jc_fenv.cmi jc/jc_constructors.cmi jc/jc_pervasives.cmi jc/jc_iterators.cmi jc/jc_type_var.cmi jc/jc_output_misc.cmi jc/jc_poutput.cmi jc/jc_output.cmi jc/jc_noutput.cmi /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/jessie cp -f lib/why/caduceus.why /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/caduceus/why cp -f lib/why/caduceus_arith.why /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/caduceus/why mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/caduceus/coq mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/coq if test "v8" = "v7"; then \ cp -f lib/coq-v7/caduceus_why.v lib/coq-v7/caduceus_tactics.v /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/caduceus/coq; \ else \ cp -f lib/coq/caduceus_why.v lib/coq/caduceus_tactics.v /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/caduceus/coq; \ cp -f lib/coq/jessie_why.v /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/coq; \ fi mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/caduceus/isabelle cp -f lib/isabelle/caduceus_why.thy /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/caduceus/isabelle mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/caduceus/harvey cp -f lib/harvey/caduceus_why.rv /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/caduceus/harvey cd lib; cp -rf java_api /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/why cd lib; cp -rf javacard_api /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/why mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/why/images cp -f lib/images/*.png /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/why/images find /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64 -name CVS | xargs rm -f -r mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/man/man1 cp -f doc/*.1 /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/man/man1 mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/coq//user-contrib cp -f lib/coq/WhyInt.v lib/coq/WhyArrays.v lib/coq/WhyBool.v lib/coq/WhyTuples.v lib/coq/WhyPermut.v lib/coq/WhyCoqCompat.v lib/coq/WhySorted.v lib/coq/WhyExn.v lib/coq/WhyLemmas.v lib/coq/WhyTactics.v lib/coq/WhyPrelude.v lib/coq/WhyCM.v lib/coq/Why.v lib/coq/WhyReal.v lib/coq/caduceus_why.v lib/coq/caduceus_tactics.v lib/coq/caduceus_lists.v lib/coq/Caduceus.v lib/coq/jessie_why.v /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/coq//user-contrib cp -f lib/coq/WhyInt.vo lib/coq/WhyArrays.vo lib/coq/WhyBool.vo lib/coq/WhyTuples.vo lib/coq/WhyPermut.vo lib/coq/WhyCoqCompat.vo lib/coq/WhySorted.vo lib/coq/WhyExn.vo lib/coq/WhyLemmas.vo lib/coq/WhyTactics.vo lib/coq/WhyPrelude.vo lib/coq/WhyCM.vo lib/coq/Why.vo lib/coq/WhyReal.vo lib/coq/caduceus_why.vo lib/coq/caduceus_tactics.vo lib/coq/caduceus_lists.vo lib/coq/Caduceus.vo lib/coq/jessie_why.vo /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/coq//user-contrib mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/pvs/lib/why cp lib/pvs/why.pvs lib/pvs/jessie.pvs lib/pvs/whyfloat.pvs lib/pvs/why.prf lib/pvs/jessie.prf lib/pvs/whyfloat.prf /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/pvs/lib/why cp lib/pvs/top.pvs lib/pvs/pvscontext.el /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/pvs/lib/why ====== Compiling PVS theories, this may take some time ====== (cd /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/pvs/lib/why ; /usr/bin/pvs-sbcl -batch -l pvscontext.el -q -v 2 > top.out) ====== Done compiling PVS theories ====== make -C frama-c-plugin install make[1]: Entering directory `/builddir/build/BUILD/why-2.26/frama-c-plugin' cp -p ./Jessie.cmi ./Jessie.cmo ./Jessie.cma ./Jessie.cmxs "/usr/lib64/frama-c/plugins" if [ -f frama-c-Jessie.byte ]; then \ cp -p frama-c-Jessie.byte "/builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin"; \ fi if [ -f frama-c-Jessie.opt ]; then \ cp -p frama-c-Jessie.opt \ "/builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin"/frama-c-Jessie; \ fi # echo "ENABLE_`echo Jessie | tr "a-z" "A-Z"`=yes" \ # >> /usr/share/frama-c/known_plugins.ac make[1]: Leaving directory `/builddir/build/BUILD/why-2.26/frama-c-plugin' + sed -e 's!/builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64!!' -i /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/pvs/lib/why/top.out + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/why + cp -p gwhy-icon.png /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/why + sed -e 's|ICON-LOCATION-BASE|/usr/share/why|' -i gwhy.desktop + desktop-file-install --vendor=fedora --dir=/builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/applications gwhy.desktop + sed -e 's|ICON-LOCATION-BASE|/usr/share/why|' -i jessie.desktop + desktop-file-install --vendor=fedora --dir=/builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/applications jessie.desktop + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/pvs/lib/ints/ + cp -p div.pvs rem.pvs /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/lib64/pvs/lib/ints/ + cp -p patch_jessie_pvs /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/bin/ + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/ + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/ + cp -p doc/manual.ps /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/why-manual.ps + dos2unix COPYING dos2unix: converting file COPYING to UNIX format ... + mv COPYING COPYING.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f COPYING.old + cp -p caduceus.ps krakatoa.pdf README.why COPYING LICENSE /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/ + cd examples ++ find -mindepth 1 -maxdepth 1 -type d + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./string-matching + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./linked-lists + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./binary-search + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./bresenham + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./algo-63-64-65 + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./heapsort + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./find + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./quicksort2 + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./quicksort + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./selectionsort + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./kmp + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./maximumsort + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./dijkstra + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./sqrt + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./queens + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./mergesort + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./edit-distance ++ find -regex '.*\(\.mlw\|\.why\)' ++ grep -E -v '_inv|_coq|_why' + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./linked-lists/length.mlw dos2unix: converting file ./linked-lists/length.mlw to UNIX format ... + mv ./linked-lists/length.mlw ./linked-lists/length.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./linked-lists/length.mlw.old + cp -p ./linked-lists/length.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./linked-lists/length.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./linked-lists/reverse.why dos2unix: converting file ./linked-lists/reverse.why to UNIX format ... + mv ./linked-lists/reverse.why ./linked-lists/reverse.why.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./linked-lists/reverse.why.old + cp -p ./linked-lists/reverse.why /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./linked-lists/reverse.why + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./linked-lists/rev.mlw dos2unix: converting file ./linked-lists/rev.mlw to UNIX format ... + mv ./linked-lists/rev.mlw ./linked-lists/rev.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./linked-lists/rev.mlw.old + cp -p ./linked-lists/rev.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./linked-lists/rev.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./binary-search/bsearch.mlw dos2unix: converting file ./binary-search/bsearch.mlw to UNIX format ... + mv ./binary-search/bsearch.mlw ./binary-search/bsearch.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./binary-search/bsearch.mlw.old + cp -p ./binary-search/bsearch.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./binary-search/bsearch.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./bresenham/bresenham.mlw dos2unix: converting file ./bresenham/bresenham.mlw to UNIX format ... + mv ./bresenham/bresenham.mlw ./bresenham/bresenham.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./bresenham/bresenham.mlw.old + cp -p ./bresenham/bresenham.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./bresenham/bresenham.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./misc/power.mlw dos2unix: converting file ./misc/power.mlw to UNIX format ... + mv ./misc/power.mlw ./misc/power.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./misc/power.mlw.old + cp -p ./misc/power.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc/power.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./misc/arith.mlw dos2unix: converting file ./misc/arith.mlw to UNIX format ... + mv ./misc/arith.mlw ./misc/arith.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./misc/arith.mlw.old + cp -p ./misc/arith.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc/arith.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./misc/sqrt_dicho.mlw dos2unix: converting file ./misc/sqrt_dicho.mlw to UNIX format ... + mv ./misc/sqrt_dicho.mlw ./misc/sqrt_dicho.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./misc/sqrt_dicho.mlw.old + cp -p ./misc/sqrt_dicho.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc/sqrt_dicho.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./misc/fib.mlw dos2unix: converting file ./misc/fib.mlw to UNIX format ... + mv ./misc/fib.mlw ./misc/fib.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./misc/fib.mlw.old + cp -p ./misc/fib.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc/fib.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./misc/loop0.mlw dos2unix: converting file ./misc/loop0.mlw to UNIX format ... + mv ./misc/loop0.mlw ./misc/loop0.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./misc/loop0.mlw.old + cp -p ./misc/loop0.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc/loop0.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./misc/flag_ax.mlw dos2unix: converting file ./misc/flag_ax.mlw to UNIX format ... + mv ./misc/flag_ax.mlw ./misc/flag_ax.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./misc/flag_ax.mlw.old + cp -p ./misc/flag_ax.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc/flag_ax.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./misc/sum.mlw dos2unix: converting file ./misc/sum.mlw to UNIX format ... + mv ./misc/sum.mlw ./misc/sum.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./misc/sum.mlw.old + cp -p ./misc/sum.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc/sum.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./misc/search.mlw dos2unix: converting file ./misc/search.mlw to UNIX format ... + mv ./misc/search.mlw ./misc/search.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./misc/search.mlw.old + cp -p ./misc/search.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc/search.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./misc/mix_max.mlw dos2unix: converting file ./misc/mix_max.mlw to UNIX format ... + mv ./misc/mix_max.mlw ./misc/mix_max.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./misc/mix_max.mlw.old + cp -p ./misc/mix_max.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc/mix_max.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./misc/max.mlw dos2unix: converting file ./misc/max.mlw to UNIX format ... + mv ./misc/max.mlw ./misc/max.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./misc/max.mlw.old + cp -p ./misc/max.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc/max.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./misc/swap0.mlw dos2unix: converting file ./misc/swap0.mlw to UNIX format ... + mv ./misc/swap0.mlw ./misc/swap0.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./misc/swap0.mlw.old + cp -p ./misc/swap0.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc/swap0.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./misc/matrix_mult.why dos2unix: converting file ./misc/matrix_mult.why to UNIX format ... + mv ./misc/matrix_mult.why ./misc/matrix_mult.why.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./misc/matrix_mult.why.old + cp -p ./misc/matrix_mult.why /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc/matrix_mult.why + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./misc/mac_carthy.mlw dos2unix: converting file ./misc/mac_carthy.mlw to UNIX format ... + mv ./misc/mac_carthy.mlw ./misc/mac_carthy.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./misc/mac_carthy.mlw.old + cp -p ./misc/mac_carthy.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc/mac_carthy.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./misc/peano.mlw dos2unix: converting file ./misc/peano.mlw to UNIX format ... + mv ./misc/peano.mlw ./misc/peano.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./misc/peano.mlw.old + cp -p ./misc/peano.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc/peano.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./misc/flag.mlw dos2unix: converting file ./misc/flag.mlw to UNIX format ... + mv ./misc/flag.mlw ./misc/flag.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./misc/flag.mlw.old + cp -p ./misc/flag.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc/flag.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./misc/matrix.why dos2unix: converting file ./misc/matrix.why to UNIX format ... + mv ./misc/matrix.why ./misc/matrix.why.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./misc/matrix.why.old + cp -p ./misc/matrix.why /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc/matrix.why + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./misc/gcd.mlw dos2unix: converting file ./misc/gcd.mlw to UNIX format ... + mv ./misc/gcd.mlw ./misc/gcd.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./misc/gcd.mlw.old + cp -p ./misc/gcd.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./misc/gcd.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./algo-63-64-65/algo64.mlw dos2unix: converting file ./algo-63-64-65/algo64.mlw to UNIX format ... + mv ./algo-63-64-65/algo64.mlw ./algo-63-64-65/algo64.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./algo-63-64-65/algo64.mlw.old + cp -p ./algo-63-64-65/algo64.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./algo-63-64-65/algo64.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./algo-63-64-65/algo63.mlw dos2unix: converting file ./algo-63-64-65/algo63.mlw to UNIX format ... + mv ./algo-63-64-65/algo63.mlw ./algo-63-64-65/algo63.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./algo-63-64-65/algo63.mlw.old + cp -p ./algo-63-64-65/algo63.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./algo-63-64-65/algo63.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./algo-63-64-65/algo65.mlw dos2unix: converting file ./algo-63-64-65/algo65.mlw to UNIX format ... + mv ./algo-63-64-65/algo65.mlw ./algo-63-64-65/algo65.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./algo-63-64-65/algo65.mlw.old + cp -p ./algo-63-64-65/algo65.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./algo-63-64-65/algo65.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./heapsort/swap.mlw dos2unix: converting file ./heapsort/swap.mlw to UNIX format ... + mv ./heapsort/swap.mlw ./heapsort/swap.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./heapsort/swap.mlw.old + cp -p ./heapsort/swap.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./heapsort/swap.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./heapsort/downheap.mlw dos2unix: converting file ./heapsort/downheap.mlw to UNIX format ... + mv ./heapsort/downheap.mlw ./heapsort/downheap.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./heapsort/downheap.mlw.old + cp -p ./heapsort/downheap.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./heapsort/downheap.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./heapsort/heapsort.mlw dos2unix: converting file ./heapsort/heapsort.mlw to UNIX format ... + mv ./heapsort/heapsort.mlw ./heapsort/heapsort.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./heapsort/heapsort.mlw.old + cp -p ./heapsort/heapsort.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./heapsort/heapsort.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./find/find.mlw dos2unix: converting file ./find/find.mlw to UNIX format ... + mv ./find/find.mlw ./find/find.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./find/find.mlw.old + cp -p ./find/find.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./find/find.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./quicksort2/quicksort2.mlw dos2unix: converting file ./quicksort2/quicksort2.mlw to UNIX format ... + mv ./quicksort2/quicksort2.mlw ./quicksort2/quicksort2.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./quicksort2/quicksort2.mlw.old + cp -p ./quicksort2/quicksort2.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./quicksort2/quicksort2.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./quicksort/quicksort.mlw dos2unix: converting file ./quicksort/quicksort.mlw to UNIX format ... + mv ./quicksort/quicksort.mlw ./quicksort/quicksort.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./quicksort/quicksort.mlw.old + cp -p ./quicksort/quicksort.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./quicksort/quicksort.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./quicksort/partition.mlw dos2unix: converting file ./quicksort/partition.mlw to UNIX format ... + mv ./quicksort/partition.mlw ./quicksort/partition.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./quicksort/partition.mlw.old + cp -p ./quicksort/partition.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./quicksort/partition.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./selectionsort/selection.mlw dos2unix: converting file ./selectionsort/selection.mlw to UNIX format ... + mv ./selectionsort/selection.mlw ./selectionsort/selection.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./selectionsort/selection.mlw.old + cp -p ./selectionsort/selection.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./selectionsort/selection.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./kmp/kmp.mlw dos2unix: converting file ./kmp/kmp.mlw to UNIX format ... + mv ./kmp/kmp.mlw ./kmp/kmp.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./kmp/kmp.mlw.old + cp -p ./kmp/kmp.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./kmp/kmp.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./maximumsort/maximumsort.mlw dos2unix: converting file ./maximumsort/maximumsort.mlw to UNIX format ... + mv ./maximumsort/maximumsort.mlw ./maximumsort/maximumsort.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./maximumsort/maximumsort.mlw.old + cp -p ./maximumsort/maximumsort.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./maximumsort/maximumsort.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./dijkstra/dijkstra.why dos2unix: converting file ./dijkstra/dijkstra.why to UNIX format ... + mv ./dijkstra/dijkstra.why ./dijkstra/dijkstra.why.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./dijkstra/dijkstra.why.old + cp -p ./dijkstra/dijkstra.why /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./dijkstra/dijkstra.why + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./sqrt/simple.mlw dos2unix: converting file ./sqrt/simple.mlw to UNIX format ... + mv ./sqrt/simple.mlw ./sqrt/simple.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./sqrt/simple.mlw.old + cp -p ./sqrt/simple.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./sqrt/simple.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./sqrt/sqrt.mlw dos2unix: converting file ./sqrt/sqrt.mlw to UNIX format ... + mv ./sqrt/sqrt.mlw ./sqrt/sqrt.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./sqrt/sqrt.mlw.old + cp -p ./sqrt/sqrt.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./sqrt/sqrt.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./queens/queens.why dos2unix: converting file ./queens/queens.why to UNIX format ... + mv ./queens/queens.why ./queens/queens.why.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./queens/queens.why.old + cp -p ./queens/queens.why /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./queens/queens.why + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./mergesort/mergesort.mlw dos2unix: converting file ./mergesort/mergesort.mlw to UNIX format ... + mv ./mergesort/mergesort.mlw ./mergesort/mergesort.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./mergesort/mergesort.mlw.old + cp -p ./mergesort/mergesort.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./mergesort/mergesort.mlw + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./mergesort/mergesort.why dos2unix: converting file ./mergesort/mergesort.why to UNIX format ... + mv ./mergesort/mergesort.why ./mergesort/mergesort.why.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./mergesort/mergesort.why.old + cp -p ./mergesort/mergesort.why /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./mergesort/mergesort.why + for f in '`find -regex '\''.*\(\.mlw\|\.why\)'\'' | grep -E -v '\''_inv|_coq|_why'\''`' + dos2unix ./edit-distance/distance.mlw dos2unix: converting file ./edit-distance/distance.mlw to UNIX format ... + mv ./edit-distance/distance.mlw ./edit-distance/distance.mlw.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./edit-distance/distance.mlw.old + cp -p ./edit-distance/distance.mlw /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/mlw/./edit-distance/distance.mlw + cd ../examples-c ++ find -mindepth 1 -maxdepth 1 -type d + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./linked-lists + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./float + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./sorting + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./puf + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./tutorial + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./g4 + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./trees + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./schorr-waite + for d in '`find -mindepth 1 -maxdepth 1 -type d`' + mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./ukkonen ++ find -regex '.*\.c' + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./linked-lists/search.c dos2unix: converting file ./linked-lists/search.c to UNIX format ... + mv ./linked-lists/search.c ./linked-lists/search.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./linked-lists/search.c.old + cp -p ./linked-lists/search.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./linked-lists/search.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./linked-lists/has_cycle.c dos2unix: converting file ./linked-lists/has_cycle.c to UNIX format ... + mv ./linked-lists/has_cycle.c ./linked-lists/has_cycle.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./linked-lists/has_cycle.c.old + cp -p ./linked-lists/has_cycle.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./linked-lists/has_cycle.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./linked-lists/swap.c dos2unix: converting file ./linked-lists/swap.c to UNIX format ... + mv ./linked-lists/swap.c ./linked-lists/swap.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./linked-lists/swap.c.old + cp -p ./linked-lists/swap.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./linked-lists/swap.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./linked-lists/reverse.c dos2unix: converting file ./linked-lists/reverse.c to UNIX format ... + mv ./linked-lists/reverse.c ./linked-lists/reverse.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./linked-lists/reverse.c.old + cp -p ./linked-lists/reverse.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./linked-lists/reverse.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./float/Sterbenz2.c dos2unix: converting file ./float/Sterbenz2.c to UNIX format ... + mv ./float/Sterbenz2.c ./float/Sterbenz2.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./float/Sterbenz2.c.old + cp -p ./float/Sterbenz2.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./float/Sterbenz2.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./float/Malcolm.c dos2unix: converting file ./float/Malcolm.c to UNIX format ... + mv ./float/Malcolm.c ./float/Malcolm.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./float/Malcolm.c.old + cp -p ./float/Malcolm.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./float/Malcolm.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./float/Sterbenz.c dos2unix: converting file ./float/Sterbenz.c to UNIX format ... + mv ./float/Sterbenz.c ./float/Sterbenz.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./float/Sterbenz.c.old + cp -p ./float/Sterbenz.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./float/Sterbenz.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./sorting/selection.c dos2unix: converting file ./sorting/selection.c to UNIX format ... + mv ./sorting/selection.c ./sorting/selection.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./sorting/selection.c.old + cp -p ./sorting/selection.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./sorting/selection.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./sorting/quicksort.c dos2unix: converting file ./sorting/quicksort.c to UNIX format ... + mv ./sorting/quicksort.c ./sorting/quicksort.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./sorting/quicksort.c.old + cp -p ./sorting/quicksort.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./sorting/quicksort.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./puf/parray.c dos2unix: converting file ./puf/parray.c to UNIX format ... + mv ./puf/parray.c ./puf/parray.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./puf/parray.c.old + cp -p ./puf/parray.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./puf/parray.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./puf/puf.c dos2unix: converting file ./puf/puf.c to UNIX format ... + mv ./puf/puf.c ./puf/puf.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./puf/puf.c.old + cp -p ./puf/puf.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./puf/puf.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./tutorial/search.c dos2unix: converting file ./tutorial/search.c to UNIX format ... + mv ./tutorial/search.c ./tutorial/search.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./tutorial/search.c.old + cp -p ./tutorial/search.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./tutorial/search.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./tutorial/binary_search.c dos2unix: converting file ./tutorial/binary_search.c to UNIX format ... + mv ./tutorial/binary_search.c ./tutorial/binary_search.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./tutorial/binary_search.c.old + cp -p ./tutorial/binary_search.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./tutorial/binary_search.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./tutorial/flag.c dos2unix: converting file ./tutorial/flag.c to UNIX format ... + mv ./tutorial/flag.c ./tutorial/flag.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./tutorial/flag.c.old + cp -p ./tutorial/flag.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./tutorial/flag.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./tutorial/abs.c dos2unix: converting file ./tutorial/abs.c to UNIX format ... + mv ./tutorial/abs.c ./tutorial/abs.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./tutorial/abs.c.old + cp -p ./tutorial/abs.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./tutorial/abs.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./tutorial/purse.c dos2unix: converting file ./tutorial/purse.c to UNIX format ... + mv ./tutorial/purse.c ./tutorial/purse.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./tutorial/purse.c.old + cp -p ./tutorial/purse.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./tutorial/purse.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./tutorial/swap.c dos2unix: converting file ./tutorial/swap.c to UNIX format ... + mv ./tutorial/swap.c ./tutorial/swap.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./tutorial/swap.c.old + cp -p ./tutorial/swap.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./tutorial/swap.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./tutorial/max.c dos2unix: converting file ./tutorial/max.c to UNIX format ... + mv ./tutorial/max.c ./tutorial/max.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./tutorial/max.c.old + cp -p ./tutorial/max.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./tutorial/max.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./tutorial/average.c dos2unix: converting file ./tutorial/average.c to UNIX format ... + mv ./tutorial/average.c ./tutorial/average.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./tutorial/average.c.old + cp -p ./tutorial/average.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./tutorial/average.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./tutorial/modulo.c dos2unix: converting file ./tutorial/modulo.c to UNIX format ... + mv ./tutorial/modulo.c ./tutorial/modulo.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./tutorial/modulo.c.old + cp -p ./tutorial/modulo.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./tutorial/modulo.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./g4/g4.c dos2unix: converting file ./g4/g4.c to UNIX format ... + mv ./g4/g4.c ./g4/g4.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./g4/g4.c.old + cp -p ./g4/g4.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./g4/g4.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./trees/search.c dos2unix: converting file ./trees/search.c to UNIX format ... + mv ./trees/search.c ./trees/search.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./trees/search.c.old + cp -p ./trees/search.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./trees/search.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./schorr-waite/schorr_waite.c dos2unix: converting file ./schorr-waite/schorr_waite.c to UNIX format ... + mv ./schorr-waite/schorr_waite.c ./schorr-waite/schorr_waite.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./schorr-waite/schorr_waite.c.old + cp -p ./schorr-waite/schorr_waite.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./schorr-waite/schorr_waite.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./ukkonen/ukkonen.c dos2unix: converting file ./ukkonen/ukkonen.c to UNIX format ... + mv ./ukkonen/ukkonen.c ./ukkonen/ukkonen.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./ukkonen/ukkonen.c.old + cp -p ./ukkonen/ukkonen.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./ukkonen/ukkonen.c + for f in '`find -regex '\''.*\.c'\''`' + dos2unix ./ukkonen/main.c dos2unix: converting file ./ukkonen/main.c to UNIX format ... + mv ./ukkonen/main.c ./ukkonen/main.c.old + iconv -f ISO-8859-1 -t UTF-8 + rm -f ./ukkonen/main.c.old + cp -p ./ukkonen/main.c /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-2.26/examples/c/./ukkonen/main.c + /usr/lib/rpm/check-buildroot + /usr/lib/rpm/redhat/brp-compress + /usr/lib/rpm/redhat/brp-strip /usr/bin/strip + /usr/lib/rpm/redhat/brp-strip-comment-note /usr/bin/strip /usr/bin/objdump + /usr/lib/rpm/redhat/brp-strip-static-archive /usr/bin/strip + /usr/lib/rpm/brp-python-bytecompile /usr/bin/python 1 + /usr/lib/rpm/redhat/brp-python-hardlink + /usr/lib/rpm/redhat/brp-java-repack-jars Executing(%check): /bin/sh -e /var/tmp/rpm-tmp.Z8LNmI + umask 022 + cd /builddir/build/BUILD + cd why-2.26 + unset DISPLAY + WHYLIB=lib + bin/why.opt --why --output min.why min.mlw + diff -u min.why min_why.why.result + exit 0 Processing files: why-2.26-1.fc14.x86_64 Finding Provides: /usr/lib/rpm/ocaml-find-provides.sh -i Project Finding Requires: /usr/lib/rpm/ocaml-find-requires.sh -i Ast -i Cc -i Error -i Logic -i Logic_decl -i Ptree -i Types -i Env -i Misc -i Cil_types -i Db_types -i Lattice_With_Isotropy -i Signature Provides: ocaml(Effect) = 7823d76c21ac7979c7c152d15f67f4b9 ocaml(Explain) = e53d93001798c873183208d28940e817 ocaml(Ident) = 33cc950cc2cfc0617782e41b0ddbdf32 ocaml(Jc_ast) = 6bc808901a81a4980b0b3c8472b239e1 ocaml(Jc) = bffcc644a5225d34f1aee5c5c197ece0 ocaml(Jc_common_options) = dde79441217e2a63203bc4ae35dce61c ocaml(Jc_constructors) = 1c3348a6d8626ba34aa7f9d4daa0ba0f ocaml(Jc_env) = b5acc9d36a01dac8502bb81b438f6bc4 ocaml(Jc_envset) = 015bf973ba4964fe0b0349c1b8922c73 ocaml(Jc_fenv) = 98104a239900ff800ba6143fb3ed4bc5 ocaml(Jc_iterators) = 4f76984c233d541b7ab4d1435b8b58d6 ocaml(Jc_noutput) = c522eb59361129977e88a635396f59f4 ocaml(Jc_output) = fc899680bf1719da8c3eec7515825784 ocaml(Jc_output_misc) = 8a96085e480a3e94cce655d63cca9f81 ocaml(Jc_pervasives) = 9caa0389341c1b5169cb587b0d99e32a ocaml(Jc_poutput) = dbd44f4974da69014bbee0a7cfa4f9ca ocaml(Jc_region) = 64e2b93ee4e5e4302b2cc8ed38c4367a ocaml(Jc_stdlib) = 744f4225f22ab804ebe8d5b6fab1a84e ocaml(Jc_type_var) = 780d8ae165b1e40cbd16eb42d70997f1 ocaml(Jessie) = a85f8fdd305b965391b3b9bf8ae96bff ocaml(Lexer) = 2765c8f7ec076a64c0dda719b70e2724 ocaml(Lib) = 30f1ddb3375de3beaad50dca9c2a4806 ocaml(Loc) = 01ae6dea38912c6ed357ee975c77af1e ocaml(Option_misc) = c197e0818b00f99a796cc59ee05c3e76 ocaml(Output) = 3c8bf592940b23eb97053af36dbddbd9 ocaml(Parser) = 70688d05d2300777d788bae72f02b19a ocaml(Pp) = 8cf35d60e8aa971c308342ee570e26a7 ocaml(Print_real) = ec7ca56c3974e897f360c46045f06dea ocaml(Rc) = 88062244b4d048e20295f11f3f20d076 ocaml(Report) = b2239450e5723355a244d64bf7168ae5 ocaml(Xml) = c3d395b8b1d06f694abc5073684d2cfe Requires(interp): /bin/sh /bin/sh Requires(rpmlib): rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(VersionedDependencies) <= 3.0.3-1 Requires(post): /bin/sh Requires(postun): /bin/sh Requires: ocaml(Abstract_interp) = 3db95d1e46919f8656a1f2e3204d9bc1 ocaml(Abstract_value) = 3e8713ee586e095e7c803c97dea28de0 ocaml(Alarms) = 8d8e6138b960caa5d1315b26280fffb6 ocaml(Annotations) = 5957f0f1ada3fcdaf7066538aa7d9ffa ocaml(Arg) = b6513be035dc9c8a458c189cd8841700 ocaml(Array) = 9c9fa5f11e2d6992c427dde4d1168489 ocaml(Base) = 6c6ccbf62570ce66705611cde69c1e88 ocaml(BaseUtils) = 8f167928e3a17081c4b56a565c62045c ocaml(Big_int) = b094bddd70d11f4b8592f3957a8b3d9f ocaml(Bit_utils) = f343dfbd4918ba75ad1f337bd076e679 ocaml(Buckx) = 2b6fdb8a283c6219044cfad4312c0d01 ocaml(Buffer) = 0ce5de86183a833ed112488a1e6d281d ocaml(Cabs2cil) = ee229578f6bc4b1177a895bd9365cb7e ocaml(Cabs) = c28c3ec371d1039fa15f5e092c25f415 ocaml(CamlinternalMod) = 34d96af9340b540539e9d022ece9fc3c ocaml(CamlinternalOO) = f83f268cd1a00c37180b9b1fb9306031 ocaml(Char) = 3da72249626c7db769beafc97036cb4f ocaml(Cil) = 90b871170e71ef80ca7a4d70b0121a5e ocaml(Cil_const) = 350d0168d0d31db5810a34e979e8551c ocaml(CilE) = c281ac75807b1b7baf94ef02e0100c1f ocaml(Cilmsg) = 74f7fa526081d861e61536e6744ee92f ocaml(Cilutil) = 17357040d20e4566735d8fdbd5e8399b ocaml(Cmdline) = 249e24cf62b50cd8fb2d122a9e4574f0 ocaml(Computation) = adcf7561c893702c8ba968fe577f217f ocaml(Config) = a7d598e35ba90eda6609419b22f3e041 ocaml(Cvalue_type) = 6daac5e1733bf95057f5a9f297f67584 ocaml(Datatype) = 40ddb900f53f073bde476577959796f2 ocaml(Db) = 364f5fb570941dd76d5525044e12b945 ocaml(Digest) = 310db9d3dd12d84178f002a532644c84 ocaml(Dynamic) = ab589ca1de42624848e81a54476fde54 ocaml(Extlib) = 5e6bcdd08c750e1d0b6d69b81b548d37 ocaml(File) = 017d784fb6b5fe23a05ab64cf08681b4 ocaml(Filename) = 9d7d89d76fb7c750cebd9ea5578bba67 ocaml(Format) = 294246d2bcc3b8adc89bd48bff122c7e ocaml(Function_Froms) = c247e77ec3d3931326f321165f8c1d72 ocaml(Globals) = b57c8738e2b96fcf1307e09a2f578bf4 ocaml(Graph) = 7857ef7b32f9bb320ed068bba9df6ea6 ocaml(Hashtbl) = ee2a3220e38a4350c5bc131ce9f3f6ce ocaml(Hook) = 241eeed5fd3737703988f05ce1663516 ocaml(Inout_type) = 14a19440b463db91852df54e7f5d62df ocaml(Int32) = b2545c419b6b6a173cac4c0a3e7e0277 ocaml(Int64) = d501d6e89fdce41c79f274fb464995d5 ocaml(Int_Base) = 7e25d25b9173d7a3ac0e896e28889c15 ocaml(Inthash) = 54a0214d8ed354f20eef160a7851af10 ocaml(Ival) = e10b1fdf1263640e38c88696cc7b2066 ocaml(Kernel_function) = a6d704c871857f2ba5c741486d840b5e ocaml(Kernel_type) = 828e4d5808516e8c549059bc8ee078f2 ocaml(Kind) = 7992108f33f4159a0da77e85ba237d1e ocaml(Lexing) = 4d17267334f1a6c75730dc3fae21fb9b ocaml(List) = a0e2e49d266ff302f8667651a43f71ba ocaml(Lmap) = 582b2eb9cbd3957fb0e513db17ac8e1f ocaml(Lmap_bitwise) = d78ee04a27c77c57aa6980f2605b5354 ocaml(Locations) = 2671bac5aa2e30c95d6284ef25680a96 ocaml(Log) = a5e182e807781c5a8b1430a7664ffe92 ocaml(Map) = d6ea0139afe59a16df7b23d35e571de7 ocaml(My_bigint) = dc0fb13f8c5c3b48f94b75a6ea2df82a ocaml(Nat) = 3ba7c2bfbc706aa841271c572dbb55de ocaml(Nativeint) = 7233ce5207a538fea4f0c61ed411ea2c ocaml(Num) = a130968f082cd5c0b9fd83b97c9603c1 ocaml(Obj) = 57b3fe2fcfe45ee25709b8ae556264d1 ocaml(Offsetmap) = 4b82c0d0e28382ff10187682b7095fb5 ocaml(Origin) = 2cdcd9a56a6a1bde3a38fc0a606dc3e1 ocaml(Parameters) = 5f550d145b28887b7f5a832634cb090e ocaml(Parsing) = 29c3f123280f8e6e639cfb025b3c9a3f ocaml(PdgIndex) = a3f60faf8daca4021b2989248abb47ac ocaml(PdgMarks) = feafea1cb38af40f2b3970a9bacadff7 ocaml(Pervasives) = 88cb1505c8bdf9a4dcd2cdf3452732b4 ocaml(Plugin) = 8583c01dbef2308d3eafdb5c15640ea9 ocaml(Pretty_utils) = 1083f5ac94a971694507d4b8ed40e247 ocaml(Printer) = 8603e36891632004cacdf6bbfabb0a33 ocaml(Printexc) = 278aebf1caaf292dc9bde915f6753bd6 ocaml(Printf) = 807ecd3a1538992580464c03462c9964 ocaml(Ptset) = b86de58ef7a28269cde7609df3833978 ocaml(Queue) = 56b5e04dcda600ae0cdf49a37f17fcd9 ocaml(Ratio) = 5ee67f3f53c78b1d40c5da48028935f3 ocaml(Relations_type) = f9a79e29677a7ffead2599b35deaa1b0 ocaml(Scanf) = c56c08d4e2ea6dddf2693c92cc7e2903 ocaml(Set) = c4be5d24d30c129dd60d2739e54db7dd ocaml(SlicingInternals) = 34bd869bdb3d1c129fb638e9ca89c3a8 ocaml(State_set) = 3e48d062e0b38f2880d4fce104aed1d5 ocaml(Stream) = 91a43ea7fb16bf36f3f10c0dc7d08a0e ocaml(String) = ecc403546c1c50056801131811c39017 ocaml(Sys) = 21bf525b2b3f3a46a54b96163adfe387 ocaml(Type) = 84f45f9ab4f59bc7d74c2982e8107df5 ocaml(Unix) = 0596a58544f8cd88fed5bf5432a53d43 ocaml(Unmarshal) = b2ee3952cce860e3bdca4f85f1a30443 ocaml(Utf8_logic) = 0d8538077ebc953dea9e5ff46d9a56a2 ocaml(Visitor) = d9ccc12e4f22db33f5b9901bdb140f52 ocaml(Weak) = aada27147107868937e9d245df90602d ocaml(runtime) = 3.11.2 Processing files: why-gwhy-2.26-1.fc14.x86_64 Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.kW8ADe + umask 022 + cd /builddir/build/BUILD + cd why-2.26 + DOCDIR=/builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-gwhy-2.26 + export DOCDIR + rm -rf /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-gwhy-2.26 + /bin/mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-gwhy-2.26 + cp -pr README.why-gwhy.Fedora /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-gwhy-2.26 + exit 0 Finding Provides: /usr/lib/rpm/ocaml-find-provides.sh -i Project Finding Requires: /usr/lib/rpm/ocaml-find-requires.sh -i Ast -i Cc -i Error -i Logic -i Logic_decl -i Ptree -i Types -i Env -i Misc -i Cil_types -i Db_types -i Lattice_With_Isotropy -i Signature Requires(rpmlib): rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 rpmlib(CompressedFileNames) <= 3.0.4-1 Processing files: why-coq-2.26-1.fc14.x86_64 Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.D9BY6K + umask 022 + cd /builddir/build/BUILD + cd why-2.26 + DOCDIR=/builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-coq-2.26 + export DOCDIR + rm -rf /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-coq-2.26 + /bin/mkdir -p /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-coq-2.26 + cp -pr README.why-coq.Fedora /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64/usr/share/doc/why-coq-2.26 + exit 0 Finding Provides: /usr/lib/rpm/ocaml-find-provides.sh -i Project Finding Requires: /usr/lib/rpm/ocaml-find-requires.sh -i Ast -i Cc -i Error -i Logic -i Logic_decl -i Ptree -i Types -i Env -i Misc -i Cil_types -i Db_types -i Lattice_With_Isotropy -i Signature Requires(rpmlib): rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 rpmlib(CompressedFileNames) <= 3.0.4-1 Processing files: why-pvs-support-2.26-1.fc14.x86_64 Finding Provides: /usr/lib/rpm/ocaml-find-provides.sh -i Project Finding Requires: /usr/lib/rpm/ocaml-find-requires.sh -i Ast -i Cc -i Error -i Logic -i Logic_decl -i Ptree -i Types -i Env -i Misc -i Cil_types -i Db_types -i Lattice_With_Isotropy -i Signature Requires(rpmlib): rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 rpmlib(CompressedFileNames) <= 3.0.4-1 Processing files: why-all-2.26-1.fc14.x86_64 Checking for unpackaged file(s): /usr/lib/rpm/check-files /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64 warning: Could not canonicalize hostname: x86-14.phx2.fedoraproject.org Wrote: /builddir/build/RPMS/why-2.26-1.fc14.x86_64.rpm Wrote: /builddir/build/RPMS/why-gwhy-2.26-1.fc14.x86_64.rpm Wrote: /builddir/build/RPMS/why-coq-2.26-1.fc14.x86_64.rpm Wrote: /builddir/build/RPMS/why-pvs-support-2.26-1.fc14.x86_64.rpm Wrote: /builddir/build/RPMS/why-all-2.26-1.fc14.x86_64.rpm Executing(%clean): /bin/sh -e /var/tmp/rpm-tmp.JPfGsK + umask 022 + cd /builddir/build/BUILD + cd why-2.26 + rm -rf /builddir/build/BUILDROOT/why-2.26-1.fc14.x86_64 + exit 0 Child returncode was: 0 LEAVE do -->