您是否有机会使用来自 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 pp。 frama-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 尝试查看预处理的输入文件。