Your message dated Wed, 10 Jul 2013 13:48:05 +0000
with message-id <e1uwukx-0003ci...@franck.debian.org>
and subject line Bug#701253: fixed in cbmc 4.4-1
has caused the Debian Bug report #701253,
regarding cbmc: ftbfs with GCC-4.8
to be marked as done.
This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.
(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact ow...@bugs.debian.org
immediately.)
--
701253: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=701253
Debian Bug Tracking System
Contact ow...@bugs.debian.org with problems
--- Begin Message ---
Package: src:cbmc
Version: 4.3-6
Severity: important
Tags: sid jessie
User: debian-...@lists.debian.org
Usertags: ftbfs-gcc-4.8
The package fails to build in a test rebuild on at least amd64 with
gcc-4.8/g++-4.8, but succeeds to build with gcc-4.7/g++-4.7. The
severity of this report may be raised before the jessie release.
wmm/cycle_collection.cpp:79:24: error: 'order' may be used uninitialized in
this function [-Werror=maybe-uninitialized]
The full build log can be found at:
http://people.debian.org/~doko/logs-20130217/gcc48/cbmc_4.3-6_unstable_gcc48.log
The last lines of the build log are at the end of this report.
To build with GCC 4.8, either set CC=gcc-4.8 CXX=g++-4.8 explicitly,
or install the gcc, g++, gfortran, ... packages from experimental.
apt-get -t experimental install g++ g++-4.7 g++-4.8 libc6-dev
The test rebuild was done with eglibc-2.17 and GCC-4.8, so some issues
might be caused by the updated glibc.
[...]
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o wmm/fence.o wmm/fence.cpp
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o wmm/event_graph.o wmm/event_graph.cpp
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o wmm/goto2graph.o wmm/goto2graph.cpp
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o wmm/data_dp.o wmm/data_dp.cpp
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o wmm/abstract_event.o
wmm/abstract_event.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 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o wmm/instrumenter_strategies.o
wmm/instrumenter_strategies.cpp
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o wmm/cycle_collection.o
wmm/cycle_collection.cpp
ld -r -o solvers.a sat/satcheck_minisat2.o sat/cnf.o sat/dimacs_cnf.o
sat/cnf_clause_list.o sat/pbs_dimacs_cnf.o sat/read_dimacs_cnf.o
sat/resolution_proof.o sat/satcheck.o qbf/qdimacs_cnf.o qbf/qbf_quantor.o
qbf/qbf_skizzo.o qbf/qdimacs_core.o qbf/qbf_qube.o qbf/qbf_qube_core.o
prop/prop.o prop/prop_conv.o prop/prop_conv_store.o prop/aig_formula.o
prop/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_ut
ils.o
make[3]: Leaving directory `/«PKGBUILDDIR»/src/goto-cc'
make[3]: Leaving directory `/«PKGBUILDDIR»/src/solvers'
## Entering cbmc
make -C cbmc
make[3]: Entering directory `/«PKGBUILDDIR»/src/cbmc'
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o main.o main.cpp
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o parseoptions.o parseoptions.cpp
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o bmc.o bmc.cpp
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o dimacs.o dimacs.cpp
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o languages.o languages.cpp
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o bv_cbmc.o bv_cbmc.cpp
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o symex_bmc.o symex_bmc.cpp
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o show_vcc.o show_vcc.cpp
wmm/cycle_collection.cpp: In member function 'void
event_grapht::graph_explorert::collect_cycles(std::set<event_grapht::critical_cyclet>&,
weak_memory_modelt)':
wmm/cycle_collection.cpp:79:24: error: 'order' may be used uninitialized in
this function [-Werror=maybe-uninitialized]
std::list<unsigned>* order;
^
cc1plus: all warnings being treated as errors
make[3]: *** [wmm/cycle_collection.o] Error 1
make[3]: *** Waiting for unfinished jobs....
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o cbmc_solvers.o cbmc_solvers.cpp
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o xml_interface.o xml_interface.cpp
wmm/goto2graph.cpp: In member function 'bool
instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet&)':
wmm/goto2graph.cpp:935:20: error: 'current_po' may be used uninitialized in
this function [-Werror=maybe-uninitialized]
goto_programt* current_po;
^
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o cover.o cover.cpp
g++ -c -MMD -MP -DSTL_HASH_TR1 -g -O2 -fstack-protector
--param=ssp-buffer-size=4 -Wformat -Werror=format-security -Wall -O2 -g -Werror
-Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing
-pedantic -I .. -I ../util -DHAVE_CPP -o counterexample_beautification.o
counterexample_beautification.cpp
cc1plus: all warnings being treated as errors
make[3]: *** [wmm/goto2graph.o] Error 1
make[2]: *** [goto-instrument.dir] Error 2
make[3]: Leaving directory `/«PKGBUILDDIR»/src/goto-instrument'
make[2]: *** Waiting for unfinished jobs....
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[3]: Leaving directory `/«PKGBUILDDIR»/src/cbmc'
make[1]: *** [all] Error 2
dh_auto_build: make -j10 returned exit code 2
make[2]: Leaving directory `/«PKGBUILDDIR»/src'
make[1]: Leaving directory `/«PKGBUILDDIR»'
make: *** [build-arch] Error 2
dpkg-buildpackage: error: debian/rules build-arch gave error exit status 2
--- End Message ---
--- Begin Message ---
Source: cbmc
Source-Version: 4.4-1
We believe that the bug you reported is fixed in the latest version of
cbmc, which is due to be installed in the Debian FTP archive.
A summary of the changes between this version and the previous one is
attached.
Thank you for reporting the bug, which will now be closed. If you
have further comments please address them to 701...@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Michael Tautschnig <m...@debian.org> (supplier of updated cbmc package)
(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmas...@ftp-master.debian.org)
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256
Format: 1.8
Date: Wed, 10 Jul 2013 12:39:13 +0100
Source: cbmc
Binary: cbmc
Architecture: source i386
Version: 4.4-1
Distribution: unstable
Urgency: low
Maintainer: Michael Tautschnig <m...@debian.org>
Changed-By: Michael Tautschnig <m...@debian.org>
Description:
cbmc - bounded model checker for C and C++ programs
Closes: 701253 713605
Changes:
cbmc (4.4-1) unstable; urgency=low
.
* New upstream release (Closes: #701253, #713605)
Checksums-Sha1:
b2eb8fa9266b20cd82400be3dba369f0df9945b0 1741 cbmc_4.4-1.dsc
f87479b4ef9ecd72bb7eb456e3a93ba553e76b70 3749566 cbmc_4.4.orig.tar.gz
aca2635ca5fd86ae928b0d5ca08f22b62568fe8f 5706 cbmc_4.4-1.debian.tar.gz
6eb79659f1fc0ac4123f33b8f9aa468ff9a377e9 5593596 cbmc_4.4-1_i386.deb
Checksums-Sha256:
b9ac24f30c00693ef66967d585401907cc97f04251005dd1558dab0975e98bb0 1741
cbmc_4.4-1.dsc
2d23471dfc9edf108263c103ed3e9d70f53047e7c4cb46feabb79926ed737086 3749566
cbmc_4.4.orig.tar.gz
72891aea51c2fbd7b2862c5eca97701636dbe3eb56995b8224c1aa42396ee1a9 5706
cbmc_4.4-1.debian.tar.gz
4729bbc33fedb5c0bf984bda35b74308c7ab1329405af89a323d8057ef14d7e8 5593596
cbmc_4.4-1_i386.deb
Files:
8fbb3c027ea6cefa180e74121d8bcc45 1741 science extra cbmc_4.4-1.dsc
1451356db27e9b5e12641771d8339bda 3749566 science extra cbmc_4.4.orig.tar.gz
f83b9bea674b7e339457b93243f1b550 5706 science extra cbmc_4.4-1.debian.tar.gz
c04459aee01e6fc37e1c4fa6591b69e9 5593596 science extra cbmc_4.4-1_i386.deb
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.12 (GNU/Linux)
Comment: GPGTools - http://gpgtools.org
iQIcBAEBCAAGBQJR3WMVAAoJEKjvEonjOGdBRAEP/R0puAitkCyF2JmjT56hjWMI
lNT9aEnk3w1ffELKIonhyxZIotU/fLqn6wv5jr8sXzJG5olbaAIkICWEmEfGGQDK
TqRlN4+1fXEw4FaOdaDVD7aAbaaAOApI/2f0zSPvAEpIgasmGqS7zfNiraSn3OQw
wxLT3YHf+n7BK1R7sK36WgnLJtaoO1G+c6OEkIPqbuD+BKsg9Jk91Ax5b2yCZhhx
xaWYzUcpTekkTpH/1Ev4j8zNhWvEHuIhK+k7kcav+hrhBB8+5CvpDPxyZvrD+kiC
+jJQZt49/g06V7BSqkMCvbTl86UKHsech8qlmJ5fp4GqmUMhHyi/2O3j8wJZ9yAh
YComDxnCinif3/d33Pq8gFDJ6YsrpEUjolD80KOFhNSyGNDe4vBEPjXPVgCtgrBS
3m0UBwl76TjQXEfdDxQM5MzeM/93IrpOuATQ3Rd7smQPam/zAsSPsyNOTTADBSc0
Pj1gCFXQ2r+9avuyRD9bHBKlHRBXVlN/c5zB0oI6mRDMxF1BZkUKq7d0RF1Da8yT
nkOSsEKNemmVM9271X/+m0++XUvlNmYz28EM/rYgN2EnOXrOVaZ75lRWZAbHDJIQ
hNNv3FaFKLjkX7Rw72FxQFYXE8IVf1apyV0WNE9dX1yikN+sE6we8kNg96kpmjuH
89QklOPariVKnjphgdT7
=c+an
-----END PGP SIGNATURE-----
--- End Message ---
