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