Name:       predator
Version:    0.1.0.20241018.165707.gabf5359f
Release:    1%{?dist}
Summary:    A Shape Analyzer Based on Symbolic Memory Graphs

License:    GPLv3+
URL:        https://github.com/kdudka/%{name}
Source0:    predator-0.1.0.20241018.165707.gabf5359f.tar.gz
Source1:    version_cl.h
Source2:    version.h

BuildRequires: boost-devel
BuildRequires: cmake
BuildRequires: gcc-c++
BuildRequires: gcc-plugin-devel
BuildRequires: glibc-devel%(tmp="%{_isa}" && echo "${tmp/-64/-32}")

Requires: gcc

%description
Predator is a tool for automated formal verification of sequential C programs
operating with pointers and linked lists. The core algorithms of Predator were
originally inspired by works on *separation logic* with higher-order list
predicates, but they are now purely graph-based and significantly extended to
support various forms of low-level memory manipulation used in system-level
code.  Such operations include pointer arithmetic, safe usage of invalid
pointers, block operations with memory, reinterpretation of the memory contents,
address alignment, etc.  The tool can be loaded into *GCC* as a *plug-in*.  This
way you can easily analyse C code sources, using the existing build system,
without manually preprocessing them first.  The analysis itself is, however, not
ready for complex projects yet.

%prep
%setup -q -n predator-0.1.0.20241018.165707.gabf5359f
install -pv %{SOURCE1} cl/
install -pv %{SOURCE2} sl/
patch -p1 < build-aux/distro-install.patch
%if 0%{?rhel} && 0%{?rhel} < 9
patch -p1 < build-aux/gcc-8.3.0.patch
%endif
%if 0%{?rhel} == 7
patch -p1 < build-aux/gcc-6.5.0.patch
patch -p1 < build-aux/gcc-5.4.0.patch
%endif

%build
mkdir cl_build
cd cl_build
%cmake -S../cl ../cl -B. -DGCC_HOST=/usr/bin/gcc -Wno-dev
make %{?_smp_mflags} VERBOSE=yes

mkdir ../sl_build
cd ../sl_build
%cmake -S../sl ../sl -B. -DGCC_HOST=/usr/bin/gcc -Wno-dev
make %{?_smp_mflags} VERBOSE=yes

%install
%global plugin_dir %(gcc --print-file-name=plugin)
mkdir -p %{buildroot}%{plugin_dir}
install -m0755 sl_build/libsl.so %{buildroot}%{plugin_dir}/predator.so

%check
make check -C cl
make check -C sl

%files
%{plugin_dir}/predator.so