Dialyzer warns about no_exit on bad record construction - is this a bug?

Question

When Dialyzer encounters a record literal where a required field is not initialized, it thinks control flow stops at the line with the record literal.

Example:

-module(sample).
-export([foo/0]).
-record(boo, {a :: number()}).
foo() ->
    erlang:display(#boo{}).

Errors:

13> dialyzer:run([{files, ["/Users/mheiber/sample.erl"]}, {from, src_code}]).
[{warn_return_no_exit,
     {"/Users/mheiber/sample.erl",11},
     {no_return,[only_normal,foo,0]}},
 {warn_matching,
     {"/Users/mheiber/sample.erl",12},
     {record_constr,
         ["#boo{a::'undefined'}","a::number()"]}}]

Is this a bug? The runtime semantics of Erlang do not match how Dialyzer is modeling them: ERTS (for better or worse!) chugs along, happily assigning the atom 'undefined' to to any unitialized fields.

Clarification: what I mean here is that it's preferable, where feasible, for the static checking to reflect how Erlang works at run time.

So is this a Dialyzer bug?

The way Dialyzer handles these incorrectly-initialized records is pernicious, because it can trigger a cascade of spurious warnings–when Dialyzer thinks a line of function foo is unreachable, any functions that are reachable only from foo are also considered dead.

Answer 1

No, it's not a bug.

I'd say that it's a limitation caused by the fact that Erlang is dynamically typed and that the -type directives are not used in runtime.

Dialyzer is built on top of ERTS, not the other way around.

The problem in this case is that dialyzer does not know how to continue its execution: Should it use the type defined in the record definition or the actual record initialization? It reports an error and the actual fix is left to the programmer.