The following commit has been merged in the master branch: commit 9d7da4102bfd0599c1ff00aa44d41bb8893384f3 Author: Mehdi Dogguy <me...@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 <me...@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 <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 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 _______________________________________________ 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