From 6e23d32bb524b44fe774429b2ae0ae803864bf42 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Mar 18 2014 15:20:33 +0000 Subject: Update to Neon version. All patches have been upstreamed; drop them. The manuals are no longer included in the source distribution; add as Sources. BR ocaml-findlib instead of ocaml-findlib-devel. BR why3 to get coq + why3 support in the wp plugin. --- diff --git a/.gitignore b/.gitignore index d500432..c330998 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,10 @@ -/frama-c-Fluorine-20130601.tar.gz +/frama-c-Neon-20140301_api.tar.gz +/frama-c-Neon-20140301.tar.gz +/acsl-implementation-Neon-20140301.pdf +/aorai-manual-Neon-20140301.pdf +/metrics-manual-Neon-20140301.pdf +/plugin-development-guide-Neon-20140301.pdf +/rte-manual-Neon-20140301.pdf +/user-manual-Neon-20140301.pdf +/value-analysis-Neon-20140301.pdf +/wp-manual-Neon-20140301.pdf diff --git a/frama-c-fixes.patch b/frama-c-fixes.patch deleted file mode 100644 index 4bdb23c..0000000 --- a/frama-c-fixes.patch +++ /dev/null @@ -1,87 +0,0 @@ -See http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-May/003637.html -and http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-May/003645.html. - -Index: src/wp/LogicCompiler.ml -=================================================================== ---- src/wp/LogicCompiler.ml (revision 22639) -+++ src/wp/LogicCompiler.ml (working copy) -@@ -606,16 +606,21 @@ - List.fold_left (heap_case labels_used) support s) - Heap.Map.empty cases in - (* Make signature with collected chunks *) -- let (parm,sigm) = Heap.Map.fold -- (fun chunk labels acc -> -- let basename = Chunk.basename_of_chunk chunk in -- let tau = Chunk.tau_of_chunk chunk in -- LabelSet.fold -- (fun label (parm,sigm) -> -- let x = Lang.freshvar ~basename tau in -- x :: parm , Sig_chunk(chunk,label) :: sigm -- ) labels acc) -- support (parp,sigp) in -+ let (parm,sigm) = -+ let frame = logic_frame l.l_var_info.lv_name l.l_tparams in -+ in_frame frame -+ (fun () -> -+ Heap.Map.fold -+ (fun chunk labels acc -> -+ let basename = Chunk.basename_of_chunk chunk in -+ let tau = Chunk.tau_of_chunk chunk in -+ LabelSet.fold -+ (fun label (parm,sigm) -> -+ let x = Lang.freshvar ~basename tau in -+ x :: parm , Sig_chunk(chunk,label) :: sigm -+ ) labels acc) -+ support (parp,sigp) -+ ) () in - (* Set global Signature *) - let lfun = ACSL l in - let ldef = { -@@ -624,8 +629,9 @@ - d_params = parm ; - d_cluster = cluster ; - d_definition = Logic Qed.Logic.Prop ; -- } in -+ } in - Definitions.update_symbol ldef ; -+ Signature.update l (SIG sigm) ; - (* Re-compile final cases *) - let cases = List.map - (fun (case,labels,types,lemma) -> -See http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-August/003702.html. - -Index: external/unmarshal.ml -=================================================================== ---- external/unmarshal.ml (revision 23277) -+++ external/unmarshal.ml (working copy) -@@ -209,6 +209,8 @@ - - (* Auxiliary functions for handling closures. *) - -+(* Not used by Frama-C, causing problems with ARM, see: -+http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-August/003702.html - let (code_area_start, cksum) = - let s = Marshal.to_string id [Marshal.Closures] in - let cksum = String.sub s 0x1E 16 in -@@ -222,6 +224,7 @@ - let start = Obj.add_offset (Obj.field (Obj.repr id) 0) (Int32.neg ofs) in - (start, cksum) - ;; -+*) - - let check_const ch s msg = - for i = 0 to String.length s - 1 do -@@ -412,10 +415,12 @@ - read_double_array stk t len readfloat_big - - | 0x10 (* CODE_CODEPOINTER *) -> -+ assert false -+(* NOT USED BY Frama-C - let ofs = getword ch in - check_const ch cksum "input_value: code mismatch"; - let offset_pointer = Obj.add_offset code_area_start ofs in -- return stk (do_transform t offset_pointer) -+ return stk (do_transform t offset_pointer) *) - | 0x11 (* CODE_INFIXPOINTER *) -> - let ofs = getword ch in - let clos = intern_rec [] t in diff --git a/frama-c-ocaml401.patch b/frama-c-ocaml401.patch deleted file mode 100644 index 77c5310..0000000 --- a/frama-c-ocaml401.patch +++ /dev/null @@ -1,132 +0,0 @@ ---- ./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-ocamlgraph.patch b/frama-c-ocamlgraph.patch deleted file mode 100644 index 9fac353..0000000 --- a/frama-c-ocamlgraph.patch +++ /dev/null @@ -1,238 +0,0 @@ ---- ./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 502f99b..3aaac3b 100644 --- a/frama-c.spec +++ b/frama-c.spec @@ -8,18 +8,15 @@ # forked their own version of cil. %global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0) -%if %opt -%global ocamlbest opt -%else -%global ocamlbest byte +%if ! %opt %global debug_package %{nil} %endif -%global pkgversion Fluorine-20130601 +%global pkgversion Neon-20140301 Name: frama-c -Version: 1.9 -Release: 9%{?dist} +Version: 1.10 +Release: 1%{?dist} Summary: Framework for source code analysis of C software Group: Development/Libraries @@ -27,16 +24,19 @@ Group: Development/Libraries License: LGPLv2 and GPLv2 and GPLv2+ and BSD and (QPL with exceptions) 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: %{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 +Source1: http://frama-c.com/download/%{name}-%{pkgversion}_api.tar.gz +Source2: frama-c-1.6.licensing +Source3: %{name}-gui.desktop +Source4: %{name}-gui.appdata.xml +Source5: acsl.el +Source6: http://frama-c.com/download/user-manual-%{pkgversion}.pdf +Source7: http://frama-c.com/download/plugin-development-guide-%{pkgversion}.pdf +Source8: http://frama-c.com/download/acsl-implementation-%{pkgversion}.pdf +Source9: http://frama-c.com/download/aorai-manual-%{pkgversion}.pdf +Source10: http://frama-c.com/download/metrics-manual-%{pkgversion}.pdf +Source11: http://frama-c.com/download/rte-manual-%{pkgversion}.pdf +Source12: http://frama-c.com/download/value-analysis-%{pkgversion}.pdf +Source13: http://frama-c.com/download/wp-manual-%{pkgversion}.pdf BuildRequires: alt-ergo BuildRequires: coq @@ -48,11 +48,12 @@ BuildRequires: gtksourceview2-devel BuildRequires: libgnomecanvas-devel BuildRequires: ltl2ba BuildRequires: ocaml -BuildRequires: ocaml-findlib-devel +BuildRequires: ocaml-findlib BuildRequires: ocaml-lablgtk-devel BuildRequires: ocaml-ocamldoc BuildRequires: ocaml-ocamlgraph-devel BuildRequires: ocaml-zarith-devel +BuildRequires: why3 Requires: cpp Requires: graphviz @@ -66,7 +67,7 @@ Provides: %{name}-devel = %{version}-%{release} ExclusiveArch: %{ocaml_arches} # Filter out bogus requires -%global __requires_exclude ocaml\\\((Formula|GtkSourceView2_types|Ltlast|Mcfg|Memory|Mfloat|Mint|Mlogic|Mvalues|Mwp|Promelaast|Sig)\\\) +%global __requires_exclude ocaml\\\((CfgTypes|GtkSourceView2_types|Ltlast|Mcfg|Memory|Promelaast)\\\) %description Frama-C is a suite of tools dedicated to the analysis of the source @@ -136,48 +137,63 @@ files marked up with ACSL. This package is not needed to use the XEmacs support. %prep -%setup -q -n %{name}-%pkgversion -%patch0 -%patch1 -%patch2 +%setup -q -n %{name}-%{pkgversion} +%setup -q -T -D -a 1 -n %{name}-%{pkgversion} + +# Copy in the manuals +mkdir doc/manuals +cp -p %{SOURCE6} %{SOURCE7} %{SOURCE8} %{SOURCE9} %{SOURCE10} %{SOURCE11} \ + %{SOURCE12} %{SOURCE13} doc/manuals -# 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 +# Do not use the bundled version of ocamlgraph +rm -f ocamlgraph.tar.gz # Enable debuginfo sed -i 's/ -pack/ -g&/;s/^OPT.*=/& -g/' src/wp/qed/src/Makefile +# Preserve timestamps when installing +sed -ri 's/^CP[[:blank:]]+=.*/& -p/' share/Makefile.common + +# Remove spurious executable bits +find -O3 . -perm /0111 \( -name \*.ml -o -name \*.mli \) | xargs chmod 0644 + +# Adapt to why3 0.83 +sed -i 's/0\.82/0.83/g' configure src/wp/configure + %build # This option prints the actual make commands so we can see what's # happening (eg: for debugging the spec file) -%global framac_make_options VERBOSEMAKE=yes OCAMLBEST=%{ocamlbest} - -# Fake the existence of why so the plugin is built -touch why why-dp -chmod a+x why why-dp -PATH=${PATH}:${PWD} - -%configure +%configure --enable-verbosemake # Harden the build due to network use -make %{framac_make_options} \ +make \ OLINKFLAGS="-I +zarith -I +ocamlgraph -I +lablgtk2 -ccopt -Wl,-z,relro,-z,now" +# Remove spurious executable bits on generated files +chmod 0644 src/lib/dynlink_common_interface.ml src/lib/integer.ml + %install -make install DESTDIR=%{buildroot} %{framac_make_options} +# Prevent rebuilds containing the buildroot when installing +sed -i.orig 's/^headers::/headers:/' Makefile +touch -r Makefile.orig Makefile +sed -i.orig '/^headers::/,/^$/d' src/aorai/Makefile +touch -r src/aorai/Makefile.orig src/aorai/Makefile -%if ! %opt +make install DESTDIR=%{buildroot} + +%if %opt +mv -f %{buildroot}%{_bindir}/ptests.opt %{buildroot}%{_bindir}/ptests +%else mv -f %{buildroot}%{_bindir}/frama-c.byte %{buildroot}%{_bindir}/frama-c mv -f %{buildroot}%{_bindir}/frama-c-gui.byte %{buildroot}%{_bindir}/frama-c-gui +mv -f %{buildroot}%{_bindir}/ptests.byte %{buildroot}%{_bindir}/ptests %endif # Install the desktop file -desktop-file-install --dir=%{buildroot}%{_datadir}/applications/ %{SOURCE2} +desktop-file-install --dir=%{buildroot}%{_datadir}/applications/ %{SOURCE3} # Install the AppData file mkdir -p %{buildroot}%{_datadir}/appdata -install -pm 644 %{SOURCE3} %{buildroot}%{_datadir}/appdata +install -pm 644 %{SOURCE4} %{buildroot}%{_datadir}/appdata # Install and bytecompile the XEmacs file mkdir -p %{buildroot}%{_xemacs_sitelispdir} @@ -185,7 +201,7 @@ cp -p share/acsl.el %{buildroot}%{_xemacs_sitelispdir} cd %{buildroot}%{_xemacs_sitelispdir} %{_xemacs_bytecompile} acsl.el mkdir -p %{buildroot}%{_xemacs_sitestartdir} -cp -p %{SOURCE4} %{buildroot}%{_xemacs_sitestartdir} +cp -p %{SOURCE5} %{buildroot}%{_xemacs_sitestartdir} # Install and bytecompile the Emacs file mkdir -p %{buildroot}%{_emacs_sitelispdir} @@ -194,7 +210,7 @@ chmod a-x %{buildroot}%{_emacs_sitelispdir}/acsl.el cd %{buildroot}%{_emacs_sitelispdir} %{_emacs_bytecompile} acsl.el mkdir -p %{buildroot}%{_emacs_sitestartdir} -cp -p %{SOURCE4} %{buildroot}%{_emacs_sitestartdir} +cp -p %{SOURCE5} %{buildroot}%{_emacs_sitestartdir} # Remove files we don't actually want rm -f %{buildroot}%{_libdir}/frama-c/*.{cmo,cmx,o} @@ -204,7 +220,7 @@ find %{buildroot}%{_datadir}/frama-c -type f -perm /0111 | \ xargs chmod a-x %{buildroot}%{_mandir}/man1/* %files -%doc licenses/* doc/manuals/user-manual.pdf VERSION +%doc licenses/* VERSION %{_bindir}/* %if %opt %exclude %{_bindir}/frama-c.byte @@ -218,14 +234,16 @@ xargs chmod a-x %{buildroot}%{_mandir}/man1/* %{_mandir}/man1/* %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/code/*.{css,htm,txt} +%doc doc/manuals/acsl-implementation-%{pkgversion}.pdf +%doc doc/manuals/aorai-manual-%{pkgversion}.pdf +%doc doc/manuals/metrics-manual-%{pkgversion}.pdf +%doc doc/manuals/plugin-development-guide-%{pkgversion}.pdf +%doc doc/manuals/rte-manual-%{pkgversion}.pdf +%doc doc/manuals/user-manual-%{pkgversion}.pdf +%doc doc/manuals/value-analysis-%{pkgversion}.pdf +%doc doc/manuals/wp-manual-%{pkgversion}.pdf +%doc frama-c-api %files emacs %{_emacs_sitelispdir}/acsl.elc @@ -242,6 +260,13 @@ xargs chmod a-x %{buildroot}%{_mandir}/man1/* %{_xemacs_sitelispdir}/acsl.el %changelog +* Mon Mar 17 2014 Jerry James - 1.10-1 +- Update to Neon version +- All patches have been upstreamed; drop them +- The manuals are no longer included in the source distribution; add as Sources +- BR ocaml-findlib instead of ocaml-findlib-devel +- BR why3 to get coq + why3 support in the wp plugin + * Wed Feb 26 2014 Jerry James - 1.9-9 - Rebuild for ocaml-ocamlgraph 1.8.4; add -ocamlgraph patch to adapt. - Add an Appdata file. diff --git a/sources b/sources index 7e77489..4cf0106 100644 --- a/sources +++ b/sources @@ -1 +1,10 @@ -69eed6b3f649725bf03d8500aaeb20a5 frama-c-Fluorine-20130601.tar.gz +ac755dfefe551bf7d964aa69b6686299 frama-c-Neon-20140301_api.tar.gz +c050eaf6f3acff2edf8edb44bf64976d frama-c-Neon-20140301.tar.gz +3ac995432474fbcc7787aaee17573e22 acsl-implementation-Neon-20140301.pdf +2c56d555d94fda814f85c9df1ba629e4 aorai-manual-Neon-20140301.pdf +c7495b89ed2b99a8c596fb0eeeb8f781 metrics-manual-Neon-20140301.pdf +53b8c1a37ad0460f2a0b033beec99c88 plugin-development-guide-Neon-20140301.pdf +a730e8487e3073393125e65c1165c506 rte-manual-Neon-20140301.pdf +6a56303db0c9c8dedb1520dafe971efa user-manual-Neon-20140301.pdf +5664248096c5cf58fddc6afb9616469d value-analysis-Neon-20140301.pdf +7105adc9b5c13108296d741a919fa2b2 wp-manual-Neon-20140301.pdf