Index: Changelog
===================================================================
--- Changelog	(revision 15681)
+++ Changelog	(revision 15937)
@@ -12,6 +12,20 @@
 # '#?nnn'  : OLD-BTS entry #nnn                                               #
 ###############################################################################
 
+-  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
 #####################################
Index: src/from/from_register.ml
===================================================================
--- src/from/from_register.ml	(revision 15681)
+++ src/from/from_register.ml	(revision 15937)
@@ -716,11 +716,12 @@
                   !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
Index: src/value/eval_exprs.ml
===================================================================
--- src/value/eval_exprs.ml	(revision 15681)
+++ src/value/eval_exprs.ml	(revision 15937)
@@ -960,7 +960,7 @@
               (* 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 @@
   | _ -> ()); *)
   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
Index: src/value/eval_exprs.mli
===================================================================
--- src/value/eval_exprs.mli	(revision 15681)
+++ src/value/eval_exprs.mli	(revision 15937)
@@ -50,6 +50,7 @@
   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 *) ->
Index: src/value/eval_stmts.ml
===================================================================
--- src/value/eval_stmts.ml	(revision 15681)
+++ src/value/eval_stmts.ml	(revision 15937)
@@ -562,12 +562,17 @@
               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
Index: src/value/eval_funs.ml
===================================================================
--- src/value/eval_funs.ml	(revision 15681)
+++ src/value/eval_funs.ml	(revision 15937)
@@ -166,7 +166,9 @@
       (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 =
Index: src/value/eval_logic.ml
===================================================================
--- src/value/eval_logic.ml	(revision 15681)
+++ src/value/eval_logic.ml	(revision 15937)
@@ -255,7 +255,9 @@
           | 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 @@
         )
     | _ -> 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 @@
             | 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