131 lines
4.5 KiB
RPMSpec
131 lines
4.5 KiB
RPMSpec
%global timestamp 11-18-2008
|
|
|
|
Name: stp
|
|
Version: 0.1
|
|
Release: 3%{?dist}
|
|
Summary: Constraint solver/decision procedure
|
|
|
|
Group: Applications/Engineering
|
|
License: MIT
|
|
URL: http://sourceforge.net/projects/stp-fast-prover/
|
|
Source0: http://downloads.sourceforge.net/stp-fast-prover/stp-ver-%{version}-%{timestamp}.tgz
|
|
|
|
# Minor patch to fix a missing #include for strcmp (modern g++ requires it)
|
|
Patch1: stp-strcmp.patch
|
|
|
|
# Note: This version does not support the SMT-LIB input format (the code
|
|
# is not complete). The SourceForge SVN contains patches that
|
|
# add SMT-LIB support.
|
|
|
|
BuildRoot: %(mktemp -ud %{_tmppath}/%{name}-%{version}-%{release}-XXXXXX)
|
|
|
|
BuildRequires: bison
|
|
BuildRequires: flex
|
|
# Requires:
|
|
|
|
%description
|
|
STP (Simple Theorem Prover) is
|
|
a constraint solver (also referred to as a decision procedure
|
|
or automated prover) aimed at solving constraints generated by program
|
|
analysis tools, theorem provers, automated bug finders, intelligent
|
|
fuzzers and model checkers. STP has been used in many research projects
|
|
at Stanford, Berkeley, MIT, CMU and other universities, as well as
|
|
companies and government agencies.
|
|
|
|
The input to STP are formulas over the theory of bit-vectors and arrays
|
|
(This theory captures most expressions from languages like C/C++/Java
|
|
and Verilog), and the output of STP is a single bit of information that
|
|
indicates whether the formula is satisfiable or not. If the input is
|
|
satisfiable, then it also generates a variable assignment to satisfy
|
|
the input formula.
|
|
|
|
Additional information can be found at:
|
|
http://people.csail.mit.edu/vganesh/STP_files/stp.html
|
|
|
|
|
|
%package devel
|
|
Summary: Development files for STP constraint solver/decision procedure
|
|
Group: Applications/Engineering
|
|
Requires: %{name} = %{version}-%{release}
|
|
Provides: %{name}-static = %{version}-%{release}
|
|
# This "devel" package provides a static (not dynamic) library because:
|
|
# 1. This is the normal usage mode when linking this as a library;
|
|
# it's what upstream and existing programs that use this program expect.
|
|
# 2. This speeds execution. In this library, speed matters.
|
|
# There's a speed penalty for .so files, and this program is much
|
|
# like a chess program - it's essentially an inner loop that searches
|
|
# a massive space of possibilities.
|
|
# A dynamic .so version could be create using:
|
|
# gcc -shared -Wl,-soname,libstp.so.1 -o libstp.so.1.0.1 libstp.a
|
|
# but this would require -fpic to compile (slowing the results).
|
|
# See my document:
|
|
# http://www.dwheeler.com/program-library/Program-Library-HOWTO/
|
|
%description devel
|
|
Development files for the STP (Simple Theorem Prover),
|
|
a constraint solver (also referred to as a decision procedure
|
|
or automated prover). Provides a static library.>>>>>> 1.84
|
|
|
|
%prep
|
|
%setup -q -n stp-ver-%{version}-%{timestamp}
|
|
%patch1
|
|
|
|
%build
|
|
# The true --libdir hack works around an rpmlint bug; this configure
|
|
# doesn't accept a --libdir argument. We'll override LIB_DIR instead.
|
|
./configure --with-prefix=%{_prefix} ; true --libdir=%{_libdir}
|
|
|
|
# DO NOT use _smp_mflags; build will fail.
|
|
make -k CPPFLAGS="%{optflags} -Wno-deprecated" LIB_DIR=%{_libdir} all
|
|
|
|
%check
|
|
make regressall
|
|
|
|
%install
|
|
rm -rf %{buildroot}
|
|
mkdir -p %{buildroot}%{_bindir}
|
|
mkdir -p %{buildroot}%{_includedir}/stp
|
|
mkdir -p %{buildroot}%{_libdir}
|
|
|
|
# This "make install" doesn't support DESTDIR=%{buildroot}.
|
|
# We'll rig PREFIX/LIB_DIR, since that happens to work for this makefile.
|
|
make install PREFIX=%{buildroot}%{_prefix} LIB_DIR=%{buildroot}%{_libdir}
|
|
|
|
%clean
|
|
rm -rf %{buildroot}
|
|
|
|
|
|
# Note: Limit the files included in _libdir, or we'll accidentally
|
|
# include the optional debugging files into the main package:
|
|
# In the future, perhaps create a "-devel" package with:
|
|
%files
|
|
%defattr(-,root,root,-)
|
|
%{_bindir}/*
|
|
%doc README LICENSE
|
|
%doc TALKS/*
|
|
%doc PAPERS/*
|
|
%doc web/*
|
|
|
|
%files devel
|
|
%defattr(-,root,root,-)
|
|
%{_libdir}/libstp*.a
|
|
%{_includedir}/stp/
|
|
|
|
%changelog
|
|
* Mon Mar 6 2009 David A. Wheeler <dwheeler at, dwheeler.com> 0.1-4
|
|
- Re-sync with CVS
|
|
|
|
* Mon Mar 6 2009 David A. Wheeler <dwheeler at, dwheeler.com> 0.1-3
|
|
- Modified spec so can rebuild in proper order on Fedora
|
|
|
|
* Mon Mar 3 2009 David A. Wheeler <dwheeler at, dwheeler.com> 0.1-2
|
|
- Fixed comments by Marcela Maslanova, mmaslano (at) redhat*DOT*com 2009-02-26
|
|
- Moved definitions of subpackages to "top" of spec before prep.
|
|
- moved "check" before "files".
|
|
- Use macro for release version 0.1-11-18-2008 for future updates.
|
|
- No doc for -devel package; it's already in the base.
|
|
- CPPFLAGS now includes optflags.
|
|
|
|
* Mon Feb 23 2009 David A. Wheeler <dwheeler at, dwheeler.com> 0.1-1
|
|
- Initial packaging
|
|
|