为什么Dialyzer相信具有过于具体的返回类型的规范?

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

在下面的代码中,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 在这里违反了它的“无误报”承诺:它在没有错误时发出警告。并且(甚至更糟)透析器轻推引入一个新的错误。

回答

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

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

对于 1,它继续成功类型,否则继续成功类型和规范类型之间的交集。

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

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

rebar.config文件中


回答

Dialyzer 自己的分析(目前)基于几种过度近似,因此它无法辨别您更严格的规范是由于您绝对错误还是由于 Dialyzer 在某处过度近似。

因此,它选择信任您的规范,然后根据该信息报告确定的错误。

通常,由于这个原因,其他现代系统的类型错误相关信息带有“报告的所有部分并且没有明确分配的责任”。这里实际上是推理、规范和模式不兼容的情况,但 Dialyzer 只是指责模式。这是使用它时要记住的一个怪癖。


以上是为什么Dialyzer相信具有过于具体的返回类型的规范?的全部内容。
THE END
分享
二维码
< <上一篇
下一篇>>