125 lines
4.3 KiB
RPMSpec
125 lines
4.3 KiB
RPMSpec
|
%global timestamp 11-18-2008
|
||
|
|
||
|
Name: stp
|
||
|
Version: 0.1
|
||
|
Release: 2%{?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 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
|
||
|
|