diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml index 3479c49f1de700aba627c3e58b669b296bab5c16..c95353544de9d0f43741b2dd4e215c48885d26f6 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 2bf8f67c110ebab50ba7ec433dec4f709631525e..883895c10dad56d1c6ac93cce79477040ef52620 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 47022a39032828eba3387bf2ff8ea6e18c5f54ad..5bed3af7537fc63e8ff0aca417886287c422070a 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 8680fd724817b967b4fbcda22a129f0d35bfd18e..3ae608c093eb7d7dcf5ff55de45a546fc49ca19d 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