Dialyzer does not report errors when module having abstraction violation on opaque type.

[zxq9]

On 2019/12/28 16:25, by wrote:
 > %% opaque1.erl
 > -module(opaque1).
 > -export_type([test_text/0]).
 > -opaquetest_text() :: [{atom(), number()}].
 > -export([make_text/0]).
 >
 > -spec make_text() ->test_text().
 >
 > make_text() ->
 >      [{a,1}, {c,3}].

[snip]

 > %% opaque2.erl
 > -module(opaque2).
 > -export([test/0]).
 >
 > test() ->
 >     X = opaque1:make_text(),
 >     [F||{F, _} <- X]. % This violates the abstraction
 >
 > Run dialyzer on these two modules will produce:
 > %%%%
 > MacBookPro:dialyzer by$ dialyzer opaque1.erl
 >    Checking whether the PLT /Users/by/.dialyzer_plt is up-to-date... yes
 >    Proceeding with analysis... done in 0m0.12s
 > done (passed successfully)
 > MacBookPro:dialyzer by$
 > %%%%
 >
 > %%%%
 > MacBookPro:dialyzer by$ dialyzer opaque2.erl
 >    Checking whether the PLT /Users/by/.dialyzer_plt is up-to-date... yes
 >    Proceeding with analysis...
 > Unknown functions:
 >    opaque1:make_text/0
 >   done in 0m0.13s
 > done (passed successfully)
 > MacBookPro:dialyzer by$
 > %%%%
 >
 > Am I missing something?
Two things:
1- You need to dialyze BOTH modules in the same run or else Dialyzer 
cannot see the typespecs in opaque1.erl while it is evaluating opaque2.erl
2- You can write code that violates opaque types, though I believe 
Dialyzer will issue a warning about it if you evaluate both at once.

-Craig