From 203b4912375abd5af40c7e2d82691080d3cbc0cd Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 27 Jan 2021 09:41:23 +0100
Subject: [PATCH] [Extlib] make exn argument mandatory in Extlib.the and update
occurrences
---
src/kernel_services/ast_printing/printer_tag.ml | 2 +-
src/libraries/stdlib/extlib.ml | 8 ++------
src/libraries/stdlib/extlib.mli | 4 +++-
src/plugins/variadic/translate.ml | 5 ++---
4 files changed, 8 insertions(+), 11 deletions(-)
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 3479c49f1de..c95353544de 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -544,7 +544,7 @@ struct
| FromAny -> super#from s fmt from
| From _ ->
let ip =
- Extlib.the
+ Option.get
(Property.ip_of_from
(Option.get self#current_kf) self#current_kinstr
self#current_behavior_or_loop from)
diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index 2bf8f67c110..883895c10da 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -240,12 +240,8 @@ let opt_filter f = function
| None -> None
| (Some x) as o -> if f x then o else None
-let the ?exn = function
- | None ->
- begin match exn with
- | None -> invalid_arg "Extlib.the"
- | Some exn -> raise exn
- end
+let the ~exn = function
+ | None -> raise exn
| Some x -> x
let opt_hash hash v = match v with
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index 47022a39032..5bed3af7537 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -206,11 +206,13 @@ val merge_opt:
val opt_filter: ('a -> bool) -> 'a option -> 'a option
-val the: ?exn:exn -> 'a option -> 'a
+val the: exn:exn -> 'a option -> 'a
(** @raise Exn if the value is [None] and [exn] is specified.
@raise Invalid_argument if the value is [None] and [exn] is not specified.
@return v if the value is [Some v].
@modify Magnesium-20151001 add optional argument [exn]
+ @modify Frama-C+dev optional argument [exn] now mandatory; otherwise,
+ use [Option.get], which is equivalent.
@plugin development guide *)
val opt_hash: ('a -> int) -> 'a option -> int
diff --git a/src/plugins/variadic/translate.ml b/src/plugins/variadic/translate.ml
index 8680fd72481..3ae608c093e 100644
--- a/src/plugins/variadic/translate.ml
+++ b/src/plugins/variadic/translate.ml
@@ -23,7 +23,6 @@
open Cil_types
open Va_types
open Options
-open Extlib
module Typ = Extends.Typ
(* List of builtin function names to translate *)
@@ -137,10 +136,10 @@ let translate_variadics (file : file) =
(* Replace variadic calls *)
method! vinst i =
- let fundec = the self#current_func in
+ let fundec = Option.get self#current_func in
let loc = Cil_datatype.Instr.loc i in
let block = self#enclosing_block () in
- let ghost = (the self#current_stmt).ghost in
+ let ghost = (Option.get self#current_stmt).ghost in
let make_new_args mk_call f args =
let vf = Table.find classification f in
try
--
GitLab