[Eva] Update the Callstack interface for Mthread

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

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 \

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

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]

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

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