diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index d31c8c679e07a341b20cddc5c021497c6a766392..7ee0a95513431c6c8a0df8879e402e7d6403537d 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -570,7 +570,7 @@ and comment = parse
| Logic_utils.Not_well_formed (loc, m) ->
output ~source:(fst loc) "%s" m;
None
- | Log.FeatureRequest(_,msg) ->
+ | Log.FeatureRequest(_,_,msg) ->
output ~source:(Cil_datatype.Position.of_lexing_pos lb.lex_curr_p) "unimplemented ACSL feature: %s" msg; None
| exn ->
Kernel.fatal ~source:(Cil_datatype.Position.of_lexing_pos lb.lex_curr_p) "Unknown error (%s)"
diff --git a/src/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml
index d4adb75535ee32a7ae221eb80b7eb80e6915f9c6..d630379cbaa65d69501c7f6ba6bfa0f8be2e4a92 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.ml
+++ b/src/kernel_services/cmdline_parameters/cmdline.ml
@@ -136,14 +136,18 @@ let protect = function
(long_plugin_name p)
(additional_info ())
request_crash_report
- | Log.FeatureRequest(p, m) ->
- let name = long_plugin_name p in
- Printf.sprintf
- "%s aborted: unimplemented feature.%s\n\
- You may send a feature request at \
- https://git.frama-c.com/pub/frama-c/issues with:\n\
- '[%s] %s'."
- name (additional_info ()) name m
+ | Log.FeatureRequest(s, p, m) ->
+ let name = long_plugin_name p in
+ let pp_oloc fmt = function
+ | None -> Format.fprintf fmt ""
+ | Some loc -> Format.fprintf fmt "%a: " Filepath.pp_pos loc
+ in
+ Format.asprintf
+ "%a%s aborted: unimplemented feature.%s\n\
+ You may send a feature request at \
+ https://git.frama-c.com/pub/frama-c/issues with:\n\
+ '[%s] %s'."
+ pp_oloc s name (additional_info ()) name m
| e ->
let bt = get_backtrace () in
Printf.sprintf
diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml
index aae66eac586ef30524b4a062ecc16adb150dd63e..fc3e425c5b59e37e2aa36cec4418533989c66ebc 100644
--- a/src/kernel_services/plugin_entry_points/log.ml
+++ b/src/kernel_services/plugin_entry_points/log.ml
@@ -49,7 +49,7 @@ let kernel_label_name = "kernel"
(* --- Exception Management --- *)
(* -------------------------------------------------------------------------- *)
-exception FeatureRequest of string * string
+exception FeatureRequest of Filepath.position option * string * string
exception AbortError of string (* plug-in *)
exception AbortFatal of string (* plug-in *)
@@ -813,7 +813,8 @@ sig
val fatal : ('a,'b) pretty_aborter
val verify : bool -> ('a,bool) pretty_aborter
- val not_yet_implemented : ('a,formatter,unit,'b) format4 -> 'a
+ val not_yet_implemented : ?current:bool -> ?source:Filepath.position ->
+ ('a,formatter,unit,'b) format4 -> 'a
val deprecated : string -> now:string -> ('a -> 'b) -> 'a -> 'b
val with_result : (event option -> 'b) -> ('a,'b) pretty_aborter
@@ -1203,12 +1204,13 @@ struct
let em = channel.emitters.(nth_kind kd) in
em.listeners <- em.listeners @ [f]
- let not_yet_implemented text =
+ let not_yet_implemented ?(current=false) ?source text =
let buffer = Buffer.create 80 in
+ let source = get_source current source in
let finally fmt =
Format.pp_print_flush fmt ();
let msg = Buffer.contents buffer in
- raise (FeatureRequest(channel.plugin,msg)) in
+ raise (FeatureRequest(source,channel.plugin,msg)) in
let fmt = Format.formatter_of_buffer buffer in
Format.kfprintf finally fmt text
diff --git a/src/kernel_services/plugin_entry_points/log.mli b/src/kernel_services/plugin_entry_points/log.mli
index a01c5b99e605d977136ca4867624ab02c8df0a68..20ffa81b0f5f76cdb498477f32d8262fd9e2b966 100644
--- a/src/kernel_services/plugin_entry_points/log.mli
+++ b/src/kernel_services/plugin_entry_points/log.mli
@@ -82,10 +82,13 @@ exception AbortFatal of string
name of the plugin.
@since Beryllium-20090601-beta1 *)
-exception FeatureRequest of string * string
+exception FeatureRequest of Filepath.position option * string * string
(** Raised by [not_yet_implemented].
- You may catch [FeatureRequest(p,r)] to support degenerated behavior.
- The responsible plugin is 'p' and the feature request is 'r'. *)
+ You may catch [FeatureRequest(s,p,r)] to support degenerated behavior.
+ The (optional) source location is s, the responsible plugin is 'p'
+ and the feature request is 'r'.
+ @modified Frama-C+dev added source location.
+*)
(* -------------------------------------------------------------------------- *)
(** {2 Option_signature.Interface}
@@ -205,11 +208,14 @@ module type Messages = sig
@since Beryllium-20090601-beta1
@plugin development guide *)
- val not_yet_implemented : ('a,formatter,unit,'b) format4 -> 'a
+ val not_yet_implemented : ?current:bool -> ?source:Filepath.position ->
+ ('a,formatter,unit,'b) format4 -> 'a
(** raises [FeatureRequest] but {i does not} send any message.
If the exception is not caught, Frama-C displays a feature-request
message to the user.
- @since Beryllium-20090901 *)
+ @since Beryllium-20090901
+ @modified Frama-C+dev added current and source arguments.
+ *)
val deprecated: string -> now:string -> ('a -> 'b) -> ('a -> 'b)
(** [deprecated s ~now f] indicates that the use of [f] of name [s] is now
diff --git a/src/plugins/metrics/metrics_acsl.ml b/src/plugins/metrics/metrics_acsl.ml
index 68210ab38d896d6da3b75e0dc1ddca83914a44fd..3a25f56a69cc217e9179f539b75f67461ad48c83 100644
--- a/src/plugins/metrics/metrics_acsl.ml
+++ b/src/plugins/metrics/metrics_acsl.ml
@@ -317,7 +317,7 @@ let dump () =
| Metrics_base.Html -> dump_acsl_stats_html fmt
| Metrics_base.Text -> dump_acsl_stats fmt
| Metrics_base.Json ->
- raise (Log.FeatureRequest ("Metrics", "JSON format for ACSL metrics"))
+ raise (Log.FeatureRequest (None, "Metrics", "JSON format for ACSL metrics"))
);
close_out chan
with Sys_error s ->
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index e761247ebc70745eeaa92b6a2cd2237e9d70eb28..fc7aacc658214ccbc139ecf745e927da4faa72c9 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -1024,7 +1024,7 @@ let compute_pdg kf =
| Pdg_state.Cannot_fold ->
Pdg_parameters.warning "too imprecise value analysis : abort" ;
degenerated true kf
- | Log.FeatureRequest (who, what) ->
+ | Log.FeatureRequest (_source, who, what) ->
(* [JS 2012/08/24] nobody should catch this exception *)
Pdg_parameters.warning "not implemented by %s yet: %s" who what ;
degenerated true kf