From 00c12afdb012666537b00d37238761c1a4920dec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Tue, 19 Jul 2022 20:22:03 +0200 Subject: [PATCH] [Eva] Adds a space before colons in results.mli. --- src/plugins/eva/Eva.mli | 10 +++++----- src/plugins/eva/utils/results.mli | 10 +++++----- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli index cc3ec581d05..9f0d113f787 100644 --- a/src/plugins/eva/Eva.mli +++ b/src/plugins/eva/Eva.mli @@ -156,7 +156,7 @@ module Results: sig function body: all requests in the function will lead to a Bottom error. - results have not been saved, due to the [-eva-no-results] parameter: all requests in the function will lead to a Top error. *) - val are_available: Cil_types.kernel_function -> bool + val are_available : Cil_types.kernel_function -> bool type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list @@ -214,7 +214,7 @@ module Results: sig (** Evaluation in a given cvalue state. Callstacks selection are silently ignored on such requests. *) - val in_cvalue_state: Cvalue.Model.t -> request + val in_cvalue_state : Cvalue.Model.t -> request (** Callstack selection *) @@ -264,7 +264,7 @@ module Results: sig request. If [filter] is provided, states are filtered on the given bases (for domains that support this feature). Returns a list of pair (name, state) for all available domains. *) - val print_states: ?filter:Base.Hptset.t -> request -> (string * string) list + val print_states : ?filter:Base.Hptset.t -> request -> (string * string) list (** Dependencies *) @@ -362,7 +362,7 @@ module Results: sig (** Converts into a Zone. Error cases are converted into bottom or top zones accordingly. *) - val as_zone: address evaluation -> Locations.Zone.t + val as_zone : address evaluation -> Locations.Zone.t (** Converts into a Zone result. *) val as_zone_result : address evaluation -> Locations.Zone.t result @@ -410,7 +410,7 @@ module Results: sig the main function has been analyzed for [Kglobal]. *) val is_reachable_kinstr : Cil_types.kinstr -> bool - val condition_truth_value: Cil_types.stmt -> bool * bool + val condition_truth_value : Cil_types.stmt -> bool * bool (** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)] (resp. snd) is true if and only if the condition of the 'if' has been evaluated to true (resp. false) at least once during the analysis. *) diff --git a/src/plugins/eva/utils/results.mli b/src/plugins/eva/utils/results.mli index 68a6d04badc..30806c77475 100644 --- a/src/plugins/eva/utils/results.mli +++ b/src/plugins/eva/utils/results.mli @@ -61,7 +61,7 @@ function body: all requests in the function will lead to a Bottom error. - results have not been saved, due to the [-eva-no-results] parameter: all requests in the function will lead to a Top error. *) -val are_available: Cil_types.kernel_function -> bool +val are_available : Cil_types.kernel_function -> bool type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list @@ -119,7 +119,7 @@ val before_kinstr : Cil_types.kinstr -> request (** Evaluation in a given cvalue state. Callstacks selection are silently ignored on such requests. *) -val in_cvalue_state: Cvalue.Model.t -> request +val in_cvalue_state : Cvalue.Model.t -> request (** Callstack selection *) @@ -169,7 +169,7 @@ val get_cvalue_model_result : request -> Cvalue.Model.t result request. If [filter] is provided, states are filtered on the given bases (for domains that support this feature). Returns a list of pair (name, state) for all available domains. *) -val print_states: ?filter:Base.Hptset.t -> request -> (string * string) list +val print_states : ?filter:Base.Hptset.t -> request -> (string * string) list (** Dependencies *) @@ -267,7 +267,7 @@ val as_location_result : address evaluation -> Locations.location result (** Converts into a Zone. Error cases are converted into bottom or top zones accordingly. *) -val as_zone: address evaluation -> Locations.Zone.t +val as_zone : address evaluation -> Locations.Zone.t (** Converts into a Zone result. *) val as_zone_result : address evaluation -> Locations.Zone.t result @@ -315,7 +315,7 @@ val is_reachable : Cil_types.stmt -> bool the main function has been analyzed for [Kglobal]. *) val is_reachable_kinstr : Cil_types.kinstr -> bool -val condition_truth_value: Cil_types.stmt -> bool * bool +val condition_truth_value : Cil_types.stmt -> bool * bool (** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)] (resp. snd) is true if and only if the condition of the 'if' has been evaluated to true (resp. false) at least once during the analysis. *) -- GitLab