[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