From 3fe032a86695282afb44f26984abe41f6211ba8b Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mar 24 2017 19:58:55 +0000 Subject: Update to Silicon version. --- diff --git a/.gitignore b/.gitignore index 07e80ed..a6da18f 100644 --- a/.gitignore +++ b/.gitignore @@ -1,14 +1,4 @@ /frama-c-icons.tar.xz -/frama-c-Magnesium-20151002.tar.gz -/frama-c-Magnesium-20151002_api.tar.gz -/acsl-implementation-Magnesium-20151002.pdf -/aorai-manual-Magnesium-20151002.pdf -/metrics-manual-Magnesium-20151002.pdf -/plugin-development-guide-Magnesium-20151002.pdf -/rte-manual-Magnesium-20151002.pdf -/user-manual-Magnesium-20151002.pdf -/value-analysis-Magnesium-20151002.pdf -/wp-manual-Magnesium-20151002.pdf /frama-c-Aluminium-20160501.tar.gz /frama-c-Aluminium-20160501_api.tar.gz /acsl-implementation-Aluminium-20160501.pdf @@ -19,3 +9,13 @@ /user-manual-Aluminium-20160501.pdf /value-analysis-Aluminium-20160501.pdf /wp-manual-Aluminium-20160501.pdf +/frama-c-Silicon-20161101.tar.gz +/frama-c-Silicon-20161101_api.tar.gz +/acsl-implementation-Silicon-20161101.pdf +/aorai-manual-Silicon-20161101.pdf +/metrics-manual-Silicon-20161101.pdf +/plugin-development-guide-Silicon-20161101.pdf +/rte-manual-Silicon-20161101.pdf +/user-manual-Silicon-20161101.pdf +/value-analysis-Silicon-20161101.pdf +/wp-manual-Silicon-20161101.pdf diff --git a/frama-c-ocaml-4-04.patch b/frama-c-ocaml-4-04.patch deleted file mode 100644 index 64459ef..0000000 --- a/frama-c-ocaml-4-04.patch +++ /dev/null @@ -1,73 +0,0 @@ -diff -ur frama-c-Aluminium-20160501.old/src/kernel_services/plugin_entry_points/db.ml frama-c-Aluminium-20160501/src/kernel_services/plugin_entry_points/db.ml ---- frama-c-Aluminium-20160501.old/src/kernel_services/plugin_entry_points/db.ml 2016-05-30 15:15:22.000000000 +0100 -+++ frama-c-Aluminium-20160501/src/kernel_services/plugin_entry_points/db.ml 2016-11-08 14:08:20.571465782 +0000 -@@ -1071,9 +1071,12 @@ - { state_opt: bool option; - ki_opt: (stmt * bool) option; - kf:Kernel_function.t } -- let mk_ctx_func_contrat = mk_fun "Interp.To_zone.mk_ctx_func_contrat" -- let mk_ctx_stmt_contrat = mk_fun "Interp.To_zone.mk_ctx_stmt_contrat" -- let mk_ctx_stmt_annot = mk_fun "Interp.To_zone.mk_ctx_stmt_annot" -+ let mk_ctx_func_contrat : (Cil_types.kernel_function -> state_opt:bool option -> t_ctx) ref -+ = mk_fun "Interp.To_zone.mk_ctx_func_contrat" -+ let mk_ctx_stmt_contrat : (Cil_types.kernel_function -> Cil_types.stmt -> state_opt:bool option -> t_ctx) ref -+ = mk_fun "Interp.To_zone.mk_ctx_stmt_contrat" -+ let mk_ctx_stmt_annot : (Cil_types.kernel_function -> Cil_types.stmt -> t_ctx) ref -+ = mk_fun "Interp.To_zone.mk_ctx_stmt_annot" - type t = {before:bool ; ki:stmt ; zone:Locations.Zone.t} - type t_zone_info = (t list) option - type t_decl = -@@ -1082,15 +1085,29 @@ - type t_pragmas = - { ctrl: Stmt.Set.t; - stmt: Stmt.Set.t } -- let from_term = mk_fun "Interp.To_zone.from_term" -- let from_terms= mk_fun "Interp.To_zone.from_terms" -- let from_pred = mk_fun "Interp.To_zone.from_pred" -- let from_preds= mk_fun "Interp.To_zone.from_preds" -- let from_zone = mk_fun "Interp.To_zone.from_zone" -- let from_stmt_annot= mk_fun "Interp.To_zone.from_stmt_annot" -- let from_stmt_annots= mk_fun "Interp.To_zone.from_stmt_annots" -- let from_func_annots= mk_fun "Interp.To_zone.from_func_annots" -- let code_annot_filter= mk_fun "Interp.To_zone.code_annot_filter" -+ let from_term : (Cil_types.term -> t_ctx -> t_zone_info * t_decl) ref -+ = mk_fun "Interp.To_zone.from_term" -+ let from_terms : (Cil_types.term list -> t_ctx -> t_zone_info * t_decl) ref -+ = mk_fun "Interp.To_zone.from_terms" -+ let from_pred : (Cil_types.predicate Cil_types.named -> t_ctx -> t_zone_info * t_decl) ref -+ = mk_fun "Interp.To_zone.from_pred" -+ let from_preds : (Cil_types.predicate Cil_types.named list -> t_ctx -> t_zone_info * t_decl) ref -+ = mk_fun "Interp.To_zone.from_preds" -+ let from_zone : (Cil_types.identified_term -> t_ctx -> t_zone_info * t_decl) ref -+ = mk_fun "Interp.To_zone.from_zone" -+ let from_stmt_annot : (Cil_types.code_annotation -> Cil_types.stmt * Cil_types.kernel_function -> (t_zone_info * t_decl) * t_pragmas) ref -+ = mk_fun "Interp.To_zone.from_stmt_annot" -+ let from_stmt_annots : ((Cil_types.code_annotation -> bool) option -> -+ Cil_types.stmt * Cil_types.kernel_function -> -+ (t_zone_info * t_decl) * t_pragmas) -+ ref -+ = mk_fun "Interp.To_zone.from_stmt_annots" -+ let from_func_annots : (((Cil_types.stmt -> unit) -> Cil_types.kernel_function -> unit) -> -+ (Cil_types.code_annotation -> bool) option -> -+ Cil_types.kernel_function -> (t_zone_info * t_decl) * t_pragmas) -+ ref -+ = mk_fun "Interp.To_zone.from_func_annots" -+ let code_annot_filter = mk_fun "Interp.To_zone.code_annot_filter" - end - - let to_result_from_pred = -diff -ur frama-c-Aluminium-20160501.old/src/plugins/loop_analysis/region_analysis_stmt.ml frama-c-Aluminium-20160501/src/plugins/loop_analysis/region_analysis_stmt.ml ---- frama-c-Aluminium-20160501.old/src/plugins/loop_analysis/region_analysis_stmt.ml 2016-05-30 15:15:22.000000000 +0100 -+++ frama-c-Aluminium-20160501/src/plugins/loop_analysis/region_analysis_stmt.ml 2016-11-08 14:11:21.254547316 +0000 -@@ -31,7 +31,10 @@ - type node = Cil_types.stmt - let pretty = Cil_datatype.Stmt.pretty - let equal = Cil_datatype.Stmt.equal -- module Set = Cil_datatype.Stmt.Set;; -+ module Set = struct -+ include Cil_datatype.Stmt.Set -+ let map _ _ = assert false -+ end;; - - module Graph = struct - diff --git a/frama-c.spec b/frama-c.spec index 5991bc8..c02857f 100644 --- a/frama-c.spec +++ b/frama-c.spec @@ -7,11 +7,11 @@ %global debug_package %{nil} %endif -%global pkgversion Aluminium-20160501 +%global pkgversion Silicon-20161101 Name: frama-c -Version: 1.13 -Release: 8%{?dist} +Version: 1.14 +Release: 1%{?dist} Summary: Framework for source code analysis of C software # Licensing breakdown in source file frama-c-1.6-licensing @@ -34,9 +34,6 @@ Source13: http://frama-c.com/download/wp-manual-%{pkgversion}.pdf # Icons created with gimp from the official upstream icon Source14: %{name}-icons.tar.xz -# Small fixes for OCaml 4.04.0. -Patch1: frama-c-ocaml-4-04.patch - BuildRequires: alt-ergo BuildRequires: coq BuildRequires: desktop-file-utils @@ -93,10 +90,6 @@ Requires: %{name} = %{version}-%{release} Requires: emacs(bin) BuildArch: noarch -# This can be removed after F-23 reaches EOL. -Obsoletes: %{name}-emacs-el < 1.11-9 -Provides: %{name}-emacs-el = %{version}-%{release} - %description emacs This package contains an Emacs support file for working with C source files marked up with ACSL. @@ -108,10 +101,6 @@ Requires: %{name} = %{version}-%{release} Requires: xemacs(bin), xemacs-packages-extra BuildArch: noarch -# This can be removed after F-23 reaches EOL. -Obsoletes: %{name}-xemacs-el < 1.11-9 -Provides: %{name}-xemacs-el = %{version}-%{release} - %description xemacs This package contains an XEmacs support file for working with C source files marked up with ACSL. @@ -121,8 +110,6 @@ files marked up with ACSL. %setup -q -T -D -a 1 -n %{name}-%{pkgversion} %setup -q -T -D -a 14 -n %{name}-%{pkgversion} -%patch1 -p1 - # Copy in the manuals mkdir doc/manuals cp -p %{SOURCE6} %{SOURCE7} %{SOURCE8} %{SOURCE9} %{SOURCE10} %{SOURCE11} \ @@ -184,18 +171,19 @@ cp -a icons %{buildroot}%{_datadir}/icons/hicolor # Install and bytecompile the XEmacs file mkdir -p %{buildroot}%{_xemacs_sitelispdir} -cp -p share/acsl.el %{buildroot}%{_xemacs_sitelispdir} +cp -p share/emacs/*.el %{buildroot}%{_xemacs_sitelispdir} pushd %{buildroot}%{_xemacs_sitelispdir} -%{_xemacs_bytecompile} acsl.el +%{_xemacs_bytecompile} *.el mkdir -p %{buildroot}%{_xemacs_sitestartdir} cp -p %{SOURCE5} %{buildroot}%{_xemacs_sitestartdir} # Install and bytecompile the Emacs file mkdir -p %{buildroot}%{_emacs_sitelispdir} -mv %{buildroot}%{_datadir}/frama-c/acsl.el %{buildroot}%{_emacs_sitelispdir} -chmod a-x %{buildroot}%{_emacs_sitelispdir}/acsl.el +mv %{buildroot}%{_datadir}/frama-c/emacs/*.el %{buildroot}%{_emacs_sitelispdir} +rmdir %{buildroot}%{_datadir}/frama-c/emacs +chmod a-x %{buildroot}%{_emacs_sitelispdir}/*.el cd %{buildroot}%{_emacs_sitelispdir} -%{_emacs_bytecompile} acsl.el +%{_emacs_bytecompile} *.el mkdir -p %{buildroot}%{_emacs_sitestartdir} cp -p %{SOURCE5} %{buildroot}%{_emacs_sitestartdir} popd @@ -251,14 +239,17 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : %doc frama-c-api %files emacs -%{_emacs_sitelispdir}/acsl.el* +%{_emacs_sitelispdir}/*.el* %{_emacs_sitestartdir}/acsl.el %files xemacs -%{_xemacs_sitelispdir}/acsl.el* +%{_xemacs_sitelispdir}/*.el* %{_xemacs_sitestartdir}/acsl.el %changelog +* Fri Mar 24 2017 Jerry James - 1.14-1 +- Update to Silicon version + * Fri Feb 10 2017 Fedora Release Engineering - 1.13-8 - Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild diff --git a/sources b/sources index 0c04960..3cb4b1b 100644 --- a/sources +++ b/sources @@ -1,11 +1,11 @@ -e52271640aebcccab894ae038c9579aa frama-c-Aluminium-20160501.tar.gz -317bfdaa7ca695e504270782c4b0e785 frama-c-Aluminium-20160501_api.tar.gz -405ae0542c80b9b49f1b9d23ca6131e3 acsl-implementation-Aluminium-20160501.pdf -018a4f1a635dc620d1e4bca75e8b2997 aorai-manual-Aluminium-20160501.pdf -263f80018f705aa9d29b7be2e74443ad metrics-manual-Aluminium-20160501.pdf -b1e531a8698d91a63af1891ca7e83bb6 plugin-development-guide-Aluminium-20160501.pdf -b5007dcb2d7277bfaef84c1c657bb789 rte-manual-Aluminium-20160501.pdf -16a7467d18e2e24e826114e834fa06a9 user-manual-Aluminium-20160501.pdf -bbbc340c15af5efb8d8bf18effed2bfb value-analysis-Aluminium-20160501.pdf -f6c2067f4e471776dce3c839ce9e25de wp-manual-Aluminium-20160501.pdf -458583247a2a66134de7feadb533c94b frama-c-icons.tar.xz +SHA512 (frama-c-Silicon-20161101.tar.gz) = d8cbc17e5f0b37bacb107828a9b09bc60f99cb50bf885f9f8cee42bb6fcc60a96daf5c95114a4c79477d66b54348ffacbaac29cc4e740535a50c113bf300024d +SHA512 (frama-c-Silicon-20161101_api.tar.gz) = 53c2214e5ad1d7af447edded17ba076eb344c7ade2128e3bd7163438204b41ca3d70633d1d18a70432cea526c5d539f6deca4268dc4e9e1266e80bacdaf27541 +SHA512 (acsl-implementation-Silicon-20161101.pdf) = 1de60d94dc8f80d0e0bd01b0176e4277197442baaca0847718730da3b339204ed8ad09a6ea21a5e39d132e4af67400ca71d8305fa65eea887e6bcfc7edaae592 +SHA512 (aorai-manual-Silicon-20161101.pdf) = 0c1b47e679cd2ab18cd35ec084347677966e4bc20e6e51432f4d35a196ddd184031a0798344dd92688dff8f232213d5d6a94a8d8294439ac67dd7446910c4529 +SHA512 (metrics-manual-Silicon-20161101.pdf) = c67e5a993ba13def50c43e299e7889a0526094ec8af717ef3485b97483ff553f0d9064b694374d592cb4bffa5e9ad074ab35ea8ed5f9136e8fbae75f06803c95 +SHA512 (plugin-development-guide-Silicon-20161101.pdf) = 40e0065522245112dba8a1c7113db19990cc5af518a8d4220b571bad12483f74272ccd1dd332361234c9626225ad54dc50b34c061bca9c10ae5293d6225d1876 +SHA512 (rte-manual-Silicon-20161101.pdf) = c43396549e4b168617c8403c5e28c064653ed2e32133c9e40d64cfdeb8955a1a543f6f96df824f7aef583f4da77df7bce04028d9e738923a6f9b0be17057a268 +SHA512 (user-manual-Silicon-20161101.pdf) = 58c7055247df9f89738aa7c71e948c4346b8f2750e546084f748595124097749d0c6ee7b2debc302b2f935924cef315c70023628466a16c9f06f4feb28414315 +SHA512 (value-analysis-Silicon-20161101.pdf) = f7f013eaa446a3f25e4263ac76ec2a8e6b808d21fd7f2d0f46c4cd209b5aac8bfa5baa770e5de76a11b0ce2ab4059d1c9514f916caa28add5b98837157c5ad89 +SHA512 (wp-manual-Silicon-20161101.pdf) = 73cef86cd3dfc7a60a059501bdbdb6ea783fe148a5f5f164ec132485ab08cc659dd605bd1eb9f4ff74a2f098cd40e642ddbebf53144491a6d590e01e8c3e4136 +SHA512 (frama-c-icons.tar.xz) = 9fb1f6fc32559cfb74491c7f284c4c111d1ce0720fecca8a84713cb68bfa1c77cbeb241c720f58ef0a1140076d2d324f1dcae6cb47650e73c7915e82b2a6914d