diff --git a/.gitignore b/.gitignore
index 06444e4..d952138 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,6 +2,7 @@
/frama-c-*.tar.gz
/acsl-implementation-*.pdf
/aorai-manual-*.pdf
+/e-acsl-implementation*.pdf
/e-acsl-manual*.pdf
/eva-manual-*.pdf
/metrics-manual-*.pdf
diff --git a/frama-c-gui.appdata.xml b/frama-c-gui.appdata.xml
index 1f51270..fb35ac1 100644
--- a/frama-c-gui.appdata.xml
+++ b/frama-c-gui.appdata.xml
@@ -20,27 +20,27 @@
- http://frama-c.com/media/first.png
+ https://www.frama-c.com/assets/img/home/gui-overview.png
Analysis of first.c
- http://frama-c.com/media/first_S.png
- Informational messages for first.c
+ https://www.frama-c.com/assets/img/home/value-analysis.png
+ Value analysis of first.c
- http://frama-c.com/media/first_effect.png
- Effect of a modification statement
+ https://www.frama-c.com/assets/img/home/effect-analysis.png
+ Effect analysis of first.c
- http://frama-c.com/media/first_defs.png
- Show definitions
+ https://www.frama-c.com/assets/img/home/dep-analysis.png
+ Dependency analysis of first.c
- http://frama-c.com/media/first_impact.png
- Impact analysis
+ https://www.frama-c.com/assets/img/home/impact-analysis.png
+ Impact analysis of first.c
- frama-c-discuss@lists.gforge.inria.fr
- http://frama-c.com/
+ frama-c-discuss@groupes.renater.fr
+ https://frama-c.com/
https://bts.frama-c.com/
diff --git a/frama-c.spec b/frama-c.spec
index 51ac817..b290503 100644
--- a/frama-c.spec
+++ b/frama-c.spec
@@ -7,32 +7,33 @@
%endif
Name: frama-c
-Version: 21.1
-Release: 7%{?dist}
+Version: 22.0
+Release: 1%{?dist}
Summary: Framework for source code analysis of C software
-%global pkgversion %{version}-Scandium
+%global pkgversion %{version}-Titanium
# Licensing breakdown in source file frama-c-1.6-licensing
License: LGPLv2 and GPLv2 and GPLv2+ and BSD and QPL
-URL: http://frama-c.com/
-Source0: http://frama-c.com/download/%{name}-%{pkgversion}.tar.gz
-Source1: http://frama-c.com/download/%{name}-%{pkgversion}-api.tar.gz
+URL: https://frama-c.com/
+Source0: https://frama-c.com/download/%{name}-%{pkgversion}.tar.gz
+Source1: https://frama-c.com/download/%{name}-%{pkgversion}-api.tar.gz
Source2: frama-c-1.6.licensing
Source3: %{name}-gui.desktop
Source4: %{name}-gui.appdata.xml
Source5: acsl.el
-Source6: http://frama-c.com/download/user-manual-%{pkgversion}.pdf
-Source7: http://frama-c.com/download/plugin-development-guide-%{pkgversion}.pdf
-Source8: http://frama-c.com/download/acsl-implementation-%{pkgversion}.pdf
-Source9: http://frama-c.com/download/aorai-manual-%{pkgversion}.pdf
-Source10: http://frama-c.com/download/metrics-manual-%{pkgversion}.pdf
-Source11: http://frama-c.com/download/rte-manual-%{pkgversion}.pdf
-Source12: http://frama-c.com/download/eva-manual-%{pkgversion}.pdf
-Source13: http://frama-c.com/download/wp-manual-%{pkgversion}.pdf
-Source14: http://frama-c.com/download/e-acsl/e-acsl-manual-%{pkgversion}.pdf
# Icons created with gimp from the official upstream icon
-Source15: %{name}-icons.tar.xz
+Source6: %{name}-icons.tar.xz
+Source7: https://frama-c.com/download/user-manual-%{pkgversion}.pdf
+Source8: https://frama-c.com/download/plugin-development-guide-%{pkgversion}.pdf
+Source9: https://frama-c.com/download/acsl-implementation-%{pkgversion}.pdf
+Source10: https://frama-c.com/download/aorai-manual-%{pkgversion}.pdf
+Source11: https://frama-c.com/download/e-acsl/e-acsl-manual-%{pkgversion}.pdf
+Source12: https://frama-c.com/download/e-acsl/e-acsl-implementation-%{pkgversion}.pdf
+Source13: https://frama-c.com/download/eva-manual-%{pkgversion}.pdf
+Source14: https://frama-c.com/download/metrics-manual-%{pkgversion}.pdf
+Source15: https://frama-c.com/download/rte-manual-%{pkgversion}.pdf
+Source16: https://frama-c.com/download/wp-manual-%{pkgversion}.pdf
# https://bugzilla.redhat.com/show_bug.cgi?id=1874879
ExcludeArch: s390x
@@ -42,6 +43,7 @@ BuildRequires: coq
BuildRequires: desktop-file-utils
BuildRequires: doxygen
BuildRequires: emacs xemacs-nox xemacs-packages-base
+BuildRequires: flamegraph
BuildRequires: graphviz
BuildRequires: libgnomecanvas-devel
BuildRequires: libtool
@@ -64,6 +66,7 @@ BuildRequires: ocaml-yojson-devel
BuildRequires: ocaml-zarith-devel
BuildRequires: ocaml-zmq-devel
BuildRequires: python3-devel
+BuildRequires: time
BuildRequires: why3
BuildRequires: z3
@@ -126,7 +129,7 @@ files marked up with ACSL.
%prep
%autosetup -n %{name}-%{pkgversion} -p0
%setup -q -T -D -a 1 -n %{name}-%{pkgversion}
-%setup -q -T -D -a 15 -n %{name}-%{pkgversion}
+%setup -q -T -D -a 6 -n %{name}-%{pkgversion}
fixtimestamp() {
touch -r $1.orig $1
@@ -135,8 +138,8 @@ fixtimestamp() {
# Copy in the manuals
mkdir doc/manuals
-cp -p %{SOURCE6} %{SOURCE7} %{SOURCE8} %{SOURCE9} %{SOURCE10} %{SOURCE11} \
- %{SOURCE12} %{SOURCE13} %{SOURCE14} doc/manuals
+cp -p %{SOURCE7} %{SOURCE8} %{SOURCE9} %{SOURCE10} %{SOURCE11} %{SOURCE12} \
+ %{SOURCE13} %{SOURCE14} %{SOURCE15} %{SOURCE16} doc/manuals
# Link with the Fedora LDFLAGS
sed -i "/OLINKFLAGS/s|-linkall|& -runtime-variant _pic -ccopt '$RPM_LD_FLAGS'|" Makefile
@@ -147,16 +150,22 @@ sed -ri 's/^CP[[:blank:]]+=.*/& -p/' share/Makefile.common
# Build buckx with the right flags
sed -i "s|-O3 -Wall|%{optflags} -fPIC|" Makefile
-# Use python3
-sed -i.orig 's,env python$,python3,' share/analysis-scripts/list_files.py
-fixtimestamp share/analysis-scripts/list_files.py
-
# Do not use env
-for fil in share/analysis-scripts/{find_fun,make_template,make_wrapper,summary}.py; do
+for fil in share/analysis-scripts/{find_fun,function_finder,list_files,make_template,make_wrapper,normalize_jcdb,summary}.py; do
sed -i.orig 's,%{_bindir}/env python3,%{_bindir}/python3,' $fil
fixtimestamp $fil
done
+%ifarch %{ocaml_native_compiler}
+# Some tests run the bytecode toplevel. This fails because why3 is built with
+# native code, not bytecode, so %%{_libdir}/ocaml/why3/why3.cma does not exist.
+sed -i 's/toplevel\.byte/toplevel.opt/g' \
+ tests/dynamic/dynamic.i \
+ tests/journal/control.i \
+ tests/journal/control2.c \
+ tests/pdg/dyn_dpds.c
+%endif
+
%build
# This option prints the actual make commands so we can see what's
# happening (eg: for debugging the spec file)
@@ -240,6 +249,9 @@ chmod 0644 src/plugins/value/domains/apron/*.ml
rm -f %{buildroot}%{_datadir}/frama-c/analysis-scripts/flamegraph.pl
ln -s %{_bindir}/flamegraph.pl %{buildroot}%{_datadir}/frama-c/analysis-scripts
+%check
+%make_build PTESTS_OPTS=-error-code tests
+
%files
%doc VERSION
%license licenses/*
@@ -257,12 +269,13 @@ ln -s %{_bindir}/flamegraph.pl %{buildroot}%{_datadir}/frama-c/analysis-scripts
%doc doc/code/*.{css,htm,txt}
%doc doc/manuals/acsl-implementation-%{pkgversion}.pdf
%doc doc/manuals/aorai-manual-%{pkgversion}.pdf
+%doc doc/manuals/e-acsl-implementation-%{pkgversion}.pdf
%doc doc/manuals/e-acsl-manual-%{pkgversion}.pdf
+%doc doc/manuals/eva-manual-%{pkgversion}.pdf
%doc doc/manuals/metrics-manual-%{pkgversion}.pdf
%doc doc/manuals/plugin-development-guide-%{pkgversion}.pdf
%doc doc/manuals/rte-manual-%{pkgversion}.pdf
%doc doc/manuals/user-manual-%{pkgversion}.pdf
-%doc doc/manuals/eva-manual-%{pkgversion}.pdf
%doc doc/manuals/wp-manual-%{pkgversion}.pdf
%doc frama-c-api
@@ -275,6 +288,10 @@ ln -s %{_bindir}/flamegraph.pl %{buildroot}%{_datadir}/frama-c/analysis-scripts
%{_xemacs_sitestartdir}/acsl.el
%changelog
+* Fri Nov 20 2020 Jerry James - 22.0-1
+- Update to Titanium 22.0
+- Add %%check script
+
* Mon Nov 16 2020 Jerry James - 21.1-7
- Rebuild for ocaml-zarith 1.11
diff --git a/sources b/sources
index 93e6ca0..d017b71 100644
--- a/sources
+++ b/sources
@@ -1,12 +1,13 @@
-SHA512 (frama-c-21.1-Scandium.tar.gz) = 57562f7f9779f040fd12a881b358383a495990f9cdc0da6d03799591ece291710a1805e32eb0cac1703974edd090a6999a2940a84f3247204715c497e4235ab5
-SHA512 (frama-c-21.1-Scandium-api.tar.gz) = 327f1c989fa2fb1e522208e1946d3c3e9d422a3e59afcfc9f87435994c18d544fac1e923ed59c12cdde413762c9603d67fd8bd7da85b7c84be23daeb5009be56
+SHA512 (frama-c-22.0-Titanium.tar.gz) = 7366127da4726ffec0022adc06fd867b6ea37fc23b6a5ddccbe7562fcaa635abc6894397d0101fcb0afc339c565299c6d637006305c8331aa62a8ce734740a0f
+SHA512 (frama-c-22.0-Titanium-api.tar.gz) = 8719439d483612fc6da3acbf5f0c55f2ededd5f11c899724937c98fa366a216b91e93afa84598bc4ad8e4fa52073bc5e79e28625f6770df3fa1d955bd0d6fd7b
SHA512 (frama-c-icons.tar.xz) = 9fb1f6fc32559cfb74491c7f284c4c111d1ce0720fecca8a84713cb68bfa1c77cbeb241c720f58ef0a1140076d2d324f1dcae6cb47650e73c7915e82b2a6914d
-SHA512 (acsl-implementation-21.1-Scandium.pdf) = e79a20708da174aa8961563b6936c8c07c5352c1092b6fff7a5620e3d78a487ecb8ca77f9f2918b5561a44870b1b381e8a6154a113f8cc0558ac558c1ec699ca
-SHA512 (aorai-manual-21.1-Scandium.pdf) = 54e4e37987f9dbe85f75e3c148665672cd77027ad911ddb4009456d40176507c9a5c3dfeaf30966c5c5971f148513f791b4268113be6ab6ee64d4a81931e5e6b
-SHA512 (e-acsl-manual-21.1-Scandium.pdf) = a82831637a55e839f57e3102a95822974cc03b9461ad3c86c4a56746f8d4b4eb4d60f7563014b2e7d309aa906001aa80508da47c7079c883aeb55b8853f0449d
-SHA512 (eva-manual-21.1-Scandium.pdf) = 1fd4a192c814e79c0a621b56a404d66a1a5d5df829ed418089cc79d958c381077545dca9ec52a40d69abed9444d35d7356ac84af1c4d1178b8a9be67c8b83fd0
-SHA512 (metrics-manual-21.1-Scandium.pdf) = 17ece00a5d14554491f805e5bd8059a7faf929bae2e33cb10703f7b5349e8066404a5afc381ce4dfe9d356eac8ef89e7766fc08d5e13840e2091eb756b32ad32
-SHA512 (plugin-development-guide-21.1-Scandium.pdf) = 089a357a739ede02d2aa5cd9954cb7f544e231014814c80622df0b4e441b62041b4a664a571af6d9171cd72565aa9d968b1db51d5046a52fe79e40f324259cf7
-SHA512 (rte-manual-21.1-Scandium.pdf) = d91468a7b95817f557bbfd55bd08ac55326045e827bf9900e821187179fac8e18910930c7129b67b28052cf8c7b3c7f3e0150b6d80b9722303f8ad19443c4c1c
-SHA512 (user-manual-21.1-Scandium.pdf) = 2a8e3c37c81c89943e8e79a0d7b6eb66861bfa263d823371f807c877089a577db8d741997cfc23c572c7459e3be8fbbfc38b781a790d49be2433411b58f564c9
-SHA512 (wp-manual-21.1-Scandium.pdf) = ac410e32b8973dc81c3912ab33bd31653582ad5c8bfbb23117a63412ae653eb7606e6ccbc71ce6454e70854d6a39a85dff09af6883541b74a0d3a49025c9c09c
+SHA512 (acsl-implementation-22.0-Titanium.pdf) = 9062d4f453f400031226b579da36078b2cfdc5bba927099f27c9b62151a1f51ea3d9e789d9d2b22dc5273bcee9d660b973c709c26596904bc8095d9c3b372a89
+SHA512 (aorai-manual-22.0-Titanium.pdf) = 54f17a74c4050a0b14d51040d7febb984ffa364334b6008bc99b6e0f28d6b8bf0b4c30a9fcb9d072883fa432bf6a20ffb944a5d4dcc495ce5e2a0fdd0b3d4449
+SHA512 (e-acsl-implementation-22.0-Titanium.pdf) = 09f87160f178f676d0fce6b0f33cd0bb18583a5b66c5f14cfe4d8913a9fb20478ae47e9e7cf3ec26199dc1d7dd3d49d1b26cf57235197ab2c015a4010df9abd5
+SHA512 (e-acsl-manual-22.0-Titanium.pdf) = 77e9c57d0fff37c00440902b8c3f3815d1303d86b5323182c7e0d541c6f9e84c87128911922d91e6712e65b3428e3aee83fdf7fa11fa1b275ea04345a00cfe5a
+SHA512 (eva-manual-22.0-Titanium.pdf) = 6aba144e4030ea05c2c3e8d7d51631dba09f8dff11e7d60428ff0f04891eb165d88248b31953353b7ae934c2fda40f70b1006c69fe211737a2f26be1d6433bf2
+SHA512 (metrics-manual-22.0-Titanium.pdf) = bb55a233d44bda8949d70d2585f4f5c4f47d6edf5a9e84cf5e6453ccd51f3c56de75f5dcd222079cd5976cdb13c21b3e2a13b507a643e5bbf55f8a0faec0c340
+SHA512 (plugin-development-guide-22.0-Titanium.pdf) = e596abc4ba291b44fa9695d6463aaeeb00c76bf624619312999b2e5ae370eeb563a16b9a541e73cab1e873eef36f288223e05e8802677cd733c43b649bc715a6
+SHA512 (rte-manual-22.0-Titanium.pdf) = ff2409b7ced36ca81e06ab5fd2cff550143c2461ad91806cf19a120ca72ceddb16ae1f376763006322d061d3892bcc0826a7c4eeb17c49fd2417431c5738dde7
+SHA512 (user-manual-22.0-Titanium.pdf) = 528533ee0957bc6c279a772381f2d90642cefddb808deddbd28bac5a351594e2a0d9191c479970bed61ae0d9f5a52a07ee0736f44ae9d31fcd46515f2fd5c0ef
+SHA512 (wp-manual-22.0-Titanium.pdf) = f0a457c816cd64dd8029ef43b86bf1065d0d3b47762a503ec15ccd1651b32bfc215035ed6ecf4b401039aaa97dca5a2c9d97454903c7e06f605d3d489ce32481