static-analysis - scanf 在 Frama-C 中没有按预期工作

Question

在下面的程序中，函数dec用于scanf读取用户的任意输入。

dec被调用main并根据输入返回 1 或 0，因此将执行操作。但是，值分析表明y始终是0，即使在调用 之后也是如此scanf。这是为什么？

Answer 1

注意：以下评论适用于早于 Frama-C 15 (Phosphorus, 20170501) 的版本；在 Frama-C 15 中，默认情况下启用 Variadic 插件（其简称为 now -variadic）。

解决方案

• -va在运行值分析 ( ) 之前启用可变参数 ( -val)，它将消除警告并且程序将按预期运行。

详细解释

严格来说，Frama-C 本身（内核）只做解析；由插件本身（例如Value/EVA）来评估程序。

根据您的描述，我相信您一定是在使用 Value/EVA 来分析程序。我不确切知道您使用的是哪个版本，所以我将描述 Frama-C Silicon 的行为。

ACSL（Frama-C 使用的规范语言）的一个限制是目前无法为可变参数函数（例如scanf. 因此，Frama-C 标准库附带的规范是不够的。您可以在以下程序中注意到这一点：

#include <stdio.h>
int d;

int main() {
  scanf("%d", &d);
  Frama_C_show_each(d);
  return 0;
}

运行frama-c -val file.c将输出，除其他外：

...
[value] using specification for function scanf
FRAMAC_SHARE/libc/stdio.h:150:[value] warning: no \from part for clause 'assigns *__fc_stdin;' of function scanf
[value] Done for function scanf
[value] Called Frama_C_show_each({0})
...

该警告意味着规范不正确，这解释了奇怪的行为。

在这种情况下，解决方案是使用 Variadic 插件（-va或-va-help更多详细信息），它将专门化 variadic 调用并为其添加规范，从而避免警告并按预期运行。-print以下是在上例中运行 Variadic 插件后的结果代码 ( )：

$ frama-c -va file.c -print

[... lots of definitions from stdio.h ...]

/*@ requires valid_read_string(format);
    requires \valid(param0);
    ensures \initialized(param0);
    assigns \result, *__fc_stdin, *param0;
    assigns \result
      \from (indirect: *__fc_stdin), (indirect: *(format + (0 ..)));
    assigns *__fc_stdin
      \from (indirect: *__fc_stdin), (indirect: *(format + (0 ..)));
    assigns *param0
      \from (indirect: *__fc_stdin), (indirect: *(format + (0 ..)));
 */
int scanf_0(char const *format, int *param0);

int main(void)
{
  int __retres;
  scanf_0("%d",& d);
  Frama_C_show_each(d);
  __retres = 0;
  return __retres;
}

在此示例中，scanf专门用于scanf_0，并带有适当的 ACSL 注释。在这个程序上运行 EVA 不会发出任何警告并产生预期的输出：

@ frama-c -va file.c -val 

...
[value] Done for function scanf_0
[value] Called Frama_C_show_each([-2147483648..2147483647])
...

注意：Frama-C 14 (Silicon) 中的 GUI 不允许启用 Variadic 插件（即使在分析面板中勾选后），因此在这种情况下您必须使用命令行才能获得预期的结果并避免警告。从 Frama-C 15（磷，将于 2017 年发布）开始，这将不是必需的：默认情况下将启用 Variadic，因此您的示例从一开始就可以工作。