2

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

我已经尝试从价值分析教程中运行相同的示例，因为我遇到了库头文件的问题。

我发现由于限制关键字而无法运行 frama-c 。它在 string.h 文件中显示错误

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

当我手动将 #define限制添加到 SkeinProject 中的所有 *.c 文件时

schneier.com/code/skein_NIST_CD_102610.zip

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

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

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.

我能用它做什么？

4

1 回答 1

1

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

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

当使用 GCC 或诸如 Clang 之类的兼容编译器时，这涉及将选项传递给预处理器，-nostdinc并且-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 做同样的事情遵循相同的想法，但有时会因为目录分隔符之间的永久模糊性\而涉及额外的麻烦。/

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

于 2014-04-18T20:54:39.437 回答