rpms / cbmc

Clone
Source Code
GIT

Files

f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 f34 f35 f36 f37 f38 f39 f40 main rawhide
  1.   f26
  2.   cbmc.spec
Blob Blame History Raw 
Name:           cbmc
Version:        5.7
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.7-fix-build.patch
# Make -Werror=format-security happy
Patch1:         %{name}-5.7-format.patch
# Fix a build failure: https://github.com/diffblue/cbmc/issues/777
Patch2:         %{name}-5.7-qbf.patch
# Fix a build failure: https://github.com/diffblue/cbmc/issues/778
Patch3:         %{name}-5.7-musketeer.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
%patch1
%patch2
%patch3

# 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 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
sed -i 's/^$/--little-endian/' regression/cbmc/byte_update2/test.desc
sed -i 's/^$/--little-endian/' regression/cbmc/byte_update3/test.desc
sed -i 's/^$/--little-endian/' regression/cbmc/byte_update4/test.desc
sed -i 's/^$/--little-endian/' regression/cbmc/byte_update5/test.desc
sed -i 's/^$/--little-endian/' regression/cbmc/byte_update6/test.desc
sed -i 's/^$/--little-endian/' regression/cbmc/byte_update7/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
* 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
Powered by Pagure 5.13.3
Documentation • File an Issue • About this Instance • SSH Hostkey/Fingerprint
© Red Hat, Inc. and others.