[frama-c] Rebuild for ocaml-ocamlgraph 1.8.4; add -ocamlgraph patch to adapt. Add an Appdata file.
Jerry James
jjames at fedoraproject.org
Wed Feb 26 15:36:05 UTC 2014
commit 0da8b3d9d5028e2b6e357fc8ffd9e2a49a3b758c
Author: Jerry James <loganjerry at gmail.com>
Date: Wed Feb 26 08:36:46 2014 -0700
Rebuild for ocaml-ocamlgraph 1.8.4; add -ocamlgraph patch to adapt.
Add an Appdata file.
frama-c-gui.appdata.xml | 29 ++++++
frama-c-ocamlgraph.patch | 238 ++++++++++++++++++++++++++++++++++++++++++++++
frama-c.spec | 28 ++++--
3 files changed, 288 insertions(+), 7 deletions(-)
---
diff --git a/frama-c-gui.appdata.xml b/frama-c-gui.appdata.xml
new file mode 100644
index 0000000..2cba178
--- /dev/null
+++ b/frama-c-gui.appdata.xml
@@ -0,0 +1,29 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<application>
+ <id type="desktop">frama-c-gui.desktop</id>
+ <licence>CC0</licence>
+ <description>
+ <p>
+ Frama-C is a suite of tools dedicated to the analysis of the source code of
+ software written in C.
+ </p>
+ <p>
+ Frama-C gathers several static analysis techniques in a single collaborative
+ framework. The collaborative approach of Frama-C allows static analyzers to
+ build upon the results already computed by other analyzers in the framework.
+ Thanks to this approach, Frama-C provides sophisticated tools, such as a
+ slicer and dependency analysis.
+ </p>
+ </description>
+ <screenshots>
+ <screenshot type="default">http://frama-c.com/media/first.png</screenshot>
+ <screenshot>http://frama-c.com/media/first_S.png</screenshot>
+ <screenshot>http://frama-c.com/media/first_effect.png</screenshot>
+ <screenshot>http://frama-c.com/media/first_defs.png</screenshot>
+ <screenshot>http://frama-c.com/media/first_impact.png</screenshot>
+ </screenshots>
+ <url type="homepage">http://frama-c.com/</url>
+ <!-- FIXME: change this to an upstream email address for spec updates
+ <updatecontact>someone_who_cares at upstream_project.org</updatecontact>
+ -->
+</application>
diff --git a/frama-c-ocamlgraph.patch b/frama-c-ocamlgraph.patch
new file mode 100644
index 0000000..9fac353
--- /dev/null
+++ b/frama-c-ocamlgraph.patch
@@ -0,0 +1,238 @@
+--- ./src/postdominators/print.ml.orig 2013-06-11 08:13:13.000000000 -0600
++++ ./src/postdominators/print.ml 2014-02-25 12:00:00.000000000 -0700
+@@ -63,7 +63,7 @@ module Printer = struct
+
+ let graph_attributes (title, _) = [`Label title]
+
+- let default_vertex_attributes _g = [`Style `Filled]
++ let default_vertex_attributes _g = [`Style [`Filled]]
+ let default_edge_attributes _g = []
+
+ let vertex_attributes (s, has_postdom) =
+--- ./src/logic/property_status.ml.orig 2013-06-11 08:13:39.000000000 -0600
++++ ./src/logic/property_status.ml 2014-02-25 12:00:00.000000000 -0700
+@@ -1427,21 +1427,21 @@ module Consolidation_graph = struct
+ let s = get_status p in
+ let color = status_color p s in
+ let style = match s with
+- | Never_tried -> [`Style `Bold; `Width 0.8 ]
+- | _ -> [`Style `Filled]
++ | Never_tried -> [`Style [`Bold]; `Width 0.8 ]
++ | _ -> [`Style [`Filled]]
+ in
+ style @ [ label v; `Color color; `Shape `Box ]
+ | Emitter _ as v ->
+- [ label v; `Shape `Diamond; `Color 0xb0c4de; `Style `Filled ]
++ [ label v; `Shape `Diamond; `Color 0xb0c4de; `Style [`Filled] ]
+ | Tuning_parameter _ as v ->
+- [ label v; (*`Style `Dotted;*) `Color 0xb0c4de; ]
++ [ label v; (*`Style [`Dotted];*) `Color 0xb0c4de; ]
+ | Correctness_parameter _ (*as v*) -> assert false (*[ label v; `Color 0xb0c4de ]*)
+
+ let edge_attributes e = match E.label e with
+ | None -> []
+ | Some s ->
+ let c = emitted_status_color s in
+- [ `Color c; `Fontcolor c; `Style `Bold ]
++ [ `Color c; `Fontcolor c; `Style [`Bold] ]
+
+ let default_vertex_attributes _ = []
+ let default_edge_attributes _ = []
+--- ./src/semantic_callgraph/register.ml.orig 2013-06-11 08:13:09.000000000 -0600
++++ ./src/semantic_callgraph/register.ml 2014-02-25 12:00:00.000000000 -0700
+@@ -103,8 +103,8 @@ module Service =
+ let name = Kernel_function.get_name
+ let attributes v =
+ [ `Style
+- (if Kernel_function.is_definition v then `Bold
+- else `Dotted) ]
++ (if Kernel_function.is_definition v then [`Bold]
++ else [`Dotted]) ]
+ let entry_point () =
+ try Some (fst (Globals.entry_point ()))
+ with Globals.No_such_entry_point _ -> None
+--- ./src/misc/service_graph.ml.orig 2013-06-11 08:13:49.000000000 -0600
++++ ./src/misc/service_graph.ml 2014-02-25 12:00:00.000000000 -0700
+@@ -289,7 +289,7 @@ Src root:%s in %s (is_root:%b) Dst:%s in
+ color e
+ else
+ match CallG.E.label e with
+- | Inter_services -> [ `Style `Invis ]
++ | Inter_services -> [ `Style [`Invis] ]
+ | Inter_functions | Both -> color e
+
+ let default_edge_attributes _ = []
+@@ -302,7 +302,8 @@ Src root:%s in %s (is_root:%b) Dst:%s in
+ sg_attributes =
+ [ `Label ("S " ^ cs);
+ `Color (Extlib.number_to_color id);
+- `Style `Bold ] }
++ `Style [`Bold] ];
++ sg_parent = None }
+
+ end
+
+--- ./src/syntactic_callgraph/register.ml.orig 2013-06-11 08:13:52.000000000 -0600
++++ ./src/syntactic_callgraph/register.ml 2014-02-25 12:00:00.000000000 -0700
+@@ -37,8 +37,8 @@ module Service =
+ let name v = nodeName v.cnInfo
+ let attributes v =
+ [ match v.cnInfo with
+- | NIVar (_,b) when not !b -> `Style `Dotted
+- | _ -> `Style `Bold ]
++ | NIVar (_,b) when not !b -> `Style [`Dotted]
++ | _ -> `Style [`Bold] ]
+ let equal v1 v2 = id v1 = id v2
+ let compare v1 v2 =
+ let i1 = id v1 in
+--- ./src/pdg_types/pdgTypes.ml.orig 2013-06-11 08:13:49.000000000 -0600
++++ ./src/pdg_types/pdgTypes.ml 2014-02-25 12:00:00.000000000 -0700
+@@ -624,7 +624,7 @@ module Pdg = struct
+
+ let graph_attributes _ = [`Rankdir `TopToBottom ]
+
+- let default_vertex_attributes _ = [`Style `Filled]
++ let default_vertex_attributes _ = [`Style [`Filled]]
+ let vertex_name v = string_of_int (Node.id v)
+
+ let vertex_attributes v =
+@@ -709,15 +709,16 @@ module Pdg = struct
+ if Dpd.is_ctrl d then (`Arrowtail `Odot)::attrib else attrib
+ in
+ let attrib =
+- if Dpd.is_addr d then (`Style `Dotted)::attrib else attrib
++ if Dpd.is_addr d then (`Style [`Dotted])::attrib else attrib
+ in
+ attrib
+
+ let get_subgraph v =
+ let mk_subgraph name attrib =
+- let attrib = (`Style `Filled) :: attrib in
++ let attrib = (`Style [`Filled]) :: attrib in
+ Some { Graph.Graphviz.DotAttributes.sg_name= name;
+- Graph.Graphviz.DotAttributes.sg_attributes = attrib }
++ Graph.Graphviz.DotAttributes.sg_attributes = attrib;
++ Graph.Graphviz.DotAttributes.sg_parent = None }
+ in
+ match Node.elem_key v with
+ | Key.CallStmt call | Key.SigCallKey (call, _) ->
+--- ./src/wp/cil2cfg.ml.orig 2013-06-11 08:13:33.000000000 -0600
++++ ./src/wp/cil2cfg.ml 2014-02-25 12:00:00.000000000 -0700
+@@ -1259,8 +1259,8 @@ module Printer (PE : sig val edge_txt :
+ | Vstart | Vend | Vexit -> [`Color 0x0000FF; `Shape `Doublecircle]
+ | VfctIn | VfctOut -> [`Color 0x0000FF; `Shape `Box]
+ | VblkIn _ | VblkOut _ -> [`Shape `Box]
+- | Vloop _ | Vloop2 _ -> [`Color 0xFF0000; `Style `Filled]
+- | Vtest _ | Vswitch _ -> [`Color 0x00FF00; `Style `Filled; `Shape `Diamond]
++ | Vloop _ | Vloop2 _ -> [`Color 0xFF0000; `Style [`Filled]]
++ | Vtest _ | Vswitch _ -> [`Color 0x00FF00; `Style [`Filled]; `Shape `Diamond]
+ | Vcall _ | Vstmt _ -> []
+ in (`Label (String.escaped label))::attr
+
+@@ -1270,15 +1270,15 @@ module Printer (PE : sig val edge_txt :
+ let attr = [] in
+ let attr = (`Label (String.escaped (PE.edge_txt e)))::attr in
+ let attr =
+- if is_back_edge e then (`Constraint false)::(`Style `Bold)::attr
++ if is_back_edge e then (`Constraint false)::(`Style [`Bold])::attr
+ else attr
+ in
+ let attr = match (edge_type e) with
+ | Ethen | EbackThen -> (`Color 0x00FF00)::attr
+ | Eelse | EbackElse -> (`Color 0xFF0000)::attr
+- | Ecase [] -> (`Color 0x0000FF)::(`Style `Dashed)::attr
++ | Ecase [] -> (`Color 0x0000FF)::(`Style [`Dashed])::attr
+ | Ecase _ -> (`Color 0x0000FF)::attr
+- | Enext -> (`Style `Dotted)::attr
++ | Enext -> (`Style [`Dotted])::attr
+ | Eback -> attr (* see is_back_edge above *)
+ | Enone -> attr
+ in
+@@ -1288,9 +1288,10 @@ module Printer (PE : sig val edge_txt :
+
+ let get_subgraph v =
+ let mk_subgraph name attrib =
+- let attrib = (`Style `Filled) :: attrib in
++ let attrib = (`Style [`Filled]) :: attrib in
+ Some { Graph.Graphviz.DotAttributes.sg_name= name;
+- Graph.Graphviz.DotAttributes.sg_attributes = attrib }
++ Graph.Graphviz.DotAttributes.sg_attributes = attrib;
++ Graph.Graphviz.DotAttributes.sg_parent = None }
+ in
+ match node_type (V.label v) with
+ | Vcall (s,_,_,_) ->
+--- ./src/impact/reason_graph.ml.orig 2013-06-11 08:13:52.000000000 -0600
++++ ./src/impact/reason_graph.ml 2014-02-25 12:00:00.000000000 -0700
+@@ -81,7 +81,7 @@ module Printer = struct
+
+ let graph_attributes _ = [`Label "Impact graph"]
+
+- let default_vertex_attributes _g = [`Style `Filled]
++ let default_vertex_attributes _g = [`Style [`Filled]]
+ let default_edge_attributes _g = []
+
+ let vertex_attributes v =
+@@ -112,6 +112,7 @@ module Printer = struct
+ let attrs = {
+ Graph.Graphviz.DotAttributes.sg_name = name;
+ sg_attributes = [`Label name];
++ sg_parent = None
+ } in
+ Some attrs
+
+--- ./src/kernel/stmts_graph.ml.orig 2013-06-11 08:13:13.000000000 -0600
++++ ./src/kernel/stmts_graph.ml 2014-02-25 12:00:00.000000000 -0700
+@@ -139,12 +139,12 @@ module TP = struct
+
+ let vertex_attributes s =
+ match s.skind with
+- | Loop _ -> [`Color 0xFF0000; `Style `Filled]
+- | If _ -> [`Color 0x00FF00; `Style `Filled; `Shape `Diamond]
+- | Return _ -> [`Color 0x0000FF; `Style `Filled]
++ | Loop _ -> [`Color 0xFF0000; `Style [`Filled]]
++ | If _ -> [`Color 0x00FF00; `Style [`Filled]; `Shape `Diamond]
++ | Return _ -> [`Color 0x0000FF; `Style [`Filled]]
+ | Block _ -> [`Shape `Box; `Fontsize 8]
+- | Goto _ -> [`Shape `Diamond; `Color 0x00FFFF ; `Style `Filled]
+- | Instr (Skip _) -> [`Color 0x00FFFF ; `Style `Filled]
++ | Goto _ -> [`Shape `Diamond; `Color 0x00FFFF ; `Style [`Filled]]
++ | Instr (Skip _) -> [`Color 0x00FFFF ; `Style [`Filled]]
+ | _ -> []
+ let default_vertex_attributes _ = []
+
+--- ./src/slicing/printSlice.ml.orig 2013-06-11 08:13:35.000000000 -0600
++++ ./src/slicing/printSlice.ml 2014-02-25 12:00:00.000000000 -0700
+@@ -227,7 +227,7 @@ module PrintProject = struct
+
+ let graph_attributes (name, _) = [`Label name]
+
+- let default_vertex_attributes _ = [`Style `Filled]
++ let default_vertex_attributes _ = [`Style [`Filled]]
+
+ let vertex_name v = match v with
+ | Src fi -> SlicingMacros.fi_name fi
+@@ -280,18 +280,19 @@ module PrintProject = struct
+
+ let edge_attributes (e, call) =
+ let attrib = match e with
+- | (Src _, Src _) -> [`Style `Invis]
+- | (OptSliceCallers _, _) -> [`Style `Invis]
+- | (_, OptSliceCallers _) -> [`Style `Invis]
++ | (Src _, Src _) -> [`Style [`Invis]]
++ | (OptSliceCallers _, _) -> [`Style [`Invis]]
++ | (_, OptSliceCallers _) -> [`Style [`Invis]]
+ | _ -> []
+ in match call with None -> attrib
+ | Some call -> (`Label (string_of_int call.sid)):: attrib
+
+ let get_subgraph v =
+ let mk_subgraph name attrib =
+- let attrib = (*(`Label name) ::*) (`Style `Filled) :: attrib in
++ let attrib = (*(`Label name) ::*) (`Style [`Filled]) :: attrib in
+ Some { Graph.Graphviz.DotAttributes.sg_name= name;
+- Graph.Graphviz.DotAttributes.sg_attributes = attrib }
++ Graph.Graphviz.DotAttributes.sg_attributes = attrib;
++ Graph.Graphviz.DotAttributes.sg_parent = None }
+ in
+ let f_subgraph fi =
+ let name = SlicingMacros.fi_name fi in
diff --git a/frama-c.spec b/frama-c.spec
index d47d18e..502f99b 100644
--- a/frama-c.spec
+++ b/frama-c.spec
@@ -12,13 +12,14 @@
%global ocamlbest opt
%else
%global ocamlbest byte
+%global debug_package %{nil}
%endif
%global pkgversion Fluorine-20130601
Name: frama-c
Version: 1.9
-Release: 8%{?dist}
+Release: 9%{?dist}
Summary: Framework for source code analysis of C software
Group: Development/Libraries
@@ -28,11 +29,14 @@ URL: http://frama-c.com/
Source0: http://frama-c.com/download/%{name}-%{pkgversion}.tar.gz
Source1: frama-c-1.6.licensing
Source2: %{name}-gui.desktop
-Source3: acsl.el
+Source3: %{name}-gui.appdata.xml
+Source4: acsl.el
# Post-release fixes from upstream
Patch0: %{name}-fixes.patch
# Adapt to OCaml 4.01.0
Patch1: %{name}-ocaml401.patch
+# Adapt to ocamlgraph 1.8.4
+Patch2: %{name}-ocamlgraph.patch
BuildRequires: alt-ergo
BuildRequires: coq
@@ -135,6 +139,7 @@ support.
%setup -q -n %{name}-%pkgversion
%patch0
%patch1
+%patch2
# Fix encodings
iconv -f iso-8859-1 -t utf8 man/frama-c.1 > man/frama-c.1.conv
@@ -166,9 +171,13 @@ make install DESTDIR=%{buildroot} %{framac_make_options}
mv -f %{buildroot}%{_bindir}/frama-c.byte %{buildroot}%{_bindir}/frama-c
mv -f %{buildroot}%{_bindir}/frama-c-gui.byte %{buildroot}%{_bindir}/frama-c-gui
%endif
-desktop-file-install \
---dir=${RPM_BUILD_ROOT}%{_datadir}/applications/ \
-%{SOURCE2}
+
+# Install the desktop file
+desktop-file-install --dir=%{buildroot}%{_datadir}/applications/ %{SOURCE2}
+
+# Install the AppData file
+mkdir -p %{buildroot}%{_datadir}/appdata
+install -pm 644 %{SOURCE3} %{buildroot}%{_datadir}/appdata
# Install and bytecompile the XEmacs file
mkdir -p %{buildroot}%{_xemacs_sitelispdir}
@@ -176,7 +185,7 @@ cp -p share/acsl.el %{buildroot}%{_xemacs_sitelispdir}
cd %{buildroot}%{_xemacs_sitelispdir}
%{_xemacs_bytecompile} acsl.el
mkdir -p %{buildroot}%{_xemacs_sitestartdir}
-cp -p %{SOURCE3} %{buildroot}%{_xemacs_sitestartdir}
+cp -p %{SOURCE4} %{buildroot}%{_xemacs_sitestartdir}
# Install and bytecompile the Emacs file
mkdir -p %{buildroot}%{_emacs_sitelispdir}
@@ -185,7 +194,7 @@ chmod a-x %{buildroot}%{_emacs_sitelispdir}/acsl.el
cd %{buildroot}%{_emacs_sitelispdir}
%{_emacs_bytecompile} acsl.el
mkdir -p %{buildroot}%{_emacs_sitestartdir}
-cp -p %{SOURCE3} %{buildroot}%{_emacs_sitestartdir}
+cp -p %{SOURCE4} %{buildroot}%{_emacs_sitestartdir}
# Remove files we don't actually want
rm -f %{buildroot}%{_libdir}/frama-c/*.{cmo,cmx,o}
@@ -204,6 +213,7 @@ xargs chmod a-x %{buildroot}%{_mandir}/man1/*
%endif
%{_libdir}/frama-c/
%{_datadir}/frama-c/
+%{_datadir}/appdata/%{name}-gui.appdata.xml
%{_datadir}/applications/*.desktop
%{_mandir}/man1/*
@@ -232,6 +242,10 @@ xargs chmod a-x %{buildroot}%{_mandir}/man1/*
%{_xemacs_sitelispdir}/acsl.el
%changelog
+* Wed Feb 26 2014 Jerry James <loganjerry at gmail.com> - 1.9-9
+- Rebuild for ocaml-ocamlgraph 1.8.4; add -ocamlgraph patch to adapt.
+- Add an Appdata file.
+
* Wed Oct 02 2013 Richard W.M. Jones <rjones at redhat.com> - 1.9-8
- Rebuild for ocaml-lablgtk 2.18.
More information about the scm-commits
mailing list