From ab3a58317a42b84caab2bc46d57c0a52b17c0ca2 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Sat, 18 Sep 2021 17:35:48 +0200
Subject: [PATCH] [Eva] api: Automatically generates Eva.mli
---
Makefile | 20 ++
src/plugins/value/Eva.mli | 201 ++++++++++++++----
src/plugins/value/domains/cvalue/builtins.mli | 2 +
src/plugins/value/eva-api.sh | 27 +++
src/plugins/value/eval.mli | 3 +-
src/plugins/value/legacy/eval_terms.mli | 18 +-
src/plugins/value/utils/eva_annotations.mli | 23 +-
src/plugins/value/utils/results.mli | 3 +
src/plugins/value/utils/unit_tests.mli | 4 +-
src/plugins/value/utils/value_results.mli | 6 +-
src/plugins/value/value_parameters.mli | 13 +-
11 files changed, 263 insertions(+), 57 deletions(-)
create mode 100755 src/plugins/value/eva-api.sh
diff --git a/Makefile b/Makefile
index 478ee8f3ab6..f580c4984d3 100644
--- a/Makefile
+++ b/Makefile
@@ -825,6 +825,8 @@ PLUGIN_EXTRA_DIRS:=engine values domains api domains/cvalue domains/apron \
domains/gauges domains/equality legacy partitioning utils gui_files \
api values/numerors domains/numerors
PLUGIN_TESTS_DIRS+=value/traces
+PLUGIN_GENERATED:=$(PLUGIN_DIR)/Eva.mli
+PLUGIN_DISTRIB_EXTERNAL+=$(PLUGIN_DIR)/eva-api.sh
# Files for the binding to Apron domains. Only available if Apron is available.
ifeq ($(HAS_APRON),yes)
@@ -927,8 +929,26 @@ VALUE_TYPES:=$(addprefix src/plugins/value_types/,\
PLUGIN_TYPES_CMO:=$(VALUE_TYPES)
PLUGIN_TYPES_TODOC:=$(addsuffix .mli,$(VALUE_TYPES))
+# Eva API
+API_HEADER := headers/open-source/CEA_LGPL_OR_PROPRIETARY
+API_MLI := $(addprefix $(PLUGIN_DIR)/, \
+ utils/results.mli utils/value_results.mli value_parameters.mli \
+ legacy/eval_terms.mli utils/unit_tests.mli utils/eva_annotations.mli \
+ eval.mli domains/cvalue/builtins.mli)
+
+$(PLUGIN_DIR)/Eva.mli: $(PLUGIN_DIR)/eva-api.sh Makefile $(API_HEADER) $(API_MLI)
+ $(PRINT_MAKING) $@
+ $(RM) $@ $@.tmp
+ $< $(API_HEADER) $(API_MLI) > $@.tmp
+ $(CHMOD_RO) $@.tmp
+ $(MV) $@.tmp $@
+
+clean::
+ $(RM) $(PLUGIN_DIR)/Eva.mli
+
$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
+
#########
# Reduc #
#########
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 74ac173305e..71b28373ba5 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -3,7 +3,7 @@
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2021 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
@@ -20,90 +20,177 @@
(* *)
(**************************************************************************)
-(** Analysis for values and pointers *)
+(* This file is generated. Do not edit. *)
+
+module Results: sig
+ (* Usage sketch :
+
+ Eva.Results.(before stmt |> in_callstack cs |> eval_var vi |> as_int)
+
+ or, if you prefer
+
+ Eva.Results.(as_int (eval_var vi (in_callstack cs (before stmt))))
+ *)
+
+ type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
+
+ type request
+ type evaluation
+ type lvaluation
+
+ type error = Bottom | Top | DisabledDomain
+ type 'a result = ('a,error) Result.t
+
+ (* Control point selection *)
+ val at_start : request
+ val at_end : request
+ val at_start_of : Cil_types.kernel_function -> request
+ val at_end_of : Cil_types.kernel_function -> request
+ val before : Cil_types.stmt -> request
+ val after : Cil_types.stmt -> request
+ val before_kinstr : Cil_types.kinstr -> request
+ val after_kinstr : Cil_types.kinstr -> request
+
+ (* Callstack selection *)
+ val in_callstack : callstack -> request -> request
+ val in_callstacks : callstack list -> request -> request
+ val filter_callstack : (callstack -> bool) -> request -> request
+
+ (* Working with callstacks *)
+ val callstacks : request -> callstack list
+ val fold_callstacks : (callstack -> request -> 'a -> 'a) -> 'a -> request -> 'a
+ val by_callstack : request -> (callstack * request) list
+
+ (* State requests *)
+ val equality_class : Cil_types.exp -> request -> Cil_types.exp list result
+ val as_cvalue_model : request -> Cvalue.Model.t result
+
+ (* Evaluation *)
+ val eval_var : Cil_types.varinfo -> request -> evaluation
+ val eval_lval : Cil_types.lval -> request -> evaluation
+ val eval_exp : Cil_types.exp -> request -> evaluation
+
+ val eval_address : Cil_types.lval -> request -> lvaluation
+
+ (* Value conversion *)
+ val as_int : evaluation -> int result
+ val as_integer : evaluation -> Integer.t result
+ val as_float : evaluation -> float result
+ val as_functions : evaluation -> Cil_types.kernel_function list result (* Ignores non-function values *)
+ val as_ival : evaluation -> Ival.t result
+ val as_fval : evaluation -> Fval.t result
+ val as_cvalue : evaluation -> Cvalue.V.t result
+
+ val as_location : lvaluation -> Locations.location result
+ val as_zone : lvaluation -> Locations.Zone.t result
+
+ (* Evaluation properties *)
+ val is_initialized : evaluation -> bool
+ val alarms : evaluation -> Alarms.t list
+
+ (* Bottomness *)
+ val is_bottom : evaluation -> bool
+ val is_called : Cil_types.kernel_function -> bool (* called during the analysis, not by the actual program *)
+ val is_reachable : Cil_types.stmt -> bool (* reachable by the analysis, not by the actual program *)
+
+end
module Value_results: sig
type results
-
+
val get_results: unit -> results
val set_results: results -> unit
val merge: results -> results -> results
val change_callstacks:
(Value_types.callstack -> Value_types.callstack) -> results -> results
+ (** Change the callstacks for the results for which this is meaningful.
+ For technical reasons, the top of the callstack must currently
+ be preserved. *)
end
module Value_parameters: sig
(** Returns the list (name, descr) of currently enabled abstract domains. *)
val enabled_domains: unit -> (string * string) list
-
+
(** [use_builtin kf name] instructs the analysis to use the builtin [name]
to interpret calls to function [kf].
Raises [Not_found] if there is no builtin of name [name]. *)
val use_builtin: Cil_types.kernel_function -> string -> unit
-
+
(** [use_global_value_partitioning vi] instructs the analysis to use
value partitioning on the global variable [vi]. *)
val use_global_value_partitioning: Cil_types.varinfo -> unit
end
module Eval_terms: sig
- (** Evaluation environment, built by [env_annot]. *)
+ type labels_states = Cvalue.Model.t Cil_datatype.Logic_label.Map.t
+
+ (** Evaluation environment. Currently available are function Pre and Post, or
+ the environment to evaluate an annotation *)
type eval_env
-
- (** Dependencies needed to evaluate a term or a predicate. *)
- type logic_deps = Locations.Zone.t Cil_datatype.Logic_label.Map.t
-
- type labels_states = Db.Value.state Cil_datatype.Logic_label.Map.t
-
val env_annot :
- ?c_labels:labels_states -> pre:Db.Value.state -> here:Db.Value.state ->
+ ?c_labels:labels_states -> pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
unit -> eval_env
-
+ (** Dependencies needed to evaluate a term or a predicate *)
+ type logic_deps = Locations.Zone.t Cil_datatype.Logic_label.Map.t
(** [predicate_deps env p] computes the logic dependencies needed to evaluate
[p] in the given evaluation environment [env].
@return None on either an evaluation error or on unsupported construct. *)
val predicate_deps: eval_env -> Cil_types.predicate -> logic_deps option
end
-
module Unit_tests: sig
- (** Runs the unit tests of Eva. *)
+ (** Currently tested by this module:
+ - semantics of sign values. *)
+
+ (** Runs some programmatic tests on Eva. *)
val run: unit -> unit
end
-(** Register special annotations to locally guide the partitioning of states
- performed by an Eva analysis. *)
module Eva_annotations: sig
-
+ (** Register special annotations to locally guide the partitioning of states
+ performed by an Eva analysis:
+
+ - slevel annotations: "slevel default", "slevel merge" and "slevel i"
+ - loop unroll annotations: "loop unroll term"
+ - value partitioning annotations: "split term" and "merge term"
+ - subdivision annotations: "subdivide i"
+
+ Widen hints annotations are still registered in !{widen_hints_ext.ml}. *)
+
(** Annotations tweaking the behavior of the -eva-slevel paramter. *)
type slevel_annotation =
| SlevelMerge (** Join all states separated by slevel. *)
| SlevelDefault (** Use the limit defined by -eva-slevel. *)
| SlevelLocal of int (** Use the given limit instead of -eva-slevel. *)
| SlevelFull (** Remove the limit of number of separated states. *)
-
+
(** Loop unroll annotations. *)
type unroll_annotation =
| UnrollAmount of Cil_types.term (** Unroll the n first iterations. *)
| UnrollFull (** Unroll amount defined by -eva-default-loop-unroll. *)
-
+
type split_kind = Static | Dynamic
+
type split_term =
| Expression of Cil_types.exp
| Predicate of Cil_types.predicate
-
+
(** Split/merge annotations for value partitioning. *)
type flow_annotation =
| FlowSplit of split_term * split_kind
(** Split states according to a term. *)
| FlowMerge of split_term
(** Merge states separated by a previous split. *)
-
+
+ type allocation_kind = By_stack | Fresh | Fresh_weak | Imprecise
+
val get_slevel_annot : Cil_types.stmt -> slevel_annotation option
val get_unroll_annot : Cil_types.stmt -> unroll_annotation list
val get_flow_annot : Cil_types.stmt -> flow_annotation list
val get_subdivision_annot : Cil_types.stmt -> int list
-
+ val get_allocation: Cil_types.stmt -> allocation_kind
+
val add_slevel_annot : emitter:Emitter.t ->
Cil_types.stmt -> slevel_annotation -> unit
val add_unroll_annot : emitter:Emitter.t ->
@@ -114,33 +201,75 @@ module Eva_annotations: sig
Cil_types.stmt -> int -> unit
end
-(** Analysis builtins for the cvalue domain, more efficient than the analysis
- of the C functions. See {builtins.mli} for more details. *)
+module Eval: sig
+ (** Can the results of a function call be cached with memexec? *)
+ type cacheable =
+ | Cacheable (** Functions whose result can be safely cached *)
+ | NoCache (** Functions whose result should not be cached, but for
+ which the caller can still be cached. Typically,
+ functions printing something during the analysis. *)
+ | NoCacheCallers (** Functions for which neither the call, neither the
+ callers, can be cached *)
+end
+
module Builtins: sig
+ (** Eva analysis builtins for the cvalue domain, more efficient than their
+ equivalent in C. *)
+
open Cil_types
-
+
exception Invalid_nb_of_args of int
exception Outside_builtin_possibilities
-
+
+ (* Signature of a builtin: type of the result, and type of the arguments. *)
type builtin_type = unit -> typ * typ list
- type cacheable = Cacheable | NoCache | NoCacheCallers
-
+
+ (** Can the results of a builtin be cached? See {eval.mli} for more details.*)
+ type cacheable = Eval.cacheable = Cacheable | NoCache | NoCacheCallers
+
type full_result = {
c_values: (Cvalue.V.t option * Cvalue.Model.t) list;
+ (** A list of results, consisting of:
+ - the value returned (ie. what is after the 'return' C keyword)
+ - the memory state after the function has been executed. *)
c_clobbered: Base.SetLattice.t;
+ (** An over-approximation of the bases in which addresses of local variables
+ might have been written *)
c_from: (Function_Froms.froms * Locations.Zone.t) option;
+ (** If not None, the froms of the function, and its sure outputs;
+ i.e. the dependencies of the result and of each zone written to. *)
}
-
+
+ (** The result of a builtin can be given in different forms. *)
type call_result =
| States of Cvalue.Model.t list
+ (** A disjunctive list of post-states at the end of the C function.
+ Can only be used if the C function does not write the address of local
+ variables, does not read other locations than the call arguments, and
+ does not write other locations than the result. *)
| Result of Cvalue.V.t list
+ (** A disjunctive list of resulting values. The specification is used to
+ compute the post-state, in which the result is replaced by the values
+ computed by the builtin. *)
| Full of full_result
-
+ (** See [full_result] type. *)
+
+ (** Type of a cvalue builtin, whose arguments are:
+ - the memory state at the beginning of the function call;
+ - the list of arguments of the function call. *)
type builtin = Cvalue.Model.t -> (exp * Cvalue.V.t) list -> call_result
-
+
+ (** [register_builtin name ?replace ?typ cacheable f] registers the function [f]
+ as a builtin to be used instead of the C function of name [name].
+ If [replace] is provided, the builtin is also used instead of the C function
+ of name [replace], unless option -eva-builtin-auto is disabled.
+ If [typ] is provided, consistency between the expected [typ] and the type of
+ the C function is checked before using the builtin.
+ The results of the builtin are cached according to [cacheable]. *)
val register_builtin:
- string -> ?replace:string -> ?typ:builtin_type -> cacheable ->
- builtin -> unit
-
+ string -> ?replace:string -> ?typ:builtin_type -> cacheable -> builtin -> unit
+
+ (** Has a builtin been registered with the given name? *)
val is_builtin: string -> bool
end
+
diff --git a/src/plugins/value/domains/cvalue/builtins.mli b/src/plugins/value/domains/cvalue/builtins.mli
index 353be4b52e8..ac9751b56a8 100644
--- a/src/plugins/value/domains/cvalue/builtins.mli
+++ b/src/plugins/value/domains/cvalue/builtins.mli
@@ -20,6 +20,7 @@
(* *)
(**************************************************************************)
+[@@@ api_start]
(** Eva analysis builtins for the cvalue domain, more efficient than their
equivalent in C. *)
@@ -78,6 +79,7 @@ val register_builtin:
(** Has a builtin been registered with the given name? *)
val is_builtin: string -> bool
+[@@@ api_end]
(** Prepares the builtins to be used for an analysis. Must be called at the
beginning of each Eva analysis. Warns about builtins of incompatible types,
diff --git a/src/plugins/value/eva-api.sh b/src/plugins/value/eva-api.sh
new file mode 100755
index 00000000000..9da4452f3ff
--- /dev/null
+++ b/src/plugins/value/eva-api.sh
@@ -0,0 +1,27 @@
+#!/bin/bash -eu
+
+header=$1
+shift
+
+IFS='' # for read to keep spaces
+
+printf '('
+printf '%0.1s' '*'{1..74}
+printf ')\n'
+while read -r line
+do
+ printf '(* %-68s *)\n' $line
+done < $header
+printf '('
+printf '%0.1s' '*'{1..74}
+printf ')\n\n'
+printf '(* This file is generated. Do not edit. *)\n\n'
+
+for i in "$@"
+do
+ file=$(basename $i)
+ module=${file%.*}
+ printf 'module %s: sig\n' ${module^}
+ awk '/\[@@@ api_start\]/{flag=1;next} /\[@@@ api_end\]/{flag=0} flag{ print " ", $0 }' $i
+ printf 'end\n\n'
+done
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index 5714172358f..4c7bcc873aa 100644
--- a/src/plugins/value/eval.mli
+++ b/src/plugins/value/eval.mli
@@ -270,6 +270,7 @@ type recursion = {
(** Same withdrawal as the previous field, for bases. *)
}
+[@@@ api_start]
(** Can the results of a function call be cached with memexec? *)
type cacheable =
| Cacheable (** Functions whose result can be safely cached *)
@@ -278,7 +279,7 @@ type cacheable =
functions printing something during the analysis. *)
| NoCacheCallers (** Functions for which neither the call, neither the
callers, can be cached *)
-
+[@@@ api_end]
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/value/legacy/eval_terms.mli b/src/plugins/value/legacy/eval_terms.mli
index e63e6a53180..59a798c9e55 100644
--- a/src/plugins/value/legacy/eval_terms.mli
+++ b/src/plugins/value/legacy/eval_terms.mli
@@ -49,17 +49,22 @@ val pretty_logic_evaluation_error :
exception LogicEvalError of logic_evaluation_error
+[@@@ api_start]
type labels_states = Cvalue.Model.t Cil_datatype.Logic_label.Map.t
(** Evaluation environment. Currently available are function Pre and Post, or
the environment to evaluate an annotation *)
type eval_env
+[@@@ api_end]
val make_env: Model.t Abstract_domain.logic_environment -> Model.t -> eval_env
val env_pre_f : pre:Model.t -> unit -> eval_env
+[@@@ api_start]
val env_annot :
- ?c_labels:labels_states -> pre:Model.t -> here:Model.t -> unit -> eval_env
+ ?c_labels:labels_states -> pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
+ unit -> eval_env
+[@@@ api_end]
val env_post_f :
?c_labels:labels_states -> pre:Model.t -> post:Model.t ->
result:varinfo option -> unit -> eval_env
@@ -70,8 +75,10 @@ val env_only_here: Model.t -> eval_env
val env_current_state: eval_env -> Model.t
+[@@@ api_start]
(** Dependencies needed to evaluate a term or a predicate *)
-type logic_deps = Zone.t Cil_datatype.Logic_label.Map.t
+type logic_deps = Locations.Zone.t Cil_datatype.Logic_label.Map.t
+[@@@ api_end]
(** Three modes to handle the alarms when evaluating a logical term. *)
type alarm_mode =
@@ -110,7 +117,12 @@ val eval_tlval_as_zone :
val eval_predicate :
eval_env -> predicate -> predicate_status
-val predicate_deps: eval_env -> predicate -> logic_deps option
+[@@@ api_start]
+(** [predicate_deps env p] computes the logic dependencies needed to evaluate
+ [p] in the given evaluation environment [env].
+ @return None on either an evaluation error or on unsupported construct. *)
+val predicate_deps: eval_env -> Cil_types.predicate -> logic_deps option
+[@@@ api_end]
val reduce_by_predicate :
eval_env -> bool -> predicate -> eval_env
diff --git a/src/plugins/value/utils/eva_annotations.mli b/src/plugins/value/utils/eva_annotations.mli
index df768e5a1fb..69cd10db0d0 100644
--- a/src/plugins/value/utils/eva_annotations.mli
+++ b/src/plugins/value/utils/eva_annotations.mli
@@ -20,7 +20,10 @@
(* *)
(**************************************************************************)
-(** Registers Eva annotations:
+[@@@ api_start]
+(** Register special annotations to locally guide the partitioning of states
+ performed by an Eva analysis:
+
- slevel annotations: "slevel default", "slevel merge" and "slevel i"
- loop unroll annotations: "loop unroll term"
- value partitioning annotations: "split term" and "merge term"
@@ -28,15 +31,17 @@
Widen hints annotations are still registered in !{widen_hints_ext.ml}. *)
+(** Annotations tweaking the behavior of the -eva-slevel paramter. *)
type slevel_annotation =
- | SlevelMerge
- | SlevelDefault
- | SlevelLocal of int
- | SlevelFull
+ | SlevelMerge (** Join all states separated by slevel. *)
+ | SlevelDefault (** Use the limit defined by -eva-slevel. *)
+ | SlevelLocal of int (** Use the given limit instead of -eva-slevel. *)
+ | SlevelFull (** Remove the limit of number of separated states. *)
+(** Loop unroll annotations. *)
type unroll_annotation =
- | UnrollAmount of Cil_types.term
- | UnrollFull
+ | UnrollAmount of Cil_types.term (** Unroll the n first iterations. *)
+ | UnrollFull (** Unroll amount defined by -eva-default-loop-unroll. *)
type split_kind = Static | Dynamic
@@ -44,9 +49,12 @@ type split_term =
| Expression of Cil_types.exp
| Predicate of Cil_types.predicate
+(** Split/merge annotations for value partitioning. *)
type flow_annotation =
| FlowSplit of split_term * split_kind
+ (** Split states according to a term. *)
| FlowMerge of split_term
+ (** Merge states separated by a previous split. *)
type allocation_kind = By_stack | Fresh | Fresh_weak | Imprecise
@@ -64,3 +72,4 @@ val add_flow_annot : emitter:Emitter.t ->
Cil_types.stmt -> flow_annotation -> unit
val add_subdivision_annot : emitter:Emitter.t ->
Cil_types.stmt -> int -> unit
+[@@@ api_end]
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
index 0e0a0c69391..870feaea2b9 100644
--- a/src/plugins/value/utils/results.mli
+++ b/src/plugins/value/utils/results.mli
@@ -20,6 +20,7 @@
(* *)
(**************************************************************************)
+[@@@ api_start]
(* Usage sketch :
Eva.Results.(before stmt |> in_callstack cs |> eval_var vi |> as_int)
@@ -89,3 +90,5 @@ val alarms : evaluation -> Alarms.t list
val is_bottom : evaluation -> bool
val is_called : Cil_types.kernel_function -> bool (* called during the analysis, not by the actual program *)
val is_reachable : Cil_types.stmt -> bool (* reachable by the analysis, not by the actual program *)
+
+[@@@ api_end]
diff --git a/src/plugins/value/utils/unit_tests.mli b/src/plugins/value/utils/unit_tests.mli
index cf1fae9cef8..db0856b3653 100644
--- a/src/plugins/value/utils/unit_tests.mli
+++ b/src/plugins/value/utils/unit_tests.mli
@@ -20,8 +20,10 @@
(* *)
(**************************************************************************)
-(** Currently tested by this file:
+[@@@ api_start]
+(** Currently tested by this module:
- semantics of sign values. *)
(** Runs some programmatic tests on Eva. *)
val run: unit -> unit
+[@@@ api_end]
diff --git a/src/plugins/value/utils/value_results.mli b/src/plugins/value/utils/value_results.mli
index 9592d1e753f..1302d5437c8 100644
--- a/src/plugins/value/utils/value_results.mli
+++ b/src/plugins/value/utils/value_results.mli
@@ -20,10 +20,6 @@
(* *)
(**************************************************************************)
-(** This file will ultimately contain all the results computed by Value
- (which must be moved out of Db.Value), both per stack and globally. *)
-
-
open Cil_types
val is_called: kernel_function -> bool
@@ -36,6 +32,7 @@ val is_non_terminating_instr: stmt -> bool
statements that are instructions. *)
(** {2 Results} *)
+[@@@ api_start]
type results
val get_results: unit -> results
@@ -46,6 +43,7 @@ val change_callstacks:
(** Change the callstacks for the results for which this is meaningful.
For technical reasons, the top of the callstack must currently
be preserved. *)
+[@@@ api_end]
(*
Local Variables:
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index a05cde2a46d..41cd18d4647 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -230,16 +230,19 @@ val register_builtin: string -> unit
(** Registers available domain names for the -eva-domains option. *)
val register_domain: name:string -> descr:string -> unit
-(** Returns the list (name, descr) of currently enabled domains. *)
+[@@@ api_start]
+(** Returns the list (name, descr) of currently enabled abstract domains. *)
val enabled_domains: unit -> (string * string) list
-(** [use_builtin kf b] adds a builtin override for function `kf` to
- builtin `b`. *)
+(** [use_builtin kf name] instructs the analysis to use the builtin [name]
+ to interpret calls to function [kf].
+ Raises [Not_found] if there is no builtin of name [name]. *)
val use_builtin: Cil_types.kernel_function -> string -> unit
-(** [use_global_value_partitioning vi] enable value partitioning on the global
- variable `vi`. *)
+(** [use_global_value_partitioning vi] instructs the analysis to use
+ value partitioning on the global variable [vi]. *)
val use_global_value_partitioning: Cil_types.varinfo -> unit
+[@@@ api_end]
(*
Local Variables:
--
GitLab