Thank you, Stavros!<br><br><div class="gmail_quote">On 5 July 2012 21:36, Stavros Aronis <span dir="ltr"><<a href="mailto:aronisstav@gmail.com" target="_blank">aronisstav@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi again,<div><br></div><div>your example shows another case of the "might also be correct" rationale of Dialyzer. Your full code is:</div><div><br></div><div><div>-spec handle_cast(term(), #state{}) -> {noreply, NewState :: #state{}}.</div>
<div><br></div><div>handle_cast({asd}, _State) -></div><div class="im"><div> NewState = {bugotak},</div><div> {noreply, NewState};</div></div><div>handle_cast(_Msg, State) -></div><div> {noreply, State}.</div>
</div><div><br></div>
<div>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.</div>
</blockquote><div><br></div><div>Why signature `my_module:handle_cast(term(),term()) -> {'noreply',term()}` used? Is it taken from -callback signature, all right?</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div> 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.</div>
<div><br></div><div>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!<span class="HOEnZb"><font color="#888888"><br>
<br>Stavros</font></span><div><div class="h5"><br><br><div class="gmail_quote">On Thu, Jul 5, 2012 at 4:31 PM, Maxim Treskin <span dir="ltr"><<a href="mailto:zerthurd@gmail.com" target="_blank">zerthurd@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hello!<div><br></div><div>File attached.</div><div>Just compile it with</div><div><br></div><div>erlc +debug_info my_module.erl</div><div><br></div><div>then</div><div><br></div><div>dialyzer . --plt ~/.r15b01_dialyzer.plt --no_native -Werror_handling -Wrace_conditions -Wunderspecs</div>
<div><br></div><div>and I see:</div><div><br></div><div><div> Checking whether the PLT /home/zert/.r15b01_dialyzer.plt is up-to-date... yes</div><div> Proceeding with analysis... done in 0m0.39s</div><div>done (passed successfully)</div>
<div><br></div><br><div class="gmail_quote"><div><div>On 5 July 2012 20:22, Stavros Aronis <span dir="ltr"><<a href="mailto:aronisstav@gmail.com" target="_blank">aronisstav@gmail.com</a>></span> wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div>
Hi!<br><br>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'!<div><br>
</div><div>- 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.</div>
<div>- 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.</div>
<div>- Spec attributes are also taken into account when anayzing callbacks in the following manner:</div><div>-- 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.</div>
<div>-- Second, the spec is used to check the arguments and return value of the function, as is the case with any spec.</div><div><br></div><div>For gen_server, the -callback attributes can be seen <a href="https://github.com/erlang/otp/blob/maint/lib/stdlib/src/gen_server.erl#L123" target="_blank">here</a>. 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?</div>
<span><font color="#888888"><div><br></div><div>Stavros</div></font></span><br></div></div>_______________________________________________<br>
erlang-questions mailing list<br>
<a href="mailto:erlang-questions@erlang.org" target="_blank">erlang-questions@erlang.org</a><br>
<a href="http://erlang.org/mailman/listinfo/erlang-questions" target="_blank">http://erlang.org/mailman/listinfo/erlang-questions</a><br>
<br></blockquote></div><span><font color="#888888"><br><br clear="all"><div><br></div>-- <br>Max Treskin<br>
</font></span></div>
</blockquote></div><br></div></div></div>
</blockquote></div><br><br clear="all"><div><br></div>-- <br>Max Treskin<br>