diff --git a/src/kernel_services/abstract_interp/eva_types.ml b/src/kernel_services/abstract_interp/eva_types.ml index b4b3a8f031b955b02b5b1a6a1f2c6718a880377f..8a1af2a6db3dc8754e12dfb00d5a0eba8b247360 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 97a4b2957e0390667edff4ce582faff520972bb6..848653329931c44097f17d965ab1771bad878475 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 1b7b47ac288ce582fd528fe56b4c17ea33606f5e..62e799b9552b57f40b6e93da154a36646a828c1b 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 7de74799a42b21f38eacae8a5b63ab3f47cd1652..08ede5fc67c0b52ad5073f1e18aded7c6c758bd2 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 ee1b6d4caa868e1bf5e81dd531e13f9ef9403472..bb7d45ac49ff7e8a7bad98b07171ae33ef87585b 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 36d0eb3b8ce5419317d81c0adbe116529dbec7f3..8fb57decf5b6c805f6776917c96f537c42709bc1 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