RUN: /bin/echo ['echo', 'Forking build subprocess...'] Forking build subprocess... RUN: /usr/share/launchpad-buildd/slavebin/unpack-chroot ['unpack-chroot', '2660107dd317f22588ba3bcea72b58b4a2435b42', '/home/buildd/filecache-default/ae10d4f56684bfa9d24ade2bcf83271f973d3afa'] Synching the system clock with the buildd NTP service... 2 Nov 21:20:33 ntpdate[24032]: adjust time server 10.211.37.1 offset -0.000061 sec Unpacking chroot for build 2660107dd317f22588ba3bcea72b58b4a2435b42 RUN: /usr/share/launchpad-buildd/slavebin/mount-chroot ['mount-chroot', '2660107dd317f22588ba3bcea72b58b4a2435b42'] Mounting chroot for build 2660107dd317f22588ba3bcea72b58b4a2435b42 RUN: /usr/share/launchpad-buildd/slavebin/override-sources-list ['override-sources-list', '2660107dd317f22588ba3bcea72b58b4a2435b42', 'deb http://ftpmaster.internal/ubuntu precise main universe'] Overriding sources.list in build-2660107dd317f22588ba3bcea72b58b4a2435b42 RUN: /usr/share/launchpad-buildd/slavebin/update-debian-chroot ['update-debian-chroot', '2660107dd317f22588ba3bcea72b58b4a2435b42', 'powerpc'] Updating debian chroot for build 2660107dd317f22588ba3bcea72b58b4a2435b42 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 powerpc Packages [1240 kB] Get:4 http://ftpmaster.internal precise/universe powerpc Packages [4531 kB] Get:5 http://ftpmaster.internal precise/main TranslationIndex [74 B] Get:6 http://ftpmaster.internal precise/universe TranslationIndex [75 B] Get:7 http://ftpmaster.internal precise/main Translation-en [715 kB] Get:8 http://ftpmaster.internal precise/universe Translation-en [3257 kB] Fetched 9793 kB in 12s (805 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 libgomp1 libgssapi-krb5-2 libk5crypto3 libkrb5-3 libkrb5support0 libnih-dbus1 libnih1 libp11-kit0 libpam-modules libpam-modules-bin libpam-runtime libpam0g libss2 libstdc++6 libstdc++6-4.6-dev linux-libc-dev pkgbinarymangler procps tzdata upstart xz-utils 40 upgraded, 1 newly installed, 0 to remove and 0 not upgraded. Need to get 28.0 MB of archives. After this operation, 3943 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 libstdc++6-4.6-dev g++-4.6 gcc-4.6 libgcc1 binutils libcomerr2 liblzma5 libpam0g libpam-modules-bin libpam-modules libss2 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 powerpc 6.5ubuntu2 [56.2 kB] Get:2 http://ftpmaster.internal/ubuntu/ precise/main dpkg powerpc 1.16.1.1ubuntu2 [1805 kB] Get:3 http://ftpmaster.internal/ubuntu/ precise/main dash powerpc 0.5.7-2ubuntu1 [86.8 kB] Get:4 http://ftpmaster.internal/ubuntu/ precise/main diffutils powerpc 1:3.2-1 [208 kB] Get:5 http://ftpmaster.internal/ubuntu/ precise/main e2fslibs powerpc 1.42~WIP-2011-10-16-1ubuntu1 [195 kB] Get:6 http://ftpmaster.internal/ubuntu/ precise/main e2fsprogs powerpc 1.42~WIP-2011-10-16-1ubuntu1 [960 kB] Get:7 http://ftpmaster.internal/ubuntu/ precise/main libgomp1 powerpc 4.6.2-2ubuntu1 [26.1 kB] Get:8 http://ftpmaster.internal/ubuntu/ precise/main gcc-4.6-base powerpc 4.6.2-2ubuntu1 [15.9 kB] Get:9 http://ftpmaster.internal/ubuntu/ precise/main libstdc++6 powerpc 4.6.2-2ubuntu1 [364 kB] Get:10 http://ftpmaster.internal/ubuntu/ precise/main cpp-4.6 powerpc 4.6.2-2ubuntu1 [4620 kB] Get:11 http://ftpmaster.internal/ubuntu/ precise/main libstdc++6-4.6-dev powerpc 4.6.2-2ubuntu1 [1646 kB] Get:12 http://ftpmaster.internal/ubuntu/ precise/main g++-4.6 powerpc 4.6.2-2ubuntu1 [6115 kB] Get:13 http://ftpmaster.internal/ubuntu/ precise/main gcc-4.6 powerpc 4.6.2-2ubuntu1 [5166 kB] Get:14 http://ftpmaster.internal/ubuntu/ precise/main libgcc1 powerpc 1:4.6.2-2ubuntu1 [42.9 kB] Get:15 http://ftpmaster.internal/ubuntu/ precise/main binutils powerpc 2.21.90.20111025-1ubuntu1 [2531 kB] Get:16 http://ftpmaster.internal/ubuntu/ precise/main libcomerr2 powerpc 1.42~WIP-2011-10-16-1ubuntu1 [56.4 kB] Get:17 http://ftpmaster.internal/ubuntu/ precise/main liblzma5 powerpc 5.1.1alpha+20110809-3 [93.0 kB] Get:18 http://ftpmaster.internal/ubuntu/ precise/main libpam0g powerpc 1.1.3-5ubuntu2 [55.6 kB] Get:19 http://ftpmaster.internal/ubuntu/ precise/main libpam-modules-bin powerpc 1.1.3-5ubuntu2 [30.3 kB] Get:20 http://ftpmaster.internal/ubuntu/ precise/main libpam-modules powerpc 1.1.3-5ubuntu2 [273 kB] Get:21 http://ftpmaster.internal/ubuntu/ precise/main libss2 powerpc 1.42~WIP-2011-10-16-1ubuntu1 [61.4 kB] Get:22 http://ftpmaster.internal/ubuntu/ precise/main libnih-dbus1 powerpc 1.0.3-4ubuntu4 [15.3 kB] Get:23 http://ftpmaster.internal/ubuntu/ precise/main libnih1 powerpc 1.0.3-4ubuntu4 [51.1 kB] Get:24 http://ftpmaster.internal/ubuntu/ precise/main libk5crypto3 powerpc 1.9.1+dfsg-1ubuntu2.1 [89.1 kB] Get:25 http://ftpmaster.internal/ubuntu/ precise/main libgssapi-krb5-2 powerpc 1.9.1+dfsg-1ubuntu2.1 [111 kB] Get:26 http://ftpmaster.internal/ubuntu/ precise/main libkrb5-3 powerpc 1.9.1+dfsg-1ubuntu2.1 [347 kB] Get:27 http://ftpmaster.internal/ubuntu/ precise/main libkrb5support0 powerpc 1.9.1+dfsg-1ubuntu2.1 [22.7 kB] Get:28 http://ftpmaster.internal/ubuntu/ precise/main libcurl3-gnutls powerpc 7.21.7-3ubuntu1 [224 kB] Get:29 http://ftpmaster.internal/ubuntu/ precise/main libp11-kit0 powerpc 0.7-2 [31.4 kB] Get:30 http://ftpmaster.internal/ubuntu/ precise/main libpam-runtime powerpc 1.1.3-5ubuntu2 [45.2 kB] Get:31 http://ftpmaster.internal/ubuntu/ precise/main tzdata powerpc 2011n-1 [401 kB] Get:32 http://ftpmaster.internal/ubuntu/ precise/main xz-utils powerpc 5.1.1alpha+20110809-3 [87.9 kB] Get:33 http://ftpmaster.internal/ubuntu/ precise/main busybox-initramfs powerpc 1:1.18.5-1ubuntu1 [179 kB] Get:34 http://ftpmaster.internal/ubuntu/ precise/main initramfs-tools all 0.99ubuntu8 [51.7 kB] Get:35 http://ftpmaster.internal/ubuntu/ precise/main initramfs-tools-bin powerpc 0.99ubuntu8 [11.9 kB] Get:36 http://ftpmaster.internal/ubuntu/ precise/main upstart powerpc 1.3-0ubuntu11 [258 kB] Get:37 http://ftpmaster.internal/ubuntu/ precise/main procps powerpc 1:3.2.8-11ubuntu1 [228 kB] Get:38 http://ftpmaster.internal/ubuntu/ precise/main dpkg-dev all 1.16.1.1ubuntu2 [468 kB] Get:39 http://ftpmaster.internal/ubuntu/ precise/main libdpkg-perl all 1.16.1.1ubuntu2 [181 kB] Get:40 http://ftpmaster.internal/ubuntu/ precise/main linux-libc-dev powerpc 3.1.0-2.3 [802 kB] Get:41 http://ftpmaster.internal/ubuntu/ precise/main pkgbinarymangler all 105 [27.1 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 28.0 MB in 2s (11.5 MB/s) (Reading database ... 14061 files and directories currently installed.) Preparing to replace base-files 6.4ubuntu6 (using .../base-files_6.5ubuntu2_powerpc.deb) ... Unpacking replacement base-files ... Setting up base-files (6.5ubuntu2) ... (Reading database ... 14061 files and directories currently installed.) Preparing to replace dpkg 1.16.1ubuntu1 (using .../dpkg_1.16.1.1ubuntu2_powerpc.deb) ... Unpacking replacement dpkg ... Setting up dpkg (1.16.1.1ubuntu2) ... (Reading database ... 14061 files and directories currently installed.) Preparing to replace dash 0.5.5.1-7.4ubuntu1 (using .../dash_0.5.7-2ubuntu1_powerpc.deb) ... Unpacking replacement dash ... Setting up dash (0.5.7-2ubuntu1) ... (Reading database ... 14061 files and directories currently installed.) Preparing to replace diffutils 1:3.0-1 (using .../diffutils_1%3a3.2-1_powerpc.deb) ... Unpacking replacement diffutils ... Setting up diffutils (1:3.2-1) ... (Reading database ... 14061 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_powerpc.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 ... 14061 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_powerpc.deb) ... Unpacking replacement e2fsprogs ... Setting up e2fsprogs (1.42~WIP-2011-10-16-1ubuntu1) ... (Reading database ... 14061 files and directories currently installed.) Preparing to replace libgomp1 4.6.1-15ubuntu1 (using .../libgomp1_4.6.2-2ubuntu1_powerpc.deb) ... Unpacking replacement libgomp1 ... Preparing to replace gcc-4.6-base 4.6.1-15ubuntu1 (using .../gcc-4.6-base_4.6.2-2ubuntu1_powerpc.deb) ... Unpacking replacement gcc-4.6-base ... Setting up gcc-4.6-base (4.6.2-2ubuntu1) ... (Reading database ... 14062 files and directories currently installed.) Preparing to replace libstdc++6 4.6.1-15ubuntu1 (using .../libstdc++6_4.6.2-2ubuntu1_powerpc.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 ... 14062 files and directories currently installed.) Preparing to replace cpp-4.6 4.6.1-15ubuntu1 (using .../cpp-4.6_4.6.2-2ubuntu1_powerpc.deb) ... Unpacking replacement cpp-4.6 ... Preparing to replace libstdc++6-4.6-dev 4.6.1-15ubuntu1 (using .../libstdc++6-4.6-dev_4.6.2-2ubuntu1_powerpc.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_powerpc.deb) ... Unpacking replacement g++-4.6 ... Preparing to replace gcc-4.6 4.6.1-15ubuntu1 (using .../gcc-4.6_4.6.2-2ubuntu1_powerpc.deb) ... Unpacking replacement gcc-4.6 ... Preparing to replace libgcc1 1:4.6.1-15ubuntu1 (using .../libgcc1_1%3a4.6.2-2ubuntu1_powerpc.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 ... 14062 files and directories currently installed.) Preparing to replace binutils 2.21.90.20111004-2ubuntu1 (using .../binutils_2.21.90.20111025-1ubuntu1_powerpc.deb) ... Unpacking replacement binutils ... Preparing to replace libcomerr2 1.42~WIP-2011-10-09-1ubuntu1 (using .../libcomerr2_1.42~WIP-2011-10-16-1ubuntu1_powerpc.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 ... 14062 files and directories currently installed.) Unpacking liblzma5 (from .../liblzma5_5.1.1alpha+20110809-3_powerpc.deb) ... Setting up liblzma5 (5.1.1alpha+20110809-3) ... Processing triggers for libc-bin ... ldconfig deferred processing now taking place (Reading database ... 14070 files and directories currently installed.) Preparing to replace libpam0g 1.1.3-2ubuntu1 (using .../libpam0g_1.1.3-5ubuntu2_powerpc.deb) ... Unpacking replacement libpam0g ... Setting up libpam0g (1.1.3-5ubuntu2) ... Processing triggers for libc-bin ... ldconfig deferred processing now taking place (Reading database ... 14070 files and directories currently installed.) Preparing to replace libpam-modules-bin 1.1.3-2ubuntu1 (using .../libpam-modules-bin_1.1.3-5ubuntu2_powerpc.deb) ... Unpacking replacement libpam-modules-bin ... Setting up libpam-modules-bin (1.1.3-5ubuntu2) ... (Reading database ... 14070 files and directories currently installed.) Preparing to replace libpam-modules 1.1.3-2ubuntu1 (using .../libpam-modules_1.1.3-5ubuntu2_powerpc.deb) ... Unpacking replacement libpam-modules ... Setting up libpam-modules (1.1.3-5ubuntu2) ... (Reading database ... 14070 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_powerpc.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 ... 14070 files and directories currently installed.) Preparing to replace libnih-dbus1 1.0.3-4ubuntu3 (using .../libnih-dbus1_1.0.3-4ubuntu4_powerpc.deb) ... Unpacking replacement libnih-dbus1 ... Preparing to replace libnih1 1.0.3-4ubuntu3 (using .../libnih1_1.0.3-4ubuntu4_powerpc.deb) ... Unpacking replacement libnih1 ... Preparing to replace libk5crypto3 1.9.1+dfsg-1ubuntu1 (using .../libk5crypto3_1.9.1+dfsg-1ubuntu2.1_powerpc.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_powerpc.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_powerpc.deb) ... Unpacking replacement libkrb5-3 ... Preparing to replace libkrb5support0 1.9.1+dfsg-1ubuntu1 (using .../libkrb5support0_1.9.1+dfsg-1ubuntu2.1_powerpc.deb) ... Unpacking replacement libkrb5support0 ... Preparing to replace libcurl3-gnutls 7.21.6-3ubuntu3 (using .../libcurl3-gnutls_7.21.7-3ubuntu1_powerpc.deb) ... Unpacking replacement libcurl3-gnutls ... Preparing to replace libp11-kit0 0.6-0ubuntu2 (using .../libp11-kit0_0.7-2_powerpc.deb) ... Unpacking replacement libp11-kit0 ... Preparing to replace libpam-runtime 1.1.3-2ubuntu1 (using .../libpam-runtime_1.1.3-5ubuntu2_powerpc.deb) ... Unpacking replacement libpam-runtime ... Setting up libpam-runtime (1.1.3-5ubuntu2) ... (Reading database ... 14072 files and directories currently installed.) Preparing to replace tzdata 2011l-2 (using .../tzdata_2011n-1_powerpc.deb) ... Unpacking replacement tzdata ... Setting up tzdata (2011n-1) ... Current default time zone: 'Etc/UTC' Local time is now: Wed Nov 2 21:22:03 UTC 2011. Universal Time is now: Wed Nov 2 21:22:03 UTC 2011. Run 'dpkg-reconfigure tzdata' if you wish to change it. (Reading database ... 14072 files and directories currently installed.) Preparing to replace xz-utils 5.1.1alpha+20110809-2 (using .../xz-utils_5.1.1alpha+20110809-3_powerpc.deb) ... Unpacking replacement xz-utils ... Setting up xz-utils (5.1.1alpha+20110809-3) ... (Reading database ... 14072 files and directories currently installed.) Preparing to replace busybox-initramfs 1:1.18.4-2ubuntu2 (using .../busybox-initramfs_1%3a1.18.5-1ubuntu1_powerpc.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_powerpc.deb) ... Unpacking replacement initramfs-tools-bin ... Preparing to replace upstart 1.3-0ubuntu10 (using .../upstart_1.3-0ubuntu11_powerpc.deb) ... Unpacking replacement upstart ... Preparing to replace procps 1:3.2.8-10ubuntu5 (using .../procps_1%3a3.2.8-11ubuntu1_powerpc.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_powerpc.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 binutils (2.21.90.20111025-1ubuntu1) ... Setting up gcc-4.6 (4.6.2-2ubuntu1) ... 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', '2660107dd317f22588ba3bcea72b58b4a2435b42', 'powerpc', 'precise', '--nolog', '--batch', '--archive=ubuntu', '--dist=precise', '--purpose=PRIMARY', '--architecture=powerpc', '--comp=universe', 'cbmc_4.0-4.dsc'] Initiating build 2660107dd317f22588ba3bcea72b58b4a2435b42 with 2 processor cores. Automatic build of cbmc_4.0-4 on adare by sbuild/powerpc 1.170.5 Build started at 20111102-2122 ****************************************************************************** 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 6689 kB of archives. After this operation, 22.7 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 powerpc 1.2.0-4 [25.6 kB] Get:2 http://ftpmaster.internal/ubuntu/ precise/main libxml2 powerpc 2.7.8.dfsg-5ubuntu1 [619 kB] Get:3 http://ftpmaster.internal/ubuntu/ precise/main m4 powerpc 1.4.16-2 [191 kB] Get:4 http://ftpmaster.internal/ubuntu/ precise/main flex powerpc 2.5.35-10ubuntu1 [244 kB] Get:5 http://ftpmaster.internal/ubuntu/ precise/main libcroco3 powerpc 0.6.2-1ubuntu1 [88.0 kB] Get:6 http://ftpmaster.internal/ubuntu/ precise/main libunistring0 powerpc 0.9.3-4ubuntu1 [409 kB] Get:7 http://ftpmaster.internal/ubuntu/ precise/main libgettextpo0 powerpc 0.18.1.1-5ubuntu1 [114 kB] Get:8 http://ftpmaster.internal/ubuntu/ precise/main libmagic1 powerpc 5.09-2 [224 kB] Get:9 http://ftpmaster.internal/ubuntu/ precise/main file powerpc 5.09-2 [19.6 kB] Get:10 http://ftpmaster.internal/ubuntu/ precise/main bsdmainutils powerpc 8.2.3 [197 kB] Get:11 http://ftpmaster.internal/ubuntu/ precise/main gettext-base powerpc 0.18.1.1-5ubuntu1 [57.3 kB] Get:12 http://ftpmaster.internal/ubuntu/ precise/main groff-base powerpc 1.21-6 [1044 kB] Get:13 http://ftpmaster.internal/ubuntu/ precise/main man-db powerpc 2.6.0.2-2 [721 kB] Get:14 http://ftpmaster.internal/ubuntu/ precise/main bison powerpc 1:2.4.1.dfsg-3 [483 kB] Get:15 http://ftpmaster.internal/ubuntu/ precise/main html2text powerpc 1.3.2a-15 [106 kB] Get:16 http://ftpmaster.internal/ubuntu/ precise/main gettext powerpc 0.18.1.1-5ubuntu1 [1132 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 powerpc 1:1.2.3.4.dfsg-3ubuntu3 [163 kB] Get:21 http://ftpmaster.internal/ubuntu/ precise/universe minisat powerpc 1:2.2.1-3 [132 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 6689 kB in 0s (10.7 MB/s) Selecting previously unselected package libpipeline1. (Reading database ... 14072 files and directories currently installed.) Unpacking libpipeline1 (from .../libpipeline1_1.2.0-4_powerpc.deb) ... Selecting previously unselected package libxml2. Unpacking libxml2 (from .../libxml2_2.7.8.dfsg-5ubuntu1_powerpc.deb) ... Selecting previously unselected package m4. Unpacking m4 (from .../m4_1.4.16-2_powerpc.deb) ... Selecting previously unselected package flex. Unpacking flex (from .../flex_2.5.35-10ubuntu1_powerpc.deb) ... Selecting previously unselected package libcroco3. Unpacking libcroco3 (from .../libcroco3_0.6.2-1ubuntu1_powerpc.deb) ... Selecting previously unselected package libunistring0. Unpacking libunistring0 (from .../libunistring0_0.9.3-4ubuntu1_powerpc.deb) ... Selecting previously unselected package libgettextpo0. Unpacking libgettextpo0 (from .../libgettextpo0_0.18.1.1-5ubuntu1_powerpc.deb) ... Selecting previously unselected package libmagic1. Unpacking libmagic1 (from .../libmagic1_5.09-2_powerpc.deb) ... Selecting previously unselected package file. Unpacking file (from .../file_5.09-2_powerpc.deb) ... Selecting previously unselected package bsdmainutils. Unpacking bsdmainutils (from .../bsdmainutils_8.2.3_powerpc.deb) ... Selecting previously unselected package gettext-base. Unpacking gettext-base (from .../gettext-base_0.18.1.1-5ubuntu1_powerpc.deb) ... Selecting previously unselected package groff-base. Unpacking groff-base (from .../groff-base_1.21-6_powerpc.deb) ... Selecting previously unselected package man-db. Unpacking man-db (from .../man-db_2.6.0.2-2_powerpc.deb) ... Selecting previously unselected package bison. Unpacking bison (from .../bison_1%3a2.4.1.dfsg-3_powerpc.deb) ... Selecting previously unselected package html2text. Unpacking html2text (from .../html2text_1.3.2a-15_powerpc.deb) ... Selecting previously unselected package gettext. Unpacking gettext (from .../gettext_0.18.1.1-5ubuntu1_powerpc.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_powerpc.deb) ... Selecting previously unselected package minisat. Unpacking minisat (from .../minisat_1%3a2.2.1-3_powerpc.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 powerpc /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/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' if [ -e cbmc/. ] ; then \ make -C cbmc 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]: Leaving directory `/build/buildd/cbmc-4.0/src/ansi-c' 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]: Leaving directory `/build/buildd/cbmc-4.0/src/cpp' if [ -e goto-instrument/. ] ; then \ make -C goto-instrument clean ; \ fi 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/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]: Leaving directory `/build/buildd/cbmc-4.0/src/goto-instrument' if [ -e goto-symex/. ] ; then \ make -C goto-symex clean ; \ fi 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]: 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]: Leaving directory `/build/buildd/cbmc-4.0/src/goto-programs' if [ -e langapi/. ] ; then \ make -C langapi clean ; \ fi make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/goto-symex' if [ -e pointer-analysis/. ] ; then \ make -C pointer-analysis clean ; \ fi 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/langapi' 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/util' rm -f arith_tools.o base_type.o cmdline.o config.o context.o expr.o expr_util.o i2string.o irep.o language.o lispexpr.o lispirep.o location.o message.o language_file.o mp_arith.o namespace.o parseoptions.o rename.o replace_expr.o threeval.o typecheck.o graph.o type.o cnf_simplify.o str_getline.o strstream2string.o bitvector.o parser.o map_util.o replace_symbol.o actuals.o get_module.o string_hash.o string_container.o identifier.o rational.o options.o c_misc.o simplify_expr.o dstring.o find_symbols.o rational_tools.o ui_message.o simplify_utils.o time_stopping.o symbol.o irep_hash_container.o type_eq.o guard.o array_name.o gcd.o message_stream.o substitute.o decision_procedure.o union_find.o pretty_names.o xml.o xml_irep.o std_types.o std_code.o format_constant.o find_macros.o ref_expr_set.o std_expr.o irep_serialization.o symbol_serialization.o fixedbv.o ieee_float.o signal_catcher.o pointer_offset_size.o bv_arithmetic.o tempdir.o tempfile.o timer.o irep_ids.o util.a rm -f irep_ids.h irep_ids.inc make[3]: 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 \ rm -f ieee_float_test ieee_float_test.o xmllang.a rm -f irep_ids_convert irep_ids_convert.o make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/util' make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/xmllang' 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 ## Entering cpp make -C langapi make -C cpp 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 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 -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 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 -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 flex -Pyycpp -olex.yy.cpp scanner.l bison -y -v $flags -pyyansi_c -d parser.y -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.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 -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_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 -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 -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 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 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_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 -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 -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 -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_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 -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 -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 -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 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_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 -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 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_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 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 -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_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 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 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 -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_scopes.o cpp_scopes.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 -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_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 -D CPP_SYSTEMC_EXTENSION -I .. -I ../util -o cpp_instantiate_template.o cpp_instantiate_template.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 -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 -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 -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 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 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 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 -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/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 -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_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_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 -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 -I .. -I ../util -o cprover_library.o cprover_library.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 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 -I .. -I ../util -o xml_parser.o xml_parser.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 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 -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/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 -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 -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 -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_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 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 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] 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 -Wall -MMD -O2 -g -I .. -I ../util -o symex_target_equation.o symex_target_equation.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_prop.o smt1/smt1_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 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 basic_symex.o basic_symex.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 symex_main.o symex_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_trace.o 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 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 build_goto_trace.o build_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 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 -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 -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_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 -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 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 -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 -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 -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 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 -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_width.o flattening/boolbv_width.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 -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 -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 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 -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 -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 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 -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_if.o flattening/boolbv_if.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 -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_mult.o flattening/boolbv_mult.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 -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 -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 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 -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_cond.o flattening/boolbv_cond.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 -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_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_overflow.o flattening/boolbv_overflow.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_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 -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_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/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 -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/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 -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 -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_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 -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 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 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 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 make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/solvers' ## 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/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 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 ## Entering goto-cc make -C cbmc make -C goto-cc 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 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 -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 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 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 -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 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 -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 -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_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 -DHAVE_CPP -o counterexample_beautification_pbs.o counterexample_beautification_pbs.cpp 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 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 make[3]: Leaving directory `/build/buildd/cbmc-4.0/src/goto-cc' ## 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/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 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 powerpc: 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_powerpc.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_powerpc.deb'. dpkg-genchanges -B -mUbuntu/powerpc Build Daemon >../cbmc_4.0-4_powerpc.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-2137 Publishing debug debs. chroot-autobuild/build/buildd/cbmc_4.0-4_powerpc.deb: new debian package, version 2.0. size 4603474 bytes: control archive= 726 bytes. 576 bytes, 14 lines control 291 bytes, 5 lines md5sums Package: cbmc Version: 4.0-4 Architecture: powerpc Maintainer: Ubuntu Developers Original-Maintainer: Michael Tautschnig Installed-Size: 10499 Depends: gcc, libc6 (>= 2.4), libgcc1 (>= 1:4.2.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_powerpc.deb: tar: Record size = 8 blocks drwxr-xr-x root/root 0 2011-11-02 21:35 ./ drwxr-xr-x root/root 0 2011-11-02 21:35 ./usr/ drwxr-xr-x root/root 0 2011-11-02 21:37 ./usr/bin/ -rwxr-xr-x root/root 4175520 2011-11-02 21:37 ./usr/bin/cbmc -rwxr-xr-x root/root 3210172 2011-11-02 21:37 ./usr/bin/goto-cc -rwxr-xr-x root/root 3331540 2011-11-02 21:37 ./usr/bin/goto-instrument drwxr-xr-x root/root 0 2011-11-02 21:35 ./usr/share/ drwxr-xr-x root/root 0 2011-11-02 21:35 ./usr/share/doc/ drwxr-xr-x root/root 0 2011-11-02 21:35 ./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_powerpc.changes: Format: 1.8 Date: Sat, 22 Oct 2011 00:51:01 +0100 Source: cbmc Binary: cbmc Architecture: powerpc Version: 4.0-4 Distribution: precise Urgency: low Maintainer: Ubuntu/powerpc 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: 1bacddb2fefdb745f56a0d18ea206ee32079d456 4603474 cbmc_4.0-4_powerpc.deb Checksums-Sha256: 6cf9b279bef888a8f5768d5338b60735d6c93236b58812776aca99b0f7f1618d 4603474 cbmc_4.0-4_powerpc.deb Files: a2fe65bb29f1f6467b085c49fbfc06ca 4603474 science extra cbmc_4.0-4_powerpc.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 ... 15396 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-2137 Build needed 00:14:26, 634920k disk space Can't open average time db /var/debbuild/avg-build-times Can't open average space db /var/debbuild/avg-build-space RUN: /usr/share/launchpad-buildd/slavebin/scan-for-processes ['/usr/share/launchpad-buildd/slavebin/scan-for-processes', '2660107dd317f22588ba3bcea72b58b4a2435b42'] Scanning for processes to kill in build /home/buildd/build-2660107dd317f22588ba3bcea72b58b4a2435b42/chroot-autobuild... RUN: /usr/share/launchpad-buildd/slavebin/umount-chroot ['umount-chroot', '2660107dd317f22588ba3bcea72b58b4a2435b42'] Unmounting chroot for build 2660107dd317f22588ba3bcea72b58b4a2435b42... none /home/buildd/build-2660107dd317f22588ba3bcea72b58b4a2435b42/chroot-autobuild/proc proc rw,relatime 0 0 none /home/buildd/build-2660107dd317f22588ba3bcea72b58b4a2435b42/chroot-autobuild/dev/pts devpts rw,relatime,mode=600,ptmxmode=000 0 0 none /home/buildd/build-2660107dd317f22588ba3bcea72b58b4a2435b42/chroot-autobuild/sys sysfs rw,relatime 0 0 none /home/buildd/build-2660107dd317f22588ba3bcea72b58b4a2435b42/chroot-autobuild/dev/shm tmpfs rw,relatime 0 0 RUN: /usr/share/launchpad-buildd/slavebin/remove-build ['remove-build', '2660107dd317f22588ba3bcea72b58b4a2435b42'] Removing build 2660107dd317f22588ba3bcea72b58b4a2435b42