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

Question

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

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

Answer 1

注意：以下注释适用于 Frama-C 15（Phosphorus，20170501）之前的版本；在 Frama-C 15 中，Variadic 插件默认启用（现在它的简称为 -variadic）。

解决方案

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

详细解释

严格来说，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 调用并为其添加规范，从而避免警告并按预期行为。这是上面示例中运行 Variadic 插件之后的结果代码 (-print)：

$ 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 插件（即使在 Analyses 面板中勾选它之后），所以在这种情况下，您必须使用命令行来获得预期的结果并避免警告。从 Frama-C 15（Phosphorus，将于 2017 年发布）开始，这将不是必需的：Variadic 将默认启用，因此您的示例从一开始就可以工作。

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

scanf not working as expected in Frama-C

static-analysis

frama-c

value-analysis

解决方案

详细解释