[Eva] add support for Top polymorphic variant

Makefile

@@ -587,6 +587,7 @@ KERNEL_CMO=\
 	src/kernel_services/abstract_interp/lattice_messages.cmo        \
 	src/kernel_services/abstract_interp/abstract_interp.cmo         \
 	src/kernel_services/abstract_interp/bottom.cmo                  \
+	src/kernel_services/abstract_interp/top.cmo                     \
 	src/kernel_services/abstract_interp/int_Base.cmo                \
 	src/kernel_services/analysis/bit_utils.cmo                      \
 	src/kernel_services/abstract_interp/fc_float.cmo                \

headers/header_spec.txt

@@ -525,6 +525,8 @@ src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.mli: CEA_LGP
 src/kernel_services/abstract_interp/offsetmap_sig.mli: CEA_LGPL
 src/kernel_services/abstract_interp/origin.ml: CEA_LGPL
 src/kernel_services/abstract_interp/origin.mli: CEA_LGPL
+src/kernel_services/abstract_interp/top.ml: CEA_LGPL
+src/kernel_services/abstract_interp/top.mli: CEA_LGPL
 src/kernel_services/abstract_interp/tr_offset.ml: CEA_LGPL
 src/kernel_services/abstract_interp/tr_offset.mli: CEA_LGPL
 src/kernel_services/analysis/README.md: .ignore

src/kernel_services/abstract_interp/top.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2022                                               *)
+(*    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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+type 'a or_top = [ `Value of 'a | `Top ]
+
+(** Combination *)
+
+let zip x y =
+  match x, y with
+  | `Top, _ | _, `Top -> `Top
+  | `Value x, `Value y -> `Value (x,y)
+
+(** Operators *)
+
+module Type = struct
+  type 'a or_top = [ `Value of 'a | `Top ]
+
+  let (>>-) t f = match t with
+    | `Top -> `Top
+    | `Value t -> f t
+
+  let (>>-:) t f = match t with
+    | `Top -> `Top
+    | `Value t -> `Value (f t)
+
+  let (let+) = (>>-:)
+  let (and+) = zip
+  let (let*) = (>>-)
+  let (and*) = zip
+end
+
+(** Conversion. *)
+
+let of_option = function
+  | None -> `Top
+  | Some x -> `Value x
+
+let to_option = function
+  | `Top -> None
+  | `Value x -> Some x
+
+(** Pretty printing. *)
+
+let pretty_top fmt =
+  Format.pp_print_string fmt (Unicode.top_string ())
+
+let pretty pp fmt = function
+  | `Top -> pretty_top fmt
+  | `Value v -> pp fmt v

src/kernel_services/abstract_interp/top.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2022                                               *)
+(*    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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Types, monads and utilitary functions for lattices in which the top is
+    managed separately from other values. *)
+
+module Type : sig
+  type 'a or_top = [ `Value of 'a | `Top ]
+
+  (** This monad propagates the `Bottom value if needed. *)
+  val (>>-) : 'a or_top -> ('a -> 'b or_top) -> 'b or_top
+
+  (** Use this monad if the following function returns a simple value. *)
+  val (>>-:) : 'a or_top -> ('a -> 'b) -> 'b or_top
+
+  (** Binding operators, applicative syntax *)
+  val (let+) : 'a or_top -> ('a -> 'b) -> 'b or_top
+  val (and+) : 'a or_top -> 'b or_top -> ('a * 'b) or_top
+
+  (** Binding operators, monad syntax *)
+  val (let*) : 'a or_top -> ('a -> 'b or_top) -> 'b or_top
+  val (and*) : 'a or_top -> 'b or_top -> ('a * 'b) or_top
+end
+
+type 'a or_top = 'a Type.or_top
+
+(** Combination, if one is `Top, the combination is `Top *)
+val zip : 'a or_top -> 'b or_top -> ('a * 'b) or_top
+
+(** Conversion. *)
+val to_option : 'a or_top -> 'a option
+val of_option : 'a option -> 'a or_top
+
+(** Pretty printing. *)
+val pretty_top : Format.formatter -> unit (* for %t specifier *)
+val pretty : (Format.formatter -> 'a -> unit) ->
+  Format.formatter -> 'a or_top -> unit