Analyze driver (monolithic)

This module provides the main entry points for performing analysis and assertion checking. It requires loading the program before (e.g., with frontend_driver).

Adding new analyses

To include a new analysis, add a clause for analyze/2 (and for analysis/1).

As an alternative, you can add clauses for the multifile predicates analysis/4 and analysis/1, directly in your own sources.

See the file examples/Extending/myanalyzer.pl in the source directory for an example of this.

Usage and interface

Library usage:
:- use_module(ciaopp(analyze_driver)). This module is loaded by default in the CiaoPP toplevel and reexported from the ciaopp module.
Exports:
- Predicates:
  assert_domain/1, last_domain_used/1, analyze/1, analyze/2, analyze1/2, acheck_summary/1, acheck_summary/2, get_assert_count/1, acheck/0, acheck/1, acheck/2, clean_analysis_info/0, clean_analysis_info0/0, cleanup_for_codegen/0.
- Regular Types:
  ctcheck_sum/1.
- Multifiles:
  lazy_analysis/1, analysis_module/2, loaded_analysis/1, analysis/4, analysis/1, aidomain/1.

Documentation on exports

PREDICATEassert_domain/1

No further documentation available for this predicate.

PREDICATElast_domain_used/1

No further documentation available for this predicate.

PREDICATEanalyze/1

Usage:analyze(Analysis)

Analyzes the current module with Analysis. If the intermod flag is not off, this predicate may call module/1.

The following properties should hold at call time:
(nonvar/1)Analysis is currently a term which is not a free variable.
(analysis/1)Analysis is a valid analysis identifier.
The following properties should hold globally:
(not_fails/1)All the calls of the form analyze(Analysis) do not fail.
(no_choicepoints/1)A call to analyze(Analysis) does not leave new choicepoints.

PREDICATEanalyze/2

Usage:analyze(Analysis,Info)

Same as analyze(Analysis) but in Info returns statistics (time and memory).

The following properties should hold at call time:
(nonvar/1)Analysis is currently a term which is not a free variable.
(var/1)Info is a free variable.

PREDICATEanalyze1/2

No further documentation available for this predicate.

REGTYPEctcheck_sum/1

A regular type, defined as follows:

ctcheck_sum(ok).
ctcheck_sum(warning).
ctcheck_sum(error).

PREDICATEacheck_summary/1

Usage:acheck_summary(S)

Checks assertions w.r.t. analysis information. Upon success S is bound to: ok (the compile-time checking process has generated no error nor warning), warning (compile-time checking has not generated any error, but there has been at least one warning) or error (at least one error has been produced).

The following properties should hold at call time:
(var/1)S is a free variable.
The following properties should hold upon exit:
(ctcheck_sum/1)ctcheck_sum(S)

PREDICATEacheck_summary/2

Usage:acheck_summary(Info,S)

Same as acheck_summary(S) but in Info returns assertion checking statistics.

The following properties should hold at call time:
(var/1)Info is a free variable.
(var/1)S is a free variable.

PREDICATEget_assert_count/1

No further documentation available for this predicate.

PREDICATEacheck/0

Usage:

Checks assertions w.r.t. analysis information, obtains from domain/1 which analyses were run.

PREDICATEacheck/1

Usage:acheck(AbsInt)

Checks assertions using the analysis information of AbsInt. The analysis must be present in CiaoPP (via analysis or restore dump).

PREDICATEacheck/2

Usage 1:acheck(AbsInt,ModList)

The following properties should hold at call time:
(nonvar/1)AbsInt is currently a term which is not a free variable.
(nonvar/1)ModList is currently a term which is not a free variable.
(list/2)AbsInt is a list of atms.
(list/2)ModList is a list of atms.

Usage 2:acheck(AbsInt,MaybeModList)

If MaybeModList is the atom all, all modules in the current punit are considered. If it is a list of module names, only the assertions or predicates in those modules are checked.

The following properties should hold at call time:
(nonvar/1)AbsInt is currently a term which is not a free variable.
(nonvar/1)MaybeModList is currently a term which is not a free variable.
(list/2)AbsInt is a list of atms.
(atm/1)MaybeModList is an atom.

PREDICATEclean_analysis_info/0

Usage:

Cleans all analysis info but keep the program as wether it would be just read.

PREDICATEclean_analysis_info0/0

No further documentation available for this predicate.

PREDICATEcleanup_for_codegen/0

No further documentation available for this predicate.

PREDICATEtrace_fixp/1

Usage 1:trace_fixp(X)

Mode for setting the current flag to a single value.

The following properties should hold at call time:
(trace_option/1)X is a valid type of fixpoint tracing:

no — disables fixpoint tracing.

- `trace` — shows certain relevant spy points during the fixpoint
  computation.
- `op_count` — counts the steps of the fixpoint operations.
- `view` — displays the analysis graph while being constructed.
- `debug` — displays debugging messages relating the source's
  subgoal being analyzed.

The following properties should hold globally:
(not_further_inst/2)X is not further instantiated.

Usage 2:trace_fixp(X)

Mode for setting the current flag to several values.

The following properties should hold at call time:
(list/2)X is a list of trace_options.
The following properties should hold globally:
(not_further_inst/2)X is not further instantiated.

Usage 3:trace_fixp(X)

Mode for getting all selected tracing options.

The following properties should hold at call time:
(var/1)X is a free variable.
The following properties should hold upon exit:
(list/2)X is a list of trace_options.

Documentation on multifiles

PREDICATElazy_analysis/1

Specifies an analysis that can be lazy loaded The predicate is multifile.

PREDICATEanalysis_module/2

Given an analysis, returns the module that contains the implementation (or entry point) of a lazy loadable analysis. Such module must implement the analysis/4 multifile clause. The predicate is multifile.

PREDICATEloaded_analysis/1

Helps to determine if an analysis was already loaded. Must be defined in the same module specified by analysis_module/2. The predicate is multifile.

PREDICATEanalysis/4

Usage:analysis(Analysis,Clauses,Dictionaries,Info)

Performs Analysis on program Clauses.

The following properties should hold at call time:
(analysis/1)Analysis is a valid analysis identifier.

The predicate is multifile.

PROPERTYanalysis/1

Usage:analysis(Analysis)

Analysis is a valid analysis identifier.

The predicate is multifile.

PREDICATEaidomain/1

See the chapter on domains. The predicate is multifile.

Documentation on imports

This module has the following direct dependencies:

Application modules:
ciaopp_log, analysis_stats, preprocess_flags, infer_db, frontend_driver, trace_fixp, incanal, intermod, plai, vartypes, inferseff, infer_dom, ctchecks_pred, ctchecks_pp, ctchecks_common, preproc_errors, intermod_ops.
System library modules:
native_props, datafacts_rt, compiler, p_unit, p_unit_db, reachability, infernf, typeslib, recurrence_processing, counters, aggregates.
Internal (engine) modules:
term_basic, arithmetic, atomic_basic, basiccontrol, exceptions, term_compare, term_typing, debugger_support, basic_props, hiord_rt, messages_basic.
Packages:
prelude, initial, condcomp, assertions, assertions/assertions_basic, basicmodes, regtypes, nativeprops, datafacts, ciaopp(ciaopp_options), ciaopp(analysis_register).