Merge branch 'bugfix/basile/eacsl-result-module' into 'master'

[eacsl] Replace `Result.t` with `Error.result`

See merge request frama-c/frama-c!3547

src/plugins/e-acsl/Makefile.in

@@ -39,7 +39,6 @@ endif
 
 # libraries
 SRC_LIBRARIES:= \
-	result \
 	error \
 	builtins \
 	functions \

src/plugins/e-acsl/headers/header_spec.txt

@@ -161,8 +161,6 @@ src/libraries/logic_aggr.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/libraries/logic_aggr.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/libraries/misc.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/libraries/misc.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/libraries/result.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/libraries/result.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/libraries/varname.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/libraries/varname.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/local_config.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL

src/plugins/e-acsl/src/analyses/bound_variables.ml

@@ -83,11 +83,11 @@ module Quantified_predicate =
 module Quantifier: sig
   val add:
     predicate ->
-    ((term * logic_var * term) list * predicate) Result.t ->
+    ((term * logic_var * term) list * predicate) Error.result ->
     unit
   val get:
     predicate ->
-    ((term * logic_var * term) list * predicate) Result.t
+    ((term * logic_var * term) list * predicate) Error.result
   (** getter and setter for the additional guard that intersects with the type
       of the variable *)
   val get_guard_for_small_type : logic_var -> predicate option
@@ -115,7 +115,7 @@ end = struct
     Cil_datatype.Logic_var.Hashtbl.add guard_tbl lv p
 
   let replace p guarded_vars goal =
-    Quantified_predicate.Hashtbl.replace tbl p (Result.Res (guarded_vars, goal))
+    Quantified_predicate.Hashtbl.replace tbl p (Result.Ok (guarded_vars, goal))
 
   let clear () =
     Cil_datatype.Logic_var.Hashtbl.clear guard_tbl;
@@ -668,9 +668,9 @@ let compute_guards loc ~is_forall p bounded_vars hyps =
     let guards,goal = compute_quantif_guards p ~is_forall bounded_vars hyps in
     (* transform [guards] into [lscope_var list] *)
     let normalized_guards = List.map (normalize_guard ~loc) guards
-    in Quantifier.add p (Result.Res (normalized_guards,goal))
+    in Quantifier.add p (Result.Ok (normalized_guards,goal))
   with exn ->
-    Quantifier.add p (Result.Err exn)
+    Quantifier.add p (Result.Error exn)
 
 module Preprocessor : sig
   val compute : file -> unit
@@ -689,11 +689,11 @@ end
     | Pforall _ ->
       Quantifier.add
         p
-        (Result.Err (Error.make_not_yet "unguarded \\forall quantification"))
+        (Result.Error (Error.make_not_yet "unguarded \\forall quantification"))
     | Pexists _ ->
       Quantifier.add
         p
-        (Result.Err (Error.make_not_yet "unguarded \\exists quantification"))
+        (Result.Error (Error.make_not_yet "unguarded \\exists quantification"))
     | _ -> ()
 
   let do_user_predicates () =

src/plugins/e-acsl/src/analyses/bound_variables.mli

@@ -23,7 +23,7 @@
 open Cil_types
 
 val get_preprocessed_quantifier:
-  predicate -> ((term * logic_var * term) list * predicate) Result.t
+  predicate -> ((term * logic_var * term) list * predicate) Error.result
 (** @return the preprocessed of a quantified predicate the
     [(term * logic_var * term) list] is the list of all the quantified variables
     along with their syntactic guards, and the [predicate] is the goal: the

src/plugins/e-acsl/src/analyses/typing.ml

@@ -198,9 +198,9 @@ module Memo: sig
     lenv:Function_params_ty.t ->
     (term -> computed_info) ->
     term ->
-    computed_info Result.t
+    computed_info Error.result
   val get: lenv:Function_params_ty.t -> term ->
-    computed_info Result.t
+    computed_info Error.result
   val clear: unit -> unit
 end = struct
 
@@ -218,7 +218,7 @@ end = struct
        the guard and once for encoding [x+1] when incrementing it. The
        memoization is only useful here and indeed prevent the generation of one
        extra variable in some cases. *)
-  let tbl : computed_info Result.t Misc.Id_term.Hashtbl.t =
+  let tbl : computed_info Error.result Misc.Id_term.Hashtbl.t =
     Misc.Id_term.Hashtbl.create 97
 
   (* The type of the logic function
@@ -231,7 +231,7 @@ end = struct
      We distinguish the calls to the function by storing the type of the
      arguments corresponding to each call, and we weaken the typing so that it
      is invariant when the arguments have the same type. *)
-  let dep_tbl : computed_info Result.t Id_term_with_lenv.Hashtbl.t
+  let dep_tbl : computed_info Error.result Id_term_with_lenv.Hashtbl.t
     = Id_term_with_lenv.Hashtbl.create 97
 
   let get_dep lenv t =
@@ -251,8 +251,8 @@ end = struct
     try Misc.Id_term.Hashtbl.find tbl t
     with Not_found ->
       let x =
-        try Result.Res (f t)
-        with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Err exn
+        try Result.Ok (f t)
+        with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Error exn
       in
       Misc.Id_term.Hashtbl.add tbl t x;
       x
@@ -262,8 +262,8 @@ end = struct
       Id_term_with_lenv.Hashtbl.find dep_tbl (t, lenv)
     with Not_found ->
       let x =
-        try Result.Res (f t)
-        with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Err exn
+        try Result.Ok (f t)
+        with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Error exn
       in
       Id_term_with_lenv.Hashtbl.add dep_tbl (t, lenv) x;
       x
@@ -689,8 +689,8 @@ let rec type_term
          | Some ctx -> coerce ~arith_operand ~ctx ~op ty)
       t
   with
-  | Res res -> res
-  | Err exn -> raise exn
+  | Result.Ok res -> res
+  | Result.Error exn -> raise exn
 
 and type_term_lval ~lenv (host, offset) =
   type_term_lhost ~lenv host;

src/plugins/e-acsl/src/libraries/error.ml

@@ -32,6 +32,7 @@ module Exn = struct
 end
 
 module type S = sig
+  type 'a result = ('a, exn) Result.t
   include module type of Exn
   val make_untypable: string -> exn
   val make_not_yet: string -> exn
@@ -44,13 +45,19 @@ module type S = sig
   val generic_handle: ('a -> 'b) -> 'b -> 'a -> 'b
   val retrieve_preprocessing:
     string ->
-    ('a -> 'b Result.t) ->
+    ('a -> 'b result) ->
     'a ->
     (Format.formatter -> 'a -> unit) ->
     'b
+  val pp_result:
+    (Format.formatter -> 'a -> unit) ->
+    Format.formatter ->
+    'a result ->
+    unit
 end
 
 module Make_with_opt(P: sig val phase:Options.category option end): S = struct
+  type 'a result = ('a, exn) Result.t
   include Exn
 
   let make_untypable msg = Typing_error (P.phase, msg)
@@ -105,14 +112,19 @@ module Make_with_opt(P: sig val phase:Options.category option end): S = struct
   let retrieve_preprocessing analyse_name getter parameter pp =
     try
       match getter parameter with
-      | Result.Res res -> res
-      | Result.Err exn -> raise exn
+      | Result.Ok res -> res
+      | Result.Error exn -> raise exn
     with Not_memoized phase ->
       Options.fatal
         "@[%s was not performed on construct %a%a@]"
         analyse_name
         pp parameter
         pp_phase phase
+
+  let pp_result pp fmt res =
+    match res with
+    | Result.Ok a -> Format.fprintf fmt "@[%a@]" pp a
+    | Result.Error err -> Format.fprintf fmt "@[%s@]" (Printexc.to_string err)
 end
 
 module Make(P: sig val phase:Options.category end): S =

src/plugins/e-acsl/src/libraries/error.mli

@@ -23,6 +23,9 @@
 (** Handling errors. *)
 
 module type S = sig
+  type 'a result = ('a, exn) Result.t
+  (** Represent either a result of type ['a] or an error with an exception. *)
+
   exception Typing_error of Options.category option * string
   (** Typing error where the first element is the phase where the error occured
       and the second element is the error message. *)
@@ -65,13 +68,21 @@ module type S = sig
 
   val retrieve_preprocessing:
     string ->
-    ('a -> 'b Result.t) ->
+    ('a -> 'b result) ->
     'a ->
     (Format.formatter -> 'a -> unit) ->
     'b
-    (** Retrieve the result of a preprocessing phase, which possibly failed.
-        The [string] argument and the formatter are used to display a message in
-        case the preprocessing phase did not compute the required result. *)
+  (** Retrieve the result of a preprocessing phase, which possibly failed.
+      The [string] argument and the formatter are used to display a message in
+      case the preprocessing phase did not compute the required result. *)
+
+  val pp_result:
+    (Format.formatter -> 'a -> unit) ->
+    Format.formatter ->
+    'a result ->
+    unit
+    (** [pp_result pp] where [pp] is a formatter for ['a] returns a formatter for
+        ['a result]. *)
 end
 
 (** Functor to build an [Error] module for a given [phase]. *)

src/plugins/e-acsl/src/libraries/result.ml

-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
-(*                                                                        *)
-(*  Copyright (C) 2012-2021                                               *)
-(*    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 holding a result or an exception *)
-
-type 'a t = Res of 'a | Err of exn
-
-let pretty pp fmt result =
-  match result with
-  | Res a -> Format.fprintf fmt "@[%a@]" pp a
-  | Err err -> Format.fprintf fmt "@[%s@]" (Printexc.to_string err)

src/plugins/e-acsl/src/libraries/result.mli

-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
-(*                                                                        *)
-(*  Copyright (C) 2012-2021                                               *)
-(*    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 holding a result or an exception *)
-
-(** Represent either a result of type ['a] or an error with an exception *)
-type 'a t = Res of 'a | Err of exn
-
-val pretty:
-  (Format.formatter -> 'a -> unit) ->
-  Format.formatter ->
-  'a t ->
-  unit
-(** [pretty pp] where [pp] is a formatter for ['a] returns a formatter for
-    ['a t]. *)