[Eva] Removes warn.ml file.

Both warnings are inlined in cvalue_transfer and locals_scoping.

src/plugins/eva/domains/cvalue/cvalue_offsetmap.ml

@@ -22,23 +22,6 @@
 
 open Eval
 
-exception Got_imprecise of Cvalue.V.t
-let offsetmap_contains_imprecision offs =
-  try
-    Cvalue.V_Offsetmap.iter_on_values
-      (fun v ->
-         match Cvalue.V_Or_Uninitialized.get_v v with
-         | Locations.Location_Bytes.Map _ -> ()
-         | Locations.Location_Bytes.Top _ as v -> raise (Got_imprecise v)
-      ) offs;
-    None
-  with Got_imprecise v -> Some v
-
-let warn_right_imprecision lval loc offsetmap =
-  match offsetmap_contains_imprecision offsetmap with
-  | Some v -> Warn.warn_right_exp_imprecision lval loc v
-  | None -> ()
-
 let offsetmap_of_v ~typ v =
   let size = Integer.of_int (Cil.bitsSizeOf typ) in
   let v = Cvalue.V.anisotropic_cast ~size v in

src/plugins/eva/domains/cvalue/cvalue_offsetmap.mli

@@ -25,12 +25,6 @@
 open Cil_types
 open Cvalue
 
-(** [warn_right_imprecision lval loc offsm] is used for the assignment of the
-    lvalue [lval] pointing to the location [loc]; it warns if the offsetmap
-    [offsm] contains a garbled mix. *)
-val warn_right_imprecision:
-  lval -> Locations.location -> V_Offsetmap.t -> unit
-
 (** Computes the offsetmap for an assignment:
     - in case of a copy, extracts the offsetmap from the state;
     - otherwise, translates the value assigned into an offsetmap. *)

src/plugins/eva/domains/cvalue/cvalue_transfer.ml

@@ -32,6 +32,52 @@ let unbottomize = function
   | `Bottom -> Cvalue.V.bottom
   | `Value v -> v
 
+(* ---------------------------------------------------------------------- *)
+(*                        Garbled mix warnings                            *)
+(* ---------------------------------------------------------------------- *)
+
+(* When computing the result of [lv = exp], warn if the evaluation of [exp]
+   results in an imprecision. [loc_lv] is the location pointed to by [lv].
+   [exp_val] is the part of the evaluation of [exp] that is imprecise. *)
+let warn_right_exp_imprecision lv loc_lv exp_val =
+  match exp_val with
+  | Locations.Location_Bytes.Top (topparam, origin) ->
+    Origin.register_write topparam origin;
+    Self.warning ~wkey:Self.wkey_garbled_mix_write ~once:true ~current:true
+      "@[<v>@[Assigning imprecise value to %a%t.@]%a%t@]"
+      Printer.pp_lval lv
+      (fun fmt -> match lv with
+         | (Mem _, _) ->
+           Format.fprintf fmt "@ (pointing to %a)"
+             (Locations.pretty_english ~prefix:false) loc_lv
+         | (Var _, _) -> ())
+      (fun fmt org ->
+         if not (Origin.is_unknown origin) then
+           Format.fprintf fmt
+             "@ @[The imprecision@ originates@ from@ %a@]"
+             Origin.pretty org)
+      origin
+      Eva_utils.pp_callstack
+  | Locations.Location_Bytes.Map _ -> ()
+
+let offsetmap_contains_imprecision offs =
+  let exception Got_imprecise of Cvalue.V.t in
+  try
+    Cvalue.V_Offsetmap.iter_on_values
+      (fun v ->
+         match Cvalue.V_Or_Uninitialized.get_v v with
+         | Locations.Location_Bytes.Map _ -> ()
+         | Locations.Location_Bytes.Top _ as v -> raise (Got_imprecise v)
+      ) offs;
+    None
+  with Got_imprecise v -> Some v
+
+let warn_right_imprecision lval loc offsetmap =
+  match offsetmap_contains_imprecision offsetmap with
+  | Some v -> warn_right_exp_imprecision lval loc v
+  | None -> ()
+
+
 (* ---------------------------------------------------------------------- *)
 (*                               Assumptions                              *)
 (* ---------------------------------------------------------------------- *)
@@ -90,7 +136,7 @@ let update valuation t =
 let write_abstract_value state (lval, loc, typ) assigned_value =
   let {v; initialized; escaping} = assigned_value in
   let value = unbottomize v in
-  Warn.warn_right_exp_imprecision lval loc value;
+  warn_right_exp_imprecision lval loc value;
   let value =
     if Cil.typeHasQualifier "volatile" typ
     then Cvalue_forward.make_volatile value
@@ -137,7 +183,7 @@ let copy_one_loc state left_lv right_lv =
     in
     if not (Eval_typ.offsetmap_matches_type left_typ offsetmap) then
       raise Do_assign_imprecise_copy;
-    Cvalue_offsetmap.warn_right_imprecision left_lval left_loc offsetmap;
+    warn_right_imprecision left_lval left_loc offsetmap;
     `Value
       (paste_offsetmap ~exact:true
          ~from:offsetmap ~dst_loc:left_loc.Locations.loc ~size state)

src/plugins/eva/domains/cvalue/locals_scoping.ml

@@ -54,6 +54,17 @@ let offsetmap_contains_local offm =
   with Exit -> true
 
 
+let warn_locals_escape is_block fundec k locals =
+  let pretty_base = Base.pretty in
+  let pretty_block fmt = Pretty_utils.pp_cond is_block fmt "a block of " in
+  let sv = fundec.svar in
+  Self.warning
+    ~wkey:Self.wkey_locals_escaping
+    ~current:true ~once:true
+    "locals %a escaping the scope of %t%a through %a"
+    Base.Hptset.pretty locals pretty_block Printer.pp_varinfo sv pretty_base k
+
+
 (* Rebuild [offsm] by applying [f] to the bindings that verify [test].
    Also call [warn] in this case. *)
 let rebuild_offsetmap f warn offsm =
@@ -123,7 +134,7 @@ let make_escaping_fundec fundec clob vars state =
         | Base.SetLattice.Top -> escaping
         | Base.SetLattice.Set bases -> Base.Hptset.inter bases escaping
       in
-      Warn.warn_locals_escape is_inner_block fundec b bases
+      warn_locals_escape is_inner_block fundec b bases
     in
     make_escaping ~exact:true ~escaping ~on_escaping ~within:clob.clob state
 

src/plugins/eva/domains/cvalue/warn.ml

-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of Frama-C.                                         *)
-(*                                                                        *)
-(*  Copyright (C) 2007-2023                                               *)
-(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
-(*         alternatives)                                                  *)
-(*                                                                        *)
-(*  you can redistribute it and/or modify it under the terms of the GNU   *)
-(*  Lesser General Public License as published by the Free Software       *)
-(*  Foundation, version 2.1.                                              *)
-(*                                                                        *)
-(*  It is distributed in the hope that it will be useful,                 *)
-(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
-(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
-(*  GNU Lesser General Public License for more details.                   *)
-(*                                                                        *)
-(*  See the GNU Lesser General Public License version 2.1                 *)
-(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-open Cil_types
-open Locations
-
-let warn_locals_escape is_block fundec k locals =
-  let pretty_base = Base.pretty in
-  let pretty_block fmt = Pretty_utils.pp_cond is_block fmt "a block of " in
-  let sv = fundec.svar in
-  Self.warning
-    ~wkey:Self.wkey_locals_escaping
-    ~current:true ~once:true
-    "locals %a escaping the scope of %t%a through %a"
-    Base.Hptset.pretty locals pretty_block Printer.pp_varinfo sv pretty_base k
-
-(* Auxiliary function for [do_assign] below. When computing the
-   result of [lv = exp], warn if the evaluation of [exp] results in
-   an imprecision. [loc_lv] is the location pointed to by [lv].
-   [exp_val] is the part of the evaluation of [exp] that is imprecise. *)
-let warn_right_exp_imprecision lv loc_lv exp_val =
-  match exp_val with
-  | Location_Bytes.Top(topparam, origin) ->
-    Origin.register_write topparam origin;
-    Self.warning ~wkey:Self.wkey_garbled_mix_write ~once:true ~current:true
-      "@[<v>@[Assigning imprecise value to %a%t.@]%a%t@]"
-      Printer.pp_lval lv
-      (fun fmt -> match lv with
-         | (Mem _, _) ->
-           Format.fprintf fmt "@ (pointing to %a)"
-             (Locations.pretty_english ~prefix:false) loc_lv
-         | (Var _, _) -> ())
-      (fun fmt org ->
-         if not (Origin.is_unknown origin) then
-           Format.fprintf fmt
-             "@ @[The imprecision@ originates@ from@ %a@]"
-             Origin.pretty org)
-      origin
-      Eva_utils.pp_callstack
-  | Location_Bytes.Map _ -> ()
-
-
-(*
-Local Variables:
-compile-command: "make -C ../../../.."
-End:
-*)

src/plugins/eva/domains/cvalue/warn.mli

-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of Frama-C.                                         *)
-(*                                                                        *)
-(*  Copyright (C) 2007-2023                                               *)
-(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
-(*         alternatives)                                                  *)
-(*                                                                        *)
-(*  you can redistribute it and/or modify it under the terms of the GNU   *)
-(*  Lesser General Public License as published by the Free Software       *)
-(*  Foundation, version 2.1.                                              *)
-(*                                                                        *)
-(*  It is distributed in the hope that it will be useful,                 *)
-(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
-(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
-(*  GNU Lesser General Public License for more details.                   *)
-(*                                                                        *)
-(*  See the GNU Lesser General Public License version 2.1                 *)
-(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-(** Alarms and imprecision warnings emitted during the analysis. *)
-
-open Cil_types
-open Locations
-
-val warn_locals_escape: bool -> fundec -> Base.t -> Base.Hptset.t -> unit
-val warn_right_exp_imprecision: lval -> location -> Cvalue.V.t -> unit