diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index c16497fde988313e85ab2038b2e81518e5c989a1..c36bf406295668e155d9df8d48142460a2762e46 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -570,8 +570,9 @@ and comment = parse
| Logic_utils.Not_well_formed (loc, m) ->
output ~source:(fst loc) "%s" m;
None
- | Log.FeatureRequest(_,msg) ->
- output ~source:(Cil_datatype.Position.of_lexing_pos lb.lex_curr_p) "unimplemented ACSL feature: %s" msg; None
+ | Log.FeatureRequest(source,_,msg) ->
+ let source = Option.value ~default:(Cil_datatype.Position.of_lexing_pos lb.lex_curr_p) source in
+ output ~source "unimplemented ACSL feature: %s" msg; None
| exn ->
Kernel.fatal ~source:(Cil_datatype.Position.of_lexing_pos lb.lex_curr_p) "Unknown error (%s)"
(Printexc.to_string exn)
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index ab09ffd36dc9e10884f4729b907dab1ae1e7ad68..aff0ff384ad84bba322d6ac71bc4ac8be26bc350 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -512,12 +512,23 @@ lexpr_inner:
| ALLOCABLE opt_label_1 LPAR lexpr RPAR { info (PLallocable ($2,$4)) }
| FREEABLE opt_label_1 LPAR lexpr RPAR { info (PLfreeable ($2,$4)) }
| ALLOCATION opt_label_1 LPAR lexpr RPAR
- { Kernel.not_yet_implemented "\\allocation" }
-| AUTOMATIC { Kernel.not_yet_implemented "\\automatic" }
-| DYNAMIC { Kernel.not_yet_implemented "\\dynamic" }
-| REGISTER { Kernel.not_yet_implemented "\\register" }
-| STATIC { Kernel.not_yet_implemented "\\static" }
-| UNALLOCATED { Kernel.not_yet_implemented "\\unallocated" }
+ { let source = fst(loc()) in
+ Kernel.not_yet_implemented ~source "\\allocation" }
+| AUTOMATIC {
+ let source = fst(loc()) in
+ Kernel.not_yet_implemented ~source "\\automatic" }
+| DYNAMIC {
+ let source = fst(loc()) in
+ Kernel.not_yet_implemented ~source "\\dynamic" }
+| REGISTER {
+ let source = fst(loc()) in
+ Kernel.not_yet_implemented ~source "\\register" }
+| STATIC {
+ let source = fst(loc()) in
+ Kernel.not_yet_implemented ~source "\\static" }
+| UNALLOCATED {
+ let source = fst(loc()) in
+ Kernel.not_yet_implemented ~source "\\unallocated" }
| NULL { info PLnull }
| constant { info (PLconstant $1) }
| lexpr_inner PLUS lexpr_inner { info (PLbinop ($1, Badd, $3)) }
@@ -710,7 +721,8 @@ abs_param_type_list:
| /* empty */ { [ ] }
| abs_param_list { $1 }
| abs_param_list COMMA DOTDOTDOT {
- Kernel.not_yet_implemented "variadic C function types"
+ let source = fst(loc()) in
+ Kernel.not_yet_implemented ~source "variadic C function types"
}
;
diff --git a/src/kernel_services/analysis/dataflow2.ml b/src/kernel_services/analysis/dataflow2.ml
index 2c31737ece909ee4ea322fcf855198cc37d8c9a2..24d9cf46ae218b4286edb020014d7ecd7bfea612 100644
--- a/src/kernel_services/analysis/dataflow2.ml
+++ b/src/kernel_services/analysis/dataflow2.ml
@@ -365,7 +365,7 @@ module Forwards(T : ForwardsTransfer) = struct
| TryExcept _ | TryFinally _
| Loop _ | Return _ | Block _ -> do_succs curr
| Throw _ | TryCatch _ ->
- Kernel.not_yet_implemented
+ Kernel.not_yet_implemented ~current:true
"[dataflow] exception handling"
diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index 32a98309ead70a015f9269dbe4c382f2abc97e72..9941844242707b22ddcd7cc01c356e408caca23c 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -331,7 +331,7 @@ let build_automaton ~annotations kf =
and do_stmt control (labels:vertex labels) stmt =
let kinstr = Kstmt stmt
and loc = stmt_loc stmt in
-
+ let source = fst loc in
let do_annot control labels (annot: code_annotation) : unit =
let labels = LabelMap.add_builtin Here control.src labels in
let annotation = make_annotation kf stmt annot labels in
@@ -511,7 +511,7 @@ let build_automaton ~annotations kf =
control.dest
| Throw _ | TryCatch _ | TryFinally _ | TryExcept _
- -> Kernel.not_yet_implemented
+ -> Kernel.not_yet_implemented ~source
"[interpreted_automata] exception handling"
in
(* Update statement table *)
diff --git a/src/kernel_services/analysis/stmts_graph.ml b/src/kernel_services/analysis/stmts_graph.ml
index 3271d4b6ef1c2018d129be949e486aa8a4f41416..8dfd0f0f66e698b55c3375cf46f1243f091c874d 100644
--- a/src/kernel_services/analysis/stmts_graph.ml
+++ b/src/kernel_services/analysis/stmts_graph.ml
@@ -267,6 +267,7 @@ let rec get_block_stmts blk =
List.fold_left add Stmt.Set.empty blk.bstmts
and get_stmt_stmts s =
+ let () = CurrentLoc.set (Cil_datatype.Stmt.loc s) in
let compute_stmt_stmts s = match s.skind with
| Instr _ | Return _ | Throw _ -> Stmt.Set.singleton s
| Continue _ | Break _ | Goto _ -> Stmt.Set.singleton s
@@ -284,7 +285,7 @@ and get_stmt_stmts s =
(fun acc (_,b) -> Stmt.Set.union acc (get_block_stmts b))
(get_block_stmts t) c
| TryExcept (_, _, _, _) | TryFinally (_, _, _) ->
- Kernel.not_yet_implemented "exception handling"
+ Kernel.not_yet_implemented ~current:true "exception handling"
in
StmtStmts.memo compute_stmt_stmts s
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index acdcb97f4f8e164586cf04ede5818b183dbf9f07..1c6ad6e42edee54bc38398b71ff62daa79b08a36 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -417,7 +417,8 @@ let float_builtin prefix fkind =
let name = match fkind with
| FFloat -> Printf.sprintf "\\%s_float" prefix
| FDouble -> Printf.sprintf "\\%s_double" prefix
- | FLongDouble -> Kernel.not_yet_implemented "Builtins for long double type"
+ | FLongDouble ->
+ Kernel.not_yet_implemented ~current:true "Builtins for long double type"
in match Logic_env.find_all_logic_functions name with
| [ lf ] -> Some lf
| _ -> Kernel.fatal "Missing or ambiguous builtin %S" name
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/aorai/aorai_dataflow.ml b/src/plugins/aorai/aorai_dataflow.ml
index 0662bf5764d7444a1214427368a085dc296b5dbe..13bf13719f7650a0b0c82d1e37f6f30cdcc42a27 100644
--- a/src/plugins/aorai/aorai_dataflow.ml
+++ b/src/plugins/aorai/aorai_dataflow.ml
@@ -471,6 +471,7 @@ module Computer(I: Init) = struct
do_call s v args d
| Call (_,e,_,_) ->
Aorai_option.not_yet_implemented
+ ~source:(fst e.eloc)
"Indirect call to %a is not handled yet" Printer.pp_exp e
| Local_init (v, ConsInit(f,args,kind),_) ->
let args =
@@ -796,6 +797,7 @@ struct
| Call (_,{ enode = Lval(Var f,NoOffset) },_,_) -> do_call s f state
| Call (_,e,_,_) ->
Aorai_option.not_yet_implemented
+ ~source:(fst e.eloc)
"Indirect call to %a is not handled yet" Printer.pp_exp e
| Local_init (_,ConsInit(f,_,_),_) -> do_call s f state
| Local_init (_,AssignInit _,_)
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index 486c67733edde58a8bbc4e091943759426a9b1f5..65c1781695d9075dc4dc77ce2108c188d842c7d6 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -46,6 +46,7 @@ let get_call_name exp = match exp.enode with
| Lval(Var(vi),NoOffset) -> vi.vname
| _ ->
Aorai_option.not_yet_implemented
+ ~source:(fst exp.eloc)
"At this time, only explicit calls are allowed by the Aorai plugin."
(****************************************************************************)
diff --git a/src/plugins/metrics/metrics_acsl.ml b/src/plugins/metrics/metrics_acsl.ml
index 68210ab38d896d6da3b75e0dc1ddca83914a44fd..6a7960d6e597a6b14e366713122d7ad35e9bdd41 100644
--- a/src/plugins/metrics/metrics_acsl.ml
+++ b/src/plugins/metrics/metrics_acsl.ml
@@ -317,7 +317,8 @@ 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"))
+ Metrics_parameters.not_yet_implemented
+ "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..e3e490fb9720377a5490d1831b638750161d54d1 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -732,6 +732,7 @@ let process_call pdg state stmt lvaloption funcexp argl _loc =
| [] ->
let stmt_str = Format.asprintf "%a" Printer.pp_stmt stmt in
Pdg_parameters.not_yet_implemented
+ ~source:(fst (Cil_datatype.Stmt.loc stmt))
"pdg with an unknown function call: %s" stmt_str
| st :: [] -> st
| st :: other_states ->
@@ -1024,9 +1025,9 @@ 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 ;
+ Pdg_parameters.warning ?source "not implemented by %s yet: %s" who what;
degenerated true kf
(*
diff --git a/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
index 7af1312eace35e3f68a49d3479fb7a3dcdcb9083..348e8c477dabbdd59001acfa7a657eb14cb7aa1b 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
@@ -1,5 +1,5 @@
[variadic] tests/erroneous/variadic-builtin.i:1:
Variadic builtin Frama_C_show_each_warning left untransformed.
-[kernel] Plug-in variadic aborted: unimplemented feature.
+[kernel] tests/erroneous/variadic-builtin.i:6: Plug-in variadic aborted: unimplemented feature.
You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
'[Plug-in variadic] The variadic plugin doesn't handle calls to a pointer to the variadic builtin Frama_C_show_each_warning.'.
diff --git a/src/plugins/variadic/translate.ml b/src/plugins/variadic/translate.ml
index 627221bc47962ca15d63ee417388d4a05826f8ee..108f03538f39c6f2e2698954dd0afc210951c9e9 100644
--- a/src/plugins/variadic/translate.ml
+++ b/src/plugins/variadic/translate.ml
@@ -236,6 +236,7 @@ let translate_variadics (file : file) =
| AddrOf (Var vi, NoOffset)
when Extends.Cil.is_variadic_function vi && is_framac_builtin vi ->
Self.not_yet_implemented
+ ~source:(fst exp.eloc)
"The variadic plugin doesn't handle calls to a pointer to the \
variadic builtin %s."
vi.vname
diff --git a/src/plugins/wp/cil2cfg.ml b/src/plugins/wp/cil2cfg.ml
index 6f09908bfe3ea88747364b4bf55b7607d5b28fef..c4ee31c13b263dc9accc68da1a0de4e37df9ed72 100644
--- a/src/plugins/wp/cil2cfg.ml
+++ b/src/plugins/wp/cil2cfg.ml
@@ -806,7 +806,8 @@ let get_stmt_node env s =
| Instr _ | Return _ -> get_node env (Vstmt s)
| Switch (e, _, _, _) -> get_node env (Vswitch (s, e))
| TryExcept _ | TryFinally _ | Throw _ | TryCatch _ ->
- Wp_parameters.not_yet_implemented "[cfg] exception handling"
+ Wp_parameters.not_yet_implemented
+ ~source:(fst (Cil_datatype.Stmt.loc s)) "[cfg] exception handling"
let cfg_stmt_goto env s next =
let node = get_node env (Vstmt s) in
@@ -942,7 +943,8 @@ and cfg_stmt env s next =
| Switch (e, b, lstmts, _) ->
cfg_switch env s e b lstmts next
| TryExcept _ | TryFinally _ | Throw _ | TryCatch _ ->
- Wp_parameters.not_yet_implemented "[cfg] exception handling"
+ Wp_parameters.not_yet_implemented
+ ~source:(fst (Cil_datatype.Stmt.loc s)) "[cfg] exception handling"
and cfg_block_with ?continue ?break env bkind block next =
let s_continue = env.node_continue in
diff --git a/tests/sparecode/oracle/intra.2.res.oracle b/tests/sparecode/oracle/intra.2.res.oracle
index 87de4bd844a80e01a9dbe5a4a43c61a29760d2c1..0f77e26b0d399eeda28acf570fbd5ba0cb3ef059 100644
--- a/tests/sparecode/oracle/intra.2.res.oracle
+++ b/tests/sparecode/oracle/intra.2.res.oracle
@@ -40,7 +40,7 @@
[pdg] Bottom for function spare_called_fct
[pdg] computing for function stop
[from] Computing for function stop
-[kernel:annot:missing-spec] tests/sparecode/intra.i:110: Warning:
+[kernel:annot:missing-spec] tests/sparecode/intra.i:93: Warning:
Neither code nor specification for function stop, generating default assigns from the prototype
[from] Done for function stop
[pdg] done for function stop