The following commit has been merged in the master branch: commit f5a9b1a8cf2a9f797b73036629bac7646b791fc2 Author: Mehdi Dogguy <me...@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 <me...@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 <dog...@pps.jussieu.fr +Packaged-By: Mehdi Dogguy <me...@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 <me...@debian.org> +Copyright: © 2008-2011 Mehdi Dogguy <me...@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 <me...@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 <me...@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 <me...@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 <me...@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@." - 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@." - 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 <me...@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 <me...@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 <me...@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 <me...@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 <me...@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 <me...@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 <me...@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 _______________________________________________ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/mailman/listinfo/pkg-ocaml-maint-commits