diff --git a/Makefile b/Makefile index ce93d4b27291c8721c7a2ffecf9b5b71fdb2e236..b99afea518b664558478423dade71ea554e0a325 100644 --- a/Makefile +++ b/Makefile @@ -929,12 +929,12 @@ VALUE_TYPES:=$(addprefix src/plugins/value_types/,\ PLUGIN_TYPES_CMO:=$(VALUE_TYPES) PLUGIN_TYPES_TODOC:=$(addsuffix .mli,$(VALUE_TYPES)) -# Eva API +# Eva API. API_MLI := $(addprefix $(PLUGIN_DIR)/, \ - engine/analysis.mli \ - 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) + engine/analysis.mli utils/results.mli \ + value_parameters.mli utils/eva_annotations.mli \ + eval.mli domains/cvalue/builtins.mli \ + legacy/eval_terms.mli utils/value_results.mli utils/unit_tests.mli) $(PLUGIN_DIR)/Eva.mli: $(PLUGIN_DIR)/gen-api.sh Makefile $(API_MLI) $(PRINT_MAKING) $@ diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli index 2047779dc2581f8be386fe36f48c4bfd4a4bcd3f..d71827450ce7cf798ef3cdccc17501b63260f379 100644 --- a/src/plugins/value/Eva.mli +++ b/src/plugins/value/Eva.mli @@ -1,3 +1,18 @@ +(** Eva public API. + + The main modules are: + - Analysis: run the analysis. + - Results: access analysis results, especially the values of expressions + and memory locations of lvalues at each program point. + + The following modules allow configuring the Eva analysis: + - Value_parameters: change the configuration of the analysis. + - Eva_annotations: add local annotations to guide the analysis. + - Builtins: register ocaml builtins to be used by the cvalue domain + instead of analysing the body of some C functions. + + Other modules are for internal use only. *) + (* This file is generated. Do not edit. *) module Analysis: sig @@ -239,19 +254,6 @@ module Results: sig 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 (** Configuration of the analysis. *) @@ -268,24 +270,6 @@ module Value_parameters: sig val use_global_value_partitioning: Cil_types.varinfo -> unit end -module Eval_terms: sig - (** [annot_predicate_deps ~pre ~here p] computes the logic dependencies needed - to evaluate the predicate [p] in a code annotation in cvalue state [here], - in a function whose pre-state is [pre]. - Returns None on either an evaluation error or on unsupported construct. *) - val annot_predicate_deps: - pre:Cvalue.Model.t -> here:Cvalue.Model.t -> - Cil_types.predicate -> Locations.Zone.t option -end - -module Unit_tests: sig - (** Currently tested by this module: - - semantics of sign values. *) - - (** Runs some programmatic tests on Eva. *) - val run: unit -> unit -end - module Eva_annotations: sig (** Register special annotations to locally guide the Eva analysis: @@ -409,3 +393,34 @@ module Builtins: sig (** Has a builtin been registered with the given name? *) val is_builtin: string -> bool end + +module Eval_terms: sig + (** [annot_predicate_deps ~pre ~here p] computes the logic dependencies needed + to evaluate the predicate [p] in a code annotation in cvalue state [here], + in a function whose pre-state is [pre]. + Returns None on either an evaluation error or on unsupported construct. *) + val annot_predicate_deps: + pre:Cvalue.Model.t -> here:Cvalue.Model.t -> + Cil_types.predicate -> Locations.Zone.t option +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 Unit_tests: sig + (** Currently tested by this module: + - semantics of sign values. *) + + (** Runs some programmatic tests on Eva. *) + val run: unit -> unit +end diff --git a/src/plugins/value/gen-api.sh b/src/plugins/value/gen-api.sh index 2bfcce11bc89e2f541d52bc4a027e5942f1dd833..82ce513c3bd3a9c39edda6e380afd1dab059e8ca 100755 --- a/src/plugins/value/gen-api.sh +++ b/src/plugins/value/gen-api.sh @@ -1,6 +1,21 @@ #!/bin/bash -eu -printf '(* This file is generated. Do not edit. *)\n' +printf '(** Eva public API. + + The main modules are: + - Analysis: run the analysis. + - Results: access analysis results, especially the values of expressions + and memory locations of lvalues at each program point. + + The following modules allow configuring the Eva analysis: + - Value_parameters: change the configuration of the analysis. + - Eva_annotations: add local annotations to guide the analysis. + - Builtins: register ocaml builtins to be used by the cvalue domain + instead of analysing the body of some C functions. + + Other modules are for internal use only. *)\n' + +printf '\n(* This file is generated. Do not edit. *)\n' for i in "$@" do