Frama-C 语法错误？

Question

我有一个入口点，我想运行 pdg-dot 打开，但是在我将头文件移动到正确的位置后，我得到了这个语法错误。

gtkwin.c:77:[kernel] user error: syntax error

在源代码中，该行只是一个 GdkPixmap 声明。如何让 Frama-C 立即创建我的 .dot 文件？

这是我的命令和输出：

frama-c -main pt_main -pdg -pdg-dot ptmain gtkwin.c 
[kernel] preprocessing with "gcc -C -E -I.  gtkwin.c"
gtkwin.c:77:[kernel] user error: syntax error
[kernel] user error: skipping file "gtkwin.c" that has errors.
[kernel] Frama-C aborted: invalid user input.

它应该只是运行通过我的函数并创建 .dot 文件。我试过只注释掉这一行，但我仍然以某种方式遇到相同的语法错误。

Answer 1

您是否正在使用 PuTTY for Unix 的 gtkwin.c？ PuTTY的第77行gtkwin.c也是GdkPixmap *pixmap;.

您可能会看到 "user error: syntax error"，因为 C 文件没有完全预处理，或者可能有一些 Frama-C 无法识别的语法。例如，当我在 Mac OS 10.10.4:

上尝试以下命令时

CPP="gcc -E `pkg-config --cflags gtk+-2.0 gdk-2.0` -I/opt/X11/include -I/usr/include -I. -Icharset -Iunix" \
frama-c -kernel-msg-key pp -no-cpp-gnu-like -main pt_main -pdg -pdg-dot ptmain unix/gtkwin.c

（请注意，我不得不注释掉 #include <gdk/gdkx.h>，因为我的 GTK+ 构建使用石英后端而不是 X11 后端。）

我得到：

[kernel] Parsing unix/gtkwin.c (with preprocessing)
/usr/include/sys/qos.h:124:[kernel] user error: syntax error
[kernel] user error: stopping on file "unix/gtkwin.c" that has errors.
[kernel] Frama-C aborted: invalid user input.

在上面的frama-c命令中，我添加了-kernel-msg-key pp。 frama-c 的这个选项允许您查看内核使用的预处理命令。使用 -kernel-msg-key pp，您应该会在 frama-c 输出中看到如下内容：

[kernel:pp] preprocessing with "..."

运行引号中列出的命令并将预处理后的输出重定向到临时文件。使用预处理器添加的行号信息，您将需要在预处理输出中找到相应的行。在我的例子中，/usr/include/sys/qos.h 的第 124 行对应于预处理输出的第 9896 行：

enum { QOS_CLASS_USER_INTERACTIVE __attribute__((availability(macosx,introduced=10.10))) = 0x21, QOS_CLASS_USER_INITIATED __attribute__((availability(macosx,introduced=10.10))) = 0x19, QOS_CLASS_DEFAULT __attribute__((availability(macosx,introduced=10.10))) = 0x15, QOS_CLASS_UTILITY __attribute__((availability(macosx,introduced=10.10))) = 0x11, QOS_CLASS_BACKGROUND __attribute__((availability(macosx,introduced=10.10))) = 0x09, QOS_CLASS_UNSPECIFIED __attribute__((availability(macosx,introduced=10.10))) = 0x00, }; typedef unsigned int qos_class_t;

我看到的可能是 "user error: syntax error" 消息，因为无法识别 __attribute__((availability(macosx,introduced=10.10))) 语法。事实上，一旦我将 -D '__attribute__(...)=' 添加到 CPP 命令以删除所有属性，我就会看到不同的错误：

/usr/include/sys/_types/_sigset_t.h:30:[kernel] user error: redefinition of 'sigset_t' in the same scope. Previous declaration was at FRAMAC_SHARE/libc/__fc_define_sigset_t.h:25
unix/gtkwin.c:143:[kernel] warning: Calling undeclared function GDK_DISPLAY. Old style K&R code?
unix/gtkwin.c:1766:[kernel] warning: Calling undeclared function GDK_ROOT_WINDOW. Old style K&R code?
unix/gtkwin.c:2636:[kernel] warning: Calling undeclared function GDK_WINDOW_XWINDOW. Old style K&R code?

我正在使用 Frama-C Sodium-20150201。

TL;DR 尝试查看预处理的输入文件。

Answer 2

所以我运行没有-no-cpp-gnu-like 的预处理和 Frama-C 命令。它似乎给了我一个更深入的理由来解释为什么 Frama-C 不会运行在文件上，尽管除了它告诉我报告错误之外我很难理解它。这真的是我需要报告的错误还是常见的 Frama-C 标志？这是我尝试运行 Frama-C 时的转储。

[kernel] /* compiler builtin: 
[kernel]    void *__builtin_frame_address(unsigned int);   */
gtkwin.c:77:[kernel] user error: syntax error
[kernel] Current source was: /usr/share/frama-c/libc/__fc_builtin_for_normalization.i:43
[kernel] The full backtrace is:
[kernel] Raised at file "cil/src/frontc/frontc.ml", line 127, characters 10-29
[kernel] Called from file "cil/src/frontc/frontc.ml", line 86, characters 13-38
[kernel] Called from file "cil/src/frontc/frontc.ml", line 140, characters 13-32
[kernel] Called from file "src/kernel/file.ml", line 913, characters 6-23
[kernel] Called from file "src/kernel/file.ml", line 1049, characters 23-30
[kernel] Re-raised at file "src/kernel/file.ml", line 1055, characters 52-55
[kernel] Called from file "list.ml", line 84, characters 24-34
[kernel] Called from file "src/kernel/file.ml", line 1046, characters 6-495
[kernel] Called from file "src/kernel/file.ml", line 1933, characters 12-30
[kernel] Called from file "src/kernel/file.ml", line 2017, characters 4-27
[kernel] Called from file "src/kernel/ast.ml", line 103, characters 2-28
[kernel] Called from file "src/kernel/ast.ml", line 114, characters 53-71
[kernel] Called from file "src/kernel/boot.ml", line 29, characters 6-20
[kernel] Called from file "src/kernel/cmdline.ml", line 732, characters 2-9
[kernel] Called from file "src/kernel/cmdline.ml", line 212, characters 4-8
[kernel] 
[kernel] Unexpected error (Parsing.Parse_error).
[kernel] Please report as 'crash' at http://bts.frama-c.com/.
[kernel] Your Frama-C version is Fluorine-20130601.
[kernel] Note that a version and a backtrace alone often do not contain enough
[kernel] information to understand the bug. Guidelines for reporting bugs are at:
[kernel] http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines

上面是一堆更多的编译器内置警告，不确定它们是否有必要帮助理解输出。预处理似乎修复了一些错误，但不是我需要的错误。

Frama-C 语法错误？

Frama-C syntax error?

c

graph

dot

frama-c