1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
Name: cbmc
Version: 3.9
Release: 1%{?dist}
Summary: bounded model checker for C and C++ programs
Group: Applications
License: BSD 4-clause
URL: http://www.cprover.org
Source0: http://www.minisat.se/downloads/minisat-2.2.0.tar.gz
Source1: cbmc-3.9.tar.gz
BuildRoot: %(mktemp -ud %{_tmppath}/%{name}-%{version}-%{release}-XXXXXX)
Requires: gcc
%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 -c cbmc+minisat
%setup -q -c cbmc+minisat -T -D -a 1
%build
mv minisat minisat-2.2.0
cd minisat-2.2.0
make MROOT=$PWD -C simp
cd ..
make -C cbmc-3.9/trunk/src/big-int
make -C cbmc-3.9/trunk/src/util
make -C cbmc-3.9/trunk/src %{?_smp_mflags}
%install
rm -rf $RPM_BUILD_ROOT
mkdir -p %{buildroot}/%{_bindir}
for b in goto-cc goto-instrument cbmc ; do cp cbmc-3.9/trunk/src/$b/$b %{buildroot}/%{_bindir} ; done
strip %{buildroot}/%{_bindir}/*
%clean
rm -rf $RPM_BUILD_ROOT
%files
%defattr(-,root,root,-)
%doc
%{_bindir}/goto-cc
%{_bindir}/goto-instrument
%{_bindir}/cbmc
%changelog
|
