frama-c mingw __restrict__ 关键字

我是 Frama-C 的新手。我想在Windows环境下运行它。我的编译器是gcc，mingw。

我尝试运行价值分析教程中的相同示例，因为我对库头文件有问题。

我发现无法运行 frama-c 因为restrict关键词。它显示 string.h 文件中的错误

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

当我手动添加#define时restrictSkeinProject 中的所有 *.c 文件

schneier.com/code/skein_NIST_CD_102610.zip

一切正常。手工完成并不是我想要的。

下一步是添加参数 -__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 文件，但错误仍然相同。

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.

我能用它做什么？

您的系统标头包含 Frama-C 不支持的非标准语法扩展。这是正常的，因为头文件通常作为编译器的完整包的一部分提供，因此头文件和编译器只需要一起工作，而不需要与所有其他以 C 源代码作为输入的程序一起工作。

一般来说，您应该始终使用 Frama-C 提供的标头 而不是您系统中的那些。

当使用 GCC 或兼容的编译器（例如 Clang）时，这涉及到 向预处理器传递选项-nostdinc and -I... where ...代表安装 Frama-C 接头的位置。这 可以使用以下选项从 Frama-C 获取位置-print-share-path.

总而言之，在 Unix 系统上，它可能看起来像：

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

使用 Windows 和 MinGW 做同样的事情遵循相同的想法，但有时会由于两者之间永久的模糊性而带来额外的麻烦。\ and /作为目录分隔符。

最近，Frank Dordowsky 在使用非常新的 GCC 版本为 Frama-C 预处理 C 文件时遇到了麻烦。那只是在使用时-pp-annot，但无论如何，解决方案是改用 Clang 作为预处理器。