# FIXME: report to upstream
%define _lto_cflags %{nil}
%define utils_version 1.3
Name: cbmc
Version: 5.95.1
Release: 4%{?dist}
Summary: Bounded Model Checker for ANSI-C and C++ programs
License: BSD-4-Clause
URL: https://www.cprover.org/cbmc
Source0: https://github.com/diffblue/%{name}/archive/%{name}-%{version}/%{name}-%{version}.tar.gz
Source1: https://github.com/aufover/%{name}-utils/archive/v%{utils_version}/%{name}-utils-%{utils_version}.tar.gz
# Disable -Werror flag
Patch0: %{name}-disable-werror.patch
# FIXME: Upstream these patches!
# Adapt to recent versions of glpk
Patch1: %{name}-5.9-glpk.patch
# Implements https://github.com/diffblue/cbmc/issues/5965
Patch2: %{name}-add-cmd-line-arg.patch
# Fix compilation on F40
Patch3: %{name}-f40-fix-build.patch
BuildRequires: bison
BuildRequires: cmake
BuildRequires: doxygen
BuildRequires: flex
BuildRequires: gcc-c++
BuildRequires: glpk-devel
BuildRequires: minisat2-devel
BuildRequires: ninja-build
BuildRequires: zlib-devel
%ifarch x86_64
# For the tests
BuildRequires: cvc5
BuildRequires: gdb
BuildRequires: jq
BuildRequires: perl
BuildRequires: python3
BuildRequires: z3
# For %%py3_shebang_fix
BuildRequires: python3-devel
%endif
Requires: gcc-c++
%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.
%package doc
Summary: Documentation for %{name}
%description doc
Documentation for %{name}.
%package utils
Summary: Output conversion utilities for CBMC
%description utils
Output conversion utilities for CBMC (GCC like format).
%prep
%setup -T -q -b 1 -n %{name}-utils-%{utils_version}
%autosetup -p1 -b 0 -n %{name}-%{name}-%{version}
%build
%cmake -GNinja -DWITH_JBMC:BOOL=OFF \
-Dsat_impl:STRING=system-minisat2 \
%ifarch %{ix86} x86_64
-DWITH_MEMORY_ANALYZER:BOOL=ON \
%endif
-DBUILD_SHARED_LIBS:BOOL=OFF
%cmake_build
%cmake_build --target doc
%install
%cmake_install
install -p -m 0755 "%{_builddir}/%{name}-utils-%{utils_version}/cbmc_utils/formatCBMCOutput.py" %{buildroot}%{_bindir}/%{name}-convert-output
install -p -m 0755 "%{_builddir}/%{name}-utils-%{utils_version}/cbmc_utils/csexec-cbmc.sh" %{buildroot}%{_bindir}/csexec-%{name}
# Remove Cprover API stuff because static libraries are not allowed!
rm -rf %{buildroot}%{_includedir}
rm -rf %{buildroot}%{_libdir}/libcprover.*.a
# FIXME: Report to upstream that the target directory for completions is wrong!
mkdir -p %{buildroot}%{bash_completions_dir}
mv %{buildroot}{/usr/etc/bash_completion.d/cbmc,%{bash_completions_dir}}
%ifarch x86_64
%check
# Fix unversioned shebang!
%py3_shebang_fix scripts/cpplint.py
# The tests were written with the assumption that they would be executed on
# an x86_64. Other platforms suffer a large number of spurious test failures.
%ctest --label-regex CORE
%ctest --tests-regex unit-xfail
%endif
%files
%doc README.md
%license LICENSE
%{_bindir}/cbmc
%{_bindir}/cprover
%{_bindir}/crangler
%{_bindir}/goto-*
%{_bindir}/ls_parse.py
%{_bindir}/symtab2gb
%{bash_completions_dir}
%{_mandir}/man1/cbmc*.1.*
%{_mandir}/man1/crangler*.1.*
%{_mandir}/man1/goto-*.1.*
%ifarch %{ix86} x86_64
%{_mandir}/man1/memory-analyzer.1.*
%endif
%{_mandir}/man1/symtab2gb.1.*
%files doc
%doc %{__cmake_builddir}/doc/html README.md TOOLS_OVERVIEW.md
%license LICENSE
%files utils
%license ../%{name}-utils-%{utils_version}/LICENSE
%{_bindir}/%{name}-convert-output
%{_bindir}/csexec-%{name}
%changelog
* Fri Feb 09 2024 Lukáš Zaoral <lzaoral@redhat.com> - 5.95.1-4
- fix FTBFS on Rawhide (rhbz#2259235)
* Tue Jan 23 2024 Fedora Release Engineering <releng@fedoraproject.org> - 5.95.1-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
* Fri Jan 19 2024 Fedora Release Engineering <releng@fedoraproject.org> - 5.95.1-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
* Tue Nov 21 2023 Lukáš Zaoral <lzaoral@redhat.com> - 5.95.1-1
- Update to 5.95.1 (rhbz#2239079)
* Fri Jul 21 2023 Lukáš Zaoral <lzaoral@redhat.com> - 5.50.0-6
- Exclude installation of test dependencies on non-x86_64 architectures
* Wed Jul 19 2023 Fedora Release Engineering <releng@fedoraproject.org> - 5.50.0-5
- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild
* Sun Jan 29 2023 Lukáš Zaoral <lzaoral@redhat.com> - 5.50.0-4
- Fix rawhide FTBFS
- Use SPDX license format
- Modernize the spec a bit
* Wed Jan 18 2023 Fedora Release Engineering <releng@fedoraproject.org> - 5.50.0-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild
* Wed Jul 20 2022 Fedora Release Engineering <releng@fedoraproject.org> - 5.50.0-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
* Wed Feb 09 2022 Vincent Mihalkovic <vmihalko@redhat.com> - 5.50.0-1
- New upstream release of cbmc and also cbmc-utils
- Add "--add-cmd-line-arg" option for goto-instrument
* Wed Jan 19 2022 Fedora Release Engineering <releng@fedoraproject.org> - 5.38.0-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
* Wed Sep 15 2021 Vincent Mihalkovic <vmihalko@redhat.com> - 5.38.0-1
- New upstream release of cbmc and also cbmc-utils
* Mon Aug 23 2021 Pavel Simovec <psimovec@redhat.com> - 5.37.0-1
- New upstream release
- fix broken indentation in a patch
* Wed Aug 4 2021 Lukas Zaoral <lzaoral@redhat.com> - 5.35.0-1
- New upstream release
- Use plain doxygen to cut-down some build dependencies
* Wed Jul 21 2021 Fedora Release Engineering <releng@fedoraproject.org> - 5.29.0-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
* Wed May 12 2021 Vincent Mihalkovic <vmihalko@redhat.com> - 5.29.0-1
- New upstream release
* Wed Mar 10 2021 Vincent Mihalkovic <vmihalko@redhat.com> - 5.25.0-2
- Add Requires: clang
* Wed Mar 10 2021 Vincent Mihalkovic <vmihalko@redhat.com> - 5.25.0-1
- Add csexec-cbmc.sh script
- New upstream release
* Tue Feb 23 2021 Vincent Mihalkovic <vmihalko@redhat.com> - 5.24.0-1
- Add goto-clang for a hybrid binary translation
- New upstream release
* Tue Jan 26 2021 Fedora Release Engineering <releng@fedoraproject.org> - 5.17.0-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild
* Mon Nov 02 2020 Vincent Mihalkovic <vmihalko@redhat.com> - 5.17.0-1
- New upstream release
* Thu Oct 08 2020 Vincent Mihalkovic <vmihalko@redhat.com> - 5.15.0-1
- New upstream release
* Wed Sep 30 2020 Vincent Mihalkovic <vmihalko@redhat.com> - 5.14.3-1
- New upstream release
* Tue Sep 29 2020 Vincent Mihalkovic <vmihalko@redhat.com> - 5.13.1-1
- New upstream release
- Use CMake instead of plain Makefiles
- Add cbmc-utils subpackage
* Tue Sep 01 2020 Vincent Mihalkovic <vmihalko@redhat.com> - 5.13.0-1
- New upstream release
* Wed Aug 12 2020 Vincent Mihalkovic <vmihalko@redhat.com> - 5.12.6-1
- Replace custom goto-cc.1 with symlinks to cbmc.1
- Enable full cbmc testsuite
- python to python3 fix in one test case
* Mon Jul 27 2020 Fedora Release Engineering <releng@fedoraproject.org> - 5.12-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
* Thu Jul 9 2020 Vincent Mihalkovic <vmihalko@redhat.com> - 5.12-1
- New upstream release. Skipping some of regression tests - temporary f33 build fix
* Tue Jan 28 2020 Fedora Release Engineering <releng@fedoraproject.org> - 5.11-5
- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild
* Fri Sep 27 2019 Jerry James <loganjerry@gmail.com> - 5.11-4
- Drop cudd support due to impending cudd retirement
* Wed Jul 24 2019 Fedora Release Engineering <releng@fedoraproject.org> - 5.11-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
* Sat Jun 8 2019 Jerry James <loganjerry@gmail.com> - 5.11-2
- Fix man page links (bz 1718287)
* Thu Jan 31 2019 Jerry James <loganjerry@gmail.com> - 5.11-1
- New upstream release
* Thu Jan 31 2019 Fedora Release Engineering <releng@fedoraproject.org> - 5.10-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
* Wed Sep 26 2018 Jerry James <loganjerry@gmail.com> - 5.10-1
- New upstream release
* Thu Jul 12 2018 Fedora Release Engineering <releng@fedoraproject.org> - 5.9-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
* Fri Jun 22 2018 Jerry James <loganjerry@gmail.com> - 5.9-1
- New upstream release
- Drop upstreamed -float128 and -vec patches
- Musketeer and symex have been removed; do not try to build them
* Mon Jun 11 2018 Jerry James <loganjerry@gmail.com> - 5.8-4
- Fix out of bounds vector accesses
* Sat Jun 2 2018 Jerry James <loganjerry@gmail.com> - 5.8-3
- Rebuild for glpk 4.65
* Wed Feb 07 2018 Fedora Release Engineering <releng@fedoraproject.org> - 5.8-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
* Sat Aug 12 2017 Jerry James <loganjerry@gmail.com> - 5.8-1
- New upstream release
- Drop upstreamed -musketeer patch
- Add -doc subpackage to hold doxygen-generated content
* Wed Aug 02 2017 Fedora Release Engineering <releng@fedoraproject.org> - 5.7-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild
* Wed Jul 26 2017 Fedora Release Engineering <releng@fedoraproject.org> - 5.7-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild
* Thu Apr 6 2017 Jerry James <loganjerry@gmail.com> - 5.7-1
- New upstream release
* Wed Apr 5 2017 Jerry James <loganjerry@gmail.com> - 5.6-3
- Rebuild for glpk 4.61
* Fri Feb 10 2017 Fedora Release Engineering <releng@fedoraproject.org> - 5.6-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild
* Sat Nov 26 2016 Jerry James <loganjerry@gmail.com> - 5.6-1
- New upstream release
* Fri Sep 16 2016 Jerry James <loganjerry@gmail.com> - 5.5-2
- Fix two tests that fail on big endian architectures (bz 1371894)
* Sat Aug 27 2016 Jerry James <loganjerry@gmail.com> - 5.5-1
- New upstream release
* Thu Mar 17 2016 Jerry James <loganjerry@gmail.com> - 5.4-1
- New upstream release
* Sat Mar 12 2016 Jerry James <loganjerry@gmail.com> - 5.3-5
- Rebuild for glpk 4.59
* Fri Feb 19 2016 Jerry James <loganjerry@gmail.com> - 5.3-4
- Rebuild for glpk 4.58
* Wed Feb 03 2016 Fedora Release Engineering <releng@fedoraproject.org> - 5.3-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
* Fri Jan 22 2016 Jerry James <loganjerry@gmail.com> - 5.3-2
- Rebuild for cudd 3.0.0
* Tue Dec 1 2015 Jerry James <loganjerry@gmail.com> - 5.3-1
- New upstream release
* Wed Oct 7 2015 Jerry James <loganjerry@gmail.com> - 5.2-1
- New upstream release
* Fri Oct 2 2015 Jerry James <loganjerry@gmail.com> - 5.1-3
- Rebuild for cudd 2.5.1
* Wed Jun 17 2015 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 5.1-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild
* Wed May 13 2015 Jerry James <loganjerry@gmail.com> - 5.1-1
- New upstream release
- Drop upstreamed -messaget patch
* Sat May 02 2015 Kalev Lember <kalevlember@gmail.com> - 5.0-2
- Rebuilt for GCC 5 C++11 ABI change
* Mon Feb 2 2015 Jerry James <loganjerry@gmail.com> - 5.0-1
- New upstream release
- Drop upstreamed ppc64le patch
- Add -messaget patch to fix a build failure
* Mon Sep 15 2014 Jerry James <loganjerry@gmail.com> - 4.9-1
- New upstream release
- Drop upstreamed patches
* Wed Sep 3 2014 Jerry James <loganjerry@gmail.com> - 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 <rel-eng@lists.fedoraproject.org> - 4.7-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild
* Wed Jun 25 2014 Jerry James <loganjerry@gmail.com> - 4.7-1
- New upstream release
- Build with CUDD support
* Sat Jun 07 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 4.6-2.20131201svn
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild
* Sun Dec 1 2013 Shakthi Kannan <shakthimaan [AT] fedoraproject.org> - 4.6-1.20131201svn
- Updated to upstream 4.6 release
* Tue Sep 10 2013 Shakthi Kannan <shakthimaan [AT] fedoraproject.org> - 4.3-7.20130515svn
- Fix build with unversioned docdir using _pkgdocdir (#992043)
* Sat Aug 03 2013 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 4.3-6.20130515svn
- Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild
* Wed Jul 10 2013 Dan Horák <dan[at]danny.cz> - 4.3-5.20130515svn
- fix build on s390x
* Mon Jul 8 2013 Shakthi Kannan <shakthimaan [AT] fedoraproject.org> - 4.3-4.20130515svn
- Fixed changelog date
* Sun Jun 30 2013 Shakthi Kannan <shakthimaan [AT] fedoraproject.org> - 4.3-3.20130515svn
- Updated license
- Fixed doc and manual page directories
* Tue Jun 25 2013 Shakthi Kannan <shakthimaan [AT] fedoraproject.org> - 4.3-2.20130515svn
- Updated release
* Wed May 15 2013 Shakthi Kannan <shakthimaan [AT] fedoraproject.org> - 4.3-1.20130515svn
- First release