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

[by]

Yes, you are right.

I get the warning after evaluate both modules at the same time.

The warning is:
%%%%
MacBookPro:dialyzer by$ dialyzer opaque1.erl opaque2.erl 
  Checking whether the PLT /Users/by/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis...
opaque2.erl:5: Function test/0 has no local return
opaque2.erl:7: The created fun has no local return
opaque2.erl:7: The attempt to match a term of type 
          opaque1:test_text() against the pattern 
          [{F, _} | _] breaks the opacity of the term
opaque2.erl:7: The attempt to match a term of type 
          opaque1:test_text() against the pattern 
          [] breaks the opacity of the term
opaque2.erl:7: Fun application with arguments 
         (X :: opaque1:test_text()) will never return since it differs in the 1st argument from the success typing arguments: 
         ([any()])
 done in 0m0.17s
done (warnings were emitted)
MacBookPro:dialyzer by$ 
%%%%

Thank you!

Kind Regards,
Yao

> 在 2019年12月28日，16:43，zxq9 <zxq9@REDACTED> 写道：
> 
> 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20191228/b96a0f5c/attachment.htm>