[Pkg-ocaml-maint-commits] [SCM] frama-c packaging branch, master, updated. debian/20111001+nitrogen+dfsg-2-1-g9d7da41
Mehdi Dogguy
mehdi at debian.org
Fri Jan 6 09:01:12 UTC 2012
The following commit has been merged in the master branch:
commit 9d7da4102bfd0599c1ff00aa44d41bb8893384f3
Author: Mehdi Dogguy <mehdi at debian.org>
Date: Fri Jan 6 09:31:41 2012 +0100
Patchlevel2 for Nitrogen 20111001
diff --git a/debian/changelog b/debian/changelog
index e9087f6..be17c9b 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,10 @@
+frama-c (20111001+nitrogen+dfsg-3) unstable; urgency=low
+
+ * Include patchlevel2 for Nitrogen 20111001.
+ - add debian/patches/0006-Patchlevel2-for-Nitrogen-20111001.patch
+
+ -- Mehdi Dogguy <mehdi at debian.org> Fri, 06 Jan 2012 09:30:44 +0100
+
frama-c (20111001+nitrogen+dfsg-2) unstable; urgency=low
* add 0005-Disable-CHMOD_RO-invocations.patch.
diff --git a/debian/patches/0006-Patchlevel2-for-Nitrogen-20111001.patch b/debian/patches/0006-Patchlevel2-for-Nitrogen-20111001.patch
new file mode 100644
index 0000000..c1f224a
--- /dev/null
+++ b/debian/patches/0006-Patchlevel2-for-Nitrogen-20111001.patch
@@ -0,0 +1,323 @@
+From: Mehdi Dogguy <mehdi at 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 at .TO:@.%a at ."
++ 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 ae3a88c..c2fedb3 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -3,3 +3,4 @@
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
--
frama-c packaging
More information about the Pkg-ocaml-maint-commits
mailing list