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