1

我对价值分析模块的选项和一些扩展选项有一些疑问。

我使用命令：frama-c-gui -val -slevel 100 -plevel 300 -absolute-valid-range 0x00000000-0xffffffff -metrics -metrics-value-cover -scope-def-interproc -main MYMAIN CODE/*.c

  • 在一个文件上，-metrics给我 3goto一个没有的函数，goto计算如何？

  • 什么是“覆盖率估计 = 100.0%”，-metrics-value-cover我得到一个介于 80% 和 100% 之间的值，一开始我认为当我有死代码时得到 <100%，但是当我得到 100% 时我有死代码，所以我认为得到100% 如果源文件中的所有函数都被分析？

  • 我想157 stmts in analyzed functions, 148 stmts analyzed (94.3%)这意味着我的项目上有死代码，是吗？

  • 使用选项-scope-def-interproc我收到 32 个警告（没有 62 个）但在网站上，我们可以阅读（在范围文档中）

    因此，用户应仔细检查值分析发出的警报。

所以我需要验证所有 62 个警告还是仅通过此选项获得 32 个？

4

2 回答 2

2

什么是 -metrics-value-cover 的“覆盖率估计 = 100.0%” 我得到一个介于 80 和 100% 之间的值，一开始我认为当我有死代码时得到 <100%，但是当我得到 100 时我有死代码%，所以我认为如果源文件中的所有函数都被分析，我认为得到 100%？

让我们举个例子。

[metrics] Value coverage statistics
      =========================
      Syntactically reachable functions = 3 (out of 3)
      Semantically reached functions = 1
      Coverage estimation = 33.3% 

      Unseen functions (2) =
        <tests/metrics/reach.c>: baz; foo;

第一行Syntactically reachable functions是程序中可能最终被调用的函数数量的过度近似，从main. 例如，从不获取地址且从不直接调用的函数将不会在此集合中。

Semantically reached functions是值分析确实分析的程序的功能数量。

Coverage estimation是这两个数字之间的比率。对于所有功能都可以访问的小程序，通常是100%。

Unseen functions是预期会到达（语法上）但从未被 Value 分析过的函数列表。

请注意，这些数字都没有涉及指令，因此您仍然可能 100% 使用死代码。

于 2014-07-29T14:03:30.910 回答
2

在单个文件上，-metrics [introduces] 3 goto on a function [that doesn't have any]

C 结构&&,||并且break;可以“规范化”为 goto 结构。

我想分析函数中有 157 个 stmts，分析了 148 个 stmts (94.3%)，这意味着我的项目中有死代码，是吗？

是的。对于价值分析可见的输入，157 条语句中只有 148 条是可访问的。请注意，例如，如果main()有参数argc和argv，则为这些参数构建的抽象值可能不包含应考虑的所有值。确定这 9 条语句是否真的无法访问的最好方法是查看它们（它们在 Frama-C 的 GUI 中显示为红色）。

使用选项 -scope-def-interproc 我收到 32 个警告（没有 62 个）但在网站上，我们可以阅读（在范围文档中）

目前还不是很清楚你在问什么。如果您提供了一个包含完整信息（源代码、命令行）的示例，这将有所帮助，以便可以重现您的步骤并为您阐明所发出消息的含义。如果无法获得完整的示例，请制作一个小的简化示例：也（几乎）不可能用目前提供的信息回答您。

于 2014-06-20T20:59:40.117 回答