# Force out-of-source build on EPEL 8.
%undefine __cmake_in_source_build

Name:       predator
Version:    0.1.0.20260325.191506.g4cbdfd04
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.20260325.191506.g4cbdfd04.tar.gz
Source1:    version_cl.h
Source2:    version.h

BuildRequires: boost-devel
BuildRequires: cmake
BuildRequires: gcc-c++
BuildRequires: gcc-plugin-devel

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.

# FIXME: temporarily disable LTO on Fedora 44+ to avoid a crash while unwinding
# the std::runtime_error exception
%if 0%{?fedora} >= 44
%define _lto_cflags %{nil}
%endif

%prep
%setup -q -n predator-0.1.0.20260325.191506.g4cbdfd04
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

%build
%define _vpath_builddir cl_build
%cmake -S cl -DGCC_HOST=/usr/bin/gcc -Wno-dev
%cmake_build

%define _vpath_builddir sl_build
%cmake -S sl -DGCC_HOST=/usr/bin/gcc -Wno-dev
%cmake_build

%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
%define _vpath_builddir cl_build
%ctest
%define _vpath_builddir sl_build
%ctest

%files
%{plugin_dir}/predator.so