【问题标题】:Frama-C syntax error?Frama-C 语法错误?
【发布时间】:2015-07-11 17:38:05
【问题描述】:

我有一个要在其上运行 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 文件。我试过只是注释掉这一行,但我仍然以某种方式得到相同的语法错误。

【问题讨论】:

  • 您需要发布的不仅仅是模糊的描述。 stackoverflow.com/help/mcve
  • gtkwin.c 的第 77 行以及该行周围的行是什么?
  • @DanielTrebbien 这是第 77 行:GdkPixmap *pixmap;它周围的一切也是 struct gui_data 中的声明。抱歉,格式已关闭,我是在 stackoverflow 上发帖的新手

标签: c graph dot frama-c


【解决方案1】:

您是否有机会使用来自 PuTTY for Unix 的 gtkwin.c? PuTTY的gtkwin.c的第77行也是GdkPixmap *pixmap;

您可能会看到“用户错误:语法错误”,因为 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 后端。)

我明白了:

[内核] 解析 unix/gtkwin.c(带预处理) /usr/include/sys/qos.h:124:[kernel] 用户错误:语法错误 [内核] 用户错误:在有错误的文件“unix/gtkwin.c”上停止。 [内核] Frama-C 中止:无效的用户输入。

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

[kernel:pp] 使用“...”进行预处理

运行引号中列出的命令并将预处理的输出重定向到临时文件。使用预处理器添加的行号信息,您将需要在预处理输出中找到相应的行。在我的例子中,/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;

我可能会看到“用户错误:语法错误”消息,因为无法识别 __attribute__((availability(macosx,introduced=10.10))) 语法。事实上,一旦我在 CPP 命令中添加了-D '__attribute__(...)=' 以删除所有属性,我就看到了不同的错误:

/usr/include/sys/_types/_sigset_t.h:30:[kernel] 用户错误:在同一范围内重新定义“sigset_t”。先前的声明位于 FRAMAC_SHARE/libc/__fc_define_sigset_t.h:25 unix/gtkwin.c:143:[kernel] 警告:调用未声明的函数 GDK_DISPLAY。旧式 K&R 代码? unix/gtkwin.c:1766:[kernel] 警告:调用未声明的函数 GDK_ROOT_WINDOW。旧式 K&R 代码? unix/gtkwin.c:2636:[kernel] 警告:调用未声明的函数 GDK_WINDOW_XWINDOW。旧式 K&R 代码?

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


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

【讨论】:

  • 感谢您提供如此详细的答案。似乎我们的解析器不支持枚举声明的属性(我认为这是 GCC 扩展)。您对#define out __attribute__ 的解决方案可能是目前最好的解决方案。
  • @DanielTrebbien 我以为我可以正常工作,但是我去打开文件并最终得到与以前相同的错误,即使是预处理文件。我尝试使用您包含的额外 Frama-C 命令,但这些命令也给了我错误。即:frama-c -kernel-msg-key pp -no-cpp-gnu-like -main pt_main -pdg -pdg-dot gtkwin.i [kernel] user error: option `-no-cpp-gnu-like' is unknown. use `frama-c -help' for more information. [kernel] Frama-C aborted: invalid user input.
  • @DanielTrebbien 也是,我正在使用 PuTTY for Unix
  • 嗨@Adam。尝试不使用 -no-cpp-gnu-like 选项。我只使用它是因为 Mac 预装了 Clang,而不是 gcc 和 GNU 工具。
  • @Adam 选项 -no-cpp-gnu-like 是 Frama-C Sodium 中的新功能。 @Daniel Trebbien:对于我们想到的用法,Clang 预处理器与 GCC 足够兼容,因此您可以改为设置 -cpp-gnu-like
【解决方案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 升级为 Sodium,并报告是否发生崩溃剧照?如果是这样,我会尝试调查。
  • 其实丹尼尔的解析也失败了,其他原因。不过,升级到 Sodium 可能会有所帮助。
  • 关于如何做到这一点的任何建议?我直接从网站下载了我的版本,Frama-C 中是否有更新选项,或者我必须获得全新的下载,如果有,我从哪里获得?
  • 您应该像安装 Fluorine 一样安装 Sodium:下载 tarball,然后配置/制作/安装。 (除非您下载了二进制文件,但在这种情况下,是哪个?)
  • 是的,事实证明我已经解压了 Sodium tarball,尝试过安装并且有很多丢失的文件。不知道我是如何安装 Fluorine 的,因为我所做的只是下载并解压压缩包......
猜你喜欢
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
  • 2015-11-27
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
相关资源
最近更新 更多