3 files changed, 219 insertions, 144 deletions

diff --git a/devel/frama-c/Makefile b/devel/frama-c/Makefile
index bcd0a20d609f..6bdb9c5528ac 100644
--- a/devel/frama-c/Makefile
+++ b/devel/frama-c/Makefile
@@ -6,8 +6,8 @@
 #
 
 PORTNAME=		frama-c
-DISTVERSIONPREFIX=	Carbon-
-DISTVERSION=		20110201
+DISTVERSIONPREFIX=	Nitrogen-
+DISTVERSION=		20111001
 CATEGORIES=		devel
 MASTER_SITES=		http://frama-c.com/download/ LOCAL/bf
 
@@ -22,13 +22,35 @@ RUN_DEPENDS=	${LOCALBASE}/lib/ocaml/ocamlgraph/graph.a:${PORTSDIR}/math/ocaml-oc
 GNU_CONFIGURE=	yes
 MAKE_ENV+=	FRAMAC_LIBDIR="${PREFIX}/lib/frama-c"
 MAN1=		frama-c.1 frama-c-gui.1
-OPTIONS=	GUI	"Build GUI" on \
+OPTIONS=	ALTERGO "Build wp plugin components that use Alt-Ergo" on \
+		COQ	"Build wp plugin components that use Coq" off \
+		GUI	"Build GUI" on \
 		PLUGINS "Build bundled plugins" on
 USE_GMAKE=	yes
 USE_OCAML=	yes
 
 .include <bsd.port.options.mk>
 
+.if defined(WITH_ALTERGO)
+.if !defined(WITH_PLUGINS)
+IGNORE =	requires WITH_PLUGINS for WITH_ALTERGO
+.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 defined(WITH_COQ)
+.if !defined(WITH_PLUGINS)
+IGNORE =	requires WITH_PLUGINS for WITH_COQ
+.endif
+BUILD_DEPENDS +=	coqc:${PORTSDIR}/math/coq
+RUN_DEPENDS+=		coqc:${PORTSDIR}/math/coq
+.else
+CONFIGURE_ENV +=	HAS_COQ=no
+.endif
+
 .if defined(WITH_GUI)
 .if !defined(WITH_PLUGINS)
 IGNORE =	requires WITH_PLUGINS for WITH_GUI
@@ -44,9 +66,9 @@ PLIST_SUB+=		GUI="@comment "
 
 .if defined(WITH_PLUGINS)
 BUILD_DEPENDS +=	dot:${PORTSDIR}/graphics/graphviz \
-		ltl2ba:${PORTSDIR}/math/ltl2ba
-RUN_DEPENDS+=		dot:${PORTSDIR}/graphics/graphviz \
-		ltl2ba:${PORTSDIR}/math/ltl2ba
+			ltl2ba:${PORTSDIR}/math/ltl2ba
+RUN_DEPENDS+=	 	dot:${PORTSDIR}/graphics/graphviz \
+			ltl2ba:${PORTSDIR}/math/ltl2ba
 PLIST_SUB+=		PLUGINS=""
 .else
 CONFIGURE_ARGS+=	--with-no-plugin
@@ -54,11 +76,17 @@ PLIST_SUB+=		PLUGINS="@comment "
 .endif
 
 post-patch:
-	@${MKDIR} ${WRKSRC}/tests/occurrence
+	@${MKDIR} ${WRKSRC}/tests/report \
+		${WRKSRC}/tests/wp \
+		${WRKSRC}/tests/wp_plugin \
+		${WRKSRC}/tests/wp_acsl \
+		${WRKSRC}/tests/wp_store \
+		${WRKSRC}/tests/wp_hoare \
+		${WRKSRC}/tests/wp_runtime \
+		${WRKSRC}/tests/wp_bts \
+		${WRKSRC}/tests/wp_engine
 	@${REINPLACE_CMD} -e 's|@make |@${GMAKE} |' \
 			${WRKSRC}/src/aorai/Makefile.in
-	@${GREP} -le 'make ' -r ${WRKSRC}/tests | ${XARGS} ${REINPLACE_CMD} \
-		-e 's|make |${GMAKE} |'
 	@${REINPLACE_CMD} \
 		-e 's|$$(CP)|${INSTALL_DATA}|' \
 		-e 's|add_prefix|addprefix|' \
@@ -76,8 +104,10 @@ post-patch:
 		\|$$(CP).*share|s|$$(CP)\( -R\)*|${INSTALL_DATA}|; \
 		s|$$(CP)|${INSTALL_DATA}|; }' \
 			${WRKSRC}/Makefile
-	@${REINPLACE_CMD} -e '\|case $$OCAMLGRAPH_VERSION in| \
-		{N; s|1\.7|1.[78]*|;}' \
+	@${REINPLACE_CMD} -e 's|HAS_ALTERGO=$$||' \
+		-e '\|case $$ALTERGO_VERSION in|{N; s|0\.92\.2|0.94*|;}' \
+		-e 's|HAS_COQ=$$||' \
+		-e '\|case $$OCAMLGRAPH_VERSION in|{N; s|1\.8|&*|;}' \
 			${WRKSRC}/configure
 
 .if defined(WITH_GUI)
@@ -96,8 +126,8 @@ pre-configure:
 .endif
 
 post-install:
-		@${TOUCH} ${PREFIX}/lib/frama-c/plugins/.keep_me \
-		${PREFIX}/lib/frama-c/plugins/gui/.keep_me
+	@${TOUCH} ${PREFIX}/lib/frama-c/plugins/.keep_me \
+	${PREFIX}/lib/frama-c/plugins/gui/.keep_me
 
 .if defined(MAINTAINER_MODE)
 check regression-test test: build
diff --git a/devel/frama-c/distinfo b/devel/frama-c/distinfo
index 22dea72971a1..f9be2b875866 100644
--- a/devel/frama-c/distinfo
+++ b/devel/frama-c/distinfo
@@ -1,2 +1,2 @@
-SHA256 (frama-c-Carbon-20110201.tar.gz) = 0c212443224fb8a3b0d6b0337db7d7666a9f53628f9b0c5f411e563dcb4b2256
-SIZE (frama-c-Carbon-20110201.tar.gz) = 34484913
+SHA256 (frama-c-Nitrogen-20111001.tar.gz) = 8afad848321c958fab265045cd152482e77ce7c175ee7c9af2d4bec57a1bc671
+SIZE (frama-c-Nitrogen-20111001.tar.gz) = 12110786
diff --git a/devel/frama-c/pkg-plist b/devel/frama-c/pkg-plist
index 6e5e02a31e97..541813d6d3f1 100644
--- a/devel/frama-c/pkg-plist
+++ b/devel/frama-c/pkg-plist
@@ -1,8 +1,91 @@
-bin/frama-c
-bin/frama-c.byte
 %%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.cmi
+%%GUI%%lib/frama-c/plugins/gui/Wp.cmo
+%%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
 %%PLUGINS%%lib/frama-c/Constant_Propagation.cmo
 %%PLUGINS%%lib/frama-c/Constant_Propagation.cmx
 %%PLUGINS%%lib/frama-c/Constant_Propagation.o
@@ -27,9 +110,6 @@ bin/ptests.byte
 %%PLUGINS%%lib/frama-c/Postdominators.cmo
 %%PLUGINS%%lib/frama-c/Postdominators.cmx
 %%PLUGINS%%lib/frama-c/Postdominators.o
-%%PLUGINS%%lib/frama-c/Report.cmo
-%%PLUGINS%%lib/frama-c/Report.cmx
-%%PLUGINS%%lib/frama-c/Report.o
 %%PLUGINS%%lib/frama-c/RteGen.cmo
 %%PLUGINS%%lib/frama-c/RteGen.cmx
 %%PLUGINS%%lib/frama-c/RteGen.o
@@ -54,6 +134,18 @@ 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/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.cmi
+%%PLUGINS%%lib/frama-c/plugins/Wp.cmo
+%%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
@@ -70,10 +162,6 @@ 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
@@ -224,10 +312,10 @@ lib/frama-c/cprint.cmi
 lib/frama-c/cprint.cmo
 lib/frama-c/cprint.cmx
 lib/frama-c/cprint.o
-lib/frama-c/cvalue_type.cmi
-lib/frama-c/cvalue_type.cmo
-lib/frama-c/cvalue_type.cmx
-lib/frama-c/cvalue_type.o
+lib/frama-c/cvalue.cmi
+lib/frama-c/cvalue.cmo
+lib/frama-c/cvalue.cmx
+lib/frama-c/cvalue.o
 lib/frama-c/dashtbl.cmi
 lib/frama-c/dashtbl.cmo
 lib/frama-c/dashtbl.cmx
@@ -244,23 +332,18 @@ lib/frama-c/db.cmi
 lib/frama-c/db.cmo
 lib/frama-c/db.cmx
 lib/frama-c/db.o
-lib/frama-c/db_types.cmi
 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
 lib/frama-c/descr.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/description.cmi
+lib/frama-c/description.cmo
+lib/frama-c/description.cmx
+lib/frama-c/description.o
 lib/frama-c/dominators.cmi
 lib/frama-c/dominators.cmo
 lib/frama-c/dominators.cmx
@@ -273,6 +356,10 @@ lib/frama-c/dynlink_common_interface.cmi
 lib/frama-c/dynlink_common_interface.cmo
 lib/frama-c/dynlink_common_interface.cmx
 lib/frama-c/dynlink_common_interface.o
+lib/frama-c/emitter.cmi
+lib/frama-c/emitter.cmo
+lib/frama-c/emitter.cmx
+lib/frama-c/emitter.o
 lib/frama-c/errorloc.cmi
 lib/frama-c/errorloc.cmo
 lib/frama-c/errorloc.cmx
@@ -293,14 +380,6 @@ 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
-%%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
@@ -321,23 +400,6 @@ lib/frama-c/growArray.cmi
 lib/frama-c/growArray.cmo
 lib/frama-c/growArray.cmx
 lib/frama-c/growArray.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
 lib/frama-c/hook.cmi
 lib/frama-c/hook.cmo
 lib/frama-c/hook.cmx
@@ -386,19 +448,15 @@ lib/frama-c/kernel.cmi
 lib/frama-c/kernel.cmo
 lib/frama-c/kernel.cmx
 lib/frama-c/kernel.o
-lib/frama-c/kernel_datatype.cmi
-lib/frama-c/kernel_datatype.cmo
-lib/frama-c/kernel_datatype.cmx
-lib/frama-c/kernel_datatype.o
 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_With_Isotropy.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
@@ -415,10 +473,6 @@ 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_whole.cmi
-lib/frama-c/lmap_whole.cmo
-lib/frama-c/lmap_whole.cmx
-lib/frama-c/lmap_whole.o
 lib/frama-c/locations.cmi
 lib/frama-c/locations.cmo
 lib/frama-c/locations.cmx
@@ -480,10 +534,6 @@ 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_ppc_32_diab.cmi
-lib/frama-c/machdep_ppc_32_diab.cmo
-lib/frama-c/machdep_ppc_32_diab.cmx
-lib/frama-c/machdep_ppc_32_diab.o
 lib/frama-c/machdep_x86_16.cmi
 lib/frama-c/machdep_x86_16.cmo
 lib/frama-c/machdep_x86_16.cmx
@@ -500,10 +550,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
-%%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/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
 lib/frama-c/mergecil.cmi
 lib/frama-c/mergecil.cmo
 lib/frama-c/mergecil.cmx
@@ -541,14 +591,10 @@ lib/frama-c/origin.cmi
 lib/frama-c/origin.cmo
 lib/frama-c/origin.cmx
 lib/frama-c/origin.o
-lib/frama-c/parameters.cmi
-lib/frama-c/parameters.cmo
-lib/frama-c/parameters.cmx
-lib/frama-c/parameters.o
-lib/frama-c/patch.cmi
-lib/frama-c/patch.cmo
-lib/frama-c/patch.cmx
-lib/frama-c/patch.o
+lib/frama-c/parameter.cmi
+lib/frama-c/parameter.cmo
+lib/frama-c/parameter.cmx
+lib/frama-c/parameter.o
 lib/frama-c/path_lattice.cmi
 lib/frama-c/path_lattice.cmo
 lib/frama-c/path_lattice.cmx
@@ -570,20 +616,7 @@ 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/Security_slicing.cmi
-%%PLUGINS%%lib/frama-c/plugins/Security_slicing.cmo
-%%PLUGINS%%lib/frama-c/plugins/Security_slicing.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/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
@@ -600,26 +633,18 @@ 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
 lib/frama-c/project_skeleton.o
-lib/frama-c/properties_status.cmi
-lib/frama-c/properties_status.cmo
-lib/frama-c/properties_status.cmx
-lib/frama-c/properties_status.o
 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/qstack.cmi
 lib/frama-c/qstack.cmo
@@ -633,10 +658,6 @@ lib/frama-c/reachingdefs.cmi
 lib/frama-c/reachingdefs.cmo
 lib/frama-c/reachingdefs.cmx
 lib/frama-c/reachingdefs.o
-lib/frama-c/relations_type.cmi
-lib/frama-c/relations_type.cmo
-lib/frama-c/relations_type.cmx
-lib/frama-c/relations_type.o
 lib/frama-c/rmciltmps.cmi
 lib/frama-c/rmciltmps.cmo
 lib/frama-c/rmciltmps.cmx
@@ -665,14 +686,6 @@ 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,6 +734,10 @@ lib/frama-c/task.cmi
 lib/frama-c/task.cmo
 lib/frama-c/task.cmx
 lib/frama-c/task.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/translate_lightweight.cmi
 lib/frama-c/translate_lightweight.cmo
 lib/frama-c/translate_lightweight.cmx
@@ -757,10 +774,6 @@ 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/whitetrack.cmi
 lib/frama-c/whitetrack.cmo
 lib/frama-c/whitetrack.cmx
@@ -773,10 +786,6 @@ lib/frama-c/widen_type.cmi
 lib/frama-c/widen_type.cmo
 lib/frama-c/widen_type.cmx
 lib/frama-c/widen_type.o
-lib/frama-c/zrapp.cmi
-lib/frama-c/zrapp.cmo
-lib/frama-c/zrapp.cmx
-lib/frama-c/zrapp.o
 share/emacs/site-lisp/acsl.el
 %%DATADIR%%/Makefile.common
 %%DATADIR%%/Makefile.config
@@ -785,17 +794,32 @@ share/emacs/site-lisp/acsl.el
 %%DATADIR%%/Makefile.kernel
 %%DATADIR%%/Makefile.plugin
 %%DATADIR%%/acsl.el
-%%GUI%%%%DATADIR%%/attach.png
 %%DATADIR%%/builtin.c
 %%DATADIR%%/builtin.h
-%%GUI%%%%DATADIR%%/check.png
+%%DATADIR%%/check.png
 %%DATADIR%%/configure.ac
-%%GUI%%%%DATADIR%%/failed.png
+%%DATADIR%%/doc/code/intro_kernel_plugin.txt
+%%DATADIR%%/doc/code/intro_plugin.txt
+%%DATADIR%%/doc/code/style.css
+%%DATADIR%%/doc/code/toc_head.htm
+%%DATADIR%%/doc/code/toc_tail.htm
+%%DATADIR%%/failed.png
+%%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/unknown.png
+%%DATADIR%%/feedback/unknown_but_dead.png
+%%DATADIR%%/feedback/valid_but_dead.png
+%%DATADIR%%/feedback/valid_under_hyp.png
 %%DATADIR%%/fluctuat.h
-%%GUI%%%%DATADIR%%/frama-c.gif
-%%GUI%%%%DATADIR%%/frama-c.ico
+%%DATADIR%%/frama-c.gif
+%%DATADIR%%/frama-c.ico
 %%DATADIR%%/frama-c.rc
-%%GUI%%%%DATADIR%%/left.png
+%%DATADIR%%/left.png
 %%DATADIR%%/libc.c
 %%DATADIR%%/libc.h
 %%DATADIR%%/libc/__fc_builtin.c
@@ -804,16 +828,20 @@ share/emacs/site-lisp/acsl.el
 %%DATADIR%%/libc/__fc_define_blksize_t.h
 %%DATADIR%%/libc/__fc_define_dev_t.h
 %%DATADIR%%/libc/__fc_define_ino_t.h
+%%DATADIR%%/libc/__fc_define_intptr_t.h
 %%DATADIR%%/libc/__fc_define_iovec.h
 %%DATADIR%%/libc/__fc_define_mode_t.h
 %%DATADIR%%/libc/__fc_define_nlink_t.h
 %%DATADIR%%/libc/__fc_define_null.h
 %%DATADIR%%/libc/__fc_define_off_t.h
+%%DATADIR%%/libc/__fc_define_pid_t.h
 %%DATADIR%%/libc/__fc_define_restrict.h
 %%DATADIR%%/libc/__fc_define_size_t.h
+%%DATADIR%%/libc/__fc_define_ssize_t.h
 %%DATADIR%%/libc/__fc_define_suseconds_t.h
 %%DATADIR%%/libc/__fc_define_time_t.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_machdep.h
 %%DATADIR%%/libc/__fc_string_axiomatic.h
@@ -828,6 +856,7 @@ share/emacs/site-lisp/acsl.el
 %%DATADIR%%/libc/errno.h
 %%DATADIR%%/libc/fc_posix_runtime.c
 %%DATADIR%%/libc/fc_runtime.c
+%%DATADIR%%/libc/fcntl.h
 %%DATADIR%%/libc/fenv.c
 %%DATADIR%%/libc/fenv.h
 %%DATADIR%%/libc/float.c
@@ -868,6 +897,7 @@ share/emacs/site-lisp/acsl.el
 %%DATADIR%%/libc/sys/uio.h
 %%DATADIR%%/libc/sys/wait.h
 %%DATADIR%%/libc/syslog.h
+%%DATADIR%%/libc/termios.h
 %%DATADIR%%/libc/test.c
 %%DATADIR%%/libc/tgmath.c
 %%DATADIR%%/libc/tgmath.h
@@ -886,6 +916,7 @@ share/emacs/site-lisp/acsl.el
 %%DATADIR%%/manuals/acsl.pdf
 %%DATADIR%%/manuals/aorai-manual.pdf
 %%DATADIR%%/manuals/jessie-tutorial.pdf
+%%DATADIR%%/manuals/metrics-manual.pdf
 %%DATADIR%%/manuals/plugin-development-guide.pdf
 %%DATADIR%%/manuals/rte-manual.pdf
 %%DATADIR%%/manuals/user-manual.pdf
@@ -893,14 +924,28 @@ share/emacs/site-lisp/acsl.el
 %%DATADIR%%/manuals/wp-manual.pdf
 %%DATADIR%%/math.c
 %%DATADIR%%/math.h
-%%GUI%%%%DATADIR%%/maybe.png
-%%GUI%%%%DATADIR%%/relies_on_hyp.png
-%%GUI%%%%DATADIR%%/right.png
+%%DATADIR%%/maybe.png
+%%DATADIR%%/right.png
+%%DATADIR%%/unmark.png
+%%PLUGINS%%%%DATADIR%%/wp/hoare_ergo.why
+%%PLUGINS%%%%DATADIR%%/wp/hoare_model.v
+%%PLUGINS%%%%DATADIR%%/wp/hoare_model.why
+%%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/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
+@dirrm %%DATADIR%%/feedback
+@dirrm %%DATADIR%%/doc/code
+@dirrm %%DATADIR%%/doc
 @dirrm %%DATADIR%%