From 5123ca6972b1628349b566cd0f5e9752c8380f66 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 15 Dec 2020 14:13:16 +0100
Subject: [PATCH] [Kernel] improve feature request messages
---
src/kernel_internals/parsing/logic_lexer.mll | 5 +++--
src/kernel_services/ast_queries/logic_utils.ml | 3 ++-
src/plugins/pdg/build.ml | 4 ++--
3 files changed, 7 insertions(+), 5 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 7ee0a955134..b58bfc4398c 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_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index acdcb97f4f8..1c6ad6e42ed 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/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index fc7aacc6582..edcb31d8933 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -1024,9 +1024,9 @@ let compute_pdg kf =
| Pdg_state.Cannot_fold ->
Pdg_parameters.warning "too imprecise value analysis : abort" ;
degenerated true kf
- | Log.FeatureRequest (_source, 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
(*
--
GitLab