为什么Dialyzer相信规格中有太具体的返回类型

Question

我希望添加规范永远不会降低的安全性，但在以下情况下正是这样。

在下面的代码中，Dialyzer(错误地(相信我bar的返回类型是1。这导致它说foo((中的模式永远无法匹配——如果注意到这一错误建议，就会导致运行时错误！

-module(sample).
-export([foo/0]).
foo() ->
case bar() of
1 -> ok;
2 -> something
end.
-spec bar() -> 1.
bar() ->
rand:uniform(2).

删除bar/0的规范解决了问题——但为什么Dialyzer信任我？Dialyzer违反了其"；没有假阳性"；这里承诺：当没有bug时，它会发出警告。更糟糕的是，Dialyzer推出了一个新的bug。

Answer 1

Dialyzer在检查其规范之前计算每个函数的成功类型，此操作有几种可能的结果：

1. 规范类型与成功类型不匹配：无效类型规范警告
2. 规范类型是成功类型的严格超类型：警告仅与-Wunderspecs或-Wspecdiffs一起使用
3. spec类型是成功类型的严格子类型：Warning only with-Woverspecsor-Wspecdiffs
4. 规格类型和成功类型完全匹配：一切都很好
5. 规范类型和成功类型重叠但不完全匹配(如-1..1和pos_integer()(：与2相同

对于1，它继续使用success类型，否则继续使用suc成功类型和spec类型之间的交集。

您的情况是3，这通常不会被警告，因为作为程序员，您更清楚(就透析器而言，也许rand:uniform(2)只能返回1(。你可以用激活它

{dialyzer, [{warnings, [underspecs,overspecs]}]}.

在rebar.config文件中

Answer 2

Dialyzer自己的分析(目前(基于几种过近似，因此它无法判断您的更严格规范是由于您绝对错误还是由于Dialyzer在某个地方过近似。

因此，它选择信任您的规范，并在以后根据该信息报告最终错误。

一般来说，其他现代系统的类型错误相关信息带有"错误"；报告了所有部件，并且没有明确指定责任"；因此。事实上，这里的推理、规范和模式是不兼容的，但Dialyzer只指责模式。这是一个怪癖，在使用时要记住。