[Pkg-ocaml-maint-commits] [SCM] frama-c packaging branch, master, updated. debian/20100401+boron+dfsg-4-10-gf188023

Mehdi Dogguy mehdi at debian.org
Sun Apr 24 16:21:22 UTC 2011


The following commit has been merged in the master branch:
commit f5a9b1a8cf2a9f797b73036629bac7646b791fc2
Author: Mehdi Dogguy <mehdi at debian.org>
Date:   Fri Apr 15 22:23:25 2011 +0200

    New upstream release
    
     - Update copyright file.
     - Remove all patches, integrated by upstream.

diff --git a/debian/changelog b/debian/changelog
index 28698b5..3a216d3 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,11 @@
+frama-c (20110201+carbon+dfsg-1) unstable; urgency=low
+
+  * New upstream release:
+    - Update copyright file.
+    - Remove all patches, integrated by upstream.
+
+ -- Mehdi Dogguy <mehdi at debian.org>  Fri, 15 Apr 2011 21:58:27 +0200
+
 frama-c (20100401+boron+dfsg-5) unstable; urgency=low
 
   [ Stéphane Glondu ]
diff --git a/debian/copyright b/debian/copyright
index febd2a1..6bdf17b 100644
--- a/debian/copyright
+++ b/debian/copyright
@@ -1,11 +1,11 @@
 Format-Specification: http://wiki.debian.org/Proposals/CopyrightFormat
-Packaged-By: Mehdi Dogguy <dogguy at pps.jussieu.fr
+Packaged-By: Mehdi Dogguy <mehdi at debian.org>
 Packaged-Date: Mon, 11 May 2009 15:11:37 +0200
 Original-Source-Location: http://frama-c.cea.fr/download.html
 Upstream-Author: Software Reliability Laboratory (LSL) and INRIA ProVal project
 
 Files: debian/*
-Copyright: © 2008-2010 Mehdi Dogguy <mehdi at debian.org>
+Copyright: © 2008-2011 Mehdi Dogguy <mehdi at debian.org>
 License: LGPL-2.1
   See `/usr/share/common-licenses/LGPL-2.1'.
 
@@ -16,6 +16,7 @@ Files: src/logic/*.ml*
 Files: cil/src/logic/*.ml*
 Files: src/pdg_types/*.ml*
 Files: src/pdg/*.ml*
+Files: src/report/*
 Files: src/slicing_types/*.ml*
 Files: src/slicing/*.ml*
 Files: src/scope/Scope.mli
@@ -23,8 +24,8 @@ Files: src/scope/datascope.ml
 Files: src/scope/dpds_gui.ml
 Files: src/scope/zones.ml
 Files: src/scope/zones.mli
-Copyright: © 2007-2010 CEA (Commissariat à l'Énergie Atomique)
-	   © 2007-2010 INRIA (Institut National de Recherche en Informatique et Automatique)
+Copyright: © 2007-2011 CEA (Commissariat à l'Énergie Atomique)
+	   © 2007-2011 INRIA (Institut National de Recherche en Informatique et Automatique)
 License: LGPL-2.1
   See `/usr/share/common-licenses/LGPL-2.1'.
 
@@ -35,8 +36,8 @@ License: LGPL-2.1
   See `/usr/share/common-licenses/LGPL-2.1'.
 
 Files: src/aorai/*
-Copyright: © 2007-2010 INSA (Institut National des Sciences Appliquees)
-	   © 2007-2010 INRIA (Institut National de Recherche en Informatique et en Automatique)
+Copyright: © 2007-2011 INSA (Institut National des Sciences Appliquees)
+	   © 2007-2011 INRIA (Institut National de Recherche en Informatique et en Automatique)
 License: LGPL-2.1
   See `/usr/share/common-licenses/LGPL-2.1'.
 
@@ -98,7 +99,11 @@ Files: share/Makefile.dynamic_config.internal
 Files: src/ai/ival.ml
 Files: src/ai/ival.mli
 Files: src/dummy/*
-Copyright: © 2007-2010 CEA (Commissariat à l'Énergie Atomique)
+Files: src/impact/*
+Files: src/security_slicing/*
+Files: src/rte/*
+Files: src/type/*
+Copyright: © 2007-2011 CEA (Commissariat à l'Énergie Atomique)
 License: LGPL-2.1
   See `/usr/share/common-licenses/LGPL-2.1'.
 
@@ -110,10 +115,9 @@ License: GPL-3
 Files: cil/src/logic/*
 Files: doc/code/*
 Files: man/frama-c.1
-Files: share/why/*
 Files: src/sparecode/*.ml*
-Copyright: © 2007-2010 CEA (Commissariat à l'Énergie Atomique et aux énergies alternatives)
-           © 2007-2010 INRIA (Institut National de Recherche en Informatique et en Automatique)
+Copyright: © 2007-2011 CEA (Commissariat à l'Énergie Atomique et aux énergies alternatives)
+           © 2007-2011 INRIA (Institut National de Recherche en Informatique et en Automatique)
 License: LGPL-2.1
   See `/usr/share/common-licenses/LGPL-2.1'.
 
@@ -141,8 +145,8 @@ Copyright: © 2009-2010 Institut National de Recherche en Informatique et en Aut
 License: BSD-3
   See `/usr/share/common-licenses/BSD'.
 
-Files: external/ptmap.ml
-Files: external/ptmap.mli
+Files: external/hptmap.ml
+Files: external/hptmap.mli
 Copyright: © 2005 Institut National de Recherche en Informatique et en Automatique
 License: QPL modified
   See `./licenses/Q_MODIFIED_LICENSE`.
diff --git a/debian/patches/0001-Fix-hyphen-used-as-minus-sign-and-a-typo.patch b/debian/patches/0001-Fix-hyphen-used-as-minus-sign-and-a-typo.patch
deleted file mode 100644
index 8bac7de..0000000
--- a/debian/patches/0001-Fix-hyphen-used-as-minus-sign-and-a-typo.patch
+++ /dev/null
@@ -1,40 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Sun, 25 Apr 2010 16:06:51 +0200
-Subject: [PATCH] Fix hyphen-used-as-minus-sign and a typo
-
----
- man/frama-c.1 |    6 +++---
- 1 files changed, 3 insertions(+), 3 deletions(-)
-
-diff --git a/man/frama-c.1 b/man/frama-c.1
-index 90d4393..fb9fa88 100644
---- a/man/frama-c.1
-+++ b/man/frama-c.1
-@@ -44,7 +44,7 @@ framework. This framework can be extended by additional plugins placed in the
- .B $FRAMAC_PLUGIN
- directory. The command
- .IP
--frama-c -help
-+frama\-c \-help
- .PP
- will provide the full list of the plugins that are currently installed.
- .P
-@@ -146,7 +146,7 @@ as the command to pre-process C files. Defaults to the
- .B CPP
- environment variable or to
- .IP
--gcc -C -E -I.
-+gcc \-C \-E \-I.
- .IP
- if it is not set. In order to preserve ACSL annotations, the preprocessor must
- keep comments (the
-@@ -307,7 +307,7 @@ alias of
- .B -print-share-path
- .TP
- .B -print-plugin-path
--outputs the directory where Frama-C searchs its plugins (can be overidden by the
-+outputs the directory where Frama-C searches its plugins (can be overidden by the
- .B FRAMAC_PLUGIN
- variable and the
- .B -add-path
--- 
diff --git a/debian/patches/0002-.make-ocamlgraph-no-op-for-non-local-ocamlgraph.patch b/debian/patches/0002-.make-ocamlgraph-no-op-for-non-local-ocamlgraph.patch
deleted file mode 100644
index 2759dce..0000000
--- a/debian/patches/0002-.make-ocamlgraph-no-op-for-non-local-ocamlgraph.patch
+++ /dev/null
@@ -1,29 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Sun, 25 Apr 2010 16:09:46 +0200
-Subject: [PATCH] .make-ocamlgraph no-op for non-local ocamlgraph
-
----
- Makefile |    2 ++
- 1 files changed, 2 insertions(+), 0 deletions(-)
-
-diff --git a/Makefile b/Makefile
-index 6f21662..4c9e01a 100644
---- a/Makefile
-+++ b/Makefile
-@@ -381,6 +381,7 @@ endif # testing ocamlgraph is local
- # change '.make-ocamlgraph-stamp' before 'cvs commit'
- .make-ocamlgraph: .make-ocamlgraph-stamp
- 	touch $@
-+ifneq ("$(OCAMLGRAPH_LOCAL)","")
- # Inline the rules of "untar-ocamlgraph" here
- # because calling a recursive make does not work
- 	$(PRINT_UNTAR) ocamlgraph
-@@ -388,6 +389,7 @@ endif # testing ocamlgraph is local
- 	$(TAR) xzf ocamlgraph.tar.gz
- 	cd $(OCAMLGRAPH_LOCAL) && ./configure
- 	$(MAKE) clean
-+endif
- 
- include .make-ocamlgraph
- DISTRIB_FILES += .make-ocamlgraph
--- 
diff --git a/debian/patches/0003-Fix-build-on-bytecode-only-architectures.patch b/debian/patches/0003-Fix-build-on-bytecode-only-architectures.patch
deleted file mode 100644
index 12f7ebe..0000000
--- a/debian/patches/0003-Fix-build-on-bytecode-only-architectures.patch
+++ /dev/null
@@ -1,60 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Tue, 27 Apr 2010 11:29:19 +0200
-Subject: [PATCH] Fix build on bytecode-only architectures
-
----
- Makefile |   19 ++++++++++++-------
- 1 files changed, 12 insertions(+), 7 deletions(-)
-
-diff --git a/Makefile b/Makefile
-index 4c9e01a..8e6a14c 100644
---- a/Makefile
-+++ b/Makefile
-@@ -1232,7 +1232,7 @@ lablgtk.cmxa:
- 
- include share/Makefile.plugin
- 
--gui: lib/plugins/Gui.cmo
-+gui:: lib/plugins/Gui.cmo
- 
- else
- 
-@@ -1249,6 +1249,7 @@ SINGLE_GUI_CMO:= gui_parameters \
- 	property_navigator
- SINGLE_GUI_CMO:= $(patsubst %, src/gui/%.cmo, $(SINGLE_GUI_CMO))
- 
-+SINGLE_GUI_O = $(SINGLE_GUI_CMO:.cmo=.o)
- SINGLE_GUI_CMI = $(SINGLE_GUI_CMO:.cmo=.cmi)
- SINGLE_GUI_CMX = $(SINGLE_GUI_CMO:.cmo=.cmx)
- 
-@@ -1271,8 +1272,10 @@ $(PLUGIN_DEP_GUI_CMX_LIST) $(PLUGIN_DYN_DEP_GUI_CMX_LIST): OFLAGS+= $(GUI_INCLUD
- 
- .PHONY:gui
- 
--gui:: bin/viewer.byte$(EXE) bin/viewer.opt$(EXE) \
--      share/Makefile.dynamic_config share/Makefile.kernel
-+ifeq ($(OCAMLBEST),opt)
-+gui:: bin/viewer.opt$(EXE)
-+endif
-+gui:: bin/viewer.byte$(EXE) share/Makefile.dynamic_config share/Makefile.kernel
- 	$(MAKE) install-gui FRAMAC_LIBDIR=lib/fc
- 
- ALL_GUI_CMO= $(ALL_CMO) $(GRAPH_GUICMO) $(GUICMO)
-@@ -1635,10 +1638,12 @@ install-kernel-opt:
- install-gui:
- 	$(PRINT_CP) gui API
- 	$(MKDIR) $(FRAMAC_LIBDIR)
--	if [ "$(ENABLE_GUI)" != "no" ]; then \
--	  $(CP) $(SINGLE_GUI_CMI) $(SINGLE_GUI_CMO) $(SINGLE_GUI_CMX) \
--	    $(FRAMAC_LIBDIR); \
--        fi
-+ifneq ($(ENABLE_GUI),no)
-+	$(CP) $(SINGLE_GUI_CMI) $(SINGLE_GUI_CMO) $(FRAMAC_LIBDIR)
-+ifeq ($(OCAMLBEST),opt)
-+	$(CP) $(SINGLE_GUI_CMX) $(SINGLE_GUI_O) $(FRAMAC_LIBDIR)
-+endif
-+endif
- 
- .PHONY: install
- install::
--- 
diff --git a/debian/patches/0004-Fix-some-typos.patch b/debian/patches/0004-Fix-some-typos.patch
deleted file mode 100644
index bf6fbff..0000000
--- a/debian/patches/0004-Fix-some-typos.patch
+++ /dev/null
@@ -1,342 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Tue, 27 Apr 2010 11:44:45 +0200
-Subject: [PATCH] Fix some typos
-
----
- cil/src/frontc/cabs2cil.ml         |    4 ++--
- cil/src/logic/logic_preprocess.ml  |    2 +-
- cil/src/logic/logic_preprocess.mll |    2 +-
- cil/src/logic/logic_typing.ml      |    2 +-
- man/frama-c.1                      |    2 +-
- ptests/ptests.ml                   |    2 +-
- src/ai/base.ml                     |    2 +-
- src/ai/base.mli                    |    2 +-
- src/aorai/abstract_ai.ml           |    2 +-
- src/aorai/bycase_ai.ml             |    2 +-
- src/kernel/journal.ml              |    2 +-
- src/kernel/special_hooks.ml        |    2 +-
- src/lib/qstack.mli                 |    2 +-
- src/memory_state/locations.mli     |    4 ++--
- src/project/kind.ml                |    4 ++--
- src/project/kind.mli               |    4 ++--
- src/scope/dpds_gui.ml              |    2 +-
- src/slicing/fct_slice.ml           |    6 +++---
- src/slicing/register.ml            |    2 +-
- src/slicing/slicingProject.ml      |    2 +-
- 20 files changed, 26 insertions(+), 26 deletions(-)
-
-diff --git a/cil/src/frontc/cabs2cil.ml b/cil/src/frontc/cabs2cil.ml
-index 1f83e58..c6c8828 100644
---- a/cil/src/frontc/cabs2cil.ml
-+++ b/cil/src/frontc/cabs2cil.ml
-@@ -1035,7 +1035,7 @@ module BlockChunk =
- 
-     let unspecified_chunk c = (* c *)
-       (* to restore previous behavior (where unspecified evaluation order
--         was not explicitely marked), comment out the line below and make
-+         was not explicitly marked), comment out the line below and make
-          unspecified_chunk the identity function.
-        *)
-       { c with unspecified_order = true }
-@@ -3777,7 +3777,7 @@ and getIntConstExp ghost (aexp) : exp =
-  * sizeof/alignof since (for CCured) we can't const-eval those,
-  * and it's not clear whether they can be bitfield width specifiers
-  * anyway (since that's where this function is used)
-- * -- VP 2006-12-20: C99 explicitely says so (par. 6.6.6)
-+ * -- VP 2006-12-20: C99 explicitly says so (par. 6.6.6)
-  *)
- and isIntegerConstant ghost (aexp) : int option =
-   match doExp (ghost_local_env ghost) true aexp (AExp None) with
-diff --git a/cil/src/logic/logic_preprocess.ml b/cil/src/logic/logic_preprocess.ml
-index 1698bcb..760b2cd 100644
---- a/cil/src/logic/logic_preprocess.ml
-+++ b/cil/src/logic/logic_preprocess.ml
-@@ -27,7 +27,7 @@
-     let debug = Cilmsg.debug_atleast 3 in
-     let (ppname, ppfile) = Filename.open_temp_file "ppannot" ".c" in
-     Buffer.output_buffer ppfile macros;
--    (* NB: the three extra spaces replace the begining of the annotation
-+    (* NB: the three extra spaces replace the beginning of the annotation
-        in order to keep the columns count accurate (at least until there's
-        a macro expansion).
-     *)
-diff --git a/cil/src/logic/logic_preprocess.mll b/cil/src/logic/logic_preprocess.mll
-index ce51e09..7900bb8 100644
---- a/cil/src/logic/logic_preprocess.mll
-+++ b/cil/src/logic/logic_preprocess.mll
-@@ -51,7 +51,7 @@
-     let debug = Cilmsg.debug_atleast 3 in
-     let (ppname, ppfile) = Filename.open_temp_file "ppannot" ".c" in
-     Buffer.output_buffer ppfile macros;
--    (* NB: the three extra spaces replace the begining of the annotation
-+    (* NB: the three extra spaces replace the beginning of the annotation
-        in order to keep the columns count accurate (at least until there's
-        a macro expansion).
-     *)
-diff --git a/cil/src/logic/logic_typing.ml b/cil/src/logic/logic_typing.ml
-index 95b0635..fe96f31 100644
---- a/cil/src/logic/logic_typing.ml
-+++ b/cil/src/logic/logic_typing.ml
-@@ -1228,7 +1228,7 @@ struct
-       | [_] -> check_current_label loc env;
-       | _ -> error loc
-           "logic function or predicate %a has multiple labels. \
--         They must be instantiated explicitely." Cil.d_logic_var info.l_var_info
-+         They must be instantiated explicitly." Cil.d_logic_var info.l_var_info
- 
-   let rec term env t =
-     match t.lexpr_node with
-diff --git a/man/frama-c.1 b/man/frama-c.1
-index fb9fa88..f77e8fa 100644
---- a/man/frama-c.1
-+++ b/man/frama-c.1
-@@ -113,7 +113,7 @@ Sets verbosity and debugging level to 0.
- considers that all numerical addresses in the range
- .I min-max
- are valid. Bounds are parsed as ocaml integer constants. By default,
--all numerical adresses are considered invalid.
-+all numerical addresses are considered invalid.
- .TP
- .BI \-add\-path\  p1[,p2[...,pn]]
- adds directories
-diff --git a/ptests/ptests.ml b/ptests/ptests.ml
-index e4b3570..ea536b6 100644
---- a/ptests/ptests.ml
-+++ b/ptests/ptests.ml
-@@ -261,7 +261,7 @@ type config =
-       (** troplevel full path and options to launch the toplevel on *)
-       dc_dont_run   : bool;
-       dc_is_explicit_test: bool
--        (** set to true for single test files that are explicitely
-+        (** set to true for single test files that are explicitly
-             mentioned on the command line. Overrides dc_dont_run. *)
-     }
- 
-diff --git a/src/ai/base.ml b/src/ai/base.ml
-index d156faf..3ec72b5 100644
---- a/src/ai/base.ml
-+++ b/src/ai/base.ml
-@@ -44,7 +44,7 @@ type t =
-   | Var of varinfo*validity
-   | Initialized_Var of varinfo*validity
-       (** base that is implicitely initialized. *)
--  | Null (** base for adresses like [(int* )0x123] *)
-+  | Null (** base for addresses like [(int* )0x123] *)
-   | String of int*string (** String constants *)
-   | Cell_class of cell_class_attributes (** a class of memory cells *)
- 
-diff --git a/src/ai/base.mli b/src/ai/base.mli
-index 6182756..dcff08c 100644
---- a/src/ai/base.mli
-+++ b/src/ai/base.mli
-@@ -32,7 +32,7 @@ type t = private
-   | Var of Cil_types.varinfo*validity (** Base for uninitialized variables *)
-   | Initialized_Var of Cil_types.varinfo*validity
-       (** Base for variables initialized to zero . *)
--  | Null (** Base for adresses like [(int* )0x123] *)
-+  | Null (** Base for addresses like [(int* )0x123] *)
-   | String of int*string (** String constants *)
-   | Cell_class of cell_class_attributes (** A class of memory cells *)
- 
-diff --git a/src/aorai/abstract_ai.ml b/src/aorai/abstract_ai.ml
-index 4215c9c..8116d11 100644
---- a/src/aorai/abstract_ai.ml
-+++ b/src/aorai/abstract_ai.ml
-@@ -800,7 +800,7 @@ class visit_propagating_pre_post_constraints (auto:Promelaast.buchautomata)  =
- 
- 
-     in
--    (* This computation is done from end to begining *)
-+    (* This computation is done from end to beginning *)
-     prop (List.rev stmt_l) (post_st,post_tr)
-   in
- 
-diff --git a/src/aorai/bycase_ai.ml b/src/aorai/bycase_ai.ml
-index 0b75a1d..faa62bb 100644
---- a/src/aorai/bycase_ai.ml
-+++ b/src/aorai/bycase_ai.ml
-@@ -816,7 +816,7 @@ class visit_propagating_pre_post_constraints_bycase (auto:Promelaast.buchautomat
- 
- 
-     in
--    (* This computation is done from end to begining *)
-+    (* This computation is done from end to beginning *)
-     prop (List.rev stmt_l) (post_st,post_tr)
- 
-   in
-diff --git a/src/kernel/journal.ml b/src/kernel/journal.ml
-index f69b752..35e9812 100644
---- a/src/kernel/journal.ml
-+++ b/src/kernel/journal.ml
-@@ -191,7 +191,7 @@ let write () =
- let () =
-   (* write the journal iff it is enable and
-      - either an error occurs;
--     - or the user explicitely wanted it. *)
-+     - or the user explicitly wanted it. *)
-   if Cmdline.journal_enable then begin
-     Cmdline.at_error_exit write;
-     if Cmdline.journal_isset then Cmdline.at_normal_exit write
-diff --git a/src/kernel/special_hooks.ml b/src/kernel/special_hooks.ml
-index 181276d..c7545c3 100644
---- a/src/kernel/special_hooks.ml
-+++ b/src/kernel/special_hooks.ml
-@@ -26,7 +26,7 @@ let version () =
- Compilation date: %s
- Share path: %s (may be overridden with FRAMAC_SHARE variable)
- Library path: %s (may be overridden with FRAMAC_LIB variable)
--Plug-in paths: %t(may be overriden with FRAMAC_PLUGIN variable)@."
-+Plug-in paths: %t(may be overridden with FRAMAC_PLUGIN variable)@."
-       Config.version Config.date Config.datadir Config.libdir
-       (fun fmt -> List.iter (fun s -> Format.fprintf fmt "%s " s)
- 	 (Dynamic.default_path ()));
-diff --git a/src/lib/qstack.mli b/src/lib/qstack.mli
-index ec58d76..658ac30 100644
---- a/src/lib/qstack.mli
-+++ b/src/lib/qstack.mli
-@@ -49,7 +49,7 @@ module Make(D: DATA) : sig
-     (** Remove all the elements of a stack. *)
-     
-   val add: D.t -> t -> unit
--    (** Add at the begining of the stack. Complexity: O(1). *)
-+    (** Add at the beginning of the stack. Complexity: O(1). *)
- 
-   val add_at_end: D.t -> t -> unit
-     (** Add at the end of the stack. Complexity: O(1). *)
-diff --git a/src/memory_state/locations.mli b/src/memory_state/locations.mli
-index 456c30f..2e2931a 100644
---- a/src/memory_state/locations.mli
-+++ b/src/memory_state/locations.mli
-@@ -116,7 +116,7 @@ module Location_Bytes : sig
-     joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a
- 
-   val contains_addresses_of_locals : (M.key -> bool) -> t -> bool
--    (** [contains_adresses_of_locals is_local loc] returns [true]
-+    (** [contains_addresses_of_locals is_local loc] returns [true]
-         if [loc] contains the adress of a variable for which
-         [is_local] returns [true]
-      *)
-@@ -128,7 +128,7 @@ module Location_Bytes : sig
-      *)
- 
-   val contains_addresses_of_any_locals : t -> bool
--    (** [contains_adresses_of_any_locals loc] returns [true] iff [loc] contains
-+    (** [contains_addresses_of_any_locals loc] returns [true] iff [loc] contains
- 	the adress of a local variable or of a formal variable. *)
- 
- end
-diff --git a/src/project/kind.ml b/src/project/kind.ml
-index 647f0a9..aa49a25 100644
---- a/src/project/kind.ml
-+++ b/src/project/kind.ml
-@@ -366,7 +366,7 @@ dependencies:@\n%s@\n%s at ."
- 	    Mark.set v 2;
- 	    acc
- 	| _, _, Some Only_Select_Dependencies, _ ->
--	    (* Do explicitely not select the dependencies *)
-+	    (* Do explicitly not select the dependencies *)
- 	    Mark.set v 2;
- 	    f v acc
- 	| true, Some _, _, _ ->
-@@ -380,7 +380,7 @@ dependencies:@\n%s@\n%s at ."
- 	    Mark.set v 1;
- 	    f v acc
- 	| false, Some Only_Select_Dependencies, None, _ ->
--	    (* Do explicitely select the dependencies *)
-+	    (* Do explicitly select the dependencies *)
- 	    Mark.set v 1;
- 	    acc
-       in
-diff --git a/src/project/kind.mli b/src/project/kind.mli
-index 979e633..b3f2394 100644
---- a/src/project/kind.mli
-+++ b/src/project/kind.mli
-@@ -138,7 +138,7 @@ sig
-     Selection.t -> Selection.t -> (t -> 'a -> 'a) -> 'a -> 'a
-     (** [apply_in_order only except f x] folds [f] for of each kind of type [t] 
- 	(or for each kind specified by [only] and [except] if one of them is 
--	non-empty), begining to [acc] and following a topological order of 
-+	non-empty), beginning to [acc] and following a topological order of
- 	kinds dependencies. *)
- 
-   val iter_in_order: 
-@@ -158,7 +158,7 @@ sig
-     Selection.t -> Selection.t -> (T.t -> 'a -> 'a) -> 'a -> 'a
-     (** [fold_in_order only except f acc] folds [f v x] for each kind value [v]
- 	of type [T.t] (or for each kind specified by [only] and 
--	[except] if one of them is non-empty), begining to [acc] and following 
-+	[except] if one of them is non-empty), beginning to [acc] and following
- 	the same order as apply_in_order. *)
- 
-   val number_of_applicants: Selection.t -> Selection.t -> int option
-diff --git a/src/scope/dpds_gui.ml b/src/scope/dpds_gui.ml
-index 4984597..d8b1e3f 100644
---- a/src/scope/dpds_gui.ml
-+++ b/src/scope/dpds_gui.ml
-@@ -236,7 +236,7 @@ module ShowDef : (DpdCmdSig with type t_in = lval) = struct
-       ^"highlight the statements that define the value of D at L,\n\t"
-       ^"and print a message if a part of D might be undefined.\n\t"
-       ^"Notice that 'undefined' only means here "
--      ^"not defined on some path from the begining of the function.")
-+      ^"not defined on some path from the beginning of the function.")
- 
- 
-   let get_info _kf_stmt_opt =
-diff --git a/src/slicing/fct_slice.ml b/src/slicing/fct_slice.ml
-index 9bf763c..ec4fd2f 100644
---- a/src/slicing/fct_slice.ml
-+++ b/src/slicing/fct_slice.ml
-@@ -418,7 +418,7 @@ end = struct
-   (** compute the marks to propagate in [pdg_caller] when the called function
-  * have the [to_prop] marks.
-  * @param fi_to_call is used to compute [more_inputs] only :
-- *        a persistant input mark is not considered as a new input.
-+ *        a persistent input mark is not considered as a new input.
-  * *)
-   let marks_for_caller_inputs pdg_caller old_marks call to_prop fi_to_call =
-     assert (not (PdgTypes.Pdg.is_top pdg_caller));
-@@ -736,7 +736,7 @@ let examine_calls ff new_marks_in_call_outputs =
-   in FctMarks.fold_calls process_this_call ff []
- 
- (** build a new empty slice in the given [fct_info].
--* If the function has some persistant selection, let's copy it in the new slice.
-+* If the function has some persistent selection, let's copy it in the new slice.
- * Notice that there can be at most one slice for the application entry point
- * (main), but we allow to have several slice for a library entry point.
- * @param build_actions (bool) is useful if the function has some persistent
-@@ -885,7 +885,7 @@ let prop_persistant_marks proj fi to_prop actions =
- * and [propagate=true], also generates the actions to make every calls to this
- * function visible. *)
- let add_marks_to_fi proj fi nodes_marks propagate actions =
--  SlicingParameters.debug ~level:2 "[Fct_Slice.add_marks_to_fi] (persistant)";
-+  SlicingParameters.debug ~level:2 "[Fct_Slice.add_marks_to_fi] (persistent)";
-   let marks, are_new_marks =
-     match FctMarks.fi_marks fi with
-       | Some m -> m, false
-diff --git a/src/slicing/register.ml b/src/slicing/register.ml
-index 3a6913f..bbe177a 100644
---- a/src/slicing/register.ml
-+++ b/src/slicing/register.ml
-@@ -378,7 +378,7 @@ let add_ff_selection proj ff db_select =
-   let _, select = check_ff_db_select ff db_select in
-       SlicingProject.add_fct_ff_filter proj ff select
- 
--(** add a persistant selection to the function.
-+(** add a persistent selection to the function.
- * This might change its slicing level in order to call slices later on. *)
- let add_fi_selection proj db_select =
-   SlicingParameters.debug ~level:1 "[Register.add_fi_selection] %a"
-diff --git a/src/slicing/slicingProject.ml b/src/slicing/slicingProject.ml
-index 9cf2858..4b9bba6 100644
---- a/src/slicing/slicingProject.ml
-+++ b/src/slicing/slicingProject.ml
-@@ -53,7 +53,7 @@ let get_name proj = proj.T.name
- let add_proj_actions proj actions = proj.T.actions <- actions @ proj.T.actions
- 
- (** Add a new slice for the function. It can be the case that it create actions
--* if the function has some persistant selection, that make function calls to
-+* if the function has some persistent selection, that make function calls to
- * choose. 
- * @raise SlicingTypes.NoPdg when the function has no PDG.
- * *)
--- 
diff --git a/debian/patches/0005-Don-t-modify-system-files.patch b/debian/patches/0005-Don-t-modify-system-files.patch
deleted file mode 100644
index 5936180..0000000
--- a/debian/patches/0005-Don-t-modify-system-files.patch
+++ /dev/null
@@ -1,26 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Tue, 27 Apr 2010 13:10:54 +0200
-Subject: [PATCH] Don't modify system files
-
----
- share/Makefile.dynamic |    6 +++---
- 1 files changed, 3 insertions(+), 3 deletions(-)
-
-diff --git a/share/Makefile.dynamic b/share/Makefile.dynamic
-index e35b0b7..dbe5098 100644
---- a/share/Makefile.dynamic
-+++ b/share/Makefile.dynamic
-@@ -191,9 +191,9 @@ install::
- 	  $(CP) frama-c-$(PLUGIN_NAME).$(OCAMLBEST)$(EXE) \
- 		$(BINDIR)/frama-c-$(PLUGIN_NAME)$(EXE); \
- 	fi
--	$(PRINT_UPDATE) $(FRAMAC_SHARE)/known_plugins.ac
--	echo "ENABLE_`echo $(PLUGIN_NAME) | tr "a-z" "A-Z"`=$(PLUGIN_ENABLE)" \
--	  >> $(FRAMAC_SHARE)/known_plugins.ac
-+#	$(PRINT_UPDATE) $(FRAMAC_SHARE)/known_plugins.ac
-+#	echo "ENABLE_`echo $(PLUGIN_NAME) | tr "a-z" "A-Z"`=$(PLUGIN_ENABLE)" \
-+#	  >> $(FRAMAC_SHARE)/known_plugins.ac
- ifeq ($(HAS_GUI),yes)
- 	$(PRINT_CP) $(PLUGIN_INSTALL_DIR)/gui
- 	$(CP) $(TARGETS_GUI) $(PLUGIN_INSTALL_DIR)/gui
--- 
diff --git a/debian/patches/0006-OCamlgraph-1.5-is-compatible.patch b/debian/patches/0006-OCamlgraph-1.5-is-compatible.patch
deleted file mode 100644
index db766e2..0000000
--- a/debian/patches/0006-OCamlgraph-1.5-is-compatible.patch
+++ /dev/null
@@ -1,35 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Tue, 1 Jun 2010 19:59:56 +0200
-Subject: [PATCH] OCamlgraph 1.5 is compatible
-
----
- configure    |    2 ++
- configure.in |    1 +
- 2 files changed, 3 insertions(+), 0 deletions(-)
-
-diff --git a/configure b/configure
-index 6c0a567..b87ee33 100755
---- a/configure
-+++ b/configure
-@@ -3121,6 +3121,8 @@ if test "$OCAMLGRAPH_EXISTS" = "yes"; then
-   case $OCAMLGRAPH_VERSION in
-   1.4) { $as_echo "$as_me:${as_lineno-$LINENO}: ocamlgraph $OCAMLGRAPH_VERSION found" >&5
- $as_echo "$as_me: ocamlgraph $OCAMLGRAPH_VERSION found" >&6;};;
-+  1.5) { $as_echo "$as_me:${as_lineno-$LINENO}: ocamlgraph $OCAMLGRAPH_VERSION found" >&5
-+$as_echo "$as_me: ocamlgraph $OCAMLGRAPH_VERSION found" >&6;};;
-   *) { $as_echo "$as_me:${as_lineno-$LINENO}: ocamlgraph $OCAMLGRAPH_VERSION is incompatible with Frama-C. Will switch to a local version." >&5
- $as_echo "$as_me: ocamlgraph $OCAMLGRAPH_VERSION is incompatible with Frama-C. Will switch to a local version." >&6;}
-      OCAMLGRAPH_EXISTS=no
-diff --git a/configure.in b/configure.in
-index d4b7db8..2e42e48 100644
---- a/configure.in
-+++ b/configure.in
-@@ -240,6 +240,7 @@ if test "$OCAMLGRAPH_EXISTS" = "yes"; then
-   OCAMLGRAPH_VERSION=`./test_ocamlgraph`
-   case $OCAMLGRAPH_VERSION in
-   1.4) AC_MSG_NOTICE([ocamlgraph $OCAMLGRAPH_VERSION found]);;
-+  1.5) AC_MSG_NOTICE([ocamlgraph $OCAMLGRAPH_VERSION found]);;
-   *) AC_MSG_NOTICE([ocamlgraph $OCAMLGRAPH_VERSION is incompatible with Frama-C. Will switch to a local version.])
-      OCAMLGRAPH_EXISTS=no
- ;;
--- 
diff --git a/debian/patches/0007-Fix-cpp-command-arguments.patch b/debian/patches/0007-Fix-cpp-command-arguments.patch
deleted file mode 100644
index 92e6efa..0000000
--- a/debian/patches/0007-Fix-cpp-command-arguments.patch
+++ /dev/null
@@ -1,22 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Mon, 14 Jun 2010 23:29:34 +0200
-Subject: [PATCH] Fix cpp command arguments
-
----
- src/kernel/file.ml |    2 +-
- 1 files changed, 1 insertions(+), 1 deletions(-)
-
-diff --git a/src/kernel/file.ml b/src/kernel/file.ml
-index 30c532b..042f29e 100644
---- a/src/kernel/file.ml
-+++ b/src/kernel/file.ml
-@@ -498,7 +498,7 @@ let parse = function
- 	  in
- 	  (* Format.eprintf "-cpp-command cmd2=|%s|@\n" cmd2; *)
-           let cmd3 =
--	    String.sub cmdl (percent2 + 2) (String.length cmdl - percent2 + 2)
-+	    String.sub cmdl (percent2 + 2) (String.length cmdl - (percent2 + 2))
-           in
- 	  (* Format.eprintf "-cpp-command cmd3=|%s|@\n" cmd3; *)
-           Format.sprintf "%s%s %s %s%s%s" cmd1
--- 
diff --git a/debian/patches/0008-Fix-ai-ival.ml-filter_ge.patch b/debian/patches/0008-Fix-ai-ival.ml-filter_ge.patch
deleted file mode 100644
index eb39ffd..0000000
--- a/debian/patches/0008-Fix-ai-ival.ml-filter_ge.patch
+++ /dev/null
@@ -1,24 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Mon, 14 Jun 2010 23:36:05 +0200
-Subject: [PATCH] Fix ai/ival.ml:filter_ge
-
----
- src/ai/ival.ml |    4 ++--
- 1 files changed, 2 insertions(+), 2 deletions(-)
-
-diff --git a/src/ai/ival.ml b/src/ai/ival.ml
-index 1e9c174..efece8c 100644
---- a/src/ai/ival.ml
-+++ b/src/ai/ival.ml
-@@ -482,8 +482,8 @@ struct
-     then f1
-     else inject b1 e2
- 
--  let filter_ge (I(b1, e1) as f1) (I(b2, e2)) =
--    let b2 = if F.equal_ieee F.minus_zero e2 then F.minus_zero else b2 in
-+  let filter_ge (I(b1, e1) as f1) (I(b2, _e2)) =
-+    let b2 = if F.equal_ieee F.minus_zero b2 then F.minus_zero else b2 in
-     if not (F.le b2 e1)
-     then raise Bottom
-     else if F.le b2 b1
--- 
diff --git a/debian/patches/0009-unrollType-in-handle_signed_overflow.patch b/debian/patches/0009-unrollType-in-handle_signed_overflow.patch
deleted file mode 100644
index c325555..0000000
--- a/debian/patches/0009-unrollType-in-handle_signed_overflow.patch
+++ /dev/null
@@ -1,22 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Fri, 16 Jul 2010 13:30:45 +0200
-Subject: [PATCH] unrollType in handle_signed_overflow
-
----
- src/value/eval.ml |    2 +-
- 1 files changed, 1 insertions(+), 1 deletions(-)
-
-diff --git a/src/value/eval.ml b/src/value/eval.ml
-index f7b5d85..10fe5f9 100644
---- a/src/value/eval.ml
-+++ b/src/value/eval.ml
-@@ -359,7 +359,7 @@ let do_promotion ~with_alarms ~src_typ ~dest_type v =
-   | _, _ -> v
- 
- let handle_signed_overflow ~with_alarms syntactic_context typ e interpreted_e =
--  match typ with
-+  match unrollType typ with
-     TInt(kind, _)
-       when Value_parameters.SignedOverflow.get()
- 	&& isSigned kind ->
--- 
diff --git a/debian/patches/0010-More-spelling-fixes.patch b/debian/patches/0010-More-spelling-fixes.patch
deleted file mode 100644
index e62f052..0000000
--- a/debian/patches/0010-More-spelling-fixes.patch
+++ /dev/null
@@ -1,36 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Fri, 16 Jul 2010 13:53:25 +0200
-Subject: [PATCH] More spelling fixes
-
----
- src/memory_state/offsetmap.ml |    2 +-
- src/value/eval.ml             |    2 +-
- 2 files changed, 2 insertions(+), 2 deletions(-)
-
-diff --git a/src/memory_state/offsetmap.ml b/src/memory_state/offsetmap.ml
-index 5b2583a..4d99013 100644
---- a/src/memory_state/offsetmap.ml
-+++ b/src/memory_state/offsetmap.ml
-@@ -437,7 +437,7 @@ exception Not_translatable
-        V.singleton_zero
-    with Is_not_included -> (* from [Int_Interv.check_coverage] *)
-      V.top (* the result depends on several intervals and is not covered
--                    completly. *)
-+                    completely. *)
- 
- 
-  (* Assumes one wants a value from V.t
-diff --git a/src/value/eval.ml b/src/value/eval.ml
-index 10fe5f9..93efb1e 100644
---- a/src/value/eval.ml
-+++ b/src/value/eval.ml
-@@ -1816,7 +1816,7 @@ let resolv_func_vinfo ~with_alarms deps state funcexp =
-            Location_Bytes.get_keys_exclusive Ival.zero loc
-          with Location_Bytes.Not_all_keys ->
-            Value_parameters.warning ~once:true ~current:true
--             "Function pointer call is completly unknown: assuming no effects: assert(TODO)";
-+             "Function pointer call is completely unknown: assuming no effects: assert(TODO)";
- 	   raise Leaf)
-       in
-       (* (ignore (Errormsg.log
--- 
diff --git a/debian/patches/0011-Fix-some-minor-memory-leaks.patch b/debian/patches/0011-Fix-some-minor-memory-leaks.patch
deleted file mode 100644
index 58eb707..0000000
--- a/debian/patches/0011-Fix-some-minor-memory-leaks.patch
+++ /dev/null
@@ -1,31 +0,0 @@
-From: Mehdi Dogguy <mehdi at debian.org>
-Date: Tue, 5 Oct 2010 18:48:13 +0200
-Subject: [PATCH] Fix some minor memory leaks
-
----
- src/value/kf_state.ml |    4 ++--
- 1 files changed, 2 insertions(+), 2 deletions(-)
-
-diff --git a/src/value/kf_state.ml b/src/value/kf_state.ml
-index 9cbf245..238ef2c 100644
---- a/src/value/kf_state.ml
-+++ b/src/value/kf_state.ml
-@@ -45,7 +45,7 @@ let is_called =
-        try Value.is_accessible (Kstmt (Kernel_function.find_first_stmt kf))
-        with Kernel_function.No_Statement -> false)
- 
--let mark_as_called kf = Is_Called.add kf true
-+let mark_as_called kf = Is_Called.replace kf true
- 
- (* ************************************************************************* *)
- (** {2 Callers} *)
-@@ -105,7 +105,7 @@ let never_terminates kf =
-     assert (not (is_called kf));
-     false
- 
--let mark_as_terminates kf = Never_Terminates.add kf false
-+let mark_as_terminates kf = Never_Terminates.replace kf false
- 
- let mark_as_never_terminates kf =
-   let noreturn =
--- 
diff --git a/debian/patches/series b/debian/patches/series
index 353e36f..e69de29 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,11 +0,0 @@
-0001-Fix-hyphen-used-as-minus-sign-and-a-typo.patch
-0002-.make-ocamlgraph-no-op-for-non-local-ocamlgraph.patch
-0003-Fix-build-on-bytecode-only-architectures.patch
-0004-Fix-some-typos.patch
-0005-Don-t-modify-system-files.patch
-0006-OCamlgraph-1.5-is-compatible.patch
-0007-Fix-cpp-command-arguments.patch
-0008-Fix-ai-ival.ml-filter_ge.patch
-0009-unrollType-in-handle_signed_overflow.patch
-0010-More-spelling-fixes.patch
-0011-Fix-some-minor-memory-leaks.patch

-- 
frama-c packaging



More information about the Pkg-ocaml-maint-commits mailing list