devel/frama-c: Update version Oxygen => Neon to unbreak and stage

Oxygen is from Sept 2012, and Neon is from Mar 2014.  Stage support was
added along with some minor cleanup.  A major patch from Debian was
required to support OcamlGraph 1.8.5.

It has been broken since Ocaml was updated to 4.01.
Work covered by Staging blanket.

5 files changed, 547 insertions, 303 deletions

diff --git a/devel/frama-c/Makefile b/devel/frama-c/Makefile
index 24aac81c88ec..bfd6caa3a754 100644
--- a/devel/frama-c/Makefile
+++ b/devel/frama-c/Makefile
@@ -2,8 +2,8 @@
 # $FreeBSD$
 
 PORTNAME=		frama-c
-DISTVERSIONPREFIX=	Oxygen-
-DISTVERSION=		20120901
+DISTVERSIONPREFIX=	Neon-
+DISTVERSION=		20140301
 CATEGORIES=		devel
 MASTER_SITES=		http://frama-c.com/download/ LOCAL/bf
 
@@ -15,21 +15,19 @@ LICENSE=	LGPL21
 BUILD_DEPENDS=	${LOCALBASE}/lib/ocaml/ocamlgraph/graph.a:${PORTSDIR}/math/ocaml-ocamlgraph
 RUN_DEPENDS=	${LOCALBASE}/lib/ocaml/ocamlgraph/graph.a:${PORTSDIR}/math/ocaml-ocamlgraph
 
+USES=		gmake
+USE_OCAML=	yes
 GNU_CONFIGURE=	yes
 CONFIGURE_ARGS+=	--with-cpp="${FRAMAC_DEFAULT_CPP}"
-MAKE_ENV+=	FRAMAC_LIBDIR="${PREFIX}/lib/frama-c"
-MAN1=		frama-c.1 frama-c-gui.1
+MAKE_ENV+=	FRAMAC_LIBDIR="${STAGEDIR}${PREFIX}/lib/frama-c"
 
-OPTIONS_DEFINE=		ALTERGO COQ GUI PLUGINS
-OPTIONS_DEFAULT=	ALTERGO GUI PLUGINS
+OPTIONS_DEFINE=	ALTERGO COQ GUI PLUGINS
+OPTIONS_DEFAULT=ALTERGO GUI PLUGINS
+OPTIONS_SUB=	yes
 ALTERGO_DESC=	Alt-Ergo plugin (requires PLUGINS)
 COQ_DESC=	Coq plugin (requires PLUGINS)
 GUI_DESC=	Graphical User Interface (requires PLUGINS)
 
-USE_GMAKE=	yes
-USE_OCAML=	yes
-
-NO_STAGE=	yes
 .include <bsd.port.options.mk>
 
 FRAMAC_DEFAULT_CPP?=	${CPP} -C -I${DATADIR}/libc -I.
@@ -38,44 +36,40 @@ FRAMAC_DEFAULT_CPP?=	${CPP} -C -I${DATADIR}/libc -I.
 .if !${PORT_OPTIONS:MPLUGINS}
 IGNORE=	the Alt-Ergo plugin requires the PLUGINS option to be enabled
 .endif
-BUILD_DEPENDS +=	alt-ergo:${PORTSDIR}/math/alt-ergo
+BUILD_DEPENDS+=		alt-ergo:${PORTSDIR}/math/alt-ergo
 RUN_DEPENDS+=		alt-ergo:${PORTSDIR}/math/alt-ergo
 .else
-CONFIGURE_ENV +=	HAS_ALTERGO=no
+CONFIGURE_ENV+=		HAS_ALTERGO=no
 .endif
 
 .if ${PORT_OPTIONS:MCOQ}
 .if !${PORT_OPTIONS:MPLUGINS}
 IGNORE=	the Coq plugin requires the PLUGINS option to be enabled
 .endif
-BUILD_DEPENDS +=	coqc:${PORTSDIR}/math/coq
+BUILD_DEPENDS+=		coqc:${PORTSDIR}/math/coq
 RUN_DEPENDS+=		coqc:${PORTSDIR}/math/coq
 .else
-CONFIGURE_ENV +=	HAS_COQ=no
+CONFIGURE_ENV+=		HAS_COQ=no
 .endif
 
 .if ${PORT_OPTIONS:MGUI}
 .if !${PORT_OPTIONS:MPLUGINS}
 IGNORE=	the GUI requires the PLUGINS option to be enabled
 .endif
-BUILD_DEPENDS +=	lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2
+BUILD_DEPENDS+=		lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2
 RUN_DEPENDS+=		lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2
 CONFIGURE_ARGS+=	--enable-gui
-PLIST_SUB+=		GUI=""
 .else
 CONFIGURE_ARGS+=	--disable-gui
-PLIST_SUB+=		GUI="@comment "
 .endif
 
 .if ${PORT_OPTIONS:MPLUGINS}
-BUILD_DEPENDS +=	dot:${PORTSDIR}/graphics/graphviz \
+BUILD_DEPENDS+=		dot:${PORTSDIR}/graphics/graphviz \
 			ltl2ba:${PORTSDIR}/math/ltl2ba
 RUN_DEPENDS+=	 	dot:${PORTSDIR}/graphics/graphviz \
 			ltl2ba:${PORTSDIR}/math/ltl2ba
-PLIST_SUB+=		PLUGINS=""
 .else
 CONFIGURE_ARGS+=	--with-no-plugin
-PLIST_SUB+=		PLUGINS="@comment "
 .endif
 
 post-patch:
@@ -119,8 +113,8 @@ pre-configure:
 .endif
 
 post-install:
-	@${TOUCH} ${PREFIX}/lib/frama-c/plugins/.keep_me \
-	${PREFIX}/lib/frama-c/plugins/gui/.keep_me
+	@${TOUCH} ${STAGEDIR}${PREFIX}/lib/frama-c/plugins/.keep_me \
+		${STAGEDIR}${PREFIX}/lib/frama-c/plugins/gui/.keep_me
 
 check regression-test test: build
 	@cd ${WRKSRC}; ${SETENV} ${MAKE_ENV:NCPP=*} \
diff --git a/devel/frama-c/distinfo b/devel/frama-c/distinfo
index 2d56d9909f4d..49700687e546 100644
--- a/devel/frama-c/distinfo
+++ b/devel/frama-c/distinfo
@@ -1,2 +1,2 @@
-SHA256 (frama-c-Oxygen-20120901.tar.gz) = f749870a2451f97d24da886c0cc7708e3ec57ad3f169f6b79f9b52be1f47c216
-SIZE (frama-c-Oxygen-20120901.tar.gz) = 10815011
+SHA256 (frama-c-Neon-20140301.tar.gz) = c5a0606f5c2d56280fd90f979c07ff398acb1e6a661323438b8d0cbd8f9f4731
+SIZE (frama-c-Neon-20140301.tar.gz) = 3122492
diff --git a/devel/frama-c/files/patch-Support_OCamlgraph185 b/devel/frama-c/files/patch-Support_OCamlgraph185
new file mode 100644
index 000000000000..889c411e1a1d
--- /dev/null
+++ b/devel/frama-c/files/patch-Support_OCamlgraph185
@@ -0,0 +1,219 @@
+This patchset came from Debian Frama-c Neon package
+
+--- src/impact/reason_graph.ml
++++ src/impact/reason_graph.ml
+@@ -139,7 +139,7 @@ module Printer (X: AdditionalInfo) = struct
+ 
+   let graph_attributes _ = [`Label "Impact graph"]
+ 
+-  let default_vertex_attributes _g = [`Style [`Filled]; `Shape `Box]
++  let default_vertex_attributes _g = [`Style `Filled; `Shape `Box]
+   let default_edge_attributes _g = []
+ 
+   let vertex_attributes v =
+--- src/kernel/stmts_graph.ml
++++ src/kernel/stmts_graph.ml
+@@ -157,12 +157,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/logic/property_status.ml
++++ src/logic/property_status.ml
+@@ -1481,12 +1481,12 @@ 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;  ]
+ 	      (*| Correctness_parameter _ (*as v*) -> assert false (*[ label v; `Color 0xb0c4de ]*)*)
+@@ -1495,7 +1495,7 @@ module Consolidation_graph = struct
+ 	      | 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/misc/service_graph.ml
++++ src/misc/service_graph.ml
+@@ -289,7 +289,7 @@ Src root:%s in %s (is_root:%b) Dst:%s in %s (is_root:%b) [2d case]"
+         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 _ = []
+@@ -303,7 +303,7 @@ Src root:%s in %s (is_root:%b) Dst:%s in %s (is_root:%b) [2d case]"
+           sg_attributes =
+             [ `Label ("S " ^ cs);
+               `Color (Extlib.number_to_color id);
+-              `Style [`Bold] ] }
++              `Style `Bold ] }
+ 
+   end
+ 
+--- src/pdg_types/pdgTypes.ml
++++ src/pdg_types/pdgTypes.ml
+@@ -626,7 +626,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 =
+@@ -711,13 +711,13 @@ 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;
+                sg_parent = None;
+                sg_attributes = attrib }
+--- src/postdominators/print.ml
++++ src/postdominators/print.ml
+@@ -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/semantic_callgraph/register.ml
++++ src/semantic_callgraph/register.ml
+@@ -102,8 +102,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/slicing/printSlice.ml
++++ src/slicing/printSlice.ml
+@@ -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,16 +280,16 @@ 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;
+                  sg_parent = None;
+                  sg_attributes = attrib }
+--- src/syntactic_callgraph/register.ml
++++ src/syntactic_callgraph/register.ml
+@@ -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/wp/cil2cfg.ml
++++ src/wp/cil2cfg.ml
+@@ -1278,9 +1278,9 @@ module Printer (PE : sig val edge_txt : edge -> string end) = struct
+       | Vstart | Vend | Vexit -> [`Color 0x0000FF; `Shape `Doublecircle]
+       | VfctIn | VfctOut -> [`Color 0x0000FF; `Shape `Box]
+       | VblkIn _ | VblkOut _ -> [`Shape `Box]
+-      | Vloop _ | Vloop2 _ -> [`Color 0xFF0000; `Style [`Filled]]
++      | Vloop _ | Vloop2 _ -> [`Color 0xFF0000; `Style `Filled]
+       | Vtest _ | Vswitch _ ->
+-        [`Color 0x00FF00; `Style [`Filled]; `Shape `Diamond]
++        [`Color 0x00FF00; `Style `Filled; `Shape `Diamond]
+       | Vcall _ | Vstmt _ -> []
+     in (`Label (String.escaped label))::attr
+ 
+@@ -1290,15 +1290,15 @@ module Printer (PE : sig val edge_txt : edge -> string end) = struct
+     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
+@@ -1308,7 +1308,7 @@ module Printer (PE : sig val edge_txt : edge -> string end) = struct
+ 
+   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;
+                  sg_parent = None;
+                  sg_attributes = attrib }
+-- 
diff --git a/devel/frama-c/pkg-descr b/devel/frama-c/pkg-descr
index 1f35d5b8309d..eb0c45a200ff 100644
--- a/devel/frama-c/pkg-descr
+++ b/devel/frama-c/pkg-descr
@@ -13,4 +13,4 @@ code where an error can happen at run-time. And it allows its user to
 manipulate functional specifications, and to prove that the source code
 satisfies these specifications.
 
-WWW:	http://frama-c.com/index.html
+WWW: http://frama-c.com/index.html
diff --git a/devel/frama-c/pkg-plist b/devel/frama-c/pkg-plist
index 22ce37585208..5dd96d84d731 100644
--- a/devel/frama-c/pkg-plist
+++ b/devel/frama-c/pkg-plist
@@ -1,94 +1,23 @@
+bin/frama-c
 %%GUI%%bin/frama-c-gui
 %%GUI%%bin/frama-c-gui.byte
-bin/frama-c
 bin/frama-c.byte
-bin/ptests.byte
-%%GUI%%lib/frama-c/analyses_manager.cmi
-%%GUI%%lib/frama-c/analyses_manager.cmo
-%%GUI%%lib/frama-c/analyses_manager.cmx
-%%GUI%%lib/frama-c/analyses_manager.o
-%%GUI%%lib/frama-c/book_manager.cmi
-%%GUI%%lib/frama-c/book_manager.cmo
-%%GUI%%lib/frama-c/book_manager.cmx
-%%GUI%%lib/frama-c/book_manager.o
-%%GUI%%lib/frama-c/debug_manager.cmi
-%%GUI%%lib/frama-c/debug_manager.cmo
-%%GUI%%lib/frama-c/debug_manager.cmx
-%%GUI%%lib/frama-c/debug_manager.o
-%%GUI%%lib/frama-c/design.cmi
-%%GUI%%lib/frama-c/design.cmo
-%%GUI%%lib/frama-c/design.cmx
-%%GUI%%lib/frama-c/design.o
-%%GUI%%lib/frama-c/file_manager.cmi
-%%GUI%%lib/frama-c/file_manager.cmo
-%%GUI%%lib/frama-c/file_manager.cmx
-%%GUI%%lib/frama-c/file_manager.o
-%%GUI%%lib/frama-c/filetree.cmi
-%%GUI%%lib/frama-c/filetree.cmo
-%%GUI%%lib/frama-c/filetree.cmx
-%%GUI%%lib/frama-c/filetree.o
-%%GUI%%lib/frama-c/gtk_form.cmi
-%%GUI%%lib/frama-c/gtk_form.cmo
-%%GUI%%lib/frama-c/gtk_form.cmx
-%%GUI%%lib/frama-c/gtk_form.o
-%%GUI%%lib/frama-c/gtk_helper.cmi
-%%GUI%%lib/frama-c/gtk_helper.cmo
-%%GUI%%lib/frama-c/gtk_helper.cmx
-%%GUI%%lib/frama-c/gtk_helper.o
-%%GUI%%lib/frama-c/gui_init.cmi
-%%GUI%%lib/frama-c/gui_parameters.cmi
-%%GUI%%lib/frama-c/gui_parameters.cmo
-%%GUI%%lib/frama-c/gui_parameters.cmx
-%%GUI%%lib/frama-c/gui_parameters.o
-%%GUI%%lib/frama-c/help_manager.cmi
-%%GUI%%lib/frama-c/help_manager.cmo
-%%GUI%%lib/frama-c/help_manager.cmx
-%%GUI%%lib/frama-c/help_manager.o
-%%GUI%%lib/frama-c/history.cmi
-%%GUI%%lib/frama-c/history.cmo
-%%GUI%%lib/frama-c/history.cmx
-%%GUI%%lib/frama-c/history.o
-%%GUI%%lib/frama-c/launcher.cmi
-%%GUI%%lib/frama-c/launcher.cmo
-%%GUI%%lib/frama-c/launcher.cmx
-%%GUI%%lib/frama-c/launcher.o
-%%GUI%%lib/frama-c/menu_manager.cmi
-%%GUI%%lib/frama-c/menu_manager.cmo
-%%GUI%%lib/frama-c/menu_manager.cmx
-%%GUI%%lib/frama-c/menu_manager.o
-%%GUI%%lib/frama-c/plugins/gui/Security_slicing.cmi
-%%GUI%%lib/frama-c/plugins/gui/Security_slicing.cmo
-%%GUI%%lib/frama-c/plugins/gui/Security_slicing.cmxs
-%%GUI%%lib/frama-c/plugins/gui/Wp.cma
-%%GUI%%lib/frama-c/plugins/gui/Wp.cmi
-%%GUI%%lib/frama-c/plugins/gui/Wp.cmxs
-%%GUI%%lib/frama-c/pretty_source.cmi
-%%GUI%%lib/frama-c/pretty_source.cmo
-%%GUI%%lib/frama-c/pretty_source.cmx
-%%GUI%%lib/frama-c/pretty_source.o
-%%GUI%%lib/frama-c/project_manager.cmi
-%%GUI%%lib/frama-c/project_manager.cmo
-%%GUI%%lib/frama-c/project_manager.cmx
-%%GUI%%lib/frama-c/project_manager.o
-%%GUI%%lib/frama-c/property_navigator.cmi
-%%GUI%%lib/frama-c/property_navigator.cmo
-%%GUI%%lib/frama-c/property_navigator.cmx
-%%GUI%%lib/frama-c/property_navigator.o
-%%GUI%%lib/frama-c/source_manager.cmi
-%%GUI%%lib/frama-c/source_manager.cmo
-%%GUI%%lib/frama-c/source_manager.cmx
-%%GUI%%lib/frama-c/source_manager.o
-%%GUI%%lib/frama-c/source_viewer.cmi
-%%GUI%%lib/frama-c/source_viewer.cmo
-%%GUI%%lib/frama-c/source_viewer.cmx
-%%GUI%%lib/frama-c/source_viewer.o
-%%GUI%%lib/frama-c/warning_manager.cmi
-%%GUI%%lib/frama-c/warning_manager.cmo
-%%GUI%%lib/frama-c/warning_manager.cmx
-%%GUI%%lib/frama-c/warning_manager.o
+bin/ptests.opt
 %%PLUGINS%%lib/frama-c/Constant_Propagation.cmo
 %%PLUGINS%%lib/frama-c/Constant_Propagation.cmx
 %%PLUGINS%%lib/frama-c/Constant_Propagation.o
+lib/frama-c/FCHashtbl.cmi
+lib/frama-c/FCHashtbl.cmo
+lib/frama-c/FCHashtbl.cmx
+lib/frama-c/FCHashtbl.o
+lib/frama-c/FCMap.cmi
+lib/frama-c/FCMap.cmo
+lib/frama-c/FCMap.cmx
+lib/frama-c/FCMap.o
+lib/frama-c/FCSet.cmi
+lib/frama-c/FCSet.cmo
+lib/frama-c/FCSet.cmx
+lib/frama-c/FCSet.o
 %%PLUGINS%%lib/frama-c/From.cmo
 %%PLUGINS%%lib/frama-c/From.cmx
 %%PLUGINS%%lib/frama-c/From.o
@@ -134,21 +63,6 @@ bin/ptests.byte
 %%PLUGINS%%lib/frama-c/Value.cmo
 %%PLUGINS%%lib/frama-c/Value.cmx
 %%PLUGINS%%lib/frama-c/Value.o
-%%PLUGINS%%lib/frama-c/plugins/Aorai.cmi
-%%PLUGINS%%lib/frama-c/plugins/Aorai.cmo
-%%PLUGINS%%lib/frama-c/plugins/Aorai.cmxs
-%%PLUGINS%%lib/frama-c/plugins/Obfuscator.cmi
-%%PLUGINS%%lib/frama-c/plugins/Obfuscator.cmo
-%%PLUGINS%%lib/frama-c/plugins/Obfuscator.cmxs
-%%PLUGINS%%lib/frama-c/plugins/Report.cmi
-%%PLUGINS%%lib/frama-c/plugins/Report.cmo
-%%PLUGINS%%lib/frama-c/plugins/Report.cmxs
-%%PLUGINS%%lib/frama-c/plugins/Security_slicing.cmi
-%%PLUGINS%%lib/frama-c/plugins/Security_slicing.cmo
-%%PLUGINS%%lib/frama-c/plugins/Security_slicing.cmxs
-%%PLUGINS%%lib/frama-c/plugins/Wp.cma
-%%PLUGINS%%lib/frama-c/plugins/Wp.cmi
-%%PLUGINS%%lib/frama-c/plugins/Wp.cmxs
 lib/frama-c/abstract_interp.cmi
 lib/frama-c/abstract_interp.cmo
 lib/frama-c/abstract_interp.cmx
@@ -165,6 +79,10 @@ lib/frama-c/alpha.cmi
 lib/frama-c/alpha.cmo
 lib/frama-c/alpha.cmx
 lib/frama-c/alpha.o
+%%GUI%%lib/frama-c/analyses_manager.cmi
+%%GUI%%lib/frama-c/analyses_manager.cmo
+%%GUI%%lib/frama-c/analyses_manager.cmx
+%%GUI%%lib/frama-c/analyses_manager.o
 lib/frama-c/annotations.cmi
 lib/frama-c/annotations.cmo
 lib/frama-c/annotations.cmx
@@ -177,10 +95,6 @@ lib/frama-c/ast_info.cmi
 lib/frama-c/ast_info.cmo
 lib/frama-c/ast_info.cmx
 lib/frama-c/ast_info.o
-lib/frama-c/ast_printer.cmi
-lib/frama-c/ast_printer.cmo
-lib/frama-c/ast_printer.cmx
-lib/frama-c/ast_printer.o
 lib/frama-c/availexpslv.cmi
 lib/frama-c/availexpslv.cmo
 lib/frama-c/availexpslv.cmx
@@ -193,18 +107,10 @@ lib/frama-c/base.cmi
 lib/frama-c/base.cmo
 lib/frama-c/base.cmx
 lib/frama-c/base.o
-lib/frama-c/base_Set_Lattice.cmi
-lib/frama-c/base_Set_Lattice.cmo
-lib/frama-c/base_Set_Lattice.cmx
-lib/frama-c/base_Set_Lattice.o
 lib/frama-c/binary_cache.cmi
 lib/frama-c/binary_cache.cmo
 lib/frama-c/binary_cache.cmx
 lib/frama-c/binary_cache.o
-lib/frama-c/bit_model_access.cmi
-lib/frama-c/bit_model_access.cmo
-lib/frama-c/bit_model_access.cmx
-lib/frama-c/bit_model_access.o
 lib/frama-c/bit_utils.cmi
 lib/frama-c/bit_utils.cmo
 lib/frama-c/bit_utils.cmx
@@ -213,6 +119,10 @@ lib/frama-c/bitvector.cmi
 lib/frama-c/bitvector.cmo
 lib/frama-c/bitvector.cmx
 lib/frama-c/bitvector.o
+%%GUI%%lib/frama-c/book_manager.cmi
+%%GUI%%lib/frama-c/book_manager.cmo
+%%GUI%%lib/frama-c/book_manager.cmx
+%%GUI%%lib/frama-c/book_manager.o
 lib/frama-c/boot.cmi
 lib/frama-c/boot.cmo
 lib/frama-c/boot.cmx
@@ -230,6 +140,10 @@ lib/frama-c/cabs2cil.cmi
 lib/frama-c/cabs2cil.cmo
 lib/frama-c/cabs2cil.cmx
 lib/frama-c/cabs2cil.o
+lib/frama-c/cabs_debug.cmi
+lib/frama-c/cabs_debug.cmo
+lib/frama-c/cabs_debug.cmx
+lib/frama-c/cabs_debug.o
 lib/frama-c/cabsbranches.cmi
 lib/frama-c/cabsbranches.cmo
 lib/frama-c/cabsbranches.cmx
@@ -270,31 +184,31 @@ lib/frama-c/cil_datatype.cmi
 lib/frama-c/cil_datatype.cmo
 lib/frama-c/cil_datatype.cmx
 lib/frama-c/cil_datatype.o
+lib/frama-c/cil_descriptive_printer.cmi
+lib/frama-c/cil_descriptive_printer.cmo
+lib/frama-c/cil_descriptive_printer.cmx
+lib/frama-c/cil_descriptive_printer.o
+lib/frama-c/cil_printer.cmi
+lib/frama-c/cil_printer.cmo
+lib/frama-c/cil_printer.cmx
+lib/frama-c/cil_printer.o
 lib/frama-c/cil_state_builder.cmi
 lib/frama-c/cil_state_builder.cmo
 lib/frama-c/cil_state_builder.cmx
 lib/frama-c/cil_state_builder.o
 lib/frama-c/cil_types.cmi
-lib/frama-c/cilglobopt.cmi
-lib/frama-c/cilglobopt.cmo
-lib/frama-c/cilglobopt.cmx
-lib/frama-c/cilglobopt.o
+lib/frama-c/cilconfig.cmi
+lib/frama-c/cilconfig.cmo
+lib/frama-c/cilconfig.cmx
+lib/frama-c/cilconfig.o
 lib/frama-c/cilmsg.cmi
 lib/frama-c/cilmsg.cmo
 lib/frama-c/cilmsg.cmx
 lib/frama-c/cilmsg.o
-lib/frama-c/cilutil.cmi
-lib/frama-c/cilutil.cmo
-lib/frama-c/cilutil.cmx
-lib/frama-c/cilutil.o
 lib/frama-c/clexer.cmi
 lib/frama-c/clexer.cmo
 lib/frama-c/clexer.cmx
 lib/frama-c/clexer.o
-lib/frama-c/clist.cmi
-lib/frama-c/clist.cmo
-lib/frama-c/clist.cmx
-lib/frama-c/clist.o
 lib/frama-c/cmdline.cmi
 lib/frama-c/cmdline.cmo
 lib/frama-c/cmdline.cmx
@@ -323,6 +237,14 @@ lib/frama-c/dataflow.cmi
 lib/frama-c/dataflow.cmo
 lib/frama-c/dataflow.cmx
 lib/frama-c/dataflow.o
+lib/frama-c/dataflow2.cmi
+lib/frama-c/dataflow2.cmo
+lib/frama-c/dataflow2.cmx
+lib/frama-c/dataflow2.o
+lib/frama-c/dataflows.cmi
+lib/frama-c/dataflows.cmo
+lib/frama-c/dataflows.cmx
+lib/frama-c/dataflows.o
 lib/frama-c/datatype.cmi
 lib/frama-c/datatype.cmo
 lib/frama-c/datatype.cmx
@@ -335,6 +257,10 @@ lib/frama-c/deadcodeelim.cmi
 lib/frama-c/deadcodeelim.cmo
 lib/frama-c/deadcodeelim.cmx
 lib/frama-c/deadcodeelim.o
+%%GUI%%lib/frama-c/debug_manager.cmi
+%%GUI%%lib/frama-c/debug_manager.cmo
+%%GUI%%lib/frama-c/debug_manager.cmx
+%%GUI%%lib/frama-c/debug_manager.o
 lib/frama-c/descr.cmi
 lib/frama-c/descr.cmo
 lib/frama-c/descr.cmx
@@ -343,6 +269,10 @@ lib/frama-c/description.cmi
 lib/frama-c/description.cmo
 lib/frama-c/description.cmx
 lib/frama-c/description.o
+%%GUI%%lib/frama-c/design.cmi
+%%GUI%%lib/frama-c/design.cmo
+%%GUI%%lib/frama-c/design.cmx
+%%GUI%%lib/frama-c/design.o
 lib/frama-c/dominators.cmi
 lib/frama-c/dominators.cmo
 lib/frama-c/dominators.cmx
@@ -379,6 +309,18 @@ lib/frama-c/file.cmi
 lib/frama-c/file.cmo
 lib/frama-c/file.cmx
 lib/frama-c/file.o
+%%GUI%%lib/frama-c/file_manager.cmi
+%%GUI%%lib/frama-c/file_manager.cmo
+%%GUI%%lib/frama-c/file_manager.cmx
+%%GUI%%lib/frama-c/file_manager.o
+lib/frama-c/filepath.cmi
+lib/frama-c/filepath.cmo
+lib/frama-c/filepath.cmx
+lib/frama-c/filepath.o
+%%GUI%%lib/frama-c/filetree.cmi
+%%GUI%%lib/frama-c/filetree.cmo
+%%GUI%%lib/frama-c/filetree.cmx
+%%GUI%%lib/frama-c/filetree.o
 lib/frama-c/filter.cmi
 lib/frama-c/filter.cmo
 lib/frama-c/filter.cmx
@@ -399,14 +341,27 @@ lib/frama-c/globals.cmi
 lib/frama-c/globals.cmo
 lib/frama-c/globals.cmx
 lib/frama-c/globals.o
-lib/frama-c/growArray.cmi
-lib/frama-c/growArray.cmo
-lib/frama-c/growArray.cmx
-lib/frama-c/growArray.o
-lib/frama-c/hashtbl_common_interface.cmi
-lib/frama-c/hashtbl_common_interface.cmo
-lib/frama-c/hashtbl_common_interface.cmx
-lib/frama-c/hashtbl_common_interface.o
+%%GUI%%lib/frama-c/gtk_form.cmi
+%%GUI%%lib/frama-c/gtk_form.cmo
+%%GUI%%lib/frama-c/gtk_form.cmx
+%%GUI%%lib/frama-c/gtk_form.o
+%%GUI%%lib/frama-c/gtk_helper.cmi
+%%GUI%%lib/frama-c/gtk_helper.cmo
+%%GUI%%lib/frama-c/gtk_helper.cmx
+%%GUI%%lib/frama-c/gtk_helper.o
+%%GUI%%lib/frama-c/gui_init.cmi
+%%GUI%%lib/frama-c/gui_parameters.cmi
+%%GUI%%lib/frama-c/gui_parameters.cmo
+%%GUI%%lib/frama-c/gui_parameters.cmx
+%%GUI%%lib/frama-c/gui_parameters.o
+%%GUI%%lib/frama-c/help_manager.cmi
+%%GUI%%lib/frama-c/help_manager.cmo
+%%GUI%%lib/frama-c/help_manager.cmx
+%%GUI%%lib/frama-c/help_manager.o
+%%GUI%%lib/frama-c/history.cmi
+%%GUI%%lib/frama-c/history.cmo
+%%GUI%%lib/frama-c/history.cmx
+%%GUI%%lib/frama-c/history.o
 lib/frama-c/hook.cmi
 lib/frama-c/hook.cmo
 lib/frama-c/hook.cmx
@@ -443,6 +398,10 @@ lib/frama-c/int_Interv_Map.cmi
 lib/frama-c/int_Interv_Map.cmo
 lib/frama-c/int_Interv_Map.cmx
 lib/frama-c/int_Interv_Map.o
+lib/frama-c/integer.cmi
+lib/frama-c/integer.cmo
+lib/frama-c/integer.cmx
+lib/frama-c/integer.o
 lib/frama-c/ival.cmi
 lib/frama-c/ival.cmo
 lib/frama-c/ival.cmx
@@ -463,7 +422,11 @@ lib/frama-c/lattice_Interval_Set.cmi
 lib/frama-c/lattice_Interval_Set.cmo
 lib/frama-c/lattice_Interval_Set.cmx
 lib/frama-c/lattice_Interval_Set.o
-lib/frama-c/lattice_With_Isotropy.cmi
+lib/frama-c/lattice_type.cmi
+%%GUI%%lib/frama-c/launcher.cmi
+%%GUI%%lib/frama-c/launcher.cmo
+%%GUI%%lib/frama-c/launcher.cmx
+%%GUI%%lib/frama-c/launcher.o
 lib/frama-c/lexerhack.cmi
 lib/frama-c/lexerhack.cmo
 lib/frama-c/lexerhack.cmx
@@ -480,6 +443,7 @@ lib/frama-c/lmap_bitwise.cmi
 lib/frama-c/lmap_bitwise.cmo
 lib/frama-c/lmap_bitwise.cmx
 lib/frama-c/lmap_bitwise.o
+lib/frama-c/lmap_sig.cmi
 lib/frama-c/locations.cmi
 lib/frama-c/locations.cmo
 lib/frama-c/locations.cmx
@@ -533,10 +497,6 @@ lib/frama-c/loop.cmi
 lib/frama-c/loop.cmo
 lib/frama-c/loop.cmx
 lib/frama-c/loop.o
-lib/frama-c/machdep.cmi
-lib/frama-c/machdep.cmo
-lib/frama-c/machdep.cmx
-lib/frama-c/machdep.o
 lib/frama-c/machdep_ppc_32.cmi
 lib/frama-c/machdep_ppc_32.cmo
 lib/frama-c/machdep_ppc_32.cmx
@@ -557,10 +517,10 @@ lib/frama-c/map_Lattice.cmi
 lib/frama-c/map_Lattice.cmo
 lib/frama-c/map_Lattice.cmx
 lib/frama-c/map_Lattice.o
-lib/frama-c/map_common_interface.cmi
-lib/frama-c/map_common_interface.cmo
-lib/frama-c/map_common_interface.cmx
-lib/frama-c/map_common_interface.o
+%%GUI%%lib/frama-c/menu_manager.cmi
+%%GUI%%lib/frama-c/menu_manager.cmo
+%%GUI%%lib/frama-c/menu_manager.cmx
+%%GUI%%lib/frama-c/menu_manager.o
 lib/frama-c/mergecil.cmi
 lib/frama-c/mergecil.cmo
 lib/frama-c/mergecil.cmx
@@ -569,19 +529,6 @@ lib/frama-c/messages.cmi
 lib/frama-c/messages.cmo
 lib/frama-c/messages.cmx
 lib/frama-c/messages.o
-lib/frama-c/my_bigint.cmi
-lib/frama-c/my_bigint.cmo
-lib/frama-c/my_bigint.cmx
-lib/frama-c/my_bigint.o
-lib/frama-c/mybigarray.o
-lib/frama-c/new_offsetmap.cmi
-lib/frama-c/new_offsetmap.cmo
-lib/frama-c/new_offsetmap.cmx
-lib/frama-c/new_offsetmap.o
-lib/frama-c/obfuscate.cmi
-lib/frama-c/obfuscate.cmo
-lib/frama-c/obfuscate.cmx
-lib/frama-c/obfuscate.o
 lib/frama-c/offsetmap.cmi
 lib/frama-c/offsetmap.cmo
 lib/frama-c/offsetmap.cmx
@@ -590,18 +537,33 @@ lib/frama-c/offsetmap_bitwise.cmi
 lib/frama-c/offsetmap_bitwise.cmo
 lib/frama-c/offsetmap_bitwise.cmx
 lib/frama-c/offsetmap_bitwise.o
+lib/frama-c/offsetmap_lattice_with_isotropy.cmi
+lib/frama-c/offsetmap_sig.cmi
 lib/frama-c/oneret.cmi
 lib/frama-c/oneret.cmo
 lib/frama-c/oneret.cmx
 lib/frama-c/oneret.o
+lib/frama-c/ordered_stmt.cmi
+lib/frama-c/ordered_stmt.cmo
+lib/frama-c/ordered_stmt.cmx
+lib/frama-c/ordered_stmt.o
 lib/frama-c/origin.cmi
 lib/frama-c/origin.cmo
 lib/frama-c/origin.cmx
 lib/frama-c/origin.o
-lib/frama-c/parameter.cmi
-lib/frama-c/parameter.cmo
-lib/frama-c/parameter.cmx
-lib/frama-c/parameter.o
+lib/frama-c/parameter_builder.cmi
+lib/frama-c/parameter_builder.cmo
+lib/frama-c/parameter_builder.cmx
+lib/frama-c/parameter_builder.o
+lib/frama-c/parameter_customize.cmi
+lib/frama-c/parameter_customize.cmo
+lib/frama-c/parameter_customize.cmx
+lib/frama-c/parameter_customize.o
+lib/frama-c/parameter_sig.cmi
+lib/frama-c/parameter_state.cmi
+lib/frama-c/parameter_state.cmo
+lib/frama-c/parameter_state.cmx
+lib/frama-c/parameter_state.o
 lib/frama-c/pdgIndex.cmi
 lib/frama-c/pdgIndex.cmo
 lib/frama-c/pdgIndex.cmx
@@ -619,7 +581,32 @@ lib/frama-c/plugin.cmo
 lib/frama-c/plugin.cmx
 lib/frama-c/plugin.o
 lib/frama-c/plugins/.keep_me
+%%PLUGINS%%lib/frama-c/plugins/Aorai.cmi
+%%PLUGINS%%lib/frama-c/plugins/Aorai.cmo
+%%PLUGINS%%lib/frama-c/plugins/Aorai.cmxs
+%%PLUGINS%%lib/frama-c/plugins/Obfuscator.cmi
+%%PLUGINS%%lib/frama-c/plugins/Obfuscator.cmo
+%%PLUGINS%%lib/frama-c/plugins/Obfuscator.cmxs
+%%PLUGINS%%lib/frama-c/plugins/Report.cmi
+%%PLUGINS%%lib/frama-c/plugins/Report.cmo
+%%PLUGINS%%lib/frama-c/plugins/Report.cmxs
+%%GUI%%lib/frama-c/plugins/Security_slicing.cmi
+%%GUI%%lib/frama-c/plugins/Security_slicing.cmo
+%%GUI%%lib/frama-c/plugins/Security_slicing.cmxs
+%%PLUGINS%%lib/frama-c/plugins/Wp.cma
+%%PLUGINS%%lib/frama-c/plugins/Wp.cmi
+%%PLUGINS%%lib/frama-c/plugins/Wp.cmxs
 lib/frama-c/plugins/gui/.keep_me
+%%GUI%%lib/frama-c/plugins/gui/Security_slicing.cmi
+%%GUI%%lib/frama-c/plugins/gui/Security_slicing.cmo
+%%GUI%%lib/frama-c/plugins/gui/Security_slicing.cmxs
+%%GUI%%lib/frama-c/plugins/gui/Wp.cma
+%%GUI%%lib/frama-c/plugins/gui/Wp.cmi
+%%GUI%%lib/frama-c/plugins/gui/Wp.cmxs
+%%GUI%%lib/frama-c/pretty_source.cmi
+%%GUI%%lib/frama-c/pretty_source.cmo
+%%GUI%%lib/frama-c/pretty_source.cmx
+%%GUI%%lib/frama-c/pretty_source.o
 lib/frama-c/pretty_utils.cmi
 lib/frama-c/pretty_utils.cmo
 lib/frama-c/pretty_utils.cmx
@@ -628,14 +615,19 @@ lib/frama-c/printer.cmi
 lib/frama-c/printer.cmo
 lib/frama-c/printer.cmx
 lib/frama-c/printer.o
-lib/frama-c/printexc_common_interface.cmi
-lib/frama-c/printexc_common_interface.cmo
-lib/frama-c/printexc_common_interface.cmx
-lib/frama-c/printexc_common_interface.o
+lib/frama-c/printer_api.cmi
+lib/frama-c/printer_builder.cmi
+lib/frama-c/printer_builder.cmo
+lib/frama-c/printer_builder.cmx
+lib/frama-c/printer_builder.o
 lib/frama-c/project.cmi
 lib/frama-c/project.cmo
 lib/frama-c/project.cmx
 lib/frama-c/project.o
+%%GUI%%lib/frama-c/project_manager.cmi
+%%GUI%%lib/frama-c/project_manager.cmo
+%%GUI%%lib/frama-c/project_manager.cmx
+%%GUI%%lib/frama-c/project_manager.o
 lib/frama-c/project_skeleton.cmi
 lib/frama-c/project_skeleton.cmo
 lib/frama-c/project_skeleton.cmx
@@ -644,11 +636,17 @@ lib/frama-c/property.cmi
 lib/frama-c/property.cmo
 lib/frama-c/property.cmx
 lib/frama-c/property.o
+%%GUI%%lib/frama-c/property_navigator.cmi
+%%GUI%%lib/frama-c/property_navigator.cmo
+%%GUI%%lib/frama-c/property_navigator.cmx
+%%GUI%%lib/frama-c/property_navigator.o
 lib/frama-c/property_status.cmi
 lib/frama-c/property_status.cmo
 lib/frama-c/property_status.cmx
 lib/frama-c/property_status.o
 lib/frama-c/ptests_config.cmi
+lib/frama-c/ptests_config.cmx
+lib/frama-c/ptests_config.o
 lib/frama-c/qstack.cmi
 lib/frama-c/qstack.cmo
 lib/frama-c/qstack.cmx
@@ -673,10 +671,6 @@ lib/frama-c/service_graph.cmi
 lib/frama-c/service_graph.cmo
 lib/frama-c/service_graph.cmx
 lib/frama-c/service_graph.o
-lib/frama-c/setWithNearest.cmi
-lib/frama-c/setWithNearest.cmo
-lib/frama-c/setWithNearest.cmx
-lib/frama-c/setWithNearest.o
 lib/frama-c/slicingInternals.cmi
 lib/frama-c/slicingInternals.cmo
 lib/frama-c/slicingInternals.cmx
@@ -685,6 +679,14 @@ lib/frama-c/slicingTypes.cmi
 lib/frama-c/slicingTypes.cmo
 lib/frama-c/slicingTypes.cmx
 lib/frama-c/slicingTypes.o
+%%GUI%%lib/frama-c/source_manager.cmi
+%%GUI%%lib/frama-c/source_manager.cmo
+%%GUI%%lib/frama-c/source_manager.cmx
+%%GUI%%lib/frama-c/source_manager.o
+%%GUI%%lib/frama-c/source_viewer.cmi
+%%GUI%%lib/frama-c/source_viewer.cmo
+%%GUI%%lib/frama-c/source_viewer.cmx
+%%GUI%%lib/frama-c/source_viewer.o
 lib/frama-c/special_hooks.cmi
 lib/frama-c/special_hooks.cmo
 lib/frama-c/special_hooks.cmx
@@ -721,18 +723,26 @@ lib/frama-c/structural_descr.cmi
 lib/frama-c/structural_descr.cmo
 lib/frama-c/structural_descr.cmx
 lib/frama-c/structural_descr.o
-lib/frama-c/subst.cmi
-lib/frama-c/subst.cmo
-lib/frama-c/subst.cmx
-lib/frama-c/subst.o
+lib/frama-c/sysutil.cmi
+lib/frama-c/sysutil.cmo
+lib/frama-c/sysutil.cmx
+lib/frama-c/sysutil.o
 lib/frama-c/task.cmi
 lib/frama-c/task.cmo
 lib/frama-c/task.cmx
 lib/frama-c/task.o
+%%GUI%%lib/frama-c/toolbox.cmi
+%%GUI%%lib/frama-c/toolbox.cmo
+%%GUI%%lib/frama-c/toolbox.cmx
+%%GUI%%lib/frama-c/toolbox.o
 lib/frama-c/tr_offset.cmi
 lib/frama-c/tr_offset.cmo
 lib/frama-c/tr_offset.cmx
 lib/frama-c/tr_offset.o
+lib/frama-c/trace.cmi
+lib/frama-c/trace.cmo
+lib/frama-c/trace.cmx
+lib/frama-c/trace.o
 lib/frama-c/translate_lightweight.cmi
 lib/frama-c/translate_lightweight.cmo
 lib/frama-c/translate_lightweight.cmx
@@ -741,6 +751,10 @@ lib/frama-c/type.cmi
 lib/frama-c/type.cmo
 lib/frama-c/type.cmx
 lib/frama-c/type.o
+lib/frama-c/typed_parameter.cmi
+lib/frama-c/typed_parameter.cmo
+lib/frama-c/typed_parameter.cmx
+lib/frama-c/typed_parameter.o
 lib/frama-c/unicode.cmi
 lib/frama-c/unicode.cmo
 lib/frama-c/unicode.cmx
@@ -765,27 +779,38 @@ lib/frama-c/utf8_logic.cmi
 lib/frama-c/utf8_logic.cmo
 lib/frama-c/utf8_logic.cmx
 lib/frama-c/utf8_logic.o
-lib/frama-c/value_aux.cmi
-lib/frama-c/value_aux.cmo
-lib/frama-c/value_aux.cmx
-lib/frama-c/value_aux.o
+lib/frama-c/value_messages.cmi
+lib/frama-c/value_messages.cmo
+lib/frama-c/value_messages.cmx
+lib/frama-c/value_messages.o
+lib/frama-c/value_types.cmi
+lib/frama-c/value_types.cmo
+lib/frama-c/value_types.cmx
+lib/frama-c/value_types.o
+lib/frama-c/vector.cmi
+lib/frama-c/vector.cmo
+lib/frama-c/vector.cmx
+lib/frama-c/vector.o
 lib/frama-c/visitor.cmi
 lib/frama-c/visitor.cmo
 lib/frama-c/visitor.cmx
 lib/frama-c/visitor.o
-lib/frama-c/whitetrack.cmi
-lib/frama-c/whitetrack.cmo
-lib/frama-c/whitetrack.cmx
-lib/frama-c/whitetrack.o
+%%GUI%%lib/frama-c/warning_manager.cmi
+%%GUI%%lib/frama-c/warning_manager.cmo
+%%GUI%%lib/frama-c/warning_manager.cmx
+%%GUI%%lib/frama-c/warning_manager.o
 lib/frama-c/widen_type.cmi
 lib/frama-c/widen_type.cmo
 lib/frama-c/widen_type.cmx
 lib/frama-c/widen_type.o
+man/man1/frama-c-gui.1.gz
+man/man1/frama-c.1.gz
 share/emacs/site-lisp/acsl.el
 %%DATADIR%%/Makefile.common
 %%DATADIR%%/Makefile.config
 %%DATADIR%%/Makefile.dynamic
 %%DATADIR%%/Makefile.dynamic_config
+%%DATADIR%%/Makefile.generic
 %%DATADIR%%/Makefile.kernel
 %%DATADIR%%/Makefile.plugin
 %%DATADIR%%/acsl.el
@@ -807,23 +832,24 @@ share/emacs/site-lisp/acsl.el
 %%DATADIR%%/feedback/never_tried.png
 %%DATADIR%%/feedback/surely_invalid.png
 %%DATADIR%%/feedback/surely_valid.png
+%%DATADIR%%/feedback/switch-off.png
+%%DATADIR%%/feedback/switch-on.png
 %%DATADIR%%/feedback/unknown.png
 %%DATADIR%%/feedback/unknown_but_dead.png
 %%DATADIR%%/feedback/valid_but_dead.png
 %%DATADIR%%/feedback/valid_under_hyp.png
-%%DATADIR%%/fluctuat.h
 %%DATADIR%%/frama-c.gif
 %%DATADIR%%/frama-c.ico
 %%DATADIR%%/frama-c.rc
 %%DATADIR%%/libc.c
 %%DATADIR%%/libc.h
-%%DATADIR%%/libc/__fc_builtin.c
 %%DATADIR%%/libc/__fc_builtin.h
 %%DATADIR%%/libc/__fc_builtin_for_normalization.i
 %%DATADIR%%/libc/__fc_define_blkcnt_t.h
 %%DATADIR%%/libc/__fc_define_blksize_t.h
 %%DATADIR%%/libc/__fc_define_dev_t.h
 %%DATADIR%%/libc/__fc_define_fd_set_t.h
+%%DATADIR%%/libc/__fc_define_file.h
 %%DATADIR%%/libc/__fc_define_id_t.h
 %%DATADIR%%/libc/__fc_define_ino_t.h
 %%DATADIR%%/libc/__fc_define_intptr_t.h
@@ -840,166 +866,171 @@ share/emacs/site-lisp/acsl.el
 %%DATADIR%%/libc/__fc_define_size_t.h
 %%DATADIR%%/libc/__fc_define_sockaddr.h
 %%DATADIR%%/libc/__fc_define_ssize_t.h
+%%DATADIR%%/libc/__fc_define_stat.h
 %%DATADIR%%/libc/__fc_define_suseconds_t.h
 %%DATADIR%%/libc/__fc_define_time_t.h
 %%DATADIR%%/libc/__fc_define_timespec.h
 %%DATADIR%%/libc/__fc_define_uid_and_gid.h
 %%DATADIR%%/libc/__fc_define_useconds_t.h
 %%DATADIR%%/libc/__fc_define_wchar_t.h
+%%DATADIR%%/libc/__fc_define_wint_t.h
 %%DATADIR%%/libc/__fc_machdep.h
+%%DATADIR%%/libc/__fc_machdep_linux_gcc_shared.h
+%%DATADIR%%/libc/__fc_select.h
 %%DATADIR%%/libc/__fc_string_axiomatic.h
-%%DATADIR%%/libc/arpa/inet.c
 %%DATADIR%%/libc/arpa/inet.h
-%%DATADIR%%/libc/assert.c
 %%DATADIR%%/libc/assert.h
-%%DATADIR%%/libc/complex.c
+%%DATADIR%%/libc/byteswap.h
 %%DATADIR%%/libc/complex.h
-%%DATADIR%%/libc/ctype.c
 %%DATADIR%%/libc/ctype.h
-%%DATADIR%%/libc/dirent.c
 %%DATADIR%%/libc/dirent.h
-%%DATADIR%%/libc/errno.c
+%%DATADIR%%/libc/dlfcn.h
+%%DATADIR%%/libc/endian.h
 %%DATADIR%%/libc/errno.h
-%%DATADIR%%/libc/fc_posix_runtime.c
-%%DATADIR%%/libc/fc_runtime.c
-%%DATADIR%%/libc/fcntl.c
 %%DATADIR%%/libc/fcntl.h
-%%DATADIR%%/libc/fenv.c
+%%DATADIR%%/libc/features.h
 %%DATADIR%%/libc/fenv.h
-%%DATADIR%%/libc/float.c
 %%DATADIR%%/libc/float.h
-%%DATADIR%%/libc/iconv.c
+%%DATADIR%%/libc/getopt.h
+%%DATADIR%%/libc/glob.h
+%%DATADIR%%/libc/grp.h
 %%DATADIR%%/libc/iconv.h
-%%DATADIR%%/libc/ifaddrs.c
 %%DATADIR%%/libc/ifaddrs.h
-%%DATADIR%%/libc/inttypes.c
 %%DATADIR%%/libc/inttypes.h
-%%DATADIR%%/libc/iso646.c
 %%DATADIR%%/libc/iso646.h
-%%DATADIR%%/libc/limits.c
+%%DATADIR%%/libc/libgen.h
+%%DATADIR%%/libc/libintl.h
 %%DATADIR%%/libc/limits.h
-%%DATADIR%%/libc/linux/fs.c
 %%DATADIR%%/libc/linux/fs.h
-%%DATADIR%%/libc/locale.c
+%%DATADIR%%/libc/linux/if_addr.h
+%%DATADIR%%/libc/linux/if_netlink.h
+%%DATADIR%%/libc/linux/netlink.h
+%%DATADIR%%/libc/linux/rtnetlink.h
 %%DATADIR%%/libc/locale.h
-%%DATADIR%%/libc/math.c
 %%DATADIR%%/libc/math.h
-%%DATADIR%%/libc/net/if.c
 %%DATADIR%%/libc/net/if.h
-%%DATADIR%%/libc/netinet/in.c
+%%DATADIR%%/libc/netdb.h
 %%DATADIR%%/libc/netinet/in.h
-%%DATADIR%%/libc/nl_types.c
+%%DATADIR%%/libc/netinet/in_systm.h
+%%DATADIR%%/libc/netinet/ip.h
+%%DATADIR%%/libc/netinet/ip_icmp.h
 %%DATADIR%%/libc/nl_types.h
-%%DATADIR%%/libc/pwd.c
 %%DATADIR%%/libc/pwd.h
-%%DATADIR%%/libc/setjmp.c
+%%DATADIR%%/libc/regex.h
 %%DATADIR%%/libc/setjmp.h
-%%DATADIR%%/libc/signal.c
 %%DATADIR%%/libc/signal.h
-%%DATADIR%%/libc/stdarg.c
 %%DATADIR%%/libc/stdarg.h
-%%DATADIR%%/libc/stdbool.c
 %%DATADIR%%/libc/stdbool.h
-%%DATADIR%%/libc/stddef.c
 %%DATADIR%%/libc/stddef.h
-%%DATADIR%%/libc/stdint.c
 %%DATADIR%%/libc/stdint.h
-%%DATADIR%%/libc/stdio.c
 %%DATADIR%%/libc/stdio.h
-%%DATADIR%%/libc/stdlib.c
 %%DATADIR%%/libc/stdlib.h
-%%DATADIR%%/libc/string.c
 %%DATADIR%%/libc/string.h
-%%DATADIR%%/libc/strings.c
 %%DATADIR%%/libc/strings.h
-%%DATADIR%%/libc/sys/ioctl.c
 %%DATADIR%%/libc/sys/ioctl.h
-%%DATADIR%%/libc/sys/param.c
 %%DATADIR%%/libc/sys/param.h
-%%DATADIR%%/libc/sys/resource.c
 %%DATADIR%%/libc/sys/resource.h
-%%DATADIR%%/libc/sys/select.c
 %%DATADIR%%/libc/sys/select.h
-%%DATADIR%%/libc/sys/socket.c
 %%DATADIR%%/libc/sys/socket.h
-%%DATADIR%%/libc/sys/stat.c
 %%DATADIR%%/libc/sys/stat.h
-%%DATADIR%%/libc/sys/time.c
+%%DATADIR%%/libc/sys/sysctl.h
 %%DATADIR%%/libc/sys/time.h
-%%DATADIR%%/libc/sys/types.c
 %%DATADIR%%/libc/sys/types.h
-%%DATADIR%%/libc/sys/uio.c
 %%DATADIR%%/libc/sys/uio.h
-%%DATADIR%%/libc/sys/un.c
 %%DATADIR%%/libc/sys/un.h
-%%DATADIR%%/libc/sys/wait.c
 %%DATADIR%%/libc/sys/wait.h
-%%DATADIR%%/libc/syslog.c
 %%DATADIR%%/libc/syslog.h
-%%DATADIR%%/libc/termios.c
 %%DATADIR%%/libc/termios.h
-%%DATADIR%%/libc/test.c
-%%DATADIR%%/libc/tgmath.c
 %%DATADIR%%/libc/tgmath.h
-%%DATADIR%%/libc/time.c
 %%DATADIR%%/libc/time.h
-%%DATADIR%%/libc/uchar.c
 %%DATADIR%%/libc/uchar.h
-%%DATADIR%%/libc/unistd.c
 %%DATADIR%%/libc/unistd.h
-%%DATADIR%%/libc/wchar.c
 %%DATADIR%%/libc/wchar.h
-%%DATADIR%%/libc/wctype.c
 %%DATADIR%%/libc/wctype.h
 %%DATADIR%%/machine.h
-%%DATADIR%%/malloc.c
-%%DATADIR%%/manuals/acsl-implementation.pdf
-%%DATADIR%%/manuals/acsl.pdf
-%%DATADIR%%/manuals/aorai-manual.pdf
-%%DATADIR%%/manuals/metrics-manual.pdf
-%%DATADIR%%/manuals/plugin-development-guide.pdf
-%%DATADIR%%/manuals/rte-manual.pdf
-%%DATADIR%%/manuals/user-manual.pdf
-%%DATADIR%%/manuals/value-analysis.pdf
-%%DATADIR%%/manuals/wp-manual.pdf
-%%DATADIR%%/manuals/wp-tutorial.pdf
 %%DATADIR%%/math.c
 %%DATADIR%%/math.h
 %%DATADIR%%/unmark.png
-%%PLUGINS%%%%DATADIR%%/wp/Cfloat.v
-%%PLUGINS%%%%DATADIR%%/wp/Cint.v
-%%PLUGINS%%%%DATADIR%%/wp/Cmath.v
-%%PLUGINS%%%%DATADIR%%/wp/Memory.v
-%%PLUGINS%%%%DATADIR%%/wp/Qedlib.v
-%%PLUGINS%%%%DATADIR%%/wp/Vset.v
-%%PLUGINS%%%%DATADIR%%/wp/cfloat.mlw
-%%PLUGINS%%%%DATADIR%%/wp/cint.mlw
-%%PLUGINS%%%%DATADIR%%/wp/cmath.mlw
-%%PLUGINS%%%%DATADIR%%/wp/hoare_ergo.why
-%%PLUGINS%%%%DATADIR%%/wp/hoare_model.v
-%%PLUGINS%%%%DATADIR%%/wp/hoare_model.why
-%%PLUGINS%%%%DATADIR%%/wp/memory.mlw
-%%PLUGINS%%%%DATADIR%%/wp/qed.mlw
-%%PLUGINS%%%%DATADIR%%/wp/runtime_ergo.why
-%%PLUGINS%%%%DATADIR%%/wp/runtime_model.v
-%%PLUGINS%%%%DATADIR%%/wp/runtime_model.why
-%%PLUGINS%%%%DATADIR%%/wp/store_ergo.why
-%%PLUGINS%%%%DATADIR%%/wp/store_model.v
-%%PLUGINS%%%%DATADIR%%/wp/store_model.why
-%%PLUGINS%%%%DATADIR%%/wp/vset.mlw
-%%PLUGINS%%%%DATADIR%%/wp/wp.v
-@dirrm lib/frama-c/plugins/gui
-@dirrm lib/frama-c/plugins
-@dirrm lib/frama-c
-%%PLUGINS%%@dirrm %%DATADIR%%/wp
-@dirrm %%DATADIR%%/manuals
-@dirrm %%DATADIR%%/libc/sys
-@dirrm %%DATADIR%%/libc/netinet
-@dirrm %%DATADIR%%/libc/net
-@dirrm %%DATADIR%%/libc/linux
-@dirrm %%DATADIR%%/libc/arpa
-@dirrm %%DATADIR%%/libc
-@dirrm %%DATADIR%%/feedback
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/Bits.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/BuiltIn.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/Cbits.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/Cfloat.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/Cint.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/Cmath.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/Memory.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/Qed.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/Qedlib.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/Vset.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/Zbits.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/bool/Bool.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/int/Abs.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/int/ComputerDivision.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/int/Int.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/int/MinMax.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/map/Map.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/real/Abs.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/real/FromInt.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/real/MinMax.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/real/Real.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/real/RealInfix.v
+%%PLUGINS%%%%DATADIR%%/wp/coqwp/real/Square.v
+%%PLUGINS%%%%DATADIR%%/wp/ergo/Cbits.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/Cfloat.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/Cint.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/Cmath.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/Memory.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/Qed.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/Vset.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/bool.Bool.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/int.Abs.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/int.ComputerDivision.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/int.Int.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/int.MinMax.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/map.Map.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/real.Abs.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/real.FromInt.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/real.MinMax.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/real.Real.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/real.RealInfix.mlw
+%%PLUGINS%%%%DATADIR%%/wp/ergo/real.Square.mlw
+%%PLUGINS%%%%DATADIR%%/wp/why3/Bits.v
+%%PLUGINS%%%%DATADIR%%/wp/why3/Cbits.v
+%%PLUGINS%%%%DATADIR%%/wp/why3/Cbits.why
+%%PLUGINS%%%%DATADIR%%/wp/why3/Cfloat.v
+%%PLUGINS%%%%DATADIR%%/wp/why3/Cfloat.why
+%%PLUGINS%%%%DATADIR%%/wp/why3/Cint.v
+%%PLUGINS%%%%DATADIR%%/wp/why3/Cint.why
+%%PLUGINS%%%%DATADIR%%/wp/why3/Cmath.v
+%%PLUGINS%%%%DATADIR%%/wp/why3/Cmath.why
+%%PLUGINS%%%%DATADIR%%/wp/why3/Memory.v
+%%PLUGINS%%%%DATADIR%%/wp/why3/Memory.why
+%%PLUGINS%%%%DATADIR%%/wp/why3/Qed.v
+%%PLUGINS%%%%DATADIR%%/wp/why3/Qed.why
+%%PLUGINS%%%%DATADIR%%/wp/why3/Qedlib.v
+%%PLUGINS%%%%DATADIR%%/wp/why3/Vset.v
+%%PLUGINS%%%%DATADIR%%/wp/why3/Vset.why
+%%PLUGINS%%%%DATADIR%%/wp/why3/Zbits.v
+%%PLUGINS%%%%DATADIR%%/wp/why3/coq.drv
+%%PLUGINS%%%%DATADIR%%/wp/why3/why3.conf
+%%PLUGINS%%%%DATADIR%%/wp/wp.driver
+@dirrmtry lib/frama-c/plugins/gui
+@dirrmtry lib/frama-c/plugins
+@dirrmtry lib/frama-c
 @dirrm %%DATADIR%%/doc/code
 @dirrm %%DATADIR%%/doc
+@dirrm %%DATADIR%%/feedback
+@dirrm %%DATADIR%%/libc/arpa
+@dirrm %%DATADIR%%/libc/linux
+@dirrm %%DATADIR%%/libc/net
+@dirrm %%DATADIR%%/libc/netinet
+@dirrm %%DATADIR%%/libc/sys
+@dirrm %%DATADIR%%/libc
+%%PLUGINS%%@dirrm %%DATADIR%%/wp/coqwp/bool
+%%PLUGINS%%@dirrm %%DATADIR%%/wp/coqwp/int
+%%PLUGINS%%@dirrm %%DATADIR%%/wp/coqwp/map
+%%PLUGINS%%@dirrm %%DATADIR%%/wp/coqwp/real
+%%PLUGINS%%@dirrm %%DATADIR%%/wp/coqwp
+%%PLUGINS%%@dirrm %%DATADIR%%/wp/ergo
+%%PLUGINS%%@dirrm %%DATADIR%%/wp/why3
+%%PLUGINS%%@dirrm %%DATADIR%%/wp
 @dirrm %%DATADIR%%