The easy answer to questions of type "why Dialyzer doesn't..." is "because it has been designed to be always correct" or "because it never promises that it will catch everything or anything specific". For the more complex answer, you need to specify your question further. If I write your example in a module:
$ dialyzer bar.erl
Checking whether the PLT /home/stavros/.dialyzer_plt is up-to-date... yes
Proceeding with analysis... done in 0m0.64s
done (passed successfully)
... neither discrepancy is 'detected', cause neither is an "error". It's just the case that the code is in some ways more generic (can return extra values) and in some ways more restrictive (cannot handle every integer, for version 1) than the spec. The second version's problem can be found with -Woverspecs :
$ dialyzer -Woverspecs bar.erl
Checking whether the PLT /home/stavros/.dialyzer_plt is up-to-date... yes
Proceeding with analysis...
bar.erl:11: Type specification bar:myfun2(integer()) -> 'zero' | 'one' is a subtype of the success typing: bar:myfun2(_) -> 'one' | 'other_number' | 'zero'
done in 0m0.58s
done (warnings were emitted)
The warning explains exactly that the spec is more restrictive than the code. Both problems can also be detected by the extremely unusual -Wspecdiffs :
$ dialyzer -Wspecdiffs bar.erl
Checking whether the PLT /home/stavros/.dialyzer_plt is up-to-date... yes
Proceeding with analysis...
bar.erl:5: Type specification bar:myfun1(integer()) -> 'zero' | 'one' is not equal to the success typing: bar:myfun1(0 | 1 | 2) -> 'one' | 'other_number' | 'zero'
bar.erl:11: Type specification bar:myfun2(integer()) -> 'zero' | 'one' is a subtype of the success typing: bar:myfun2(_) -> 'one' | 'other_number' | 'zero'
done in 0m0.61s
done (warnings were emitted)
Neither -Woverspecs nor -Wspecdiffs mode of operation is encouraged, as Dialyzer's type analysis can and will generalize types, so "something being specified in a more restrictive way" can be the result of generalization. It can also be the case that you intend these functions to be called only with 0 and 1 as arguments, in which case the spec is 'ok'.
1条答案
按热度按时间tyu7yeag1#
The easy answer to questions of type "why Dialyzer doesn't..." is "because it has been designed to be always correct" or "because it never promises that it will catch everything or anything specific".
For the more complex answer, you need to specify your question further. If I write your example in a module:
And Dialyze it:
... neither discrepancy is 'detected', cause neither is an "error". It's just the case that the code is in some ways more generic (can return extra values) and in some ways more restrictive (cannot handle every integer, for version 1) than the spec.
The second version's problem can be found with
-Woverspecs
:The warning explains exactly that the spec is more restrictive than the code.
Both problems can also be detected by the extremely unusual
-Wspecdiffs
:Neither
-Woverspecs
nor-Wspecdiffs
mode of operation is encouraged, as Dialyzer's type analysis can and will generalize types, so "something being specified in a more restrictive way" can be the result of generalization.It can also be the case that you intend these functions to be called only with 0 and 1 as arguments, in which case the spec is 'ok'.