diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli index 9f0d113f7872764ec2b03a6e57414fb0f83af1ec..5fc9ded3be8d4c07e658455346c9484de411fab1 100644 --- a/src/plugins/eva/Eva.mli +++ b/src/plugins/eva/Eva.mli @@ -212,8 +212,9 @@ module Results: sig (** Just before a statement or at the start of the analysis. *) val before_kinstr : Cil_types.kinstr -> request - (** Evaluation in a given cvalue state. - Callstacks selection are silently ignored on such requests. *) + (** Evaluation in a given cvalue state. Callstacks selection are silently + ignored on such requests. For internal use, could be modified or removed + in a future version. *) val in_cvalue_state : Cvalue.Model.t -> request @@ -594,7 +595,10 @@ end module Cvalue_callbacks: sig (** Register actions to performed during the Eva analysis, - with access to the states of the cvalue domain. *) + with access to the states of the cvalue domain. + This API is for internal use only, and may be modified or removed + in a future version. Please contact us if you need to register callbacks + to be executed during an Eva analysis. *) type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list type state = Cvalue.Model.t @@ -674,6 +678,10 @@ module Logic_inout: sig end module Eva_results: sig + + (** Internal temporary API: please do not use it, as it should be removed in a + future version. *) + type results val get_results: unit -> results diff --git a/src/plugins/eva/utils/cvalue_callbacks.mli b/src/plugins/eva/utils/cvalue_callbacks.mli index cb26f37aa10beb18fff6f8edc4f9e4eaff19445c..3122b1b3c6554bb3e68d48c5cc320016cc2149cc 100644 --- a/src/plugins/eva/utils/cvalue_callbacks.mli +++ b/src/plugins/eva/utils/cvalue_callbacks.mli @@ -23,7 +23,10 @@ [@@@ api_start] (** Register actions to performed during the Eva analysis, - with access to the states of the cvalue domain. *) + with access to the states of the cvalue domain. + This API is for internal use only, and may be modified or removed + in a future version. Please contact us if you need to register callbacks + to be executed during an Eva analysis. *) type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list type state = Cvalue.Model.t diff --git a/src/plugins/eva/utils/eva_results.mli b/src/plugins/eva/utils/eva_results.mli index 6144615c2e453f9366bd1c1c096c4418784439ab..19e35f6bd7b67061ba4db590f2d0f1ea614690bf 100644 --- a/src/plugins/eva/utils/eva_results.mli +++ b/src/plugins/eva/utils/eva_results.mli @@ -30,6 +30,10 @@ val is_non_terminating_instr: stmt -> bool (** {2 Results} *) [@@@ api_start] + +(** Internal temporary API: please do not use it, as it should be removed in a + future version. *) + type results val get_results: unit -> results diff --git a/src/plugins/eva/utils/results.mli b/src/plugins/eva/utils/results.mli index 30806c774755a5114c59b667d395390b4167b860..ec7bc51d785b9b4c67436b2af5f527584a4412d6 100644 --- a/src/plugins/eva/utils/results.mli +++ b/src/plugins/eva/utils/results.mli @@ -117,8 +117,9 @@ val after : Cil_types.stmt -> request (** Just before a statement or at the start of the analysis. *) val before_kinstr : Cil_types.kinstr -> request -(** Evaluation in a given cvalue state. - Callstacks selection are silently ignored on such requests. *) +(** Evaluation in a given cvalue state. Callstacks selection are silently + ignored on such requests. For internal use, could be modified or removed + in a future version. *) val in_cvalue_state : Cvalue.Model.t -> request