4 files changed, 306 insertions, 605 deletions

diff --git a/devel/frama-c/Makefile b/devel/frama-c/Makefile
index 9573a3a628ad..850b6a19a39b 100644
--- a/devel/frama-c/Makefile
+++ b/devel/frama-c/Makefile
@@ -1,80 +1,31 @@
 # Created by: b.f. <bf@FreeBSD.org>
 # $FreeBSD$
 
-PORTNAME=		frama-c
-DISTVERSIONPREFIX=	Neon-
-DISTVERSION=		20140301
-PORTREVISION=	2
-CATEGORIES=		devel
-MASTER_SITES=		http://frama-c.com/download/ LOCAL/bf
+PORTNAME=	frama-c
+DISTVERSIONPREFIX=	Sodium-
+DISTVERSION=	20150201
+CATEGORIES=	devel
+MASTER_SITES=	http://frama-c.com/download/
 
-MAINTAINER=	bf@FreeBSD.org
+MAINTAINER=	ports@FreeBSD.org
 COMMENT=	Extensible platform for source-code analysis of C
 
 LICENSE=	LGPL21
 
-BROKEN=		Fails to build with ocamlgraph 1.8.6
-
+EXTRACT_DEPENDS=	gtar:${PORTSDIR}/archivers/gtar
 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
+EXTRACT_CMD=	gtar
+EXTRACT_BEFORE_ARGS=	-xf
 CONFIGURE_ARGS+=--with-cpp="${FRAMAC_DEFAULT_CPP}"
 MAKE_ENV+=	FRAMAC_LIBDIR="${PREFIX}/lib/frama-c"
 
-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)
-
-.include <bsd.port.options.mk>
-
 FRAMAC_DEFAULT_CPP?=	${CPP} -C -I${DATADIR}/libc -I.
 
-.if ${PORT_OPTIONS:MALTERGO}
-.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
-RUN_DEPENDS+=		alt-ergo:${PORTSDIR}/math/alt-ergo
-.else
-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
-RUN_DEPENDS+=		coqc:${PORTSDIR}/math/coq
-.else
-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
-RUN_DEPENDS+=		lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2
-CONFIGURE_ARGS+=	--enable-gui
-.else
-CONFIGURE_ARGS+=	--disable-gui
-.endif
-
-.if ${PORT_OPTIONS:MPLUGINS}
-BUILD_DEPENDS+=		dot:${PORTSDIR}/graphics/graphviz \
-			ltl2ba:${PORTSDIR}/math/ltl2ba
-RUN_DEPENDS+=	 	dot:${PORTSDIR}/graphics/graphviz \
-			ltl2ba:${PORTSDIR}/math/ltl2ba
-.else
-CONFIGURE_ARGS+=	--with-no-plugin
-.endif
-
 post-patch:
 	@cd ${WRKSRC}/tests; ${MKDIR} aorai report wp wp_acsl wp_bts \
 	wp_engine wp_hoare wp_plugin wp_runtime wp_store wp_typed
@@ -95,31 +46,6 @@ post-patch:
 		\|$$(CP).*man/|s|$$(CP)|${INSTALL_MAN}|; \
 		s|$$(CP)|${INSTALL_DATA}|; }' \
 			${WRKSRC}/Makefile
-	@${REINPLACE_CMD} -e 's|HAS_ALTERGO=$$||' \
-		-e '\|case $$ALTERGO_VERSION in|{N; s|0\.92\.2|0.94*|;}' \
-		-e 's|HAS_COQ=$$||' \
-			${WRKSRC}/configure
-	@${REINPLACE_CMD} -Ee 's@(\+|/)(lablgtk2)@\1site-lib/\2@' \
-		${WRKSRC}/src/kernel/dynamic.ml
-
-.if ${PORT_OPTIONS:MGUI}
-pre-configure:
-	@(if [ ! -e ${LOCALBASE}/${OCAML_SITELIBDIR}/lablgtk2/gtkSourceView2.cmi -o \
-	! -e ${LOCALBASE}/${OCAML_SITELIBDIR}/lablgtk2/gnomeCanvas.cmi ] ; then \
-	${ECHO_MSG} "==> The WITH_GUI option for ${PKGNAME} requires" ; \
-	${ECHO_MSG} "==> x11-toolkits/ocaml-lablgtk2 to be built" ; \
-	${ECHO_MSG} "==> WITH_GNOMECANVAS and WITH_GTKSOURCEVIEW2" ; \
-	exit 1; fi)
-	@(if [ ! -e ${LOCALBASE}/lib/ocaml/ocamlgraph/dgraph.cmi ] ; then \
-	${ECHO_MSG} "==> The WITH_GUI option for ${PKGNAME} requires" ; \
-	${ECHO_MSG} "==> math/ocaml-ocamlgraph to be built WITH_GUI" ; \
-	exit 1; fi)
-
-.endif
-
-post-install:
-	@${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 49700687e546..7d80e312085a 100644
--- a/devel/frama-c/distinfo
+++ b/devel/frama-c/distinfo
@@ -1,2 +1,2 @@
-SHA256 (frama-c-Neon-20140301.tar.gz) = c5a0606f5c2d56280fd90f979c07ff398acb1e6a661323438b8d0cbd8f9f4731
-SIZE (frama-c-Neon-20140301.tar.gz) = 3122492
+SHA256 (frama-c-Sodium-20150201.tar.gz) = b61638809e5e2f4138052844dd58aa2d2c44d542a65111cc80b65f6b999a4c71
+SIZE (frama-c-Sodium-20150201.tar.gz) = 5993348
diff --git a/devel/frama-c/files/patch-Support_OCamlgraph185 b/devel/frama-c/files/patch-Support_OCamlgraph185
deleted file mode 100644
index 889c411e1a1d..000000000000
--- a/devel/frama-c/files/patch-Support_OCamlgraph185
+++ /dev/null
@@ -1,219 +0,0 @@
-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-plist b/devel/frama-c/pkg-plist
index 28153a9dc500..fdd56cb5957d 100644
--- a/devel/frama-c/pkg-plist
+++ b/devel/frama-c/pkg-plist
@@ -1,11 +1,13 @@
 bin/frama-c
-%%GUI%%bin/frama-c-gui
-%%GUI%%bin/frama-c-gui.byte
+bin/frama-c-config
+bin/frama-c-gui
+bin/frama-c-gui.byte
 bin/frama-c.byte
 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/Constant_Propagation.cmi
+lib/frama-c/Constant_Propagation.cmo
+lib/frama-c/Constant_Propagation.cmx
+lib/frama-c/Constant_Propagation.o
 lib/frama-c/FCHashtbl.cmi
 lib/frama-c/FCHashtbl.cmo
 lib/frama-c/FCHashtbl.cmx
@@ -18,51 +20,66 @@ 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
-%%PLUGINS%%lib/frama-c/Impact.cmo
-%%PLUGINS%%lib/frama-c/Impact.cmx
-%%PLUGINS%%lib/frama-c/Impact.o
-%%PLUGINS%%lib/frama-c/Inout.cmo
-%%PLUGINS%%lib/frama-c/Inout.cmx
-%%PLUGINS%%lib/frama-c/Inout.o
-%%PLUGINS%%lib/frama-c/Metrics.cmo
-%%PLUGINS%%lib/frama-c/Metrics.cmx
-%%PLUGINS%%lib/frama-c/Metrics.o
-%%PLUGINS%%lib/frama-c/Occurrence.cmo
-%%PLUGINS%%lib/frama-c/Occurrence.cmx
-%%PLUGINS%%lib/frama-c/Occurrence.o
-%%PLUGINS%%lib/frama-c/Pdg.cmo
-%%PLUGINS%%lib/frama-c/Pdg.cmx
-%%PLUGINS%%lib/frama-c/Pdg.o
-%%PLUGINS%%lib/frama-c/Postdominators.cmo
-%%PLUGINS%%lib/frama-c/Postdominators.cmx
-%%PLUGINS%%lib/frama-c/Postdominators.o
-%%PLUGINS%%lib/frama-c/RteGen.cmo
-%%PLUGINS%%lib/frama-c/RteGen.cmx
-%%PLUGINS%%lib/frama-c/RteGen.o
-%%PLUGINS%%lib/frama-c/Scope.cmo
-%%PLUGINS%%lib/frama-c/Scope.cmx
-%%PLUGINS%%lib/frama-c/Scope.o
-%%PLUGINS%%lib/frama-c/Semantic_callgraph.cmo
-%%PLUGINS%%lib/frama-c/Semantic_callgraph.cmx
-%%PLUGINS%%lib/frama-c/Semantic_callgraph.o
-%%PLUGINS%%lib/frama-c/Slicing.cmo
-%%PLUGINS%%lib/frama-c/Slicing.cmx
-%%PLUGINS%%lib/frama-c/Slicing.o
-%%PLUGINS%%lib/frama-c/Sparecode.cmo
-%%PLUGINS%%lib/frama-c/Sparecode.cmx
-%%PLUGINS%%lib/frama-c/Sparecode.o
-%%PLUGINS%%lib/frama-c/Syntactic_callgraph.cmo
-%%PLUGINS%%lib/frama-c/Syntactic_callgraph.cmx
-%%PLUGINS%%lib/frama-c/Syntactic_callgraph.o
-%%PLUGINS%%lib/frama-c/Users.cmo
-%%PLUGINS%%lib/frama-c/Users.cmx
-%%PLUGINS%%lib/frama-c/Users.o
-%%PLUGINS%%lib/frama-c/Value.cmo
-%%PLUGINS%%lib/frama-c/Value.cmx
-%%PLUGINS%%lib/frama-c/Value.o
+lib/frama-c/From.cmi
+lib/frama-c/From.cmo
+lib/frama-c/From.cmx
+lib/frama-c/From.o
+lib/frama-c/Impact.cmi
+lib/frama-c/Impact.cmo
+lib/frama-c/Impact.cmx
+lib/frama-c/Impact.o
+lib/frama-c/Inout.cmi
+lib/frama-c/Inout.cmo
+lib/frama-c/Inout.cmx
+lib/frama-c/Inout.o
+lib/frama-c/Metrics.cmi
+lib/frama-c/Metrics.cmo
+lib/frama-c/Metrics.cmx
+lib/frama-c/Metrics.o
+lib/frama-c/Occurrence.cmi
+lib/frama-c/Occurrence.cmo
+lib/frama-c/Occurrence.cmx
+lib/frama-c/Occurrence.o
+lib/frama-c/Pdg.cmi
+lib/frama-c/Pdg.cmo
+lib/frama-c/Pdg.cmx
+lib/frama-c/Pdg.o
+lib/frama-c/Postdominators.cmi
+lib/frama-c/Postdominators.cmo
+lib/frama-c/Postdominators.cmx
+lib/frama-c/Postdominators.o
+lib/frama-c/RteGen.cmi
+lib/frama-c/RteGen.cmo
+lib/frama-c/RteGen.cmx
+lib/frama-c/RteGen.o
+lib/frama-c/Scope.cmi
+lib/frama-c/Scope.cmo
+lib/frama-c/Scope.cmx
+lib/frama-c/Scope.o
+lib/frama-c/Semantic_callgraph.cmi
+lib/frama-c/Semantic_callgraph.cmo
+lib/frama-c/Semantic_callgraph.cmx
+lib/frama-c/Semantic_callgraph.o
+lib/frama-c/Slicing.cmi
+lib/frama-c/Slicing.cmo
+lib/frama-c/Slicing.cmx
+lib/frama-c/Slicing.o
+lib/frama-c/Sparecode.cmi
+lib/frama-c/Sparecode.cmo
+lib/frama-c/Sparecode.cmx
+lib/frama-c/Sparecode.o
+lib/frama-c/Syntactic_callgraph.cmi
+lib/frama-c/Syntactic_callgraph.cmo
+lib/frama-c/Syntactic_callgraph.cmx
+lib/frama-c/Syntactic_callgraph.o
+lib/frama-c/Users.cmi
+lib/frama-c/Users.cmo
+lib/frama-c/Users.cmx
+lib/frama-c/Users.o
+lib/frama-c/Value.cmi
+lib/frama-c/Value.cmo
+lib/frama-c/Value.cmx
+lib/frama-c/Value.o
 lib/frama-c/abstract_interp.cmi
 lib/frama-c/abstract_interp.cmo
 lib/frama-c/abstract_interp.cmx
@@ -79,10 +96,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/analyses_manager.cmi
+lib/frama-c/analyses_manager.cmo
+lib/frama-c/analyses_manager.cmx
+lib/frama-c/analyses_manager.o
 lib/frama-c/annotations.cmi
 lib/frama-c/annotations.cmo
 lib/frama-c/annotations.cmx
@@ -95,10 +112,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/availexpslv.cmi
-lib/frama-c/availexpslv.cmo
-lib/frama-c/availexpslv.cmx
-lib/frama-c/availexpslv.o
 lib/frama-c/bag.cmi
 lib/frama-c/bag.cmo
 lib/frama-c/bag.cmx
@@ -119,18 +132,14 @@ 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/book_manager.cmi
+lib/frama-c/book_manager.cmo
+lib/frama-c/book_manager.cmx
+lib/frama-c/book_manager.o
 lib/frama-c/boot.cmi
 lib/frama-c/boot.cmo
 lib/frama-c/boot.cmx
 lib/frama-c/boot.o
-lib/frama-c/buckx.cmi
-lib/frama-c/buckx.cmo
-lib/frama-c/buckx.cmx
-lib/frama-c/buckx.o
 lib/frama-c/buckx_c.o
 lib/frama-c/cabs.cmi
 lib/frama-c/cabs.cmo
@@ -144,14 +153,6 @@ 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
-lib/frama-c/cabsbranches.o
-lib/frama-c/cabscond.cmi
-lib/frama-c/cabscond.cmo
-lib/frama-c/cabscond.cmx
-lib/frama-c/cabscond.o
 lib/frama-c/cabshelper.cmi
 lib/frama-c/cabshelper.cmo
 lib/frama-c/cabshelper.cmx
@@ -209,6 +210,10 @@ lib/frama-c/clexer.cmi
 lib/frama-c/clexer.cmo
 lib/frama-c/clexer.cmx
 lib/frama-c/clexer.o
+lib/frama-c/clone.cmi
+lib/frama-c/clone.cmo
+lib/frama-c/clone.cmx
+lib/frama-c/clone.o
 lib/frama-c/cmdline.cmi
 lib/frama-c/cmdline.cmo
 lib/frama-c/cmdline.cmx
@@ -253,14 +258,10 @@ lib/frama-c/db.cmi
 lib/frama-c/db.cmo
 lib/frama-c/db.cmx
 lib/frama-c/db.o
-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/debug_manager.cmi
+lib/frama-c/debug_manager.cmo
+lib/frama-c/debug_manager.cmx
+lib/frama-c/debug_manager.o
 lib/frama-c/descr.cmi
 lib/frama-c/descr.cmo
 lib/frama-c/descr.cmx
@@ -269,10 +270,11 @@ 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/design.cmi
+lib/frama-c/design.cmo
+lib/frama-c/design.cmx
+lib/frama-c/design.o
+lib/frama-c/dgraph.cmi
 lib/frama-c/dominators.cmi
 lib/frama-c/dominators.cmo
 lib/frama-c/dominators.cmx
@@ -297,10 +299,10 @@ lib/frama-c/escape.cmi
 lib/frama-c/escape.cmo
 lib/frama-c/escape.cmx
 lib/frama-c/escape.o
-lib/frama-c/expcompare.cmi
-lib/frama-c/expcompare.cmo
-lib/frama-c/expcompare.cmx
-lib/frama-c/expcompare.o
+lib/frama-c/exn_flow.cmi
+lib/frama-c/exn_flow.cmo
+lib/frama-c/exn_flow.cmx
+lib/frama-c/exn_flow.o
 lib/frama-c/extlib.cmi
 lib/frama-c/extlib.cmo
 lib/frama-c/extlib.cmx
@@ -309,18 +311,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/file_manager.cmi
+lib/frama-c/file_manager.cmo
+lib/frama-c/file_manager.cmx
+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/filetree.cmi
+lib/frama-c/filetree.cmo
+lib/frama-c/filetree.cmx
+lib/frama-c/filetree.o
 lib/frama-c/filter.cmi
 lib/frama-c/filter.cmo
 lib/frama-c/filter.cmx
@@ -329,6 +331,11 @@ lib/frama-c/floating_point.cmi
 lib/frama-c/floating_point.cmo
 lib/frama-c/floating_point.cmx
 lib/frama-c/floating_point.o
+lib/frama-c/frama_c_config.cmi
+lib/frama-c/frama_c_init.cmi
+lib/frama-c/frama_c_init.cmo
+lib/frama-c/frama_c_init.cmx
+lib/frama-c/frama_c_init.o
 lib/frama-c/frontc.cmi
 lib/frama-c/frontc.cmo
 lib/frama-c/frontc.cmx
@@ -341,27 +348,31 @@ lib/frama-c/globals.cmi
 lib/frama-c/globals.cmo
 lib/frama-c/globals.cmx
 lib/frama-c/globals.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/graph.cmi
+lib/frama-c/graph.cmo
+lib/frama-c/graph.cmx
+lib/frama-c/graph.o
+lib/frama-c/gtk_form.cmi
+lib/frama-c/gtk_form.cmo
+lib/frama-c/gtk_form.cmx
+lib/frama-c/gtk_form.o
+lib/frama-c/gtk_helper.cmi
+lib/frama-c/gtk_helper.cmo
+lib/frama-c/gtk_helper.cmx
+lib/frama-c/gtk_helper.o
+lib/frama-c/gui_init.cmi
+lib/frama-c/gui_parameters.cmi
+lib/frama-c/gui_parameters.cmo
+lib/frama-c/gui_parameters.cmx
+lib/frama-c/gui_parameters.o
+lib/frama-c/help_manager.cmi
+lib/frama-c/help_manager.cmo
+lib/frama-c/help_manager.cmx
+lib/frama-c/help_manager.o
+lib/frama-c/history.cmi
+lib/frama-c/history.cmo
+lib/frama-c/history.cmx
+lib/frama-c/history.o
 lib/frama-c/hook.cmi
 lib/frama-c/hook.cmo
 lib/frama-c/hook.cmx
@@ -390,14 +401,11 @@ lib/frama-c/int_Base.cmi
 lib/frama-c/int_Base.cmo
 lib/frama-c/int_Base.cmx
 lib/frama-c/int_Base.o
-lib/frama-c/int_Interv.cmi
-lib/frama-c/int_Interv.cmo
-lib/frama-c/int_Interv.cmx
-lib/frama-c/int_Interv.o
-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/int_Intervals.cmi
+lib/frama-c/int_Intervals.cmo
+lib/frama-c/int_Intervals.cmx
+lib/frama-c/int_Intervals.o
+lib/frama-c/int_Intervals_sig.cmi
 lib/frama-c/integer.cmi
 lib/frama-c/integer.cmo
 lib/frama-c/integer.cmx
@@ -418,23 +426,15 @@ lib/frama-c/kernel_function.cmi
 lib/frama-c/kernel_function.cmo
 lib/frama-c/kernel_function.cmx
 lib/frama-c/kernel_function.o
-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_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/launcher.cmi
+lib/frama-c/launcher.cmo
+lib/frama-c/launcher.cmx
+lib/frama-c/launcher.o
 lib/frama-c/lexerhack.cmi
 lib/frama-c/lexerhack.cmo
 lib/frama-c/lexerhack.cmx
 lib/frama-c/lexerhack.o
-lib/frama-c/liveness.cmi
-lib/frama-c/liveness.cmo
-lib/frama-c/liveness.cmx
-lib/frama-c/liveness.o
 lib/frama-c/lmap.cmi
 lib/frama-c/lmap.cmo
 lib/frama-c/lmap.cmx
@@ -497,30 +497,18 @@ lib/frama-c/loop.cmi
 lib/frama-c/loop.cmo
 lib/frama-c/loop.cmx
 lib/frama-c/loop.o
-lib/frama-c/machdep_ppc_32.cmi
-lib/frama-c/machdep_ppc_32.cmo
-lib/frama-c/machdep_ppc_32.cmx
-lib/frama-c/machdep_ppc_32.o
-lib/frama-c/machdep_x86_16.cmi
-lib/frama-c/machdep_x86_16.cmo
-lib/frama-c/machdep_x86_16.cmx
-lib/frama-c/machdep_x86_16.o
-lib/frama-c/machdep_x86_32.cmi
-lib/frama-c/machdep_x86_32.cmo
-lib/frama-c/machdep_x86_32.cmx
-lib/frama-c/machdep_x86_32.o
-lib/frama-c/machdep_x86_64.cmi
-lib/frama-c/machdep_x86_64.cmo
-lib/frama-c/machdep_x86_64.cmx
-lib/frama-c/machdep_x86_64.o
+lib/frama-c/machdeps.cmi
+lib/frama-c/machdeps.cmo
+lib/frama-c/machdeps.cmx
+lib/frama-c/machdeps.o
 lib/frama-c/map_Lattice.cmi
 lib/frama-c/map_Lattice.cmo
 lib/frama-c/map_Lattice.cmx
 lib/frama-c/map_Lattice.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/menu_manager.cmi
+lib/frama-c/menu_manager.cmo
+lib/frama-c/menu_manager.cmx
+lib/frama-c/menu_manager.o
 lib/frama-c/mergecil.cmi
 lib/frama-c/mergecil.cmo
 lib/frama-c/mergecil.cmx
@@ -533,10 +521,7 @@ lib/frama-c/offsetmap.cmi
 lib/frama-c/offsetmap.cmo
 lib/frama-c/offsetmap.cmx
 lib/frama-c/offsetmap.o
-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_bitwise_sig.cmi
 lib/frama-c/offsetmap_lattice_with_isotropy.cmi
 lib/frama-c/offsetmap_sig.cmi
 lib/frama-c/oneret.cmi
@@ -555,6 +540,10 @@ 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_category.cmi
+lib/frama-c/parameter_category.cmo
+lib/frama-c/parameter_category.cmx
+lib/frama-c/parameter_category.o
 lib/frama-c/parameter_customize.cmi
 lib/frama-c/parameter_customize.cmo
 lib/frama-c/parameter_customize.cmx
@@ -580,33 +569,35 @@ lib/frama-c/plugin.cmi
 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/plugins/Aorai.cmi
+lib/frama-c/plugins/Aorai.cmo
+lib/frama-c/plugins/Aorai.cmxs
+lib/frama-c/plugins/Obfuscator.cmi
+lib/frama-c/plugins/Obfuscator.cmo
+lib/frama-c/plugins/Obfuscator.cmxs
+lib/frama-c/plugins/Report.cmi
+lib/frama-c/plugins/Report.cmo
+lib/frama-c/plugins/Report.cmxs
+lib/frama-c/plugins/Security_slicing.cmi
+lib/frama-c/plugins/Security_slicing.cmo
+lib/frama-c/plugins/Security_slicing.cmxs
+lib/frama-c/plugins/Wp.cma
+lib/frama-c/plugins/Wp.cmi
+lib/frama-c/plugins/Wp.cmxs
+lib/frama-c/plugins/gui/Security_slicing.cmi
+lib/frama-c/plugins/gui/Security_slicing.cmo
+lib/frama-c/plugins/gui/Security_slicing.cmxs
+lib/frama-c/plugins/gui/Wp.cma
+lib/frama-c/plugins/gui/Wp.cmi
+lib/frama-c/plugins/gui/Wp.cmxs
+lib/frama-c/precise_locs.cmi
+lib/frama-c/precise_locs.cmo
+lib/frama-c/precise_locs.cmx
+lib/frama-c/precise_locs.o
+lib/frama-c/pretty_source.cmi
+lib/frama-c/pretty_source.cmo
+lib/frama-c/pretty_source.cmx
+lib/frama-c/pretty_source.o
 lib/frama-c/pretty_utils.cmi
 lib/frama-c/pretty_utils.cmo
 lib/frama-c/pretty_utils.cmx
@@ -624,10 +615,10 @@ 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_manager.cmi
+lib/frama-c/project_manager.cmo
+lib/frama-c/project_manager.cmx
+lib/frama-c/project_manager.o
 lib/frama-c/project_skeleton.cmi
 lib/frama-c/project_skeleton.cmo
 lib/frama-c/project_skeleton.cmx
@@ -636,10 +627,10 @@ 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_navigator.cmi
+lib/frama-c/property_navigator.cmo
+lib/frama-c/property_navigator.cmx
+lib/frama-c/property_navigator.o
 lib/frama-c/property_status.cmi
 lib/frama-c/property_status.cmo
 lib/frama-c/property_status.cmx
@@ -655,14 +646,6 @@ lib/frama-c/rangemap.cmi
 lib/frama-c/rangemap.cmo
 lib/frama-c/rangemap.cmx
 lib/frama-c/rangemap.o
-lib/frama-c/reachingdefs.cmi
-lib/frama-c/reachingdefs.cmo
-lib/frama-c/reachingdefs.cmx
-lib/frama-c/reachingdefs.o
-lib/frama-c/rmciltmps.cmi
-lib/frama-c/rmciltmps.cmo
-lib/frama-c/rmciltmps.cmx
-lib/frama-c/rmciltmps.o
 lib/frama-c/rmtmps.cmi
 lib/frama-c/rmtmps.cmo
 lib/frama-c/rmtmps.cmx
@@ -679,14 +662,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/source_manager.cmi
+lib/frama-c/source_manager.cmo
+lib/frama-c/source_manager.cmx
+lib/frama-c/source_manager.o
+lib/frama-c/source_viewer.cmi
+lib/frama-c/source_viewer.cmo
+lib/frama-c/source_viewer.cmx
+lib/frama-c/source_viewer.o
 lib/frama-c/special_hooks.cmi
 lib/frama-c/special_hooks.cmo
 lib/frama-c/special_hooks.cmx
@@ -731,10 +714,10 @@ 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/toolbox.cmi
+lib/frama-c/toolbox.cmo
+lib/frama-c/toolbox.cmx
+lib/frama-c/toolbox.o
 lib/frama-c/tr_offset.cmi
 lib/frama-c/tr_offset.cmo
 lib/frama-c/tr_offset.cmx
@@ -771,10 +754,6 @@ lib/frama-c/unroll_loops.cmi
 lib/frama-c/unroll_loops.cmo
 lib/frama-c/unroll_loops.cmx
 lib/frama-c/unroll_loops.o
-lib/frama-c/usedef.cmi
-lib/frama-c/usedef.cmo
-lib/frama-c/usedef.cmx
-lib/frama-c/usedef.o
 lib/frama-c/utf8_logic.cmi
 lib/frama-c/utf8_logic.cmo
 lib/frama-c/utf8_logic.cmx
@@ -795,10 +774,10 @@ lib/frama-c/visitor.cmi
 lib/frama-c/visitor.cmo
 lib/frama-c/visitor.cmx
 lib/frama-c/visitor.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/warning_manager.cmi
+lib/frama-c/warning_manager.cmo
+lib/frama-c/warning_manager.cmx
+lib/frama-c/warning_manager.o
 lib/frama-c/widen_type.cmi
 lib/frama-c/widen_type.cmo
 lib/frama-c/widen_type.cmx
@@ -825,19 +804,6 @@ share/emacs/site-lisp/acsl.el
 %%DATADIR%%/doc/code/style.css
 %%DATADIR%%/doc/code/toc_head.htm
 %%DATADIR%%/doc/code/toc_tail.htm
-%%DATADIR%%/feedback/considered_valid.png
-%%DATADIR%%/feedback/inconsistent.png
-%%DATADIR%%/feedback/invalid_but_dead.png
-%%DATADIR%%/feedback/invalid_under_hyp.png
-%%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%%/frama-c.gif
 %%DATADIR%%/frama-c.ico
 %%DATADIR%%/frama-c.rc
@@ -850,6 +816,7 @@ share/emacs/site-lisp/acsl.el
 %%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_fpos_t.h
 %%DATADIR%%/libc/__fc_define_id_t.h
 %%DATADIR%%/libc/__fc_define_ino_t.h
 %%DATADIR%%/libc/__fc_define_intptr_t.h
@@ -950,66 +917,93 @@ share/emacs/site-lisp/acsl.el
 %%DATADIR%%/machine.h
 %%DATADIR%%/math.c
 %%DATADIR%%/math.h
+%%DATADIR%%/theme/colorblind/considered_valid.png
+%%DATADIR%%/theme/colorblind/inconsistent.png
+%%DATADIR%%/theme/colorblind/invalid_but_dead.png
+%%DATADIR%%/theme/colorblind/invalid_under_hyp.png
+%%DATADIR%%/theme/colorblind/never_tried.png
+%%DATADIR%%/theme/colorblind/surely_invalid.png
+%%DATADIR%%/theme/colorblind/surely_valid.png
+%%DATADIR%%/theme/colorblind/switch-off.png
+%%DATADIR%%/theme/colorblind/switch-on.png
+%%DATADIR%%/theme/colorblind/unknown.png
+%%DATADIR%%/theme/colorblind/unknown_but_dead.png
+%%DATADIR%%/theme/colorblind/valid_but_dead.png
+%%DATADIR%%/theme/colorblind/valid_under_hyp.png
+%%DATADIR%%/theme/default/considered_valid.png
+%%DATADIR%%/theme/default/inconsistent.png
+%%DATADIR%%/theme/default/invalid_but_dead.png
+%%DATADIR%%/theme/default/invalid_under_hyp.png
+%%DATADIR%%/theme/default/never_tried.png
+%%DATADIR%%/theme/default/surely_invalid.png
+%%DATADIR%%/theme/default/surely_valid.png
+%%DATADIR%%/theme/default/switch-off.png
+%%DATADIR%%/theme/default/switch-on.png
+%%DATADIR%%/theme/default/unknown.png
+%%DATADIR%%/theme/default/unknown_but_dead.png
+%%DATADIR%%/theme/default/valid_but_dead.png
+%%DATADIR%%/theme/default/valid_under_hyp.png
 %%DATADIR%%/unmark.png
-%%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
+%%DATADIR%%/wp/coqwp/Bits.v
+%%DATADIR%%/wp/coqwp/BuiltIn.v
+%%DATADIR%%/wp/coqwp/Cbits.v
+%%DATADIR%%/wp/coqwp/Cfloat.v
+%%DATADIR%%/wp/coqwp/Cint.v
+%%DATADIR%%/wp/coqwp/Cmath.v
+%%DATADIR%%/wp/coqwp/Memory.v
+%%DATADIR%%/wp/coqwp/Qed.v
+%%DATADIR%%/wp/coqwp/Qedlib.v
+%%DATADIR%%/wp/coqwp/Vset.v
+%%DATADIR%%/wp/coqwp/Zbits.v
+%%DATADIR%%/wp/coqwp/bool/Bool.v
+%%DATADIR%%/wp/coqwp/int/Abs.v
+%%DATADIR%%/wp/coqwp/int/ComputerDivision.v
+%%DATADIR%%/wp/coqwp/int/Int.v
+%%DATADIR%%/wp/coqwp/int/MinMax.v
+%%DATADIR%%/wp/coqwp/map/Map.v
+%%DATADIR%%/wp/coqwp/real/Abs.v
+%%DATADIR%%/wp/coqwp/real/FromInt.v
+%%DATADIR%%/wp/coqwp/real/MinMax.v
+%%DATADIR%%/wp/coqwp/real/Real.v
+%%DATADIR%%/wp/coqwp/real/RealInfix.v
+%%DATADIR%%/wp/coqwp/real/Square.v
+%%DATADIR%%/wp/ergo/Cbits.mlw
+%%DATADIR%%/wp/ergo/Cfloat.mlw
+%%DATADIR%%/wp/ergo/Cint.mlw
+%%DATADIR%%/wp/ergo/Cmath.mlw
+%%DATADIR%%/wp/ergo/Memory.mlw
+%%DATADIR%%/wp/ergo/Qed.mlw
+%%DATADIR%%/wp/ergo/Vset.mlw
+%%DATADIR%%/wp/ergo/bool.Bool.mlw
+%%DATADIR%%/wp/ergo/int.Abs.mlw
+%%DATADIR%%/wp/ergo/int.ComputerDivision.mlw
+%%DATADIR%%/wp/ergo/int.Int.mlw
+%%DATADIR%%/wp/ergo/int.MinMax.mlw
+%%DATADIR%%/wp/ergo/map.Map.mlw
+%%DATADIR%%/wp/ergo/real.Abs.mlw
+%%DATADIR%%/wp/ergo/real.FromInt.mlw
+%%DATADIR%%/wp/ergo/real.MinMax.mlw
+%%DATADIR%%/wp/ergo/real.Real.mlw
+%%DATADIR%%/wp/ergo/real.RealInfix.mlw
+%%DATADIR%%/wp/ergo/real.Square.mlw
+%%DATADIR%%/wp/why3/Bits.v
+%%DATADIR%%/wp/why3/Cbits.v
+%%DATADIR%%/wp/why3/Cbits.why
+%%DATADIR%%/wp/why3/Cfloat.v
+%%DATADIR%%/wp/why3/Cfloat.why
+%%DATADIR%%/wp/why3/Cint.v
+%%DATADIR%%/wp/why3/Cint.why
+%%DATADIR%%/wp/why3/Cmath.v
+%%DATADIR%%/wp/why3/Cmath.why
+%%DATADIR%%/wp/why3/Memory.v
+%%DATADIR%%/wp/why3/Memory.why
+%%DATADIR%%/wp/why3/Qed.v
+%%DATADIR%%/wp/why3/Qed.why
+%%DATADIR%%/wp/why3/Qedlib.v
+%%DATADIR%%/wp/why3/Vset.v
+%%DATADIR%%/wp/why3/Vset.why
+%%DATADIR%%/wp/why3/Zbits.v
+%%DATADIR%%/wp/why3/coq.drv
+%%DATADIR%%/wp/why3/why3.conf
+%%DATADIR%%/wp/wp.driver
+@dir lib/frama-c/plugins/gui