From bd807bf96e002c1329aa4dbcad5673d5f5b5e5b5 Mon Sep 17 00:00:00 2001 From: Richard W.M. Jones Date: Nov 08 2016 14:20:15 +0000 Subject: - Add small fixes for OCaml 4.04.0. --- diff --git a/frama-c-ocaml-4-04.patch b/frama-c-ocaml-4-04.patch new file mode 100644 index 0000000..64459ef --- /dev/null +++ b/frama-c-ocaml-4-04.patch @@ -0,0 +1,73 @@ +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 2b4bb00..6410fbe 100644 --- a/frama-c.spec +++ b/frama-c.spec @@ -34,6 +34,9 @@ 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 @@ -118,6 +121,8 @@ 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} \ @@ -256,6 +261,7 @@ gtk-update-icon-cache %{_datadir}/icons/hicolor &>/dev/null || : %changelog * Mon Nov 07 2016 Richard W.M. Jones - 1.13-5 - Rebuild for OCaml 4.04.0. +- Add small fixes for OCaml 4.04.0. * Fri Oct 28 2016 Jerry James - 1.13-4 - Rebuild for coq 8.5pl3