Name: cbmc Version: 5.6 Release: 1%{?dist} Summary: Bounded Model Checker for ANSI-C and C++ programs License: BSD with advertising URL: http://www.cprover.org/cbmc/ Source0: https://github.com/diffblue/cbmc/archive/%{name}-%{version}.tar.gz # Man page link for goto-cc and goto-instrument Source1: goto-cc.1 # Fedora-specific patch: set up our build options Patch0: %{name}-5.6-fix-build.patch BuildRequires: bash BuildRequires: bison BuildRequires: cudd-devel BuildRequires: flex BuildRequires: gcc-c++ BuildRequires: glpk-devel BuildRequires: minisat2-devel BuildRequires: tex(latex) BuildRequires: zlib-devel Requires: sed %description CBMC generates traces that demonstrate how an assertion can be violated, or proves that the assertion cannot be violated within a given number of loop iterations. %prep %setup -q -n %{name}-%{name}-%{version} %patch0 # Use the right build flags sed -e "s|@RPM_OPT_FLAGS@|$RPM_OPT_FLAGS|" \ -e "s|@RPM_LD_FLAGS@|-Wl,--as-needed $RPM_LD_FLAGS|" \ -i src/config.inc # Fix a broken test sed -i '/main\.cpp/a-std=c++98' regression/cpp/enum8/test.desc # Fix two tests that are broken on big endian machines sed -i 's/^$/--little-endian/' regression/cbmc/Pointer_array5/test.desc sed -i 's/--bounds/--little-endian &/' regression/cbmc/Pointer_byte_extract5/test.desc %build make %{?_smp_mflags} -C src # Build optional tools make %{?_smp_mflags} -C src cegis.dir musketeer.dir # Build the guide pushd doc/guide pdflatex CBMC-guide.tex pdflatex CBMC-guide.tex popd %install mkdir -p %{buildroot}%{_bindir} %{buildroot}%{_mandir}/man1 install -p -m 0755 src/cbmc/cbmc %{buildroot}%{_bindir} install -p -m 0755 src/cegis/cegis %{buildroot}%{_bindir} install -p -m 0755 src/goto-analyzer/goto-analyzer %{buildroot}%{_bindir} install -p -m 0755 src/goto-cc/goto-cc %{buildroot}%{_bindir} install -p -m 0755 src/goto-diff/goto-diff %{buildroot}%{_bindir} install -p -m 0755 src/goto-instrument/goto-instrument %{buildroot}%{_bindir} install -p -m 0755 src/musketeer/musketeer %{buildroot}%{_bindir} install -p -m 0755 src/symex/symex %{buildroot}%{_bindir} install -p -m 0644 doc/man/cbmc.1 %{buildroot}%{_mandir}/man1 install -p -m 0644 %{SOURCE1} %{buildroot}%{_mandir}/man1 install -p -m 0644 %{SOURCE1} %{buildroot}%{_mandir}/man1/goto-instrument.1 # Feed the debuginfo generator ln -s xml_y.tab.h src/xmllang/xml_y.tab.hpp %check make -C regression %files %doc CHANGELOG doc/guide/CBMC-guide.pdf doc/html-manual %license LICENSE %{_bindir}/cbmc %{_bindir}/cegis %{_bindir}/goto-analyzer %{_bindir}/goto-cc %{_bindir}/goto-diff %{_bindir}/goto-instrument %{_bindir}/musketeer %{_bindir}/symex %{_mandir}/man1/* %changelog * Sat Nov 26 2016 Jerry James - 5.6-1 - New upstream release * Fri Sep 16 2016 Jerry James - 5.5-2 - Fix two tests that fail on big endian architectures (bz 1371894) * Sat Aug 27 2016 Jerry James - 5.5-1 - New upstream release * Thu Mar 17 2016 Jerry James - 5.4-1 - New upstream release * Sat Mar 12 2016 Jerry James - 5.3-5 - Rebuild for glpk 4.59 * Fri Feb 19 2016 Jerry James - 5.3-4 - Rebuild for glpk 4.58 * Wed Feb 03 2016 Fedora Release Engineering - 5.3-3 - Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild * Fri Jan 22 2016 Jerry James - 5.3-2 - Rebuild for cudd 3.0.0 * Tue Dec 1 2015 Jerry James - 5.3-1 - New upstream release * Wed Oct 7 2015 Jerry James - 5.2-1 - New upstream release * Fri Oct 2 2015 Jerry James - 5.1-3 - Rebuild for cudd 2.5.1 * Wed Jun 17 2015 Fedora Release Engineering - 5.1-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild * Wed May 13 2015 Jerry James - 5.1-1 - New upstream release - Drop upstreamed -messaget patch * Sat May 02 2015 Kalev Lember - 5.0-2 - Rebuilt for GCC 5 C++11 ABI change * Mon Feb 2 2015 Jerry James - 5.0-1 - New upstream release - Drop upstreamed ppc64le patch - Add -messaget patch to fix a build failure * Mon Sep 15 2014 Jerry James - 4.9-1 - New upstream release - Drop upstreamed patches * Wed Sep 3 2014 Jerry James - 4.7-3 - Add patch to fix the ppc64le build (bz 1133066) - Add man page links for goto-cc and goto-instrument - Fix license handling * Fri Aug 15 2014 Fedora Release Engineering - 4.7-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild * Wed Jun 25 2014 Jerry James - 4.7-1 - New upstream release - Build with CUDD support * Sat Jun 07 2014 Fedora Release Engineering - 4.6-2.20131201svn - Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild * Sun Dec 1 2013 Shakthi Kannan - 4.6-1.20131201svn - Updated to upstream 4.6 release * Tue Sep 10 2013 Shakthi Kannan - 4.3-7.20130515svn - Fix build with unversioned docdir using _pkgdocdir (#992043) * Sat Aug 03 2013 Fedora Release Engineering - 4.3-6.20130515svn - Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild * Wed Jul 10 2013 Dan Horák - 4.3-5.20130515svn - fix build on s390x * Mon Jul 8 2013 Shakthi Kannan - 4.3-4.20130515svn - Fixed changelog date * Sun Jun 30 2013 Shakthi Kannan - 4.3-3.20130515svn - Updated license - Fixed doc and manual page directories * Tue Jun 25 2013 Shakthi Kannan - 4.3-2.20130515svn - Updated release * Wed May 15 2013 Shakthi Kannan - 4.3-1.20130515svn - First release