Mock Version: 1.1.33 Mock Version: 1.1.33 ENTER do(['bash', '--login', '-c', 'rpmbuild -bs --target i686 --nodeps builddir/build/SPECS/cbmc.spec'], False, '/var/lib/mock/f18-build-1845203-320396/root/', None, 86400, True, False, 1000, 425, None, False, {'LANG': 'en_US.UTF-8', 'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOSTNAME': 'mock', 'PROMPT_COMMAND': 'echo -n ""', 'HOME': '/builddir', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin'}, logger=) Executing command: ['bash', '--login', '-c', 'rpmbuild -bs --target i686 --nodeps builddir/build/SPECS/cbmc.spec'] with env {'LANG': 'en_US.UTF-8', 'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOSTNAME': 'mock', 'PROMPT_COMMAND': 'echo -n ""', 'HOME': '/builddir', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin'} Building target platforms: i686 Building for target i686 Wrote: /builddir/build/SRPMS/cbmc-4.3-7.20130515svn.fc18.src.rpm Child return code was: 0 LEAVE do --> ENTER do(['bash', '--login', '-c', 'rpmbuild -bb --target i686 --nodeps builddir/build/SPECS/cbmc.spec'], False, '/var/lib/mock/f18-build-1845203-320396/root/', None, 86400, True, False, 1000, 425, None, False, {'LANG': 'en_US.UTF-8', 'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOSTNAME': 'mock', 'PROMPT_COMMAND': 'echo -n ""', 'HOME': '/builddir', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin'}, logger=) Executing command: ['bash', '--login', '-c', 'rpmbuild -bb --target i686 --nodeps builddir/build/SPECS/cbmc.spec'] with env {'LANG': 'en_US.UTF-8', 'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOSTNAME': 'mock', 'PROMPT_COMMAND': 'echo -n ""', 'HOME': '/builddir', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin'} Building target platforms: i686 Building for target i686 Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.Tt9tBA + umask 022 + cd /builddir/build/BUILD + cd /builddir/build/BUILD + rm -rf cbmc-4.3-20130515svn + /usr/bin/gzip -dc /builddir/build/SOURCES/cbmc-4.3-20130515svn.tar.gz + /usr/bin/tar -xf - + STATUS=0 + '[' 0 -ne 0 ']' + cd cbmc-4.3-20130515svn + /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w . + cp /builddir/build/SOURCES/cbmc-20130515-regression.Makefile regression/Makefile Patch #0 (cbmc-20130515svn-fix-build.patch): + echo 'Patch #0 (cbmc-20130515svn-fix-build.patch):' + /usr/bin/cat /builddir/build/SOURCES/cbmc-20130515svn-fix-build.patch + /usr/bin/patch -p1 --fuzz=0 patching file src/cbmc/Makefile patching file src/common patching file src/config.inc patching file src/solvers/Makefile Patch #1 (cbmc-20130515svn-regression-test.patch): + echo 'Patch #1 (cbmc-20130515svn-regression-test.patch):' + /usr/bin/cat /builddir/build/SOURCES/cbmc-20130515svn-regression-test.patch + /usr/bin/patch -p1 --fuzz=0 patching file regression/ansi-c/Makefile patching file regression/cbmc-cpp/Makefile patching file regression/cbmc/Makefile patching file regression/cpp/Makefile Patch #2 (cbmc-20130515svn-no-long_width.patch): + echo 'Patch #2 (cbmc-20130515svn-no-long_width.patch):' + /usr/bin/cat /builddir/build/SOURCES/cbmc-20130515svn-no-long_width.patch + /usr/bin/patch -p1 --fuzz=0 patching file src/util/config.cpp + exit 0 Executing(%build): /bin/sh -e /var/tmp/rpm-tmp.UU7AWQ + umask 022 + cd /builddir/build/BUILD + cd cbmc-4.3-20130515svn + make -j5 -C src make: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src' ## Entering big-int make -C big-int make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/big-int' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -o bigint-test.o bigint-test.cc g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -o bigint-func.o bigint-func.cc g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -o bigint.o bigint.cc g++ -o test-bigint bigint-test.o bigint-func.o bigint.o make[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/big-int' ## Entering util make -C util make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/util' g++ -o irep_ids_convert irep_ids_convert.cpp ./irep_ids_convert header < irep_ids.txt > irep_ids.h ./irep_ids_convert table < irep_ids.txt > irep_ids.inc g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o arith_tools.o arith_tools.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o base_type.o base_type.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o cmdline.o cmdline.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o config.o config.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o symbol_table.o symbol_table.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o expr.o expr.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o expr_util.o expr_util.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o i2string.o i2string.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o irep.o irep.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o language.o language.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o lispexpr.o lispexpr.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o lispirep.o lispirep.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o location.o location.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o message.o message.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o language_file.o language_file.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o mp_arith.o mp_arith.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o namespace.o namespace.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o parseoptions.o parseoptions.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o rename.o rename.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o replace_expr.o replace_expr.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o threeval.o threeval.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o typecheck.o typecheck.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o graph.o graph.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o type.o type.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o cnf_simplify.o cnf_simplify.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o pointer_predicates.o pointer_predicates.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o bitvector.o bitvector.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o parser.o parser.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o map_util.o map_util.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o replace_symbol.o replace_symbol.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o actuals.o actuals.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o get_module.o get_module.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o string_hash.o string_hash.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o string_container.o string_container.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o identifier.o identifier.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o rational.o rational.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o options.o options.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o c_misc.o c_misc.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o simplify_expr.o simplify_expr.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o dstring.o dstring.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o find_symbols.o find_symbols.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o rational_tools.o rational_tools.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o ui_message.o ui_message.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o simplify_utils.o simplify_utils.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o time_stopping.o time_stopping.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o symbol.o symbol.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o irep_hash_container.o irep_hash_container.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o cout_message.o cout_message.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o type_eq.o type_eq.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o guard.o guard.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o array_name.o array_name.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o gcd.o gcd.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o message_stream.o message_stream.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o substitute.o substitute.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o decision_procedure.o decision_procedure.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o union_find.o union_find.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o pretty_names.o pretty_names.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o xml.o xml.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o xml_irep.o xml_irep.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o xml_expr.o xml_expr.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o std_types.o std_types.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o std_code.o std_code.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o format_constant.o format_constant.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o find_macros.o find_macros.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o ref_expr_set.o ref_expr_set.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o std_expr.o std_expr.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o irep_serialization.o irep_serialization.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o symbol_serialization.o symbol_serialization.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o fixedbv.o fixedbv.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o ieee_float.o ieee_float.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o signal_catcher.o signal_catcher.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o pointer_offset_size.o pointer_offset_size.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o bv_arithmetic.o bv_arithmetic.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o tempdir.o tempdir.cpp tempdir.cpp: In destructor 'temp_working_dirt::~temp_working_dirt()': tempdir.cpp:166:39: warning: ignoring return value of 'int chdir(const char*)', declared with attribute warn_unused_result [-Wunused-result] tempdir.cpp: In constructor 'temp_working_dirt::temp_working_dirt(const string&)': tempdir.cpp:149:22: warning: ignoring return value of 'int chdir(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o tempfile.o tempfile.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o timer.o timer.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o unicode.o unicode.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o irep_ids.o irep_ids.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o byte_operators.o byte_operators.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o string2int.o string2int.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o file_util.o file_util.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I . -o ieee_float_test.o ieee_float_test.cpp ld -r -o util.a arith_tools.o base_type.o cmdline.o config.o symbol_table.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 pointer_predicates.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 cout_message.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 xml_expr.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 unicode.o irep_ids.o byte_operators.o string2int.o file_util.o g++ -o ieee_float_test ieee_float_test.o util.a ../big-int/bigint.o make[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/util' ## Entering langapi ## Entering cpp ## Entering ansi-c ## Entering xmllang make -C langapi make -C cpp make -C ansi-c make -C xmllang ## Entering assembler make -C assembler make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/langapi' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o mode.o mode.cpp make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/assembler' flex -Pyyassembler -olex.yy.cpp scanner.l make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/xmllang' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o xml_language.o xml_language.cpp make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/cpp' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_id.o cpp_id.cpp scanner.l:92: warning, rule cannot be matched make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/ansi-c' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o c_typecast.o c_typecast.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o assembler_parser.o assembler_parser.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o lex.yy.o lex.yy.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o language_ui.o language_ui.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_language.o cpp_language.cpp lex.yy.cpp: In function 'yy_buffer_state* yyassembler_scan_bytes(const char*, yy_size_t)': lex.yy.cpp:1618:19: warning: comparison between signed and unsigned integer expressions [-Wsign-compare] g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o xml_parser.o xml_parser.cpp bison -y -v $flags -pyyansi_c -d parser.y -o y.tab.cpp bison -y -v $flags -pyyxml -d parser.y -o y.tab.cpp flex -Pyyxml -olex.yy.cpp scanner.l g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o xml_typecheck.o xml_typecheck.cpp ld -r -o assembler.a lex.yy.o assembler_parser.o flex -Pyyansi_c -olex.yy.cpp scanner.l make[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/assembler' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o ansi_c_parser.o ansi_c_parser.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o expr2c.o expr2c.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o languages.o languages.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o language_util.o language_util.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o expr2cpp.o expr2cpp.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -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 -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o ansi_c_language.o ansi_c_language.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o y.tab.o y.tab.cpp ld -r -o langapi.a mode.o language_ui.o languages.o language_util.o make[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/langapi' ## Entering solvers make -C solvers make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/solvers' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o sat/satcheck_minisat2.o sat/satcheck_minisat2.cpp In file included from /usr/include/minisat/core/Solver.h:27:0, from sat/satcheck_minisat2.cpp:21: /usr/include/minisat/utils/Options.h: In member function 'bool Minisat::Option::OptionLt::operator()(const Minisat::Option*, const Minisat::Option*)': /usr/include/minisat/utils/Options.h:63:84: warning: suggest parentheses around '&&' within '||' [-Wparentheses] In file included from /usr/include/minisat/core/Solver.h:24:0, from sat/satcheck_minisat2.cpp:21: /usr/include/minisat/mtl/Vec.h: In instantiation of 'void Minisat::vec::capacity(int) [with T = Minisat::Lit]': sat/satcheck_minisat2.cpp:42:26: required from here /usr/include/minisat/mtl/Vec.h:99:5: warning: suggest parentheses around '&&' within '||' [-Wparentheses] /usr/include/minisat/mtl/Vec.h: In instantiation of 'void Minisat::vec::capacity(int) [with T = Minisat::Option*]': /usr/include/minisat/mtl/Vec.h:74:57: required from 'void Minisat::vec::push(const T&) [with T = Minisat::Option*]' /usr/include/minisat/utils/Options.h:76:34: required from here /usr/include/minisat/mtl/Vec.h:99:5: warning: suggest parentheses around '&&' within '||' [-Wparentheses] /usr/include/minisat/mtl/Vec.h: In instantiation of 'void Minisat::vec::capacity(int) [with T = int]': /usr/include/minisat/mtl/Vec.h:74:57: required from 'void Minisat::vec::push(const T&) [with T = int]' /usr/include/minisat/core/Solver.h:317:94: required from here /usr/include/minisat/mtl/Vec.h:99:5: warning: suggest parentheses around '&&' within '||' [-Wparentheses] /usr/include/minisat/mtl/Vec.h: In instantiation of 'void Minisat::vec::capacity(int) [with T = Minisat::lbool]': /usr/include/minisat/mtl/Vec.h:115:5: required from 'void Minisat::vec::growTo(int) [with T = Minisat::lbool]' sat/satcheck_minisat2.cpp:268:3: required from 'void satcheck_minisat2_baset::set_assignment(literalt, bool) [with T = Minisat::SimpSolver]' sat/satcheck_minisat2.cpp:425:1: required from here /usr/include/minisat/mtl/Vec.h:99:5: warning: suggest parentheses around '&&' within '||' [-Wparentheses] g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_parser.o cpp_parser.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o lex.yy.o lex.yy.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o sat/cnf.o sat/cnf.cpp lex.yy.cpp: In function 'yy_buffer_state* yyxml_scan_bytes(const char*, yy_size_t)': lex.yy.cpp:1740:19: warning: comparison between signed and unsigned integer expressions [-Wsign-compare] flex -Pyycpp -olex.yy.cpp scanner.l g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck.o cpp_typecheck.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o c_sizeof.o c_sizeof.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[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/xmllang' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o sat/dimacs_cnf.o sat/dimacs_cnf.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o sat/cnf_clause_list.o sat/cnf_clause_list.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o sat/pbs_dimacs_cnf.o sat/pbs_dimacs_cnf.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o c_types.o c_types.cpp sat/pbs_dimacs_cnf.cpp: In member function 'bool pbs_dimacs_cnft::pbs_solve()': sat/pbs_dimacs_cnf.cpp:128:26: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o sat/read_dimacs_cnf.o sat/read_dimacs_cnf.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o sat/resolution_proof.o sat/resolution_proof.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o trans_unit.o trans_unit.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o ansi_c_typecheck.o ansi_c_typecheck.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o c_preprocess.o c_preprocess.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_convert_type.o cpp_convert_type.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o sat/satcheck.o sat/satcheck.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_expr.o cpp_typecheck_expr.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o qbf/qdimacs_cnf.o qbf/qdimacs_cnf.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_code.o cpp_typecheck_code.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o c_typecheck_base.o c_typecheck_base.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o c_typecheck_initializer.o c_typecheck_initializer.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o qbf/qbf_quantor.o qbf/qbf_quantor.cpp qbf/qbf_quantor.cpp: In member function 'virtual propt::resultt qbf_quantort::prop_solve()': qbf/qbf_quantor.cpp:123:42: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o qbf/qbf_skizzo.o qbf/qbf_skizzo.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o c_typecheck_typecast.o c_typecheck_typecast.cpp qbf/qbf_skizzo.cpp: In member function 'virtual propt::resultt qbf_skizzot::prop_solve()': qbf/qbf_skizzo.cpp:129:41: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o qbf/qdimacs_core.o qbf/qdimacs_core.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_type.o cpp_typecheck_type.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o c_typecheck_code.o c_typecheck_code.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o c_typecheck_expr.o c_typecheck_expr.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -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:129:41: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o parse.o parse.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -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:109:42: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o c_typecheck_type.o c_typecheck_type.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_parse_tree.o cpp_parse_tree.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/prop.o prop/prop.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_token_buffer.o cpp_token_buffer.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/prop_conv.o prop/prop_conv.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_fargs.o cpp_typecheck_fargs.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o string_constant.o string_constant.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/prop_conv_store.o prop/prop_conv_store.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_resolve.o cpp_typecheck_resolve.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o c_qualifiers.o c_qualifiers.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/aig_formula.o prop/aig_formula.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o c_typecheck_argc_argv.o c_typecheck_argc_argv.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/cover_goals.o prop/cover_goals.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/aig.o prop/aig.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o ansi_c_parse_tree.o ansi_c_parse_tree.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/aig_prop.o prop/aig_prop.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/minimize.o prop/minimize.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o preprocessor_line.o preprocessor_line.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o cvc/cvc_prop.o cvc/cvc_prop.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o ansi_c_convert.o ansi_c_convert.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o cvc/cvc_conv.o cvc/cvc_conv.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o cvc/cvc_dec.o cvc/cvc_dec.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_util.o cpp_util.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o ansi_c_convert_type.o ansi_c_convert_type.cpp cvc/cvc_dec.cpp: In member function 'virtual decision_proceduret::resultt cvc_dect::dec_solve()': cvc/cvc_dec.cpp:98:26: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o type2name.o type2name.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o smt1/smt1_dec.o smt1/smt1_dec.cpp g++ -o library/converter library/converter.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o anonymous_member.o anonymous_member.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o printf_formatter.o printf_formatter.cpp smt1/smt1_dec.cpp: In member function 'virtual decision_proceduret::resultt smt1_dect::dec_solve()': smt1/smt1_dec.cpp:188:26: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_enum_type.o cpp_enum_type.cpp g++ -o file_converter file_converter.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_function.o cpp_typecheck_function.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o smt1/smt1_prop.o smt1/smt1_prop.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o padding.o padding.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o ansi_c_declaration.o ansi_c_declaration.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o designator.o designator.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o literals/parse_float.o literals/parse_float.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o literals/unescape_string.o literals/unescape_string.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_namespace.o cpp_typecheck_namespace.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o smt1/smt1_conv.o smt1/smt1_conv.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o literals/convert_float_literal.o literals/convert_float_literal.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o literals/convert_character_literal.o literals/convert_character_literal.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o smt2/smt2_dec.o smt2/smt2_dec.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o literals/convert_integer_literal.o literals/convert_integer_literal.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o literals/convert_string_literal.o literals/convert_string_literal.cpp smt2/smt2_dec.cpp: In member function 'virtual decision_proceduret::resultt smt2_dect::dec_solve()': smt2/smt2_dec.cpp:172:26: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_name.o cpp_name.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_is_pod.o cpp_is_pod.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 ./file_converter < gcc_builtin_headers_generic.h > gcc_builtin_headers_generic.inc ./file_converter < gcc_builtin_headers_ia32.h > gcc_builtin_headers_ia32.inc g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_scope.o cpp_scope.cpp ./file_converter < gcc_builtin_headers_alpha.h > gcc_builtin_headers_alpha.inc ./file_converter < gcc_builtin_headers_arm.h > gcc_builtin_headers_arm.inc ./file_converter < gcc_builtin_headers_mips.h > gcc_builtin_headers_mips.inc ./file_converter < gcc_builtin_headers_power.h > gcc_builtin_headers_power.inc ./file_converter < arm_builtin_headers.h > arm_builtin_headers.inc ./file_converter < cw_builtin_headers.h > cw_builtin_headers.inc g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o y.tab.o y.tab.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o lex.yy.o lex.yy.cpp lex.yy.cpp: In function 'yy_buffer_state* yyansi_c_scan_bytes(const char*, yy_size_t)': lex.yy.cpp:5719:19: warning: comparison between signed and unsigned integer expressions [-Wsign-compare] g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o smt2/smt2_prop.o smt2/smt2_prop.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_find_constructor.o cpp_typecheck_find_constructor.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cprover_library.o cprover_library.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o smt2/smt2_conv.o smt2/smt2_conv.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o template_map.o template_map.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o internal_additions.o internal_additions.cpp ## Entering goto-symex make -C goto-symex make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/goto-symex' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o symex_target.o symex_target.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o dplib/dplib_conv.o dplib/dplib_conv.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_scopes.o cpp_scopes.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o symex_target_equation.o symex_target_equation.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_declarator.o cpp_declarator.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_types.o trans_unit.o ansi_c_typecheck.o c_preprocess.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 padding.o ansi_c_declaration.o designator.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[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/ansi-c' ## Entering analyses make -C analyses make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/analyses' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cfg_dominators.o cfg_dominators.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_instantiate_template.o cpp_instantiate_template.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o dplib/dplib_dec.o dplib/dplib_dec.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o natural_loops.o natural_loops.cpp dplib/dplib_dec.cpp: In member function 'virtual decision_proceduret::resultt dplib_dect::dec_solve()': dplib/dplib_dec.cpp:98:26: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result] g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_symex.o goto_symex.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o dplib/dplib_prop.o dplib/dplib_prop.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o internal_additions.o internal_additions.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/equality.o flattening/equality.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_type2name.o cpp_type2name.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o is_threaded.o is_threaded.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o symex_main.o symex_main.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_trace.o goto_trace.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_linkage_spec.o cpp_typecheck_linkage_spec.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o invariant_set.o invariant_set.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/arrays.o flattening/arrays.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_template.o cpp_typecheck_template.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/functions.o flattening/functions.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o build_goto_trace.o build_goto_trace.cpp ## Entering pointer-analysis make -C pointer-analysis make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/pointer-analysis' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o value_set.o value_set.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o symex_function_call.o symex_function_call.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_function_bodies.o cpp_typecheck_function_bodies.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o invariant_set_domain.o invariant_set_domain.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/bv_minimize.o flattening/bv_minimize.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o invariant_propagation.o invariant_propagation.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_initializer.o cpp_typecheck_initializer.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_width.o flattening/boolbv_width.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv.o flattening/boolbv.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_compound_type.o cpp_typecheck_compound_type.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_program_dereference.o goto_program_dereference.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o static_analysis.o static_analysis.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_symex_state.o goto_symex_state.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o uninitialized_domain.o uninitialized_domain.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o value_set_analysis.o value_set_analysis.cpp ld -r -o analyses.a cfg_dominators.o natural_loops.o is_threaded.o invariant_set.o invariant_set_domain.o invariant_propagation.o static_analysis.o uninitialized_domain.o make[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/analyses' ## Entering goto-programs make -C goto-programs make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/goto-programs' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_convert.o goto_convert.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_constraint_select_one.o flattening/boolbv_constraint_select_one.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/bv_pointers.o flattening/bv_pointers.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o dereference.o dereference.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_constructor.o cpp_constructor.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o symex_dereference.o symex_dereference.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o symex_goto.o symex_goto.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_destructor.o cpp_destructor.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o pointer_offset_sum.o pointer_offset_sum.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_convert_function_call.o goto_convert_function_call.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o add_failed_symbols.o add_failed_symbols.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/bv_utils.o flattening/bv_utils.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o show_value_sets.o show_value_sets.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_conversions.o cpp_typecheck_conversions.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o builtin_functions.o builtin_functions.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o value_set_domain.o value_set_domain.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_convert_side_effect.o goto_convert_side_effect.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_abs.o flattening/boolbv_abs.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o rewrite_index.o rewrite_index.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_with.o flattening/boolbv_with.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o value_set_analysis_fi.o value_set_analysis_fi.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o slice.o slice.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_typecast.o flattening/boolbv_typecast.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_program.o goto_program.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_declaration.o cpp_typecheck_declaration.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o symex_other.o symex_other.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o value_set_fi.o value_set_fi.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o basic_blocks.o basic_blocks.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o slice_by_trace.o slice_by_trace.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_check.o goto_check.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_index.o flattening/boolbv_index.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_declarator_converter.o cpp_declarator_converter.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_member.o flattening/boolbv_member.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_declaration.o cpp_declaration.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_if.o flattening/boolbv_if.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_namespace_spec.o cpp_namespace_spec.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o value_set_domain_fi.o value_set_domain_fi.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_using.o cpp_typecheck_using.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_byte_extract.o flattening/boolbv_byte_extract.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o xml_goto_trace.o xml_goto_trace.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o remove_function_pointers.o remove_function_pointers.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o value_set_analysis_fivr.o value_set_analysis_fivr.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_exception_id.o cpp_exception_id.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_add_sub.o flattening/boolbv_add_sub.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_enum_type.o cpp_typecheck_enum_type.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o symex_decl.o symex_decl.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_functions.o goto_functions.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_mult.o flattening/boolbv_mult.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o value_set_fivr.o value_set_fivr.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_inline.o goto_inline.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_bases.o cpp_typecheck_bases.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_constant.o flattening/boolbv_constant.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o precondition.o precondition.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_extractbit.o flattening/boolbv_extractbit.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_constructor.o cpp_typecheck_constructor.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o postcondition.o postcondition.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_bv_rel.o flattening/boolbv_bv_rel.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o symex_clean_expr.o symex_clean_expr.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o remove_skip.o remove_skip.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_shift.o flattening/boolbv_shift.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o symex_dereference_state.o symex_dereference_state.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_convert_functions.o goto_convert_functions.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o value_set_domain_fivr.o value_set_domain_fivr.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_virtual_table.o cpp_typecheck_virtual_table.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o vcd_goto_trace.o vcd_goto_trace.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_case.o flattening/boolbv_case.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o value_set_analysis_fivrns.o value_set_analysis_fivrns.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o cpp_typecheck_static_assert.o cpp_typecheck_static_assert.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o auto_objects.o auto_objects.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_cond.o flattening/boolbv_cond.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o string_instrumentation.o string_instrumentation.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o lex.yy.o lex.yy.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o value_set_fivrns.o value_set_fivrns.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_concatenation.o flattening/boolbv_concatenation.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o symex_catch.o symex_catch.cpp lex.yy.cpp: In function 'yy_buffer_state* yycpp_scan_bytes(const char*, yy_size_t)': lex.yy.cpp:3775:19: warning: comparison between signed and unsigned integer expressions [-Wsign-compare] g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_div.o flattening/boolbv_div.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o symex_start_thread.o symex_start_thread.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_enum_type.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_typecheck_conversions.o cpp_typecheck_declaration.o cpp_declarator_converter.o cpp_declaration.o cpp_namespace_spec.o cpp_typecheck_using.o cpp_exception_id.o cpp_typecheck_enum_type.o cpp_typecheck_bases.o cpp_typecheck_constructor.o cpp_typecheck_virtual_table.o cpp_typecheck_static_assert.o make[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/cpp' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o value_set_domain_fivrns.o value_set_domain_fivrns.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_mod.o flattening/boolbv_mod.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o builtin_functions.o builtin_functions.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o show_claims.o show_claims.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_extractbits.o flattening/boolbv_extractbits.cpp ld -r -o pointer-analysis.a value_set.o goto_program_dereference.o value_set_analysis.o dereference.o pointer_offset_sum.o add_failed_symbols.o show_value_sets.o value_set_domain.o rewrite_index.o value_set_analysis_fi.o value_set_fi.o value_set_domain_fi.o value_set_analysis_fivr.o value_set_fivr.o value_set_domain_fivr.o value_set_analysis_fivrns.o value_set_fivrns.o value_set_domain_fivrns.o make[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/pointer-analysis' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_replication.o flattening/boolbv_replication.cpp ## Entering linking make -C linking make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/linking' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o linking.o linking.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o symex_assign.o symex_assign.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_reduction.o flattening/boolbv_reduction.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_overflow.o flattening/boolbv_overflow.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_get.o flattening/boolbv_get.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_bitwise.o flattening/boolbv_bitwise.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o linking_type_eq.o linking_type_eq.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o destructor.o destructor.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o symex_throw.o symex_throw.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o zero_initializer.o zero_initializer.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o set_claims.o set_claims.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o reachability_slicer.o reachability_slicer.cpp ld -r -o goto-symex.a symex_target.o symex_target_equation.o goto_symex.o symex_main.o goto_trace.o build_goto_trace.o symex_function_call.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 symex_catch.o symex_start_thread.o symex_assign.o symex_throw.o make[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/goto-symex' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o remove_internal_symbols.o remove_internal_symbols.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o entry_point.o entry_point.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o read_goto_binary.o read_goto_binary.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_equality.o flattening/boolbv_equality.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_asm.o goto_asm.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o elf_reader.o elf_reader.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o string_abstraction.o string_abstraction.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_unary_minus.o flattening/boolbv_unary_minus.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_program_serialization.o goto_program_serialization.cpp ld -r -o linking.a linking.o linking_type_eq.o zero_initializer.o remove_internal_symbols.o entry_point.o make[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/linking' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_ieee_float_rel.o flattening/boolbv_ieee_float_rel.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_function_serialization.o goto_function_serialization.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/pointer_logic.o flattening/pointer_logic.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o read_bin_goto_object.o read_bin_goto_object.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_quantifier.o flattening/boolbv_quantifier.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_program_irep.o goto_program_irep.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_struct.o flattening/boolbv_struct.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_byte_update.o flattening/boolbv_byte_update.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o interpreter.o interpreter.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_array_of.o flattening/boolbv_array_of.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o interpreter_evaluate.o interpreter_evaluate.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_map.o flattening/boolbv_map.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_type.o flattening/boolbv_type.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o flow_insensitive_analysis.o flow_insensitive_analysis.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_array.o flattening/boolbv_array.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_vector.o flattening/boolbv_vector.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o format_strings.o format_strings.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_complex.o flattening/boolbv_complex.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o loop_ids.o loop_ids.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o pointer_arithmetic.o pointer_arithmetic.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_program_template.o goto_program_template.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o write_goto_binary.o write_goto_binary.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o remove_unreachable.o remove_unreachable.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o remove_unused_functions.o remove_unused_functions.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_floatbv_op.o flattening/boolbv_floatbv_op.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o wp.o wp.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_rw.o goto_rw.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o goto_clean_expr.o goto_clean_expr.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o safety_checker.o safety_checker.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o compute_called_functions.o compute_called_functions.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o link_to_library.o link_to_library.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_union.o flattening/boolbv_union.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -o remove_return_values.o remove_return_values.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/flatten_byte_operators.o flattening/flatten_byte_operators.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -I /usr/include/minisat -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o floatbv/float_utils.o floatbv/float_utils.cpp ld -r -o goto-programs.a goto_convert.o goto_convert_function_call.o goto_convert_side_effect.o goto_program.o basic_blocks.o goto_check.o remove_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 reachability_slicer.o read_goto_binary.o goto_asm.o elf_reader.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_ids.o pointer_arithmetic.o goto_program_template.o write_goto_binary.o remove_unreachable.o remove_unused_functions.o wp.o goto_rw.o goto_clean_expr.o safety_checker.o compute_called_functions.o link_to_library.o remove_return_values.o ld -r -o solvers.a sat/satcheck_minisat2.o sat/cnf.o sat/dimacs_cnf.o sat/cnf_clause_list.o sat/pbs_dimacs_cnf.o sat/read_dimacs_cnf.o sat/resolution_proof.o sat/satcheck.o qbf/qdimacs_cnf.o qbf/qbf_quantor.o qbf/qbf_skizzo.o qbf/qdimacs_core.o qbf/qbf_qube.o qbf/qbf_qube_core.o prop/prop.o prop/prop_conv.o prop/prop_conv_store.o prop/aig_formula.o prop/cover_goals.o prop/aig.o prop/aig_prop.o prop/minimize.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/bv_minimize.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_array.o flattening/boolbv_vector.o flattening/boolbv_complex.o flattening/boolbv_floatbv_op.o flattening/boolbv_union.o flattening/flatten_byte_operators.o floatbv/float_utils.o make[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/goto-programs' ## Entering goto-cc ## Entering goto-instrument make -C goto-cc make -C goto-instrument make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/goto-cc' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -D HAVE_CPP -o goto-cc.o goto-cc.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -D HAVE_CPP -o goto_cc_mode.o goto_cc_mode.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -D HAVE_CPP -o gcc_mode.o gcc_mode.cpp make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/goto-instrument' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o main.o main.cpp make[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/solvers' ## Entering cbmc make -C cbmc make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/cbmc' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o main.o main.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -D HAVE_CPP -o get_base_name.o get_base_name.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o parseoptions.o parseoptions.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o parseoptions.o parseoptions.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o document_claims.o document_claims.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -D HAVE_CPP -o gcc_cmdline.o gcc_cmdline.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -D HAVE_CPP -o ms_cl_cmdline.o ms_cl_cmdline.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -D HAVE_CPP -o compile.o compile.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o languages.o languages.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -D HAVE_CPP -o armcc_cmdline.o armcc_cmdline.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o uninitialized.o uninitialized.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -D HAVE_CPP -o run.o run.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -D HAVE_CPP -o languages.o languages.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o bmc.o bmc.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o full_slicer.o full_slicer.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -D HAVE_CPP -o goto_cc_cmdline.o goto_cc_cmdline.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -D HAVE_CPP -o ms_cl_mode.o ms_cl_mode.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o object_id.o object_id.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -D HAVE_CPP -o armcc_mode.o armcc_mode.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -D HAVE_CPP -o cw_mode.o cw_mode.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o show_locations.o show_locations.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o points_to.o points_to.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o alignment_checks.o alignment_checks.cpp g++ -o goto-cc ../big-int/bigint.o ../goto-programs/goto-programs.a ../util/util.a ../linking/linking.a ../ansi-c/ansi-c.a ../xmllang/xmllang.a ../assembler/assembler.a ../langapi/langapi.a goto-cc.o goto_cc_mode.o gcc_mode.o get_base_name.o gcc_cmdline.o ms_cl_cmdline.o compile.o armcc_cmdline.o run.o languages.o goto_cc_cmdline.o ms_cl_mode.o armcc_mode.o cw_mode.o ../cpp/cpp.a g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o race_check.o race_check.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o rw_set.o rw_set.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o nondet_volatile.o nondet_volatile.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o dimacs.o dimacs.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o interrupt.o interrupt.cpp make[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/goto-cc' g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o mmio.o mmio.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o stack_depth.o stack_depth.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o nondet_static.o nondet_static.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o concurrency.o concurrency.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o dump_c.o dump_c.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o languages.o languages.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o dot.o dot.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o wmm/weak_memory.o wmm/weak_memory.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o bv_cbmc.o bv_cbmc.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o wmm/fence.o wmm/fence.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o wmm/event_graph.o wmm/event_graph.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o wmm/goto2graph.o wmm/goto2graph.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o symex_bmc.o symex_bmc.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o show_vcc.o show_vcc.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o wmm/data_dp.o wmm/data_dp.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o wmm/abstract_event.o wmm/abstract_event.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o wmm/instrumenter_strategies.o wmm/instrumenter_strategies.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o wmm/cycle_collection.o wmm/cycle_collection.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o cbmc_solvers.o cbmc_solvers.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o xml_interface.o xml_interface.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o cover.o cover.cpp g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector --param=ssp-buffer-size=4 -m32 -march=i686 -mtune=atom -fasynchronous-unwind-tables -I .. -I ../util -DHAVE_CPP -o counterexample_beautification.o counterexample_beautification.cpp g++ -o goto-instrument ../ansi-c/ansi-c.a ../linking/linking.a ../big-int/bigint.o ../goto-programs/goto-programs.a ../goto-symex/goto-symex.a ../assembler/assembler.a ../pointer-analysis/pointer-analysis.a ../analyses/analyses.a ../langapi/langapi.a ../util/util.a main.o parseoptions.o document_claims.o languages.o uninitialized.o full_slicer.o object_id.o show_locations.o points_to.o alignment_checks.o race_check.o rw_set.o nondet_volatile.o interrupt.o mmio.o stack_depth.o nondet_static.o concurrency.o dump_c.o dot.o wmm/weak_memory.o wmm/fence.o wmm/event_graph.o wmm/goto2graph.o wmm/data_dp.o wmm/abstract_event.o wmm/instrumenter_strategies.o wmm/cycle_collection.o ../cpp/cpp.a g++ -o cbmc ../ansi-c/ansi-c.a ../linking/linking.a ../big-int/bigint.o ../goto-programs/goto-programs.a ../goto-symex/goto-symex.a ../pointer-analysis/value_set.o ../pointer-analysis/dereference.o ../pointer-analysis/add_failed_symbols.o ../pointer-analysis/rewrite_index.o ../pointer-analysis/goto_program_dereference.o ../langapi/langapi.a ../xmllang/xmllang.a ../assembler/assembler.a ../solvers/solvers.a ../util/util.a 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 cover.o counterexample_beautification.o ../cpp/cpp.a -lminisat make[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/goto-instrument' make[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src/cbmc' make: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/src' + exit 0 Executing(%install): /bin/sh -e /var/tmp/rpm-tmp.fD1koh + umask 022 + cd /builddir/build/BUILD + '[' /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386 '!=' / ']' + rm -rf /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386 ++ dirname /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386 + mkdir -p /builddir/build/BUILDROOT + mkdir /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386 + cd cbmc-4.3-20130515svn + mkdir -p /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386/usr/bin /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386/usr/share/doc/cbmc-4.3/cbmc-4.3 /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386/usr/share/man/man1 + install -p src/cbmc/cbmc /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386/usr/bin + install -p src/goto-cc/goto-cc /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386/usr/bin + install -p src/goto-instrument/goto-instrument /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386/usr/bin + cp -pr doc/html-manual /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386/usr/share/doc/cbmc-4.3/cbmc-4.3 + install -p doc/man/cbmc.1 /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386/usr/share/man/man1 + /usr/lib/rpm/find-debuginfo.sh --strict-build-id -m --run-dwz --dwz-low-mem-die-limit 10000000 --dwz-max-die-limit 50000000 /builddir/build/BUILD/cbmc-4.3-20130515svn extracting debug info from /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386/usr/bin/goto-instrument extracting debug info from /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386/usr/bin/cbmc extracting debug info from /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386/usr/bin/goto-cc cpio: cbmc-4.3-20130515svn/src/xmllang/y.tab.hpp: Cannot stat: No such file or directory 10472 blocks + /usr/lib/rpm/check-buildroot + /usr/lib/rpm/redhat/brp-compress + /usr/lib/rpm/redhat/brp-strip-static-archive /usr/bin/strip + /usr/lib/rpm/brp-python-bytecompile /usr/bin/python 1 + /usr/lib/rpm/redhat/brp-python-hardlink + /usr/lib/rpm/redhat/brp-java-repack-jars Executing(%check): /bin/sh -e /var/tmp/rpm-tmp.kGp9pK + umask 022 + cd /builddir/build/BUILD + cd cbmc-4.3-20130515svn + cd regression + make make -C ansi-c test; make -C cbmc test; make -C cpp test; make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/regression/ansi-c' Loading 51 tests found Running tests Running Assignment_to_typecast1 [OK] Running Builtins1 [OK] Running Defines1 [OK] Running Empty_Declaration1 [OK] Running Forward_Declaration1 [OK] Running Forward_Declaration2 [OK] Running Incomplete_Type1 [OK] Running Initializer_cast1 [OK] Running Lvalue1 [OK] Running MMX1 [OK] Running MMX2 [OK] Running Multiple [OK] Running Qualifiers1 [OK] Running Recursive_Structure1 [OK] Running Struct_Hierarchy1 [OK] Running Struct_Padding2 [OK] Running Struct_Padding3 [OK] Running Struct_Padding4 [OK] Running Struct_Padding5 [OK] Running Transparent_union1 [OK] Running Typecast_to_union1 [OK] Running Union_Initialization1 [OK] Running _Alignof1 [OK] Running _Bool1 [OK] Running _Generic1 [OK] Running _Static_assert1 [OK] Running arithmetic_right_shift1 [OK] Running asm1 [OK] Running asm2 [OK] Running character_literals1 [OK] Running envp1 [OK] Running extern1 [OK] Running extern2 [OK] Running float_constant1 [OK] Running for_scope1 [OK] Running gcc_attributes1 [SKIPPED] Running gcc_attributes2 [SKIPPED] Running gcc_types_compatible_p1 [OK] Running integer_constant1 [OK] Running integer_constant2 [OK] Running return_void [OK] Running sizeof1 [OK] Running sizeof2 [OK] Running struct2 [OK] Running struct5 [OK] Running typedef1 [OK] Running typedef_code [OK] Running windows_h_VS_2005 [OK] Running windows_h_VS_2008 [OK] Running windows_h_VS_2010 [OK] Running windows_h_VS_2012 [OK] All tests were successful, 2 tests skipped make[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/regression/ansi-c' make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/regression/cbmc' Loading 214 tests found Running tests Running ASHR1 [OK] Running Address_of1 [OK] Running Anonymous_Struct1 [OK] Running Anonymous_Struct2 [OK] Running Anonymous_Struct3 [OK] Running Array_Initialization1 [OK] Running Array_Initialization2 [OK] Running Array_Initialization3 [OK] Running BV_Arithmetic1 [OK] Running BV_Arithmetic2 [OK] Running BV_Arithmetic3 [OK] Running BV_Arithmetic4 [OK] Running BV_Arithmetic5 [OK] Running BV_Arithmetic6 [OK] Running Bitfields1 [OK] Running Bool1 [OK] Running Boolean_Guards1 [OK] Running Computed-Goto1 [OK] Running Division1 [OK] Running Division2 [OK] Running Ellipsis1 [OK] Running Endianness1 [OK] Running Endianness2 [OK] Running Endianness3 [OK] Running Endianness4 [OK] Running Endianness5 [OK] Running Endianness6 [OK] Running Error_Label1 [OK] Running Failing_Assert1 [OK] Running Fixedbv1 [OK] Running Fixedbv2 [OK] Running Fixedbv3 [OK] Running Fixedbv4 [OK] Running Fixedbv5 [OK] Running Fixedbv6 [OK] Running Fixedbv7 [OK] Running Float-Rounding1 [SKIPPED] Running Float-flags-no-simp1 [OK] Running Float-flags-simp1 [OK] Running Float-no-simp1 [OK] Running Float-no-simp2 [OK] Running Float-no-simp3 [OK] Running Float-no-simp4 [OK] Running Float-no-simp5 [OK] Running Float1 [OK] Running Float11 [OK] Running Float12 [OK] Running Float13 [OK] Running Float14 [OK] Running Float18 [OK] Running Float2 [OK] Running Float3 [OK] Running Float4 [OK] Running Float5 [OK] Running Float6 [OK] Running Float7 [OK] Running Float8 [OK] Running Float_lib1 [OK] Running Free1 [OK] Running Free2 [OK] Running Free3 [OK] Running Free4 [OK] Running Function-KnR1 [OK] Running Function1 [OK] Running Function10 [OK] Running Function11 [OK] Running Function12 [OK] Running Function2 [OK] Running Function3 [OK] Running Function4 [OK] Running Function5 [OK] Running Function6 [OK] Running Function7 [OK] Running Function8 [OK] Running Function9 [OK] Running Function_Pointer1 [OK] Running Function_Pointer10 [OK] Running Function_Pointer11 [OK] Running Function_Pointer12 [OK] Running Function_Pointer13 [OK] Running Function_Pointer14 [OK] Running Function_Pointer15 [OK] Running Function_Pointer2 [OK] Running Function_Pointer3 [OK] Running Function_Pointer4 [OK] Running Function_Pointer5 [OK] Running Function_Pointer6 [OK] Running Function_Pointer7 [OK] Running Function_Pointer8 [OK] Running Function_Pointer9 [OK] Running Global_Initialization1 [OK] Running Initialization1 [OK] Running Initialization2 [OK] Running Linking1 [OK] Running Linking2 [OK] Running Linking3 [OK] Running Linking4 [OK] Running Mod1 [OK] Running Mod2 [OK] Running Multi_Dimensional_Array1 [OK] Running Multi_Dimensional_Array2 [OK] Running Multi_Dimensional_Array3 [OK] Running Multi_Dimensional_Array4 [OK] Running Multi_Dimensional_Array5 [OK] Running Negation1 [OK] Running Overflow_Addition1 [OK] Running Overflow_Multiplication1 [OK] Running Pointer_Arithmetic1 [OK] Running Pointer_Arithmetic10 [OK] Running Pointer_Arithmetic11 [OK] Running Pointer_Arithmetic2 [OK] Running Pointer_Arithmetic3 [OK] Running Pointer_Arithmetic4 [OK] Running Pointer_Arithmetic5 [OK] Running Pointer_Arithmetic6 [OK] Running Pointer_Arithmetic7 [OK] Running Pointer_Arithmetic8 [OK] Running Pointer_Arithmetic9 [OK] Running Pointer_difference1 [OK] Running Promotion1 [OK] Running Promotion2 [OK] Running Recursion1 [OK] Running Recursion2 [OK] Running Recursion3 [OK] Running Recursion4 [OK] Running Sideeffects1 [OK] Running Sideeffects2 [OK] Running Sideeffects3 [OK] Running Sideeffects4 [OK] Running Static2 [OK] Running Static_Functions1 [OK] Running String1 [OK] Running String2 [OK] Running String3 [SKIPPED] Running String4 [OK] Running String5 [OK] Running String6 [OK] Running String7 [OK] Running String_Literal1 [OK] Running Struct_Bytewise1 [OK] Running Struct_Bytewise2 [OK] Running Struct_Initialization1 [OK] Running Struct_Initialization10 [OK] Running Struct_Initialization2 [OK] Running Struct_Initialization3 [OK] Running Struct_Initialization4 [OK] Running Struct_Initialization5 [OK] Running Struct_Initialization6 [OK] Running Struct_Initialization7 [OK] Running Struct_Initialization8 [SKIPPED] Running Struct_Initialization9 [OK] Running Struct_Padding1 [OK] Running Typecast1 [OK] Running Undefined_Function1 [OK] Running Unwinding_Locality1 [OK] Running Visual_Studio_Types1 [OK] Running Visual_Studio_Types2 [OK] Running Zero_Initialization1 [OK] Running __func__1 [OK] Running abs1 [OK] Running argv1 [OK] Running character_handling1 [OK] Running complex1 [OK] Running const_ptr1 [OK] Running enum1 [OK] Running enum2 [OK] Running enum3 [OK] Running exit1 [OK] Running for-break1 [OK] Running for1 [OK] Running for2 [OK] Running for3 [OK] Running function_option1 [OK] Running gcc_conditional_expr1 [OK] Running gcc_local_label1 [OK] Running gcc_statement_expression1 [OK] Running gcc_statement_expression2 [OK] Running gcc_statement_expression3 [OK] Running gcc_vector1 [OK] Running goto1 [OK] Running goto2 [OK] Running goto3 [OK] Running goto4 [OK] Running if1 [OK] Running if2 [OK] Running if3 [OK] Running if4 [OK] Running inline1 [OK] Running offsetof1 [OK] Running return1 [OK] Running return3 [OK] Running return4 [OK] Running return5 [OK] Running struct1 [OK] Running struct3 [OK] Running struct4 [OK] Running struct6 [OK] Running struct7 [OK] Running struct8 [OK] Running switch1 [OK] Running switch2 [OK] Running switch3 [OK] Running switch4 [OK] Running switch5 [OK] Running switch6 [OK] Running union1 [OK] Running union2 [OK] Running union3 [OK] Running union4 [OK] Running unsigned_char1 [OK] Running va_list1 [OK] Running va_list2 [SKIPPED] Running void_ifthenelse [OK] Running while1 [OK] All tests were successful, 4 tests skipped make[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/regression/cbmc' make[1]: Entering directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/regression/cpp' Loading 46 tests found Running tests Running Address_of_Method2 [OK] Running Address_of_Method3 [OK] Running Constant1 [OK] Running Constant2 [OK] Running Constant3 [OK] Running Constant4 [OK] Running Friend2 [OK] Running Function_Bodies1 [OK] Running Function_Overloading1 [OK] Running Function_Overloading2 [OK] Running Method_qualifier1 [OK] Running ModeC1 [OK] Running ModeC2 [OK] Running Pointer_Conversion1 [OK] Running Resolver1 [OK] Running Resolver10 [OK] Running Resolver11 [OK] Running Resolver12 [OK] Running Resolver2 [OK] Running Resolver3 [OK] Running Resolver4 [OK] Running Scope1 [OK] Running Templates1 [OK] Running Templates2 [OK] Running Templates7 [OK] Running bitwise_and1 [OK] Running enum1 [OK] Running enum2 [OK] Running enum3 [SKIPPED] Running enum4 [OK] Running enum5 [SKIPPED] Running enum6 [OK] Running lvalue1 [OK] Running namespace4 [OK] Running sizeof1 [OK] Running sizeof2 [OK] Running static_assert1 [OK] Running typecast_ambiguity1 [OK] Running typecast_ambiguity2 [OK] Running union3 [OK] Running union4 [OK] Running union5 [OK] Running windows_h_VS_2005 [OK] Running windows_h_VS_2008 [OK] Running windows_h_VS_2010 [OK] Running windows_h_VS_2012 [OK] All tests were successful, 2 tests skipped make[1]: Leaving directory `/builddir/build/BUILD/cbmc-4.3-20130515svn/regression/cpp' + exit 0 Processing files: cbmc-4.3-7.20130515svn.fc18.i686 Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.pwfMtr + umask 022 + cd /builddir/build/BUILD + cd cbmc-4.3-20130515svn + DOCDIR=/builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386/usr/share/doc/cbmc-4.3 + export DOCDIR + /usr/bin/mkdir -p /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386/usr/share/doc/cbmc-4.3 + cp -pr CHANGELOG CODING_STANDARD LICENSE /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386/usr/share/doc/cbmc-4.3 + exit 0 Provides: cbmc = 4.3-7.20130515svn.fc18 cbmc(x86-32) = 4.3-7.20130515svn.fc18 Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Requires: libc.so.6 libc.so.6(GLIBC_2.0) libc.so.6(GLIBC_2.1) libc.so.6(GLIBC_2.1.3) libc.so.6(GLIBC_2.2) libc.so.6(GLIBC_2.3) libc.so.6(GLIBC_2.3.4) libc.so.6(GLIBC_2.4) libgcc_s.so.1 libgcc_s.so.1(GCC_3.0) libgcc_s.so.1(GLIBC_2.0) libm.so.6 libm.so.6(GLIBC_2.0) libminisat.so.2 libstdc++.so.6 libstdc++.so.6(CXXABI_1.3) libstdc++.so.6(CXXABI_1.3.1) libstdc++.so.6(GLIBCXX_3.4) libstdc++.so.6(GLIBCXX_3.4.10) libstdc++.so.6(GLIBCXX_3.4.11) libstdc++.so.6(GLIBCXX_3.4.15) libstdc++.so.6(GLIBCXX_3.4.9) rtld(GNU_HASH) Processing files: cbmc-debuginfo-4.3-7.20130515svn.fc18.i686 Provides: cbmc-debuginfo = 4.3-7.20130515svn.fc18 cbmc-debuginfo(x86-32) = 4.3-7.20130515svn.fc18 Requires(rpmlib): rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 rpmlib(CompressedFileNames) <= 3.0.4-1 Checking for unpackaged file(s): /usr/lib/rpm/check-files /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386 Wrote: /builddir/build/RPMS/cbmc-4.3-7.20130515svn.fc18.i686.rpm Wrote: /builddir/build/RPMS/cbmc-debuginfo-4.3-7.20130515svn.fc18.i686.rpm Executing(%clean): /bin/sh -e /var/tmp/rpm-tmp.JSyhJl + umask 022 + cd /builddir/build/BUILD + cd cbmc-4.3-20130515svn + /usr/bin/rm -rf /builddir/build/BUILDROOT/cbmc-4.3-7.20130515svn.fc18.i386 + exit 0 Child return code was: 0 LEAVE do -->