Update to Frama-C Nitrogen release 2011-10-01

See full list of changes at http://frama-c.com/Changelog.html#Nitrogen-20111001


Nitrogen Release [20111001]

Frama-C General

New Features

  * [Cil]   Enumerated constants are kept in the AST.
  * [Cil]   Implement precise dataflow on switch constructs. As side effect, improve precision of value analysis.
  * [Cil]   Fixed #720 (incorrect simplification of switch).
  * [Cil]   Support for &"constant_string" in parser.
  * [Cil]   Normalization of lval: T+1 ==> &T[1] when T is in fact an array (implies *(T+1) ==> T[1])
  * [Cil]   Pretty-printing lval and term_lval the same way
  * [Cil]   Cache results of offsets computations.
  * [Cil]   Add support for GCC specific cast from field of union to union
  * [Kernel]   Exit status on unknown error is now 125. 127 and 126 are reserved for the shell by POSIX.
  * [Kernel]   Better error message when plug-in crashes on loading (bts #737).
  * [Kernel]   Big integers can now be displayed using hexadecimal notation.
  * [Kernel]   \at(p,Old) is pretty-printed as \old(p).
  * [Kernel]   Some messages may be printed several time for the same line if they refer to different columns.
  * [Kernel]   Better handling of comments with -keep-comments and new API. See Cabshelper.Comments and Globals.get_comments_*
  * [Kernel]   Better pretty printing of lists of any elements
  * [Kernel]   Current pragmas no longer give rise to code annotations (as they do not contain anything that can be proven).
  * [Kernel]   Improve space complexity of function stmt_can_reach.
  * [Kernel]   New kind of command-line parameter, for commands that do heavy output. Used for Value, Pdg and Metrics.
  * [Logic]   Added support for bitwise operators --> and <--> into ACSL formula.


Carbon Release [20110201]

Frama-C General

New Features

  * [Configure]   Frama-C does not require Apron anymore (Why does for Jessie). Thus fix bug #647.
  * [Kernel]   Improve performance on platform with dynami.c loading. Mainly impact value analysis (for developers: improve
    efficiency of Dynamic.get).
  * [Kernel]   Handle errors better when they occur when exiting Frama-C. Slight semantic changes for exit code: - old code 5 is now
    127; - code 5 is now: error raised when exiting Frama-C normally; - code 6: error raised when exiting Frama-C abnormally.
  * [Logic]   Fix priority bug in parser.
  * [Logic]   Mentioning a formal on the left-hand side of an assigns clause is now an error when type-checking logic annotations.
  * [Makefile]   Fixed bug #638. By default, warnings are no more errors when compiling a public Frama-C distribution and plug-ins.
    SVN versions of Frama-C are still compiled with "-warn-error A".


Carbon Release [20101201]

Frama-C General

New Features

  * [Cil]   Be less agressive during inline function merge. Alpha equivalent function are now kept separate.
  * [Cil]   Clean up local variables handling and pretty-printing modified pBlock method interface (unified pBlock and pInnerBlock)
  * [Cil]   Cil normalization takes care of abrupt clauses
  * [Configure]   Better detection of native dynlink support.
  * [Kernel]   Feature #484 about requires into named behaviors
  * [Kernel]   Fixed bug #548: limit.h now syntactically correct. Architectures other than x86_32 still unsupported.


Boron Release [20100401]

Frama-C General

New Features

  * [Cil]   Extend logic pretty printer to handle all specific clauses
  * [Configure]   Dynamic plug-ins are now statically linked by default whenever native dynlink is not usable (bts #301).
  * [Configure]   Compiling the GUI now requires LablGnomeCanvas.
  * [Kernel]   Add status for all clauses
  * [Kernel]   Clarification of the multiple accesses warning. Becomes "undefined multiple accesses in expression".
  * [Kernel]   Better error messages when a dynamic plug-in cannot be loaded.
  * [Kernel]   Better -*-help.
  * [Kernel]   New option -no-dynlink in order to prevent loading of dynamic plug-ins.
  * [Kernel]   The journal is generated only if the GUI is crashing, or if the option -journal-enable is explicitely set (fixed issue
    #330).
  * [Kernel]   Backtrace when Frama-C is crashing (only if Frama-C is compiled with caml >= 3.11.0)
  * [Kernel]   New option "-plugin-h" as an alias for option "-plugin-help"
  * [Kernel]   Preliminary standard C library in $FRAMAC_SHARE/libc
  * [Logic]   Better error message when using = in annotations
  * [Logic]   ordering of clauses in contracts
  * [Logic]   If a C typedef integer, real or boolean exists, it takes precedence over corresponding logic type. The logic type
    remains accessible through its utf-8 denomination.
  * [Logic]   Support for type abbreviation in logic
  * [Logic]   Support for "reads \nothing"
  * [Logic]   Adding "\pi" as built-in symbol


Beryllium Release [20090902]

Frama-C General

New Features

  * [Configure]   Detection of dot if required.
  * [Journal]   Better handling of exceptions.
  * [Kernel]   Slightly less false alarms with -warn-unspecified-order
  * [Makefile]   Why is no longer a compilation dependency. It is required only at runtime for the experimental WP plugin.
  * [Makefile]   Now possible to build custom binaries for plug-ins. Roughly these binaries are frama-c[.byte] + the plug-in
    statically-linked. The goal is called "static" in the plug-in's makefile.

7 files changed, 808 insertions, 1480 deletions

diff --git a/devel/frama-c/Makefile b/devel/frama-c/Makefile
index dc7ccb51623..c64a59ab6cf 100644
--- a/devel/frama-c/Makefile
+++ b/devel/frama-c/Makefile
@@ -1,9 +1,8 @@
-# $NetBSD: Makefile,v 1.15 2011/12/24 13:18:00 dholland Exp $
+# $NetBSD: Makefile,v 1.16 2011/12/25 15:52:12 asau Exp $
 #
 
-DISTNAME=	frama-c-Beryllium-20090901
-PKGNAME=	${DISTNAME:S/-Beryllium//}
-PKGREVISION=	9
+DISTNAME=	frama-c-Nitrogen-20111001
+PKGNAME=	${DISTNAME:S/-Nitrogen//}
 CATEGORIES=	devel
 MASTER_SITES=	http://frama-c.com/download/
 
@@ -17,11 +16,8 @@ PKG_DESTDIR_SUPPORT=	user-destdir
 USE_TOOLS+=	gmake
 GNU_CONFIGURE=	yes
 
-PLIST_SRC=	${PLIST_SRC_DFLT}
-
 .include "options.mk"
 
-.include "../../x11/gtksourceview/buildlink3.mk"
 .include "../../x11/lablgtk/buildlink3.mk"
 .include "../../lang/ocaml/buildlink3.mk"
 .include "../../mk/bsd.pkg.mk"
diff --git a/devel/frama-c/PLIST b/devel/frama-c/PLIST
index 0bfd049cca5..24ddf30bc83 100644
--- a/devel/frama-c/PLIST
+++ b/devel/frama-c/PLIST
@@ -1,372 +1,945 @@
-@comment $NetBSD: PLIST,v 1.2 2009/12/07 16:39:12 wiz Exp $
-bin/caduceus
+@comment $NetBSD: PLIST,v 1.3 2011/12/25 15:52:12 asau Exp $
 bin/frama-c
-bin/frama-c-gui
-bin/frama-c-gui.byte
+${PLIST.gui}bin/frama-c-gui
+${PLIST.gui}bin/frama-c-gui.byte
 bin/frama-c.byte
-bin/gwhy
-bin/gwhy-bin
-bin/jessie
-bin/krakatoa
-bin/rv_merge
-bin/simplify2why
-bin/tool-stat
-bin/why
-bin/why-config
-bin/why-cpulimit
-bin/why-dp
-bin/why-obfuscator
-bin/why-stat
-bin/why2html
-lib/frama-c/about_dialog.cmi
+bin/ptests.byte
+lib/frama-c/Constant_Propagation.cmo
+lib/frama-c/Constant_Propagation.cmx
+lib/frama-c/Constant_Propagation.o
+lib/frama-c/From.cmo
+lib/frama-c/From.cmx
+lib/frama-c/From.o
+lib/frama-c/Impact.cmo
+lib/frama-c/Impact.cmx
+lib/frama-c/Impact.o
+lib/frama-c/Inout.cmo
+lib/frama-c/Inout.cmx
+lib/frama-c/Inout.o
+lib/frama-c/Metrics.cmo
+lib/frama-c/Metrics.cmx
+lib/frama-c/Metrics.o
+lib/frama-c/Occurrence.cmo
+lib/frama-c/Occurrence.cmx
+lib/frama-c/Occurrence.o
+lib/frama-c/Pdg.cmo
+lib/frama-c/Pdg.cmx
+lib/frama-c/Pdg.o
+lib/frama-c/Postdominators.cmo
+lib/frama-c/Postdominators.cmx
+lib/frama-c/Postdominators.o
+lib/frama-c/RteGen.cmo
+lib/frama-c/RteGen.cmx
+lib/frama-c/RteGen.o
+lib/frama-c/Scope.cmo
+lib/frama-c/Scope.cmx
+lib/frama-c/Scope.o
+lib/frama-c/Semantic_callgraph.cmo
+lib/frama-c/Semantic_callgraph.cmx
+lib/frama-c/Semantic_callgraph.o
+lib/frama-c/Slicing.cmo
+lib/frama-c/Slicing.cmx
+lib/frama-c/Slicing.o
+lib/frama-c/Sparecode.cmo
+lib/frama-c/Sparecode.cmx
+lib/frama-c/Sparecode.o
+lib/frama-c/Syntactic_callgraph.cmo
+lib/frama-c/Syntactic_callgraph.cmx
+lib/frama-c/Syntactic_callgraph.o
+lib/frama-c/Users.cmo
+lib/frama-c/Users.cmx
+lib/frama-c/Users.o
+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
+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/alpha.cmi
+lib/frama-c/alpha.cmo
+lib/frama-c/alpha.cmx
+lib/frama-c/alpha.o
+${PLIST.gui}lib/frama-c/analyses_manager.cmi
+${PLIST.gui}lib/frama-c/analyses_manager.cmo
+${PLIST.gui}lib/frama-c/analyses_manager.cmx
+${PLIST.gui}lib/frama-c/analyses_manager.o
 lib/frama-c/annotations.cmi
+lib/frama-c/annotations.cmo
+lib/frama-c/annotations.cmx
+lib/frama-c/annotations.o
 lib/frama-c/ast.cmi
+lib/frama-c/ast.cmo
+lib/frama-c/ast.cmx
+lib/frama-c/ast.o
 lib/frama-c/ast_info.cmi
+lib/frama-c/ast_info.cmo
+lib/frama-c/ast_info.cmx
+lib/frama-c/ast_info.o
 lib/frama-c/ast_printer.cmi
+lib/frama-c/ast_printer.cmo
+lib/frama-c/ast_printer.cmx
+lib/frama-c/ast_printer.o
 lib/frama-c/availexpslv.cmi
+lib/frama-c/availexpslv.cmo
+lib/frama-c/availexpslv.cmx
+lib/frama-c/availexpslv.o
+lib/frama-c/bag.cmi
+lib/frama-c/bag.cmo
+lib/frama-c/bag.cmx
+lib/frama-c/bag.o
 lib/frama-c/base.cmi
-lib/frama-c/baseUtils.cmi
+lib/frama-c/base.cmo
+lib/frama-c/base.cmx
+lib/frama-c/base.o
 lib/frama-c/base_Set_Lattice.cmi
+lib/frama-c/base_Set_Lattice.cmo
+lib/frama-c/base_Set_Lattice.cmx
+lib/frama-c/base_Set_Lattice.o
 lib/frama-c/binary_cache.cmi
+lib/frama-c/binary_cache.cmo
+lib/frama-c/binary_cache.cmx
+lib/frama-c/binary_cache.o
 lib/frama-c/bit_model_access.cmi
+lib/frama-c/bit_model_access.cmo
+lib/frama-c/bit_model_access.cmx
+lib/frama-c/bit_model_access.o
 lib/frama-c/bit_utils.cmi
+lib/frama-c/bit_utils.cmo
+lib/frama-c/bit_utils.cmx
+lib/frama-c/bit_utils.o
+lib/frama-c/bitvector.cmi
+lib/frama-c/bitvector.cmo
+lib/frama-c/bitvector.cmx
+lib/frama-c/bitvector.o
+${PLIST.gui}lib/frama-c/book_manager.cmi
+${PLIST.gui}lib/frama-c/book_manager.cmo
+${PLIST.gui}lib/frama-c/book_manager.cmx
+${PLIST.gui}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
+lib/frama-c/cabs.cmx
+lib/frama-c/cabs.o
 lib/frama-c/cabs2cil.cmi
+lib/frama-c/cabs2cil.cmo
+lib/frama-c/cabs2cil.cmx
+lib/frama-c/cabs2cil.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
+lib/frama-c/cabshelper.o
 lib/frama-c/cabsvisit.cmi
+lib/frama-c/cabsvisit.cmo
+lib/frama-c/cabsvisit.cmx
+lib/frama-c/cabsvisit.o
 lib/frama-c/callgraph.cmi
+lib/frama-c/callgraph.cmo
+lib/frama-c/callgraph.cmx
+lib/frama-c/callgraph.o
 lib/frama-c/cfg.cmi
+lib/frama-c/cfg.cmo
+lib/frama-c/cfg.cmx
+lib/frama-c/cfg.o
 lib/frama-c/cil.cmi
+lib/frama-c/cil.cmo
+lib/frama-c/cil.cmx
+lib/frama-c/cil.o
 lib/frama-c/cilE.cmi
-lib/frama-c/cil_computation.cmi
+lib/frama-c/cilE.cmo
+lib/frama-c/cilE.cmx
+lib/frama-c/cilE.o
 lib/frama-c/cil_const.cmi
+lib/frama-c/cil_const.cmo
+lib/frama-c/cil_const.cmx
+lib/frama-c/cil_const.o
 lib/frama-c/cil_datatype.cmi
+lib/frama-c/cil_datatype.cmo
+lib/frama-c/cil_datatype.cmx
+lib/frama-c/cil_datatype.o
+lib/frama-c/cil_state_builder.cmi
+lib/frama-c/cil_state_builder.cmo
+lib/frama-c/cil_state_builder.cmx
+lib/frama-c/cil_state_builder.o
 lib/frama-c/cil_types.cmi
 lib/frama-c/cilglobopt.cmi
+lib/frama-c/cilglobopt.cmo
+lib/frama-c/cilglobopt.cmx
+lib/frama-c/cilglobopt.o
 lib/frama-c/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
+lib/frama-c/cilutil.o
 lib/frama-c/clexer.cmi
+lib/frama-c/clexer.cmo
+lib/frama-c/clexer.cmx
+lib/frama-c/clexer.o
 lib/frama-c/clist.cmi
+lib/frama-c/clist.cmo
+lib/frama-c/clist.cmx
+lib/frama-c/clist.o
 lib/frama-c/cmdline.cmi
-lib/frama-c/computation.cmi
+lib/frama-c/cmdline.cmo
+lib/frama-c/cmdline.cmx
+lib/frama-c/cmdline.o
+lib/frama-c/command.cmi
+lib/frama-c/command.cmo
+lib/frama-c/command.cmx
+lib/frama-c/command.o
 lib/frama-c/config.cmi
+lib/frama-c/config.cmo
+lib/frama-c/config.cmx
+lib/frama-c/config.o
 lib/frama-c/cparser.cmi
+lib/frama-c/cparser.cmo
+lib/frama-c/cparser.cmx
+lib/frama-c/cparser.o
 lib/frama-c/cprint.cmi
-lib/frama-c/cvalue_type.cmi
+lib/frama-c/cprint.cmo
+lib/frama-c/cprint.cmx
+lib/frama-c/cprint.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
+lib/frama-c/dashtbl.o
 lib/frama-c/dataflow.cmi
+lib/frama-c/dataflow.cmo
+lib/frama-c/dataflow.cmx
+lib/frama-c/dataflow.o
 lib/frama-c/datatype.cmi
+lib/frama-c/datatype.cmo
+lib/frama-c/datatype.cmx
+lib/frama-c/datatype.o
 lib/frama-c/db.cmi
-lib/frama-c/db_types.cmi
+lib/frama-c/db.cmo
+lib/frama-c/db.cmx
+lib/frama-c/db.o
 lib/frama-c/deadcodeelim.cmi
-lib/frama-c/debug.cmi
+lib/frama-c/deadcodeelim.cmo
+lib/frama-c/deadcodeelim.cmx
+lib/frama-c/deadcodeelim.o
+${PLIST.gui}lib/frama-c/debug_manager.cmi
+${PLIST.gui}lib/frama-c/debug_manager.cmo
+${PLIST.gui}lib/frama-c/debug_manager.cmx
+${PLIST.gui}lib/frama-c/debug_manager.o
 lib/frama-c/descr.cmi
-lib/frama-c/design.cmi
+lib/frama-c/descr.cmo
+lib/frama-c/descr.cmx
+lib/frama-c/descr.o
+lib/frama-c/description.cmi
+lib/frama-c/description.cmo
+lib/frama-c/description.cmx
+lib/frama-c/description.o
+${PLIST.gui}lib/frama-c/design.cmi
+${PLIST.gui}lib/frama-c/design.cmo
+${PLIST.gui}lib/frama-c/design.cmx
+${PLIST.gui}lib/frama-c/design.o
+${PLIST.gui}lib/frama-c/dgraph.cmi
 lib/frama-c/dominators.cmi
+lib/frama-c/dominators.cmo
+lib/frama-c/dominators.cmx
+lib/frama-c/dominators.o
 lib/frama-c/dynamic.cmi
+lib/frama-c/dynamic.cmo
+lib/frama-c/dynamic.cmx
+lib/frama-c/dynamic.o
 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
+lib/frama-c/errorloc.o
 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/extlib.cmi
+lib/frama-c/extlib.cmo
+lib/frama-c/extlib.cmx
+lib/frama-c/extlib.o
 lib/frama-c/file.cmi
-lib/frama-c/filetree.cmi
+lib/frama-c/file.cmo
+lib/frama-c/file.cmx
+lib/frama-c/file.o
+${PLIST.gui}lib/frama-c/file_manager.cmi
+${PLIST.gui}lib/frama-c/file_manager.cmo
+${PLIST.gui}lib/frama-c/file_manager.cmx
+${PLIST.gui}lib/frama-c/file_manager.o
+${PLIST.gui}lib/frama-c/filetree.cmi
+${PLIST.gui}lib/frama-c/filetree.cmo
+${PLIST.gui}lib/frama-c/filetree.cmx
+${PLIST.gui}lib/frama-c/filetree.o
 lib/frama-c/filter.cmi
+lib/frama-c/filter.cmo
+lib/frama-c/filter.cmx
+lib/frama-c/filter.o
 lib/frama-c/frontc.cmi
+lib/frama-c/frontc.cmo
+lib/frama-c/frontc.cmx
+lib/frama-c/frontc.o
 lib/frama-c/function_Froms.cmi
+lib/frama-c/function_Froms.cmo
+lib/frama-c/function_Froms.cmx
+lib/frama-c/function_Froms.o
 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/gtk_helper.cmi
-lib/frama-c/gui_init.cmi
+lib/frama-c/growArray.cmo
+lib/frama-c/growArray.cmx
+lib/frama-c/growArray.o
+${PLIST.gui}lib/frama-c/gtk_form.cmi
+${PLIST.gui}lib/frama-c/gtk_form.cmo
+${PLIST.gui}lib/frama-c/gtk_form.cmx
+${PLIST.gui}lib/frama-c/gtk_form.o
+${PLIST.gui}lib/frama-c/gtk_helper.cmi
+${PLIST.gui}lib/frama-c/gtk_helper.cmo
+${PLIST.gui}lib/frama-c/gtk_helper.cmx
+${PLIST.gui}lib/frama-c/gtk_helper.o
+${PLIST.gui}lib/frama-c/gui_init.cmi
+${PLIST.gui}lib/frama-c/gui_parameters.cmi
+${PLIST.gui}lib/frama-c/gui_parameters.cmo
+${PLIST.gui}lib/frama-c/gui_parameters.cmx
+${PLIST.gui}lib/frama-c/gui_parameters.o
+${PLIST.gui}lib/frama-c/help_manager.cmi
+${PLIST.gui}lib/frama-c/help_manager.cmo
+${PLIST.gui}lib/frama-c/help_manager.cmx
+${PLIST.gui}lib/frama-c/help_manager.o
+${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/hook.cmi
+lib/frama-c/hook.cmo
+lib/frama-c/hook.cmx
+lib/frama-c/hook.o
+lib/frama-c/hptmap.cmi
+lib/frama-c/hptmap.cmo
+lib/frama-c/hptmap.cmx
+lib/frama-c/hptmap.o
+lib/frama-c/hptset.cmi
+lib/frama-c/hptset.cmo
+lib/frama-c/hptset.cmx
+lib/frama-c/hptset.o
 lib/frama-c/infer_annotations.cmi
+lib/frama-c/infer_annotations.cmo
+lib/frama-c/infer_annotations.cmx
+lib/frama-c/infer_annotations.o
 lib/frama-c/inout_type.cmi
+lib/frama-c/inout_type.cmo
+lib/frama-c/inout_type.cmx
+lib/frama-c/inout_type.o
 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/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
+lib/frama-c/ival.o
 lib/frama-c/journal.cmi
+lib/frama-c/journal.cmo
+lib/frama-c/journal.cmx
+lib/frama-c/journal.o
 lib/frama-c/kernel.cmi
+lib/frama-c/kernel.cmo
+lib/frama-c/kernel.cmx
+lib/frama-c/kernel.o
 lib/frama-c/kernel_function.cmi
-lib/frama-c/kernel_type.cmi
-lib/frama-c/kind.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
-lib/frama-c/launcher.cmi
+${PLIST.gui}lib/frama-c/launcher.cmi
+${PLIST.gui}lib/frama-c/launcher.cmo
+${PLIST.gui}lib/frama-c/launcher.cmx
+${PLIST.gui}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
+lib/frama-c/lmap.o
 lib/frama-c/lmap_bitwise.cmi
-lib/frama-c/lmap_whole.cmi
+lib/frama-c/lmap_bitwise.cmo
+lib/frama-c/lmap_bitwise.cmx
+lib/frama-c/lmap_bitwise.o
 lib/frama-c/locations.cmi
+lib/frama-c/locations.cmo
+lib/frama-c/locations.cmx
+lib/frama-c/locations.o
 lib/frama-c/log.cmi
+lib/frama-c/log.cmo
+lib/frama-c/log.cmx
+lib/frama-c/log.o
 lib/frama-c/logic_builtin.cmi
+lib/frama-c/logic_builtin.cmo
+lib/frama-c/logic_builtin.cmx
+lib/frama-c/logic_builtin.o
 lib/frama-c/logic_const.cmi
+lib/frama-c/logic_const.cmo
+lib/frama-c/logic_const.cmx
+lib/frama-c/logic_const.o
 lib/frama-c/logic_env.cmi
+lib/frama-c/logic_env.cmo
+lib/frama-c/logic_env.cmx
+lib/frama-c/logic_env.o
 lib/frama-c/logic_interp.cmi
+lib/frama-c/logic_interp.cmo
+lib/frama-c/logic_interp.cmx
+lib/frama-c/logic_interp.o
 lib/frama-c/logic_lexer.cmi
+lib/frama-c/logic_lexer.cmo
+lib/frama-c/logic_lexer.cmx
+lib/frama-c/logic_lexer.o
 lib/frama-c/logic_parser.cmi
+lib/frama-c/logic_parser.cmo
+lib/frama-c/logic_parser.cmx
+lib/frama-c/logic_parser.o
 lib/frama-c/logic_preprocess.cmi
+lib/frama-c/logic_preprocess.cmo
+lib/frama-c/logic_preprocess.cmx
+lib/frama-c/logic_preprocess.o
+lib/frama-c/logic_print.cmi
+lib/frama-c/logic_print.cmo
+lib/frama-c/logic_print.cmx
+lib/frama-c/logic_print.o
 lib/frama-c/logic_ptree.cmi
 lib/frama-c/logic_typing.cmi
+lib/frama-c/logic_typing.cmo
+lib/frama-c/logic_typing.cmx
+lib/frama-c/logic_typing.o
 lib/frama-c/logic_utils.cmi
+lib/frama-c/logic_utils.cmo
+lib/frama-c/logic_utils.cmx
+lib/frama-c/logic_utils.o
 lib/frama-c/loop.cmi
+lib/frama-c/loop.cmo
+lib/frama-c/loop.cmx
+lib/frama-c/loop.o
 lib/frama-c/machdep.cmi
+lib/frama-c/machdep.cmo
+lib/frama-c/machdep.cmx
+lib/frama-c/machdep.o
 lib/frama-c/machdep_ppc_32.cmi
-lib/frama-c/machdep_ppc_32_diab.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/map_Lattice.cmi
+lib/frama-c/map_Lattice.cmo
+lib/frama-c/map_Lattice.cmx
+lib/frama-c/map_Lattice.o
+lib/frama-c/map_common_interface.cmi
+lib/frama-c/map_common_interface.cmo
+lib/frama-c/map_common_interface.cmx
+lib/frama-c/map_common_interface.o
+${PLIST.gui}lib/frama-c/menu_manager.cmi
+${PLIST.gui}lib/frama-c/menu_manager.cmo
+${PLIST.gui}lib/frama-c/menu_manager.cmx
+${PLIST.gui}lib/frama-c/menu_manager.o
 lib/frama-c/mergecil.cmi
-lib/frama-c/mergemap.cmi
+lib/frama-c/mergecil.cmo
+lib/frama-c/mergecil.cmx
+lib/frama-c/mergecil.o
 lib/frama-c/messages.cmi
-lib/frama-c/mweak.cmi
+lib/frama-c/messages.cmo
+lib/frama-c/messages.cmx
+lib/frama-c/messages.o
 lib/frama-c/my_bigint.cmi
-lib/frama-c/namespace.cmi
+lib/frama-c/my_bigint.cmo
+lib/frama-c/my_bigint.cmx
+lib/frama-c/my_bigint.o
+lib/frama-c/mybigarray.o
 lib/frama-c/new_offsetmap.cmi
+lib/frama-c/new_offsetmap.cmo
+lib/frama-c/new_offsetmap.cmx
+lib/frama-c/new_offsetmap.o
 lib/frama-c/obfuscate.cmi
+lib/frama-c/obfuscate.cmo
+lib/frama-c/obfuscate.cmx
+lib/frama-c/obfuscate.o
 lib/frama-c/offsetmap.cmi
+lib/frama-c/offsetmap.cmo
+lib/frama-c/offsetmap.cmx
+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/oneret.cmi
+lib/frama-c/oneret.cmo
+lib/frama-c/oneret.cmx
+lib/frama-c/oneret.o
 lib/frama-c/origin.cmi
-lib/frama-c/parameters.cmi
-lib/frama-c/patch.cmi
+lib/frama-c/origin.cmo
+lib/frama-c/origin.cmx
+lib/frama-c/origin.o
+lib/frama-c/parameter.cmi
+lib/frama-c/parameter.cmo
+lib/frama-c/parameter.cmx
+lib/frama-c/parameter.o
 lib/frama-c/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
+lib/frama-c/pdgIndex.o
 lib/frama-c/pdgMarks.cmi
+lib/frama-c/pdgMarks.cmo
+lib/frama-c/pdgMarks.cmx
+lib/frama-c/pdgMarks.o
 lib/frama-c/pdgTypes.cmi
+lib/frama-c/pdgTypes.cmo
+lib/frama-c/pdgTypes.cmx
+lib/frama-c/pdgTypes.o
 lib/frama-c/plugin.cmi
-lib/frama-c/plugins/Jessie.cma
-lib/frama-c/plugins/Jessie.cmxs
-lib/frama-c/plugins/Ltl_to_acsl.cmo
-lib/frama-c/plugins/Ltl_to_acsl.cmxs
-lib/frama-c/pretty_source.cmi
+lib/frama-c/plugin.cmo
+lib/frama-c/plugin.cmx
+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/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.cmi
+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.cmi
+${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
+${PLIST.gui}lib/frama-c/pretty_source.cmx
+${PLIST.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
+lib/frama-c/pretty_utils.o
 lib/frama-c/printer.cmi
+lib/frama-c/printer.cmo
+lib/frama-c/printer.cmx
+lib/frama-c/printer.o
+lib/frama-c/printexc_common_interface.cmi
+lib/frama-c/printexc_common_interface.cmo
+lib/frama-c/printexc_common_interface.cmx
+lib/frama-c/printexc_common_interface.o
 lib/frama-c/project.cmi
-lib/frama-c/project_manager.cmi
-lib/frama-c/ptmap.cmi
-lib/frama-c/ptset.cmi
+lib/frama-c/project.cmo
+lib/frama-c/project.cmx
+lib/frama-c/project.o
+${PLIST.gui}lib/frama-c/project_manager.cmi
+${PLIST.gui}lib/frama-c/project_manager.cmo
+${PLIST.gui}lib/frama-c/project_manager.cmx
+${PLIST.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/property.cmi
+lib/frama-c/property.cmo
+lib/frama-c/property.cmx
+lib/frama-c/property.o
+${PLIST.gui}lib/frama-c/property_navigator.cmi
+${PLIST.gui}lib/frama-c/property_navigator.cmo
+${PLIST.gui}lib/frama-c/property_navigator.cmx
+${PLIST.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
+lib/frama-c/qstack.cmx
+lib/frama-c/qstack.o
 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/relations_type.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
+lib/frama-c/rmtmps.o
 lib/frama-c/service_graph.cmi
+lib/frama-c/service_graph.cmo
+lib/frama-c/service_graph.cmx
+lib/frama-c/service_graph.o
 lib/frama-c/setWithNearest.cmi
+lib/frama-c/setWithNearest.cmo
+lib/frama-c/setWithNearest.cmx
+lib/frama-c/setWithNearest.o
 lib/frama-c/shifted_Location.cmi
-lib/frama-c/signature.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
+lib/frama-c/slicingInternals.o
 lib/frama-c/slicingTypes.cmi
-lib/frama-c/source_manager.cmi
-lib/frama-c/source_viewer.cmi
+lib/frama-c/slicingTypes.cmo
+lib/frama-c/slicingTypes.cmx
+lib/frama-c/slicingTypes.o
+${PLIST.gui}lib/frama-c/source_manager.cmi
+${PLIST.gui}lib/frama-c/source_manager.cmo
+${PLIST.gui}lib/frama-c/source_manager.cmx
+${PLIST.gui}lib/frama-c/source_manager.o
+${PLIST.gui}lib/frama-c/source_viewer.cmi
+${PLIST.gui}lib/frama-c/source_viewer.cmo
+${PLIST.gui}lib/frama-c/source_viewer.cmx
+${PLIST.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
+lib/frama-c/special_hooks.o
+lib/frama-c/state.cmi
+lib/frama-c/state.cmo
+lib/frama-c/state.cmx
+lib/frama-c/state.o
+lib/frama-c/state_builder.cmi
+lib/frama-c/state_builder.cmo
+lib/frama-c/state_builder.cmx
+lib/frama-c/state_builder.o
+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/stmts_graph.cmi
+lib/frama-c/stmts_graph.cmo
+lib/frama-c/stmts_graph.cmx
+lib/frama-c/stmts_graph.o
+lib/frama-c/structural_descr.cmi
+lib/frama-c/structural_descr.cmo
+lib/frama-c/structural_descr.cmx
+lib/frama-c/structural_descr.o
 lib/frama-c/subst.cmi
+lib/frama-c/subst.cmo
+lib/frama-c/subst.cmx
+lib/frama-c/subst.o
+lib/frama-c/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
+lib/frama-c/translate_lightweight.o
 lib/frama-c/type.cmi
+lib/frama-c/type.cmo
+lib/frama-c/type.cmx
+lib/frama-c/type.o
 lib/frama-c/unicode.cmi
+lib/frama-c/unicode.cmo
+lib/frama-c/unicode.cmx
+lib/frama-c/unicode.o
 lib/frama-c/unmarshal.cmi
+lib/frama-c/unmarshal.cmo
+lib/frama-c/unmarshal.cmx
+lib/frama-c/unmarshal.o
 lib/frama-c/unmarshal_nums.cmi
+lib/frama-c/unmarshal_nums.cmo
+lib/frama-c/unmarshal_nums.cmx
+lib/frama-c/unmarshal_nums.o
 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
+lib/frama-c/utf8_logic.o
 lib/frama-c/visitor.cmi
-lib/frama-c/warning_manager.cmi
+lib/frama-c/visitor.cmo
+lib/frama-c/visitor.cmx
+lib/frama-c/visitor.o
+${PLIST.gui}lib/frama-c/warning_manager.cmi
+${PLIST.gui}lib/frama-c/warning_manager.cmo
+${PLIST.gui}lib/frama-c/warning_manager.cmx
+${PLIST.gui}lib/frama-c/warning_manager.o
 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/zrapp.cmi
+lib/frama-c/widen_type.cmo
+lib/frama-c/widen_type.cmx
+lib/frama-c/widen_type.o
 man/man1/frama-c-gui.1
 man/man1/frama-c.1
-man/man1/why.1
 share/frama-c/Makefile.common
 share/frama-c/Makefile.config
 share/frama-c/Makefile.dynamic
 share/frama-c/Makefile.dynamic_config
+share/frama-c/Makefile.kernel
 share/frama-c/Makefile.plugin
+share/frama-c/acsl.el
 share/frama-c/builtin.c
 share/frama-c/builtin.h
-share/frama-c/caduceus/coq/caduceus_tactics.v
-share/frama-c/caduceus/coq/caduceus_why.v
-share/frama-c/caduceus/harvey/caduceus_why.rv
-share/frama-c/caduceus/isabelle/caduceus_why.thy
-share/frama-c/caduceus/why/caduceus.why
-share/frama-c/caduceus/why/caduceus_arith.why
-share/frama-c/coq/jessie_why.v
+share/frama-c/check.png
+share/frama-c/configure.ac
+share/frama-c/doc/code/intro_kernel_plugin.txt
+share/frama-c/doc/code/intro_plugin.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
+share/frama-c/feedback/considered_valid.png
+share/frama-c/feedback/inconsistent.png
+share/frama-c/feedback/invalid_but_dead.png
+share/frama-c/feedback/invalid_under_hyp.png
+share/frama-c/feedback/never_tried.png
+share/frama-c/feedback/surely_invalid.png
+share/frama-c/feedback/surely_valid.png
+share/frama-c/feedback/unknown.png
+share/frama-c/feedback/unknown_but_dead.png
+share/frama-c/feedback/valid_but_dead.png
+share/frama-c/feedback/valid_under_hyp.png
 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/jessie/assert.h
-share/frama-c/jessie/ctype.h
-share/frama-c/jessie/jc.cmi
-share/frama-c/jessie/jc.cmo
-share/frama-c/jessie/jc.cmx
-share/frama-c/jessie/jc.o
-share/frama-c/jessie/jc_ast.cmi
-share/frama-c/jessie/jc_common_options.cmi
-share/frama-c/jessie/jc_constructors.cmi
-share/frama-c/jessie/jc_env.cmi
-share/frama-c/jessie/jc_envset.cmi
-share/frama-c/jessie/jc_fenv.cmi
-share/frama-c/jessie/jc_iterators.cmi
-share/frama-c/jessie/jc_noutput.cmi
-share/frama-c/jessie/jc_output.cmi
-share/frama-c/jessie/jc_output_misc.cmi
-share/frama-c/jessie/jc_pervasives.cmi
-share/frama-c/jessie/jc_poutput.cmi
-share/frama-c/jessie/jc_region.cmi
-share/frama-c/jessie/jc_stdlib.cmi
-share/frama-c/jessie/jc_type_var.cmi
-share/frama-c/jessie/jessie_exact_prolog.h
-share/frama-c/jessie/jessie_machine_prolog.h
-share/frama-c/jessie/jessie_prolog.h
-share/frama-c/jessie/lib.cmi
-share/frama-c/jessie/loc.cmi
-share/frama-c/jessie/option_misc.cmi
-share/frama-c/jessie/output.cmi
-share/frama-c/jessie/pp.cmi
-share/frama-c/jessie/prolog.c
-share/frama-c/jessie/rc.cmi
-share/frama-c/jessie/stddef.h
-share/frama-c/jessie/stdio.h
-share/frama-c/jessie/stdlib.h
-share/frama-c/jessie/string.h
-share/frama-c/jessie/strings.h
-share/frama-c/jessie/unistd.h
-share/frama-c/jessie/wchar.h
+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_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_ino_t.h
+share/frama-c/libc/__fc_define_intptr_t.h
+share/frama-c/libc/__fc_define_iovec.h
+share/frama-c/libc/__fc_define_mode_t.h
+share/frama-c/libc/__fc_define_nlink_t.h
+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_size_t.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_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/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.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.h
+share/frama-c/libc/fenv.c
+share/frama-c/libc/fenv.h
+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/iso646.c
+share/frama-c/libc/iso646.h
+share/frama-c/libc/limits.c
+share/frama-c/libc/limits.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/netinet/in.h
+share/frama-c/libc/pwd.h
+share/frama-c/libc/setjmp.c
+share/frama-c/libc/setjmp.h
+share/frama-c/libc/signal.c
+share/frama-c/libc/signal.h
+share/frama-c/libc/stdarg.c
+share/frama-c/libc/stdarg.h
+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.h
+share/frama-c/libc/stdio.c
+share/frama-c/libc/stdio.h
+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/sys/socket.h
+share/frama-c/libc/sys/stat.h
+share/frama-c/libc/sys/time.h
+share/frama-c/libc/sys/types.h
+share/frama-c/libc/sys/uio.h
+share/frama-c/libc/sys/wait.h
+share/frama-c/libc/syslog.h
+share/frama-c/libc/termios.h
+share/frama-c/libc/test.c
+share/frama-c/libc/tgmath.c
+share/frama-c/libc/tgmath.h
+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.h
+share/frama-c/libc/wchar.c
+share/frama-c/libc/wchar.h
+share/frama-c/libc/wctype.c
+share/frama-c/libc/wctype.h
 share/frama-c/machine.h
 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
+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/math.c
 share/frama-c/math.h
-share/frama-c/why/Makefile
-share/frama-c/why/acsl.why
-share/frama-c/why/java_api/java/io/BufferedWriter.java
-share/frama-c/why/java_api/java/io/File.java
-share/frama-c/why/java_api/java/io/FileDescriptor.java
-share/frama-c/why/java_api/java/io/FileNotFoundException.java
-share/frama-c/why/java_api/java/io/FileReader.java
-share/frama-c/why/java_api/java/io/FilterOutputStream.java
-share/frama-c/why/java_api/java/io/IOException.java
-share/frama-c/why/java_api/java/io/InputStream.java
-share/frama-c/why/java_api/java/io/InputStreamReader.java
-share/frama-c/why/java_api/java/io/ObjectStreamClass.java
-share/frama-c/why/java_api/java/io/OutputStream.java
-share/frama-c/why/java_api/java/io/OutputStreamWriter.java
-share/frama-c/why/java_api/java/io/PrintStream.java
-share/frama-c/why/java_api/java/io/Reader.java
-share/frama-c/why/java_api/java/io/Serializable.java
-share/frama-c/why/java_api/java/io/StreamTokenizer.java
-share/frama-c/why/java_api/java/lang/ArrayStoreException.java
-share/frama-c/why/java_api/java/lang/CharSequence.java
-share/frama-c/why/java_api/java/lang/Character.java
-share/frama-c/why/java_api/java/lang/Class.java
-share/frama-c/why/java_api/java/lang/Cloneable.java
-share/frama-c/why/java_api/java/lang/Comparable.java
-share/frama-c/why/java_api/java/lang/Double.java
-share/frama-c/why/java_api/java/lang/Exception.java
-share/frama-c/why/java_api/java/lang/IllegalArgumentException.java
-share/frama-c/why/java_api/java/lang/Integer.java
-share/frama-c/why/java_api/java/lang/Long.java
-share/frama-c/why/java_api/java/lang/Math.java
-share/frama-c/why/java_api/java/lang/Number.java
-share/frama-c/why/java_api/java/lang/NumberFormatException.java
-share/frama-c/why/java_api/java/lang/Object.java
-share/frama-c/why/java_api/java/lang/RuntimeException.java
-share/frama-c/why/java_api/java/lang/String.java
-share/frama-c/why/java_api/java/lang/StringBuffer.java
-share/frama-c/why/java_api/java/lang/System.java
-share/frama-c/why/java_api/java/lang/Throwable.java
-share/frama-c/why/java_api/java/util/AbstractMap.java
-share/frama-c/why/java_api/java/util/Collection.java
-share/frama-c/why/java_api/java/util/HashMap.java
-share/frama-c/why/java_api/java/util/HashMapIntegerInteger.java
-share/frama-c/why/java_api/java/util/HashMapIntegerLong.java
-share/frama-c/why/java_api/java/util/Iterator.java
-share/frama-c/why/java_api/java/util/Locale.java
-share/frama-c/why/java_api/java/util/Map.java
-share/frama-c/why/java_api/java/util/Set.java
-share/frama-c/why/javacard_api/com/sun/javacard/impl/Constants.java
-share/frama-c/why/javacard_api/com/sun/javacard/impl/NativeMethods.java
-share/frama-c/why/javacard_api/com/sun/javacard/impl/PackedBoolean.java
-share/frama-c/why/javacard_api/com/sun/javacard/impl/PrivAccess.java
-share/frama-c/why/javacard_api/java/lang/ArrayIndexOutOfBoundsException.java
-share/frama-c/why/javacard_api/java/lang/Exception.java
-share/frama-c/why/javacard_api/java/lang/IndexOutOfBoundsException.java
-share/frama-c/why/javacard_api/java/lang/Object.java
-share/frama-c/why/javacard_api/java/lang/RuntimeException.java
-share/frama-c/why/javacard_api/java/lang/Throwable.java
-share/frama-c/why/javacard_api/javacard/framework/AID.java
-share/frama-c/why/javacard_api/javacard/framework/APDU.java
-share/frama-c/why/javacard_api/javacard/framework/APDUException.java
-share/frama-c/why/javacard_api/javacard/framework/Applet.java
-share/frama-c/why/javacard_api/javacard/framework/CardException.java
-share/frama-c/why/javacard_api/javacard/framework/CardRuntimeException.java
-share/frama-c/why/javacard_api/javacard/framework/Dispatcher.java
-share/frama-c/why/javacard_api/javacard/framework/ISO7816.java
-share/frama-c/why/javacard_api/javacard/framework/ISOException.java
-share/frama-c/why/javacard_api/javacard/framework/JCSystem.java
-share/frama-c/why/javacard_api/javacard/framework/OwnerPIN.java
-share/frama-c/why/javacard_api/javacard/framework/PIN.java
-share/frama-c/why/javacard_api/javacard/framework/PINException.java
-share/frama-c/why/javacard_api/javacard/framework/Shareable.java
-share/frama-c/why/javacard_api/javacard/framework/SystemException.java
-share/frama-c/why/javacard_api/javacard/framework/TransactionException.java
-share/frama-c/why/javacard_api/javacard/framework/UserException.java
-share/frama-c/why/javacard_api/javacard/framework/Util.java
-share/frama-c/why/javacard_api/javacard/security/CryptoException.java
-share/frama-c/why/javacard_api/javacard/security/DESKey.java
-share/frama-c/why/javacard_api/javacard/security/DSAKey.java
-share/frama-c/why/javacard_api/javacard/security/DSAPrivateKey.java
-share/frama-c/why/javacard_api/javacard/security/DSAPublicKey.java
-share/frama-c/why/javacard_api/javacard/security/Key.java
-share/frama-c/why/javacard_api/javacard/security/KeyBuilder.java
-share/frama-c/why/javacard_api/javacard/security/KeyPair.java
-share/frama-c/why/javacard_api/javacard/security/MessageDigest.java
-share/frama-c/why/javacard_api/javacard/security/PrivateKey.java
-share/frama-c/why/javacard_api/javacard/security/PublicKey.java
-share/frama-c/why/javacard_api/javacard/security/RSAPrivateCrtKey.java
-share/frama-c/why/javacard_api/javacard/security/RSAPrivateKey.java
-share/frama-c/why/javacard_api/javacard/security/RSAPublicKey.java
-share/frama-c/why/javacard_api/javacard/security/RandomData.java
-share/frama-c/why/javacard_api/javacard/security/SecretKey.java
-share/frama-c/why/javacard_api/javacard/security/Signature.java
-share/frama-c/why/javacard_api/javacardx/crypto/Cipher.java
-share/frama-c/why/low-level.why
-share/frama-c/why/model0.why.src
-share/frama-c/why/model1.why.src
-share/frama-c/why/model2.why.src
-share/frama-c/why/test.why
-share/frama-c/why/test_low-level.why.src
-share/frama-c/why/test_model0.why.src
-share/frama-c/why/test_model1.why.src
-share/frama-c/why/test_model2.why.src
-share/frama-c/why/why-logo-1.png
-share/frama-c/why/why/arrays.why
-share/frama-c/why/why/bool.why
-share/frama-c/why/why/floats.why
-share/frama-c/why/why/floats_common.why
-share/frama-c/why/why/floats_full.why
-share/frama-c/why/why/floats_multi_rounding.why
-share/frama-c/why/why/floats_strict.why
-share/frama-c/why/why/integer.why
-share/frama-c/why/why/jessie.why
-share/frama-c/why/why/mix.why
-share/frama-c/why/why/prelude.why
-share/frama-c/why/why/real.why
-share/manuals/acsl-implementation.pdf
-share/manuals/aorai-manual.pdf
-share/manuals/plugin-developer.pdf
-share/manuals/value-analysis.pdf
+share/frama-c/maybe.png
+share/frama-c/right.png
+share/frama-c/unmark.png
+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/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/wp.v
 @pkgdir lib/frama-c/plugins/gui
diff --git a/devel/frama-c/PLIST.gnomecanvas b/devel/frama-c/PLIST.gnomecanvas
deleted file mode 100644
index 4f45f26e077..00000000000
--- a/devel/frama-c/PLIST.gnomecanvas
+++ /dev/null
@@ -1,10 +0,0 @@
-@comment $NetBSD: PLIST.gnomecanvas,v 1.1 2009/12/07 16:39:12 wiz Exp $
-lib/frama-c/concreteModel.cmi
-lib/frama-c/dGraphModel.cmi
-lib/frama-c/dGraphView.cmi
-lib/frama-c/dGraphViewItem.cmi
-lib/frama-c/viewGraph.cmi
-lib/frama-c/viewGraph_select.cmi
-lib/frama-c/viewGraph_utils.cmi
-lib/frama-c/xDot.cmi
-lib/frama-c/xDotDraw.cmi
diff --git a/devel/frama-c/distinfo b/devel/frama-c/distinfo
index d70646ad260..dea5dca9d00 100644
--- a/devel/frama-c/distinfo
+++ b/devel/frama-c/distinfo
@@ -1,7 +1,5 @@
-$NetBSD: distinfo,v 1.2 2010/06/15 08:26:54 wiz Exp $
+$NetBSD: distinfo,v 1.3 2011/12/25 15:52:12 asau Exp $
 
-SHA1 (frama-c-Beryllium-20090901.tar.gz) = 17b1516e9807a9a34ab20a3413efc372549e6fed
-RMD160 (frama-c-Beryllium-20090901.tar.gz) = b29038e948b898196947cae636eef9adbea99ed6
-Size (frama-c-Beryllium-20090901.tar.gz) = 18162700 bytes
-SHA1 (patch-aa) = fbeccfdd1b90c1d72d954d4ea06309da5684f6a4
-SHA1 (patch-ab) = 3f59690f68cfe408cc5dc86adf4c2d66b361eca5
+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
diff --git a/devel/frama-c/options.mk b/devel/frama-c/options.mk
index 4eab8584ac7..e9ee4ac2f6e 100644
--- a/devel/frama-c/options.mk
+++ b/devel/frama-c/options.mk
@@ -1,15 +1,17 @@
-# $NetBSD: options.mk,v 1.2 2009/12/21 12:45:38 joerg Exp $
+# $NetBSD: options.mk,v 1.3 2011/12/25 15:52:12 asau Exp $
 
 PKG_OPTIONS_VAR=	PKG_OPTIONS.frama-c
-PKG_SUPPORTED_OPTIONS=	gnomecanvas
-# actually, depends completely on lablgtk's gnomecanvas option
-# but I didn't manage to check for that.
-PKG_SUGGESTED_OPTIONS=	gnomecanvas
+PKG_SUPPORTED_OPTIONS=	gui
+PKG_SUGGESTED_OPTIONS=	gui
+
+PLIST_VARS=	gui
 
 .include "../../mk/bsd.options.mk"
 
-.if !empty(PKG_OPTIONS:Mgnomecanvas)
-PLIST_SRC+=	PLIST.gnomecanvas
+.if !empty(PKG_OPTIONS:Mgui)
+PLIST.gui=	yes
 
-.include "../../graphics/libgnomecanvas/buildlink3.mk"
+.include "../../x11/gtksourceview2/buildlink3.mk"
+.else
+CONFIGURE_ARGS+=	--enable-gui=no
 .endif
diff --git a/devel/frama-c/patches/patch-aa b/devel/frama-c/patches/patch-aa
deleted file mode 100644
index 0b6102c685a..00000000000
--- a/devel/frama-c/patches/patch-aa
+++ /dev/null
@@ -1,1213 +0,0 @@
-$NetBSD: patch-aa,v 1.1.1.1 2009/09/11 15:09:35 tonio Exp $
-
-Fix sh portability
-
---- configure.orig	2009-09-10 22:50:15.000000000 +0200
-+++ configure
-@@ -2170,7 +2170,7 @@ echo $ECHO_N "ocaml version is $OCAMLVER
- case $OCAMLVERSION in
-   3.0*) echo "${ECHO_T}Incompatible version! Use at least OCaml 3.10.1."; exit 2;;
-   3.10.0) echo "${ECHO_T}Warning: unsupported version." ;
--         if test "$UNSUPPORTED_OCAML" == "yes"; then
-+         if test "$UNSUPPORTED_OCAML" = "yes"; then
-            echo "Compile at your own risks";
-          else
-            echo "If you want to compile Frama-C with this version, use the \
-@@ -2621,7 +2621,7 @@ as_val=`eval 'as_val=${'$as_ac_File'}
- fi
- 
- 
--if test "$OCAMLGRAPH_EXISTS" == "no"; then
-+if test "$OCAMLGRAPH_EXISTS" = "no"; then
-    OCAMLGRAPH_TEST=$OCAMLLIB
-    OCAMLGRAPH=
-    as_ac_File=`$as_echo "ac_cv_file_$OCAMLGRAPH_HOME/graph.$OBJ_SUFFIX" | $as_tr_sh`
-@@ -2653,7 +2653,7 @@ fi
- fi
- 
- # Is the installed version compatible?
--if test "$OCAMLGRAPH_EXISTS" == "yes"; then
-+if test "$OCAMLGRAPH_EXISTS" = "yes"; then
-  test_ocamlgraph_version='print_string Graph.Version.version;;'
-  echo $test_ocamlgraph_version > test_ocamlgraph.ml
-  if ocamlc -o test_ocamlgraph $OCAMLGRAPH graph.cmo test_ocamlgraph.ml 2> /dev/null; then
-@@ -2676,7 +2676,7 @@ fi
- 
- #revert back to local version of ocamlgraph
- 
--if test "$OCAMLGRAPH_EXISTS" == "no"; then
-+if test "$OCAMLGRAPH_EXISTS" = "no"; then
-    { $as_echo "$as_me:$LINENO: Switching to local ocamlgraph" >&5
- $as_echo "$as_me: Switching to local ocamlgraph" >&6;}
-    OCAMLGRAPH_LOCAL=ocamlgraph
-@@ -2711,7 +2711,7 @@ as_val=`eval 'as_val=${'$as_ac_File'}
- fi
- 
- 
--   if test "$OCAMLGRAPH_EXISTS" == "no"; then
-+   if test "$OCAMLGRAPH_EXISTS" = "no"; then
-     { $as_echo "$as_me:$LINENO: checking for ocamlgraph.tar.gz" >&5
- $as_echo_n "checking for ocamlgraph.tar.gz... " >&6; }
- if test "${ac_cv_file_ocamlgraph_tar_gz+set}" = set; then
-@@ -2733,7 +2733,7 @@ if test "x$ac_cv_file_ocamlgraph_tar_gz"
-   OCAMLGRAPH_EXISTS=yes
- fi
- 
--    if test "$OCAMLGRAPH_EXISTS" == "yes"; then
-+    if test "$OCAMLGRAPH_EXISTS" = "yes"; then
-          { $as_echo "$as_me:$LINENO: Unarchiving ocamlgraph.tar.gz" >&5
- $as_echo "$as_me: Unarchiving ocamlgraph.tar.gz" >&6;}
-          tar zxf ocamlgraph.tar.gz
-@@ -2760,7 +2760,7 @@ if test "x$ac_cv_file_ocamlgraph_tar_gz"
-   OCAMLGRAPH_TAR=yes
- fi
- 
--    if test "$OCAMLGRAPH_TAR" == "yes"; then
-+    if test "$OCAMLGRAPH_TAR" = "yes"; then
-      if test ocamlgraph.tar.gz -nt ocamlgraph; then
-        rm -rf ocamlgraph
-        { $as_echo "$as_me:$LINENO: ocamlgraph updated" >&5
-@@ -2770,7 +2770,7 @@ $as_echo "$as_me: ocamlgraph updated" >&
-     fi
-    fi
- 
--   if test "$OCAMLGRAPH_EXISTS" == "no"; then
-+   if test "$OCAMLGRAPH_EXISTS" = "no"; then
-       { { $as_echo "$as_me:$LINENO: error: Cannot find $OCAMLGRAPH_LOCAL in current directory
-       Please download the latest version from http://ocamlgraph.lri.fr/download
-       Compile it in \"ocamlgraph\" then rerun ./configure" >&5
-@@ -5310,7 +5310,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: constant_propagation is not available" >&5
- $as_echo "$as_me: error: constant_propagation is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -5323,7 +5323,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=constant_propagation
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -5332,7 +5332,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} constant_propagation"
-   eval DYNAMIC_$up=yes
- else
-@@ -5404,7 +5404,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: from is not available" >&5
- $as_echo "$as_me: error: from is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -5417,7 +5417,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=from
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -5426,7 +5426,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} from"
-   eval DYNAMIC_$up=yes
- else
-@@ -5498,7 +5498,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: gui is not available" >&5
- $as_echo "$as_me: error: gui is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -5511,7 +5511,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=gui
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -5520,7 +5520,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} gui"
-   eval DYNAMIC_$up=yes
- else
-@@ -5530,7 +5530,7 @@ fi
- echo "gui... $ENABLE"
- 
- 
--if test "$ENABLE_GUI" == "yes"; then
-+if test "$ENABLE_GUI" = "yes"; then
-   REQUIRE_LABLGTK=${REQUIRE_LABLGTK}" gui"
- fi
- 
-@@ -5596,7 +5596,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: impact is not available" >&5
- $as_echo "$as_me: error: impact is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -5609,7 +5609,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=impact
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -5618,7 +5618,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} impact"
-   eval DYNAMIC_$up=yes
- else
-@@ -5690,7 +5690,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: inout is not available" >&5
- $as_echo "$as_me: error: inout is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -5703,7 +5703,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=inout
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -5712,7 +5712,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} inout"
-   eval DYNAMIC_$up=yes
- else
-@@ -5784,7 +5784,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: jessie is not available" >&5
- $as_echo "$as_me: error: jessie is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -5797,7 +5797,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=jessie
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -5815,7 +5815,7 @@ fi
- 
- 
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} jessie"
-   eval DYNAMIC_$up=yes
- else
-@@ -5825,7 +5825,7 @@ fi
- echo "jessie... $ENABLE"
- 
- 
--if test "$ENABLE_JESSIE" == "yes"; then
-+if test "$ENABLE_JESSIE" = "yes"; then
-   REQUIRE_WHYJC=${REQUIRE_WHYJC}" jessie"
-   USE_APRON=${USE_APRON}" jessie"
- fi
-@@ -5892,7 +5892,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: ltl_to_acsl is not available" >&5
- $as_echo "$as_me: error: ltl_to_acsl is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -5905,7 +5905,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=ltl_to_acsl
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -5923,7 +5923,7 @@ fi
- 
- 
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} ltl_to_acsl"
-   eval DYNAMIC_$up=yes
- else
-@@ -5932,7 +5932,7 @@ fi
- 
- echo "ltl_to_acsl... $ENABLE"
- 
--if test "$ENABLE_LTL_TO_ACSL" == "yes"; then
-+if test "$ENABLE_LTL_TO_ACSL" = "yes"; then
-    USE_LTLTOBA=${USE_LTLTOBA}" ltl_to_acsl"
- fi
- 
-@@ -5998,7 +5998,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: metrics is not available" >&5
- $as_echo "$as_me: error: metrics is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -6011,7 +6011,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=metrics
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -6020,7 +6020,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} metrics"
-   eval DYNAMIC_$up=yes
- else
-@@ -6092,7 +6092,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: miel is not available" >&5
- $as_echo "$as_me: error: miel is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -6105,7 +6105,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=miel
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -6114,7 +6114,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} miel"
-   eval DYNAMIC_$up=yes
- else
-@@ -6124,7 +6124,7 @@ fi
- echo "miel... $ENABLE"
- 
- 
--if test "$ENABLE_MIEL" == "yes" -a "$ENABLE_GUI" == "yes"; then
-+if test "$ENABLE_MIEL" = "yes" -a "$ENABLE_GUI" = "yes"; then
-   REQUIRE_LABLGTK=${REQUIRE_LABLGTK}" miel"
-   REQUIRE_LABLGLADECC=${REQUIRE_LABLGLADECC}" miel"
- fi
-@@ -6191,7 +6191,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: occurrence is not available" >&5
- $as_echo "$as_me: error: occurrence is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -6204,7 +6204,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=occurrence
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -6213,7 +6213,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} occurrence"
-   eval DYNAMIC_$up=yes
- else
-@@ -6289,7 +6289,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: pdg is not available" >&5
- $as_echo "$as_me: error: pdg is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -6302,7 +6302,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=pdg
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -6311,7 +6311,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} pdg"
-   eval DYNAMIC_$up=yes
- else
-@@ -6383,7 +6383,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: postdominators is not available" >&5
- $as_echo "$as_me: error: postdominators is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -6396,7 +6396,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=postdominators
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -6405,7 +6405,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} postdominators"
-   eval DYNAMIC_$up=yes
- else
-@@ -6477,7 +6477,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: scope is not available" >&5
- $as_echo "$as_me: error: scope is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -6490,7 +6490,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=scope
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -6499,7 +6499,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} scope"
-   eval DYNAMIC_$up=yes
- else
-@@ -6571,7 +6571,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: security is not available" >&5
- $as_echo "$as_me: error: security is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -6584,7 +6584,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=security
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -6593,7 +6593,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} security"
-   eval DYNAMIC_$up=yes
- else
-@@ -6665,7 +6665,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: semantic_callgraph is not available" >&5
- $as_echo "$as_me: error: semantic_callgraph is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -6678,7 +6678,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=semantic_callgraph
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -6687,7 +6687,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} semantic_callgraph"
-   eval DYNAMIC_$up=yes
- else
-@@ -6759,7 +6759,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: slicing is not available" >&5
- $as_echo "$as_me: error: slicing is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -6772,7 +6772,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=slicing
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -6781,7 +6781,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} slicing"
-   eval DYNAMIC_$up=yes
- else
-@@ -6853,7 +6853,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: sparecode is not available" >&5
- $as_echo "$as_me: error: sparecode is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -6866,7 +6866,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=sparecode
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -6875,7 +6875,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} sparecode"
-   eval DYNAMIC_$up=yes
- else
-@@ -6947,7 +6947,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: syntactic_callgraph is not available" >&5
- $as_echo "$as_me: error: syntactic_callgraph is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -6960,7 +6960,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=syntactic_callgraph
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -6969,7 +6969,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} syntactic_callgraph"
-   eval DYNAMIC_$up=yes
- else
-@@ -6979,7 +6979,7 @@ fi
- echo "syntactic_callgraph... $ENABLE"
- 
- 
--if test "$ENABLE_SYNTACTIC_CALLGRAPH" == "yes"; then
-+if test "$ENABLE_SYNTACTIC_CALLGRAPH" = "yes"; then
-   USE_GNOMECANVAS=${USE_GNOMECANVAS}" syntactic_callgraph"
- fi
- 
-@@ -7045,7 +7045,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: users is not available" >&5
- $as_echo "$as_me: error: users is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -7058,7 +7058,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=users
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -7067,7 +7067,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} users"
-   eval DYNAMIC_$up=yes
- else
-@@ -7139,7 +7139,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: value is not available" >&5
- $as_echo "$as_me: error: value is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -7152,7 +7152,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=value
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -7161,7 +7161,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} value"
-   eval DYNAMIC_$up=yes
- else
-@@ -7233,7 +7233,7 @@ fi
- #)
- #eval ENABLE_DYNAMIC_$up=\$ENABLE
- 
--if test "$plugin_present" == "no" -a "$FORCE" == "yes"; then
-+if test "$plugin_present" = "no" -a "$FORCE" = "yes"; then
-   { { $as_echo "$as_me:$LINENO: error: wp is not available" >&5
- $as_echo "$as_me: error: wp is not available" >&2;}
-    { (exit 1); exit 1; }; }
-@@ -7246,7 +7246,7 @@ PLUGINS_FORCE_LIST=${PLUGINS_FORCE_LIST}
- eval ENABLE_$up=\$ENABLE
- eval NAME_$up=wp
- 
--if test "$default" == "no" -a "$FORCE" == "no"; then
-+if test "$default" = "no" -a "$FORCE" = "no"; then
-   # [JS 2009/03/27] don't know why that doesn't work in one single line
-   tmp=" (not available by default)"
-   eval INFO_$up=\$tmp
-@@ -7255,7 +7255,7 @@ fi
- # Dynamic plug-ins configuration
- is_static=yes
- 
--if test "$is_static" == "no"; then
-+if test "$is_static" = "no"; then
-   USE_NATIVE_DYNLINK="${USE_NATIVE_DYNLINK} wp"
-   eval DYNAMIC_$up=yes
- else
-@@ -7265,7 +7265,7 @@ fi
- echo "wp... $ENABLE"
- 
- 
--if test "$ENABLE_WP" == "yes"; then
-+if test "$ENABLE_WP" = "yes"; then
-   USE_ALTERGO=${USE_ALTERGO}" wp"
-   USE_WHY=${USE_WHY}" wp"
- fi
-@@ -7278,7 +7278,7 @@ EXTRA_EXTERNAL_PLUGINS=
- 
- # Check whether --enable-external was given.
- if test "${enable_external+set}" = set; then
--  enableval=$enable_external; if test "$enableval" == "yes" || test "$enableval" == "no"; then
-+  enableval=$enable_external; if test "$enableval" = "yes" || test "$enableval" = "no"; then
-     { { $as_echo "$as_me:$LINENO: error: --enable-external expects a directory as argument" >&5
- $as_echo "$as_me: error: --enable-external expects a directory as argument" >&2;}
-    { (exit 1); exit 1; }; };
-@@ -7629,11 +7629,11 @@ USE_GTKSOURCEVIEW=
- HAS_GTKSOURCEVIEW=
- FORCE_GTKSOURCEVIEW="yes"
- 
--if test "$FORCE_GTKSOURCEVIEW" == "yes"; then
-+if test "$FORCE_GTKSOURCEVIEW" = "yes"; then
-   REQUIRE_GTKSOURCEVIEW="$REQUIRE_LABLGTK"
-   USE_GTKSOURCEVIEW="$USE_LABLGTK"
- else
--  if test "$has" == "yes"; then
-+  if test "$has" = "yes"; then
-     USE_GTKSOURCEVIEW="$REQUIRE_LABLGTK$USE_LABLGTK"
-   fi
- fi
-@@ -7726,7 +7726,7 @@ fi
- 
- 
- 
--  if test -n "$REQUIRE_LABLGLADECC" -o -n "$USE_LABLGLADECC" -o "$no" == "yes"; then
-+  if test -n "$REQUIRE_LABLGLADECC" -o -n "$USE_LABLGLADECC" -o "$no" = "yes"; then
-     for file in lablgladecc2; do
-      HAS_LABLGLADECC=
-     # Extract the first word of "$file", so it can be a program name with args.
-@@ -7767,9 +7767,9 @@ $as_echo "no" >&6; }
- fi
- 
- 
--      if test "$HAS_LABLGLADECC" == "yes"; then SELECTED_VAR=$file break; fi
-+      if test "$HAS_LABLGLADECC" = "yes"; then SELECTED_VAR=$file break; fi
-       done
--    if test "$HAS_LABLGLADECC" == "no"; then
-+    if test "$HAS_LABLGLADECC" = "no"; then
-       { $as_echo "$as_me:$LINENO: WARNING: lablgladecc2 not found." >&5
- $as_echo "$as_me: WARNING: lablgladecc2 not found." >&2;}
-       if test "$REQUIRE_LABLGLADECC" != ""; then
-@@ -7777,7 +7777,7 @@ $as_echo "$as_me: WARNING: lablgladecc2 
-  $REQUIRE_LABLGLADECC"
-         for p in $REQUIRE_LABLGLADECC; do
- 	  fp=FORCE_`upper "$p"`
--	  if eval test "\$$fp" == "yes"; then
-+	  if eval test "\$$fp" = "yes"; then
- 	    { { $as_echo "$as_me:$LINENO: error: $p requested but lablgladecc2 missing." >&5
- $as_echo "$as_me: error: $p requested but lablgladecc2 missing." >&2;}
-    { (exit 1); exit 1; }; }
-@@ -7819,7 +7819,7 @@ $as_echo "$as_me: error: $p requested bu
- 
- 
- 
--  if test -n "$REQUIRE_LTLTOBA" -o -n "$USE_LTLTOBA" -o "$no" == "yes"; then
-+  if test -n "$REQUIRE_LTLTOBA" -o -n "$USE_LTLTOBA" -o "$no" = "yes"; then
-     for file in ltl2ba; do
-      HAS_LTLTOBA=
-     # Extract the first word of "$file", so it can be a program name with args.
-@@ -7860,9 +7860,9 @@ $as_echo "no" >&6; }
- fi
- 
- 
--      if test "$HAS_LTLTOBA" == "yes"; then SELECTED_VAR=$file break; fi
-+      if test "$HAS_LTLTOBA" = "yes"; then SELECTED_VAR=$file break; fi
-       done
--    if test "$HAS_LTLTOBA" == "no"; then
-+    if test "$HAS_LTLTOBA" = "no"; then
-       { $as_echo "$as_me:$LINENO: WARNING: ltl2ba not found." >&5
- $as_echo "$as_me: WARNING: ltl2ba not found." >&2;}
-       if test "$REQUIRE_LTLTOBA" != ""; then
-@@ -7870,7 +7870,7 @@ $as_echo "$as_me: WARNING: ltl2ba not fo
-  $REQUIRE_LTLTOBA"
-         for p in $REQUIRE_LTLTOBA; do
- 	  fp=FORCE_`upper "$p"`
--	  if eval test "\$$fp" == "yes"; then
-+	  if eval test "\$$fp" = "yes"; then
- 	    { { $as_echo "$as_me:$LINENO: error: $p requested but ltl2ba missing." >&5
- $as_echo "$as_me: error: $p requested but ltl2ba missing." >&2;}
-    { (exit 1); exit 1; }; }
-@@ -7915,7 +7915,7 @@ $as_echo "$as_me: error: $p requested bu
- # [JS 2009/06/02] sh tests and m4 variables do not mix well together.
- # It works by chance but it is not robust enough.
- # Should be rewritten
--  if test -n "$REQUIRE_LABLGTK" -o -n "$USE_LABLGTK" -o "no" == "yes"; then
-+  if test -n "$REQUIRE_LABLGTK" -o -n "$USE_LABLGTK" -o "no" = "yes"; then
-     HAS_LABLGTK=no
-     if test "$HAS_LABLGTK" != "yes"; then
-           as_ac_File=`$as_echo "ac_cv_file_$OCAMLLIB/lablgtk2/lablgtk.$LIB_SUFFIX" | $as_tr_sh`
-@@ -7946,11 +7946,11 @@ else
-   HAS_LABLGTK=no
- fi
- 
--          if test "$HAS_LABLGTK" == "yes"; then SELECTED_LABLGTK=$OCAMLLIB/lablgtk2/lablgtk.$LIB_SUFFIX
-+          if test "$HAS_LABLGTK" = "yes"; then SELECTED_LABLGTK=$OCAMLLIB/lablgtk2/lablgtk.$LIB_SUFFIX
-           fi
-        fi
- 
--    if test "$HAS_LABLGTK" == "no"; then
-+    if test "$HAS_LABLGTK" = "no"; then
-       { $as_echo "$as_me:$LINENO: WARNING: lablgtk2/lablgtk.$LIB_SUFFIX not found." >&5
- $as_echo "$as_me: WARNING: lablgtk2/lablgtk.$LIB_SUFFIX not found." >&2;}
-       if test "$REQUIRE_LABLGTK" != ""; then
-@@ -7958,7 +7958,7 @@ $as_echo "$as_me: WARNING: lablgtk2/labl
-  $REQUIRE_LABLGTK"
-         for p in $REQUIRE_LABLGTK; do
- 	  fp=FORCE_`upper "$p"`
--	  if eval test "\$$fp" == "yes"; then
-+	  if eval test "\$$fp" = "yes"; then
- 	    { { $as_echo "$as_me:$LINENO: error: $p requested but $OCAMLLIB/lablgtk2/lablgtk.$LIB_SUFFIX missing." >&5
- $as_echo "$as_me: error: $p requested but $OCAMLLIB/lablgtk2/lablgtk.$LIB_SUFFIX missing." >&2;}
-    { (exit 1); exit 1; }; }
-@@ -8002,7 +8002,7 @@ $as_echo "$as_me: error: $p requested bu
- # [JS 2009/06/02] sh tests and m4 variables do not mix well together.
- # It works by chance but it is not robust enough.
- # Should be rewritten
--  if test -n "$REQUIRE_GTKSOURCEVIEW" -o -n "$USE_GTKSOURCEVIEW" -o "no" == "yes"; then
-+  if test -n "$REQUIRE_GTKSOURCEVIEW" -o -n "$USE_GTKSOURCEVIEW" -o "no" = "yes"; then
-     HAS_GTKSOURCEVIEW=no
-     if test "$HAS_GTKSOURCEVIEW" != "yes"; then
-           as_ac_File=`$as_echo "ac_cv_file_$OCAMLLIB/lablgtk2/lablgtksourceview.$LIB_SUFFIX" | $as_tr_sh`
-@@ -8033,7 +8033,7 @@ else
-   HAS_GTKSOURCEVIEW=no
- fi
- 
--          if test "$HAS_GTKSOURCEVIEW" == "yes"; then SELECTED_GTKSOURCEVIEW=$OCAMLLIB/lablgtk2/lablgtksourceview.$LIB_SUFFIX
-+          if test "$HAS_GTKSOURCEVIEW" = "yes"; then SELECTED_GTKSOURCEVIEW=$OCAMLLIB/lablgtk2/lablgtksourceview.$LIB_SUFFIX
-           fi
-        fi
-        if test "$HAS_GTKSOURCEVIEW" != "yes"; then
-@@ -8065,11 +8065,11 @@ else
-   HAS_GTKSOURCEVIEW=no
- fi
- 
--          if test "$HAS_GTKSOURCEVIEW" == "yes"; then SELECTED_GTKSOURCEVIEW=$OCAMLLIB/lablgtksourceview/lablgtksourceview.$LIB_SUFFIX
-+          if test "$HAS_GTKSOURCEVIEW" = "yes"; then SELECTED_GTKSOURCEVIEW=$OCAMLLIB/lablgtksourceview/lablgtksourceview.$LIB_SUFFIX
-           fi
-        fi
- 
--    if test "$HAS_GTKSOURCEVIEW" == "no"; then
-+    if test "$HAS_GTKSOURCEVIEW" = "no"; then
-       { $as_echo "$as_me:$LINENO: WARNING: lablgtksourceview.$LIB_SUFFIX not found" >&5
- $as_echo "$as_me: WARNING: lablgtksourceview.$LIB_SUFFIX not found" >&2;}
-       if test "$REQUIRE_GTKSOURCEVIEW" != ""; then
-@@ -8077,7 +8077,7 @@ $as_echo "$as_me: WARNING: lablgtksource
-  $REQUIRE_GTKSOURCEVIEW"
-         for p in $REQUIRE_GTKSOURCEVIEW; do
- 	  fp=FORCE_`upper "$p"`
--	  if eval test "\$$fp" == "yes"; then
-+	  if eval test "\$$fp" = "yes"; then
- 	    { { $as_echo "$as_me:$LINENO: error: $p requested but $OCAMLLIB/lablgtk2/lablgtksourceview.$LIB_SUFFIX" >&5
- $as_echo "$as_me: error: $p requested but $OCAMLLIB/lablgtk2/lablgtksourceview.$LIB_SUFFIX" >&2;}
-    { (exit $OCAMLLIB/lablgtksourceview/lablgtksourceview.$LIB_SUFFIX missing.); exit $OCAMLLIB/lablgtksourceview/lablgtksourceview.$LIB_SUFFIX missing.; }; }
-@@ -8121,7 +8121,7 @@ $as_echo "$as_me: error: $p requested bu
- # [JS 2009/06/02] sh tests and m4 variables do not mix well together.
- # It works by chance but it is not robust enough.
- # Should be rewritten
--  if test -n "$REQUIRE_GNOMECANVAS" -o -n "$USE_GNOMECANVAS" -o "" == "yes"; then
-+  if test -n "$REQUIRE_GNOMECANVAS" -o -n "$USE_GNOMECANVAS" -o "" = "yes"; then
-     HAS_GNOMECANVAS=no
-     if test "$HAS_GNOMECANVAS" != "yes"; then
-           as_ac_File=`$as_echo "ac_cv_file_$OCAMLLIB/lablgtk2/lablgnomecanvas.$LIB_SUFFIX" | $as_tr_sh`
-@@ -8152,11 +8152,11 @@ else
-   HAS_GNOMECANVAS=no
- fi
- 
--          if test "$HAS_GNOMECANVAS" == "yes"; then SELECTED_GNOMECANVAS=$OCAMLLIB/lablgtk2/lablgnomecanvas.$LIB_SUFFIX
-+          if test "$HAS_GNOMECANVAS" = "yes"; then SELECTED_GNOMECANVAS=$OCAMLLIB/lablgtk2/lablgnomecanvas.$LIB_SUFFIX
-           fi
-        fi
- 
--    if test "$HAS_GNOMECANVAS" == "no"; then
-+    if test "$HAS_GNOMECANVAS" = "no"; then
-       { $as_echo "$as_me:$LINENO: WARNING: lablgnomecanvas.$LIB_SUFFIX not found" >&5
- $as_echo "$as_me: WARNING: lablgnomecanvas.$LIB_SUFFIX not found" >&2;}
-       if test "$REQUIRE_GNOMECANVAS" != ""; then
-@@ -8164,7 +8164,7 @@ $as_echo "$as_me: WARNING: lablgnomecanv
-  $REQUIRE_GNOMECANVAS"
-         for p in $REQUIRE_GNOMECANVAS; do
- 	  fp=FORCE_`upper "$p"`
--	  if eval test "\$$fp" == "yes"; then
-+	  if eval test "\$$fp" = "yes"; then
- 	    { { $as_echo "$as_me:$LINENO: error: $p requested but $OCAMLLIB/lablgtk2/lablgnomecanvas.$LIB_SUFFIX missing." >&5
- $as_echo "$as_me: error: $p requested but $OCAMLLIB/lablgtk2/lablgnomecanvas.$LIB_SUFFIX missing." >&2;}
-    { (exit 1); exit 1; }; }
-@@ -8208,7 +8208,7 @@ $as_echo "$as_me: error: $p requested bu
- # [JS 2009/06/02] sh tests and m4 variables do not mix well together.
- # It works by chance but it is not robust enough.
- # Should be rewritten
--  if test -n "$REQUIRE_APRON" -o -n "$USE_APRON" -o "" == "yes"; then
-+  if test -n "$REQUIRE_APRON" -o -n "$USE_APRON" -o "" = "yes"; then
-     HAS_APRON=no
-     if test "$HAS_APRON" != "yes"; then
-           { $as_echo "$as_me:$LINENO: checking for /usr/local/lib/apron.a" >&5
-@@ -8234,7 +8234,7 @@ else
-   HAS_APRON=no
- fi
- 
--          if test "$HAS_APRON" == "yes"; then SELECTED_APRON=/usr/local/lib/apron.a
-+          if test "$HAS_APRON" = "yes"; then SELECTED_APRON=/usr/local/lib/apron.a
-           fi
-        fi
-        if test "$HAS_APRON" != "yes"; then
-@@ -8261,11 +8261,11 @@ else
-   HAS_APRON=no
- fi
- 
--          if test "$HAS_APRON" == "yes"; then SELECTED_APRON=/usr/lib/apron.a
-+          if test "$HAS_APRON" = "yes"; then SELECTED_APRON=/usr/lib/apron.a
-           fi
-        fi
- 
--    if test "$HAS_APRON" == "no"; then
-+    if test "$HAS_APRON" = "no"; then
-       { $as_echo "$as_me:$LINENO: WARNING: apron not found" >&5
- $as_echo "$as_me: WARNING: apron not found" >&2;}
-       if test "$REQUIRE_APRON" != ""; then
-@@ -8273,7 +8273,7 @@ $as_echo "$as_me: WARNING: apron not fou
-  $REQUIRE_APRON"
-         for p in $REQUIRE_APRON; do
- 	  fp=FORCE_`upper "$p"`
--	  if eval test "\$$fp" == "yes"; then
-+	  if eval test "\$$fp" = "yes"; then
- 	    { { $as_echo "$as_me:$LINENO: error: $p requested but /usr/local/lib/apron.a" >&5
- $as_echo "$as_me: error: $p requested but /usr/local/lib/apron.a" >&2;}
-    { (exit /usr/lib/apron.a missing.); exit /usr/lib/apron.a missing.; }; }
-@@ -8314,7 +8314,7 @@ $as_echo "$as_me: error: $p requested bu
- 
- 
- 
--  if test -n "$REQUIRE_WHY" -o -n "$USE_WHY" -o "$no" == "yes"; then
-+  if test -n "$REQUIRE_WHY" -o -n "$USE_WHY" -o "$no" = "yes"; then
-     for FILE_APRON in why; do
-      HAS_WHY=
-     # Extract the first word of "$FILE_APRON", so it can be a program name with args.
-@@ -8355,9 +8355,9 @@ $as_echo "no" >&6; }
- fi
- 
- 
--      if test "$HAS_WHY" == "yes"; then SELECTED_VAR=$FILE_APRON break; fi
-+      if test "$HAS_WHY" = "yes"; then SELECTED_VAR=$FILE_APRON break; fi
-       done
--    if test "$HAS_WHY" == "no"; then
-+    if test "$HAS_WHY" = "no"; then
-       { $as_echo "$as_me:$LINENO: WARNING: why not found" >&5
- $as_echo "$as_me: WARNING: why not found" >&2;}
-       if test "$REQUIRE_WHY" != ""; then
-@@ -8365,7 +8365,7 @@ $as_echo "$as_me: WARNING: why not found
-  $REQUIRE_WHY"
-         for p in $REQUIRE_WHY; do
- 	  fp=FORCE_`upper "$p"`
--	  if eval test "\$$fp" == "yes"; then
-+	  if eval test "\$$fp" = "yes"; then
- 	    { { $as_echo "$as_me:$LINENO: error: $p requested but why missing." >&5
- $as_echo "$as_me: error: $p requested but why missing." >&2;}
-    { (exit 1); exit 1; }; }
-@@ -8410,7 +8410,7 @@ $as_echo "$as_me: error: $p requested bu
- # [JS 2009/06/02] sh tests and m4 variables do not mix well together.
- # It works by chance but it is not robust enough.
- # Should be rewritten
--  if test -n "$REQUIRE_WHYJC" -o -n "$USE_WHYJC" -o "no" == "yes"; then
-+  if test -n "$REQUIRE_WHYJC" -o -n "$USE_WHYJC" -o "no" = "yes"; then
-     HAS_WHYJC=no
-     if test "$HAS_WHYJC" != "yes"; then
-           as_ac_File=`$as_echo "ac_cv_file_$WHYDISTRIB/jc" | $as_tr_sh`
-@@ -8441,7 +8441,7 @@ else
-   HAS_WHYJC=no
- fi
- 
--          if test "$HAS_WHYJC" == "yes"; then SELECTED_WHYJC=$WHYDISTRIB/jc
-+          if test "$HAS_WHYJC" = "yes"; then SELECTED_WHYJC=$WHYDISTRIB/jc
-           fi
-        fi
-        if test "$HAS_WHYJC" != "yes"; then
-@@ -8473,11 +8473,11 @@ else
-   HAS_WHYJC=no
- fi
- 
--          if test "$HAS_WHYJC" == "yes"; then SELECTED_WHYJC=$OCAMLLIB/jessie/jc.$OBJ_SUFFIX
-+          if test "$HAS_WHYJC" = "yes"; then SELECTED_WHYJC=$OCAMLLIB/jessie/jc.$OBJ_SUFFIX
-           fi
-        fi
- 
--    if test "$HAS_WHYJC" == "no"; then
-+    if test "$HAS_WHYJC" = "no"; then
-       { $as_echo "$as_me:$LINENO: WARNING: jc not found" >&5
- $as_echo "$as_me: WARNING: jc not found" >&2;}
-       if test "$REQUIRE_WHYJC" != ""; then
-@@ -8485,7 +8485,7 @@ $as_echo "$as_me: WARNING: jc not found"
-  $REQUIRE_WHYJC"
-         for p in $REQUIRE_WHYJC; do
- 	  fp=FORCE_`upper "$p"`
--	  if eval test "\$$fp" == "yes"; then
-+	  if eval test "\$$fp" = "yes"; then
- 	    { { $as_echo "$as_me:$LINENO: error: $p requested but $WHYDISTRIB/jc" >&5
- $as_echo "$as_me: error: $p requested but $WHYDISTRIB/jc" >&2;}
-    { (exit $OCAMLLIB/jessie/jc.$OBJ_SUFFIX missing.); exit $OCAMLLIB/jessie/jc.$OBJ_SUFFIX missing.; }; }
-@@ -8529,7 +8529,7 @@ $as_echo "$as_me: error: $p requested bu
- # [JS 2009/06/02] sh tests and m4 variables do not mix well together.
- # It works by chance but it is not robust enough.
- # Should be rewritten
--  if test -n "$REQUIRE_NATIVE_DYNLINK" -o -n "$USE_NATIVE_DYNLINK" -o "yes" == "yes"; then
-+  if test -n "$REQUIRE_NATIVE_DYNLINK" -o -n "$USE_NATIVE_DYNLINK" -o "yes" = "yes"; then
-     HAS_NATIVE_DYNLINK=no
-     if test "$HAS_NATIVE_DYNLINK" != "yes"; then
-           as_ac_File=`$as_echo "ac_cv_file_$OCAMLLIB/dynlink.cmxa" | $as_tr_sh`
-@@ -8560,11 +8560,11 @@ else
-   HAS_NATIVE_DYNLINK=no
- fi
- 
--          if test "$HAS_NATIVE_DYNLINK" == "yes"; then SELECTED_NATIVE_DYNLINK=$OCAMLLIB/dynlink.cmxa
-+          if test "$HAS_NATIVE_DYNLINK" = "yes"; then SELECTED_NATIVE_DYNLINK=$OCAMLLIB/dynlink.cmxa
-           fi
-        fi
- 
--    if test "$HAS_NATIVE_DYNLINK" == "no"; then
-+    if test "$HAS_NATIVE_DYNLINK" = "no"; then
-       { $as_echo "$as_me:$LINENO: WARNING: native dynlink unavailable (ocaml 3.11 or higher required)" >&5
- $as_echo "$as_me: WARNING: native dynlink unavailable (ocaml 3.11 or higher required)" >&2;}
-       if test "$REQUIRE_NATIVE_DYNLINK" != ""; then
-@@ -8572,7 +8572,7 @@ $as_echo "$as_me: WARNING: native dynlin
-  $REQUIRE_NATIVE_DYNLINK"
-         for p in $REQUIRE_NATIVE_DYNLINK; do
- 	  fp=FORCE_`upper "$p"`
--	  if eval test "\$$fp" == "yes"; then
-+	  if eval test "\$$fp" = "yes"; then
- 	    { { $as_echo "$as_me:$LINENO: error: $p requested but $OCAMLLIB/dynlink.cmxa missing." >&5
- $as_echo "$as_me: error: $p requested but $OCAMLLIB/dynlink.cmxa missing." >&2;}
-    { (exit 1); exit 1; }; }
-@@ -8613,7 +8613,7 @@ $as_echo "$as_me: error: $p requested bu
- 
- 
- 
--  if test -n "$REQUIRE_ALTERGO" -o -n "$USE_ALTERGO" -o "$no" == "yes"; then
-+  if test -n "$REQUIRE_ALTERGO" -o -n "$USE_ALTERGO" -o "$no" = "yes"; then
-     for FILE_NATIVE_DYNLINK in alt-ergo; do
-      HAS_ALTERGO=
-     # Extract the first word of "$FILE_NATIVE_DYNLINK", so it can be a program name with args.
-@@ -8654,9 +8654,9 @@ $as_echo "no" >&6; }
- fi
- 
- 
--      if test "$HAS_ALTERGO" == "yes"; then SELECTED_VAR=$FILE_NATIVE_DYNLINK break; fi
-+      if test "$HAS_ALTERGO" = "yes"; then SELECTED_VAR=$FILE_NATIVE_DYNLINK break; fi
-       done
--    if test "$HAS_ALTERGO" == "no"; then
-+    if test "$HAS_ALTERGO" = "no"; then
-       { $as_echo "$as_me:$LINENO: WARNING: alt-ergo not found" >&5
- $as_echo "$as_me: WARNING: alt-ergo not found" >&2;}
-       if test "$REQUIRE_ALTERGO" != ""; then
-@@ -8664,7 +8664,7 @@ $as_echo "$as_me: WARNING: alt-ergo not 
-  $REQUIRE_ALTERGO"
-         for p in $REQUIRE_ALTERGO; do
- 	  fp=FORCE_`upper "$p"`
--	  if eval test "\$$fp" == "yes"; then
-+	  if eval test "\$$fp" = "yes"; then
- 	    { { $as_echo "$as_me:$LINENO: error: $p requested but alt-ergo missing." >&5
- $as_echo "$as_me: error: $p requested but alt-ergo missing." >&2;}
-    { (exit 1); exit 1; }; }
-@@ -8702,13 +8702,13 @@ $as_echo "$as_me: error: $p requested bu
- # Why
- #####
- 
--if test "$HAS_WHY" == "yes"; then
-+if test "$HAS_WHY" = "yes"; then
-    rm -f tests/wp/test_config_dev
-    cp tests/wp/test_config_dev.system_why tests/wp/test_config_dev
-    chmod a-w  tests/wp/test_config_dev
- fi
- 
--if test "$HAS_WHYJC" == "yes" -a "$REQUIRE_WHYJC" != ""; then
-+if test "$HAS_WHYJC" = "yes" -a "$REQUIRE_WHYJC" != ""; then
-   case $SELECTED_WHYJC in
-   $WHYDISTRIB/jc)
-     WHYBIN=$WHYDISTRIB/bin/why.opt
-@@ -8723,7 +8723,7 @@ if test "$HAS_WHYJC" == "yes" -a "$REQUI
-     # for fresh cvs checkout of why...
-     if test ! -r $WHYDISTRIB/configure; then (cd $WHYDISTRIB && autoconf); fi
-     if test ! -d $WHYDISTRIB/ocamlgraph -a "$OCAMLGRAPH_LOCAL" != ""; then
--      if test "$OCAMLGRAPH_TAR" == "yes"; then
-+      if test "$OCAMLGRAPH_TAR" = "yes"; then
-        (cd $WHYDISTRIB && tar -xzf ../ocamlgraph.tar.gz);
-       else
-        { $as_echo "$as_me:$LINENO: WARNING: No ocamlgraph available. Why configuration might fail" >&5
-@@ -8739,12 +8739,12 @@ $as_echo "$as_me: WARNING: No ocamlgraph
-       --exec_prefix=$exec_prefix --bindir=$bindir --libdir=$datadir/frama-c \
-       --host=$host --build=$build --mandir=$mandir --enable-apron=$HAS_APRON) || ENABLE_JESSIE=no
-     fi
--    if test "$ENABLE_JESSIE" == "no"; then
-+    if test "$ENABLE_JESSIE" = "no"; then
-        INFO_JESSIE=" (configuration of Why failed)"
-        # wp can still attempt to use system why if it exists.
-        JESSIE_LOCAL=no
-        rm -f tests/wp/test_config_dev
--       if test "$HAS_WHY" == "yes"; then
-+       if test "$HAS_WHY" = "yes"; then
-          cp tests/wp/test_config_dev.system_why tests/wp/test_config_dev
-          chmod a-w  tests/wp/test_config_dev
-        fi
-@@ -8776,7 +8776,7 @@ fi
- # Usable native dynlink
- 
- # Checking internal invariant
--if test "$HAS_NATIVE_DYNLINK" == "uncheck"; then
-+if test "$HAS_NATIVE_DYNLINK" = "uncheck"; then
-    { { $as_echo "$as_me:$LINENO: error: Internal error with check of native dynlink. Please report." >&5
- $as_echo "$as_me: error: Internal error with check of native dynlink. Please report." >&2;}
-    { (exit 1); exit 1; }; }
-@@ -8814,7 +8814,7 @@ if test "$HAS_NATIVE_DYNLINK" != "no" ; 
- # [JS 2009/06/02] sh tests and m4 variables do not mix well together.
- # It works by chance but it is not robust enough.
- # Should be rewritten
--  if test -n "$REQUIRE_USABLE_NATIVE_DYNLINK" -o -n "$USE_USABLE_NATIVE_DYNLINK" -o "yes" == "yes"; then
-+  if test -n "$REQUIRE_USABLE_NATIVE_DYNLINK" -o -n "$USE_USABLE_NATIVE_DYNLINK" -o "yes" = "yes"; then
-     HAS_USABLE_NATIVE_DYNLINK=no
-     if test "$HAS_USABLE_NATIVE_DYNLINK" != "yes"; then
-           { $as_echo "$as_me:$LINENO: checking for dynlink" >&5
-@@ -8840,11 +8840,11 @@ else
-   HAS_USABLE_NATIVE_DYNLINK=no
- fi
- 
--          if test "$HAS_USABLE_NATIVE_DYNLINK" == "yes"; then SELECTED_USABLE_NATIVE_DYNLINK=dynlink
-+          if test "$HAS_USABLE_NATIVE_DYNLINK" = "yes"; then SELECTED_USABLE_NATIVE_DYNLINK=dynlink
-           fi
-        fi
- 
--    if test "$HAS_USABLE_NATIVE_DYNLINK" == "no"; then
-+    if test "$HAS_USABLE_NATIVE_DYNLINK" = "no"; then
-       { $as_echo "$as_me:$LINENO: WARNING: native dynlink unsupported on this platform" >&5
- $as_echo "$as_me: WARNING: native dynlink unsupported on this platform" >&2;}
-       if test "$REQUIRE_USABLE_NATIVE_DYNLINK" != ""; then
-@@ -8852,7 +8852,7 @@ $as_echo "$as_me: WARNING: native dynlin
-  $REQUIRE_USABLE_NATIVE_DYNLINK"
-         for p in $REQUIRE_USABLE_NATIVE_DYNLINK; do
- 	  fp=FORCE_`upper "$p"`
--	  if eval test "\$$fp" == "yes"; then
-+	  if eval test "\$$fp" = "yes"; then
- 	    { { $as_echo "$as_me:$LINENO: error: $p requested but dynlink missing." >&5
- $as_echo "$as_me: error: $p requested but dynlink missing." >&2;}
-    { (exit 1); exit 1; }; }
-@@ -8891,7 +8891,7 @@ fi
- 
- # Lablgtk2's custom tree model
- 
--if test "$HAS_LABLGTK" == "yes"; then
-+if test "$HAS_LABLGTK" = "yes"; then
-   if echo "type ('a,'b,'c,'d) t = ('a,'b,'c,'d) GTree.custom_tree_model" > test_custommodel.ml && ocamlc -c -I +lablgtk2 test_custommodel.ml 2> /dev/null; \
-   then
-     { $as_echo "$as_me:$LINENO: checking for lablgtk2's custom tree model" >&5
-@@ -8921,7 +8921,7 @@ $as_echo "yes" >&6; }
- # It works by chance but it is not robust enough.
- # Should be rewritten
-   if test -n "$REQUIRE_LABLGTK" -o -n "$USE_LABLGTK" -o "yes
--    " == "yes"; then
-+    " = "yes"; then
-     HAS_LABLGTK=no
-     if test "$HAS_LABLGTK" != "yes"; then
-           { $as_echo "$as_me:$LINENO: checking for custom-tree-model" >&5
-@@ -8947,11 +8947,11 @@ else
-   HAS_LABLGTK=no
- fi
- 
--          if test "$HAS_LABLGTK" == "yes"; then SELECTED_LABLGTK=custom-tree-model
-+          if test "$HAS_LABLGTK" = "yes"; then SELECTED_LABLGTK=custom-tree-model
-           fi
-        fi
- 
--    if test "$HAS_LABLGTK" == "no"; then
-+    if test "$HAS_LABLGTK" = "no"; then
-       { $as_echo "$as_me:$LINENO: WARNING: lablgtk2's custom tree model unavailable. You need at least LablGtk 2.12." >&5
- $as_echo "$as_me: WARNING: lablgtk2's custom tree model unavailable. You need at least LablGtk 2.12." >&2;}
-       if test "$REQUIRE_LABLGTK" != ""; then
-@@ -8959,7 +8959,7 @@ $as_echo "$as_me: WARNING: lablgtk2's cu
-  $REQUIRE_LABLGTK"
-         for p in $REQUIRE_LABLGTK; do
- 	  fp=FORCE_`upper "$p"`
--	  if eval test "\$$fp" == "yes"; then
-+	  if eval test "\$$fp" = "yes"; then
- 	    { { $as_echo "$as_me:$LINENO: error: $p requested but custom-tree-model missing." >&5
- $as_echo "$as_me: error: $p requested but custom-tree-model missing." >&2;}
-    { (exit 1); exit 1; }; }
-@@ -9074,9 +9074,9 @@ check_and_propagate () {
-       short_mark=`echo $2 | sed -e 's/ .*//'`
-       lp=`lower $p`
-       reason=`echo $2 | sed -e 's/no (\(.*\))/\1/' `
--      if test "$short_mark" == "no"; then
-+      if test "$short_mark" = "no"; then
-         fp=FORCE_"$up"
--        if eval test "\$$fp" == "yes"; then
-+        if eval test "\$$fp" = "yes"; then
- 	  { { $as_echo "$as_me:$LINENO: error: $lp requested but $reason." >&5
- $as_echo "$as_me: error: $lp requested but $reason." >&2;}
-    { (exit 1); exit 1; }; }
-@@ -9085,7 +9085,7 @@ $as_echo "$as_me: error: $lp requested b
- $as_echo "$as_me: WARNING: $lp disable because $reason." >&2;}
-         fi
-       else
--        if test "$short_mark" == "partial"; then
-+        if test "$short_mark" = "partial"; then
-           reason=`echo $2 | sed -e 's/partial (\(.*\))/\1/' `
- 	  { $as_echo "$as_me:$LINENO: WARNING: $lp only partially enable because $reason." >&5
- $as_echo "$as_me: WARNING: $lp only partially enable because $reason." >&2;}
-@@ -9140,7 +9140,7 @@ compute_dependency () {
-     case `echo "$mark" | sed -e 's/ .*//' ` in
-       "" | "yes")
-        if test -n "$enable"; then mark="$enable"; else mark="yes"; fi;;
--      "partial") if test "$enable" == "no"; then mark="no"; fi;;
-+      "partial") if test "$enable" = "no"; then mark="no"; fi;;
-       "no")      ;;
-     esac
-     # update plug-in attributes with the new mark
diff --git a/devel/frama-c/patches/patch-ab b/devel/frama-c/patches/patch-ab
deleted file mode 100644
index 5d378d00ffc..00000000000
--- a/devel/frama-c/patches/patch-ab
+++ /dev/null
@@ -1,18 +0,0 @@
-$NetBSD: patch-ab,v 1.1 2010/06/15 08:26:54 wiz Exp $
-
-Fix known incompatibility introduced in a recent version of OCaml.
-The following patch, taken from
-http://old.nabble.com/Bug-569260:-FTBFS:-expression-was-expected-of-type-string--%3E-string--%3E-string-td27540744.html ,
-fixes it.
-
---- ptests/ptests.ml.orig	2009-08-31 15:38:55.000000000 +0000
-+++ ptests/ptests.ml
-@@ -54,7 +54,7 @@ module Filename = struct
-       fun a b -> let r = temp_file a b in
- 	cygpath r
-     else
--      temp_file
-+      (fun x y -> temp_file x y)
- end
- 
- let default_env var value =