Updated devel/frama-c to its latest version. Changes include:

-! Kernel     [2012/09/17] Remove useless negative options -no-help,
	      -no-version, -no-print-share-path, -no-print-lib-path and
	      -no-print-plugin-path.
o!* Cil       [2012/09/12] Split constants of logic and C (fixes bts #745).
o! Cil        [2012/09/12] Remove type Cil_type.typsig. Use the functions in
	      Cil_datatype.Typ and Cil_datatype.Logic_typ to compare types.
o! Kernel     [2012/09/03] Remove obsolete constructors Cabs.TRANSFORMER and
	      Cabs.EXPRTRANSFORMER and related parsing rules.
o! Value      [2012/08/29] Signature change for function
	      Db.Value.register_builtin: builtins can now return multiple
	      states.
o! Value      [2012/08/20] Rename Db.Value.assigns_to_zone_inputs_state to
	      Db.Value.assigns_inputs_to_zone. Add new functions
	      Db.Value.assigns_outputs_to_zone and
	      Db.Value.assigns_inputs_to_locations.
o!* Kernel    [2012/07/31] Operations that silently mutate AST should now call
	      Ast.mark_as_changed to clear states depending on it
	      (fixes #!1244).
-! Inout      [2012/07/22] Option -inout-callwise restarts Value when it is
	      newly set
o! Cil        [2012/07/16] Ast changed: Unrool_level renamed into Unroll_specs
	      and its argument becomes a list for next evolutions.
o! Kernel     [2012/07/16] Add function [stmt_can_reach] to the arguments
	      of Dataflow.Backwards, which is used to speed up the analysis.
	      See dataflow.mli for good possible values.
-! Rte        [2012/07/16] Rename option -rte-const into
	      -rte-no-trivial-annotations (set by default).
-! Value      [2012/07/12] More thorough checks for calls through a function
	      pointer: warn when the function type and the pointer are
              not compatible, and stop when they cannot be reconciled.
-! Kernel     [2012/07/12] A negative value given to -ulevel option hides all
	      UNROLL_LOOP pragmas.
+! Kernel     [2012/07/10] Change semantics of 'reachable' properties
	      for functions. Use intrinsic notion instead of accessibility
	      of first statement.
o! Kernel     [2012/06/25] Correct (albeit slow) hash function for terms
	      and term lvalues.
-! Kernel     [2012/06/22] improve 'reachable' properties.
o! Kernel     [2012/06/19] Remove module Inthash. Use Datatype.Int.Hashtbl
	      instead, or directly carbon2nitrogen.sh migration script.
o! Value      [2012/06/18] Made type Ival.tt private.
o! Kernel     [2012/06/11] New API for Annotations which merges old
	      Annotations, Globals.Annotations and operations of Kernel_function
	      over function contracts.
-! Pdg        [2012/06/08] Rename option -dot-pdg into -pdg-dot
o! Kernel     [2012/05/30] Kernel.Functions.get does not silently create
	      a kernel function if it does not already exist. This behavior
	      is kept for Cil builtins.
o! Kernel     [2012/04/26] Plugin.set_optional_help is now deprecated.
*! Kernel     [2012/04/14] Introduce more temporaries for a call [lv = f()] if
	      the return type of f and the type of lv do not match. Fix
	      issue #1024.
o! Kernel     [2012/03/26] Kernel.CppExtraArgs now gets type
	      Plugin.String_list and not Plugin.String_set (fixed bts #!1132).
-! Kernel     [2012/02/29] Adding some more supports for built-in related to
	      memory blocks.
-!  Cil       [2012/02/24] Functions returning a value cannot let control flow
	      falling through the closing '}'  Fixes #685.
-! Kernel     [2012/02/23] Sets generated assigns clauses into the default
	      behavior.
-! Kernel     [2012/02/08] Adding supports for clause allocates and frees
              and their version for loops.
o! Value      [2011/12/02] Moved contents of memory_state/Abstract_value
	      into ai/Lattice_Interval_Set. Use bin/nitrogen2oxygen for
	      automatic migration.
-*! Kernel    [2011/11/07] empty list in complete/disjoint is expanded by
	      logic type-checker to the list of behavior name of current
	      contract. Fixes issue #1006. See bts comments for the
	      differences that can appear in the treatment of specs.
o! Cil        [2011/11/04] Add method pFile in printers. Signature change for
	      Cil.d_file (but you should use !Ast_printer.d_file).
o! Kernel     [2011/10/18] Logic_preprocess.file takes an additional parameter,
	      as gcc pre-processor treats differently .c and .cxx files,
	      and this must be reflected in annotation pre-processing.

3 files changed, 149 insertions, 53 deletions

diff --git a/devel/frama-c/Makefile b/devel/frama-c/Makefile
index d576c6becb2..6c23d94af08 100644
--- a/devel/frama-c/Makefile
+++ b/devel/frama-c/Makefile
@@ -1,9 +1,8 @@
-# $NetBSD: Makefile,v 1.27 2012/10/02 17:10:46 tron Exp $
+# $NetBSD: Makefile,v 1.28 2012/10/08 15:28:03 jaapb Exp $
 #
 
-DISTNAME=	frama-c-Nitrogen-20111001
-PKGNAME=	${DISTNAME:S/-Nitrogen//}
-PKGREVISION=	11
+DISTNAME=	frama-c-Oxygen-20120901
+PKGNAME=	${DISTNAME:S/-Oxygen//}
 CATEGORIES=	devel
 MASTER_SITES=	http://frama-c.com/download/
 
diff --git a/devel/frama-c/PLIST b/devel/frama-c/PLIST
index 24ddf30bc83..d1ffd7a9b44 100644
--- a/devel/frama-c/PLIST
+++ b/devel/frama-c/PLIST
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.3 2011/12/25 15:52:12 asau Exp $
+@comment $NetBSD: PLIST,v 1.4 2012/10/08 15:28:04 jaapb Exp $
 bin/frama-c
 ${PLIST.gui}bin/frama-c-gui
 ${PLIST.gui}bin/frama-c-gui.byte
@@ -56,14 +56,18 @@ 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
+@comment lib/frama-c/abstract_value.cmi
+@comment lib/frama-c/abstract_value.cmo
+@comment lib/frama-c/abstract_value.cmx
+@comment 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
@@ -141,6 +145,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
@@ -190,10 +198,10 @@ 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
+@comment lib/frama-c/ciltools.cmi
+@comment lib/frama-c/ciltools.cmo
+@comment lib/frama-c/ciltools.cmx
+@comment lib/frama-c/ciltools.o
 lib/frama-c/cilutil.cmi
 lib/frama-c/cilutil.cmo
 lib/frama-c/cilutil.cmx
@@ -230,10 +238,10 @@ 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
+@comment lib/frama-c/dashtbl.cmi
+@comment lib/frama-c/dashtbl.cmo
+@comment lib/frama-c/dashtbl.cmx
+@comment lib/frama-c/dashtbl.o
 lib/frama-c/dataflow.cmi
 lib/frama-c/dataflow.cmo
 lib/frama-c/dataflow.cmx
@@ -315,6 +323,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
@@ -356,6 +368,10 @@ ${PLIST.gui}lib/frama-c/history.cmi
 ${PLIST.gui}lib/frama-c/history.cmo
 ${PLIST.gui}lib/frama-c/history.cmx
 ${PLIST.gui}lib/frama-c/history.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
@@ -368,6 +384,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
@@ -388,10 +408,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/inthash.cmi
-lib/frama-c/inthash.cmo
-lib/frama-c/inthash.cmx
-lib/frama-c/inthash.o
+@comment lib/frama-c/inthash.cmi
+@comment lib/frama-c/inthash.cmo
+@comment lib/frama-c/inthash.cmx
+@comment lib/frama-c/inthash.o
 lib/frama-c/ival.cmi
 lib/frama-c/ival.cmo
 lib/frama-c/ival.cmx
@@ -559,10 +579,10 @@ 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
+@comment lib/frama-c/path_lattice.cmi
+@comment lib/frama-c/path_lattice.cmo
+@comment lib/frama-c/path_lattice.cmx
+@comment lib/frama-c/path_lattice.o
 lib/frama-c/pdgIndex.cmi
 lib/frama-c/pdgIndex.cmo
 lib/frama-c/pdgIndex.cmx
@@ -582,20 +602,25 @@ lib/frama-c/plugin.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.cmo
+@comment lib/frama-c/plugins/Wp.cmo
 lib/frama-c/plugins/Wp.cmxs
 ${PLIST.gui}lib/frama-c/plugins/gui/Security_slicing.cmi
 ${PLIST.gui}lib/frama-c/plugins/gui/Security_slicing.cmo
 ${PLIST.gui}lib/frama-c/plugins/gui/Security_slicing.cmxs
+${PLIST.gui}lib/frama-c/plugins/gui/Wp.cma
 ${PLIST.gui}lib/frama-c/plugins/gui/Wp.cmi
-${PLIST.gui}lib/frama-c/plugins/gui/Wp.cmo
+@comment ${PLIST.gui}lib/frama-c/plugins/gui/Wp.cmo
 ${PLIST.gui}lib/frama-c/plugins/gui/Wp.cmxs
 ${PLIST.gui}lib/frama-c/pretty_source.cmi
 ${PLIST.gui}lib/frama-c/pretty_source.cmo
@@ -666,10 +691,10 @@ 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
+@comment lib/frama-c/shifted_Location.cmi
+@comment lib/frama-c/shifted_Location.cmo
+@comment lib/frama-c/shifted_Location.cmx
+@comment lib/frama-c/shifted_Location.o
 lib/frama-c/slicingInternals.cmi
 lib/frama-c/slicingInternals.cmo
 lib/frama-c/slicingInternals.cmx
@@ -702,22 +727,26 @@ 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
+@comment lib/frama-c/state_imp.cmi
+@comment lib/frama-c/state_imp.cmo
+@comment lib/frama-c/state_imp.cmx
+@comment 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
+@comment lib/frama-c/state_set.cmi
+@comment lib/frama-c/state_set.cmo
+@comment lib/frama-c/state_set.cmx
+@comment 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
@@ -770,6 +799,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
@@ -782,10 +815,10 @@ 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
+@comment lib/frama-c/widen.cmi
+@comment lib/frama-c/widen.cmo
+@comment lib/frama-c/widen.cmx
+@comment 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 +834,17 @@ share/frama-c/Makefile.plugin
 share/frama-c/acsl.el
 share/frama-c/builtin.c
 share/frama-c/builtin.h
-share/frama-c/check.png
+@comment share/frama-c/check.png
 share/frama-c/configure.ac
+share/frama-c/doc/code/docgen_ge400.ml
+share/frama-c/doc/code/docgen_lt400.ml
 share/frama-c/doc/code/intro_kernel_plugin.txt
 share/frama-c/doc/code/intro_plugin.txt
+share/frama-c/doc/code/intro_plugin_default.txt
 share/frama-c/doc/code/style.css
 share/frama-c/doc/code/toc_head.htm
 share/frama-c/doc/code/toc_tail.htm
-share/frama-c/failed.png
+@comment share/frama-c/failed.png
 share/frama-c/feedback/considered_valid.png
 share/frama-c/feedback/inconsistent.png
 share/frama-c/feedback/invalid_but_dead.png
@@ -824,14 +860,17 @@ share/frama-c/fluctuat.h
 share/frama-c/frama-c.gif
 share/frama-c/frama-c.ico
 share/frama-c/frama-c.rc
-share/frama-c/left.png
+@comment share/frama-c/left.png
 share/frama-c/libc.c
 share/frama-c/libc.h
 share/frama-c/libc/__fc_builtin.c
 share/frama-c/libc/__fc_builtin.h
+share/frama-c/libc/__fc_builtin_for_normalization.i
 share/frama-c/libc/__fc_define_blkcnt_t.h
 share/frama-c/libc/__fc_define_blksize_t.h
 share/frama-c/libc/__fc_define_dev_t.h
+share/frama-c/libc/__fc_define_fd_set_t.h
+share/frama-c/libc/__fc_define_id_t.h
 share/frama-c/libc/__fc_define_ino_t.h
 share/frama-c/libc/__fc_define_intptr_t.h
 share/frama-c/libc/__fc_define_iovec.h
@@ -841,26 +880,35 @@ share/frama-c/libc/__fc_define_null.h
 share/frama-c/libc/__fc_define_off_t.h
 share/frama-c/libc/__fc_define_pid_t.h
 share/frama-c/libc/__fc_define_restrict.h
+share/frama-c/libc/__fc_define_sa_family_t.h
+share/frama-c/libc/__fc_define_seek_macros.h
+share/frama-c/libc/__fc_define_sigset_t.h
 share/frama-c/libc/__fc_define_size_t.h
+share/frama-c/libc/__fc_define_sockaddr.h
 share/frama-c/libc/__fc_define_ssize_t.h
 share/frama-c/libc/__fc_define_suseconds_t.h
 share/frama-c/libc/__fc_define_time_t.h
+share/frama-c/libc/__fc_define_timespec.h
 share/frama-c/libc/__fc_define_uid_and_gid.h
 share/frama-c/libc/__fc_define_useconds_t.h
 share/frama-c/libc/__fc_define_wchar_t.h
 share/frama-c/libc/__fc_machdep.h
 share/frama-c/libc/__fc_string_axiomatic.h
+share/frama-c/libc/arpa/inet.c
+share/frama-c/libc/arpa/inet.h
 share/frama-c/libc/assert.c
 share/frama-c/libc/assert.h
 share/frama-c/libc/complex.c
 share/frama-c/libc/complex.h
 share/frama-c/libc/ctype.c
 share/frama-c/libc/ctype.h
+share/frama-c/libc/dirent.c
 share/frama-c/libc/dirent.h
 share/frama-c/libc/errno.c
 share/frama-c/libc/errno.h
 share/frama-c/libc/fc_posix_runtime.c
 share/frama-c/libc/fc_runtime.c
+share/frama-c/libc/fcntl.c
 share/frama-c/libc/fcntl.h
 share/frama-c/libc/fenv.c
 share/frama-c/libc/fenv.h
@@ -868,15 +916,27 @@ share/frama-c/libc/float.c
 share/frama-c/libc/float.h
 share/frama-c/libc/inttypes.c
 share/frama-c/libc/inttypes.h
+share/frama-c/libc/iconv.c
+share/frama-c/libc/iconv.h
+share/frama-c/libc/ifaddrs.c
+share/frama-c/libc/ifaddrs.h
 share/frama-c/libc/iso646.c
 share/frama-c/libc/iso646.h
 share/frama-c/libc/limits.c
 share/frama-c/libc/limits.h
+share/frama-c/libc/linux/fs.c
+share/frama-c/libc/linux/fs.h
 share/frama-c/libc/locale.c
 share/frama-c/libc/locale.h
 share/frama-c/libc/math.c
 share/frama-c/libc/math.h
+share/frama-c/libc/net/if.c
+share/frama-c/libc/net/if.h
+share/frama-c/libc/netinet/in.c
 share/frama-c/libc/netinet/in.h
+share/frama-c/libc/nl_types.c
+share/frama-c/libc/nl_types.h
+share/frama-c/libc/pwd.c
 share/frama-c/libc/pwd.h
 share/frama-c/libc/setjmp.c
 share/frama-c/libc/setjmp.h
@@ -888,6 +948,7 @@ share/frama-c/libc/stdbool.c
 share/frama-c/libc/stdbool.h
 share/frama-c/libc/stddef.c
 share/frama-c/libc/stddef.h
+share/frama-c/libc/stdint.c
 share/frama-c/libc/stdint.h
 share/frama-c/libc/stdio.c
 share/frama-c/libc/stdio.h
@@ -895,13 +956,33 @@ share/frama-c/libc/stdlib.c
 share/frama-c/libc/stdlib.h
 share/frama-c/libc/string.c
 share/frama-c/libc/string.h
+share/frama-c/libc/strings.c
+share/frama-c/libc/strings.h
+share/frama-c/libc/sys/ioctl.c
+share/frama-c/libc/sys/ioctl.h
+share/frama-c/libc/sys/param.c
+share/frama-c/libc/sys/param.h
+share/frama-c/libc/sys/resource.c
+share/frama-c/libc/sys/resource.h
+share/frama-c/libc/sys/select.c
+share/frama-c/libc/sys/select.h
+share/frama-c/libc/sys/socket.c
 share/frama-c/libc/sys/socket.h
+share/frama-c/libc/sys/stat.c
 share/frama-c/libc/sys/stat.h
+share/frama-c/libc/sys/time.c
 share/frama-c/libc/sys/time.h
+share/frama-c/libc/sys/types.c
 share/frama-c/libc/sys/types.h
+share/frama-c/libc/sys/uio.c
 share/frama-c/libc/sys/uio.h
+share/frama-c/libc/sys/un.c
+share/frama-c/libc/sys/un.h
+share/frama-c/libc/sys/wait.c
 share/frama-c/libc/sys/wait.h
+share/frama-c/libc/syslog.c
 share/frama-c/libc/syslog.h
+share/frama-c/libc/termios.c
 share/frama-c/libc/termios.h
 share/frama-c/libc/test.c
 share/frama-c/libc/tgmath.c
@@ -910,6 +991,7 @@ share/frama-c/libc/time.c
 share/frama-c/libc/time.h
 share/frama-c/libc/uchar.c
 share/frama-c/libc/uchar.h
+share/frama-c/libc/unistd.c
 share/frama-c/libc/unistd.h
 share/frama-c/libc/wchar.c
 share/frama-c/libc/wchar.h
@@ -920,26 +1002,39 @@ share/frama-c/malloc.c
 share/frama-c/manuals/acsl-implementation.pdf
 share/frama-c/manuals/acsl.pdf
 share/frama-c/manuals/aorai-manual.pdf
-share/frama-c/manuals/jessie-tutorial.pdf
+@comment share/frama-c/manuals/jessie-tutorial.pdf
 share/frama-c/manuals/metrics-manual.pdf
 share/frama-c/manuals/plugin-development-guide.pdf
 share/frama-c/manuals/rte-manual.pdf
 share/frama-c/manuals/user-manual.pdf
 share/frama-c/manuals/value-analysis.pdf
 share/frama-c/manuals/wp-manual.pdf
+share/frama-c/manuals/wp-tutorial.pdf
 share/frama-c/math.c
 share/frama-c/math.h
-share/frama-c/maybe.png
-share/frama-c/right.png
+@comment share/frama-c/maybe.png
+@comment share/frama-c/right.png
 share/frama-c/unmark.png
+share/frama-c/wp/Cfloat.v
+share/frama-c/wp/Cint.v
+share/frama-c/wp/Cmath.v
+share/frama-c/wp/Memory.v
+share/frama-c/wp/Qedlib.v
+share/frama-c/wp/Vset.v
+share/frama-c/wp/cfloat.mlw
+share/frama-c/wp/cint.mlw
+share/frama-c/wp/cmath.mlw
 share/frama-c/wp/hoare_ergo.why
 share/frama-c/wp/hoare_model.v
 share/frama-c/wp/hoare_model.why
+share/frama-c/wp/memory.mlw
+share/frama-c/wp/qed.mlw
 share/frama-c/wp/runtime_ergo.why
 share/frama-c/wp/runtime_model.v
 share/frama-c/wp/runtime_model.why
 share/frama-c/wp/store_ergo.why
 share/frama-c/wp/store_model.v
 share/frama-c/wp/store_model.why
+share/frama-c/wp/vset.mlw
 share/frama-c/wp/wp.v
 @pkgdir lib/frama-c/plugins/gui
diff --git a/devel/frama-c/distinfo b/devel/frama-c/distinfo
index dea5dca9d00..43384e9e51a 100644
--- a/devel/frama-c/distinfo
+++ b/devel/frama-c/distinfo
@@ -1,5 +1,7 @@
-$NetBSD: distinfo,v 1.3 2011/12/25 15:52:12 asau Exp $
+$NetBSD: distinfo,v 1.4 2012/10/08 15:28:04 jaapb Exp $
 
-SHA1 (frama-c-Nitrogen-20111001.tar.gz) = 5b5b8cd0b21e007012c899ab74bb33cbe23582ed
-RMD160 (frama-c-Nitrogen-20111001.tar.gz) = 4401666bdca00c9f8fe9882309116633e5d68984
-Size (frama-c-Nitrogen-20111001.tar.gz) = 12110786 bytes
+SHA1 (frama-c-Oxygen-20120901.tar.gz) = 65aef0a88b788d11a6b5061dc08741492859de40
+RMD160 (frama-c-Oxygen-20120901.tar.gz) = 76daf11770a52b1b1bc59ca9c576208ac08755a8
+Size (frama-c-Oxygen-20120901.tar.gz) = 10815011 bytes
+SHA1 (patch-Makefile) = f851797e599f682c4067fb02543b66c38cbd3446
+SHA1 (patch-src_wp_Makefile) = bce0f55bae0718df462b2e1b6da689a4a00113d1