more

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@167 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

scripts/cbmc.spec

@@ -0,0 +1,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
+

scripts/make-rpm

@@ -0,0 +1,9 @@
+#!/bin/bash
+
+svn export http://svn.cprover.org/svn/cbmc
+mv cbmc cbmc-3.9
+tar czf cbmc-3.9.tar.gz cbmc-3.9
+wget http://www.minisat.se/downloads/minisat-2.2.0.tar.gz
+mkdir $HOME/rpmbuild/SOURCES
+mv cbmc-3.9.tar.gz minisat-2.2.0.tar.gz $HOME/rpmbuild/SOURCES
+rpmbuild -qa cbmc.spec