Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Polish Dialyzer documentation after migration #8432

Merged
merged 1 commit into from
May 2, 2024
Merged

Polish Dialyzer documentation after migration #8432

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
49 changes: 23 additions & 26 deletions lib/dialyzer/doc/guides/dialyzer_chapter.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,16 +24,12 @@ limitations under the License.
### Scope

Dialyzer is a static analysis tool that identifies software discrepancies, such
as definite type errors, code that has become dead or unreachable because of
programming error, and unnecessary tests, in single Erlang modules or entire
(sets of) applications.
as definite type errors, code that is unreachable because of
programming error, and unnecessary tests in single Erlang modules or an entire
codebase.

Dialyzer can be called from the command line and from Erlang.

### Prerequisites

It is assumed that the reader is familiar with the Erlang programming language.

[](){: #plt }

## The Persistent Lookup Table
Expand Down Expand Up @@ -64,7 +60,7 @@ then use the following command:
dialyzer --add_to_plt --apps compiler --output_plt my.plt
```

Then you can add your favorite application my_app to the new PLT:
Then you can add your favorite application `my_app` to the new PLT:

```text
dialyzer --add_to_plt --plt my.plt -r my_app/ebin
Expand All @@ -76,7 +72,7 @@ But you realize that it is unnecessary to have the Erlang compiler in this one:
dialyzer --remove_from_plt --plt my.plt --apps compiler
```

Later, when you have fixed a bug in your application my_app, you want to update
Later, when you have fixed a bug in your application `my_app`, you want to update
the PLT so that it becomes fresh the next time you run Dialyzer. In this case,
run the following command:

Expand All @@ -85,9 +81,9 @@ dialyzer --check_plt --plt my.plt
```

Dialyzer then reanalyzes the changed files and the files that depend on these
files. Notice that this consistency check is performed automatically the next
time you run Dialyzer with this PLT. Option `--check_plt` is only for doing so
without doing any other analysis.
files. Note that this consistency check is performed automatically the next
time you run Dialyzer with this PLT. Use option `--check_plt` to perform the
consistency check without doing any other analysis.

To get information about a PLT, use the following option:

Expand All @@ -99,7 +95,7 @@ To specify which PLT, use option `--plt`.

To get the output printed to a file, use option `--output_file`.

Notice that when manipulating the PLT, no warnings are emitted. To turn on
Note that no warnings are emitted when manipulating the PLT. To turn on
warnings during (re)analysis of the PLT, use option `--get_warnings`.

## Using Dialyzer from the Command Line
Expand All @@ -113,34 +109,34 @@ Dialyzer can also be used directly from Erlang. See `m:dialyzer`.
## Dialyzer's Model of Analysis

Dialyzer operates somewhere between a classical type checker and a more general
static-analysis tool: It checks and consumes function specs, yet doesn't require
static-analysis tool: It checks and consumes function specs, yet does not require
them, and it can find bugs across modules which consider the dataflow of the
programs under analysis. This means Dialyzer can find genuine bugs in complex
code, and is pragmatic in the face of missing specs or limited information about
the codebase, only reporting issues which it can prove have the potential to
cause a genuine issue at runtime. This means Dialyzer will sometimes not report
every bug, since it cannot always find this proof.

### How Dialyzer Utilises Function Specifications
### How Dialyzer Uses Function Specifications

Dialyzer infers types for all top-level functions in a module. If the module
also has a spec given in the source-code, Dialyzer will compare the inferred
type to the spec. The comparison checks, for each argument and the return, that
the inferred and specified types overlap - which is to say, the types have at
the inferred and specified types overlap — which is to say, the types have at
least one possible runtime value in common. Notice that Dialyzer does not check
that one type contains a subset of values of the other, or that they're
that one type contains a subset of values of the other, or that they are
precisely equal: This allows Dialyzer to make simplifying assumptions to
preserve performance and avoid reporting program flows which could potentially
succeed at runtime.

If the inferred and specified types do not overlap, Dialyzer will warn that the
spec is invalid with respect to the implementation. If they do overlap, however,
spec is invalid with respect to the implementation. However, if they do overlap,
Dialyzer will proceed under the assumption that the correct type for the given
function is the intersection of the inferred type and the specified type (the
rationale being that the user may know something that Dialyzer itself cannot
deduce). One implication of this is that if the user gives a spec for a function
which overlaps with Dialyzer's inferred type, but is more restrictive, Dialyzer
will trust those restrictions. This may then generate an error elsewhere which
will trust those restrictions. This may then generate an error elsewhere that
follows from the erroneously restricted spec.

_Examples:_
Expand All @@ -159,9 +155,9 @@ Dialyzer inferred, Dialyzer will generate the following warning:

```erlang
some_module.erl:7:2: Invalid type specification for function some_module:foo/1.
The success typing is t:foo
The success typing is some_module:foo
(integer()) -> string()
But the spec is t:foo
But the spec is some_module:foo
(boolean()) -> string()
They do not overlap in the 1st argument
```
Expand All @@ -180,9 +176,9 @@ different, Dialyzer will generate the following warning:

```erlang
some_module.erl:11:2: Invalid type specification for function some_module:bar/1.
The success typing is t:bar
The success typing is some_module:bar
('a' | 'b') -> <<_:8>>
But the spec is t:bar
But the spec is some_module:bar
('a' | 'b') -> atom()
The return types do not overlap
```
Expand Down Expand Up @@ -246,6 +242,7 @@ some_module.erl:31:9: The call t:baz

## Feedback and Bug Reports

We very much welcome user feedback - even wishlists\! If you notice anything
weird, especially if Dialyzer reports any discrepancy that is a false positive,
please send an error report describing the symptoms and how to reproduce them.
We very much welcome user feedback! If you notice anything weird,
especially if Dialyzer reports any discrepancy that is a false
positive, please open an issue describing the symptoms and how to
reproduce them.
35 changes: 17 additions & 18 deletions lib/dialyzer/doc/references/typer_cmd.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,16 +19,16 @@ limitations under the License.
-->
# typer

Typer, a Type annotator for ERlang programs.
TypEr is a **TYP**e annotator for **ER**lang programs.

## Description

TypEr shows type information for Erlang modules to the user. Additionally, it
can annotate the code of files with such type information.
TypEr shows type information for Erlang modules. Additionally, it can
annotate the code of files with such type information.

[](){: #command_line }

## Using TypEr from the Command Line
## Using TypEr

TypEr is used from the command-line. This section provides a brief description
of the options. The same information can be obtained by writing the following in
Expand All @@ -54,24 +54,24 @@ typer [--help] [--version] [--plt PLT] [--edoc]
_Options:_

- **`-r`** - Search directories recursively for .erl files below them. If a list
of files is given, this must be after them.
of files is given, this option must given be after them.

- **`--show`** - Print type specifications for all functions on stdout. (This is
the default behaviour; this option is not really needed.)

- **`--show-exported` (or `show_exported`)** - Same as `--show`, but print
specifications for exported functions only. Specs are displayed sorted
alphabetically on the function's name.
alphabetically according to the function's name.

- **`--annotate`** - Annotate the specified files with type specifications.

- **`--annotate-inc-files`** - Same as `--annotate` but annotates all
`-include()` files as well as all .erl files. (Use this option with caution -
it has not been tested much).
- **`--annotate-inc-files`** - Same as `--annotate`, but annotates all
`-include()` files as well as all .erl files. (Use this option with caution —
it is not well-tested.)

- **`--annotate-in-place`** - Annotate directly on the source code files,
instead of dumping the annotated files in a different directory (use this
option with caution - has not been tested much)
- **`--annotate-in-place`** - Annotate directly in the source code files,
instead of dumping the annotated files in a different directory. (Use this
option with caution — it is not well-tested.)

- **`--edoc`** - Print type information as Edoc `@spec` comments, not as type
specs.
Expand All @@ -80,23 +80,22 @@ _Options:_

- **`-T file*`** - The specified file(s) already contain type specifications and
these are to be trusted in order to print specs for the rest of the files.
(Multiple files or dirs, separated by spaces, can be specified.)
(Multiple files or directories, separated by spaces, can be specified.)

- **`-Dname` (or `-Dname=value`)** - Pass the defined name(s) to TypEr. (\*\*)

- **`-I`** - Pass the include_dir to TypEr. (\*\*)

- **`-pa dir`** - Include `dir` in the path for Erlang. This is useful when
analyzing files that have `-include_lib()` directives or use parse transforms.
analyzing files that use `-include_lib()` directives or parse transforms.

- **`-pz dir`** - Include `dir` in the path for Erlang. This is useful when
analyzing files that have `-include_lib()` directives or use parse transforms.
analyzing files that use `-include_lib()` directives or parse transforms.

- **`--version` (or `-v`)** - Print the TypEr version and some more information
and exit.

> #### Note {: .info }
>
> \*\* options `-D` and `-I` work both from the command line and in the TypEr
> GUI; the syntax of defines and includes is the same as that used by
> [erlc(1)](`e:erts:erlc_cmd.md`).
> \*\* options `-D` and `-I` work the same way as in
> [erlc](`e:erts:erlc_cmd.md`).
58 changes: 29 additions & 29 deletions lib/dialyzer/src/dialyzer.erl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,26 +23,26 @@

-module(dialyzer).
-moduledoc """
Dialyzer, a DIscrepancy AnaLYZer for ERlang programs.
Dialyzer is a **DI**screpancy **A**na**LYZ**er for **ER**lang programs.

Dialyzer is a static analysis tool that identifies software discrepancies, such
as definite type errors, code that has become dead or unreachable because of
programming errors, and unnecessary tests, in single Erlang modules or entire
(sets of) applications.
Dialyzer is a static analysis tool that identifies software
discrepancies, such as definite type errors, code that is unreachable
because of programming errors, and unnecessary tests in single Erlang
modules or an entire codebase.

Dialyzer starts its analysis from either debug-compiled BEAM bytecode or from
Erlang source code. The file and line number of a discrepancy is reported along
with an indication of what the discrepancy is about. Dialyzer bases its analysis
on the concept of success typings, which allows for sound warnings (no false
positives).
Dialyzer starts its analysis from either debug-compiled BEAM code or
from Erlang source code. The file and line number of a discrepancy is
reported along with an indication of the nature of the discrepancy.
Dialyzer bases its analysis on the concept of success typings,
ensuring sound warnings without false positives.

[](){: #command_line }

## Using Dialyzer from the Command Line

Dialyzer has a command-line version for automated use. This section provides a
brief description of the options. The same information can be obtained by
writing the following in a shell:
This section provides a brief description of the options available
when running Dialyzer from the command line. The same information can
be obtained by writing the following in a shell:

```text
dialyzer --help
Expand Down Expand Up @@ -80,9 +80,9 @@ _Options of the command-line version:_

- **`--add_to_plt`** - The PLT is extended to also include the files specified
with `-c` and `-r`. Use `--plt` to specify which PLT to start from, and
`--output_plt` to specify where to put the PLT. Notice that the analysis
possibly can include files from the PLT if they depend on the new files. This
option only works for BEAM files.
`--output_plt` to specify where to put the PLT. Note that files already
included in the PLT will be reanalyzed if they depend on the new files.
This option only works for BEAM files, not source files.

- **`--apps applications`** - By default, warnings will be reported to all
applications given by `--apps`. However, if `--warning_apps` is used, only
Expand All @@ -101,10 +101,10 @@ _Options of the command-line version:_
dialyzer --build_plt --apps erts kernel stdlib mnesia ...
```

to refer conveniently to library applications corresponding to the Erlang/OTP
installation. However, this option is general and can also be used during
analysis to refer to Erlang/OTP applications. File or directory names can also
be included, as in:
to refer conveniently to library applications corresponding to the
Erlang/OTP installation. This option can also be used during
analysis to refer to Erlang/OTP applications. File or directory
names can also be included, as in:

```text
dialyzer --apps inets ssl ./ebin ../other_lib/ebin/my_module.beam
Expand All @@ -124,7 +124,7 @@ _Options of the command-line version:_
- **`--dump_callgraph file`** - Dump the call graph into the specified file
whose format is determined by the filename extension. Supported extensions
are: `raw`, `dot`, and `ps`. If something else is used as filename extension,
default format `.raw` is used.
the default `.raw` format is used.

- **`--error_location column | line`{: #error_location }** - Use a pair
`{Line, Column}` or an integer `Line` to pinpoint the location of warnings.
Expand All @@ -142,7 +142,7 @@ _Options of the command-line version:_
- **`--get_warnings`** - Make Dialyzer emit warnings even when manipulating the
PLT. Warnings are only emitted for files that are analyzed.

- **`--help` (or `-h`)** - Print this message and exit.
- **`--help` (or `-h`)** - Print a help message and exit.

- **`-I include_dir`** - When analyzing from source, pass the `include_dir` to
Dialyzer. (\*\*)
Expand Down Expand Up @@ -246,7 +246,7 @@ _Options of the command-line version:_
> #### Note {: .info }
>
> \*\* the syntax of defines and includes is the same as that used by
> [erlc(1)](`e:erts:erlc_cmd.md`).
> [erlc](`e:erts:erlc_cmd.md`).

[](){: #warning_options }

Expand Down Expand Up @@ -314,10 +314,10 @@ are mostly for Dialyzer developers and internal debugging):
>
> \*\*\* denotes options that turn on warnings rather than turning them off.

The following option is not strictly needed as it specifies the default. It is
primarily intended to be used with the `-dialyzer` attribute. For an example see
section
[Requesting or Suppressing Warnings in Source Files](`m:dialyzer#suppression`).
The following options are not strictly needed as they specify the
default. They are primarily intended to be used with the `-dialyzer`
attribute. For an example see section [Requesting or Suppressing
Warnings in Source Files](`m:dialyzer#suppression`).

- **`-Wno_underspecs`** - Suppress warnings about underspecified functions (the
specification is strictly more allowing than the success typing).
Expand All @@ -331,7 +331,7 @@ section
## Using Dialyzer from Erlang

Dialyzer can be used directly from Erlang. The options are similar to the ones
given from the command line, see section
given from the command line. See section
[Using Dialyzer from the Command Line](`m:dialyzer#command_line`).

## Default Dialyzer Options
Expand Down Expand Up @@ -578,7 +578,7 @@ cl(Opts) ->
end,
doit(F).

-doc "Dialyzer command-line version.".
-doc "Run Dialyzer and return warnings.".
-spec run(Options) -> Warnings when
Options :: [dial_option()],
Warnings :: [dial_warning()].
Expand Down