From 39a42241ea7786e5f4d6efe53fb9913fd25a6e9b Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 27 Jun 2023 23:11:23 +0200
Subject: [PATCH] [Eva] Update the Callstack interface for Mthread
---
src/kernel_services/abstract_interp/eva_types.ml | 9 +++++++++
src/kernel_services/abstract_interp/eva_types.mli | 2 ++
src/plugins/eva/Eva.mli | 2 ++
src/plugins/eva/types/callstack.mli | 2 ++
src/plugins/eva/utils/private.ml | 1 +
src/plugins/eva/utils/private.mli | 1 +
6 files changed, 17 insertions(+)
diff --git a/src/kernel_services/abstract_interp/eva_types.ml b/src/kernel_services/abstract_interp/eva_types.ml
index b4b3a8f031b..8a1af2a6db3 100644
--- a/src/kernel_services/abstract_interp/eva_types.ml
+++ b/src/kernel_services/abstract_interp/eva_types.ml
@@ -202,4 +202,13 @@ struct
| Global _vi -> []
| Local ls ->
List.rev_map snd ls.stack
+
+ (* This function should not be used as callstack should be initialized
+ with their thread instead of fixing it afterwards. To be removed as soon
+ as this issue is fixed. *)
+ let change_thread cs thread =
+ match cs with
+ | Global _ -> cs
+ | Local ls ->
+ Local { ls with thread }
end
diff --git a/src/kernel_services/abstract_interp/eva_types.mli b/src/kernel_services/abstract_interp/eva_types.mli
index 97a4b2957e0..84865332993 100644
--- a/src/kernel_services/abstract_interp/eva_types.mli
+++ b/src/kernel_services/abstract_interp/eva_types.mli
@@ -58,6 +58,8 @@ sig
val to_legacy : t -> Value_types.callstack
val to_kf_list : t -> Cil_types.kernel_function list
val to_stmt_list : t -> Cil_types.stmt list
+
+ val change_thread : t -> int -> t
end
[@@alert db_deprecated
"Eva_types is only provided for compatibility reason and will be removed \
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 1b7b47ac288..62e799b9552 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -173,6 +173,8 @@ module Callstack: sig
(** Gives the list of call statements from the bottom to the top of the callstack (i.e. reverse order of the call stack). *)
val to_stmt_list : t -> Cil_types.stmt list
+
+ val change_thread : t -> int -> t
end
module Results: sig
diff --git a/src/plugins/eva/types/callstack.mli b/src/plugins/eva/types/callstack.mli
index 7de74799a42..08ede5fc67c 100644
--- a/src/plugins/eva/types/callstack.mli
+++ b/src/plugins/eva/types/callstack.mli
@@ -78,4 +78,6 @@ val to_kf_list : t -> Cil_types.kernel_function list
(** Gives the list of call statements from the bottom to the top of the callstack (i.e. reverse order of the call stack). *)
val to_stmt_list : t -> Cil_types.stmt list
+
+val change_thread : t -> int -> t
[@@@ api_end]
diff --git a/src/plugins/eva/utils/private.ml b/src/plugins/eva/utils/private.ml
index ee1b6d4caa8..bb7d45ac49f 100644
--- a/src/plugins/eva/utils/private.ml
+++ b/src/plugins/eva/utils/private.ml
@@ -28,6 +28,7 @@ module Abstractions = Abstractions
module Active_behaviors = Active_behaviors
module Alarmset = Alarmset
module Analysis = Analysis
+module Callstack = Callstack
module Cvalue_domain = Cvalue_domain
module Domain_builder = Domain_builder
module Eva_dynamic = Eva_dynamic
diff --git a/src/plugins/eva/utils/private.mli b/src/plugins/eva/utils/private.mli
index 36d0eb3b8ce..8fb57decf5b 100644
--- a/src/plugins/eva/utils/private.mli
+++ b/src/plugins/eva/utils/private.mli
@@ -32,6 +32,7 @@ module Abstractions = Abstractions
module Active_behaviors = Active_behaviors
module Alarmset = Alarmset
module Analysis = Analysis
+module Callstack = Callstack
module Cvalue_domain = Cvalue_domain
module Domain_builder = Domain_builder
module Eva_dynamic = Eva_dynamic
--
GitLab