From c72f4226a911a10b031062a0d9051e4c1f5fa346 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 13 Jan 2021 17:45:14 +0100
Subject: [PATCH] Add location information for many not_yet_implemented errors
---
src/kernel_internals/parsing/logic_parser.mly | 26 ++++++++++++++-----
src/kernel_services/analysis/dataflow2.ml | 2 +-
.../analysis/interpreted_automata.ml | 4 +--
src/kernel_services/analysis/stmts_graph.ml | 3 ++-
src/plugins/aorai/aorai_dataflow.ml | 2 ++
src/plugins/aorai/aorai_visitors.ml | 1 +
src/plugins/pdg/build.ml | 1 +
src/plugins/variadic/translate.ml | 1 +
src/plugins/wp/cil2cfg.ml | 6 +++--
9 files changed, 33 insertions(+), 13 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 8a41fe69f4f..df34ef16ecc 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -510,12 +510,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)) }
@@ -706,7 +717,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 2c31737ece9..24d9cf46ae2 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 32a98309ead..99418442427 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 3271d4b6ef1..8dfd0f0f66e 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/plugins/aorai/aorai_dataflow.ml b/src/plugins/aorai/aorai_dataflow.ml
index 0662bf5764d..13bf13719f7 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 486c67733ed..65c1781695d 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/pdg/build.ml b/src/plugins/pdg/build.ml
index edcb31d8933..e3e490fb972 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 ->
diff --git a/src/plugins/variadic/translate.ml b/src/plugins/variadic/translate.ml
index 627221bc479..108f03538f3 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 6f09908bfe3..c4ee31c13b2 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
--
GitLab