diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 9adf75183d4d77db8012b6edffd3063eeb2d3fe3..8c3bf917e67240eafef14c38769cbac2bb745a7a 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -39,7 +39,6 @@ endif
# libraries
SRC_LIBRARIES:= \
- result \
error \
builtins \
functions \
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 0f167bcdc56cfba05508ea91ef7a3a08120781f5..03276ab748ebabdd0e1e438bc8ed3b32dcdc78ad 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/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
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 344736aa651363d15c8ebb2445f2f6a93a0f3a81..e7eaa96b0cd410bfe1c2ce7def431d9d1a9068c3 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/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 () =
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.mli b/src/plugins/e-acsl/src/analyses/bound_variables.mli
index e3bf6ea78ebe48e89823eda5d9e9548ffe69a0e6..233d77ef6d7843d59e48d5756a02c8bd9d7f7b22 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.mli
+++ b/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
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 8c949b9b18f6b3d79d9f7e40806a6d2fc107b9c4..f23e7f2d050b547d41689b5c49840c6bf9bb8fc3 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/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;
diff --git a/src/plugins/e-acsl/src/libraries/error.ml b/src/plugins/e-acsl/src/libraries/error.ml
index 98e9ecefb42709dd98cb1da72ffc78f41610ad70..4fdf23fe5993d7e7189e82bad9feba010b7361f8 100644
--- a/src/plugins/e-acsl/src/libraries/error.ml
+++ b/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 =
diff --git a/src/plugins/e-acsl/src/libraries/error.mli b/src/plugins/e-acsl/src/libraries/error.mli
index b36dd277dcfd93e3a7e86827356b7fc46cd740c3..c83496560bf0279258eeb0f07534d4aef78f2757 100644
--- a/src/plugins/e-acsl/src/libraries/error.mli
+++ b/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]. *)
diff --git a/src/plugins/e-acsl/src/libraries/result.ml b/src/plugins/e-acsl/src/libraries/result.ml
deleted file mode 100644
index 701b5dd6d6fae32831a676d4f35f29bad9e1a83e..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/src/libraries/result.ml
+++ /dev/null
@@ -1,30 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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)
diff --git a/src/plugins/e-acsl/src/libraries/result.mli b/src/plugins/e-acsl/src/libraries/result.mli
deleted file mode 100644
index d992f305fc630253a6bb6117a2318a4e9ae2f712..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/src/libraries/result.mli
+++ /dev/null
@@ -1,34 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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]. *)