[frama-c] Update to Fluorine version. Merge -devel into the main package (bz 888865).
Jerry James
jjames at fedoraproject.org
Tue May 14 21:00:01 UTC 2013
commit 94bf6fa8cfd8a43cc88972ef170f834306daa25a
Author: Jerry James <jamesjer at betterlinux.com>
Date: Tue May 14 14:59:49 2013 -0600
Update to Fluorine version.
Merge -devel into the main package (bz 888865).
.gitignore | 1 +
frama-c-fixes.patch | 237 ++++++++++++++++++++++++++++++++++++++++++++++++---
frama-c.spec | 58 +++++--------
sources | 2 +-
4 files changed, 247 insertions(+), 51 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index 6f885ad..1c265e3 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
/frama-c-Oxygen-20120901.tar.gz
+/frama-c-Fluorine-20130401.tar.gz
diff --git a/frama-c-fixes.patch b/frama-c-fixes.patch
index aed54f0..17c64de 100644
--- a/frama-c-fixes.patch
+++ b/frama-c-fixes.patch
@@ -1,13 +1,224 @@
-Index: src/pdg_types/pdgTypes.ml
-===================================================================
---- src/pdg_types/pdgTypes.ml (révision 20081)
-+++ src/pdg_types/pdgTypes.ml (révision 20082)
-@@ -701,7 +701,7 @@
- in (`Color color) :: attrib
- in
- let attrib =
-- if Dpd.is_ctrl d then (`Arrowhead `Odot)::attrib else attrib
-+ 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
+--- ./src/wp/LogicSemantics.ml.orig 2013-04-19 01:55:54.000000000 -0600
++++ ./src/wp/LogicSemantics.ml 2013-05-08 14:34:37.762596322 -0600
+@@ -401,7 +401,7 @@ struct
+ let te = Logic_typing.ctype_of_pointed a.term_type in
+ let la = loc_of_term env a in
+ let lb = loc_of_term env b in
+- Vexp(M.loc_offset (Ctypes.object_of te) la lb)
++ Vexp(M.loc_diff (Ctypes.object_of te) la lb)
+ | Shiftlt -> L.apply Cint.l_lsl (C.logic env a) (C.logic env b)
+ | Shiftrt -> L.apply Cint.l_lsr (C.logic env a) (C.logic env b)
+ | BAnd -> L.apply Cint.l_and (C.logic env a) (C.logic env b)
+--- ./src/wp/MemEmpty.ml.orig 2013-04-19 01:55:54.000000000 -0600
++++ ./src/wp/MemEmpty.ml 2013-05-08 14:34:37.761596324 -0600
+@@ -93,7 +93,7 @@ let loc_eq _ _ = no_pointer ()
+ let loc_lt _ _ = no_pointer ()
+ let loc_leq _ _ = no_pointer ()
+ let loc_neq _ _ = no_pointer ()
+-let loc_offset _ _ _ = no_pointer ()
++let loc_diff _ _ _ = no_pointer ()
+
+ let valid _sigma _l = Warning.error ~source "No validity"
+ let scope sigma _s _xs = sigma , []
+--- ./src/wp/ProverWhy3.ml.orig 2013-04-19 01:55:54.000000000 -0600
++++ ./src/wp/ProverWhy3.ml 2013-05-08 14:51:43.973920953 -0600
+@@ -70,8 +70,8 @@ let engine =
+ let module E = Qed.Export_why3.Make(Lang.F) in
+ object(self)
+ inherit E.engine
+- method datatype = ADT.id
+- method field = Field.id
++ method datatype x = self#basename (ADT.id x)
++ method field x = self#basename (Field.id x)
+ method link e f =
+ match Lang.link e f with
+ | Engine.F_call s ->
+--- ./src/wp/Memory.mli.orig 2013-04-19 01:55:54.000000000 -0600
++++ ./src/wp/Memory.mli 2013-05-08 14:34:37.762596322 -0600
+@@ -153,7 +153,7 @@ sig
+ val loc_lt : loc -> loc -> pred
+ val loc_neq : loc -> loc -> pred
+ val loc_leq : loc -> loc -> pred
+- val loc_offset : c_object -> loc -> loc -> term
++ val loc_diff : c_object -> loc -> loc -> term
+
+ val valid : sigma -> acs -> segment -> pred
+ val scope : sigma -> Mcfg.scope -> varinfo list -> sigma * pred list
+--- ./src/wp/MemVar.ml.orig 2013-04-19 01:55:54.000000000 -0600
++++ ./src/wp/MemVar.ml 2013-05-08 14:34:37.760596325 -0600
+@@ -427,12 +427,12 @@ struct
+ | Field f :: ofs -> e_add (e_int64 (Ctypes.field_offset f)) (offset ofs)
+ | Index(obj,k)::ofs -> e_add (e_fact (Ctypes.sizeof_object obj) k) (offset ofs)
+
+- let loc_offset obj a b =
++ let loc_diff obj a b =
+ match a , b with
+- | Mloc l1 , Mloc l2 -> M.loc_offset obj l1 l2
++ | Mloc l1 , Mloc l2 -> M.loc_diff obj l1 l2
+ | Fref x , Fref y when Varinfo.equal x y -> e_zero
+ | (Fval(x,p)|Mval(x,p)) , (Fval(y,q)|Mval(y,q)) when Varinfo.equal x y ->
+- e_div (e_sub (offset p) (offset q)) (e_int64 (sizeof_object obj))
++ e_div (e_sub (offset p) (offset q)) (e_int64 (Ctypes.sizeof_object obj))
+ | Mval _ , _ | _ , Mval _
+ | Fval _ , _ | _ , Fval _
+ | Fref _ , _ | _ , Fref _
+--- ./src/wp/ctypes.ml.orig 2013-04-19 01:55:54.000000000 -0600
++++ ./src/wp/ctypes.ml 2013-05-08 14:34:37.760596325 -0600
+@@ -45,12 +45,18 @@ let signed = function
+ | UInt8 | UInt16 | UInt32 | UInt64 -> false
+ | SInt8 | SInt16 | SInt32 | SInt64 -> true
+
+-let i_sizeof = function
++let i_bits = function
+ | UInt8 | SInt8 -> 8
+ | UInt16 | SInt16 -> 16
+ | UInt32 | SInt32 -> 32
+ | UInt64 | SInt64 -> 64
+
++let i_bytes = function
++ | UInt8 | SInt8 -> 1
++ | UInt16 | SInt16 -> 2
++ | UInt32 | SInt32 -> 4
++ | UInt64 | SInt64 -> 8
++
+ let make_c_int signed = function
+ | 1 -> if signed then SInt8 else UInt8
+ | 2 -> if signed then SInt16 else UInt16
+@@ -103,8 +109,8 @@ let c_ptr () =
+ make_c_int false Cil.theMachine.Cil.theMachine.sizeof_ptr
+
+ let sub_c_int t1 t2 =
+- if (signed t1 = signed t2) then i_sizeof t1 <= i_sizeof t2
+- else (not(signed t1) && (i_sizeof t1 < i_sizeof t2))
++ if (signed t1 = signed t2) then i_bits t1 <= i_bits t2
++ else (not(signed t1) && (i_bits t1 < i_bits t2))
+
+ type c_float =
+ | Float32
+@@ -112,7 +118,11 @@ type c_float =
+
+ let compare_c_float : c_float -> c_float -> _ = Extlib.compare_basic
+
+-let f_sizeof = function
++let f_bytes = function
++ | Float32 -> 4
++ | Float64 -> 8
++
++let f_bits = function
+ | Float32 -> 32
+ | Float64 -> 64
+
+@@ -128,7 +138,7 @@ let c_float fkind =
+ | FDouble -> make_c_float mach.sizeof_double
+ | FLongDouble -> make_c_float mach.sizeof_longdouble
+
+-let sub_c_float f1 f2 = f_sizeof f1 <= f_sizeof f2
++let sub_c_float f1 f2 = f_bits f1 <= f_bits f2
+
+ (* Array objects, with both the head view and the flatten view. *)
+
+@@ -191,9 +201,9 @@ let fmemo f =
+ (* -------------------------------------------------------------------------- *)
+
+ let pp_int fmt i = Format.fprintf fmt "%cint%d"
+- (if signed i then 's' else 'u') (i_sizeof i)
++ (if signed i then 's' else 'u') (i_bits i)
+
+-let pp_float fmt f = Format.fprintf fmt "float%d" (f_sizeof f)
++let pp_float fmt f = Format.fprintf fmt "float%d" (f_bits f)
+
+ let pp_object fmt = function
+ | C_int i -> pp_int fmt i
+@@ -349,9 +359,9 @@ let int64_max a b =
+ if Int64.compare a b < 0 then b else a
+
+ let rec sizeof_object = function
+- | C_int i -> Int64.of_int (i_sizeof i)
+- | C_float f -> Int64.of_int (f_sizeof f)
+- | C_pointer _ty -> Int64.of_int (i_sizeof (c_ptr()))
++ | C_int i -> Int64.of_int (i_bytes i)
++ | C_float f -> Int64.of_int (f_bytes f)
++ | C_pointer _ty -> Int64.of_int (i_bytes (c_ptr()))
+ | C_comp cinfo ->
+ let merge = if cinfo.cstruct then Int64.add else int64_max in
+ List.fold_left
+@@ -398,8 +408,8 @@ let field_offset f =
+ (* with greater rank, whatever *)
+ (* their sign. *)
+
+-let i_convert t1 t2 = if i_sizeof t1 < i_sizeof t2 then t2 else t1
+-let f_convert t1 t2 = if f_sizeof t1 < f_sizeof t2 then t2 else t1
++let i_convert t1 t2 = if i_bits t1 < i_bits t2 then t2 else t1
++let f_convert t1 t2 = if f_bits t1 < f_bits t2 then t2 else t1
+
+ let promote a1 a2 =
+ match a1 , a2 with
+--- ./src/wp/CodeSemantics.ml.orig 2013-04-19 01:55:54.000000000 -0600
++++ ./src/wp/CodeSemantics.ml 2013-05-08 14:34:37.761596324 -0600
+@@ -195,7 +195,7 @@ struct
+ | MinusPP ->
+ let te = Cil.typeOf_pointed (Cil.typeOf e1) in
+ let obj = Ctypes.object_of te in
+- Val(M.loc_offset obj (loc_of_exp env e1) (loc_of_exp env e2))
++ Val(M.loc_diff obj (loc_of_exp env e1) (loc_of_exp env e2))
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Cast --- *)
+--- ./src/wp/share/memory.why.orig 2013-04-19 01:55:46.000000000 -0600
++++ ./src/wp/share/memory.why 2013-05-08 14:34:24.545614985 -0600
+@@ -26,11 +26,29 @@
+
+ theory Memory
+
++ use import bool.Bool
+ use import int.Int
+ use import map.Map
+
+ type addr = { base : int ; offset : int }
+
++ predicate addr_le addr addr
++ predicate addr_lt addr addr
++ function addr_le_bool addr addr : bool
++ function addr_lt_bool addr addr : bool
++
++ axiom addr_le_def: forall p q :addr [addr_le p q].
++ p.base = q.base -> (addr_le p q <-> p.offset <= q.offset)
++
++ axiom addr_lt_def: forall p q :addr [addr_lt p q].
++ p.base = q.base -> (addr_le p q <-> p.offset < q.offset)
++
++ axiom addr_le_bool_def : forall p q : addr [ addr_le_bool p q].
++ addr_le p q <-> addr_le_bool p q = True
++
++ axiom addr_lt_bool_def : forall p q : addr [ addr_lt_bool p q].
++ addr_lt p q <-> addr_lt_bool p q = True
++
+ constant null : addr = { base = 0 ; offset = 0 }
+ function global (b:int) : addr = { base = b ; offset = 0 }
+ function shift (p:addr) (k:int) : addr = { p with offset = p.offset + k }
+--- ./src/wp/ctypes.mli.orig 2013-04-19 01:55:54.000000000 -0600
++++ ./src/wp/ctypes.mli 2013-05-08 14:34:37.762596322 -0600
+@@ -96,10 +96,6 @@ val c_int_bounds: c_int -> Qed.Z.t * Qed
+
+ (** All sizes are in bits *)
+
+-val i_sizeof : c_int -> int
+-
+-val f_sizeof : c_float -> int
+-
+ val sub_c_int: c_int -> c_int -> bool
+
+ val sub_c_float : c_float -> c_float -> bool
+--- ./src/wp/MemTyped.ml.orig 2013-04-19 01:55:54.000000000 -0600
++++ ./src/wp/MemTyped.ml 2013-05-08 14:34:37.759596326 -0600
+@@ -875,8 +875,8 @@ let loc_eq = p_equal
+ let loc_neq = p_neq
+ let loc_lt = loc_compare a_lt p_lt
+ let loc_leq = loc_compare a_leq p_leq
+-let loc_offset obj p q =
+- let delta = e_sub (a_offset q) (a_offset p) in
++let loc_diff obj p q =
++ let delta = e_sub (a_offset p) (a_offset q) in
+ e_fact (Ctypes.sizeof_object obj) delta
+
+ (* -------------------------------------------------------------------------- *)
diff --git a/frama-c.spec b/frama-c.spec
index 0b5696c..b7d137c 100644
--- a/frama-c.spec
+++ b/frama-c.spec
@@ -16,11 +16,11 @@
%global ocamlbest byte
%endif
-%global pkgversion Oxygen-20120901
+%global pkgversion Fluorine-20130401
Name: frama-c
-Version: 1.8
-Release: 6%{?dist}
+Version: 1.9
+Release: 1%{?dist}
Summary: Framework for source code analysis of C software
Group: Development/Libraries
@@ -54,6 +54,10 @@ Requires: cpp
Requires: graphviz
Requires: ltl2ba
+# This can be removed once F-19 goes EOL
+Obsoletes: %{name}-devel < 1.9-1
+Provides: %{name}-devel = %{version}-%{release}
+
# ocaml only available on these:
ExclusiveArch: %{ocaml_arches}
@@ -70,16 +74,6 @@ 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.
-%package devel
-Summary: Development files for %{name}
-Group: Development/Libraries
-Requires: %{name}%{?_isa} = %{version}-%{release}
-
-%description devel
-The %{name}-devel package contains libraries and signature files for
-developing applications that use %{name}. In particular, this package
-is necessary to compile plug ins for Frama-C.
-
%package doc
Summary: Large documentation files for %{name}
Group: Documentation
@@ -146,10 +140,6 @@ 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
-# Allow use of alt-ergo 0.95
-sed -i 's/0\.92\.2/0.95/' configure
-sed -i 's/0\.92\.2/0.95/' src/wp/configure
-
%build
# This option prints the actual make commands so we can see what's
# happening (eg: for debugging the spec file)
@@ -161,7 +151,9 @@ chmod a+x why why-dp
PATH=${PATH}:${PWD}
%configure
-make %{framac_make_options}
+# Harden the build due to network use
+make %{framac_make_options} \
+OLINKFLAGS="-I +zarith -I +ocamlgraph -I +lablgtk2 -ccopt -Wl,-z,relro,-z,now"
%install
make install DESTDIR=%{buildroot} %{framac_make_options}
@@ -204,40 +196,28 @@ xargs chmod a-x %{buildroot}%{_libdir}/frama-c/*.cmx \
%files
%doc licenses/* doc/manuals/user-manual.pdf VERSION
%{_bindir}/*
+%if %opt
%exclude %{_bindir}/frama-c.byte
%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
-%dir %{_datadir}/frama-c/
-%{_datadir}/frama-c/*.gif
-%{_datadir}/frama-c/*.ico
-%{_datadir}/frama-c/*.png
+%{_libdir}/frama-c/
+%{_datadir}/frama-c/
%{_datadir}/applications/*.desktop
%{_mandir}/man1/*
-%files devel
-%doc doc/manuals/plugin-development-guide.pdf
-%{_datadir}/frama-c/*
-%{_libdir}/frama-c/*.cmo
-%{_libdir}/frama-c/*.cmx
-%{_libdir}/frama-c/*.o
-%exclude %{_datadir}/frama-c/*.gif
-%exclude %{_datadir}/frama-c/*.ico
-%exclude %{_datadir}/frama-c/*.png
-%exclude %{_datadir}/frama-c/manuals
-
%files doc
%doc doc/code/*.txt
%doc doc/manuals/acsl*
%doc doc/manuals/aorai-manual.pdf
%doc doc/manuals/metrics-manual.pdf
+%doc doc/manuals/plugin-development-guide.pdf
%doc doc/manuals/rte-manual.pdf
%doc doc/manuals/value-analysis.pdf
%doc doc/manuals/wp-manual.pdf
-%doc doc/manuals/wp-tutorial.pdf
%files emacs
%{_emacs_sitelispdir}/acsl.elc
@@ -254,6 +234,10 @@ xargs chmod a-x %{buildroot}%{_libdir}/frama-c/*.cmx \
%{_xemacs_sitelispdir}/acsl.el
%changelog
+* Tue May 14 2013 Jerry James <loganjerry at gmail.com> - 1.9-1
+- Update to Fluorine version
+- Merge -devel into the main package (bz 888865)
+
* Wed Feb 13 2013 Fedora Release Engineering <rel-eng at lists.fedoraproject.org> - 1.8-6
- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild
@@ -318,7 +302,7 @@ xargs chmod a-x %{buildroot}%{_libdir}/frama-c/*.cmx \
* Sat Jan 22 2011 Dan Horák <dan[at]danny.cz> - 1.5-2
- updated the supported arch list
-* Sat Jul 07 2010 Mark Rader <msrader at gmail.com> 1.5-1
+* Sat Jul 17 2010 Mark Rader <msrader at gmail.com> 1.5-1
- Upgraded Frama C to Boron version and added ltl2ba dependencies.
* Mon Jul 05 2010 Mark Rader <msrader at gmail.com> 1.4-4
@@ -328,7 +312,7 @@ xargs chmod a-x %{buildroot}%{_libdir}/frama-c/*.cmx \
- Added documentation to explain the various licensing entries.
- Added .desktop file
-* Wed May 24 2010 Mark Rader <msrader at gmail.com> 1.4-2
+* Wed May 26 2010 Mark Rader <msrader at gmail.com> 1.4-2
- Add SELinux context settings.
* Wed Feb 10 2010 Alan Dunn <amdunn at gmail.com> 1.4-1
diff --git a/sources b/sources
index 592ca6b..d355c9d 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-f8f22501761fc67fcac5daceac82bb31 frama-c-Oxygen-20120901.tar.gz
+9543def7e765403e51f3cdb506698159 frama-c-Fluorine-20130401.tar.gz
More information about the scm-commits
mailing list