From 86c3adfb8d24d6d5148a595f85c256fb2b95ea78 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 29 Jan 2024 19:07:29 +0100
Subject: [PATCH] [Kernel] remove unsafe Kinstr.loc
---
src/kernel_services/ast_data/alarms.ml | 7 ++++++-
src/kernel_services/ast_queries/cil_datatype.ml | 4 ----
src/kernel_services/ast_queries/cil_datatype.mli | 1 -
src/plugins/aorai/aorai_dataflow.ml | 2 +-
src/plugins/eva/engine/compute_functions.ml | 14 +++++++++-----
5 files changed, 16 insertions(+), 12 deletions(-)
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 99658f1077b..16ab1a0a5cb 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -664,8 +664,13 @@ let find_alarm_in_emitters tbl alarm =
(** Converts an alarm to a code annotation. Returns the code annotation,
whether said code annotation is new, and the table in which the code annot
is/should be inserted. *)
-let to_annot_aux kinstr ?(loc=Kinstr.loc kinstr) alarm =
+let to_annot_aux kinstr ?loc alarm =
(* Kernel.debug "registering alarm %a" D.pretty alarm;*)
+ let loc = match loc, kinstr with
+ | Some l, _ -> l
+ | None, Kstmt stmt -> Stmt.loc stmt
+ | None, Kglobal -> Location.unknown
+ in
let add alarm =
let pred = create_predicate ~loc alarm in
let pred = Logic_const.toplevel_predicate pred in
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index e1dd788e464..0e02f014f61 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -363,10 +363,6 @@ module Kinstr = struct
| Kstmt s -> Stmt.pretty fmt s
end)
- let loc = function
- | Kstmt st -> Stmt.loc st
- | Kglobal -> assert false
-
let kinstr_of_opt_stmt = function
| None -> Kglobal
| Some s -> Kstmt s
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index e0d2eb8b9b9..e0ec1076378 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -200,7 +200,6 @@ module Kinstr: sig
val kinstr_of_opt_stmt: stmt option -> kinstr
(** @since Nitrogen-20111001. *)
- val loc: t -> location
end
module Label: S_with_collections_pretty with type t = label
diff --git a/src/plugins/aorai/aorai_dataflow.ml b/src/plugins/aorai/aorai_dataflow.ml
index 202e2e46c03..b44b715ecd4 100644
--- a/src/plugins/aorai/aorai_dataflow.ml
+++ b/src/plugins/aorai/aorai_dataflow.ml
@@ -621,7 +621,7 @@ let compute_func_aux stack call_site kf init_state =
let source =
match call_site with
| Kglobal -> None
- | Kstmt _ -> Some (fst (Cil_datatype.Kinstr.loc call_site))
+ | Kstmt stmt -> Some (fst (Cil_datatype.Stmt.loc stmt))
in
Aorai_option.warning ?source
"Call to %a does not follow automaton's specification. \
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index b90145463ac..09a3b4d353b 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -252,11 +252,15 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
specification or body according to [target]. If [-eva-show-progress] is
true, the callstack and additional information are printed. *)
let compute_using_spec_or_body target kinstr call state =
- if kinstr <> Kglobal && Parameters.ValShowProgress.get () then
- Self.feedback
- "@[computing for function %a.@\nCalled from %a.@]"
- Callstack.pretty_short call.callstack
- Cil_datatype.Location.pretty (Cil_datatype.Kinstr.loc kinstr);
+ begin
+ match kinstr with
+ | Kstmt stmt when Parameters.ValShowProgress.get () ->
+ Self.feedback
+ "@[computing for function %a.@\nCalled from %a.@]"
+ Callstack.pretty_short call.callstack
+ Cil_datatype.Location.pretty (Cil_datatype.Stmt.loc stmt)
+ | _ -> ()
+ end;
let compute, kind =
match target with
| `Body (fundec, save_results) ->
--
GitLab