[erlang-questions] Dialyzer cannot catch gen_server callback return type error

[Maxim Treskin]

Hello!

File attached.
Just compile it with

erlc +debug_info my_module.erl

then

dialyzer . --plt ~/.r15b01_dialyzer.plt --no_native -Werror_handling
-Wrace_conditions -Wunderspecs

and I see:

  Checking whether the PLT /home/zert/.r15b01_dialyzer.plt is up-to-date...
yes
  Proceeding with analysis... done in 0m0.39s
done (passed successfully)


On 5 July 2012 20:22, Stavros Aronis <aronisstav@REDACTED> wrote:

> Hi!
>
> Your description is not very clear, so it might be better to send me some
> code snippet off-list, but let me put some facts here to make sure that the
> expectations from Dialyzer are 'reasonable'!
>
> - Dialyzer first uses the -callback attibutes of the behaviour and will
> always warn if the arguments or return value of a callback function are not
> subtypes of those attributes. If e.g. the return value of a callback is
> expected to be {noreply, term()} and the callback always returns {reply,
> term(), term()}, Dialyzer will warn about this.
> - As long as your implementation can possibly return an acceptable value,
> Dialyzer is happy. You might have a callback that either returns a correct
> value or something else that cannot be handled by the behaviour, but
> Dialyzer will assume that the correct term will always be returned. This
> happens because Dialyzer should never emit a false warning and this
> additional bad value might have been inferred because Dialyzer's analysis
> was not strong enough to exclude it.
> - Spec attributes are also taken into account when anayzing callbacks in
> the following manner:
> -- First the specs themselves are checked for compatibility with the
> -callback attributes of the behaviour. Here it is the user (and not
> Dialyzer) that writes these specs, so if these specs allow more values you
> get a warning. The rationale is that if you are providing a spec it should
> be at least as restrictive as the callback attribute.
> -- Second, the spec is used to check the arguments and return value of the
> function, as is the case with any spec.
>
> For gen_server, the -callback attributes can be seen here<https://github.com/erlang/otp/blob/maint/lib/stdlib/src/gen_server.erl#L123>.
> There, the State and NewState can be any terms. If you also have a spec
> saying that this callback function should return {noreply, State ::
> #state{}} and you return {noreply, {bugotak}} then you are violating your
> own spec (but not the callback attribute of gen_server) and you should get
> a warning. Is this not the case when you run Dialyzer?
>
> Stavros
>
> _______________________________________________
> erlang-questions mailing list
> erlang-questions@REDACTED
> http://erlang.org/mailman/listinfo/erlang-questions
>
>


-- 
Max Treskin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20120705/ea974a66/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: my_module.erl
Type: application/octet-stream
Size: 957 bytes
Desc: not available
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20120705/ea974a66/attachment.obj>