frama-c mingw __restrict__ keyword

Question

I am new to Frama-C. I would like to run it under Windows enviroments. My compiler is gcc,mingw.

I have tryied to run same examples from Value Analysis tutorial by I have a problem with library header files.

I've found that it's not possible to run frama-c because restrict keyword. It shows error in string.h file

  void * __cdecl memcpy(void * __restrict__ _Dst,const void * __restrict__ _Src,size_t _Size) __MINGW_ATTRIB_DEPRECATED_SEC_WARN;

When I manually add #define restrict to all *.c files in SkeinProject

schneier.com/code/skein_NIST_CD_102610.zip

everything works correcly. By doing it by hand is not what I'm looking for.

Next step was to add argument -D__restrict__

frama-c -cpp-extra-args=-D__restrict__ -main=Init -val SHA3api_ref.c

[kernel] preprocessing with "gcc -C -E -I. -D__restrict__ SHA3api_ref.c"
../lib/gcc/i686-w64-mingw32/4.7.2/../../../../i686-w64-mingw32/include/string.h:41:[kernel] user error: syntax error
[kernel] user error: skipping file "SHA3api_ref.c" that has errors.
[kernel] Frama-C aborted because of an invalid user input.

I've also generated precompiled *.i files but error still the same.

gcc -E -D__restrict__ SHA3api_ref.c >SHA3api_ref.i

frama-c -main=Init -val SHA3api_ref.i

../lib/gcc/i686-w64-mingw32/4.7.2/../../../../i686-w64-mingw32/include/string.h:41:[kernel] user error: syntax error
[kernel] user error: skipping file "SHA3api_ref.i" that has errors.
[kernel] Frama-C aborted because of an invalid user input.

What can I do with it?

Answer 1

Your system headers contain non-standard syntax extensions that are not supported by Frama-C. This is normal, as the headers are often provided as part of a complete package with the compiler, so the headers and the compiler only need to work together, not to work with all the other programs that take C source code as input.

Generally speaking, you should always use the headers provided with Frama-C instead of those from your system.

When using GCC or a compatible compiler such as Clang, this involves passing the pre-processor the options -nostdinc and -I... where ... stands for the place where Frama-C's headers were installed. This location can be obtained from Frama-C with the option -print-share-path.

All in all, on a Unix system, it may look like:

frama-c -cpp-extra-args=-nostdinc -cpp-extra-args=-I`frama-c -print-share-path`/libc .....

Doing the same thing with Windows and MinGW follows the same idea but sometimes involves extra trouble due to the perpetual ambiguity between \ and / as directory separators.

Recently, Frank Dordowsky has been having trouble with using a very new GCC version to pre-process C files for Frama-C. That was only when using -pp-annot, but in any case, the solution was to switch to Clang as pre-processor.