RUN: /bin/echo ['echo', 'Forking build subprocess...'] Forking build subprocess... RUN: /usr/share/launchpad-buildd/slavebin/unpack-chroot ['unpack-chroot', '46bb7d668cc12656460de3cceab2f15fa1ccc233', '/home/buildd/filecache-default/09280e31193d9ed26f1efd407c11b3c1a910dcf0'] Synching the system clock with the buildd NTP service... 2 Nov 12:58:43 ntpdate[25954]: adjust time server 10.122.37.1 offset 0.000012 sec Unpacking chroot for build 46bb7d668cc12656460de3cceab2f15fa1ccc233 RUN: /usr/share/launchpad-buildd/slavebin/mount-chroot ['mount-chroot', '46bb7d668cc12656460de3cceab2f15fa1ccc233'] Mounting chroot for build 46bb7d668cc12656460de3cceab2f15fa1ccc233 RUN: /usr/share/launchpad-buildd/slavebin/override-sources-list ['override-sources-list', '46bb7d668cc12656460de3cceab2f15fa1ccc233', 'deb http://ftpmaster.internal/ubuntu precise main universe'] Overriding sources.list in build-46bb7d668cc12656460de3cceab2f15fa1ccc233 RUN: /usr/share/launchpad-buildd/slavebin/update-debian-chroot ['update-debian-chroot', '46bb7d668cc12656460de3cceab2f15fa1ccc233', 'amd64'] Updating debian chroot for build 46bb7d668cc12656460de3cceab2f15fa1ccc233 Ign http://ftpmaster.internal precise InRelease Get:1 http://ftpmaster.internal precise Release.gpg [198 B] Get:2 http://ftpmaster.internal precise Release [49.6 kB] Get:3 http://ftpmaster.internal precise/main amd64 Packages [1246 kB] Get:4 http://ftpmaster.internal precise/universe amd64 Packages [4601 kB] Get:5 http://ftpmaster.internal precise/main i386 Packages [1247 kB] Get:6 http://ftpmaster.internal precise/universe i386 Packages [4611 kB] Get:7 http://ftpmaster.internal precise/main TranslationIndex [74 B] Get:8 http://ftpmaster.internal precise/universe TranslationIndex [75 B] Get:9 http://ftpmaster.internal precise/main Translation-en [713 kB] Get:10 http://ftpmaster.internal precise/universe Translation-en [3259 kB] Fetched 15.7 MB in 12s (1303 kB/s) Reading package lists... Reading package lists... Building dependency tree... Reading state information... The following NEW packages will be installed: liblzma5 The following packages will be upgraded: base-files binutils busybox-initramfs cpp-4.6 dash diffutils dpkg dpkg-dev e2fslibs e2fsprogs g++-4.6 gcc-4.6 gcc-4.6-base initramfs-tools initramfs-tools-bin libcomerr2 libcurl3-gnutls libdpkg-perl libgcc1 libglib2.0-0 libgomp1 libgssapi-krb5-2 libk5crypto3 libkrb5-3 libkrb5support0 libnih-dbus1 libnih1 libp11-kit0 libpam-modules libpam-modules-bin libpam-runtime libpam0g libquadmath0 libss2 libstdc++6 libstdc++6-4.6-dev linux-libc-dev pkgbinarymangler procps tzdata upstart xz-utils 42 upgraded, 1 newly installed, 0 to remove and 0 not upgraded. Need to get 33.0 MB of archives. After this operation, 4086 kB disk space will be freed. WARNING: The following packages cannot be authenticated! base-files dpkg dash diffutils e2fslibs e2fsprogs libgomp1 gcc-4.6-base libstdc++6 cpp-4.6 libquadmath0 libstdc++6-4.6-dev g++-4.6 gcc-4.6 libgcc1 binutils libcomerr2 liblzma5 libpam0g libpam-modules-bin libpam-modules libss2 libglib2.0-0 libnih-dbus1 libnih1 libk5crypto3 libgssapi-krb5-2 libkrb5-3 libkrb5support0 libcurl3-gnutls libp11-kit0 libpam-runtime tzdata xz-utils busybox-initramfs initramfs-tools initramfs-tools-bin upstart procps dpkg-dev libdpkg-perl linux-libc-dev pkgbinarymangler Authentication warning overridden. Get:1 http://ftpmaster.internal/ubuntu/ precise/main base-files amd64 6.5ubuntu2 [56.2 kB] Get:2 http://ftpmaster.internal/ubuntu/ precise/main dpkg amd64 1.16.1.1ubuntu2 [1835 kB] Get:3 http://ftpmaster.internal/ubuntu/ precise/main dash amd64 0.5.7-2ubuntu1 [89.1 kB] Get:4 http://ftpmaster.internal/ubuntu/ precise/main diffutils amd64 1:3.2-1 [212 kB] Get:5 http://ftpmaster.internal/ubuntu/ precise/main e2fslibs amd64 1.42~WIP-2011-10-16-1ubuntu1 [187 kB] Get:6 http://ftpmaster.internal/ubuntu/ precise/main e2fsprogs amd64 1.42~WIP-2011-10-16-1ubuntu1 [952 kB] Get:7 http://ftpmaster.internal/ubuntu/ precise/main libgomp1 amd64 4.6.2-2ubuntu1 [25.4 kB] Get:8 http://ftpmaster.internal/ubuntu/ precise/main gcc-4.6-base amd64 4.6.2-2ubuntu1 [15.8 kB] Get:9 http://ftpmaster.internal/ubuntu/ precise/main libstdc++6 amd64 4.6.2-2ubuntu1 [320 kB] Get:10 http://ftpmaster.internal/ubuntu/ precise/main cpp-4.6 amd64 4.6.2-2ubuntu1 [4825 kB] Get:11 http://ftpmaster.internal/ubuntu/ precise/main libquadmath0 amd64 4.6.2-2ubuntu1 [126 kB] Get:12 http://ftpmaster.internal/ubuntu/ precise/main libstdc++6-4.6-dev amd64 4.6.2-2ubuntu1 [1609 kB] Get:13 http://ftpmaster.internal/ubuntu/ precise/main g++-4.6 amd64 4.6.2-2ubuntu1 [6972 kB] Get:14 http://ftpmaster.internal/ubuntu/ precise/main gcc-4.6 amd64 4.6.2-2ubuntu1 [7525 kB] Get:15 http://ftpmaster.internal/ubuntu/ precise/main libgcc1 amd64 1:4.6.2-2ubuntu1 [42.6 kB] Get:16 http://ftpmaster.internal/ubuntu/ precise/main binutils amd64 2.21.90.20111025-1ubuntu1 [2638 kB] Get:17 http://ftpmaster.internal/ubuntu/ precise/main libcomerr2 amd64 1.42~WIP-2011-10-16-1ubuntu1 [56.6 kB] Get:18 http://ftpmaster.internal/ubuntu/ precise/main liblzma5 amd64 5.1.1alpha+20110809-3 [88.7 kB] Get:19 http://ftpmaster.internal/ubuntu/ precise/main libpam0g amd64 1.1.3-5ubuntu2 [56.9 kB] Get:20 http://ftpmaster.internal/ubuntu/ precise/main libpam-modules-bin amd64 1.1.3-5ubuntu2 [42.0 kB] Get:21 http://ftpmaster.internal/ubuntu/ precise/main libpam-modules amd64 1.1.3-5ubuntu2 [275 kB] Get:22 http://ftpmaster.internal/ubuntu/ precise/main libss2 amd64 1.42~WIP-2011-10-16-1ubuntu1 [61.8 kB] Get:23 http://ftpmaster.internal/ubuntu/ precise/main libglib2.0-0 amd64 2.30.1-2ubuntu1 [1170 kB] Get:24 http://ftpmaster.internal/ubuntu/ precise/main libnih-dbus1 amd64 1.0.3-4ubuntu4 [15.8 kB] Get:25 http://ftpmaster.internal/ubuntu/ precise/main libnih1 amd64 1.0.3-4ubuntu4 [54.9 kB] Get:26 http://ftpmaster.internal/ubuntu/ precise/main libk5crypto3 amd64 1.9.1+dfsg-1ubuntu2.1 [84.0 kB] Get:27 http://ftpmaster.internal/ubuntu/ precise/main libgssapi-krb5-2 amd64 1.9.1+dfsg-1ubuntu2.1 [118 kB] Get:28 http://ftpmaster.internal/ubuntu/ precise/main libkrb5-3 amd64 1.9.1+dfsg-1ubuntu2.1 [350 kB] Get:29 http://ftpmaster.internal/ubuntu/ precise/main libkrb5support0 amd64 1.9.1+dfsg-1ubuntu2.1 [24.0 kB] Get:30 http://ftpmaster.internal/ubuntu/ precise/main libcurl3-gnutls amd64 7.21.7-3ubuntu1 [221 kB] Get:31 http://ftpmaster.internal/ubuntu/ precise/main libp11-kit0 amd64 0.7-2 [33.7 kB] Get:32 http://ftpmaster.internal/ubuntu/ precise/main libpam-runtime amd64 1.1.3-5ubuntu2 [45.2 kB] Get:33 http://ftpmaster.internal/ubuntu/ precise/main tzdata amd64 2011m-1 [467 kB] Get:34 http://ftpmaster.internal/ubuntu/ precise/main xz-utils amd64 5.1.1alpha+20110809-3 [87.6 kB] Get:35 http://ftpmaster.internal/ubuntu/ precise/main busybox-initramfs amd64 1:1.18.5-1ubuntu1 [185 kB] Get:36 http://ftpmaster.internal/ubuntu/ precise/main initramfs-tools all 0.99ubuntu8 [51.7 kB] Get:37 http://ftpmaster.internal/ubuntu/ precise/main initramfs-tools-bin amd64 0.99ubuntu8 [11.9 kB] Get:38 http://ftpmaster.internal/ubuntu/ precise/main upstart amd64 1.3-0ubuntu11 [288 kB] Get:39 http://ftpmaster.internal/ubuntu/ precise/main procps amd64 1:3.2.8-11ubuntu1 [235 kB] Get:40 http://ftpmaster.internal/ubuntu/ precise/main dpkg-dev all 1.16.1.1ubuntu2 [468 kB] Get:41 http://ftpmaster.internal/ubuntu/ precise/main libdpkg-perl all 1.16.1.1ubuntu2 [181 kB] Get:42 http://ftpmaster.internal/ubuntu/ precise/main linux-libc-dev amd64 3.1.0-2.3 [836 kB] Get:43 http://ftpmaster.internal/ubuntu/ precise/main pkgbinarymangler all 105 [27.1 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 33.0 MB in 1s (21.8 MB/s) (Reading database ... 14112 files and directories currently installed.) Preparing to replace base-files 6.4ubuntu6 (using .../base-files_6.5ubuntu2_amd64.deb) ... Unpacking replacement base-files ... Setting up base-files (6.5ubuntu2) ... (Reading database ... 14112 files and directories currently installed.) Preparing to replace dpkg 1.16.1ubuntu1 (using .../dpkg_1.16.1.1ubuntu2_amd64.deb) ... Unpacking replacement dpkg ... Setting up dpkg (1.16.1.1ubuntu2) ... (Reading database ... 14112 files and directories currently installed.) Preparing to replace dash 0.5.5.1-7.4ubuntu1 (using .../dash_0.5.7-2ubuntu1_amd64.deb) ... Unpacking replacement dash ... Setting up dash (0.5.7-2ubuntu1) ... (Reading database ... 14112 files and directories currently installed.) Preparing to replace diffutils 1:3.0-1 (using .../diffutils_1%3a3.2-1_amd64.deb) ... Unpacking replacement diffutils ... Setting up diffutils (1:3.2-1) ... (Reading database ... 14112 files and directories currently installed.) Preparing to replace e2fslibs 1.42~WIP-2011-10-09-1ubuntu1 (using .../e2fslibs_1.42~WIP-2011-10-16-1ubuntu1_amd64.deb) ... Unpacking replacement e2fslibs ... Setting up e2fslibs (1.42~WIP-2011-10-16-1ubuntu1) ... Processing triggers for libc-bin ... ldconfig deferred processing now taking place (Reading database ... 14112 files and directories currently installed.) Preparing to replace e2fsprogs 1.42~WIP-2011-10-09-1ubuntu1 (using .../e2fsprogs_1.42~WIP-2011-10-16-1ubuntu1_amd64.deb) ... Unpacking replacement e2fsprogs ... Setting up e2fsprogs (1.42~WIP-2011-10-16-1ubuntu1) ... (Reading database ... 14112 files and directories currently installed.) Preparing to replace libgomp1 4.6.1-15ubuntu1 (using .../libgomp1_4.6.2-2ubuntu1_amd64.deb) ... Unpacking replacement libgomp1 ... Preparing to replace gcc-4.6-base 4.6.1-15ubuntu1 (using .../gcc-4.6-base_4.6.2-2ubuntu1_amd64.deb) ... Unpacking replacement gcc-4.6-base ... Setting up gcc-4.6-base (4.6.2-2ubuntu1) ... (Reading database ... 14113 files and directories currently installed.) Preparing to replace libstdc++6 4.6.1-15ubuntu1 (using .../libstdc++6_4.6.2-2ubuntu1_amd64.deb) ... Unpacking replacement libstdc++6 ... Setting up libstdc++6 (4.6.2-2ubuntu1) ... Processing triggers for libc-bin ... ldconfig deferred processing now taking place (Reading database ... 14113 files and directories currently installed.) Preparing to replace cpp-4.6 4.6.1-15ubuntu1 (using .../cpp-4.6_4.6.2-2ubuntu1_amd64.deb) ... Unpacking replacement cpp-4.6 ... Preparing to replace libquadmath0 4.6.1-15ubuntu1 (using .../libquadmath0_4.6.2-2ubuntu1_amd64.deb) ... Unpacking replacement libquadmath0 ... Preparing to replace libstdc++6-4.6-dev 4.6.1-15ubuntu1 (using .../libstdc++6-4.6-dev_4.6.2-2ubuntu1_amd64.deb) ... Unpacking replacement libstdc++6-4.6-dev ... Preparing to replace g++-4.6 4.6.1-15ubuntu1 (using .../g++-4.6_4.6.2-2ubuntu1_amd64.deb) ... Unpacking replacement g++-4.6 ... Preparing to replace gcc-4.6 4.6.1-15ubuntu1 (using .../gcc-4.6_4.6.2-2ubuntu1_amd64.deb) ... Unpacking replacement gcc-4.6 ... Preparing to replace libgcc1 1:4.6.1-15ubuntu1 (using .../libgcc1_1%3a4.6.2-2ubuntu1_amd64.deb) ... Unpacking replacement libgcc1 ... Setting up libgcc1 (1:4.6.2-2ubuntu1) ... Processing triggers for libc-bin ... ldconfig deferred processing now taking place (Reading database ... 14113 files and directories currently installed.) Preparing to replace binutils 2.21.90.20111004-2ubuntu1 (using .../binutils_2.21.90.20111025-1ubuntu1_amd64.deb) ... Unpacking replacement binutils ... Preparing to replace libcomerr2 1.42~WIP-2011-10-09-1ubuntu1 (using .../libcomerr2_1.42~WIP-2011-10-16-1ubuntu1_amd64.deb) ... Unpacking replacement libcomerr2 ... Setting up libcomerr2 (1.42~WIP-2011-10-16-1ubuntu1) ... Processing triggers for libc-bin ... ldconfig deferred processing now taking place Selecting previously unselected package liblzma5. (Reading database ... 14113 files and directories currently installed.) Unpacking liblzma5 (from .../liblzma5_5.1.1alpha+20110809-3_amd64.deb) ... Setting up liblzma5 (5.1.1alpha+20110809-3) ... Processing triggers for libc-bin ... ldconfig deferred processing now taking place (Reading database ... 14121 files and directories currently installed.) Preparing to replace libpam0g 1.1.3-2ubuntu1 (using .../libpam0g_1.1.3-5ubuntu2_amd64.deb) ... Unpacking replacement libpam0g ... Setting up libpam0g (1.1.3-5ubuntu2) ... Processing triggers for libc-bin ... ldconfig deferred processing now taking place (Reading database ... 14121 files and directories currently installed.) Preparing to replace libpam-modules-bin 1.1.3-2ubuntu1 (using .../libpam-modules-bin_1.1.3-5ubuntu2_amd64.deb) ... Unpacking replacement libpam-modules-bin ... Setting up libpam-modules-bin (1.1.3-5ubuntu2) ... (Reading database ... 14121 files and directories currently installed.) Preparing to replace libpam-modules 1.1.3-2ubuntu1 (using .../libpam-modules_1.1.3-5ubuntu2_amd64.deb) ... Unpacking replacement libpam-modules ... Setting up libpam-modules (1.1.3-5ubuntu2) ... (Reading database ... 14121 files and directories currently installed.) Preparing to replace libss2 1.42~WIP-2011-10-09-1ubuntu1 (using .../libss2_1.42~WIP-2011-10-16-1ubuntu1_amd64.deb) ... Unpacking replacement libss2 ... Setting up libss2 (1.42~WIP-2011-10-16-1ubuntu1) ... Processing triggers for libc-bin ... ldconfig deferred processing now taking place (Reading database ... 14121 files and directories currently installed.) Preparing to replace libglib2.0-0 2.30.0-0ubuntu4 (using .../libglib2.0-0_2.30.1-2ubuntu1_amd64.deb) ... Unpacking replacement libglib2.0-0 ... Preparing to replace libnih-dbus1 1.0.3-4ubuntu3 (using .../libnih-dbus1_1.0.3-4ubuntu4_amd64.deb) ... Unpacking replacement libnih-dbus1 ... Preparing to replace libnih1 1.0.3-4ubuntu3 (using .../libnih1_1.0.3-4ubuntu4_amd64.deb) ... Unpacking replacement libnih1 ... Preparing to replace libk5crypto3 1.9.1+dfsg-1ubuntu1 (using .../libk5crypto3_1.9.1+dfsg-1ubuntu2.1_amd64.deb) ... Unpacking replacement libk5crypto3 ... Preparing to replace libgssapi-krb5-2 1.9.1+dfsg-1ubuntu1 (using .../libgssapi-krb5-2_1.9.1+dfsg-1ubuntu2.1_amd64.deb) ... Unpacking replacement libgssapi-krb5-2 ... Preparing to replace libkrb5-3 1.9.1+dfsg-1ubuntu1 (using .../libkrb5-3_1.9.1+dfsg-1ubuntu2.1_amd64.deb) ... Unpacking replacement libkrb5-3 ... Preparing to replace libkrb5support0 1.9.1+dfsg-1ubuntu1 (using .../libkrb5support0_1.9.1+dfsg-1ubuntu2.1_amd64.deb) ... Unpacking replacement libkrb5support0 ... Preparing to replace libcurl3-gnutls 7.21.6-3ubuntu3 (using .../libcurl3-gnutls_7.21.7-3ubuntu1_amd64.deb) ... Unpacking replacement libcurl3-gnutls ... Preparing to replace libp11-kit0 0.6-0ubuntu2 (using .../libp11-kit0_0.7-2_amd64.deb) ... Unpacking replacement libp11-kit0 ... Preparing to replace libpam-runtime 1.1.3-2ubuntu1 (using .../libpam-runtime_1.1.3-5ubuntu2_amd64.deb) ... Unpacking replacement libpam-runtime ... Setting up libpam-runtime (1.1.3-5ubuntu2) ... (Reading database ... 14123 files and directories currently installed.) Preparing to replace tzdata 2011l-2 (using .../tzdata_2011m-1_amd64.deb) ... Unpacking replacement tzdata ... Setting up tzdata (2011m-1) ... Current default time zone: 'Etc/UTC' Local time is now: Wed Nov 2 13:00:08 UTC 2011. Universal Time is now: Wed Nov 2 13:00:08 UTC 2011. Run 'dpkg-reconfigure tzdata' if you wish to change it. (Reading database ... 14123 files and directories currently installed.) Preparing to replace xz-utils 5.1.1alpha+20110809-2 (using .../xz-utils_5.1.1alpha+20110809-3_amd64.deb) ... Unpacking replacement xz-utils ... Setting up xz-utils (5.1.1alpha+20110809-3) ... (Reading database ... 14123 files and directories currently installed.) Preparing to replace busybox-initramfs 1:1.18.4-2ubuntu2 (using .../busybox-initramfs_1%3a1.18.5-1ubuntu1_amd64.deb) ... Unpacking replacement busybox-initramfs ... Preparing to replace initramfs-tools 0.99ubuntu7 (using .../initramfs-tools_0.99ubuntu8_all.deb) ... Unpacking replacement initramfs-tools ... Preparing to replace initramfs-tools-bin 0.99ubuntu7 (using .../initramfs-tools-bin_0.99ubuntu8_amd64.deb) ... Unpacking replacement initramfs-tools-bin ... Preparing to replace upstart 1.3-0ubuntu10 (using .../upstart_1.3-0ubuntu11_amd64.deb) ... Unpacking replacement upstart ... Preparing to replace procps 1:3.2.8-10ubuntu5 (using .../procps_1%3a3.2.8-11ubuntu1_amd64.deb) ... invoke-rc.d: policy-rc.d denied execution of stop. Unpacking replacement procps ... Preparing to replace dpkg-dev 1.16.1ubuntu1 (using .../dpkg-dev_1.16.1.1ubuntu2_all.deb) ... Unpacking replacement dpkg-dev ... Preparing to replace libdpkg-perl 1.16.1ubuntu1 (using .../libdpkg-perl_1.16.1.1ubuntu2_all.deb) ... Unpacking replacement libdpkg-perl ... Preparing to replace linux-libc-dev 3.1.0-1.1 (using .../linux-libc-dev_3.1.0-2.3_amd64.deb) ... Unpacking replacement linux-libc-dev ... Preparing to replace pkgbinarymangler 104 (using .../pkgbinarymangler_105_all.deb) ... Unpacking replacement pkgbinarymangler ... Setting up libgomp1 (4.6.2-2ubuntu1) ... Setting up cpp-4.6 (4.6.2-2ubuntu1) ... Setting up libquadmath0 (4.6.2-2ubuntu1) ... Setting up binutils (2.21.90.20111025-1ubuntu1) ... Setting up gcc-4.6 (4.6.2-2ubuntu1) ... Setting up libglib2.0-0 (2.30.1-2ubuntu1) ... No schema files found: doing nothing. Setting up libnih1 (1.0.3-4ubuntu4) ... Setting up libnih-dbus1 (1.0.3-4ubuntu4) ... Setting up libkrb5support0 (1.9.1+dfsg-1ubuntu2.1) ... Setting up libk5crypto3 (1.9.1+dfsg-1ubuntu2.1) ... Setting up libkrb5-3 (1.9.1+dfsg-1ubuntu2.1) ... Setting up libgssapi-krb5-2 (1.9.1+dfsg-1ubuntu2.1) ... Setting up libcurl3-gnutls (7.21.7-3ubuntu1) ... Setting up libp11-kit0 (0.7-2) ... Setting up busybox-initramfs (1:1.18.5-1ubuntu1) ... Setting up initramfs-tools-bin (0.99ubuntu8) ... Setting up initramfs-tools (0.99ubuntu8) ... update-initramfs: deferring update (trigger activated) Setting up upstart (1.3-0ubuntu11) ... Installing new version of config file /etc/init/failsafe.conf ... Setting up procps (1:3.2.8-11ubuntu1) ... invoke-rc.d: policy-rc.d denied execution of start. Setting up libdpkg-perl (1.16.1.1ubuntu2) ... Setting up dpkg-dev (1.16.1.1ubuntu2) ... Setting up linux-libc-dev (3.1.0-2.3) ... Setting up pkgbinarymangler (105) ... Setting up libstdc++6-4.6-dev (4.6.2-2ubuntu1) ... Setting up g++-4.6 (4.6.2-2ubuntu1) ... Processing triggers for libc-bin ... ldconfig deferred processing now taking place Processing triggers for initramfs-tools ... RUN: /usr/share/launchpad-buildd/slavebin/sbuild-package ['sbuild-package', '46bb7d668cc12656460de3cceab2f15fa1ccc233', 'amd64', 'precise', '--nolog', '--batch', '--archive=ubuntu', '--dist=precise', '--purpose=PRIMARY', '--architecture=amd64', '--comp=universe', 'cbmc_4.0-4.dsc'] Initiating build 46bb7d668cc12656460de3cceab2f15fa1ccc233 with 2 processor cores. Automatic build of cbmc_4.0-4 on yellow by sbuild/amd64 1.170.5 Build started at 20111102-1300 ****************************************************************************** cbmc_4.0-4.dsc exists in cwd sh: gcc: not found dpkg-architecture: warning: Couldn't determine gcc system type, falling back to default (native compilation) ** Using build dependencies supplied by package: Build-Depends: debhelper (>= 7.0.50~), minisat (>= 1:2.2.1-2), zlib1g-dev, flex, bison sh: gcc: not found dpkg-architecture: warning: Couldn't determine gcc system type, falling back to default (native compilation) sh: gcc: not found dpkg-architecture: warning: Couldn't determine gcc system type, falling back to default (native compilation) sh: gcc: not found dpkg-architecture: warning: Couldn't determine gcc system type, falling back to default (native compilation) sh: gcc: not found dpkg-architecture: warning: Couldn't determine gcc system type, falling back to default (native compilation) sh: gcc: not found dpkg-architecture: warning: Couldn't determine gcc system type, falling back to default (native compilation) sh: gcc: not found dpkg-architecture: warning: Couldn't determine gcc system type, falling back to default (native compilation) sh: gcc: not found dpkg-architecture: warning: Couldn't determine gcc system type, falling back to default (native compilation) sh: gcc: not found dpkg-architecture: warning: Couldn't determine gcc system type, falling back to default (native compilation) Checking for already installed source dependencies... debhelper: missing minisat: missing zlib1g-dev: missing flex: missing bison: missing Checking for source dependency conflicts... /usr/bin/sudo /usr/bin/apt-get --purge $CHROOT_OPTIONS -q -y install debhelper minisat zlib1g-dev flex bison Reading package lists... Building dependency tree... Reading state information... The following extra packages will be installed: bsdmainutils file gettext gettext-base groff-base html2text intltool-debian libcroco3 libgettextpo0 libmagic1 libpipeline1 libunistring0 libxml2 m4 man-db po-debconf Suggested packages: bison-doc wamerican wordlist whois vacation dh-make gettext-doc groff less www-browser libmail-box-perl Recommended packages: curl wget lynx-cur 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 libcroco3 libgettextpo0 libmagic1 libpipeline1 libunistring0 libxml2 m4 man-db minisat po-debconf zlib1g-dev 0 upgraded, 21 newly installed, 0 to remove and 0 not upgraded. Need to get 6882 kB of archives. After this operation, 23.1 MB of additional disk space will be used. WARNING: The following packages cannot be authenticated! libpipeline1 libxml2 m4 flex libcroco3 libunistring0 libgettextpo0 libmagic1 file bsdmainutils gettext-base groff-base man-db bison html2text gettext intltool-debian po-debconf debhelper zlib1g-dev minisat Authentication warning overridden. Get:1 http://ftpmaster.internal/ubuntu/ precise/main libpipeline1 amd64 1.2.0-4 [26.2 kB] Get:2 http://ftpmaster.internal/ubuntu/ precise/main libxml2 amd64 2.7.8.dfsg-5ubuntu1 [673 kB] Get:3 http://ftpmaster.internal/ubuntu/ precise/main m4 amd64 1.4.16-2 [200 kB] Get:4 http://ftpmaster.internal/ubuntu/ precise/main flex amd64 2.5.35-10ubuntu1 [250 kB] Get:5 http://ftpmaster.internal/ubuntu/ precise/main libcroco3 amd64 0.6.2-1ubuntu1 [96.0 kB] Get:6 http://ftpmaster.internal/ubuntu/ precise/main libunistring0 amd64 0.9.3-4ubuntu1 [426 kB] Get:7 http://ftpmaster.internal/ubuntu/ precise/main libgettextpo0 amd64 0.18.1.1-5ubuntu1 [120 kB] Get:8 http://ftpmaster.internal/ubuntu/ precise/main libmagic1 amd64 5.09-2 [217 kB] Get:9 http://ftpmaster.internal/ubuntu/ precise/main file amd64 5.09-2 [19.7 kB] Get:10 http://ftpmaster.internal/ubuntu/ precise/main bsdmainutils amd64 8.2.3 [198 kB] Get:11 http://ftpmaster.internal/ubuntu/ precise/main gettext-base amd64 0.18.1.1-5ubuntu1 [80.3 kB] Get:12 http://ftpmaster.internal/ubuntu/ precise/main groff-base amd64 1.21-6 [1047 kB] Get:13 http://ftpmaster.internal/ubuntu/ precise/main man-db amd64 2.6.0.2-2 [729 kB] Get:14 http://ftpmaster.internal/ubuntu/ precise/main bison amd64 1:2.4.1.dfsg-3 [493 kB] Get:15 http://ftpmaster.internal/ubuntu/ precise/main html2text amd64 1.3.2a-15 [104 kB] Get:16 http://ftpmaster.internal/ubuntu/ precise/main gettext amd64 0.18.1.1-5ubuntu1 [1188 kB] Get:17 http://ftpmaster.internal/ubuntu/ precise/main intltool-debian all 0.35.0+20060710.1 [31.6 kB] Get:18 http://ftpmaster.internal/ubuntu/ precise/main po-debconf all 1.0.16+nmu1 [212 kB] Get:19 http://ftpmaster.internal/ubuntu/ precise/main debhelper all 8.9.8ubuntu1 [478 kB] Get:20 http://ftpmaster.internal/ubuntu/ precise/main zlib1g-dev amd64 1:1.2.3.4.dfsg-3ubuntu3 [167 kB] Get:21 http://ftpmaster.internal/ubuntu/ precise/universe minisat amd64 1:2.2.1-3 [127 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 6882 kB in 0s (16.9 MB/s) Selecting previously unselected package libpipeline1. (Reading database ... 14123 files and directories currently installed.) Unpacking libpipeline1 (from .../libpipeline1_1.2.0-4_amd64.deb) ... Selecting previously unselected package libxml2. Unpacking libxml2 (from .../libxml2_2.7.8.dfsg-5ubuntu1_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-10ubuntu1_amd64.deb) ... Selecting previously unselected package libcroco3. Unpacking libcroco3 (from .../libcroco3_0.6.2-1ubuntu1_amd64.deb) ... Selecting previously unselected package libunistring0. Unpacking libunistring0 (from .../libunistring0_0.9.3-4ubuntu1_amd64.deb) ... Selecting previously unselected package libgettextpo0. Unpacking libgettextpo0 (from .../libgettextpo0_0.18.1.1-5ubuntu1_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 bsdmainutils. Unpacking bsdmainutils (from .../bsdmainutils_8.2.3_amd64.deb) ... Selecting previously unselected package gettext-base. Unpacking gettext-base (from .../gettext-base_0.18.1.1-5ubuntu1_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-2_amd64.deb) ... Selecting previously unselected package bison. Unpacking bison (from .../bison_1%3a2.4.1.dfsg-3_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-5ubuntu1_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+nmu1_all.deb) ... Selecting previously unselected package debhelper. Unpacking debhelper (from .../debhelper_8.9.8ubuntu1_all.deb) ... Selecting previously unselected package zlib1g-dev. Unpacking zlib1g-dev (from .../zlib1g-dev_1%3a1.2.3.4.dfsg-3ubuntu3_amd64.deb) ... Selecting previously unselected package minisat. Unpacking minisat (from .../minisat_1%3a2.2.1-3_amd64.deb) ... Setting up libpipeline1 (1.2.0-4) ... Setting up libxml2 (2.7.8.dfsg-5ubuntu1) ... Setting up m4 (1.4.16-2) ... Setting up flex (2.5.35-10ubuntu1) ... Setting up libcroco3 (0.6.2-1ubuntu1) ... Setting up libunistring0 (0.9.3-4ubuntu1) ... Setting up libgettextpo0 (0.18.1.1-5ubuntu1) ... Setting up libmagic1 (5.09-2) ... Setting up file (5.09-2) ... 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 gettext-base (0.18.1.1-5ubuntu1) ... Setting up groff-base (1.21-6) ... Setting up man-db (2.6.0.2-2) ... Building database of manual pages ... Setting up bison (1:2.4.1.dfsg-3) ... 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-5ubuntu1) ... Setting up intltool-debian (0.35.0+20060710.1) ... Setting up po-debconf (1.0.16+nmu1) ... Setting up debhelper (8.9.8ubuntu1) ... Setting up zlib1g-dev (1:1.2.3.4.dfsg-3ubuntu3) ... Setting up minisat (1:2.2.1-3) ... Processing triggers for libc-bin ... ldconfig deferred processing now taking place Checking correctness of source dependencies... Toolchain package versions: libc6-dev_2.13-20ubuntu5 make_3.81-8.1ubuntu1 dpkg-dev_1.16.1.1ubuntu2 gcc-4.6_4.6.2-2ubuntu1 g++-4.6_4.6.2-2ubuntu1 binutils_2.21.90.20111025-1ubuntu1 libstdc++6-4.6-dev_4.6.2-2ubuntu1 libstdc++6_4.6.2-2ubuntu1 ------------------------------------------------------------------------------ dpkg-source: warning: -sn is not a valid option for Dpkg::Source::Package::V3::quilt gpgv: Signature made Sat Oct 22 20:17:17 2011 UTC 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 dpkg-buildpackage: export CFLAGS from dpkg-buildflags (origin: vendor): -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security dpkg-buildpackage: export CPPFLAGS from dpkg-buildflags (origin: vendor): -D_FORTIFY_SOURCE=2 dpkg-buildpackage: export CXXFLAGS from dpkg-buildflags (origin: vendor): -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security dpkg-buildpackage: export FFLAGS from dpkg-buildflags (origin: vendor): -g -O2 dpkg-buildpackage: export LDFLAGS from dpkg-buildflags (origin: vendor): -Wl,-Bsymbolic-functions -Wl,-z,relro dpkg-buildpackage: source package cbmc dpkg-buildpackage: source version 4.0-4 dpkg-source --before-build cbmc-4.0 dpkg-buildpackage: host architecture amd64 /usr/bin/fakeroot debian/rules clean dh --parallel clean dh_testdir -O--parallel dh_auto_clean -O--parallel make[1]: Entering directory `/build/buildd/cbmc-4.0' make -C src clean make[2]: Entering directory `/build/buildd/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 make[3]: Entering directory `/build/buildd/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 rm -f y.tab.h y.tab.cpp lex.yy.cpp y.tab.cpp.output y.output rm -f library/converter cprover_library.inc make[3]: Entering directory `/build/buildd/cbmc-4.0/src/big-int' rm -f bigint-test.o bigint-func.o bigint.o test-bigint make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/big-int' make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/ansi-c' if [ -e cbmc/. ] ; then \ make -C cbmc clean ; \ fi if [ -e cpp/. ] ; then \ make -C cpp clean ; \ fi make[3]: Entering directory `/build/buildd/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/buildd/cbmc-4.0/src/cbmc' if [ -e goto-cc/. ] ; then \ make -C goto-cc clean ; \ fi make[3]: Entering directory `/build/buildd/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/buildd/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/buildd/cbmc-4.0/src/cpp' if [ -e goto-instrument/. ] ; then \ make -C goto-instrument clean ; \ fi make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/goto-cc' if [ -e goto-programs/. ] ; then \ make -C goto-programs clean ; \ fi make[3]: Entering directory `/build/buildd/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 make[3]: Entering directory `/build/buildd/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/buildd/cbmc-4.0/src/goto-instrument' if [ -e goto-symex/. ] ; then \ make -C goto-symex clean ; \ fi make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/goto-programs' if [ -e langapi/. ] ; then \ make -C langapi clean ; \ fi make[3]: Entering directory `/build/buildd/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/buildd/cbmc-4.0/src/langapi' rm -f mode.o language_ui.o languages.o language_util.o langapi.a make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/goto-symex' make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/langapi' if [ -e pointer-analysis/. ] ; then \ make -C pointer-analysis clean ; \ fi if [ -e solvers/. ] ; then \ make -C solvers clean ; \ fi make[3]: Entering directory `/build/buildd/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]: Leaving directory `/build/buildd/cbmc-4.0/src/pointer-analysis' if [ -e util/. ] ; then \ make -C util clean ; \ fi make[3]: Entering directory `/build/buildd/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]: Leaving directory `/build/buildd/cbmc-4.0/src/solvers' if [ -e xmllang/. ] ; then \ make -C xmllang clean ; \ fi make[3]: Entering directory `/build/buildd/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/buildd/cbmc-4.0/src/xmllang' make[3]: Entering directory `/build/buildd/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 rm -f ieee_float_test ieee_float_test.o rm -f irep_ids_convert irep_ids_convert.o make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/util' rm -f *.o make[2]: Leaving directory `/build/buildd/cbmc-4.0/src' make[1]: Leaving directory `/build/buildd/cbmc-4.0' dh_clean -O--parallel 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/buildd/cbmc-4.0' make -C src make[2]: Entering directory `/build/buildd/cbmc-4.0/src' ## Entering big-int make -C big-int make[3]: Entering directory `/build/buildd/cbmc-4.0/src/big-int' g++ -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D_FORTIFY_SOURCE=2 -c -o bigint-test.o bigint-test.cc g++ -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D_FORTIFY_SOURCE=2 -c -o bigint-func.o bigint-func.cc g++ -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D_FORTIFY_SOURCE=2 -c -o bigint.o bigint.cc g++ -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -o test-bigint bigint-test.o bigint-func.o bigint.o make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/big-int' ## Entering util make -C util make[3]: Entering directory `/build/buildd/cbmc-4.0/src/util' g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -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 -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o arith_tools.o arith_tools.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o base_type.o base_type.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o cmdline.o cmdline.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o config.o config.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o context.o context.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o expr.o expr.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o expr_util.o expr_util.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o i2string.o i2string.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o irep.o irep.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o language.o language.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o lispexpr.o lispexpr.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o lispirep.o lispirep.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o location.o location.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o message.o message.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o language_file.o language_file.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o mp_arith.o mp_arith.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o namespace.o namespace.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o parseoptions.o parseoptions.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o rename.o rename.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o replace_expr.o replace_expr.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o threeval.o threeval.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o typecheck.o typecheck.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o graph.o graph.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o type.o type.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o cnf_simplify.o cnf_simplify.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o str_getline.o str_getline.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o strstream2string.o strstream2string.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o bitvector.o bitvector.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o parser.o parser.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o map_util.o map_util.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o replace_symbol.o replace_symbol.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o actuals.o actuals.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o get_module.o get_module.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o string_hash.o string_hash.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o string_container.o string_container.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o identifier.o identifier.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o rational.o rational.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o options.o options.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o c_misc.o c_misc.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o simplify_expr.o simplify_expr.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o dstring.o dstring.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o find_symbols.o find_symbols.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o rational_tools.o rational_tools.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o ui_message.o ui_message.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o simplify_utils.o simplify_utils.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o time_stopping.o time_stopping.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o symbol.o symbol.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o irep_hash_container.o irep_hash_container.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o type_eq.o type_eq.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o guard.o guard.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o array_name.o array_name.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o gcd.o gcd.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o message_stream.o message_stream.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o substitute.o substitute.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o decision_procedure.o decision_procedure.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o union_find.o union_find.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o pretty_names.o pretty_names.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o xml.o xml.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o xml_irep.o xml_irep.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o std_types.o std_types.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o std_code.o std_code.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o format_constant.o format_constant.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o find_macros.o find_macros.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o ref_expr_set.o ref_expr_set.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o std_expr.o std_expr.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o irep_serialization.o irep_serialization.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o symbol_serialization.o symbol_serialization.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o fixedbv.o fixedbv.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o ieee_float.o ieee_float.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o signal_catcher.o signal_catcher.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o pointer_offset_size.o pointer_offset_size.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o bv_arithmetic.o bv_arithmetic.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o tempdir.o tempdir.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o tempfile.o tempfile.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o timer.o timer.cpp ./irep_ids_convert table < irep_ids.txt > irep_ids.inc g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o irep_ids.o irep_ids.cpp ld -r -o util.a 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 g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I . -o ieee_float_test.o ieee_float_test.cpp g++ -o ieee_float_test util.a ieee_float_test.o ../big-int/bigint.o make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/util' ## Entering langapi make -C langapi make[3]: Entering directory `/build/buildd/cbmc-4.0/src/langapi' g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o mode.o mode.cpp ## Entering cpp make -C cpp make[3]: Entering directory `/build/buildd/cbmc-4.0/src/cpp' g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_id.o cpp_id.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o language_ui.o language_ui.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_language.o cpp_language.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o languages.o languages.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o expr2cpp.o expr2cpp.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o language_util.o language_util.cpp ld -r -o langapi.a mode.o language_ui.o languages.o language_util.o make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/langapi' ## Entering ansi-c make -C ansi-c make[3]: Entering directory `/build/buildd/cbmc-4.0/src/ansi-c' g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o c_typecast.o c_typecast.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_parser.o cpp_parser.cpp bison -y -v $flags -pyyansi_c -d parser.y -o y.tab.cpp flex -Pyycpp -olex.yy.cpp scanner.l g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck.o cpp_typecheck.cpp flex -Pyyansi_c -olex.yy.cpp scanner.l g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o ansi_c_parser.o ansi_c_parser.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o expr2c.o expr2c.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_convert_type.o cpp_convert_type.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_expr.o cpp_typecheck_expr.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o ansi_c_language.o ansi_c_language.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o c_sizeof.o c_sizeof.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o c_main.o c_main.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o c_types.o c_types.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_code.o cpp_typecheck_code.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o c_final.o c_final.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o trans_unit.o trans_unit.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o ansi_c_typecheck.o ansi_c_typecheck.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_type.o cpp_typecheck_type.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o c_link.o c_link.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o parse.o parse.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o c_preprocess.o c_preprocess.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o c_link_type_eq.o c_link_type_eq.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o c_typecheck_base.o c_typecheck_base.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o c_typecheck_initializer.o c_typecheck_initializer.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_parse_tree.o cpp_parse_tree.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_token_buffer.o cpp_token_buffer.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o c_typecheck_typecast.o c_typecheck_typecast.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_fargs.o cpp_typecheck_fargs.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o c_typecheck_code.o c_typecheck_code.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_resolve.o cpp_typecheck_resolve.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o c_typecheck_expr.o c_typecheck_expr.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_util.o cpp_util.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_function.o cpp_typecheck_function.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o c_typecheck_type.o c_typecheck_type.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_namespace.o cpp_typecheck_namespace.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o string_constant.o string_constant.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_name.o cpp_name.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o c_qualifiers.o c_qualifiers.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_is_pod.o cpp_is_pod.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o c_typecheck_argc_argv.o c_typecheck_argc_argv.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o ansi_c_parse_tree.o ansi_c_parse_tree.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_scope.o cpp_scope.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o preprocessor_line.o preprocessor_line.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o ansi_c_convert.o ansi_c_convert.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_find_constructor.o cpp_typecheck_find_constructor.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o ansi_c_convert_type.o ansi_c_convert_type.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o template_map.o template_map.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o type2name.o type2name.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_scopes.o cpp_scopes.cpp g++ -o library/converter library/converter.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o anonymous_member.o anonymous_member.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_declarator.o cpp_declarator.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o printf_formatter.o printf_formatter.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_instantiate_template.o cpp_instantiate_template.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o internal_additions.o internal_additions.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o ansi_c_declaration.o ansi_c_declaration.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o designator.o designator.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o internal_additions.o internal_additions.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o concatenate_strings.o concatenate_strings.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o literals/parse_float.o literals/parse_float.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_type2name.o cpp_type2name.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o literals/unescape_string.o literals/unescape_string.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_linkage_spec.o cpp_typecheck_linkage_spec.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o literals/convert_float_literal.o literals/convert_float_literal.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_template.o cpp_typecheck_template.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o literals/convert_character_literal.o literals/convert_character_literal.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o literals/convert_integer_literal.o literals/convert_integer_literal.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o literals/convert_string_literal.o literals/convert_string_literal.cpp if [ -e y.tab.hpp ] ; then mv y.tab.hpp y.tab.h ; else \ mv y.tab.cpp.h y.tab.h ; fi cat library/*.c | library/converter > cprover_library.inc g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o y.tab.o y.tab.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_function_bodies.o cpp_typecheck_function_bodies.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_initializer.o cpp_typecheck_initializer.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_compound_type.o cpp_typecheck_compound_type.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o lex.yy.o lex.yy.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_constructor.o cpp_constructor.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o cprover_library.o cprover_library.cpp ld -r -o ansi-c.a 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 make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/ansi-c' ## Entering xmllang make -C xmllang make[3]: Entering directory `/build/buildd/cbmc-4.0/src/xmllang' g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o xml_language.o xml_language.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_destructor.o cpp_destructor.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o xml_parser.o xml_parser.cpp bison -y -v $flags -pyyxml -d parser.y -o y.tab.cpp flex -Pyyxml -olex.yy.cpp scanner.l g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o xml_typecheck.o xml_typecheck.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_final.o cpp_final.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_conversions.o cpp_typecheck_conversions.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o xml_parse_tree.o xml_parse_tree.cpp if [ -e y.tab.hpp ] ; then mv y.tab.hpp y.tab.h ; else \ mv y.tab.cpp.h y.tab.h ; fi g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o y.tab.o y.tab.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o lex.yy.o lex.yy.cpp ld -r -o xmllang.a xml_language.o xml_parser.o y.tab.o lex.yy.o xml_typecheck.o xml_parse_tree.o make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/xmllang' ## Entering solvers make -C solvers make[3]: Entering directory `/build/buildd/cbmc-4.0/src/solvers' g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o sat/satcheck_minisat2.o sat/satcheck_minisat2.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o sat/cnf.o sat/cnf.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_declaration.o cpp_typecheck_declaration.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o sat/dimacs_cnf.o sat/dimacs_cnf.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o sat/cnf_clause_list.o sat/cnf_clause_list.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o sat/pbs_dimacs_cnf.o sat/pbs_dimacs_cnf.cpp sat/pbs_dimacs_cnf.cpp: In member function 'bool pbs_dimacs_cnft::pbs_solve()': sat/pbs_dimacs_cnf.cpp:129:26: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o sat/read_dimacs_cnf.o sat/read_dimacs_cnf.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_declarator_converter.o cpp_declarator_converter.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o sat/resolution_proof.o sat/resolution_proof.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o sat/satcheck.o sat/satcheck.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o qbf/qdimacs_cnf.o qbf/qdimacs_cnf.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_declaration.o cpp_declaration.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o qbf/qbf_quantor.o qbf/qbf_quantor.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_namespace_spec.o cpp_namespace_spec.cpp qbf/qbf_quantor.cpp: In member function 'virtual propt::resultt qbf_quantort::prop_solve()': qbf/qbf_quantor.cpp:124:42: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_using.o cpp_typecheck_using.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o qbf/qbf_skizzo.o qbf/qbf_skizzo.cpp qbf/qbf_skizzo.cpp: In member function 'virtual propt::resultt qbf_skizzot::prop_solve()': qbf/qbf_skizzo.cpp:130:41: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o qbf/qdimacs_core.o qbf/qdimacs_core.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_enum_type.o cpp_typecheck_enum_type.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o qbf/qbf_qube.o qbf/qbf_qube.cpp qbf/qbf_qube.cpp: In member function 'virtual propt::resultt qbf_qubet::prop_solve()': qbf/qbf_qube.cpp:130:41: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_bases.o cpp_typecheck_bases.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o qbf/qbf_qube_core.o qbf/qbf_qube_core.cpp qbf/qbf_qube_core.cpp: In member function 'virtual propt::resultt qbf_qube_coret::prop_solve()': qbf/qbf_qube_core.cpp:110:42: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_constructor.o cpp_typecheck_constructor.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o prop/prop.o prop/prop.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o prop/prop_conv.o prop/prop_conv.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o prop/prop_conv_store.o prop/prop_conv_store.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o prop/aig_formula.o prop/aig_formula.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o prop/aig.o prop/aig.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o prop/aig_prop.o prop/aig_prop.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o cvc/cvc_prop.o cvc/cvc_prop.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o cvc/cvc_conv.o cvc/cvc_conv.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_typecheck_virtual_table.o cpp_typecheck_virtual_table.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o lex.yy.o lex.yy.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o cvc/cvc_dec.o cvc/cvc_dec.cpp cvc/cvc_dec.cpp: In member function 'virtual decision_proceduret::resultt cvc_dect::dec_solve()': cvc/cvc_dec.cpp:99:26: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o smt1/smt1_dec.o smt1/smt1_dec.cpp smt1/smt1_dec.cpp: In member function 'virtual decision_proceduret::resultt smt1_dect::dec_solve()': smt1/smt1_dec.cpp:150:26: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] ld -r -o cpp.a 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 g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o smt1/smt1_prop.o smt1/smt1_prop.cpp make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/cpp' ## Entering goto-symex make -C goto-symex make[3]: Entering directory `/build/buildd/cbmc-4.0/src/goto-symex' g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o symex_target.o symex_target.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o smt1/smt1_conv.o smt1/smt1_conv.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o symex_target_equation.o symex_target_equation.cpp smt1/smt1_conv.cpp: In member function 'exprt smt1_convt::binary2union(const union_typet&, const string&) const': smt1/smt1_conv.cpp:2987:35: warning: unused variable 'components' [-Wunused-variable] g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o basic_symex.o basic_symex.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o symex_main.o symex_main.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o smt2/smt2_dec.o smt2/smt2_dec.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_trace.o goto_trace.cpp smt2/smt2_dec.cpp: In member function 'virtual decision_proceduret::resultt smt2_dect::dec_solve()': smt2/smt2_dec.cpp:150:26: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o build_goto_trace.o build_goto_trace.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o symex_function.o symex_function.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o smt2/smt2_prop.o smt2/smt2_prop.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o smt2/smt2_conv.o smt2/smt2_conv.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_symex_state.o goto_symex_state.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o dplib/dplib_conv.o dplib/dplib_conv.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o symex_dereference.o symex_dereference.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o symex_goto.o symex_goto.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o dplib/dplib_dec.o dplib/dplib_dec.cpp dplib/dplib_dec.cpp: In member function 'virtual decision_proceduret::resultt dplib_dect::dec_solve()': dplib/dplib_dec.cpp:99:26: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o dplib/dplib_prop.o dplib/dplib_prop.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o builtin_functions.o builtin_functions.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/equality.o flattening/equality.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o slice.o slice.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/arrays.o flattening/arrays.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o symex_other.o symex_other.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o slice_by_trace.o slice_by_trace.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/functions.o flattening/functions.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/sat_minimizer.o flattening/sat_minimizer.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_width.o flattening/boolbv_width.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o xml_goto_trace.o xml_goto_trace.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv.o flattening/boolbv.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o symex_decl.o symex_decl.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_constraint_select_one.o flattening/boolbv_constraint_select_one.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o precondition.o precondition.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/bv_pointers.o flattening/bv_pointers.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o postcondition.o postcondition.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o symex_clean_expr.o symex_clean_expr.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/bv_utils.o flattening/bv_utils.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o symex_dereference_state.o symex_dereference_state.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o vcd_goto_trace.o vcd_goto_trace.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_abs.o flattening/boolbv_abs.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o auto_objects.o auto_objects.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_with.o flattening/boolbv_with.cpp ld -r -o goto-symex.a 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 make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/goto-symex' ## Entering pointer-analysis make -C pointer-analysis make[3]: Entering directory `/build/buildd/cbmc-4.0/src/pointer-analysis' g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o value_set.o value_set.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_typecast.o flattening/boolbv_typecast.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_index.o flattening/boolbv_index.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_member.o flattening/boolbv_member.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_if.o flattening/boolbv_if.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_program_dereference.o goto_program_dereference.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_byte_extract.o flattening/boolbv_byte_extract.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o value_set_analysis.o value_set_analysis.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_add_sub.o flattening/boolbv_add_sub.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_mult.o flattening/boolbv_mult.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o dereference.o dereference.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_constant.o flattening/boolbv_constant.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_extractbit.o flattening/boolbv_extractbit.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o pointer_offset_sum.o pointer_offset_sum.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_bv_rel.o flattening/boolbv_bv_rel.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o add_failed_symbols.o add_failed_symbols.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o show_value_sets.o show_value_sets.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_shift.o flattening/boolbv_shift.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o value_set_domain.o value_set_domain.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_case.o flattening/boolbv_case.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o rewrite_index.o rewrite_index.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_cond.o flattening/boolbv_cond.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o value_set_analysis_fi.o value_set_analysis_fi.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_concatenation.o flattening/boolbv_concatenation.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_div.o flattening/boolbv_div.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o value_set_fi.o value_set_fi.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_mod.o flattening/boolbv_mod.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_extractbits.o flattening/boolbv_extractbits.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_replication.o flattening/boolbv_replication.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o value_set_domain_fi.o value_set_domain_fi.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_reduction.o flattening/boolbv_reduction.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o value_set_analysis_fivr.o value_set_analysis_fivr.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_overflow.o flattening/boolbv_overflow.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_get.o flattening/boolbv_get.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o value_set_fivr.o value_set_fivr.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_bitwise.o flattening/boolbv_bitwise.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_equality.o flattening/boolbv_equality.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_unary_minus.o flattening/boolbv_unary_minus.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o value_set_domain_fivr.o value_set_domain_fivr.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_ieee_float_rel.o flattening/boolbv_ieee_float_rel.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o value_set_analysis_fivrns.o value_set_analysis_fivrns.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/pointer_logic.o flattening/pointer_logic.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_quantifier.o flattening/boolbv_quantifier.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o value_set_fivrns.o value_set_fivrns.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_struct.o flattening/boolbv_struct.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_byte_update.o flattening/boolbv_byte_update.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_array_of.o flattening/boolbv_array_of.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_map.o flattening/boolbv_map.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o value_set_domain_fivrns.o value_set_domain_fivrns.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_type.o flattening/boolbv_type.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Wall -MMD -O2 -g -I .. -I /usr/include/minisat -I ../util -o flattening/boolbv_union.o flattening/boolbv_union.cpp ld -r -o pointer-analysis.a 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 ld -r -o solvers.a 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 make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/pointer-analysis' ## Entering goto-programs make -C goto-programs make[3]: Entering directory `/build/buildd/cbmc-4.0/src/goto-programs' g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_convert.o goto_convert.cpp make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/solvers' g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_function.o goto_function.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_main.o goto_main.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_sideeffects.o goto_sideeffects.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_program.o goto_program.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o basic_blocks.o basic_blocks.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_threads.o goto_threads.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_check.o goto_check.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_function_pointers.o goto_function_pointers.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_functions.o goto_functions.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_inline.o goto_inline.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o remove_skip.o remove_skip.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_convert_functions.o goto_convert_functions.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o string_instrumentation.o string_instrumentation.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o builtin_functions.o builtin_functions.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o show_claims.o show_claims.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o destructor.o destructor.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o set_claims.o set_claims.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o slicer.o slicer.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o invariant_set.o invariant_set.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o invariant_propagation.o invariant_propagation.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o add_race_assertions.o add_race_assertions.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o rw_set.o rw_set.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o read_goto_binary.o read_goto_binary.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o invariant_set_domain.o invariant_set_domain.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o static_analysis.o static_analysis.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o string_abstraction.o string_abstraction.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_program_serialization.o goto_program_serialization.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_function_serialization.o goto_function_serialization.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o read_bin_goto_object.o read_bin_goto_object.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_program_irep.o goto_program_irep.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o interpreter.o interpreter.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o interpreter_evaluate.o interpreter_evaluate.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o flow_insensitive_analysis.o flow_insensitive_analysis.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o format_strings.o format_strings.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o loop_numbers.o loop_numbers.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o pointer_arithmetic.o pointer_arithmetic.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_program_template.o goto_program_template.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o write_goto_binary.o write_goto_binary.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o remove_unreachable.o remove_unreachable.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o remove_unused_functions.o remove_unused_functions.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o dynamic_memory.o dynamic_memory.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o dump_c.o dump_c.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o wp.o wp.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_rw.o goto_rw.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o goto_clean_expr.o goto_clean_expr.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o safety_checker.o safety_checker.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o compute_called_functions.o compute_called_functions.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -o link_to_library.o link_to_library.cpp ld -r -o goto-programs.a 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 make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/goto-programs' ## Entering cbmc make -C cbmc make[3]: Entering directory `/build/buildd/cbmc-4.0/src/cbmc' g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o main.o main.cpp ## Entering goto-cc make -C goto-cc make[3]: Entering directory `/build/buildd/cbmc-4.0/src/goto-cc' g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -D HAVE_CPP -o goto-cc.o goto-cc.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -D HAVE_CPP -o cmdline_options.o cmdline_options.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o parseoptions.o parseoptions.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -D HAVE_CPP -o get_base_name.o get_base_name.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -D HAVE_CPP -o gcc_cmdline.o gcc_cmdline.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -D HAVE_CPP -o ms_cl_cmdline.o ms_cl_cmdline.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -D HAVE_CPP -o compile.o compile.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o bmc.o bmc.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o dimacs.o dimacs.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -D HAVE_CPP -o armcc_cmdline.o armcc_cmdline.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -D HAVE_CPP -o languages.o languages.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o languages.o languages.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -D HAVE_CPP -o goto_cc_cmdline.o goto_cc_cmdline.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -D HAVE_CPP -o xml_binaries/xml_irep_hashing.o xml_binaries/xml_irep_hashing.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o bv_cbmc.o bv_cbmc.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -D HAVE_CPP -o xml_binaries/xml_symbol_hashing.o xml_binaries/xml_symbol_hashing.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -D HAVE_CPP -o xml_binaries/xml_symbol.o xml_binaries/xml_symbol.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o symex_bmc.o symex_bmc.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o show_vcc.o show_vcc.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -D HAVE_CPP -o xml_binaries/xml_goto_function.o xml_binaries/xml_goto_function.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -D HAVE_CPP -o xml_binaries/xml_goto_function_hashing.o xml_binaries/xml_goto_function_hashing.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o cbmc_solvers.o cbmc_solvers.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -D HAVE_CPP -o xml_binaries/xml_goto_program.o xml_binaries/xml_goto_program.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o xml_interface.o xml_interface.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -D HAVE_CPP -o xml_binaries/xml_goto_program_hashing.o xml_binaries/xml_goto_program_hashing.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o counterexample_beautification.o counterexample_beautification.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o counterexample_beautification_greedy.o counterexample_beautification_greedy.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -D HAVE_CPP -o xml_binaries/read_goto_object.o xml_binaries/read_goto_object.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o counterexample_beautification_pbs.o counterexample_beautification_pbs.cpp g++ -o cbmc 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 ../ansi-c/ansi-c.a ../big-int/bigint.o ../goto-programs/goto-programs.a ../goto-symex/goto-symex.a ../pointer-analysis/pointer-analysis.a ../langapi/langapi.a ../xmllang/xmllang.a ../solvers/solvers.a ../util/util.a ../cpp/cpp.a -lminisat g++ -o goto-cc 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 ../big-int/bigint.o ../goto-programs/goto-programs.a ../pointer-analysis/pointer-analysis.a ../util/util.a ../ansi-c/ansi-c.a ../xmllang/xmllang.a ../langapi/langapi.a ../cpp/cpp.a make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/cbmc' ## Entering goto-instrument make -C goto-instrument make[3]: Entering directory `/build/buildd/cbmc-4.0/src/goto-instrument' g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o main.o main.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o parseoptions.o parseoptions.cpp make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/goto-cc' g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o document_claims.o document_claims.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o languages.o languages.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o uninitialized.o uninitialized.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o uninitialized_domain.o uninitialized_domain.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o full_slicer.o full_slicer.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o object_id.o object_id.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o show_locations.o show_locations.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o points_to.o points_to.cpp g++ -c -g -O2 -fstack-protector --param=ssp-buffer-size=4 -Wformat -Wformat-security -Wall -MMD -O2 -g -Wall -MMD -O2 -g -I .. -I ../util -DHAVE_CPP -o alignment_checks.o alignment_checks.cpp g++ -o goto-instrument 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 ../ansi-c/ansi-c.a ../big-int/bigint.o ../goto-programs/goto-programs.a ../goto-symex/goto-symex.a ../pointer-analysis/pointer-analysis.a ../langapi/langapi.a ../util/util.a ../cpp/cpp.a make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/goto-instrument' make[2]: Leaving directory `/build/buildd/cbmc-4.0/src' make[1]: Leaving directory `/build/buildd/cbmc-4.0' dh_auto_test -O--parallel /usr/bin/fakeroot debian/rules binary-arch dh --parallel binary-arch dh_testroot -a -O--parallel dh_prep -a -O--parallel dh_installdirs -a -O--parallel dh_auto_install -a -O--parallel dh_install -a -O--parallel dh_installdocs -a -O--parallel dh_installchangelogs -a -O--parallel dh_installexamples -a -O--parallel dh_installman -a -O--parallel dh_installcatalogs -a -O--parallel dh_installcron -a -O--parallel dh_installdebconf -a -O--parallel dh_installemacsen -a -O--parallel dh_installifupdown -a -O--parallel dh_installinfo -a -O--parallel dh_installinit -a -O--parallel dh_installmenu -a -O--parallel dh_installmime -a -O--parallel dh_installmodules -a -O--parallel dh_installlogcheck -a -O--parallel dh_installlogrotate -a -O--parallel dh_installpam -a -O--parallel dh_installppp -a -O--parallel dh_installudev -a -O--parallel dh_installwm -a -O--parallel dh_installxfonts -a -O--parallel dh_installgsettings -a -O--parallel dh_bugfiles -a -O--parallel dh_ucf -a -O--parallel dh_lintian -a -O--parallel dh_gconf -a -O--parallel dh_icons -a -O--parallel dh_perl -a -O--parallel dh_usrlocal -a -O--parallel dh_link -a -O--parallel dh_compress -a -O--parallel dh_fixperms -a -O--parallel dh_strip -a -O--parallel dh_strip debug symbol extraction: all non-arch-all packages for this build platform amd64: cbmc dh_strip debug symbol extraction: packages to act on: cbmc dh_strip debug symbol extraction: ignored packages: dpkg-deb: building package `cbmc-dbgsym' in `../cbmc-dbgsym_4.0-4_amd64.ddeb'. dh_makeshlibs -a -O--parallel dh_shlibdeps -a -O--parallel dh_installdeb -a -O--parallel dh_gencontrol -a -O--parallel dh_md5sums -a -O--parallel dh_builddeb -a -O--parallel INFO: pkgstriptranslations version 105 pkgstriptranslations: processing control file: ./debian/cbmc/DEBIAN/control, package cbmc, directory ./debian/cbmc pkgstriptranslations: cbmc does not contain translations, skipping pkgmaintainermangler: Maintainer field overridden to "Ubuntu Developers " pkgstripfiles: processing control file: debian/cbmc/DEBIAN/control, package cbmc, directory debian/cbmc dpkg-deb: warning: 'debian/cbmc/DEBIAN/control' contains user-defined field 'Original-Maintainer' dpkg-deb: warning: ignoring 1 warning about the control file(s) dpkg-deb: building package `cbmc' in `../cbmc_4.0-4_amd64.deb'. dpkg-genchanges -B -mUbuntu/amd64 Build Daemon >../cbmc_4.0-4_amd64.changes dpkg-genchanges: arch-specific upload - not including arch-independent packages dpkg-genchanges: binary-only upload - not including any source code dpkg-source --after-build cbmc-4.0 dpkg-buildpackage: binary only upload (no source included) ****************************************************************************** Build finished at 20111102-1311 Publishing debug debs. chroot-autobuild/build/buildd/cbmc_4.0-4_amd64.deb: new debian package, version 2.0. size 4519864 bytes: control archive= 724 bytes. 574 bytes, 14 lines control 291 bytes, 5 lines md5sums Package: cbmc Version: 4.0-4 Architecture: amd64 Maintainer: Ubuntu Developers Original-Maintainer: Michael Tautschnig Installed-Size: 10560 Depends: gcc, libc6 (>= 2.4), libgcc1 (>= 1:4.1.1), libstdc++6 (>= 4.6), minisat Section: science Priority: extra Homepage: http://www.cprover.org/cbmc/ Description: bounded model checker for C and C++ programs CBMC generates traces that demonstrate how an assertion can be violated, or proves that the assertion cannot be violated within a given number of loop iterations. chroot-autobuild/build/buildd/cbmc_4.0-4_amd64.deb: drwxr-xr-x root/root 0 2011-11-02 13:09 ./ drwxr-xr-x root/root 0 2011-11-02 13:09 ./usr/ drwxr-xr-x root/root 0 2011-11-02 13:11 ./usr/bin/ -rwxr-xr-x root/root 4179424 2011-11-02 13:11 ./usr/bin/cbmc -rwxr-xr-x root/root 3236312 2011-11-02 13:11 ./usr/bin/goto-cc -rwxr-xr-x root/root 3364264 2011-11-02 13:11 ./usr/bin/goto-instrument drwxr-xr-x root/root 0 2011-11-02 13:09 ./usr/share/ drwxr-xr-x root/root 0 2011-11-02 13:09 ./usr/share/doc/ drwxr-xr-x root/root 0 2011-11-02 13:09 ./usr/share/doc/cbmc/ -rw-r--r-- root/root 3580 2011-05-13 23:02 ./usr/share/doc/cbmc/copyright -rw-r--r-- root/root 576 2011-10-21 23:51 ./usr/share/doc/cbmc/changelog.Debian.gz cbmc_4.0-4_amd64.changes: Format: 1.8 Date: Sat, 22 Oct 2011 00:51:01 +0100 Source: cbmc Binary: cbmc Architecture: amd64 Version: 4.0-4 Distribution: precise Urgency: low Maintainer: Ubuntu/amd64 Build Daemon Changed-By: Michael Tautschnig Description: cbmc - bounded model checker for C and C++ programs Closes: 643074 Changes: cbmc (4.0-4) unstable; urgency=low . * Rename patches and update description to make dpkg-source happy (closes: #643074) Checksums-Sha1: bf9af342ea138df355b03c6a4dc97c2eafa99c87 4519864 cbmc_4.0-4_amd64.deb Checksums-Sha256: 630b0717a2433c506736d92e6158f07b6b5fe8bd661489c39abc0af1b326c81c 4519864 cbmc_4.0-4_amd64.deb Files: 2692d0ac79e245b17093e0e8635943e1 4519864 science extra cbmc_4.0-4_amd64.deb ****************************************************************************** Built successfully Purging chroot-autobuild/build/buildd/cbmc-4.0 ------------------------------------------------------------------------------ /usr/bin/sudo dpkg --purge intltool-debian groff-base m4 gettext file zlib1g-dev html2text flex gettext-base debhelper bison po-debconf libunistring0 libcroco3 libmagic1 libpipeline1 libxml2 bsdmainutils minisat libgettextpo0 man-db (Reading database ... 15447 files and directories currently installed.) Removing zlib1g-dev ... Removing flex ... Removing debhelper ... Removing bison ... Removing po-debconf ... Removing minisat ... Purging configuration files for minisat ... Removing man-db ... Purging configuration files for man-db ... Removing catpages as well as /var/cache/man hierarchy. Removing intltool-debian ... Removing groff-base ... Purging configuration files for groff-base ... Removing m4 ... Removing gettext ... Removing file ... Removing html2text ... Purging configuration files for html2text ... Removing gettext-base ... Removing libmagic1 ... Purging configuration files for libmagic1 ... Removing libpipeline1 ... Purging configuration files for libpipeline1 ... Removing bsdmainutils ... Purging configuration files for bsdmainutils ... Removing libgettextpo0 ... Removing libunistring0 ... Purging configuration files for libunistring0 ... Removing libcroco3 ... Purging configuration files for libcroco3 ... Removing libxml2 ... Purging configuration files for libxml2 ... Processing triggers for libc-bin ... ldconfig deferred processing now taking place ****************************************************************************** Finished at 20111102-1311 Build needed 00:09:47, 825516k disk space RUN: /usr/share/launchpad-buildd/slavebin/scan-for-processes ['/usr/share/launchpad-buildd/slavebin/scan-for-processes', '46bb7d668cc12656460de3cceab2f15fa1ccc233'] Scanning for processes to kill in build /home/buildd/build-46bb7d668cc12656460de3cceab2f15fa1ccc233/chroot-autobuild... RUN: /usr/share/launchpad-buildd/slavebin/umount-chroot ['umount-chroot', '46bb7d668cc12656460de3cceab2f15fa1ccc233'] Unmounting chroot for build 46bb7d668cc12656460de3cceab2f15fa1ccc233... none /home/buildd/build-46bb7d668cc12656460de3cceab2f15fa1ccc233/chroot-autobuild/proc proc rw,relatime 0 0 none /home/buildd/build-46bb7d668cc12656460de3cceab2f15fa1ccc233/chroot-autobuild/dev/pts devpts rw,relatime 0 0 none /home/buildd/build-46bb7d668cc12656460de3cceab2f15fa1ccc233/chroot-autobuild/sys sysfs rw,relatime 0 0 none /home/buildd/build-46bb7d668cc12656460de3cceab2f15fa1ccc233/chroot-autobuild/dev/shm tmpfs rw,relatime 0 0 RUN: /usr/share/launchpad-buildd/slavebin/remove-build ['remove-build', '46bb7d668cc12656460de3cceab2f15fa1ccc233'] Removing build 46bb7d668cc12656460de3cceab2f15fa1ccc233