[rpms/frama-c] f44: Version 33.0

[Jerry James <loganjerry@gmail.com>]

            A new commit has been pushed.

            Repo   : rpms/frama-c
            Branch : f44
            Commit : f5db078ed23c2a810780a89d279f55fa68d82e1e
            Author : Jerry James <loganjerry@gmail.com>
            Date   : 2026-07-29T14:48:35-06:00
            Stats  : +70/-93 in 6 file(s)
            URL    : https://src.fedoraproject.org/rpms/frama-c/c/f5db078ed23c2a810780a89d279f55fa68d82e1e?branch=f44

            Log:
            Version 33.0

- Drop unneeded patches
- Disable testing, which is now completely broken
- Use the dune declarative buildsystem
- Fedora RPM builds now deduplicate by default

---
diff --git a/.gitignore b/.gitignore
index d952138..ca90bc1 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,13 +1,16 @@
 /frama-c-icons.tar.xz
 /frama-c-*.tar.gz
 /acsl-implementation-*.pdf
+/acsl-importer-manual-*.pdf
 /aorai-manual-*.pdf
 /e-acsl-implementation*.pdf
 /e-acsl-manual*.pdf
 /eva-manual-*.pdf
 /metrics-manual-*.pdf
+/mthread-manual-*.pdf
 /plugin-development-guide-*.pdf
 /rte-manual-*.pdf
 /user-manual-*.pdf
 /value-analysis-*.pdf
+/volatile-manual-*.pdf
 /wp-manual-*.pdf

diff --git a/frama-c-bytes.patch b/frama-c-bytes.patch
index ee7431b..1d2f8d8 100644
--- a/frama-c-bytes.patch
+++ b/frama-c-bytes.patch
@@ -1,11 +1,11 @@
---- frama-c-32.0-Germanium/src/dune.orig	2025-12-01 17:00:00.000000000 -0700
-+++ frama-c-32.0-Germanium/src/dune	2025-12-04 14:15:00.042836553 -0700
-@@ -46,7 +46,7 @@
+--- frama-c-33.0-Arsenic/src/dune.orig	2026-07-23 18:00:00.000000000 -0600
++++ frama-c-33.0-Arsenic/src/dune	2026-07-28 15:56:34.040551758 -0600
+@@ -49,7 +49,7 @@
    (public_name frama-c.kernel)
    (foreign_stubs (language c) (names c_bindings floating_point))
    (flags :standard -w -9)
--  (libraries frama-c.init fpath str unix zarith ocamlgraph dynlink bytes yaml.unix yojson menhirLib dune-site dune-site.plugins zip)
-+  (libraries frama-c.init fpath str unix zarith ocamlgraph dynlink yaml.unix yojson menhirLib dune-site dune-site.plugins zip)
+-  (libraries frama-c.init fpath str unix zarith ocamlgraph dynlink bytes yaml.unix yojson menhirLib dune-site dune-site.plugins zip frama-c.fc_internal_z)
++  (libraries frama-c.init fpath str unix zarith ocamlgraph dynlink yaml.unix yojson menhirLib dune-site dune-site.plugins zip frama-c.fc_internal_z)
    (instrumentation (backend landmarks))
    (instrumentation (backend bisect_ppx))
-   (inline_tests (libraries frama-c.init.cmdline))
+   (inline_tests (libraries frama-c.init))

diff --git a/frama-c-dune-bug.patch b/frama-c-dune-bug.patch
deleted file mode 100644
index 102573b..0000000
--- a/frama-c-dune-bug.patch
+++ /dev/null
@@ -1,12 +0,0 @@
---- frama-c-32.1-Germanium/src/plugins/aorai/dune.orig	2026-03-15 18:00:00.000000000 -0600
-+++ frama-c-32.1-Germanium/src/plugins/aorai/dune	2026-03-20 11:47:32.527775996 -0600
-@@ -8,6 +8,9 @@
- ;;                                                                            ;;
- ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
- 
-+(dirs ../eva)
-+(include_subdirs unqualified)
-+
- (rule
-  (alias frama-c-configure)
-  (deps (universe))

diff --git a/frama-c-mathlib.patch b/frama-c-mathlib.patch
index 6998dce..5bf2788 100644
--- a/frama-c-mathlib.patch
+++ b/frama-c-mathlib.patch
@@ -1,10 +1,10 @@
---- frama-c-32.0-Germanium/src/dune.orig	2025-12-04 14:15:00.042836553 -0700
-+++ frama-c-32.0-Germanium/src/dune	2025-12-04 14:15:15.346716318 -0700
-@@ -47,6 +47,7 @@
+--- frama-c-33.0-Arsenic/src/dune.orig	2026-07-28 15:56:34.040551758 -0600
++++ frama-c-33.0-Arsenic/src/dune	2026-07-28 15:57:37.592107558 -0600
+@@ -50,6 +50,7 @@
    (foreign_stubs (language c) (names c_bindings floating_point))
    (flags :standard -w -9)
-   (libraries frama-c.init fpath str unix zarith ocamlgraph dynlink yaml.unix yojson menhirLib dune-site dune-site.plugins zip)
+   (libraries frama-c.init fpath str unix zarith ocamlgraph dynlink yaml.unix yojson menhirLib dune-site dune-site.plugins zip frama-c.fc_internal_z)
 +  (c_library_flags -lm)
    (instrumentation (backend landmarks))
    (instrumentation (backend bisect_ppx))
-   (inline_tests (libraries frama-c.init.cmdline))
+   (inline_tests (libraries frama-c.init))

diff --git a/frama-c.spec b/frama-c.spec
index 1485461..55b4c04 100644
--- a/frama-c.spec
+++ b/frama-c.spec
@@ -1,15 +1,12 @@
-# Coq's plugin architecture requires cmxs files, so:
-ExclusiveArch: %{ocaml_native_compiler}
-
 # Without this, gcc flags are passed to frama-c in the test suite
 %undefine _auto_set_build_flags
 
 Name:           frama-c
-Version:        32.1
+Version:        33.0
 Release:        %autorelease
 Summary:        Framework for source code analysis of C software
 
-%global pkgversion %{version}-Germanium
+%global pkgversion %{version}-Arsenic
 
 # Licensing breakdown in source file frama-c.licensing
 License:        LGPL-2.1-only AND LGPL-2.1-or-later AND LGPL-2.0-only WITH OCaml-LGPL-linking-exception AND GPL-2.0-or-later AND CC0-1.0 AND CC-BY-SA-4.0 AND BSD-3-Clause AND QPL-1.0-INRIA-2004 WITH QPL-1.0-INRIA-2004-exception
@@ -21,19 +18,22 @@ Source2:        https://frama-c.com/download/%{name}-server-%{pkgversion}-api.ta
 Source3:        https://frama-c.com/download/user-manual-%{pkgversion}.pdf
 Source4:        https://frama-c.com/download/plugin-development-guide-%{pkgversion}.pdf
 Source5:        https://frama-c.com/download/acsl-implementation-%{pkgversion}.pdf
-Source6:        https://frama-c.com/download/aorai-manual-%{pkgversion}.pdf
-Source7:        https://frama-c.com/download/e-acsl/e-acsl-manual-%{pkgversion}.pdf
-Source8:        https://frama-c.com/download/e-acsl/e-acsl-implementation-%{pkgversion}.pdf
-Source9:        https://frama-c.com/download/eva-manual-%{pkgversion}.pdf
-Source10:       https://frama-c.com/download/metrics-manual-%{pkgversion}.pdf
-Source11:       https://frama-c.com/download/rte-manual-%{pkgversion}.pdf
-Source12:       https://frama-c.com/download/wp-manual-%{pkgversion}.pdf
+Source6:        https://frama-c.com/download/acsl-importer-manual-%{pkgversion}.pdf
+Source7:        https://frama-c.com/download/aorai-manual-%{pkgversion}.pdf
+Source8:        https://frama-c.com/download/e-acsl/e-acsl-manual-%{pkgversion}.pdf
+Source9:        https://frama-c.com/download/e-acsl/e-acsl-implementation-%{pkgversion}.pdf
+Source10:       https://frama-c.com/download/eva-manual-%{pkgversion}.pdf
+Source11:       https://frama-c.com/download/metrics-manual-%{pkgversion}.pdf
+Source12:       https://frama-c.com/download/mthread-manual-%{pkgversion}.pdf
+Source13:       https://frama-c.com/download/rte-manual-%{pkgversion}.pdf
+Source14:       https://frama-c.com/download/volatile-manual-%{pkgversion}.pdf
+Source15:       https://frama-c.com/download/wp-manual-%{pkgversion}.pdf
 # Icons created with gimp from the official upstream icon
-Source13:       %{name}-icons.tar.xz
-Source14:       com.%{name}.%{name}-gui.desktop
-Source15:       com.%{name}.%{name}-gui.metainfo.xml
-Source16:       acsl.el
-Source17:       frama-c.licensing
+Source16:       %{name}-icons.tar.xz
+Source17:       com.%{name}.%{name}-gui.desktop
+Source18:       com.%{name}.%{name}-gui.metainfo.xml
+Source19:       acsl.el
+Source20:       frama-c.licensing
 
 # Do not require the bytes library for OCaml 5.x
 Patch:          %{name}-bytes.patch
@@ -41,16 +41,14 @@ Patch:          %{name}-bytes.patch
 # Expose use of math library symbols to RPM
 Patch:          %{name}-mathlib.patch
 
-# Work around a change in dune behavior
-Patch:          %{name}-dune-bug.patch
+# Coq's plugin architecture requires cmxs files, so:
+ExclusiveArch:  %{ocaml_native_compiler}
 
-BuildRequires:  alt-ergo
+BuildSystem:    dune
 BuildRequires:  clang
 BuildRequires:  desktop-file-utils
 BuildRequires:  doxygen
 BuildRequires:  emacs-nw
-BuildRequires:  fdupes
-BuildRequires:  flamegraph
 BuildRequires:  graphviz
 BuildRequires:  libappstream-glib
 BuildRequires:  make
@@ -60,7 +58,6 @@ BuildRequires:  ocaml-dune > 3.13.0
 BuildRequires:  ocaml-dune-configurator-devel
 BuildRequires:  ocaml-dune-site-devel > 3.13.0
 BuildRequires:  ocaml-lablgtk3-devel >= 3.1.0
-BuildRequires:  ocaml-lablgtk3-sourceview3-devel
 BuildRequires:  ocaml-menhir >= 20181006
 BuildRequires:  ocaml-mlmpfr-devel
 BuildRequires:  ocaml-ocamlgraph-devel >= 2.2.0
@@ -76,15 +73,9 @@ BuildRequires:  ocaml-yojson-devel >= 2.0.1
 BuildRequires:  ocaml-zarith-devel >= 1.13
 BuildRequires:  ocaml-zip-devel
 BuildRequires:  ocaml-zmq-devel
-BuildRequires:  pandoc
 BuildRequires:  python3-devel
-BuildRequires:  %{py3_dist jsonschema}
-BuildRequires:  %{py3_dist pyyaml}
-BuildRequires:  time
 BuildRequires:  unix2dos
 BuildRequires:  why3
-BuildRequires:  yq
-BuildRequires:  z3
 
 Requires:       alt-ergo
 Requires:       flamegraph
@@ -139,13 +130,14 @@ marked up with ACSL.
 %autosetup -p1 -n %{name}-%{pkgversion}
 %setup -q -T -D -a 1 -n %{name}-%{pkgversion}
 %setup -q -T -D -a 2 -n %{name}-%{pkgversion}
-%setup -q -T -D -a 13 -n %{name}-%{pkgversion}
+%setup -q -T -D -a 16 -n %{name}-%{pkgversion}
 
 %conf
 # Copy in the manuals
 mkdir doc/manuals
 cp -p %{SOURCE3} %{SOURCE4} %{SOURCE5} %{SOURCE6} %{SOURCE7} %{SOURCE8} \
-   %{SOURCE9} %{SOURCE10} %{SOURCE11} %{SOURCE12} doc/manuals
+   %{SOURCE9} %{SOURCE10} %{SOURCE11} %{SOURCE12} %{SOURCE13} %{SOURCE14} \
+   %{SOURCE15} doc/manuals
 
 # Preserve timestamps when installing
 sed -ri 's/^CP[[:blank:]]+=.*/& -p/' share/Makefile.common
@@ -157,23 +149,18 @@ sed -ri 's/^CP[[:blank:]]+=.*/& -p/' share/Makefile.common
 %py3_shebang_fix tests/libc
 %py3_shebang_fix tests/syntax/cpp-command.t
 
-%build
-%dune_build
-
-%install
-%dune_install
-
+%install -a
 # Two of the man pages are duplicates, so make one a link to the other.
 cat > %{buildroot}%{_mandir}/man1/frama-c-gui.1 << EOF
 .so man1/frama-c.1
 EOF
 
 # Install the desktop file
-desktop-file-install --dir=%{buildroot}%{_datadir}/applications/ %{SOURCE14}
+desktop-file-install --dir=%{buildroot}%{_datadir}/applications/ %{SOURCE17}
 
 # Install the AppData file
 mkdir -p %{buildroot}%{_metainfodir}
-install -pm 644 %{SOURCE15} %{buildroot}%{_metainfodir}
+install -pm 644 %{SOURCE18} %{buildroot}%{_metainfodir}
 appstream-util validate-relax --nonet \
   %{buildroot}%{_metainfodir}/com.%{name}.%{name}-gui.metainfo.xml
 
@@ -197,7 +184,7 @@ chmod a-x %{buildroot}%{_emacs_sitelispdir}/*.el
 cd %{buildroot}%{_emacs_sitelispdir}
 %{_emacs_bytecompile} *.el
 mkdir -p %{buildroot}%{_emacs_sitestartdir}
-cp -p %{SOURCE16} %{buildroot}%{_emacs_sitestartdir}
+cp -p %{SOURCE19} %{buildroot}%{_emacs_sitestartdir}
 cd -
 
 # Remove files we don't actually want
@@ -224,30 +211,26 @@ if [ "%{_lib}" != "lib" ]; then
     sed -i '/EACSL_LIB/s,/lib/,/%{_lib}/,' %{buildroot}%{_bindir}/e-acsl-gcc
 fi
 
-# Link duplicate files
-%fdupes %{buildroot}%{ocamldir}
-%fdupes %{buildroot}%{_datadir}/frama-c
-%fdupes frama-c-api
-
-# FIXME: tests fail on ppc6le due to redefinition of bool
-# FIXME: test issue-eacsl-40.1.exec.wtests fails on aarch64
-%ifarch %{x86_64}
 %check
-# Skip a broken test for now
-rm -fr tests/fc_script/make-machdep.t
-sed -i '10,+4d' tests/fc_script/dune
-
-export PYTHONPATH=%{buildroot}%{ocamldir}/frama-c/lib/analysis-scripts
-why3 config detect
-# Parallel testing sometimes fails
-make default-tests PTESTS_OPTS=-error-code
-%endif
+# Starting with frama-c 33.0, the tests don't work at all
+# They seem to need a non-release build now.
+#%%ifarch %%{x86_64}
+## Skip a broken test for now
+#rm -fr tests/fc_script/make-machdep.t
+#sed -i '10,+4d' tests/fc_script/dune
+#
+#export PYTHONPATH=%%{buildroot}%%{ocamldir}/frama-c/lib/analysis-scripts
+#why3 config detect
+## Parallel testing sometimes fails
+#make default-tests PTESTS_OPTS=-error-code
+#%%endif
 
 %files
 %doc README.md VERSION
 %license licenses/*
 %{_bindir}/e-acsl-gcc
 %{_bindir}/frama-c*
+%{ocamldir}/crowbar_utils/
 %{ocamldir}/frama-c*
 %{ocamldir}/qed/
 %{ocamldir}/stublibs/dllframa_c_kernel_stubs.so

diff --git a/sources b/sources
index 74aefe2..3f21227 100644
--- a/sources
+++ b/sources
@@ -1,14 +1,17 @@
-SHA512 (frama-c-32.1-Germanium.tar.gz) = 31fd15520b8ef70a8681907787bb36dfd55d72819941e8772170ee0ebc6f5beaa1023bde3e36f247a1665fa5c131a25f573c3aea12c441b4f2a36951481f6af1
-SHA512 (frama-c-32.1-Germanium-api.tar.gz) = 048ebc366a30956a86625e7a02502c5c89ab63d38b1c003df555523cfe92b39bd42c3fe3e63c02ce1650f49b101334ab7f17432ee9e659e20f2f0d2926528feb
-SHA512 (frama-c-server-32.1-Germanium-api.tar.gz) = c3f13533ae739e54e727820439cbd0f4f8b28e23d8f195e4b715bbd3e4d30bd89ec718b383681ed6bea16b2182fa8527c38707c3a8013c116db62cecd315562b
+SHA512 (frama-c-33.0-Arsenic.tar.gz) = dd2e0559420946d0fa66f736c2e63aacd6546126a02bb3c8b0f96ebdcbfe6743736ba5701a8d6d89740ef6ec8a2974c8a3033712ac828a57ce976e2def883e80
+SHA512 (frama-c-33.0-Arsenic-api.tar.gz) = d5154b5528922460a709e41e7ace187cb29376b33e316a24b17e6a689713666059f05111bd19db3727c39f03b5db72ac0eb5ed3e94077828217adfe555bdbba3
+SHA512 (frama-c-server-33.0-Arsenic-api.tar.gz) = 83c0241bb1d4f3799eb95f2d6d4e33c5a2d04d5dd178a49583fde04fafd1b6fb544da0fa7bd15f8b41a70e319e4fce94006e0d7bc9a2666b1fdbc72b6dc2edad
 SHA512 (frama-c-icons.tar.xz) = 9fb1f6fc32559cfb74491c7f284c4c111d1ce0720fecca8a84713cb68bfa1c77cbeb241c720f58ef0a1140076d2d324f1dcae6cb47650e73c7915e82b2a6914d
-SHA512 (acsl-implementation-32.1-Germanium.pdf) = 0987de22358f682218fb7879a7c08760aee682ca7b5d5c78385afd5e6cd666c7ecb7eb1ee12f42fa07689f8d6043649bfab0d4965772a194e247d077e6d638d8
-SHA512 (aorai-manual-32.1-Germanium.pdf) = 7f33e119c5fdec6fd25acc960f7f2201e93bf0ac7ea2103051bd1b611714d637a789baf5d00a606b420527420e7adae7b9638e4db0246e1c370a8a319a5821d8
-SHA512 (e-acsl-implementation-32.1-Germanium.pdf) = fb5c6168ac11944009aaab7e32e8d24ec387e641ac115eba46fd84c1fc670651b94acea83acc0c4e2c7e63f500b74d58b5513a5c214f274494ba8105c9fcc669
-SHA512 (e-acsl-manual-32.1-Germanium.pdf) = 0470d3b63fdc89dce1b027c6618a2a1ec557cdceba5b96c16d8507f91c5a3bd4b408858031a56f4d73c6ab2a9e3337f89991f4df454de212ccad1bc4091a7d0b
-SHA512 (eva-manual-32.1-Germanium.pdf) = 6169f5689850ff80fe64f043320d333647e1de521ec327e471910a61576f702ed25e6f9d0c7175abcd1252cbbe50410e68a47fb2aba588aea97c8eb7f5c67b67
-SHA512 (metrics-manual-32.1-Germanium.pdf) = 2336fb61cafca5de45d1f0bf342ae6247a4934b776d81de56a770793e4b2dadb352f7e4cd56778bf1e0e5bfe268cafe90712b31333de8c6c4d73ff0fb896501a
-SHA512 (plugin-development-guide-32.1-Germanium.pdf) = 4855838b72583ee28d46cd6958bbddf4d02debb00e803992b43ab44d623bccef40507f0de3a2c6ca6ea539c7f1e99e2228b86d657b17c4ff7235acff31a3ae82
-SHA512 (rte-manual-32.1-Germanium.pdf) = aca04fc669141aaaa06455019c35b6e29e41cf91333e1fe027fa594520c3c2387879d4fa9b8faa8c442dca31719dac80ca20aecd0ca98a4a694305ab423d8c62
-SHA512 (user-manual-32.1-Germanium.pdf) = 3993943c8e06b2d808de3fee08b155e3ac8102c7cc5980d358e4c06554c12e9e0b2ca2f820ee8fbd40b0b57410c6cf421a984195a0f70a2db65b9845974c19cb
-SHA512 (wp-manual-32.1-Germanium.pdf) = 016d366aa47c1bca619ebc5e957d9f385a56b7afc2fc2de2dc79ec402a77b27517714adb2361c6746d672485fcedb95e10bf3dbde4e09cff864d255c15e46d78
+SHA512 (acsl-implementation-33.0-Arsenic.pdf) = 200e32f0b80062b410bf271508fc662e5f33de822e552c7e9e75df5c9bed1088a707ff83b637f9836365fcae79a9c1fd30f7182b2eec88bd21114b1a2ca1c531
+SHA512 (acsl-importer-manual-33.0-Arsenic.pdf) = 207f1a524b1b05fa5610894c5aa7b72a4536a2aa28b15f3f6c84b32933916dbdaec7761870e7d8857c78b9840e5a697c699c6bc06155e8aacc9f2c87d8c6d430
+SHA512 (aorai-manual-33.0-Arsenic.pdf) = a557b6d89a68a098c06f33e7884aeadd7ceb3ecfeaf672beb10e6d05f20653ac18d954af04a7eee4f149d5f059f9b5f7beb36914a031942d3f40a8a5b0c83efc
+SHA512 (e-acsl-implementation-33.0-Arsenic.pdf) = 42df93b714314dd106b3516b9b8d8588b3f320f944fb2249032f4172f5f016412b24a6ad71294edd022e67a09a863ba63402e8d7c9a56ea32fc4d696da9bc772
+SHA512 (e-acsl-manual-33.0-Arsenic.pdf) = 6174163afe7b84f579cf9d20f520fa92e2f356d710dd74587bf6ee2ab46c5736cc0d8bc0a1b09a7c65a686bff06641e6f8da94023631f59832ad80ca5b7235fb
+SHA512 (eva-manual-33.0-Arsenic.pdf) = 8d3273403df27e34251701b5a752b4e1ce9f20149f98542571e9c7a07ea1b5fbd8a704b7ec2d73e2bb7f72d05f51d7b958e6febe8af6a30b4594b3a76ab729f7
+SHA512 (metrics-manual-33.0-Arsenic.pdf) = 70b3259d8e774dd362ddfef2612dea54172d1d3e3805e8a4d5644ac8c1931f9277c8cd5268081b6e20d2edaa0253e0c1e33f4a7799768c0d745d80415635c6c8
+SHA512 (mthread-manual-33.0-Arsenic.pdf) = 26eca6a0416353b08340fa64edd1c41e24f7f3db7e1928e6a7a0be5640e178e5a93153a45fcbf32c7bee6bef490e4cc47b731c47e9e761c69998aa95b934b444
+SHA512 (plugin-development-guide-33.0-Arsenic.pdf) = 41d1df41c641c515589c3003e80ceafb0d9a9de616dc5c6583b7a53fdca4be1b1170ab1221817cfe3933c4b4c8a11d9673e06563f0d879101b0faea89cb664ff
+SHA512 (rte-manual-33.0-Arsenic.pdf) = 8d3e5bbea9ec4c57d77afaeb8147628077595f05d3d54936b92d0fd3129c83cdb9dc04da61f13d3ef6a67e2d7cc51f33c15b9b484b006ab94231469ab1d76e82
+SHA512 (user-manual-33.0-Arsenic.pdf) = 83da5b5a0b411dea3f8b71ab9a03e622767ad80ed59dfbed88d769920ab300918892e68d45b8b5db8cf219a89f82386b46205fa76a32818cdbffb4954b85872d
+SHA512 (volatile-manual-33.0-Arsenic.pdf) = a70cb68f8a10fb58cc11ed5254d9a6dca230e8ce2579aa3b8ba2afc07c49c630d8b684092181c28b448a75274f80a5f35066c68402d10ab17a5cd44cadc4884f
+SHA512 (wp-manual-33.0-Arsenic.pdf) = c9cd47247eaa4d063da89f38693f57f489a3735c403afb55c9df0594a29370d43b509d1ceb5eae641099f46871d77bcc01b70d757da53377247a15d060d21d80