update to the Oxygen release

3 files changed, 132 insertions, 100 deletions

diff --git a/devel/frama-c/Makefile b/devel/frama-c/Makefile
index ee402e908a10..a72577ff9cf6 100644
--- a/devel/frama-c/Makefile
+++ b/devel/frama-c/Makefile
@@ -2,9 +2,8 @@
 # $FreeBSD$
 
 PORTNAME=		frama-c
-DISTVERSIONPREFIX=	Nitrogen-
-DISTVERSION=		20111001
-PORTREVISION=		3
+DISTVERSIONPREFIX=	Oxygen-
+DISTVERSION=		20120901
 CATEGORIES=		devel
 MASTER_SITES=		http://frama-c.com/download/ LOCAL/bf
 
@@ -13,21 +12,30 @@ COMMENT=	Extensible platform for source-code analysis of C
 
 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
+
 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
-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
+
+OPTIONS_DEFINE=		ALTERGO COQ GUI PLUGINS
+OPTIONS_DEFAULT=	ALTERGO GUI PLUGINS
+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
 
 .include <bsd.port.options.mk>
 
-.if defined(WITH_ALTERGO)
-.if !defined(WITH_PLUGINS)
-IGNORE =	requires WITH_PLUGINS for WITH_ALTERGO
+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
@@ -35,9 +43,9 @@ RUN_DEPENDS+=		alt-ergo:${PORTSDIR}/math/alt-ergo
 CONFIGURE_ENV +=	HAS_ALTERGO=no
 .endif
 
-.if defined(WITH_COQ)
-.if !defined(WITH_PLUGINS)
-IGNORE =	requires WITH_PLUGINS for WITH_COQ
+.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
@@ -45,9 +53,9 @@ RUN_DEPENDS+=		coqc:${PORTSDIR}/math/coq
 CONFIGURE_ENV +=	HAS_COQ=no
 .endif
 
-.if defined(WITH_GUI)
-.if !defined(WITH_PLUGINS)
-IGNORE =	requires WITH_PLUGINS for WITH_GUI
+.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
@@ -58,7 +66,7 @@ CONFIGURE_ARGS+=	--disable-gui
 PLIST_SUB+=		GUI="@comment "
 .endif
 
-.if defined(WITH_PLUGINS)
+.if ${PORT_OPTIONS:MPLUGINS}
 BUILD_DEPENDS +=	dot:${PORTSDIR}/graphics/graphviz \
 			ltl2ba:${PORTSDIR}/math/ltl2ba
 RUN_DEPENDS+=	 	dot:${PORTSDIR}/graphics/graphviz \
@@ -69,20 +77,9 @@ CONFIGURE_ARGS+=	--with-no-plugin
 PLIST_SUB+=		PLUGINS="@comment "
 .endif
 
-post-extract:
-	@cd ${WRKSRC}; ${EXTRACT_CMD} ${EXTRACT_BEFORE_ARGS} \
-		ocamlgraph.tar.gz ${EXTRACT_AFTER_ARGS}
-
 post-patch:
-	@${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
+	@cd ${WRKSRC}/tests; ${MKDIR} aorai report wp wp_acsl wp_bts \
+	wp_engine wp_hoare wp_plugin wp_runtime wp_store wp_typed
 	@${REINPLACE_CMD} -e 's|@make |@${GMAKE} |' \
 			${WRKSRC}/src/aorai/Makefile.in
 	@${REINPLACE_CMD} \
@@ -95,11 +92,7 @@ post-patch:
 			${WRKSRC}/share/Makefile.dynamic
 	@${REINPLACE_CMD} -e '\|^# Installation|,\|^# File headers|{ \
 		\|$$(CP).*bin|s|$$(CP)|${INSTALL_SCRIPT}|; \
-		\|$$(CP) -R doc/manuals $$(FRAMAC_DATADIR)| \
-		s||${MKDIR} $$(FRAMAC_DATADIR)/manuals ; \
-		${INSTALL_DATA} doc/manuals/* $$(FRAMAC_DATADIR)/manuals|; \
-		\|$$(CP).*man|s|$$(CP)\( -R\)*|${INSTALL_MAN}|; \
-		\|$$(CP).*share|s|$$(CP)\( -R\)*|${INSTALL_DATA}|; \
+		\|$$(CP).*man/|s|$$(CP)|${INSTALL_MAN}|; \
 		s|$$(CP)|${INSTALL_DATA}|; }' \
 			${WRKSRC}/Makefile
 	@${REINPLACE_CMD} -e 's|HAS_ALTERGO=$$||' \
@@ -107,14 +100,9 @@ post-patch:
 		-e 's|HAS_COQ=$$||' \
 			${WRKSRC}/configure
 	@${REINPLACE_CMD} -Ee 's@(\+|/)(lablgtk2)@\1site-lib/\2@' \
-		${WRKSRC}/Makefile \
-		${WRKSRC}/configure \
-		${WRKSRC}/ocamlgraph/configure \
-		${WRKSRC}/ocamlgraph/view_graph/Makefile \
-		${WRKSRC}/share/Makefile.plugin \
 		${WRKSRC}/src/kernel/dynamic.ml
 
-.if defined(WITH_GUI)
+.if ${PORT_OPTIONS:MGUI}
 pre-configure:
 	@(if [ ! -e ${LOCALBASE}/${OCAML_SITELIBDIR}/lablgtk2/gtkSourceView2.cmi -o \
 	! -e ${LOCALBASE}/${OCAML_SITELIBDIR}/lablgtk2/gnomeCanvas.cmi ] ; then \
@@ -133,14 +121,9 @@ post-install:
 	@${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
-	@(cd ${WRKSRC}; ${SETENV} ${MAKE_ENV} \
-	FRAMAC_LIB=${WRKSRC}/lib/fc \
-	FRAMAC_PLUGIN=${WRKSRC}/lib/plugins \
-	FRAMAC_SHARE=${WRKSRC}/share \
-	${GMAKE} ${_MAKE_JOBS} ${MAKE_ARGS} tests)
-
-.endif
+	@cd ${WRKSRC}; ${SETENV} ${MAKE_ENV:NCPP=*} \
+	CPP="${CPP} -C -I${WRKSRC}/share/libc -I." \
+	${GMAKE} ${MAKE_ARGS} oracles fulltests
 
 .include <bsd.port.mk>
diff --git a/devel/frama-c/distinfo b/devel/frama-c/distinfo
index f9be2b875866..2d56d9909f4d 100644
--- a/devel/frama-c/distinfo
+++ b/devel/frama-c/distinfo
@@ -1,2 +1,2 @@
-SHA256 (frama-c-Nitrogen-20111001.tar.gz) = 8afad848321c958fab265045cd152482e77ce7c175ee7c9af2d4bec57a1bc671
-SIZE (frama-c-Nitrogen-20111001.tar.gz) = 12110786
+SHA256 (frama-c-Oxygen-20120901.tar.gz) = f749870a2451f97d24da886c0cc7708e3ec57ad3f169f6b79f9b52be1f47c216
+SIZE (frama-c-Oxygen-20120901.tar.gz) = 10815011
diff --git a/devel/frama-c/pkg-plist b/devel/frama-c/pkg-plist
index 5e82a1904188..22ce37585208 100644
--- a/devel/frama-c/pkg-plist
+++ b/devel/frama-c/pkg-plist
@@ -19,7 +19,6 @@ bin/ptests.byte
 %%GUI%%lib/frama-c/design.cmo
 %%GUI%%lib/frama-c/design.cmx
 %%GUI%%lib/frama-c/design.o
-%%GUI%%lib/frama-c/dgraph.cmi
 %%GUI%%lib/frama-c/file_manager.cmi
 %%GUI%%lib/frama-c/file_manager.cmo
 %%GUI%%lib/frama-c/file_manager.cmx
@@ -60,8 +59,8 @@ bin/ptests.byte
 %%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.cmo
 %%GUI%%lib/frama-c/plugins/gui/Wp.cmxs
 %%GUI%%lib/frama-c/pretty_source.cmi
 %%GUI%%lib/frama-c/pretty_source.cmo
@@ -138,27 +137,30 @@ bin/ptests.byte
 %%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.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
 lib/frama-c/abstract_interp.o
-lib/frama-c/abstract_value.cmi
-lib/frama-c/abstract_value.cmo
-lib/frama-c/abstract_value.cmx
-lib/frama-c/abstract_value.o
 lib/frama-c/alarms.cmi
 lib/frama-c/alarms.cmo
 lib/frama-c/alarms.cmx
 lib/frama-c/alarms.o
+lib/frama-c/allocates.cmi
+lib/frama-c/allocates.cmo
+lib/frama-c/allocates.cmx
+lib/frama-c/allocates.o
 lib/frama-c/alpha.cmi
 lib/frama-c/alpha.cmo
 lib/frama-c/alpha.cmx
@@ -228,6 +230,10 @@ lib/frama-c/cabs2cil.cmi
 lib/frama-c/cabs2cil.cmo
 lib/frama-c/cabs2cil.cmx
 lib/frama-c/cabs2cil.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
@@ -277,10 +283,6 @@ lib/frama-c/cilmsg.cmi
 lib/frama-c/cilmsg.cmo
 lib/frama-c/cilmsg.cmx
 lib/frama-c/cilmsg.o
-lib/frama-c/ciltools.cmi
-lib/frama-c/ciltools.cmo
-lib/frama-c/ciltools.cmx
-lib/frama-c/ciltools.o
 lib/frama-c/cilutil.cmi
 lib/frama-c/cilutil.cmo
 lib/frama-c/cilutil.cmx
@@ -317,10 +319,6 @@ 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
-lib/frama-c/dashtbl.o
 lib/frama-c/dataflow.cmi
 lib/frama-c/dataflow.cmo
 lib/frama-c/dataflow.cmx
@@ -385,6 +383,10 @@ lib/frama-c/filter.cmi
 lib/frama-c/filter.cmo
 lib/frama-c/filter.cmx
 lib/frama-c/filter.o
+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/frontc.cmi
 lib/frama-c/frontc.cmo
 lib/frama-c/frontc.cmx
@@ -397,14 +399,14 @@ lib/frama-c/globals.cmi
 lib/frama-c/globals.cmo
 lib/frama-c/globals.cmx
 lib/frama-c/globals.o
-lib/frama-c/graph.cmi
-lib/frama-c/graph.cmo
-lib/frama-c/graph.cmx
-lib/frama-c/graph.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
 lib/frama-c/hook.cmi
 lib/frama-c/hook.cmo
 lib/frama-c/hook.cmx
@@ -417,6 +419,10 @@ lib/frama-c/hptset.cmi
 lib/frama-c/hptset.cmo
 lib/frama-c/hptset.cmx
 lib/frama-c/hptset.o
+lib/frama-c/indexer.cmi
+lib/frama-c/indexer.cmo
+lib/frama-c/indexer.cmx
+lib/frama-c/indexer.o
 lib/frama-c/infer_annotations.cmi
 lib/frama-c/infer_annotations.cmo
 lib/frama-c/infer_annotations.cmx
@@ -437,10 +443,6 @@ 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/inthash.cmi
-lib/frama-c/inthash.cmo
-lib/frama-c/inthash.cmx
-lib/frama-c/inthash.o
 lib/frama-c/ival.cmi
 lib/frama-c/ival.cmo
 lib/frama-c/ival.cmx
@@ -600,10 +602,6 @@ 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
-lib/frama-c/path_lattice.o
 lib/frama-c/pdgIndex.cmi
 lib/frama-c/pdgIndex.cmo
 lib/frama-c/pdgIndex.cmx
@@ -679,10 +677,6 @@ lib/frama-c/setWithNearest.cmi
 lib/frama-c/setWithNearest.cmo
 lib/frama-c/setWithNearest.cmx
 lib/frama-c/setWithNearest.o
-lib/frama-c/shifted_Location.cmi
-lib/frama-c/shifted_Location.cmo
-lib/frama-c/shifted_Location.cmx
-lib/frama-c/shifted_Location.o
 lib/frama-c/slicingInternals.cmi
 lib/frama-c/slicingInternals.cmo
 lib/frama-c/slicingInternals.cmx
@@ -707,22 +701,18 @@ lib/frama-c/state_dependency_graph.cmi
 lib/frama-c/state_dependency_graph.cmo
 lib/frama-c/state_dependency_graph.cmx
 lib/frama-c/state_dependency_graph.o
-lib/frama-c/state_imp.cmi
-lib/frama-c/state_imp.cmo
-lib/frama-c/state_imp.cmx
-lib/frama-c/state_imp.o
 lib/frama-c/state_selection.cmi
 lib/frama-c/state_selection.cmo
 lib/frama-c/state_selection.cmx
 lib/frama-c/state_selection.o
-lib/frama-c/state_set.cmi
-lib/frama-c/state_set.cmo
-lib/frama-c/state_set.cmx
-lib/frama-c/state_set.o
 lib/frama-c/state_topological.cmi
 lib/frama-c/state_topological.cmo
 lib/frama-c/state_topological.cmx
 lib/frama-c/state_topological.o
+lib/frama-c/statuses_by_call.cmi
+lib/frama-c/statuses_by_call.cmo
+lib/frama-c/statuses_by_call.cmx
+lib/frama-c/statuses_by_call.o
 lib/frama-c/stmts_graph.cmi
 lib/frama-c/stmts_graph.cmo
 lib/frama-c/stmts_graph.cmx
@@ -775,6 +765,10 @@ 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/visitor.cmi
 lib/frama-c/visitor.cmo
 lib/frama-c/visitor.cmx
@@ -783,10 +777,6 @@ lib/frama-c/whitetrack.cmi
 lib/frama-c/whitetrack.cmo
 lib/frama-c/whitetrack.cmx
 lib/frama-c/whitetrack.o
-lib/frama-c/widen.cmi
-lib/frama-c/widen.cmo
-lib/frama-c/widen.cmx
-lib/frama-c/widen.o
 lib/frama-c/widen_type.cmi
 lib/frama-c/widen_type.cmo
 lib/frama-c/widen_type.cmx
@@ -801,14 +791,15 @@ share/emacs/site-lisp/acsl.el
 %%DATADIR%%/acsl.el
 %%DATADIR%%/builtin.c
 %%DATADIR%%/builtin.h
-%%DATADIR%%/check.png
 %%DATADIR%%/configure.ac
+%%DATADIR%%/doc/code/docgen_ge400.ml
+%%DATADIR%%/doc/code/docgen_lt400.ml
 %%DATADIR%%/doc/code/intro_kernel_plugin.txt
 %%DATADIR%%/doc/code/intro_plugin.txt
+%%DATADIR%%/doc/code/intro_plugin_default.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
@@ -824,14 +815,16 @@ share/emacs/site-lisp/acsl.el
 %%DATADIR%%/frama-c.gif
 %%DATADIR%%/frama-c.ico
 %%DATADIR%%/frama-c.rc
-%%DATADIR%%/left.png
 %%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_id_t.h
 %%DATADIR%%/libc/__fc_define_ino_t.h
 %%DATADIR%%/libc/__fc_define_intptr_t.h
 %%DATADIR%%/libc/__fc_define_iovec.h
@@ -841,42 +834,63 @@ share/emacs/site-lisp/acsl.el
 %%DATADIR%%/libc/__fc_define_off_t.h
 %%DATADIR%%/libc/__fc_define_pid_t.h
 %%DATADIR%%/libc/__fc_define_restrict.h
+%%DATADIR%%/libc/__fc_define_sa_family_t.h
+%%DATADIR%%/libc/__fc_define_seek_macros.h
+%%DATADIR%%/libc/__fc_define_sigset_t.h
 %%DATADIR%%/libc/__fc_define_size_t.h
+%%DATADIR%%/libc/__fc_define_sockaddr.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_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_machdep.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/complex.h
 %%DATADIR%%/libc/ctype.c
 %%DATADIR%%/libc/ctype.h
+%%DATADIR%%/libc/dirent.c
 %%DATADIR%%/libc/dirent.h
 %%DATADIR%%/libc/errno.c
 %%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/fenv.h
 %%DATADIR%%/libc/float.c
 %%DATADIR%%/libc/float.h
+%%DATADIR%%/libc/iconv.c
+%%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/limits.h
+%%DATADIR%%/libc/linux/fs.c
+%%DATADIR%%/libc/linux/fs.h
 %%DATADIR%%/libc/locale.c
 %%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/netinet/in.h
+%%DATADIR%%/libc/nl_types.c
+%%DATADIR%%/libc/nl_types.h
+%%DATADIR%%/libc/pwd.c
 %%DATADIR%%/libc/pwd.h
 %%DATADIR%%/libc/setjmp.c
 %%DATADIR%%/libc/setjmp.h
@@ -888,6 +902,7 @@ share/emacs/site-lisp/acsl.el
 %%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
@@ -895,13 +910,33 @@ share/emacs/site-lisp/acsl.el
 %%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/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
@@ -910,6 +945,7 @@ share/emacs/site-lisp/acsl.el
 %%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
@@ -920,27 +956,37 @@ share/emacs/site-lisp/acsl.el
 %%DATADIR%%/manuals/acsl-implementation.pdf
 %%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
 %%DATADIR%%/manuals/value-analysis.pdf
 %%DATADIR%%/manuals/wp-manual.pdf
+%%DATADIR%%/manuals/wp-tutorial.pdf
 %%DATADIR%%/math.c
 %%DATADIR%%/math.h
-%%DATADIR%%/maybe.png
-%%DATADIR%%/right.png
 %%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
@@ -949,6 +995,9 @@ share/emacs/site-lisp/acsl.el
 @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
 @dirrm %%DATADIR%%/doc/code