Frama-C syntax error?

Question

I have an entry point that I want to run pdg-dot on, however after I moved the header files to be in the right place I get this syntax error.

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

In the source code that line is just a GdkPixmap declaration. How do I get Frama-C to create my .dot file now?

This is my command and the output:

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.

It should just be running through my function and creating the .dot file. I've tried just commenting the line out and I still get the same syntax error somehow.

You''ll need to post something more than a vague description please. stackoverflow.com/help/mcve — Weather Vane
@DanielTrebbien This is line 77: GdkPixmap *pixmap; Everything around it is also declarations inside of the struct gui_data. Sorry the formatting is off I'm new to posting on stackoverflow — Adam

Daniel Trebbien Daniel Trebbien · Accepted Answer · 2015-07-12T19:19:45

By any chance are you using gtkwin.c from PuTTY for Unix? Line 77 of PuTTY's gtkwin.c is also GdkPixmap *pixmap;.

You might be seeing "user error: syntax error" because the C file is not fully preprocessed, or there might be some syntax that Frama-C does not recognize. For example, when I try the following command on 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

(Note that I had to comment out #include <gdk/gdkx.h> because my GTK+ build uses the quartz backend rather than the X11 backend.)

I get:

[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.

In the frama-c command above, I added -kernel-msg-key pp. This option to frama-c allows you to see the preprocessing command that the kernel used. With -kernel-msg-key pp, you should see something like the following in the frama-c output:

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

Run the command listed in quotes and redirect the preprocessed output to a temporary file. Using the line number information added by the preprocessor, you will need to find the corresponding line in the preprocessed output. In my case, line 124 of /usr/include/sys/qos.h corresponded to line 9896 of the preprocessed output:

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;

I am probably seeing the "user error: syntax error" message because the __attribute__((availability(macosx,introduced=10.10))) syntax is not recognized. And in fact, once I added -D '__attribute__(...)=' to the CPP command to remove all attributes, I saw different errors:

/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?

I am using Frama-C Sodium-20150201.

TL;DR Try looking at the preprocessed input file.

Frama-C syntax error?

2 Answers