Frama-C 的 Eva 插件分析完成后报告 "invalid user input"

Question

当我尝试将 Eva 插件应用于 C 项目时，我收到以下日志。

[eva:summary] ====== ANALYSIS SUMMARY ======
  ----------------------------------------------------------------------------
  53 functions analyzed (out of 9107): 0% coverage.
  In these functions, 5300 statements reached (out of 14354): 36% coverage.
  ----------------------------------------------------------------------------
  Some errors and warnings have been raised during the analysis:
    by the Eva analyzer:      0 errors   15 warnings
    by the Frama-C kernel:    0 errors    2 warnings
  ----------------------------------------------------------------------------
  45 alarms generated by the analysis:
      29 invalid memory accesses
       4 accesses out of bounds index
       6 invalid shifts
       1 access to uninitialized left-values
       5 others
  ----------------------------------------------------------------------------
  Evaluation of the logical properties reached by the analysis:
    Assertions     1113 valid    18 unknown     1 invalid   1132 total
    Preconditions     0 valid     0 unknown     0 invalid      0 total
  98% of the logical properties reached have been proven.
  ----------------------------------------------------------------------------
[kernel] Warning: warning CERT:MSC:38 treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.

Frama-C 在提供分析摘要后中止了分析。但是，它并没有指出哪个文件和哪一行代码有问题。你能告诉我在这种情况下可能存在哪些问题吗？分析完成了吗？

Answer 1

正如该行的 header 所示，该消息不是 Eva 发出的，而是由 Frama-C 的 kernel 发出的。此错误表明您的代码违反了 CERT C 编码标准，更具体地说，它的 rule MSC-38 基本上表明声明属于标准库的标识符是个坏主意，在标准库中它们被指定为可能实现为一个宏。这特别包括 assert 和 errno.

由于此规则表明代码不严格 ISO-C 兼容，因此已决定默认将其视为错误，但考虑到问题本身不太可能使分析器崩溃，Frama-C不会一触发就中止。这就是为什么您仍然可以启动 Eva，它运行完美，然后内核提醒您的代码中存在问题（第一条消息，警告状态，可能在日志开头输出）。

您可以使用 -kernel-warn-key CERT:MSC:38=<status> 修改 CERT:MSC:38 的严重性状态，其中 <status> 的范围可以从 inactive（完全忽略）到 abort（发出错误并立即中止）。可以在 section 6.2 of the user manual.

上找到完整的状态列表

Frama-C 的 Eva 插件分析完成后报告 "invalid user input"

Eva plugin of Frama-C reports "invalid user input" after finishing analysis

frama-c