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

Maxim Treskin zerthurd@REDACTED
Thu Jul 5 19:12:21 CEST 2012


Thank you, Stavros!

On 5 July 2012 21:36, Stavros Aronis <aronisstav@REDACTED> wrote:

> Hi again,
>
> your example shows another case of the "might also be correct" rationale
> of Dialyzer. Your full code is:
>
> -spec handle_cast(term(), #state{}) -> {noreply, NewState :: #state{}}.
>
> handle_cast({asd}, _State) ->
>     NewState = {bugotak},
>     {noreply, NewState};
> handle_cast(_Msg, State) ->
>     {noreply, State}.
>
> It is true that the return value of the first clause violates the spec,
> but this information is lost within Dialyzer as the "general" type
> signature that Dialyzer will find and use
> is my_module:handle_cast(term(),term()) -> {'noreply',term()} due to the
> second clause.
>

Why signature `my_module:handle_cast(term(),term()) ->
{'noreply',term()}`  used? Is it taken from -callback signature, all right?


> This more general type signature "absorbs" and hides the incorrect result.
> The function "can work" if you only call with a message different than
> {asd} and provide a correct #state{} as input, so Dialyzer remains silent.
> If, on the other hand, you had just the first clause, or both clauses
> returned a value that couldn't be #state{}, you would get a warning.
>
> Remember that Dialyzer does not promise to find all the bugs in your code.
> It might be interesting and possible to check the return value of each
> separate clause of a function, if there exists a spec, however... Thanks
> for the example and idea!
>
> Stavros
>
>
> On Thu, Jul 5, 2012 at 4:31 PM, Maxim Treskin <zerthurd@REDACTED> wrote:
>
>> 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
>>
>
>


-- 
Max Treskin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20120706/4e368345/attachment.htm>


More information about the erlang-questions mailing list