[frama-c] Rebuild for OCaml 4.01.0. Enable debuginfo.
Jerry James
jjames at fedoraproject.org
Tue Sep 17 17:52:27 UTC 2013
commit 3f558f3647b47875b02370998639ce9acc312b47
Author: Jerry James <jamesjer at betterlinux.com>
Date: Tue Sep 17 11:52:07 2013 -0600
Rebuild for OCaml 4.01.0.
Enable debuginfo.
frama-c-ocaml401.patch | 132 ++++++++++++++++++++++++++++++++++++++++++++++++
frama-c.spec | 30 ++++++-----
2 files changed, 148 insertions(+), 14 deletions(-)
---
diff --git a/frama-c-ocaml401.patch b/frama-c-ocaml401.patch
new file mode 100644
index 0000000..77c5310
--- /dev/null
+++ b/frama-c-ocaml401.patch
@@ -0,0 +1,132 @@
+--- ./share/Makefile.common.orig 2013-06-11 08:13:56.000000000 -0600
++++ ./share/Makefile.common 2013-09-16 21:45:00.000000000 -0600
+@@ -59,8 +59,8 @@ ifeq ($(HAS_OCAML311),yes)
+ ifeq ($(findstring 3.13,$(OCAMLVERSION)),) # obsolete version number
+ ifeq ($(findstring 4.00,$(OCAMLVERSION)),)
+ ifeq ($(findstring 4.01,$(OCAMLVERSION)),)
+- HAS_OCAML312 = no # Ocaml 3.11
+- HAS_OCAML400 = no
++ HAS_OCAML312 = yes # Ocaml 3.11
++ HAS_OCAML400 = yes
+ else
+ HAS_OCAML312 = yes
+ HAS_OCAML400 = yes
+--- ./src/kernel/file.ml.orig 2013-06-11 08:13:13.000000000 -0600
++++ ./src/kernel/file.ml 2013-09-16 21:45:00.000000000 -0600
+@@ -321,18 +321,6 @@ object(self)
+ C variable %a"
+ Printer.pp_logic_var lv Printer.pp_varinfo v
+
+- method vlogic_info_decl li =
+- List.iter
+- (fun lv ->
+- if lv.lv_kind <> LVFormal then
+- check_abort
+- "Formal parameter %a of logic function/predicate is \
+- flagged with wrong origin"
+- Printer.pp_logic_var lv)
+- li.l_profile;
+- DoChildren
+-
+-
+ method vlogic_var_use v =
+ if v.lv_name <> "\\exit_status" then begin
+ if Logic_env.is_builtin_logic_function v.lv_name then begin
+@@ -770,6 +758,14 @@ object(self)
+ | _ -> DoChildren
+
+ method vlogic_info_decl li =
++ List.iter
++ (fun lv ->
++ if lv.lv_kind <> LVFormal then
++ check_abort
++ "Formal parameter %a of logic function/predicate is \
++ flagged with wrong origin"
++ Printer.pp_logic_var lv)
++ li.l_profile;
+ Logic_var.Hashtbl.add known_logic_info li.l_var_info li;
+ DoChildren
+
+--- ./src/lib/hptset.ml.orig 2013-06-11 08:13:42.000000000 -0600
++++ ./src/lib/hptset.ml 2013-09-16 21:45:00.000000000 -0600
+@@ -46,6 +46,7 @@ module type S = sig
+ val contains_single_elt: t -> elt option
+ val choose: t -> elt
+ val split: elt -> t -> t * bool * t
++ val find: elt -> t -> elt
+ val intersects: t -> t -> bool
+ val clear_caches: unit -> unit
+ end
+@@ -97,6 +98,8 @@ module Make(X: Id_Datatype)
+
+ let mem x s = try find x s; true with Not_found -> false
+
++ let find x s = if mem x s then x else raise Not_found
++
+ let diff s1 s2 =
+ fold (fun x acc -> if mem x s2 then acc else add x acc) s1 empty
+
+--- ./src/lib/hptset.mli.orig 2013-06-11 08:13:42.000000000 -0600
++++ ./src/lib/hptset.mli 2013-09-16 21:45:00.000000000 -0600
+@@ -137,6 +137,12 @@ module type S = sig
+ [present] is [false] if [s] contains no element equal to [x],
+ or [true] if [s] contains an element equal to [x]. *)
+
++ val find : elt -> t -> elt
++ (** [find x s] returns the element of [s] equal to [x] (according
++ to [Ord.compare]), or raise [Not_found] if no such element
++ exists.
++ @since 4.01.0 *)
++
+ val intersects: t -> t -> bool
+ (** [intersects s1 s2] returns [true] if and only if [s1] and [s2]
+ have an element in common *)
+--- ./src/lib/setWithNearest.ml.orig 2013-06-11 08:13:42.000000000 -0600
++++ ./src/lib/setWithNearest.ml 2013-09-16 21:45:00.000000000 -0600
+@@ -286,6 +286,13 @@ module Make(Ord: Datatype.S) = struct
+
+ let choose = min_elt
+
++ let rec find x = function
++ Empty -> raise Not_found
++ | Node(l, v, r, _) ->
++ let c = Ord.compare x v in
++ if c = 0 then v
++ else find x (if c < 0 then l else r)
++
+ (************************* Extra functions **************************)
+
+ (* The nearest value of [s] le [v]. Raise Not_found if none *)
+--- ./src/memory_state/cvalue.mli.orig 2013-06-11 08:13:51.000000000 -0600
++++ ./src/memory_state/cvalue.mli 2013-09-16 21:45:00.000000000 -0600
+@@ -35,8 +35,8 @@ module V : sig
+ include module type of Location_Bytes
+ (* Too many aliases, and OCaml module system is not able to keep track
+ of all of them. Use some shortcuts *)
+- with type z = Location_Bytes.z
+- and type M.t = Location_Bytes.M.t
++ with type M.t = Location_Bytes.M.t
++ and type z = Location_Bytes.z
+
+ include Lattice_With_Isotropy.S
+ with type t := t
+--- ./src/wp/qed/src/idxset.ml.orig 2013-06-11 08:13:23.000000000 -0600
++++ ./src/wp/qed/src/idxset.ml 2013-09-16 21:45:00.000000000 -0600
+@@ -59,6 +59,8 @@ struct
+
+ let mem e s = mem_k (E.id e) s
+
++ let find x s = if mem x s then x else raise Not_found
++
+ let lowest_bit x = x land (-x)
+
+ let branching_bit p0 p1 = lowest_bit (p0 lxor p1)
+@@ -360,6 +362,8 @@ struct
+
+ let mem e s = mem_k (index e) s
+
++ let find x s = if mem x s then x else raise Not_found
++
+ let mask k m = (k lor (m-1)) land (lnot m)
+
+ (* we first write a naive implementation of [highest_bit]
diff --git a/frama-c.spec b/frama-c.spec
index f851a54..fdd4723 100644
--- a/frama-c.spec
+++ b/frama-c.spec
@@ -7,8 +7,6 @@
# are not availible with the ocaml-cil because the upstream has
# forked their own version of cil.
-%global debug_package %{nil}
-%global __strip /usr/bin/true
%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
%if %opt
%global ocamlbest opt
@@ -20,7 +18,7 @@
Name: frama-c
Version: 1.9
-Release: 6%{?dist}
+Release: 7%{?dist}
Summary: Framework for source code analysis of C software
Group: Development/Libraries
@@ -33,6 +31,8 @@ Source2: %{name}-gui.desktop
Source3: acsl.el
# Post-release fixes from upstream
Patch0: %{name}-fixes.patch
+# Adapt to OCaml 4.01.0
+Patch1: %{name}-ocaml401.patch
BuildRequires: alt-ergo
BuildRequires: coq
@@ -134,12 +134,16 @@ support.
%prep
%setup -q -n %{name}-%pkgversion
%patch0
+%patch1
# Fix encodings
iconv -f iso-8859-1 -t utf8 man/frama-c.1 > man/frama-c.1.conv
touch -r man/frama-c.1 man/frama-c.1.conv
mv -f man/frama-c.1.conv man/frama-c.1
+# Enable debuginfo
+sed -i 's/ -pack/ -g&/;s/^OPT.*=/& -g/' src/wp/qed/src/Makefile
+
%build
# This option prints the actual make commands so we can see what's
# happening (eg: for debugging the spec file)
@@ -158,12 +162,7 @@ OLINKFLAGS="-I +zarith -I +ocamlgraph -I +lablgtk2 -ccopt -Wl,-z,relro,-z,now"
%install
make install DESTDIR=%{buildroot} %{framac_make_options}
-%if %opt
-strip %{buildroot}%{_bindir}/frama-c
-strip %{buildroot}%{_bindir}/frama-c-gui
-strip %{buildroot}%{_libdir}/frama-c/plugins/*.cmxs
-strip %{buildroot}%{_libdir}/frama-c/plugins/gui/*.cmxs
-%else
+%if ! %opt
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
@@ -188,10 +187,12 @@ cd %{buildroot}%{_emacs_sitelispdir}
mkdir -p %{buildroot}%{_emacs_sitestartdir}
cp -p %{SOURCE3} %{buildroot}%{_emacs_sitestartdir}
+# Remove files we don't actually want
+rm -f %{buildroot}%{_libdir}/frama-c/*.{cmo,cmx,o}
+
# The install step adds lots of spurious executable bits
find %{buildroot}%{_datadir}/frama-c -type f -perm /0111 | \
-xargs chmod a-x %{buildroot}%{_libdir}/frama-c/*.cmx \
- %{buildroot}%{_mandir}/man1/*
+xargs chmod a-x %{buildroot}%{_mandir}/man1/*
%files
%doc licenses/* doc/manuals/user-manual.pdf VERSION
@@ -201,9 +202,6 @@ xargs chmod a-x %{buildroot}%{_libdir}/frama-c/*.cmx \
%exclude %{_bindir}/frama-c-gui.byte
%exclude %{_bindir}/ptests.byte
%endif
-%exclude %{_libdir}/frama-c/*.cmo
-%exclude %{_libdir}/frama-c/*.cmx
-%exclude %{_libdir}/frama-c/*.o
%{_libdir}/frama-c/
%{_datadir}/frama-c/
%{_datadir}/applications/*.desktop
@@ -234,6 +232,10 @@ xargs chmod a-x %{buildroot}%{_libdir}/frama-c/*.cmx \
%{_xemacs_sitelispdir}/acsl.el
%changelog
+* Mon Sep 16 2013 Jerry James <loganjerry at gmail.com> - 1.9-7
+- Rebuild for OCaml 4.01.0
+- Enable debuginfo
+
* Fri Aug 9 2013 Jerry James <loganjerry at gmail.com> - 1.9-6
- Update -fixes patch to fix startup failures on ARM
More information about the scm-commits
mailing list