DC-Build-Header: cbmc 4.0-4 / Fri Jan 13 00:04:23 +0100 2012 Another build requested exclusive access to the build node Another build requested exclusive access to the build node Another build requested exclusive access to the build node Another build requested exclusive access to the build node Another build requested exclusive access to the build node Another build requested exclusive access to the build node Another build requested exclusive access to the build node Another build requested exclusive access to the build node sbuild (Debian sbuild) 0.62.2 (05 Apr 2011) on stremi-5.reims.grid5000.fr ╔══════════════════════════════════════════════════════════════════════════════╗ ║ cbmc 4.0-4 (amd64) 13 Jan 2012 00:08 ║ ╚══════════════════════════════════════════════════════════════════════════════╝ Package: cbmc Version: 4.0-4 Source Version: 4.0-4 Distribution: lsid64b Architecture: amd64 ┌──────────────────────────────────────────────────────────────────────────────┐ │ Update chroot │ └──────────────────────────────────────────────────────────────────────────────┘ Ign http://localhost sid InRelease Get:1 http://localhost sid Release.gpg [836 B] Get:2 http://localhost sid Release [188 kB] Ign http://localhost sid/main Sources/DiffIndex Ign http://localhost sid/main amd64 Packages/DiffIndex Ign http://localhost sid/main TranslationIndex Get:3 http://localhost sid/main Sources [7544 kB] Get:4 http://localhost sid/main amd64 Packages [10.4 MB] Ign http://localhost sid/main Translation-en Fetched 18.2 MB in 3s (4653 kB/s) Reading package lists... Reading package lists... Building dependency tree... Reading state information... The following packages have been kept back: clang cpp-4.6 g++-4.6 gcc-4.6 gcc-4.6-base libgcc1 libgomp1 libquadmath0 libstdc++6 libstdc++6-4.6-dev 0 upgraded, 0 newly installed, 0 to remove and 10 not upgraded. ┌──────────────────────────────────────────────────────────────────────────────┐ │ Fetch source files │ └──────────────────────────────────────────────────────────────────────────────┘ Check APT ───────── Checking available source versions... Download source files with APT ────────────────────────────── Reading package lists... Building dependency tree... Reading state information... Need to get 875 kB of source archives. Get:1 http://localhost/debian/ sid/main cbmc 4.0-4 (dsc) [1064 B] Get:2 http://localhost/debian/ sid/main cbmc 4.0-4 (tar) [869 kB] Get:3 http://localhost/debian/ sid/main cbmc 4.0-4 (diff) [4883 B] Fetched 875 kB in 0s (10.3 MB/s) Download complete and in download only mode Check arch ────────── Merged Build-Depends: build-essential, fakeroot Filtered Build-Depends: build-essential, fakeroot dpkg-deb: building package `sbuild-build-depends-core-dummy' in `/build/cbmc-3FyMI5/resolver-VIdrrl/apt_archive/sbuild-build-depends-core-dummy.deb'. OK Reading package lists... ┌──────────────────────────────────────────────────────────────────────────────┐ │ Install core build dependencies (apt-based resolver) │ └──────────────────────────────────────────────────────────────────────────────┘ Installing build dependencies Reading package lists... Building dependency tree... Reading state information... The following NEW packages will be installed: sbuild-build-depends-core-dummy 0 upgraded, 1 newly installed, 0 to remove and 10 not upgraded. Need to get 0 B/702 B of archives. After this operation, 0 B of additional disk space will be used. WARNING: The following packages cannot be authenticated! sbuild-build-depends-core-dummy Authentication warning overridden. Selecting previously unselected package sbuild-build-depends-core-dummy. (Reading database ... 10821 files and directories currently installed.) Unpacking sbuild-build-depends-core-dummy (from .../sbuild-build-depends-core-dummy.deb) ... Setting up sbuild-build-depends-core-dummy (0.invalid.0) ... Cannot open /var/lib/schroot/mount/lsid64b-1b570873-b857-488a-bf01-393a9de7f29e/etc/lsb-release: No such file or directory Merged Build-Depends: base-files, base-passwd, bash, coreutils, dash, debianutils, diffutils, dpkg, e2fsprogs, findutils, grep, gzip, hostname, ncurses-base, ncurses-bin, perl-base, sed, login, sysvinit-utils, sysvinit, tar, bsdutils, mount, util-linux, libc6-dev | libc-dev, gcc (>= 4:4.4.3), g++ (>= 4:4.4.3), make, dpkg-dev (>= 1.13.5), debhelper (>= 7.0.50~), minisat (>= 1:2.2.1-2), zlib1g-dev, flex, bison Filtered Build-Depends: base-files, base-passwd, bash, coreutils, dash, debianutils, diffutils, dpkg, e2fsprogs, findutils, grep, gzip, hostname, ncurses-base, ncurses-bin, perl-base, sed, login, sysvinit-utils, sysvinit, tar, bsdutils, mount, util-linux, libc6-dev, gcc (>= 4:4.4.3), g++ (>= 4:4.4.3), make, dpkg-dev (>= 1.13.5), debhelper (>= 7.0.50~), minisat (>= 1:2.2.1-2), zlib1g-dev, flex, bison dpkg-deb: building package `sbuild-build-depends-cbmc-dummy' in `/build/cbmc-3FyMI5/resolver-Xt_t3d/apt_archive/sbuild-build-depends-cbmc-dummy.deb'. OK Reading package lists... ┌──────────────────────────────────────────────────────────────────────────────┐ │ Install cbmc build dependencies (apt-based resolver) │ └──────────────────────────────────────────────────────────────────────────────┘ Installing build dependencies Reading package lists... Building dependency tree... Reading state information... The following extra packages will be installed: bison bsdmainutils debhelper file flex gettext gettext-base groff-base html2text intltool-debian libbison-dev libcroco3 libglib2.0-0 libmagic1 libpcre3 libpipeline1 libunistring0 libxml2 m4 man-db minisat po-debconf zlib1g-dev Suggested packages: bison-doc wamerican wordlist whois vacation dh-make gettext-doc groff www-browser libmail-box-perl Recommended packages: curl wget lynx-cur autopoint libglib2.0-data shared-mime-info xml-core libmail-sendmail-perl The following NEW packages will be installed: bison bsdmainutils debhelper file flex gettext gettext-base groff-base html2text intltool-debian libbison-dev libcroco3 libglib2.0-0 libmagic1 libpcre3 libpipeline1 libunistring0 libxml2 m4 man-db minisat po-debconf sbuild-build-depends-cbmc-dummy zlib1g-dev 0 upgraded, 24 newly installed, 0 to remove and 10 not upgraded. Need to get 11.4 MB/11.4 MB of archives. After this operation, 30.8 MB of additional disk space will be used. WARNING: The following packages cannot be authenticated! libpipeline1 libpcre3 m4 flex libglib2.0-0 libxml2 libcroco3 libunistring0 bsdmainutils groff-base man-db libmagic1 file gettext-base libbison-dev bison html2text gettext intltool-debian po-debconf debhelper zlib1g-dev minisat sbuild-build-depends-cbmc-dummy Authentication warning overridden. Get:1 http://localhost/debian/ sid/main libpipeline1 amd64 1.2.0-5 [38.2 kB] Get:2 http://localhost/debian/ sid/main libpcre3 amd64 8.12-4 [225 kB] Get:3 http://localhost/debian/ sid/main m4 amd64 1.4.16-2 [259 kB] Get:4 http://localhost/debian/ sid/main flex amd64 2.5.35-10 [332 kB] Get:5 http://localhost/debian/ sid/main libglib2.0-0 amd64 2.30.2-4 [1844 kB] Get:6 http://localhost/debian/ sid/main libxml2 amd64 2.7.8.dfsg-5.1 [891 kB] Get:7 http://localhost/debian/ sid/main libcroco3 amd64 0.6.2-2 [122 kB] Get:8 http://localhost/debian/ sid/main libunistring0 amd64 0.9.3-5 [434 kB] Get:9 http://localhost/debian/ sid/main bsdmainutils amd64 8.2.3 [208 kB] Get:10 http://localhost/debian/ sid/main groff-base amd64 1.21-6 [1150 kB] Get:11 http://localhost/debian/ sid/main man-db amd64 2.6.0.2-3 [1015 kB] Get:12 http://localhost/debian/ sid/main libmagic1 amd64 5.09-2 [246 kB] Get:13 http://localhost/debian/ sid/main file amd64 5.09-2 [52.0 kB] Get:14 http://localhost/debian/ sid/main gettext-base amd64 0.18.1.1-5 [154 kB] Get:15 http://localhost/debian/ sid/main libbison-dev amd64 1:2.5.dfsg-2.1 [289 kB] Get:16 http://localhost/debian/ sid/main bison amd64 1:2.5.dfsg-2.1 [689 kB] Get:17 http://localhost/debian/ sid/main html2text amd64 1.3.2a-15 [103 kB] Get:18 http://localhost/debian/ sid/main gettext amd64 0.18.1.1-5 [2080 kB] Get:19 http://localhost/debian/ sid/main intltool-debian all 0.35.0+20060710.1 [30.8 kB] Get:20 http://localhost/debian/ sid/main po-debconf all 1.0.16+nmu2 [224 kB] Get:21 http://localhost/debian/ sid/main debhelper all 8.9.14 [693 kB] Get:22 http://localhost/debian/ sid/main zlib1g-dev amd64 1:1.2.3.4.dfsg-3 [192 kB] Get:23 http://localhost/debian/ sid/main minisat amd64 1:2.2.1-3 [130 kB] Preconfiguring packages ... Fetched 11.4 MB in 0s (35.6 MB/s) Selecting previously unselected package libpipeline1. (Reading database ... 10821 files and directories currently installed.) Unpacking libpipeline1 (from .../libpipeline1_1.2.0-5_amd64.deb) ... Selecting previously unselected package libpcre3. Unpacking libpcre3 (from .../libpcre3_8.12-4_amd64.deb) ... Selecting previously unselected package m4. Unpacking m4 (from .../archives/m4_1.4.16-2_amd64.deb) ... Selecting previously unselected package flex. Unpacking flex (from .../flex_2.5.35-10_amd64.deb) ... Selecting previously unselected package libglib2.0-0. Unpacking libglib2.0-0 (from .../libglib2.0-0_2.30.2-4_amd64.deb) ... Selecting previously unselected package libxml2. Unpacking libxml2 (from .../libxml2_2.7.8.dfsg-5.1_amd64.deb) ... Selecting previously unselected package libcroco3. Unpacking libcroco3 (from .../libcroco3_0.6.2-2_amd64.deb) ... Selecting previously unselected package libunistring0. Unpacking libunistring0 (from .../libunistring0_0.9.3-5_amd64.deb) ... Selecting previously unselected package bsdmainutils. Unpacking bsdmainutils (from .../bsdmainutils_8.2.3_amd64.deb) ... Selecting previously unselected package groff-base. Unpacking groff-base (from .../groff-base_1.21-6_amd64.deb) ... Selecting previously unselected package man-db. Unpacking man-db (from .../man-db_2.6.0.2-3_amd64.deb) ... Selecting previously unselected package libmagic1. Unpacking libmagic1 (from .../libmagic1_5.09-2_amd64.deb) ... Selecting previously unselected package file. Unpacking file (from .../archives/file_5.09-2_amd64.deb) ... Selecting previously unselected package gettext-base. Unpacking gettext-base (from .../gettext-base_0.18.1.1-5_amd64.deb) ... Selecting previously unselected package libbison-dev. Unpacking libbison-dev (from .../libbison-dev_1%3a2.5.dfsg-2.1_amd64.deb) ... Selecting previously unselected package bison. Unpacking bison (from .../bison_1%3a2.5.dfsg-2.1_amd64.deb) ... Selecting previously unselected package html2text. Unpacking html2text (from .../html2text_1.3.2a-15_amd64.deb) ... Selecting previously unselected package gettext. Unpacking gettext (from .../gettext_0.18.1.1-5_amd64.deb) ... Selecting previously unselected package intltool-debian. Unpacking intltool-debian (from .../intltool-debian_0.35.0+20060710.1_all.deb) ... Selecting previously unselected package po-debconf. Unpacking po-debconf (from .../po-debconf_1.0.16+nmu2_all.deb) ... Selecting previously unselected package debhelper. Unpacking debhelper (from .../debhelper_8.9.14_all.deb) ... Selecting previously unselected package zlib1g-dev. Unpacking zlib1g-dev (from .../zlib1g-dev_1%3a1.2.3.4.dfsg-3_amd64.deb) ... Selecting previously unselected package minisat. Unpacking minisat (from .../minisat_1%3a2.2.1-3_amd64.deb) ... Selecting previously unselected package sbuild-build-depends-cbmc-dummy. Unpacking sbuild-build-depends-cbmc-dummy (from .../sbuild-build-depends-cbmc-dummy.deb) ... Processing triggers for install-info ... Setting up libpipeline1 (1.2.0-5) ... Setting up libpcre3 (8.12-4) ... Setting up m4 (1.4.16-2) ... Setting up flex (2.5.35-10) ... Setting up libglib2.0-0 (2.30.2-4) ... No schema files found: doing nothing. Setting up libxml2 (2.7.8.dfsg-5.1) ... Setting up libcroco3 (0.6.2-2) ... Setting up libunistring0 (0.9.3-5) ... Setting up bsdmainutils (8.2.3) ... update-alternatives: using /usr/bin/bsd-write to provide /usr/bin/write (write) in auto mode. update-alternatives: using /usr/bin/bsd-from to provide /usr/bin/from (from) in auto mode. Setting up groff-base (1.21-6) ... Setting up man-db (2.6.0.2-3) ... Building database of manual pages ... Setting up libmagic1 (5.09-2) ... Setting up file (5.09-2) ... Setting up gettext-base (0.18.1.1-5) ... Setting up libbison-dev (1:2.5.dfsg-2.1) ... Setting up bison (1:2.5.dfsg-2.1) ... update-alternatives: using /usr/bin/bison.yacc to provide /usr/bin/yacc (yacc) in auto mode. Setting up html2text (1.3.2a-15) ... Setting up gettext (0.18.1.1-5) ... Setting up intltool-debian (0.35.0+20060710.1) ... Setting up po-debconf (1.0.16+nmu2) ... Setting up debhelper (8.9.14) ... Setting up zlib1g-dev (1:1.2.3.4.dfsg-3) ... Setting up minisat (1:2.2.1-3) ... Setting up sbuild-build-depends-cbmc-dummy (0.invalid.0) ... ┌──────────────────────────────────────────────────────────────────────────────┐ │ Build environment │ └──────────────────────────────────────────────────────────────────────────────┘ Kernel: Linux 2.6.32-5-amd64 amd64 (x86_64) Toolchain package versions: binutils_2.22-4 dpkg-dev_1.16.1.2 g++-4.6_4.6.2-9 gcc-4.6_4.6.2-9 libc6-dev_2.13-24 libstdc++6_4.6.2-9 libstdc++6-4.6-dev_4.6.2-9 linux-libc-dev_3.1.8-2 Package versions: apt_0.8.15.9 apt-utils_0.8.15.9 base-files_6.5 base-passwd_3.5.24 bash_4.2-1 binutils_2.22-4 bison_1:2.5.dfsg-2.1 bsdmainutils_8.2.3 bsdutils_1:2.20.1-1.1 build-essential_11.5 bzip2_1.0.6-1 clang_3.0-5 coreutils_8.13-3 cpp_4:4.6.2-4 cpp-4.6_4.6.2-9 dash_0.5.7-2 debconf_1.5.41 debfoster_2.7-1.1 debhelper_8.9.14 debian-archive-keyring_2010.08.28 debianutils_4.1 diffutils_1:3.2-1 dpkg_1.16.1.2 dpkg-dev_1.16.1.2 e2fslibs_1.42-1 e2fsprogs_1.42-1 fakeroot_1.18.2-1 file_5.09-2 findutils_4.4.2-4 flex_2.5.35-10 g++_4:4.6.2-4 g++-4.6_4.6.2-9 gcc_4:4.6.2-4 gcc-4.6_4.6.2-9 gcc-4.6-base_4.6.2-9 gettext_0.18.1.1-5 gettext-base_0.18.1.1-5 gnupg_1.4.11-3 gpgv_1.4.11-3 grep_2.10-1 groff-base_1.21-6 gzip_1.4-2 hostname_3.09 html2text_1.3.2a-15 initscripts_2.88dsf-18 insserv_1.14.0-2.1 install-info_4.13a.dfsg.1-8 intltool-debian_0.35.0+20060710.1 less_444-1 libacl1_2.2.51-5 libattr1_1:2.4.46-5 libbison-dev_1:2.5.dfsg-2.1 libblkid1_2.20.1-1.1 libbz2-1.0_1.0.6-1 libc-bin_2.13-24 libc-dev-bin_2.13-24 libc6_2.13-24 libc6-dev_2.13-24 libclang-common-dev_3.0-5 libclass-isa-perl_0.36-3 libcomerr2_1.42-1 libcroco3_0.6.2-2 libdb5.1_5.1.29-1 libdpkg-perl_1.16.1.2 libffi5_3.0.10-3 libgc1c2_1:7.1-8 libgcc1_1:4.6.2-9 libgdbm3_1.8.3-10 libglib2.0-0_2.30.2-4 libgmp10_2:5.0.2+dfsg-2 libgomp1_4.6.2-9 libllvm3.0_3.0-5 liblzma2_5.1.1alpha+20110809-2 liblzma5_5.1.1alpha+20110809-3 libmagic1_5.09-2 libmount1_2.20.1-1.1 libmpc2_0.9-4 libmpfr4_3.1.0-3 libncurses5_5.9-4 libncursesw5_5.9-4 libpam-modules_1.1.3-6 libpam-modules-bin_1.1.3-6 libpam-runtime_1.1.3-6 libpam0g_1.1.3-6 libpcre3_8.12-4 libpipeline1_1.2.0-5 libquadmath0_4.6.2-9 libreadline6_6.2-8 libselinux1_2.1.0-4 libsepol1_2.1.0-1.2 libslang2_2.2.4-5 libss2_1.42-1 libstdc++6_4.6.2-9 libstdc++6-4.6-dev_4.6.2-9 libswitch-perl_2.16-2 libtimedate-perl_1.2000-1 libtinfo5_5.9-4 libunistring0_0.9.3-5 libusb-0.1-4_2:0.1.12-20 libuuid1_2.20.1-1.1 libxml2_2.7.8.dfsg-5.1 linux-libc-dev_3.1.8-2 login_1:4.1.4.2+svn3283-3 lsb-base_3.2-28 m4_1.4.16-2 make_3.81-8.1 man-db_2.6.0.2-3 mawk_1.3.3-16 minisat_1:2.2.1-3 mount_2.20.1-1.1 multiarch-support_2.13-24 ncurses-base_5.9-4 ncurses-bin_5.9-4 nvi_1.81.6-8.2 passwd_1:4.1.4.2+svn3283-3 patch_2.6.1-2 perl_5.14.2-6 perl-base_5.14.2-6 perl-modules_5.14.2-6 po-debconf_1.0.16+nmu2 readline-common_6.2-8 sbuild-build-depends-cbmc-dummy_0.invalid.0 sbuild-build-depends-core-dummy_0.invalid.0 sed_4.2.1-9 sensible-utils_0.0.6 sysv-rc_2.88dsf-18 sysvinit_2.88dsf-18 sysvinit-utils_2.88dsf-18 tar_1.26-4 tzdata_2011n-2 util-linux_2.20.1-1.1 xz-utils_5.1.1alpha+20110809-3 zlib1g_1:1.2.3.4.dfsg-3 zlib1g-dev_1:1.2.3.4.dfsg-3 ┌──────────────────────────────────────────────────────────────────────────────┐ │ Build │ └──────────────────────────────────────────────────────────────────────────────┘ Unpack source ───────────── gpgv: keyblock resource `/var/lib/sbuild/.gnupg/trustedkeys.gpg': file open error gpgv: Signature made Sat Oct 22 22:17:17 2011 CEST using DSA key ID 76D52AC4 gpgv: Can't check signature: public key not found dpkg-source: warning: failed to verify signature on ./cbmc_4.0-4.dsc dpkg-source: info: extracting cbmc in cbmc-4.0 dpkg-source: info: unpacking cbmc_4.0.orig.tar.gz dpkg-source: info: unpacking cbmc_4.0-4.debian.tar.gz dpkg-source: info: applying top-makefile dpkg-source: info: applying debug-info dpkg-source: info: applying minisat-debian dpkg-source: info: applying freebsd-compat dpkg-source: info: applying LIBS-linker-fix Check disc space ──────────────── Sufficient free space for build dpkg-buildpackage ───────────────── dpkg-buildpackage: source package cbmc dpkg-buildpackage: source version 4.0-4 dpkg-source --before-build cbmc-4.0 dpkg-buildpackage: host architecture amd64 fakeroot debian/rules clean dh --parallel clean dh_testdir -O--parallel dh_auto_clean -O--parallel make[1]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0' make -C src clean make[2]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0/src' if [ -e ansi-c/. ] ; then \ make -C ansi-c clean ; \ fi if [ -e big-int/. ] ; then \ make -C big-int clean ; \ fi if [ -e cbmc/. ] ; then \ make -C cbmc clean ; \ fi if [ -e cpp/. ] ; then \ make -C cpp clean ; \ fi if [ -e goto-cc/. ] ; then \ make -C goto-cc clean ; \ fi if [ -e goto-instrument/. ] ; then \ make -C goto-instrument clean ; \ fi if [ -e goto-programs/. ] ; then \ make -C goto-programs clean ; \ fi if [ -e goto-symex/. ] ; then \ make -C goto-symex clean ; \ fi if [ -e langapi/. ] ; then \ make -C langapi clean ; \ fi if [ -e pointer-analysis/. ] ; then \ make -C pointer-analysis clean ; \ fi make[3]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0/src/big-int' rm -f bigint-test.o bigint-func.o bigint.o test-bigint make[3]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0/src/big-int' make[3]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0/src/cbmc' rm -f main.o parseoptions.o bmc.o dimacs.o languages.o bv_cbmc.o symex_bmc.o show_vcc.o cbmc_solvers.o xml_interface.o counterexample_beautification.o counterexample_beautification_greedy.o counterexample_beautification_pbs.o cbmc if [ -e solvers/. ] ; then \ make -C solvers clean ; \ make[3]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0/src/goto-instrument' fi rm -f main.o parseoptions.o document_claims.o languages.o uninitialized.o uninitialized_domain.o full_slicer.o object_id.o show_locations.o points_to.o alignment_checks.o goto-instrument make[3]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0/src/goto-cc' rm -f goto-cc.o cmdline_options.o get_base_name.o gcc_cmdline.o ms_cl_cmdline.o compile.o armcc_cmdline.o languages.o goto_cc_cmdline.o xml_binaries/xml_irep_hashing.o xml_binaries/xml_symbol_hashing.o xml_binaries/xml_symbol.o xml_binaries/xml_goto_function.o xml_binaries/xml_goto_function_hashing.o xml_binaries/xml_goto_program.o xml_binaries/xml_goto_program_hashing.o xml_binaries/read_goto_object.o goto-cc.d cmdline_options.d get_base_name.d gcc_cmdline.d ms_cl_cmdline.d compile.d armcc_cmdline.d languages.d goto_cc_cmdline.d xml_binaries/xml_irep_hashing.d xml_binaries/xml_symbol_hashing.d xml_binaries/xml_symbol.d xml_binaries/xml_goto_function.d xml_binaries/xml_goto_function_hashing.d xml_binaries/xml_goto_program.d xml_binaries/xml_goto_program_hashing.d xml_binaries/read_goto_object.d goto-cc make[3]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0/src/cbmc' make[3]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0/src/goto-instrument' make[3]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0/src/langapi' rm -f mode.o language_ui.o languages.o language_util.o langapi.a if [ -e util/. ] ; then \ make -C util clean ; \ fi if [ -e xmllang/. ] ; then \ make -C xmllang clean ; \ fi make[3]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0/src/goto-cc' make[3]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0/src/goto-symex' rm -f symex_target.o symex_target_equation.o basic_symex.o symex_main.o goto_trace.o build_goto_trace.o symex_function.o goto_symex_state.o symex_dereference.o symex_goto.o builtin_functions.o slice.o symex_other.o slice_by_trace.o xml_goto_trace.o symex_decl.o precondition.o postcondition.o symex_clean_expr.o symex_dereference_state.o vcd_goto_trace.o auto_objects.o goto-symex.a make[3]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0/src/pointer-analysis' rm -f value_set.o goto_program_dereference.o value_set_analysis.o dereference.o pointer_offset_sum.o add_failed_symbols.o show_value_sets.o value_set_domain.o rewrite_index.o value_set_analysis_fi.o value_set_fi.o value_set_domain_fi.o value_set_analysis_fivr.o value_set_fivr.o value_set_domain_fivr.o value_set_analysis_fivrns.o value_set_fivrns.o value_set_domain_fivrns.o pointer-analysis.a make[3]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0/src/ansi-c' rm -f c_typecast.o y.tab.o lex.yy.o ansi_c_parser.o expr2c.o ansi_c_language.o c_sizeof.o c_main.o c_types.o c_final.o trans_unit.o ansi_c_typecheck.o c_link.o c_preprocess.o c_link_type_eq.o c_typecheck_base.o c_typecheck_initializer.o c_typecheck_typecast.o c_typecheck_code.o c_typecheck_expr.o c_typecheck_type.o string_constant.o c_qualifiers.o c_typecheck_argc_argv.o ansi_c_parse_tree.o preprocessor_line.o ansi_c_convert.o ansi_c_convert_type.o type2name.o cprover_library.o anonymous_member.o printf_formatter.o internal_additions.o ansi_c_declaration.o designator.o concatenate_strings.o literals/parse_float.o literals/unescape_string.o literals/convert_float_literal.o literals/convert_character_literal.o literals/convert_integer_literal.o literals/convert_string_literal.o ansi-c.a make[3]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0/src/langapi' make[3]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0/src/cpp' rm -f cpp_id.o cpp_language.o expr2cpp.o cpp_parser.o lex.yy.o cpp_typecheck.o cpp_convert_type.o cpp_typecheck_expr.o cpp_typecheck_code.o cpp_typecheck_type.o parse.o cpp_parse_tree.o cpp_token_buffer.o cpp_typecheck_fargs.o cpp_typecheck_resolve.o cpp_util.o cpp_typecheck_function.o cpp_typecheck_namespace.o cpp_name.o cpp_is_pod.o cpp_scope.o cpp_typecheck_find_constructor.o template_map.o cpp_scopes.o cpp_declarator.o cpp_instantiate_template.o internal_additions.o cpp_type2name.o cpp_typecheck_linkage_spec.o cpp_typecheck_template.o cpp_typecheck_function_bodies.o cpp_typecheck_initializer.o cpp_typecheck_compound_type.o cpp_constructor.o cpp_destructor.o cpp_final.o cpp_typecheck_conversions.o cpp_typecheck_declaration.o cpp_declarator_converter.o cpp_declaration.o cpp_namespace_spec.o cpp_typecheck_using.o cpp_typecheck_enum_type.o cpp_typecheck_bases.o cpp_typecheck_constructor.o cpp_typecheck_virtual_table.o cpp.a lex.yy.cpp y.tab.cpp.output make[3]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0/src/goto-programs' rm -f goto_convert.o goto_function.o goto_main.o goto_sideeffects.o goto_program.o basic_blocks.o goto_threads.o goto_check.o goto_function_pointers.o goto_functions.o goto_inline.o remove_skip.o goto_convert_functions.o string_instrumentation.o builtin_functions.o show_claims.o destructor.o set_claims.o slicer.o invariant_set.o invariant_propagation.o add_race_assertions.o rw_set.o read_goto_binary.o invariant_set_domain.o static_analysis.o string_abstraction.o goto_program_serialization.o goto_function_serialization.o read_bin_goto_object.o goto_program_irep.o interpreter.o interpreter_evaluate.o flow_insensitive_analysis.o format_strings.o loop_numbers.o pointer_arithmetic.o goto_program_template.o write_goto_binary.o remove_unreachable.o remove_unused_functions.o dynamic_memory.o dump_c.o wp.o goto_rw.o goto_clean_expr.o safety_checker.o compute_called_functions.o link_to_library.o goto-programs.a test_wp make[3]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0/src/goto-symex' make[3]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0/src/pointer-analysis' rm -f y.tab.h y.tab.cpp lex.yy.cpp y.tab.cpp.output y.output make[3]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0/src/cpp' make[3]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0/src/goto-programs' rm -f library/converter cprover_library.inc make[3]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0/src/ansi-c' make[3]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0/src/xmllang' rm -f xml_language.o xml_parser.o y.tab.o lex.yy.o xml_typecheck.o xml_parse_tree.o \ y.tab.h y.tab.cpp lex.yy.cpp y.tab.cpp.output y.output \ xmllang.a make[3]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0/src/xmllang' make[3]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0/src/solvers' rm -f sat/satcheck_minisat2.o sat/cnf.o sat/dimacs_cnf.o sat/cnf_clause_list.o sat/pbs_dimacs_cnf.o sat/read_dimacs_cnf.o sat/resolution_proof.o sat/satcheck.o qbf/qdimacs_cnf.o qbf/qbf_quantor.o qbf/qbf_skizzo.o qbf/qdimacs_core.o qbf/qbf_qube.o qbf/qbf_qube_core.o prop/prop.o prop/prop_conv.o prop/prop_conv_store.o prop/aig_formula.o prop/aig.o prop/aig_prop.o cvc/cvc_prop.o cvc/cvc_conv.o cvc/cvc_dec.o smt1/smt1_dec.o smt1/smt1_prop.o smt1/smt1_conv.o smt2/smt2_dec.o smt2/smt2_prop.o smt2/smt2_conv.o dplib/dplib_conv.o dplib/dplib_dec.o dplib/dplib_prop.o flattening/equality.o flattening/arrays.o flattening/functions.o flattening/sat_minimizer.o flattening/boolbv_width.o flattening/boolbv.o flattening/boolbv_constraint_select_one.o flattening/bv_pointers.o flattening/bv_utils.o flattening/boolbv_abs.o flattening/boolbv_with.o flattening/boolbv_typecast.o flattening/boolbv_index.o flattening/boolbv_member.o flattening/boolbv_if.o flattening/boolbv_byte_extract.o flattening/boolbv_add_sub.o flattening/boolbv_mult.o flattening/boolbv_constant.o flattening/boolbv_extractbit.o flattening/boolbv_bv_rel.o flattening/boolbv_shift.o flattening/boolbv_case.o flattening/boolbv_cond.o flattening/boolbv_concatenation.o flattening/boolbv_div.o flattening/boolbv_mod.o flattening/boolbv_extractbits.o flattening/boolbv_replication.o flattening/boolbv_reduction.o flattening/boolbv_overflow.o flattening/boolbv_get.o flattening/boolbv_bitwise.o flattening/boolbv_equality.o flattening/boolbv_unary_minus.o flattening/boolbv_ieee_float_rel.o flattening/pointer_logic.o flattening/boolbv_quantifier.o flattening/boolbv_struct.o flattening/boolbv_byte_update.o flattening/boolbv_array_of.o flattening/boolbv_map.o flattening/boolbv_type.o flattening/boolbv_union.o solvers.a make[3]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0/src/util' rm -f arith_tools.o base_type.o cmdline.o config.o context.o expr.o expr_util.o i2string.o irep.o language.o lispexpr.o lispirep.o location.o message.o language_file.o mp_arith.o namespace.o parseoptions.o rename.o replace_expr.o threeval.o typecheck.o graph.o type.o cnf_simplify.o str_getline.o strstream2string.o bitvector.o parser.o map_util.o replace_symbol.o actuals.o get_module.o string_hash.o string_container.o identifier.o rational.o options.o c_misc.o simplify_expr.o dstring.o find_symbols.o rational_tools.o ui_message.o simplify_utils.o time_stopping.o symbol.o irep_hash_container.o type_eq.o guard.o array_name.o gcd.o message_stream.o substitute.o decision_procedure.o union_find.o pretty_names.o xml.o xml_irep.o std_types.o std_code.o format_constant.o find_macros.o ref_expr_set.o std_expr.o irep_serialization.o symbol_serialization.o fixedbv.o ieee_float.o signal_catcher.o pointer_offset_size.o bv_arithmetic.o tempdir.o tempfile.o timer.o irep_ids.o util.a rm -f irep_ids.h irep_ids.inc make[3]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0/src/solvers' rm -f ieee_float_test ieee_float_test.o rm -f irep_ids_convert irep_ids_convert.o make[3]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0/src/util' rm -f *.o make[2]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0/src' make[1]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0' dh_clean -O--parallel dpkg-source -b cbmc-4.0 dpkg-source: info: using source format `3.0 (quilt)' dpkg-source: info: building cbmc using existing ./cbmc_4.0.orig.tar.gz dpkg-source: info: building cbmc in cbmc_4.0-4.debian.tar.gz dpkg-source: info: building cbmc in cbmc_4.0-4.dsc debian/rules build dh --parallel build dh_testdir -O--parallel dh_auto_configure -O--parallel dh_auto_build -O--parallel make[1]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0' make -C src make[2]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0/src' ## Entering big-int make -C big-int make[3]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0/src/big-int' g++ -Wall -MMD -O2 -g -c -o bigint-test.o bigint-test.cc g++ -Wall -MMD -O2 -g -c -o bigint-func.o bigint-func.cc g++ -Wall -MMD -O2 -g -c -o bigint.o bigint.cc g++ -Wall -MMD -O2 -g -o test-bigint bigint-test.o bigint-func.o bigint.o make[3]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0/src/big-int' ## Entering util make -C util make[3]: Entering directory `/build/cbmc-3FyMI5/cbmc-4.0/src/util' g++ -c -Wall -MMD -O2 -g -I .. -I . -o irep_ids_convert.o irep_ids_convert.cpp g++ -o irep_ids_convert irep_ids_convert.o ./irep_ids_convert header < irep_ids.txt > irep_ids.h g++ -c -Wall -MMD -O2 -g -I .. -I . -o arith_tools.o arith_tools.cpp g++ -c -Wall -MMD -O2 -g -I .. -I . -o base_type.o base_type.cpp In file included from base_type.cpp:13: In file included from ./base_type.h:13: In file included from ./namespace.h:12: In file included from ./context.h:18: ./symbol.h:48:25: warning: 'thread_local' is a keyword in C++11 [-Wc++11-compat] bool static_lifetime, thread_local; ^ In file included from base_type.cpp:13: In file included from ./base_type.h:14: In file included from ./union_find.h:16: ./numbering.h:32:7: error: use of undeclared identifier 'push_back' push_back(a); ^ this-> ./union_find.h:142:22: note: in instantiation of member function 'numbering::number' requested here unsigned n=subt::number(a); ^ ./union_find.h:109:17: note: in instantiation of member function 'union_find::number' requested here unsigned na=number(a), nb=number(b); ^ base_type.cpp:173:20: note: in instantiation of member function 'union_find::make_union' requested here if(identifiers.make_union( ^ /usr/include/c++/4.6/bits/stl_vector.h:826:7: note: must qualify identifier to find this declaration in dependent base class push_back(const value_type& __x) ^ 1 warning and 1 error generated. make[3]: *** [base_type.o] Error 1 make[3]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0/src/util' make[2]: *** [util.dir] Error 2 make[2]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0/src' make[1]: *** [all] Error 2 make[1]: Leaving directory `/build/cbmc-3FyMI5/cbmc-4.0' dh_auto_build: make -j10 returned exit code 2 make: *** [build] Error 2 dpkg-buildpackage: error: debian/rules build gave error exit status 2 ──────────────────────────────────────────────────────────────────────────────── Build finished at 20120113-0008 Finished ──────── E: Build failure (dpkg-buildpackage died) ┌──────────────────────────────────────────────────────────────────────────────┐ │ Cleanup │ └──────────────────────────────────────────────────────────────────────────────┘ Purging /var/lib/schroot/mount/lsid64b-1b570873-b857-488a-bf01-393a9de7f29e/build/cbmc-3FyMI5 Not cleaning session: cloned chroot in use ┌──────────────────────────────────────────────────────────────────────────────┐ │ Summary │ └──────────────────────────────────────────────────────────────────────────────┘ Architecture: amd64 Build-Space: 7452 Build-Time: 5 Distribution: lsid64b Fail-Stage: build Install-Time: 7 Job: cbmc_4.0-4 Package: cbmc Package-Time: 25 Source-Version: 4.0-4 Space: 7452 Status: attempted Version: 4.0-4 ──────────────────────────────────────────────────────────────────────────────── Finished at 20120113-0008 Build needed 00:00:25, 7452k disc space DC-Message: Failed, but took only 266.461046. Retrying, you never know. Another build requested exclusive access to the build node Another build requested exclusive access to the build node Another build requested exclusive access to the build node Another build requested exclusive access to the build node Another build requested exclusive access to the build node Another build requested exclusive access to the build node Another build requested exclusive access to the build node Another build requested exclusive access to the build node Requested exclusive mode, but other builds running. Requested exclusive mode, but other builds running. Requested exclusive mode, but other builds running. Requested exclusive mode, but other builds running. Requested exclusive mode, but other builds running. Requested exclusive mode, but other builds running. Requested exclusive mode, but other builds running. Requested exclusive mode, but other builds running. Requested exclusive mode, but other builds running. Requested exclusive mode, but other builds running. Requested exclusive mode, but other builds running. Requested exclusive mode, but other builds running. sbuild (Debian sbuild) 0.62.2 (05 Apr 2011) on stremi-5.reims.grid5000.fr ╔══════════════════════════════════════════════════════════════════════════════╗ ║ cbmc 4.0-4 (amd64) 13 Jan 2012 00:18 ║ ╚══════════════════════════════════════════════════════════════════════════════╝ Package: cbmc Version: 4.0-4 Source Version: 4.0-4 Distribution: lsid64b Architecture: amd64 ┌──────────────────────────────────────────────────────────────────────────────┐ │ Update chroot │ └──────────────────────────────────────────────────────────────────────────────┘ Ign http://localhost sid InRelease Get:1 http://localhost sid Release.gpg [836 B] Get:2 http://localhost sid Release [188 kB] Ign http://localhost sid/main Sources/DiffIndex Ign http://localhost sid/main amd64 Packages/DiffIndex Ign http://localhost sid/main TranslationIndex Get:3 http://localhost sid/main Sources [7544 kB] Get:4 http://localhost sid/main amd64 Packages [10.4 MB] Ign http://localhost sid/main Translation-en Fetched 18.2 MB in 3s (5477 kB/s) Reading package lists... Reading package lists... Building dependency tree... Reading state information... The following packages have been kept back: clang cpp-4.6 g++-4.6 gcc-4.6 gcc-4.6-base libgcc1 libgomp1 libquadmath0 libstdc++6 libstdc++6-4.6-dev 0 upgraded, 0 newly installed, 0 to remove and 10 not upgraded. ┌──────────────────────────────────────────────────────────────────────────────┐ │ Fetch source files │ └──────────────────────────────────────────────────────────────────────────────┘ Check APT ───────── Checking available source versions... Download source files with APT ────────────────────────────── Reading package lists... Building dependency tree... Reading state information... Need to get 875 kB of source archives. Get:1 http://localhost/debian/ sid/main cbmc 4.0-4 (dsc) [1064 B] Get:2 http://localhost/debian/ sid/main cbmc 4.0-4 (tar) [869 kB] Get:3 http://localhost/debian/ sid/main cbmc 4.0-4 (diff) [4883 B] Fetched 875 kB in 0s (29.7 MB/s) Download complete and in download only mode Check arch ────────── Merged Build-Depends: build-essential, fakeroot Filtered Build-Depends: build-essential, fakeroot dpkg-deb: building package `sbuild-build-depends-core-dummy' in `/build/cbmc-jcBgCw/resolver-cf4pNY/apt_archive/sbuild-build-depends-core-dummy.deb'. OK Reading package lists... ┌──────────────────────────────────────────────────────────────────────────────┐ │ Install core build dependencies (apt-based resolver) │ └──────────────────────────────────────────────────────────────────────────────┘ Installing build dependencies Reading package lists... Building dependency tree... Reading state information... The following NEW packages will be installed: sbuild-build-depends-core-dummy 0 upgraded, 1 newly installed, 0 to remove and 10 not upgraded. Need to get 0 B/702 B of archives. After this operation, 0 B of additional disk space will be used. WARNING: The following packages cannot be authenticated! sbuild-build-depends-core-dummy Authentication warning overridden. Selecting previously unselected package sbuild-build-depends-core-dummy. (Reading database ... 10821 files and directories currently installed.) Unpacking sbuild-build-depends-core-dummy (from .../sbuild-build-depends-core-dummy.deb) ... Setting up sbuild-build-depends-core-dummy (0.invalid.0) ... Cannot open /var/lib/schroot/mount/lsid64b-eb409885-d07c-40c5-ba15-008d842e65a0/etc/lsb-release: No such file or directory Merged Build-Depends: base-files, base-passwd, bash, coreutils, dash, debianutils, diffutils, dpkg, e2fsprogs, findutils, grep, gzip, hostname, ncurses-base, ncurses-bin, perl-base, sed, login, sysvinit-utils, sysvinit, tar, bsdutils, mount, util-linux, libc6-dev | libc-dev, gcc (>= 4:4.4.3), g++ (>= 4:4.4.3), make, dpkg-dev (>= 1.13.5), debhelper (>= 7.0.50~), minisat (>= 1:2.2.1-2), zlib1g-dev, flex, bison Filtered Build-Depends: base-files, base-passwd, bash, coreutils, dash, debianutils, diffutils, dpkg, e2fsprogs, findutils, grep, gzip, hostname, ncurses-base, ncurses-bin, perl-base, sed, login, sysvinit-utils, sysvinit, tar, bsdutils, mount, util-linux, libc6-dev, gcc (>= 4:4.4.3), g++ (>= 4:4.4.3), make, dpkg-dev (>= 1.13.5), debhelper (>= 7.0.50~), minisat (>= 1:2.2.1-2), zlib1g-dev, flex, bison dpkg-deb: building package `sbuild-build-depends-cbmc-dummy' in `/build/cbmc-jcBgCw/resolver-RjC5FA/apt_archive/sbuild-build-depends-cbmc-dummy.deb'. OK Reading package lists... ┌──────────────────────────────────────────────────────────────────────────────┐ │ Install cbmc build dependencies (apt-based resolver) │ └──────────────────────────────────────────────────────────────────────────────┘ Installing build dependencies Reading package lists... Building dependency tree... Reading state information... The following extra packages will be installed: bison bsdmainutils debhelper file flex gettext gettext-base groff-base html2text intltool-debian libbison-dev libcroco3 libglib2.0-0 libmagic1 libpcre3 libpipeline1 libunistring0 libxml2 m4 man-db minisat po-debconf zlib1g-dev Suggested packages: bison-doc wamerican wordlist whois vacation dh-make gettext-doc groff www-browser libmail-box-perl Recommended packages: curl wget lynx-cur autopoint libglib2.0-data shared-mime-info xml-core libmail-sendmail-perl The following NEW packages will be installed: bison bsdmainutils debhelper file flex gettext gettext-base groff-base html2text intltool-debian libbison-dev libcroco3 libglib2.0-0 libmagic1 libpcre3 libpipeline1 libunistring0 libxml2 m4 man-db minisat po-debconf sbuild-build-depends-cbmc-dummy zlib1g-dev 0 upgraded, 24 newly installed, 0 to remove and 10 not upgraded. Need to get 11.4 MB/11.4 MB of archives. After this operation, 30.8 MB of additional disk space will be used. WARNING: The following packages cannot be authenticated! libpipeline1 libpcre3 m4 flex libglib2.0-0 libxml2 libcroco3 libunistring0 bsdmainutils groff-base man-db libmagic1 file gettext-base libbison-dev bison html2text gettext intltool-debian po-debconf debhelper zlib1g-dev minisat sbuild-build-depends-cbmc-dummy Authentication warning overridden. Get:1 http://localhost/debian/ sid/main libpipeline1 amd64 1.2.0-5 [38.2 kB] Get:2 http://localhost/debian/ sid/main libpcre3 amd64 8.12-4 [225 kB] Get:3 http://localhost/debian/ sid/main m4 amd64 1.4.16-2 [259 kB] Get:4 http://localhost/debian/ sid/main flex amd64 2.5.35-10 [332 kB] Get:5 http://localhost/debian/ sid/main libglib2.0-0 amd64 2.30.2-4 [1844 kB] Get:6 http://localhost/debian/ sid/main libxml2 amd64 2.7.8.dfsg-5.1 [891 kB] Get:7 http://localhost/debian/ sid/main libcroco3 amd64 0.6.2-2 [122 kB] Get:8 http://localhost/debian/ sid/main libunistring0 amd64 0.9.3-5 [434 kB] Get:9 http://localhost/debian/ sid/main bsdmainutils amd64 8.2.3 [208 kB] Get:10 http://localhost/debian/ sid/main groff-base amd64 1.21-6 [1150 kB] Get:11 http://localhost/debian/ sid/main man-db amd64 2.6.0.2-3 [1015 kB] Get:12 http://localhost/debian/ sid/main libmagic1 amd64 5.09-2 [246 kB] Get:13 http://localhost/debian/ sid/main file amd64 5.09-2 [52.0 kB] Get:14 http://localhost/debian/ sid/main gettext-base amd64 0.18.1.1-5 [154 kB] Get:15 http://localhost/debian/ sid/main libbison-dev amd64 1:2.5.dfsg-2.1 [289 kB] Get:16 http://localhost/debian/ sid/main bison amd64 1:2.5.dfsg-2.1 [689 kB] Get:17 http://localhost/debian/ sid/main html2text amd64 1.3.2a-15 [103 kB] Get:18 http://localhost/debian/ sid/main gettext amd64 0.18.1.1-5 [2080 kB] Get:19 http://localhost/debian/ sid/main intltool-debian all 0.35.0+20060710.1 [30.8 kB] Get:20 http://localhost/debian/ sid/main po-debconf all 1.0.16+nmu2 [224 kB] Get:21 http://localhost/debian/ sid/main debhelper all 8.9.14 [693 kB] Get:22 http://localhost/debian/ sid/main zlib1g-dev amd64 1:1.2.3.4.dfsg-3 [192 kB] Get:23 http://localhost/debian/ sid/main minisat amd64 1:2.2.1-3 [130 kB] Preconfiguring packages ... Fetched 11.4 MB in 0s (42.0 MB/s) Selecting previously unselected package libpipeline1. (Reading database ... 10821 files and directories currently installed.) Unpacking libpipeline1 (from .../libpipeline1_1.2.0-5_amd64.deb) ... Selecting previously unselected package libpcre3. Unpacking libpcre3 (from .../libpcre3_8.12-4_amd64.deb) ... Selecting previously unselected package m4. Unpacking m4 (from .../archives/m4_1.4.16-2_amd64.deb) ... Selecting previously unselected package flex. Unpacking flex (from .../flex_2.5.35-10_amd64.deb) ... Selecting previously unselected package libglib2.0-0. Unpacking libglib2.0-0 (from .../libglib2.0-0_2.30.2-4_amd64.deb) ... Selecting previously unselected package libxml2. Unpacking libxml2 (from .../libxml2_2.7.8.dfsg-5.1_amd64.deb) ... Selecting previously unselected package libcroco3. Unpacking libcroco3 (from .../libcroco3_0.6.2-2_amd64.deb) ... Selecting previously unselected package libunistring0. Unpacking libunistring0 (from .../libunistring0_0.9.3-5_amd64.deb) ... Selecting previously unselected package bsdmainutils. Unpacking bsdmainutils (from .../bsdmainutils_8.2.3_amd64.deb) ... Selecting previously unselected package groff-base. Unpacking groff-base (from .../groff-base_1.21-6_amd64.deb) ... Selecting previously unselected package man-db. Unpacking man-db (from .../man-db_2.6.0.2-3_amd64.deb) ... Selecting previously unselected package libmagic1. Unpacking libmagic1 (from .../libmagic1_5.09-2_amd64.deb) ... Selecting previously unselected package file. Unpacking file (from .../archives/file_5.09-2_amd64.deb) ... Selecting previously unselected package gettext-base. Unpacking gettext-base (from .../gettext-base_0.18.1.1-5_amd64.deb) ... Selecting previously unselected package libbison-dev. Unpacking libbison-dev (from .../libbison-dev_1%3a2.5.dfsg-2.1_amd64.deb) ... Selecting previously unselected package bison. Unpacking bison (from .../bison_1%3a2.5.dfsg-2.1_amd64.deb) ... Selecting previously unselected package html2text. Unpacking html2text (from .../html2text_1.3.2a-15_amd64.deb) ... Selecting previously unselected package gettext. Unpacking gettext (from .../gettext_0.18.1.1-5_amd64.deb) ... Selecting previously unselected package intltool-debian. Unpacking intltool-debian (from .../intltool-debian_0.35.0+20060710.1_all.deb) ... Selecting previously unselected package po-debconf. Unpacking po-debconf (from .../po-debconf_1.0.16+nmu2_all.deb) ... Selecting previously unselected package debhelper. Unpacking debhelper (from .../debhelper_8.9.14_all.deb) ... Selecting previously unselected package zlib1g-dev. Unpacking zlib1g-dev (from .../zlib1g-dev_1%3a1.2.3.4.dfsg-3_amd64.deb) ... Selecting previously unselected package minisat. Unpacking minisat (from .../minisat_1%3a2.2.1-3_amd64.deb) ... Selecting previously unselected package sbuild-build-depends-cbmc-dummy. Unpacking sbuild-build-depends-cbmc-dummy (from .../sbuild-build-depends-cbmc-dummy.deb) ... Processing triggers for install-info ... Setting up libpipeline1 (1.2.0-5) ... Setting up libpcre3 (8.12-4) ... Setting up m4 (1.4.16-2) ... Setting up flex (2.5.35-10) ... Setting up libglib2.0-0 (2.30.2-4) ... No schema files found: doing nothing. Setting up libxml2 (2.7.8.dfsg-5.1) ... Setting up libcroco3 (0.6.2-2) ... Setting up libunistring0 (0.9.3-5) ... Setting up bsdmainutils (8.2.3) ... update-alternatives: using /usr/bin/bsd-write to provide /usr/bin/write (write) in auto mode. update-alternatives: using /usr/bin/bsd-from to provide /usr/bin/from (from) in auto mode. Setting up groff-base (1.21-6) ... Setting up man-db (2.6.0.2-3) ... Building database of manual pages ... Setting up libmagic1 (5.09-2) ... Setting up file (5.09-2) ... Setting up gettext-base (0.18.1.1-5) ... Setting up libbison-dev (1:2.5.dfsg-2.1) ... Setting up bison (1:2.5.dfsg-2.1) ... update-alternatives: using /usr/bin/bison.yacc to provide /usr/bin/yacc (yacc) in auto mode. Setting up html2text (1.3.2a-15) ... Setting up gettext (0.18.1.1-5) ... Setting up intltool-debian (0.35.0+20060710.1) ... Setting up po-debconf (1.0.16+nmu2) ... Setting up debhelper (8.9.14) ... Setting up zlib1g-dev (1:1.2.3.4.dfsg-3) ... Setting up minisat (1:2.2.1-3) ... Setting up sbuild-build-depends-cbmc-dummy (0.invalid.0) ... ┌──────────────────────────────────────────────────────────────────────────────┐ │ Build environment │ └──────────────────────────────────────────────────────────────────────────────┘ Kernel: Linux 2.6.32-5-amd64 amd64 (x86_64) Toolchain package versions: binutils_2.22-4 dpkg-dev_1.16.1.2 g++-4.6_4.6.2-9 gcc-4.6_4.6.2-9 libc6-dev_2.13-24 libstdc++6_4.6.2-9 libstdc++6-4.6-dev_4.6.2-9 linux-libc-dev_3.1.8-2 Package versions: apt_0.8.15.9 apt-utils_0.8.15.9 base-files_6.5 base-passwd_3.5.24 bash_4.2-1 binutils_2.22-4 bison_1:2.5.dfsg-2.1 bsdmainutils_8.2.3 bsdutils_1:2.20.1-1.1 build-essential_11.5 bzip2_1.0.6-1 clang_3.0-5 coreutils_8.13-3 cpp_4:4.6.2-4 cpp-4.6_4.6.2-9 dash_0.5.7-2 debconf_1.5.41 debfoster_2.7-1.1 debhelper_8.9.14 debian-archive-keyring_2010.08.28 debianutils_4.1 diffutils_1:3.2-1 dpkg_1.16.1.2 dpkg-dev_1.16.1.2 e2fslibs_1.42-1 e2fsprogs_1.42-1 fakeroot_1.18.2-1 file_5.09-2 findutils_4.4.2-4 flex_2.5.35-10 g++_4:4.6.2-4 g++-4.6_4.6.2-9 gcc_4:4.6.2-4 gcc-4.6_4.6.2-9 gcc-4.6-base_4.6.2-9 gettext_0.18.1.1-5 gettext-base_0.18.1.1-5 gnupg_1.4.11-3 gpgv_1.4.11-3 grep_2.10-1 groff-base_1.21-6 gzip_1.4-2 hostname_3.09 html2text_1.3.2a-15 initscripts_2.88dsf-18 insserv_1.14.0-2.1 install-info_4.13a.dfsg.1-8 intltool-debian_0.35.0+20060710.1 less_444-1 libacl1_2.2.51-5 libattr1_1:2.4.46-5 libbison-dev_1:2.5.dfsg-2.1 libblkid1_2.20.1-1.1 libbz2-1.0_1.0.6-1 libc-bin_2.13-24 libc-dev-bin_2.13-24 libc6_2.13-24 libc6-dev_2.13-24 libclang-common-dev_3.0-5 libclass-isa-perl_0.36-3 libcomerr2_1.42-1 libcroco3_0.6.2-2 libdb5.1_5.1.29-1 libdpkg-perl_1.16.1.2 libffi5_3.0.10-3 libgc1c2_1:7.1-8 libgcc1_1:4.6.2-9 libgdbm3_1.8.3-10 libglib2.0-0_2.30.2-4 libgmp10_2:5.0.2+dfsg-2 libgomp1_4.6.2-9 libllvm3.0_3.0-5 liblzma2_5.1.1alpha+20110809-2 liblzma5_5.1.1alpha+20110809-3 libmagic1_5.09-2 libmount1_2.20.1-1.1 libmpc2_0.9-4 libmpfr4_3.1.0-3 libncurses5_5.9-4 libncursesw5_5.9-4 libpam-modules_1.1.3-6 libpam-modules-bin_1.1.3-6 libpam-runtime_1.1.3-6 libpam0g_1.1.3-6 libpcre3_8.12-4 libpipeline1_1.2.0-5 libquadmath0_4.6.2-9 libreadline6_6.2-8 libselinux1_2.1.0-4 libsepol1_2.1.0-1.2 libslang2_2.2.4-5 libss2_1.42-1 libstdc++6_4.6.2-9 libstdc++6-4.6-dev_4.6.2-9 libswitch-perl_2.16-2 libtimedate-perl_1.2000-1 libtinfo5_5.9-4 libunistring0_0.9.3-5 libusb-0.1-4_2:0.1.12-20 libuuid1_2.20.1-1.1 libxml2_2.7.8.dfsg-5.1 linux-libc-dev_3.1.8-2 login_1:4.1.4.2+svn3283-3 lsb-base_3.2-28 m4_1.4.16-2 make_3.81-8.1 man-db_2.6.0.2-3 mawk_1.3.3-16 minisat_1:2.2.1-3 mount_2.20.1-1.1 multiarch-support_2.13-24 ncurses-base_5.9-4 ncurses-bin_5.9-4 nvi_1.81.6-8.2 passwd_1:4.1.4.2+svn3283-3 patch_2.6.1-2 perl_5.14.2-6 perl-base_5.14.2-6 perl-modules_5.14.2-6 po-debconf_1.0.16+nmu2 readline-common_6.2-8 sbuild-build-depends-cbmc-dummy_0.invalid.0 sbuild-build-depends-core-dummy_0.invalid.0 sed_4.2.1-9 sensible-utils_0.0.6 sysv-rc_2.88dsf-18 sysvinit_2.88dsf-18 sysvinit-utils_2.88dsf-18 tar_1.26-4 tzdata_2011n-2 util-linux_2.20.1-1.1 xz-utils_5.1.1alpha+20110809-3 zlib1g_1:1.2.3.4.dfsg-3 zlib1g-dev_1:1.2.3.4.dfsg-3 ┌──────────────────────────────────────────────────────────────────────────────┐ │ Build │ └──────────────────────────────────────────────────────────────────────────────┘ Unpack source ───────────── gpgv: keyblock resource `/var/lib/sbuild/.gnupg/trustedkeys.gpg': file open error gpgv: Signature made Sat Oct 22 22:17:17 2011 CEST using DSA key ID 76D52AC4 gpgv: Can't check signature: public key not found dpkg-source: warning: failed to verify signature on ./cbmc_4.0-4.dsc dpkg-source: info: extracting cbmc in cbmc-4.0 dpkg-source: info: unpacking cbmc_4.0.orig.tar.gz dpkg-source: info: unpacking cbmc_4.0-4.debian.tar.gz dpkg-source: info: applying top-makefile dpkg-source: info: applying debug-info dpkg-source: info: applying minisat-debian dpkg-source: info: applying freebsd-compat dpkg-source: info: applying LIBS-linker-fix Check disc space ──────────────── Sufficient free space for build dpkg-buildpackage ───────────────── dpkg-buildpackage: source package cbmc dpkg-buildpackage: source version 4.0-4 dpkg-source --before-build cbmc-4.0 dpkg-buildpackage: host architecture amd64 fakeroot debian/rules clean dh --parallel clean dh_testdir -O--parallel dh_auto_clean -O--parallel make[1]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0' make -C src clean make[2]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0/src' if [ -e ansi-c/. ] ; then \ make -C ansi-c clean ; \ fi if [ -e big-int/. ] ; then \ make -C big-int clean ; \ fi if [ -e cbmc/. ] ; then \ make -C cbmc clean ; \ fi if [ -e cpp/. ] ; then \ make -C cpp clean ; \ fi if [ -e goto-cc/. ] ; then \ make -C goto-cc clean ; \ fi if [ -e goto-instrument/. ] ; then \ make -C goto-instrument clean ; \ fi if [ -e goto-programs/. ] ; then \ make -C goto-programs clean ; \ fi if [ -e goto-symex/. ] ; then \ make -C goto-symex clean ; \ fi if [ -e langapi/. ] ; then \ make -C langapi clean ; \ fi if [ -e pointer-analysis/. ] ; then \ make -C pointer-analysis clean ; \ fi make[3]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0/src/big-int' rm -f bigint-test.o bigint-func.o bigint.o test-bigint make[3]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0/src/cbmc' rm -f main.o parseoptions.o bmc.o dimacs.o languages.o bv_cbmc.o symex_bmc.o show_vcc.o cbmc_solvers.o xml_interface.o counterexample_beautification.o counterexample_beautification_greedy.o counterexample_beautification_pbs.o cbmc make[3]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0/src/big-int' make[3]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0/src/goto-instrument' rm -f main.o parseoptions.o document_claims.o languages.o uninitialized.o uninitialized_domain.o full_slicer.o object_id.o show_locations.o points_to.o alignment_checks.o goto-instrument if [ -e solvers/. ] ; then \ make -C solvers clean ; \ fi make[3]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0/src/langapi' rm -f mode.o language_ui.o languages.o language_util.o langapi.a make[3]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0/src/goto-cc' rm -f goto-cc.o cmdline_options.o get_base_name.o gcc_cmdline.o ms_cl_cmdline.o compile.o armcc_cmdline.o languages.o goto_cc_cmdline.o xml_binaries/xml_irep_hashing.o xml_binaries/xml_symbol_hashing.o xml_binaries/xml_symbol.o xml_binaries/xml_goto_function.o xml_binaries/xml_goto_function_hashing.o xml_binaries/xml_goto_program.o xml_binaries/xml_goto_program_hashing.o xml_binaries/read_goto_object.o goto-cc.d cmdline_options.d get_base_name.d gcc_cmdline.d ms_cl_cmdline.d compile.d armcc_cmdline.d languages.d goto_cc_cmdline.d xml_binaries/xml_irep_hashing.d xml_binaries/xml_symbol_hashing.d xml_binaries/xml_symbol.d xml_binaries/xml_goto_function.d xml_binaries/xml_goto_function_hashing.d xml_binaries/xml_goto_program.d xml_binaries/xml_goto_program_hashing.d xml_binaries/read_goto_object.d goto-cc make[3]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0/src/cbmc' make[3]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0/src/ansi-c' rm -f c_typecast.o y.tab.o lex.yy.o ansi_c_parser.o expr2c.o ansi_c_language.o c_sizeof.o c_main.o c_types.o c_final.o trans_unit.o ansi_c_typecheck.o c_link.o c_preprocess.o c_link_type_eq.o c_typecheck_base.o c_typecheck_initializer.o c_typecheck_typecast.o c_typecheck_code.o c_typecheck_expr.o c_typecheck_type.o string_constant.o c_qualifiers.o c_typecheck_argc_argv.o ansi_c_parse_tree.o preprocessor_line.o ansi_c_convert.o ansi_c_convert_type.o type2name.o cprover_library.o anonymous_member.o printf_formatter.o internal_additions.o ansi_c_declaration.o designator.o concatenate_strings.o literals/parse_float.o literals/unescape_string.o literals/convert_float_literal.o literals/convert_character_literal.o literals/convert_integer_literal.o literals/convert_string_literal.o ansi-c.a make[3]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0/src/goto-symex' rm -f symex_target.o symex_target_equation.o basic_symex.o symex_main.o goto_trace.o build_goto_trace.o symex_function.o goto_symex_state.o symex_dereference.o symex_goto.o builtin_functions.o slice.o symex_other.o slice_by_trace.o xml_goto_trace.o symex_decl.o precondition.o postcondition.o symex_clean_expr.o symex_dereference_state.o vcd_goto_trace.o auto_objects.o goto-symex.a make[3]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0/src/pointer-analysis' rm -f value_set.o goto_program_dereference.o value_set_analysis.o dereference.o pointer_offset_sum.o add_failed_symbols.o show_value_sets.o value_set_domain.o rewrite_index.o value_set_analysis_fi.o value_set_fi.o value_set_domain_fi.o value_set_analysis_fivr.o value_set_fivr.o value_set_domain_fivr.o value_set_analysis_fivrns.o value_set_fivrns.o value_set_domain_fivrns.o pointer-analysis.a if [ -e util/. ] ; then \ make -C util clean ; \ fi make[3]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0/src/cpp' rm -f cpp_id.o cpp_language.o expr2cpp.o cpp_parser.o lex.yy.o cpp_typecheck.o cpp_convert_type.o cpp_typecheck_expr.o cpp_typecheck_code.o cpp_typecheck_type.o parse.o cpp_parse_tree.o cpp_token_buffer.o cpp_typecheck_fargs.o cpp_typecheck_resolve.o cpp_util.o cpp_typecheck_function.o cpp_typecheck_namespace.o cpp_name.o cpp_is_pod.o cpp_scope.o cpp_typecheck_find_constructor.o template_map.o cpp_scopes.o cpp_declarator.o cpp_instantiate_template.o internal_additions.o cpp_type2name.o cpp_typecheck_linkage_spec.o cpp_typecheck_template.o cpp_typecheck_function_bodies.o cpp_typecheck_initializer.o cpp_typecheck_compound_type.o cpp_constructor.o cpp_destructor.o cpp_final.o cpp_typecheck_conversions.o cpp_typecheck_declaration.o cpp_declarator_converter.o cpp_declaration.o cpp_namespace_spec.o cpp_typecheck_using.o cpp_typecheck_enum_type.o cpp_typecheck_bases.o cpp_typecheck_constructor.o cpp_typecheck_virtual_table.o cpp.a lex.yy.cpp y.tab.cpp.output make[3]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0/src/goto-instrument' make[3]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0/src/langapi' if [ -e xmllang/. ] ; then \ make -C xmllang clean ; \ fi make[3]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0/src/goto-cc' make[3]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0/src/goto-programs' rm -f goto_convert.o goto_function.o goto_main.o goto_sideeffects.o goto_program.o basic_blocks.o goto_threads.o goto_check.o goto_function_pointers.o goto_functions.o goto_inline.o remove_skip.o goto_convert_functions.o string_instrumentation.o builtin_functions.o show_claims.o destructor.o set_claims.o slicer.o invariant_set.o invariant_propagation.o add_race_assertions.o rw_set.o read_goto_binary.o invariant_set_domain.o static_analysis.o string_abstraction.o goto_program_serialization.o goto_function_serialization.o read_bin_goto_object.o goto_program_irep.o interpreter.o interpreter_evaluate.o flow_insensitive_analysis.o format_strings.o loop_numbers.o pointer_arithmetic.o goto_program_template.o write_goto_binary.o remove_unreachable.o remove_unused_functions.o dynamic_memory.o dump_c.o wp.o goto_rw.o goto_clean_expr.o safety_checker.o compute_called_functions.o link_to_library.o goto-programs.a test_wp make[3]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0/src/goto-symex' make[3]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0/src/pointer-analysis' rm -f y.tab.h y.tab.cpp lex.yy.cpp y.tab.cpp.output y.output make[3]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0/src/cpp' make[3]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0/src/goto-programs' rm -f library/converter cprover_library.inc make[3]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0/src/ansi-c' make[3]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0/src/xmllang' rm -f xml_language.o xml_parser.o y.tab.o lex.yy.o xml_typecheck.o xml_parse_tree.o \ y.tab.h y.tab.cpp lex.yy.cpp y.tab.cpp.output y.output \ xmllang.a make[3]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0/src/xmllang' make[3]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0/src/solvers' rm -f sat/satcheck_minisat2.o sat/cnf.o sat/dimacs_cnf.o sat/cnf_clause_list.o sat/pbs_dimacs_cnf.o sat/read_dimacs_cnf.o sat/resolution_proof.o sat/satcheck.o qbf/qdimacs_cnf.o qbf/qbf_quantor.o qbf/qbf_skizzo.o qbf/qdimacs_core.o qbf/qbf_qube.o qbf/qbf_qube_core.o prop/prop.o prop/prop_conv.o prop/prop_conv_store.o prop/aig_formula.o prop/aig.o prop/aig_prop.o cvc/cvc_prop.o cvc/cvc_conv.o cvc/cvc_dec.o smt1/smt1_dec.o smt1/smt1_prop.o smt1/smt1_conv.o smt2/smt2_dec.o smt2/smt2_prop.o smt2/smt2_conv.o dplib/dplib_conv.o dplib/dplib_dec.o dplib/dplib_prop.o flattening/equality.o flattening/arrays.o flattening/functions.o flattening/sat_minimizer.o flattening/boolbv_width.o flattening/boolbv.o flattening/boolbv_constraint_select_one.o flattening/bv_pointers.o flattening/bv_utils.o flattening/boolbv_abs.o flattening/boolbv_with.o flattening/boolbv_typecast.o flattening/boolbv_index.o flattening/boolbv_member.o flattening/boolbv_if.o flattening/boolbv_byte_extract.o flattening/boolbv_add_sub.o flattening/boolbv_mult.o flattening/boolbv_constant.o flattening/boolbv_extractbit.o flattening/boolbv_bv_rel.o flattening/boolbv_shift.o flattening/boolbv_case.o flattening/boolbv_cond.o flattening/boolbv_concatenation.o flattening/boolbv_div.o flattening/boolbv_mod.o flattening/boolbv_extractbits.o flattening/boolbv_replication.o flattening/boolbv_reduction.o flattening/boolbv_overflow.o flattening/boolbv_get.o flattening/boolbv_bitwise.o flattening/boolbv_equality.o flattening/boolbv_unary_minus.o flattening/boolbv_ieee_float_rel.o flattening/pointer_logic.o flattening/boolbv_quantifier.o flattening/boolbv_struct.o flattening/boolbv_byte_update.o flattening/boolbv_array_of.o flattening/boolbv_map.o flattening/boolbv_type.o flattening/boolbv_union.o solvers.a make[3]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0/src/util' rm -f arith_tools.o base_type.o cmdline.o config.o context.o expr.o expr_util.o i2string.o irep.o language.o lispexpr.o lispirep.o location.o message.o language_file.o mp_arith.o namespace.o parseoptions.o rename.o replace_expr.o threeval.o typecheck.o graph.o type.o cnf_simplify.o str_getline.o strstream2string.o bitvector.o parser.o map_util.o replace_symbol.o actuals.o get_module.o string_hash.o string_container.o identifier.o rational.o options.o c_misc.o simplify_expr.o dstring.o find_symbols.o rational_tools.o ui_message.o simplify_utils.o time_stopping.o symbol.o irep_hash_container.o type_eq.o guard.o array_name.o gcd.o message_stream.o substitute.o decision_procedure.o union_find.o pretty_names.o xml.o xml_irep.o std_types.o std_code.o format_constant.o find_macros.o ref_expr_set.o std_expr.o irep_serialization.o symbol_serialization.o fixedbv.o ieee_float.o signal_catcher.o pointer_offset_size.o bv_arithmetic.o tempdir.o tempfile.o timer.o irep_ids.o util.a make[3]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0/src/solvers' rm -f irep_ids.h irep_ids.inc rm -f ieee_float_test ieee_float_test.o rm -f irep_ids_convert irep_ids_convert.o make[3]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0/src/util' rm -f *.o make[2]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0/src' make[1]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0' dh_clean -O--parallel dpkg-source -b cbmc-4.0 dpkg-source: info: using source format `3.0 (quilt)' dpkg-source: info: building cbmc using existing ./cbmc_4.0.orig.tar.gz dpkg-source: info: building cbmc in cbmc_4.0-4.debian.tar.gz dpkg-source: info: building cbmc in cbmc_4.0-4.dsc debian/rules build dh --parallel build dh_testdir -O--parallel dh_auto_configure -O--parallel dh_auto_build -O--parallel make[1]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0' make -C src make[2]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0/src' ## Entering big-int make -C big-int make[3]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0/src/big-int' g++ -Wall -MMD -O2 -g -c -o bigint-test.o bigint-test.cc g++ -Wall -MMD -O2 -g -c -o bigint-func.o bigint-func.cc g++ -Wall -MMD -O2 -g -c -o bigint.o bigint.cc g++ -Wall -MMD -O2 -g -o test-bigint bigint-test.o bigint-func.o bigint.o make[3]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0/src/big-int' ## Entering util make -C util make[3]: Entering directory `/build/cbmc-jcBgCw/cbmc-4.0/src/util' g++ -c -Wall -MMD -O2 -g -I .. -I . -o irep_ids_convert.o irep_ids_convert.cpp g++ -o irep_ids_convert irep_ids_convert.o ./irep_ids_convert header < irep_ids.txt > irep_ids.h g++ -c -Wall -MMD -O2 -g -I .. -I . -o arith_tools.o arith_tools.cpp g++ -c -Wall -MMD -O2 -g -I .. -I . -o base_type.o base_type.cpp In file included from base_type.cpp:13: In file included from ./base_type.h:13: In file included from ./namespace.h:12: In file included from ./context.h:18: ./symbol.h:48:25: warning: 'thread_local' is a keyword in C++11 [-Wc++11-compat] bool static_lifetime, thread_local; ^ In file included from base_type.cpp:13: In file included from ./base_type.h:14: In file included from ./union_find.h:16: ./numbering.h:32:7: error: use of undeclared identifier 'push_back' push_back(a); ^ this-> ./union_find.h:142:22: note: in instantiation of member function 'numbering::number' requested here unsigned n=subt::number(a); ^ ./union_find.h:109:17: note: in instantiation of member function 'union_find::number' requested here unsigned na=number(a), nb=number(b); ^ base_type.cpp:173:20: note: in instantiation of member function 'union_find::make_union' requested here if(identifiers.make_union( ^ /usr/include/c++/4.6/bits/stl_vector.h:826:7: note: must qualify identifier to find this declaration in dependent base class push_back(const value_type& __x) ^ 1 warning and 1 error generated. make[3]: *** [base_type.o] Error 1 make[3]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0/src/util' make[2]: *** [util.dir] Error 2 make[2]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0/src' make[1]: *** [all] Error 2 make[1]: Leaving directory `/build/cbmc-jcBgCw/cbmc-4.0' dh_auto_build: make -j10 returned exit code 2 make: *** [build] Error 2 dpkg-buildpackage: error: debian/rules build gave error exit status 2 ──────────────────────────────────────────────────────────────────────────────── Build finished at 20120113-0019 Finished ──────── E: Build failure (dpkg-buildpackage died) ┌──────────────────────────────────────────────────────────────────────────────┐ │ Cleanup │ └──────────────────────────────────────────────────────────────────────────────┘ Purging /var/lib/schroot/mount/lsid64b-eb409885-d07c-40c5-ba15-008d842e65a0/build/cbmc-jcBgCw Not cleaning session: cloned chroot in use ┌──────────────────────────────────────────────────────────────────────────────┐ │ Summary │ └──────────────────────────────────────────────────────────────────────────────┘ Architecture: amd64 Build-Space: 7452 Build-Time: 4 Distribution: lsid64b Fail-Stage: build Install-Time: 6 Job: cbmc_4.0-4 Package: cbmc Package-Time: 23 Source-Version: 4.0-4 Space: 7452 Status: attempted Version: 4.0-4 ──────────────────────────────────────────────────────────────────────────────── Finished at 20120113-0019 Build needed 00:00:23, 7452k disc space DC-Build-Status: Failed 891.469769s ### Content of /var/log/daemon.log ### Jan 12 21:03:53 stremi-5 approx: Concurrent download of debian/dists/sid/Release.gpg is taking too long Jan 12 21:04:14 stremi-5 approx: Concurrent download of debian/dists/sid/main/i18n/Translation-en.bz2 is taking too long Jan 12 21:04:20 stremi-5 approx: Concurrent download of debian/dists/sid/Release is taking too long Jan 12 21:04:30 stremi-5 approx: Concurrent download of debian/dists/sid/Release.gpg is taking too long Jan 12 21:04:41 stremi-5 approx: Concurrent download of debian/dists/sid/Release.gpg is taking too long Jan 12 21:04:52 stremi-5 approx: Concurrent download of debian/dists/sid/Release.gpg is taking too long Jan 12 21:04:54 stremi-5 approx: Concurrent download of debian/dists/sid/main/source/Sources.xz is taking too long Jan 12 21:05:10 stremi-5 approx: Concurrent download of debian/dists/sid/Release.gpg is taking too long Jan 12 21:05:34 stremi-5 approx: Concurrent download of debian/dists/sid/main/binary-amd64/Packages.xz is taking too long Jan 12 21:05:43 stremi-5 approx: Concurrent download of debian/dists/sid/Release is taking too long Jan 12 21:06:08 stremi-5 approx: Concurrent download of debian/dists/sid/main/binary-amd64/Packages.xz is taking too long ### End of content of /var/log/daemon.log ### DC-Time-Estimation: 891.469769 versus expected 134 (r/m: 5.65275947014925 ; m: 134.0) DC-Build-Network: USED. See /tmp/rulesafter.EXS2gj ! ************************************************************ # Generated by iptables-save v1.4.8 on Fri Jan 13 00:19:15 2012 *filter :INPUT ACCEPT [2669723:18313495550] :FORWARD ACCEPT [0:0] :OUTPUT DROP [0:0] :LD - [0:0] [1229851:15319480295] -A OUTPUT -o lo -j ACCEPT [0:0] -A OUTPUT -d 129.88.0.0/16 -j ACCEPT [0:0] -A OUTPUT -d 10.0.0.0/8 -j ACCEPT [0:0] -A OUTPUT -d 192.168.133.0/24 -j ACCEPT [0:0] -A OUTPUT -d 192.168.159.0/24 -j ACCEPT [0:0] -A OUTPUT -d 192.168.160.0/24 -j ACCEPT [0:0] -A OUTPUT -d 10.69.0.0/17 -j ACCEPT [0:0] -A OUTPUT -d 172.28.52.0/22 -j ACCEPT [0:0] -A OUTPUT -d 172.24.0.0/16 -j ACCEPT [0:0] -A OUTPUT -d 131.254.202.0/23 -j ACCEPT [0:0] -A OUTPUT -d 138.96.20.0/22 -j ACCEPT [0:0] -A OUTPUT -d 192.168.22.0/24 -j ACCEPT [280270:130376730] -A OUTPUT -d 172.16.0.0/16 -j ACCEPT [0:0] -A OUTPUT -d 192.168.67.0/24 -j ACCEPT [23900:3188848] -A OUTPUT -d 224.0.0.0/4 -p udp -j ACCEPT [148:8880] -A OUTPUT -j LD [148:8880] -A LD -j LOG [148:8880] -A LD -j REJECT --reject-with icmp-port-unreachable COMMIT # Completed on Fri Jan 13 00:19:15 2012 ************************************************************ --- /tmp/rulesbefore.yuS0E5 2012-01-13 00:04:23.853938528 +0100 +++ /tmp/rulesafter.EXS2gj 2012-01-13 00:19:15.329766135 +0100 @@ -1,10 +1,10 @@ -# Generated by iptables-save v1.4.8 on Fri Jan 13 00:04:23 2012 +# Generated by iptables-save v1.4.8 on Fri Jan 13 00:19:15 2012 *filter -:INPUT ACCEPT [2404118:16028169208] +:INPUT ACCEPT [2669723:18313495550] :FORWARD ACCEPT [0:0] :OUTPUT DROP [0:0] :LD - [0:0] -[1075744:13283607019] -A OUTPUT -o lo -j ACCEPT +[1229851:15319480295] -A OUTPUT -o lo -j ACCEPT [0:0] -A OUTPUT -d 129.88.0.0/16 -j ACCEPT [0:0] -A OUTPUT -d 10.0.0.0/8 -j ACCEPT [0:0] -A OUTPUT -d 192.168.133.0/24 -j ACCEPT @@ -16,11 +16,11 @@ [0:0] -A OUTPUT -d 131.254.202.0/23 -j ACCEPT [0:0] -A OUTPUT -d 138.96.20.0/22 -j ACCEPT [0:0] -A OUTPUT -d 192.168.22.0/24 -j ACCEPT -[259972:111167717] -A OUTPUT -d 172.16.0.0/16 -j ACCEPT +[280270:130376730] -A OUTPUT -d 172.16.0.0/16 -j ACCEPT [0:0] -A OUTPUT -d 192.168.67.0/24 -j ACCEPT -[22115:2954240] -A OUTPUT -d 224.0.0.0/4 -p udp -j ACCEPT -[146:8760] -A OUTPUT -j LD -[146:8760] -A LD -j LOG -[146:8760] -A LD -j REJECT --reject-with icmp-port-unreachable +[23900:3188848] -A OUTPUT -d 224.0.0.0/4 -p udp -j ACCEPT +[148:8880] -A OUTPUT -j LD +[148:8880] -A LD -j LOG +[148:8880] -A LD -j REJECT --reject-with icmp-port-unreachable COMMIT -# Completed on Fri Jan 13 00:04:23 2012 +# Completed on Fri Jan 13 00:19:15 2012 ************************************************************ [10252.789322] IN= OUT=eth0 SRC=172.16.160.5 DST=193.166.3.2 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=16751 DF PROTO=TCP SPT=52102 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10255.808032] IN= OUT=eth0 SRC=172.16.160.5 DST=193.166.3.2 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=16752 DF PROTO=TCP SPT=52102 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10255.828543] IN= OUT=eth0 SRC=172.16.160.5 DST=193.166.3.2 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=1031 DF PROTO=TCP SPT=52103 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10258.848031] IN= OUT=eth0 SRC=172.16.160.5 DST=193.166.3.2 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=1032 DF PROTO=TCP SPT=52103 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10258.892443] IN= OUT=eth0 SRC=172.16.160.5 DST=195.220.53.232 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=48414 DF PROTO=TCP SPT=40034 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10261.908046] IN= OUT=eth0 SRC=172.16.160.5 DST=195.220.53.232 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=48415 DF PROTO=TCP SPT=40034 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10261.929880] IN= OUT=eth0 SRC=172.16.160.5 DST=195.220.53.232 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=44487 DF PROTO=TCP SPT=40035 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10264.945701] IN= OUT=eth0 SRC=172.16.160.5 DST=195.220.53.232 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=44488 DF PROTO=TCP SPT=40035 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10265.017145] IN= OUT=eth0 SRC=172.16.160.5 DST=212.117.177.118 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=58589 DF PROTO=TCP SPT=50287 DPT=80 WINDOW=5840 RES=0x00 SYN URGP=0 [10268.036028] IN= OUT=eth0 SRC=172.16.160.5 DST=212.117.177.118 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=58590 DF PROTO=TCP SPT=50287 DPT=80 WINDOW=5840 RES=0x00 SYN URGP=0 [10268.056983] IN= OUT=eth0 SRC=172.16.160.5 DST=212.117.177.118 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=29059 DF PROTO=TCP SPT=50288 DPT=80 WINDOW=5840 RES=0x00 SYN URGP=0 [10271.072025] IN= OUT=eth0 SRC=172.16.160.5 DST=212.117.177.118 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=29060 DF PROTO=TCP SPT=50288 DPT=80 WINDOW=5840 RES=0x00 SYN URGP=0 [10271.092284] IN= OUT=eth0 SRC=172.16.160.5 DST=212.117.177.118 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=40158 DF PROTO=TCP SPT=50291 DPT=80 WINDOW=5840 RES=0x00 SYN URGP=0 [10274.108028] IN= OUT=eth0 SRC=172.16.160.5 DST=212.117.177.118 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=40159 DF PROTO=TCP SPT=50291 DPT=80 WINDOW=5840 RES=0x00 SYN URGP=0 [10274.142270] IN= OUT=eth0 SRC=172.16.160.5 DST=188.40.67.148 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=45644 DF PROTO=TCP SPT=36598 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10277.160029] IN= OUT=eth0 SRC=172.16.160.5 DST=188.40.67.148 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=45645 DF PROTO=TCP SPT=36598 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10277.181050] IN= OUT=eth0 SRC=172.16.160.5 DST=188.40.67.148 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=39793 DF PROTO=TCP SPT=36600 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10280.196029] IN= OUT=eth0 SRC=172.16.160.5 DST=188.40.67.148 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=39794 DF PROTO=TCP SPT=36600 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10280.229365] IN= OUT=eth0 SRC=172.16.160.5 DST=46.43.35.231 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=56838 DF PROTO=TCP SPT=52142 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10283.248025] IN= OUT=eth0 SRC=172.16.160.5 DST=46.43.35.231 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=56839 DF PROTO=TCP SPT=52142 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10283.268854] IN= OUT=eth0 SRC=172.16.160.5 DST=46.43.35.231 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=34209 DF PROTO=TCP SPT=52144 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10286.284111] IN= OUT=eth0 SRC=172.16.160.5 DST=46.43.35.231 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=34210 DF PROTO=TCP SPT=52144 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10286.317203] IN= OUT=eth0 SRC=172.16.160.5 DST=193.166.3.2 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=49998 DF PROTO=TCP SPT=52121 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10289.336026] IN= OUT=eth0 SRC=172.16.160.5 DST=193.166.3.2 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=49999 DF PROTO=TCP SPT=52121 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10289.356789] IN= OUT=eth0 SRC=172.16.160.5 DST=193.166.3.2 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=27194 DF PROTO=TCP SPT=52122 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10292.376188] IN= OUT=eth0 SRC=172.16.160.5 DST=193.166.3.2 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=27195 DF PROTO=TCP SPT=52122 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10292.418471] IN= OUT=eth0 SRC=172.16.160.5 DST=195.220.53.232 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=48347 DF PROTO=TCP SPT=40052 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10295.436109] IN= OUT=eth0 SRC=172.16.160.5 DST=195.220.53.232 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=48348 DF PROTO=TCP SPT=40052 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10295.457006] IN= OUT=eth0 SRC=172.16.160.5 DST=195.220.53.232 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=25159 DF PROTO=TCP SPT=40053 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10298.473053] IN= OUT=eth0 SRC=172.16.160.5 DST=195.220.53.232 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=25160 DF PROTO=TCP SPT=40053 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10298.508168] IN= OUT=eth0 SRC=172.16.160.5 DST=212.117.177.118 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=62768 DF PROTO=TCP SPT=50317 DPT=80 WINDOW=5840 RES=0x00 SYN URGP=0 [10301.524110] IN= OUT=eth0 SRC=172.16.160.5 DST=212.117.177.118 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=62769 DF PROTO=TCP SPT=50317 DPT=80 WINDOW=5840 RES=0x00 SYN URGP=0 [10301.545145] IN= OUT=eth0 SRC=172.16.160.5 DST=212.117.177.118 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=26288 DF PROTO=TCP SPT=50321 DPT=80 WINDOW=5840 RES=0x00 SYN URGP=0 [10304.564363] IN= OUT=eth0 SRC=172.16.160.5 DST=212.117.177.118 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=26289 DF PROTO=TCP SPT=50321 DPT=80 WINDOW=5840 RES=0x00 SYN URGP=0 [10304.584883] IN= OUT=eth0 SRC=172.16.160.5 DST=212.117.177.118 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=31364 DF PROTO=TCP SPT=50322 DPT=80 WINDOW=5840 RES=0x00 SYN URGP=0 [10307.600030] IN= OUT=eth0 SRC=172.16.160.5 DST=212.117.177.118 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=31365 DF PROTO=TCP SPT=50322 DPT=80 WINDOW=5840 RES=0x00 SYN URGP=0 [10307.634367] IN= OUT=eth0 SRC=172.16.160.5 DST=188.40.67.148 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=61768 DF PROTO=TCP SPT=36629 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10310.648038] IN= OUT=eth0 SRC=172.16.160.5 DST=188.40.67.148 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=61769 DF PROTO=TCP SPT=36629 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10310.669191] IN= OUT=eth0 SRC=172.16.160.5 DST=188.40.67.148 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=19477 DF PROTO=TCP SPT=36630 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10313.684027] IN= OUT=eth0 SRC=172.16.160.5 DST=188.40.67.148 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=19478 DF PROTO=TCP SPT=36630 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10313.718533] IN= OUT=eth0 SRC=172.16.160.5 DST=46.43.35.231 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=477 DF PROTO=TCP SPT=52172 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10316.736028] IN= OUT=eth0 SRC=172.16.160.5 DST=46.43.35.231 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=478 DF PROTO=TCP SPT=52172 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10321.782852] IN= OUT=eth0 SRC=172.16.160.5 DST=46.43.35.231 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=65022 DF PROTO=TCP SPT=52183 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10324.800033] IN= OUT=eth0 SRC=172.16.160.5 DST=46.43.35.231 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=65023 DF PROTO=TCP SPT=52183 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10324.832128] IN= OUT=eth0 SRC=172.16.160.5 DST=193.166.3.2 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=2857 DF PROTO=TCP SPT=52160 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10327.856028] IN= OUT=eth0 SRC=172.16.160.5 DST=193.166.3.2 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=2858 DF PROTO=TCP SPT=52160 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10327.876559] IN= OUT=eth0 SRC=172.16.160.5 DST=193.166.3.2 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=23071 DF PROTO=TCP SPT=52161 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [10330.888027] IN= OUT=eth0 SRC=172.16.160.5 DST=193.166.3.2 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=23072 DF PROTO=TCP SPT=52161 DPT=21 WINDOW=5840 RES=0x00 SYN URGP=0 [11729.108943] IN= OUT=eth0 SRC=172.16.160.5 DST=192.9.162.55 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=3229 DF PROTO=TCP SPT=35585 DPT=80 WINDOW=5840 RES=0x00 SYN URGP=0 [11738.715137] IN= OUT=eth0 SRC=172.16.160.5 DST=192.9.162.55 LEN=60 TOS=0x00 PREC=0x00 TTL=64 ID=42174 DF PROTO=TCP SPT=48829 DPT=80 WINDOW=5840 RES=0x00 SYN URGP=0 ************************************************************