Search code examples
gccwindows-7-x64mingw-w64strawberry-perlframa-c

trying to make frama-c work on Windows 7, using Perl or MinGW or

I want to use frama-c for static C code analysis. It already took me some effort to install it (hopefully) properly. The files are located at C:\CodeAnalysis\frama-c. I want to apply it via Windows console, e.g.:

C:\CodeAnalysis\frama-c\bin\frama-c hello.c

hello.c is just a simple hello-world-program (I am no C programmer btw and a newbie in programming)

#include <stdio.h>

main()
{
 printf("Hello World \n");
}

So when running the above command there is the following output:

[kernel] preprocessing with "gcc -C -E -I. hello.c"
C:/Strawberry/c/x86_64-w64-mingw32/include/stdio.h:141:[kernel] user error: syntax error
[kernel] user error: skipping file "hello.c" that has errors.
[kernel] Frama-C aborted: invalid user input

Yes, I have Perl installed but have no idea why Frama uses it. To me it seems that there is somehow something wrong with the stdio.h. Can this be? But I can compile my program successfully.

C:\Strawberry\c\bin\gcc hello.c produces a nicely working exe file.

When removing the include statement from the file, there is the following output:

[kernel] preprocessing with "gcc -C -E I. hello.c"
hello.c:5:[kernel] warning: Calling undeclared function printf. Old style K&R code?

So frama itself does work and this is the kind of output I expected to have.

I also have MinGW installed and tried to make Frama use this for compiling. So I removed the Strawberry entries in my Windows Path. After that calling frama-c produces the same output.

When completely uninstalling Strawberry Perl, frama doesn't work (stating gcc is an unknown command), although C:\MinGW\mingw64\bin is also added to my Windows Path, even as very first entry.

C:\MinGW\mingw64\bin\gcc hello.c works, gcc hello.c doesn't.

When Perl is installed gcc hello.c works, even when I delete the Strawberry parts from the Windows Path variable. Wtf?

How can I make things work properly?

Solution

  • There are several issues here, and we have to isolate them in order to fix things.

    1. Strawberry Perl installs its own gcc (based on MinGW), binutils, C headers, etc., by default on directory C:\Strawberry\c\bin. It adds this directory (among others) to the Windows Path variable. Frama-C expects gcc to be in the path, and it is Windows who decides which gcc to choose, if there are several directories in the path which contain a gcc binary. This is why Frama-C seems to use it.

    2. One common mistake (not Windows-specific, but which happens more often in Windows due to the nature of its graphical applications) is to modify environment variables and forget to restart the processes which still have old copies of them (such as Command Prompt). echo %path% should confirm which directories are present in the path for the current command prompt, if there are any doubts about its value.

    3. In case echo %path% contains the expected value, this is what might have happened (unfortunately I cannot reproduce your configuration to test it thoroughly): during installation of Frama-C, it may use the settings present during installation time to choose which directory contains gcc (in your case, C:\Strawberry\c\bin) and later hardcode this directory in its scripts.

      This could explain why, after uninstalling Strawberry Perl, even if another gcc was in the path, it was not considered by Frama-C. Ideally, reinstalling Frama-C with a single gcc in the path could allow it to find the right version this time. Note that this is just a hypothesis, I may be completely wrong here.

      In any case, the major problem you're having is not with gcc itself, but with the headers included with Strawberry Perl, as explained in the next item.

    4. Concerning the error message:

      C:/Strawberry/c/x86_64-w64-mingw32/include/stdio.h:141:[kernel] user error: syntax error
[kernel] user error: skipping file "hello.c" that has errors.

      It is indeed not extremely informative and might change in future versions, but it does point to the source line which causes the error (file stdio.h, line 141):

      int __cdecl __mingw_vsscanf (const char * __restrict__ _Str,
    const char * __restrict__ Format,va_list argp);

      In particular, it seems that __restrict__ is the source of the error here (Frama-C Sodium accepts restrict and __restrict, but not __restrict__; this may change in future versions).

      Unfortunately, even fixing this (by adding e.g. #define __restrict__ restrict before #include <stdio.h> in your file) does not guarantee that the rest of the file will be parsed, since it seems to be a Windows-specific, C++-prone header that likely contains other C definitions/extensions that are not in the C99 standard, and possibly not accepted by Frama-C.

    The best solution would be to ensure Frama-C uses its own stdio.h header, instead of Strawberry Perl's. It is usually installed in share/frama-c/libc (that is, it could be in C:\CodeAnalysis\frama-c\share\frama-c\libc in your installation), but depending on your configuration the headers might not have been found during execution, and Strawberry Perl's headers were included instead.

    A quick hack for this specific case might be replacing:

    #include <stdio.h>

    with:

    #include "C:\CodeAnalysis\frama-c\share\frama-c\libc\stdio.h"

    But it is far from ideal and likely to lead to other errors.

    If you manage to find out how to prevent Strawberry Perl's headers from being included, and ensure Frama-C's header files are included instead, you should be able to run Frama-C.

    Note about Cygwin/MinGW path issues

    I've had some issues when using a MinGW compiler and a Cygwin build (which is not necessarily a good idea), so here are some quick instructions on how to build Frama-C Sodium with a MinGW-based OCaml compiler using a Cygwin shell (but not a Cygwin-based OCaml compiler), in case it might help someone:

    1. When running ./configure, you'll need to specify a --prefix using a Windows-based path instead of a Cygwin-based one, such as:

      ./configure --prefix="C:/CodeAnalysis/build"

      If you don't, when running Frama-C (after make/make install) it will fail to find the libc/__fc_builtin_for_normalization.i file because it will try to use the Cygwin-based path, which will not work with the MinGW-based OCaml compiler.

      Note that you cannot use backslashes (\) when specifying the prefix path, since they will not be correctly converted later.

    2. I had to use the following command to ensure the makefile worked correctly:

      make FRAMAC_TOP_SRCDIR="$(cygpath -a -m $PWD)"

      Again, this is due to Cygwin paths not being recognized by the MinGW compiler (in particular, the absolute paths used by the plug-ins).

    3. The previous steps are sufficient to compile and run Frama-C (plus the GUI, if you have lablgtk and other dependencies installed). However, there are still some issues, e.g. absolute Windows filenames are not always handled correctly. This can often be avoided by specifying the file names directly in the command line with relative paths (e.g. frama-c-gui -val hello.c), but in the general case, MinGW+Cygwin is not a very robust combination and other issues may arise.

    Overall, mixing Cygwin and MinGW is not a good idea due to path issues, but it is nevertheless possible to compile and run Frama-C in such conditions.