The following commit has been merged in the master branch:
commit decd56b430b648f3a8db8a8cefc40c9e7a7498c4
Author: Mehdi Dogguy <me...@debian.org>
Date: Tue Jun 25 22:04:38 2013 +0200
Update patches.
- Disable 0001-Add-ocamlgraph-to-DYN_-O-B-LINKFLAGS.patch
- Remove 0002-Accept-ocamlgraph-1.8.patch, fixed upstream
- Remove 0006-Patchlevel2-for-Nitrogen-20111001.patch, integrated
diff --git a/debian/changelog b/debian/changelog
index b11834f..4803605 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,6 +1,10 @@
frama-c (20130601+fluorine3+dfsg-1) UNRELEASED; urgency=low
* New upstream release
+ - Remove 0001-Add-ocamlgraph-to-DYN_-O-B-LINKFLAGS.patch, fixed
+ upstream
+ - Remove 0002-Accept-ocamlgraph-1.8.patch, fixed upstream
+ - Remove 0006-Patchlevel2-for-Nitrogen-20111001.patch, integrated
-- Mehdi Dogguy <me...@debian.org> Tue, 25 Jun 2013 21:51:45 +0200
diff --git a/debian/patches/0001-Add-ocamlgraph-to-DYN_-O-B-LINKFLAGS.patch
b/debian/patches/0001-Add-ocamlgraph-to-DYN_-O-B-LINKFLAGS.patch
deleted file mode 100644
index adaf32d..0000000
--- a/debian/patches/0001-Add-ocamlgraph-to-DYN_-O-B-LINKFLAGS.patch
+++ /dev/null
@@ -1,27 +0,0 @@
-From: Mehdi Dogguy <me...@debian.org>
-Date: Mon, 25 Apr 2011 12:01:09 +0200
-Subject: Add +ocamlgraph to DYN_{O,B}LINKFLAGS
-
----
- Makefile | 4 ++--
- 1 files changed, 2 insertions(+), 2 deletions(-)
-
-diff --git a/Makefile b/Makefile
-index b70d794..6432662 100644
---- a/Makefile
-+++ b/Makefile
-@@ -1324,11 +1324,11 @@ share/Makefile.kernel: Makefile share/Makefile.config
share/Makefile.common
- $(ECHO) "DYN_OPT_LIBS=$(filter-out $(GEN_OPT_LIBS), $(OPT_LIBS))" >> $@
- $(ECHO) "DYN_ALL_BATCH_CMX=$(addprefix $(FRAMAC_TOP_SRCDIR)/,
$(ALL_BATCH_CMX))" >> $@
- $(ECHO) "else" >> $@
-- $(ECHO) "DYN_BLINKFLAGS=$(filter-out $(INCLUDES), $(BLINKFLAGS))" >> $@
-+ $(ECHO) "DYN_BLINKFLAGS=$(filter-out $(INCLUDES), $(BLINKFLAGS)) -I
+ocamlgraph" >> $@
- $(ECHO) "DYN_GEN_BYTE_LIBS=$(addprefix $(FRAMAC_LIBDIR)/, $(notdir
$(GEN_BYTE_LIBS)))" >> $@
- $(ECHO) "DYN_BYTE_LIBS=$(filter-out $(GEN_BYTE_LIBS), $(BYTE_LIBS))" >>
$@
- $(ECHO) "DYN_ALL_BATCH_CMO=$(addprefix $(FRAMAC_LIBDIR)/, $(notdir
$(ALL_BATCH_CMO)))" >> $@
-- $(ECHO) "DYN_OLINKFLAGS=$(filter-out $(INCLUDES), $(OLINKFLAGS))" >> $@
-+ $(ECHO) "DYN_OLINKFLAGS=$(filter-out $(INCLUDES), $(OLINKFLAGS)) -I
+ocamlgraph" >> $@
- $(ECHO) "DYN_GEN_OPT_LIBS=$(addprefix $(FRAMAC_LIBDIR)/, $(notdir
$(GEN_OPT_LIBS)))" >> $@
- $(ECHO) "DYN_OPT_LIBS=$(filter-out $(GEN_OPT_LIBS), $(OPT_LIBS))" >> $@
- $(ECHO) "DYN_ALL_BATCH_CMX=$(addprefix $(FRAMAC_LIBDIR)/, $(notdir
$(ALL_BATCH_CMX)))" >> $@
---
diff --git a/debian/patches/0001-Fix-spelling-error-in-binary.patch
b/debian/patches/0001-Fix-spelling-error-in-binary.patch
new file mode 100644
index 0000000..d635ea1
--- /dev/null
+++ b/debian/patches/0001-Fix-spelling-error-in-binary.patch
@@ -0,0 +1,68 @@
+From: Mehdi Dogguy <me...@debian.org>
+Date: Mon, 2 Jan 2012 14:36:52 +0100
+Subject: Fix spelling-error-in-binary
+
+---
+ Changelog | 4 ++--
+ cil/src/frontc/cabs2cil.ml | 4 ++--
+ man/frama-c.1 | 2 +-
+ 3 files changed, 5 insertions(+), 5 deletions(-)
+
+diff --git a/Changelog b/Changelog
+index aaae442..5f972ef 100644
+--- a/Changelog
++++ b/Changelog
+@@ -219,7 +219,7 @@ o! Kernel [2012/11/24] Various types whose names
started by t_ in
+ o Rte [2012/11/23] Export function "exp_annotations" to get RTEs of a
C
+ expression as annotations.
+ o*!Kernel [2012/11/23] Added TLogic_coerce constructor to mark
+- explicitely a conversion from a C type to a logical one
++ explicitly a conversion from a C type to a logical one
+ (in particular floating point -> real and integral -> integer).
+ Fixes issue #1309.
+ o! Kernel [2012/11/22] Remove unintuitive ?prj argument from Cil visitors,
+@@ -1237,7 +1237,7 @@ o* Cil [2010/12/20] Fixed bug #645.
Ast_info.constant_expr,
+ mkAddrOrStartOf,mkString,parseInt,sizeOf] no longer use
+ an optional argument ?loc. It is now a non optional labeled
+ argument. Previous default value of loc was
+- ~loc:Cil_datatype.Location.unkown which is most of the time
++ ~loc:Cil_datatype.Location.unknown which is most of the time
+ not accurate.
+
+ ###################################
+diff --git a/cil/src/frontc/cabs2cil.ml b/cil/src/frontc/cabs2cil.ml
+index 8351fc2..23d7769 100644
+--- a/cil/src/frontc/cabs2cil.ml
++++ b/cil/src/frontc/cabs2cil.ml
+@@ -2233,7 +2233,7 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) :
varinfo * bool =
+ * local. This can happen when we declare an extern variable with
+ * global scope but we are in a local scope. *)
+
+- (* We lookup in the environement. If this is extern inline then the name
++ (* We lookup in the environment. If this is extern inline then the name
+ * was already changed to foo__extinline. We lookup with the old name *)
+ let lookupname =
+ if vi.vstorage = Static then
+@@ -3427,7 +3427,7 @@ let default_argument_promotion idx exp =
+ "implicit prototype cannot have variadic arguments"
+ | TNamed _ -> assert false (* unrollType *)
+ in
+- (* if we make a promotion, take it explicitely
++ (* if we make a promotion, take it explicitly
+ into account in the argument itself *)
+ let (_,e) = castTo arg_type typ exp in
+ (name,typ,[]), e
+diff --git a/man/frama-c.1 b/man/frama-c.1
+index 667f6a3..e2a1a70 100644
+--- a/man/frama-c.1
++++ b/man/frama-c.1
+@@ -395,7 +395,7 @@ removes break, continue and switch statement before
analyses. Defaults to
+ no.
+ .TP
+ .B -then
+-allows to compose analyzes: a first run of Frama-C will occur with the
++allows one to compose analyzes: a first run of Frama-C will occur with the
+ options before
+ .B -then
+ and a second run will be done with the options after
+--
diff --git a/debian/patches/0002-Accept-ocamlgraph-1.8.patch
b/debian/patches/0002-Accept-ocamlgraph-1.8.patch
deleted file mode 100644
index 6f2f4e8..0000000
--- a/debian/patches/0002-Accept-ocamlgraph-1.8.patch
+++ /dev/null
@@ -1,36 +0,0 @@
-From: Stephane Glondu <st...@glondu.net>
-Date: Sat, 3 Dec 2011 17:58:39 +0100
-Subject: Accept ocamlgraph 1.8*
-
----
- configure | 2 +-
- configure.in | 2 +-
- 2 files changed, 2 insertions(+), 2 deletions(-)
-
-diff --git a/configure b/configure
-index aecf0e1..9b31779 100755
---- a/configure
-+++ b/configure
-@@ -3122,7 +3122,7 @@ if test "$OCAMLGRAPH_EXISTS" = "yes"; then
- then
- OCAMLGRAPH_VERSION=`./test_ocamlgraph`
- case $OCAMLGRAPH_VERSION in
-- 1.8) { $as_echo "$as_me:${as_lineno-$LINENO}: OcamlGraph
$OCAMLGRAPH_VERSION found: great!" >&5
-+ 1.8*) { $as_echo "$as_me:${as_lineno-$LINENO}: OcamlGraph
$OCAMLGRAPH_VERSION found: great!" >&5
- $as_echo "$as_me: OcamlGraph $OCAMLGRAPH_VERSION found: great!" >&6;};;
- *) { $as_echo "$as_me:${as_lineno-$LINENO}: OcamlGraph
$OCAMLGRAPH_VERSION is incompatible with Frama-C." >&5
- $as_echo "$as_me: OcamlGraph $OCAMLGRAPH_VERSION is incompatible with
Frama-C." >&6;}
-diff --git a/configure.in b/configure.in
-index e2ecfe0..abb6c11 100644
---- a/configure.in
-+++ b/configure.in
-@@ -240,7 +240,7 @@ if test "$OCAMLGRAPH_EXISTS" = "yes"; then
- then
- OCAMLGRAPH_VERSION=`./test_ocamlgraph`
- case $OCAMLGRAPH_VERSION in
-- 1.8) AC_MSG_NOTICE([OcamlGraph $OCAMLGRAPH_VERSION found: great!]);;
-+ 1.8*) AC_MSG_NOTICE([OcamlGraph $OCAMLGRAPH_VERSION found: great!]);;
- *) AC_MSG_NOTICE([OcamlGraph $OCAMLGRAPH_VERSION is incompatible with
Frama-C.])
- OCAMLGRAPH_EXISTS=no
- OCAMLGRAPH_INCLUDE=;;
---
diff --git a/debian/patches/0004-Use-bin-cp-instead-of-usr-bin-install.patch
b/debian/patches/0002-Use-bin-cp-instead-of-usr-bin-install.patch
similarity index 71%
rename from debian/patches/0004-Use-bin-cp-instead-of-usr-bin-install.patch
rename to debian/patches/0002-Use-bin-cp-instead-of-usr-bin-install.patch
index df3cf91..0ea4a21 100644
--- a/debian/patches/0004-Use-bin-cp-instead-of-usr-bin-install.patch
+++ b/debian/patches/0002-Use-bin-cp-instead-of-usr-bin-install.patch
@@ -4,18 +4,18 @@ Subject: Use /bin/cp instead of /usr/bin/install
---
share/Makefile.common | 2 +-
- 1 files changed, 1 insertions(+), 1 deletions(-)
+ 1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/share/Makefile.common b/share/Makefile.common
-index c9e8727..ce1a699 100644
+index 90c877e..4441720 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
-@@ -138,7 +138,7 @@ CHMOD_RW= sh -c \
+@@ -157,7 +157,7 @@ CHMOD_RW= sh -c \
'for f in "$$@"; do \
if test -e $$f; then chmod u+w $$f; fi \
done' chmod_rw
--CP = /usr/bin/install
-+CP = /bin/cp
+-CP = install
++CP = cp
ECHO = echo
MKDIR = mkdir -p
MV = mv
diff --git a/debian/patches/0005-Disable-CHMOD_RO-invocations.patch
b/debian/patches/0003-Disable-CHMOD_RO-invocations.patch
similarity index 78%
rename from debian/patches/0005-Disable-CHMOD_RO-invocations.patch
rename to debian/patches/0003-Disable-CHMOD_RO-invocations.patch
index 10e610b..5cfbd65 100644
--- a/debian/patches/0005-Disable-CHMOD_RO-invocations.patch
+++ b/debian/patches/0003-Disable-CHMOD_RO-invocations.patch
@@ -4,13 +4,13 @@ Subject: Disable CHMOD_RO invocations
---
share/Makefile.common | 2 +-
- 1 files changed, 1 insertions(+), 1 deletions(-)
+ 1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/share/Makefile.common b/share/Makefile.common
-index ce1a699..1993cf1 100644
+index 4441720..16a6f61 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
-@@ -133,7 +133,7 @@ external_make = \
+@@ -152,7 +152,7 @@ external_make = \
CAT = cat
CHMOD = chmod
diff --git a/debian/patches/0003-Fix-spelling-error-in-binary.patch
b/debian/patches/0003-Fix-spelling-error-in-binary.patch
deleted file mode 100644
index 3e439ef..0000000
--- a/debian/patches/0003-Fix-spelling-error-in-binary.patch
+++ /dev/null
@@ -1,171 +0,0 @@
-From: Mehdi Dogguy <me...@debian.org>
-Date: Mon, 2 Jan 2012 14:36:52 +0100
-Subject: Fix spelling-error-in-binary
-
----
- Changelog | 8 ++++----
- cil/src/cil.ml | 2 +-
- cil/src/ext/cfg.mli | 2 +-
- cil/src/frontc/cabs2cil.ml | 2 +-
- cil/src/logic/logic_typing.ml | 6 +++---
- man/frama-c.1 | 2 +-
- src/impact/register.ml | 4 ++--
- src/kernel/cmdline.mli | 2 +-
- 8 files changed, 14 insertions(+), 14 deletions(-)
-
-diff --git a/Changelog b/Changelog
-index e527189..909b359 100644
---- a/Changelog
-+++ b/Changelog
-@@ -576,7 +576,7 @@ o* Cil [2010/12/20] Fixed bug #645.
Ast_info.constant_expr,
- mkAddrOrStartOf,mkString,parseInt,sizeOf] no longer use
- an optional argument ?loc. It is now a non optional labeled
- argument. Previous default value of loc was
-- ~loc:Cil_datatype.Location.unkown which is most of the time
-+ ~loc:Cil_datatype.Location.unknown which is most of the time
- not accurate.
-
- ###################################
-@@ -729,7 +729,7 @@ o Cil [2010/06/04] Support for custom extension in
grammar of behaviors.
- -* Cil [2010/05/31] Extended grammar of pragma lines.
- o* Cil [2010/05/28] Fix bug #489: constant literal present in original
- source are preserved in the AST. NB: this implies that they might
-- be explicitely cast when an integer conversion occur.
-+ be explicitly cast when an integer conversion occur.
- -* Kernel [2010/05/28] Fixed bug in handling of -cpp-command
- o! Cil [2010/05/21] Remove deprecated annotation_status of AAssert
- in the AST
-@@ -908,7 +908,7 @@ o! Kernel [2009/11/24] Use of global logic constants
is now a
- - Value [2009/11/24] Handling of behavior-specific assertions now
- correct (albeit imprecise).
- -! Kernel [2009/11/19] The journal is generated only if the GUI is
-- crashing, or if the option -journal-enable is explicitely
-+ crashing, or if the option -journal-enable is explicitly
- set (fixed issue #!330).
- +- Value [2009/11/19] New option -slevel-exclude f for fine-tuning
- semantic unrolling.
-@@ -1206,7 +1206,7 @@ o! Kernel [2009/01/23] File.pretty does not take
anymore a formatter
- -* Journal [2009/01/19] Fixed bug with -disable-journal and type with
- no pretty-printer.
- - Configure [2009/01/19] New option -with-all-static in order to
-- statically link all plug-ins, except those explicitely
-+ statically link all plug-ins, except those explicitly
- specified as dynamic (bts #?430).
- -* Journal [2009/01/19] Fixed bug in journalisation of non-functional
values.
- -* Makefile [2009/01/19] Fixed bug whenever all plug-ins should be static.
-diff --git a/cil/src/cil.ml b/cil/src/cil.ml
-index 8fb03a2..ea04622 100644
---- a/cil/src/cil.ml
-+++ b/cil/src/cil.ml
-@@ -8880,7 +8880,7 @@ let rec mkCastT ~(e: exp) ~(oldt: typ) ~(newt: typ) =
- (* Watch out for constants *)
- match newt, e.enode with
- (* In the case were we have a representation for the literal,
-- add explicitely the cast. *)
-+ add explicitly the cast. *)
- TInt(newik, []), Const(CInt64(i, _, None)) -> kinteger64 ~loc newik i
- | _ ->
- new_exp
-diff --git a/cil/src/ext/cfg.mli b/cil/src/ext/cfg.mli
-index 1467255..f40ad47 100644
---- a/cil/src/ext/cfg.mli
-+++ b/cil/src/ext/cfg.mli
-@@ -51,7 +51,7 @@ open Cil_types
- (** Compute the CFG for an entire file, by calling cfgFun on each function. *)
- val computeFileCFG: file -> unit
-
--(** clear the sid (except when clear_id is explicitely set to false),
-+(** clear the sid (except when clear_id is explicitly set to false),
- succs, and preds fields of each statement. *)
- val clearFileCFG: ?clear_id:bool -> file -> unit
-
-diff --git a/cil/src/frontc/cabs2cil.ml b/cil/src/frontc/cabs2cil.ml
-index fabb198..a69c921 100644
---- a/cil/src/frontc/cabs2cil.ml
-+++ b/cil/src/frontc/cabs2cil.ml
-@@ -2257,7 +2257,7 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) :
varinfo * bool =
- * local. This can happen when we declare an extern variable with
- * global scope but we are in a local scope. *)
-
-- (* We lookup in the environement. If this is extern inline then the name
-+ (* We lookup in the environment. If this is extern inline then the name
- * was already changed to foo__extinline. We lookup with the old name *)
- let lookupname =
- if vi.vstorage = Static then
-diff --git a/cil/src/logic/logic_typing.ml b/cil/src/logic/logic_typing.ml
-index 88d686f..8f76da6 100644
---- a/cil/src/logic/logic_typing.ml
-+++ b/cil/src/logic/logic_typing.ml
-@@ -1803,7 +1803,7 @@ struct
- info.ctor_name
- with Not_found ->
- (* We have a global logic variable. It may depend on
-- a single state (multiple labels need to be explicitely
-+ a single state (multiple labels need to be explicitly
- instantiated and are treated as PLapp below).
- NB: for now, if we have a real function (with
parameters
- other than labels) and a label,
-@@ -1832,7 +1832,7 @@ struct
- Tapp(f,[l,curr],[]), typ
- | _ ->
- error loc
-- "%s labels must be explicitely instantiated" x
-+ "%s labels must be explicitly instantiated" x
- in
- match C.find_all_logic_functions x with
-
-@@ -2581,7 +2581,7 @@ struct
- | [l] -> [l,find_current_label loc env]
- | _ ->
- error loc
-- "%s labels must be explicitely instantiated" x
-+ "%s labels must be explicitly instantiated" x
- in
- papp ~loc (info,labels,[])
- | Some _ -> boolean_to_predicate env p0
-diff --git a/man/frama-c.1 b/man/frama-c.1
-index 4c90286..7bfb92d 100644
---- a/man/frama-c.1
-+++ b/man/frama-c.1
-@@ -356,7 +356,7 @@ removes break, continue and switch statement before
analyses. Defaults to
- no.
- .TP
- .B -then
--allows to compose analyzes: a first run of Frama-C will occur with the
-+allows one to compose analyzes: a first run of Frama-C will occur with the
- options before
- .B -then
- and a second run will be done with the options after
-diff --git a/src/impact/register.ml b/src/impact/register.ml
-index 42778b7..6b160a4 100644
---- a/src/impact/register.ml
-+++ b/src/impact/register.ml
-@@ -41,12 +41,12 @@ let from_stmt s =
- with
- | Dynamic.Incompatible_type _ ->
- error "versions of plug-ins `impact' and `Security_slicing' seem \
--incompatible.\nCheck the environement variable FRAMAC_PLUGIN.\n\
-+incompatible.\nCheck the environment variable FRAMAC_PLUGIN.\n\
- Analysis discarded.";
- []
- | Dynamic.Unbound_value _ ->
- error "cannot access to plug-in `Security_slicing'.\n\
--Are you sure that it is loaded? Check the environement variable \
-+Are you sure that it is loaded? Check the environment variable \
- FRAMAC_PLUGIN.\n\
- Analysis discarded.";
- []
-diff --git a/src/kernel/cmdline.mli b/src/kernel/cmdline.mli
-index 7bf4673..cb5cdb7 100644
---- a/src/kernel/cmdline.mli
-+++ b/src/kernel/cmdline.mli
-@@ -274,7 +274,7 @@ val journal_enable: bool
- (** @since Beryllium-20090601-beta1 *)
-
- val journal_isset: bool
-- (** -journal-enable/disable explicitely set on the command line.
-+ (** -journal-enable/disable explicitly set on the command line.
- @since Boron-20100401 *)
-
- val journal_name: string
---
diff --git a/debian/patches/0006-Patchlevel2-for-Nitrogen-20111001.patch
b/debian/patches/0006-Patchlevel2-for-Nitrogen-20111001.patch
deleted file mode 100644
index c1f224a..0000000
--- a/debian/patches/0006-Patchlevel2-for-Nitrogen-20111001.patch
+++ /dev/null
@@ -1,323 +0,0 @@
-From: Mehdi Dogguy <me...@debian.org>
-Date: Fri, 6 Jan 2012 09:30:22 +0100
-Subject: Patchlevel2 for Nitrogen 20111001
-
----
- Changelog | 21 ++++++++++++
- src/ai/base.ml | 6 ++-
- src/from/from_register.ml | 3 +-
- src/lib/rangemap.ml | 4 +-
- src/memory_state/lmap.ml | 2 +-
- src/value/eval_exprs.ml | 81 +++++++++++++++++++++++---------------------
- src/value/eval_exprs.mli | 1 +
- src/value/eval_funs.ml | 4 ++-
- src/value/eval_logic.ml | 11 +++++-
- src/value/eval_stmts.ml | 15 +++++---
- 10 files changed, 95 insertions(+), 53 deletions(-)
-
-diff --git a/Changelog b/Changelog
-index 909b359..e60a3ba 100644
---- a/Changelog
-+++ b/Changelog
-@@ -12,6 +12,27 @@
- # '#?nnn' : OLD-BTS entry #nnn
#
-
###############################################################################
-
-+-* Value [2011/12/05] An alarm could be omitted on *p = lval;
-+ when p could point into a read-only location such as a string
-+ constant. Fixed.
-+o* Value [2011/12/05] Fix option -absolute-valid-range being reset by
-+ project copies.
-+-* Value [2011/12/05] Fix wrong hash function, which could cause
-+ memory overuse and worse.
-+- Value [2011/10/25] Improve interpretation of ACSL annotations in
-+ presence of typedefs.
-+-* From [2011/10/21] The interpretation of explicit assigns clauses for
-+ library function "assigns *p \from x;" was wrong: every possible
-+ location was assumed to have been overwritten.
-+- Value [2011/10/18] Improve evaluation of logic when option
-+ -val-signed-overflow-alarms is active.
-+-* Value [2011/10/17] Fixed crash when a library function is called in
-+ a state where the function's precondition cannot be true.
-+-* Value [2011/10/10] Fixed spurious alarm \valid(p) in *p = e; when e is
-+ completely invalid. Soundness was not affected (the
-+ alarm for whatever made e invalid was present).
-+
-+
- #####################################
- Open Source Release Nitrogen_20111001
- #####################################
-diff --git a/src/ai/base.ml b/src/ai/base.ml
-index 5669a8c..45659d0 100644
---- a/src/ai/base.ml
-+++ b/src/ai/base.ml
-@@ -117,12 +117,14 @@ let bits_sizeof v =
- | Var (v,_) | Initialized_Var (v,_) ->
- Bit_utils.sizeof_vid v
-
-+let dep_absolute = [Kernel.AbsoluteValidRange.self]
-+
- module MinValidAbsoluteAddress =
- State_builder.Ref
- (Abstract_interp.Int)
- (struct
- let name = "MinValidAbsoluteAddress"
-- let dependencies = []
-+ let dependencies = dep_absolute
- let kind = `Internal
- let default () = Abstract_interp.Int.zero
- end)
-@@ -132,7 +134,7 @@ module MaxValidAbsoluteAddress =
- (Abstract_interp.Int)
- (struct
- let name = "MaxValidAbsoluteAddress"
-- let dependencies = []
-+ let dependencies = dep_absolute
- let kind = `Internal
- let default () = Abstract_interp.Int.minus_one
- end)
-diff --git a/src/from/from_register.ml b/src/from/from_register.ml
-index ca13011..deae68a 100644
---- a/src/from/from_register.ml
-+++ b/src/from/from_register.ml
-@@ -716,11 +716,12 @@ let compute_using_prototype_for_state state kf =
- !Properties.Interp.loc_to_loc ~result:None state
- out.it_content
- in
-+ let exact = Locations.Location_Bits.cardinal_zero_or_one
output_loc.loc in
- let output_zone =
- Locations.valid_enumerate_bits ~for_writing:true
- output_loc
- in
-- Lmap_bitwise.From_Model.add_binding ~exact:true
-+ Lmap_bitwise.From_Model.add_binding ~exact
- acc output_zone (input_zone ins)
- with Invalid_argument "not an lvalue" ->
- From_parameters.result
-diff --git a/src/lib/rangemap.ml b/src/lib/rangemap.ml
-index 67a58cd..a93953e 100644
---- a/src/lib/rangemap.ml
-+++ b/src/lib/rangemap.ml
-@@ -88,7 +88,7 @@ module Make(Ord: Datatype.S)(Value: Datatype.S) = struct
- | Node(_,_,_,_,h,_) -> h
-
- let hash = function
-- | Empty -> 13
-+ | Empty -> 0
- | Node(_,_,_,_,_,h) -> h
-
-
-@@ -126,7 +126,7 @@ module Make(Ord: Datatype.S)(Value: Datatype.S) = struct
- let hl = height l and hr = height r in
- let hashl = hash l and hashr = hash r in
- let hashbinding = Hashtbl.hash (x_h, d_h) in
-- let hashtree = 289 (* =17*17 *) * hashl + 17 * hashbinding + hashr in
-+ let hashtree = hashl lxor hashbinding lxor hashr in
- Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1), hashtree)
-
- let bal l x d r =
-diff --git a/src/memory_state/lmap.ml b/src/memory_state/lmap.ml
-index 9867584..8786e5b 100644
---- a/src/memory_state/lmap.ml
-+++ b/src/memory_state/lmap.ml
-@@ -943,7 +943,7 @@ let is_included =
- let plevel = Kernel.ArrayPrecisionLevel.get() in
- let treat_dst k_dst i_dst (acc_lmap : LBase.t) =
- if Base.is_read_only k_dst
-- then acc_lmap
-+ then (CilE.warn_mem_write with_alarms; acc_lmap)
- else
- let validity = Base.validity k_dst in
- let offsetmap_dst = LBase.find_or_default k_dst m in
-diff --git a/src/value/eval_exprs.ml b/src/value/eval_exprs.ml
-index 543bc91..73b5349 100644
---- a/src/value/eval_exprs.ml
-+++ b/src/value/eval_exprs.ml
-@@ -960,7 +960,7 @@ and eval_expr_with_deps_state ~with_alarms deps state e =
- (* Can raise a pointer comparison. CilE needs a binop there *)
- in
- CilE.set_syntactic_context syntactic_context;
-- let result = eval_unop ~with_alarms expr t op in
-+ let result = eval_unop ~check_overflow:true ~with_alarms expr t op in
- state, deps, result
- in
- let r =
-@@ -979,46 +979,49 @@ and eval_expr_with_deps_state ~with_alarms deps state e =
- | _ -> ()); *)
- state, deps, rr
-
--and eval_unop ~with_alarms expr t op =
-+(* This function evaluates a unary minus, but does _not_ check for overflows.
-+ This is left to the caller *)
-+and eval_uneg_exp ~with_alarms expr t =
-+ match unrollType t with
-+ | TFloat _ ->
-+ (try
-+ let v = V.project_ival expr in
-+ let f = Ival.project_float v in
-+ V.inject_ival
-+ (Ival.inject_float (Ival.Float_abstract.neg_float f))
-+ with
-+ V.Not_based_on_null ->
-+ begin match with_alarms.CilE.others with
-+ | CilE.Aignore -> ()
-+ | CilE.Acall f -> f()
-+ | CilE.Alog _ ->
-+ warning_once_current
-+ "converting address to float: assert(TODO)"
-+ end;
-+ V.topify_arith_origin expr
-+ | Ival.Float_abstract.Nan_or_infinite ->
-+ begin match with_alarms.CilE.others with
-+ | CilE.Aignore -> ()
-+ | CilE.Acall f -> f()
-+ | CilE.Alog _ ->
-+ warning_once_current
-+ "converting value to float: assert (TODO)"
-+ end;
-+ V.top_float
-+ )
-+ | _ ->
-+ try
-+ let v = V.project_ival expr in
-+ V.inject_ival (Ival.neg v)
-+ with V.Not_based_on_null -> V.topify_arith_origin expr
-+
-+and eval_unop ~check_overflow ~with_alarms expr t op =
- match op with
- | Neg ->
-- let t = unrollType t in
-- (match t with TFloat _ ->
-- (try
-- let v = V.project_ival expr in
-- let f = Ival.project_float v in
-- V.inject_ival
-- (Ival.inject_float (Ival.Float_abstract.neg_float f))
-- with
-- V.Not_based_on_null ->
-- begin match with_alarms.CilE.others with
-- CilE.Aignore -> ()
-- | CilE.Acall f -> f()
-- | CilE.Alog _ ->
-- warning_once_current
-- "converting address to float: assert(TODO)"
-- end;
-- V.topify_arith_origin expr
-- | Ival.Float_abstract.Nan_or_infinite ->
-- begin match with_alarms.CilE.others with
-- CilE.Aignore -> ()
-- | CilE.Acall f -> f()
-- | CilE.Alog _ ->
-- warning_once_current
-- "converting value to float: assert (TODO)"
-- end;
-- V.top_float
-- )
-- | _ ->
-- let result =
-- try
-- let v = V.project_ival expr in
-- V.inject_ival (Ival.neg v)
-- with V.Not_based_on_null -> V.topify_arith_origin expr
-- in
-- handle_signed_overflow ~with_alarms t result
-- )
--
-+ let r = eval_uneg_exp ~with_alarms expr t in
-+ if check_overflow
-+ then handle_signed_overflow ~with_alarms t r
-+ else r
- | BNot ->
- (try
- let v = V.project_ival expr in
-diff --git a/src/value/eval_exprs.mli b/src/value/eval_exprs.mli
-index 3914cb8..4f76da5 100644
---- a/src/value/eval_exprs.mli
-+++ b/src/value/eval_exprs.mli
-@@ -50,6 +50,7 @@ val eval_binop_int :
- Cvalue.V.t -> binop -> Cvalue.V.t -> Cvalue.V.t
-
- val eval_unop:
-+ check_overflow:bool ->
- with_alarms:CilE.warn_mode ->
- Cvalue.V.t ->
- typ (** Type of the expression under the unop *) ->
-diff --git a/src/value/eval_funs.ml b/src/value/eval_funs.ml
-index 5db6453..4d1c0f4 100644
---- a/src/value/eval_funs.ml
-+++ b/src/value/eval_funs.ml
-@@ -166,7 +166,9 @@ let compute_using_prototype kf ~active_behaviors
~state_with_formals =
- (Kernel_function.get_name kf)
- Cvalue.Model.pretty state_with_formals; *)
- let vi = Kernel_function.get_vi kf in
-- if Cil.hasAttribute "noreturn" vi.vattr then
-+ if (not (Cvalue.Model.is_reachable state_with_formals)) ||
-+ Cil.hasAttribute "noreturn" vi.vattr
-+ then
- None, Cvalue.Model.bottom, Location_Bits.Top_Param.bottom
- else
- let return_type,_formals_type,_inline,_attr =
-diff --git a/src/value/eval_logic.ml b/src/value/eval_logic.ml
-index 52d5276..4be53b6 100644
---- a/src/value/eval_logic.ml
-+++ b/src/value/eval_logic.ml
-@@ -255,7 +255,9 @@ let rec eval_term env result t =
- | BNot -> t (* can only be used on an integer type *)
- | LNot -> intType
- in
-- let eval typ v = eval_unop ~with_alarms v typ op in
-+ let eval typ v =
-+ eval_unop ~check_overflow:false ~with_alarms v typ op
-+ in
- List.map (fun (typ, v) -> typ' typ, eval typ v) l
-
- | Trange (otlow, othigh) ->
-@@ -405,6 +407,11 @@ let eval_term_as_exact_loc env result t =
- )
- | _ -> raise Not_an_exact_loc
-
-+let isPointerCType ct =
-+ match unrollType ct with
-+ TPtr _ -> true
-+ | _ -> false
-+
- let rec reduce_by_predicate ~result env positive p =
- let result =
- match positive,p.content with
-@@ -459,7 +466,7 @@ let rec reduce_by_predicate ~result env positive p =
- | t when isLogicRealOrFloatType t ->
- eval_float (Value_parameters.AllRoundingModes.get ())
- | t when isLogicIntegralType t -> eval_int
-- | Ctype (TPtr _) -> eval_int
-+ | Ctype (ct) when isPointerCType ct -> eval_int
- | _ -> raise Predicate_alarm
- in
- reduce_by_relation eval ~result env positive t1 op t2
-diff --git a/src/value/eval_stmts.ml b/src/value/eval_stmts.ml
-index ca95ff7..64f2415 100644
---- a/src/value/eval_stmts.ml
-+++ b/src/value/eval_stmts.ml
-@@ -562,12 +562,17 @@ struct
- mem_e
- reduced_state
- in
-- if not (Cvalue.Model.is_reachable new_reduced_state)
-+ if (Cvalue.Model.is_reachable reduced_state) &&
-+ not (Cvalue.Model.is_reachable new_reduced_state)
- then begin
-- CilE.set_syntactic_context (CilE.SyMem lv);
-- CilE.warn_mem_write with_alarms ;
-- Value_parameters.result ~current:true
-- "all target addresses were invalid. This path is assumed to be
dead.";
-+(* Value_parameters.result ~current:true
-+ "REDUCED:@.%a@.TO:@.%a@."
-+ Cvalue.Model.pretty reduced_state
-+ Cvalue.Model.pretty new_reduced_state; *)
-+ CilE.set_syntactic_context (CilE.SyMem lv);
-+ CilE.warn_mem_write with_alarms ;
-+ Value_parameters.result ~current:true
-+ "all target addresses were invalid. This path is assumed to be dead.";
- end;
- new_reduced_state
- (* | Var _ , Index _ -> assert false
---
diff --git a/debian/patches/series b/debian/patches/series
index c2fedb3..06464b6 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,6 +1,3 @@
-0001-Add-ocamlgraph-to-DYN_-O-B-LINKFLAGS.patch
-0002-Accept-ocamlgraph-1.8.patch
-0003-Fix-spelling-error-in-binary.patch
-0004-Use-bin-cp-instead-of-usr-bin-install.patch
-0005-Disable-CHMOD_RO-invocations.patch
-0006-Patchlevel2-for-Nitrogen-20111001.patch
+0001-Fix-spelling-error-in-binary.patch
+0002-Use-bin-cp-instead-of-usr-bin-install.patch
+0003-Disable-CHMOD_RO-invocations.patch
--
frama-c packaging
_______________________________________________
Pkg-ocaml-maint-commits mailing list
Pkg-ocaml-maint-commits@lists.alioth.debian.org
http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
