Package: spin
Version: 6.5.2+dfsg-1
Severity: normal
Dear Maintainer,
When I compile Spin manually, without changing anything to its
makefile, it supports the "X" (next) operator. For instance:
% ./spin -V
Spin Version 6.5.2 -- 6 December 2019
% ./spin -f 'X a'
never { /* X a */
accept_init:
T0_init:
do
:: (1) -> goto accept_S0
od;
accept_S0:
T0_S0:
do
:: atomic { ((a)) -> assert(!((a))) }
od;
accept_all:
skip
}
However the version shipped with Debian does not:
% spin -V
Spin Version 6.5.2 -- 6 December 2019
% spin -f 'X a'
tl_spin: expected predicate, saw 'X'
tl_spin: X a
----------^
My understanding is that this is because Src/makefile has
CFLAGS?=-O2 -DNXT -Wall -pedantic
but debhelper very likely defines its own CFLAGS, so this line
get ignored, and -DNXT (needed for "next" support) is lost.
-- System Information:
Debian Release: trixie/sid
APT prefers stable-security
APT policy: (500, 'stable-security'), (500, 'unstable'), (500, 'testing'),
(500, 'stable')
Architecture: amd64 (x86_64)
Foreign Architectures: i386
Kernel: Linux 6.10.9-amd64 (SMP w/12 CPU threads; PREEMPT)
Locale: LANG=en_US.UTF-8, LC_CTYPE=en_US.UTF-8 (charmap=UTF-8),
LANGUAGE=en_US:en
Shell: /bin/sh linked to /usr/bin/dash
Init: systemd (via /run/systemd/system)
LSM: AppArmor: enabled
Versions of packages spin depends on:
ii libc6 2.40-2
spin recommends no packages.
spin suggests no packages.
-- no debconf information
