尝试使用 Perl 或 MinGW 使 frama-c 在 Windows 7 上工作或

Question

我想使用 frama-c 进行静态 C 代码分析。我已经花了一些精力来正确安装它（希望如此）。这些文件位于C:\CodeAnalysis\frama-c。我想通过 Windows 控制台应用它，例如：

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

hello.c 只是一个简单的 hello-world-program（顺便说一句，我不是 C 程序员，也是编程新手）

#include <stdio.h>

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

所以当运行上面的命令有如下输出：

[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

是的，我已经安装了 Perl，但不知道 Frama 为何使用它。在我看来，stdio.h 似乎有些问题。这可以吗？但是我可以成功编译我的程序。

C:\Strawberry\c\bin\gcc hello.c 生成一个运行良好的 exe 文件。

当从文件中删除include语句时，有如下输出：

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

所以框架本身确实有效，这是我期望的输出。

我也安装了 MinGW 并试图让 Frama 使用它进行编译。所以我删除了 Windows 路径中的草莓条目。之后调用 frama-c 会产生相同的输出。

当完全卸载 Strawberry Perl 时，frama 不起作用（说明 gcc 是一个未知命令），尽管 C:\MinGW\mingw64\bin 也被添加到我的 Windows 路径中，即使是第一个条目。

C:\MinGW\mingw64\bin\gcc hello.c 有效，gcc hello.c 无效。

安装 Perl 后，gcc hello.c 可以工作，即使我从 Windows 路径变量中删除了草莓部分。怎么回事？

我怎样才能让事情正常工作？

Answer 1

这里有几个问题，我们必须隔离它们才能解决问题。

1. Strawberry Perl 默认在目录C:\Strawberry\c\bin 上安装自己的 gcc（基于 MinGW）、binutils、C 头文件等。它将这个目录（以及其他目录）添加到 Windows Path 变量中。 Frama-C 期望 gcc 在路径中，如果路径中有多个目录包含 gcc 二进制文件，则由 Windows 决定选择哪个 gcc。这就是 Frama-C 似乎使用它的原因。

2. 一个常见的错误（不是特定于 Windows，但由于其图形应用程序的性质而在 Windows 中更常见）是修改环境变量并忘记重新启动仍然有旧副本的进程（例如命令提示符）。 echo %path% 应该确认当前命令提示符的路径中存在哪些目录，如果对其值有任何疑问。

3. 如果echo %path% 包含预期值，这就是可能发生的情况（不幸的是，我无法重现您的配置以彻底测试它）：在安装 Frama-C 期间，它可能会使用安装期间存在的设置是时候选择哪个目录包含 gcc（在您的情况下为 C:\Strawberry\c\bin），然后在其脚本中对该目录进行硬编码。

   这可以解释为什么在卸载 Strawberry Perl 后，即使路径中有另一个 gcc，Frama-C 也不会考虑它。理想情况下，在路径中使用单个 gcc 重新安装 Frama-C 可以让它这次找到正确的版本。请注意，这只是一个假设，我可能完全错了。

   无论如何，您遇到的主要问题不在于 gcc 本身，而在于 Strawberry Perl 中包含的标头，如下一项所述。

4. 关于错误信息：

   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.
   

   它确实不是非常有用，并且可能在未来的版本中发生变化，但它确实指向导致错误的源代码行（文件stdio.h，第 141 行）：

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

   特别是，__restrict__ 似乎是此处错误的根源（Frama-C Sodium 接受 restrict 和 __restrict，但不接受 __restrict__；这可能会在未来的版本中改变）。

   不幸的是，即使修复此问题（通过在文件中的 #include <stdio.h> 之前添加例如 #define __restrict__ restrict）也不能保证文件的其余部分将被解析，因为它似乎是 Windows 特定的、易于 C++ 的标头可能包含其他 C 定义/扩展，这些定义/扩展不在 C99 标准中，并且可能不被 Frama-C 接受。

最好的解决方案是确保 Frama-C 使用自己的 stdio.h 标头，而不是 Strawberry Perl 的标头。它通常安装在 share/frama-c/libc 中（也就是说，它可能在您的安装中位于 C:\CodeAnalysis\frama-c\share\frama-c\libc 中），但根据您的配置，可能在执行期间找不到标头，而是包含了 Strawberry Perl 的标头。

这个特定案例的快速破解可能会替换：

#include <stdio.h>

与：

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

但这远非理想，可能会导致其他错误。

如果您设法找出如何防止 Strawberry Perl 的头文件被包含，并确保 Frama-C 的头文件被包含在内，您应该能够运行 Frama-C。

关于 Cygwin/MinGW 路径问题的注意事项

我在使用 MinGW 编译器和 Cygwin 构建时遇到了一些问题（这不一定是一个好主意），所以这里有一些关于如何使用基于 MinGW 的 OCaml 编译器构建 Frama-C Sodium 的快速说明一个 Cygwin shell（但不是一个基于 Cygwin 的 OCaml 编译器），以防它可能对某人有所帮助：

1. 运行./configure 时，您需要使用基于Windows 的路径而不是基于Cygwin 的路径指定--prefix，例如：

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

   如果你不这样做，在运行 Frama-C 时（在 make/make install 之后）它将无法找到 libc/__fc_builtin_for_normalization.i 文件，因为它会尝试使用基于 Cygwin 的路径，这不适用于 MinGW-基于 OCaml 的编译器。

   请注意，在指定前缀路径时不能使用反斜杠 (\)，因为它们以后不会被正确转换。

2. 我必须使用以下命令来确保 makefile 正常工作：

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

   同样，这是由于 MinGW 编译器无法识别 Cygwin 路径（特别是插件使用的绝对路径）。

3. 前面的步骤足以编译和运行 Frama-C（加上 GUI，如果您安装了 lablgtk 和其他依赖项）。但是，仍然存在一些问题，例如绝对 Windows 文件名并不总是正确处理。这通常可以通过直接在命令行中使用相对路径指定文件名来避免（例如frama-c-gui -val hello.c），但在一般情况下，MinGW+Cygwin 不是一个非常强大的组合，可能会出现其他问题。

总体而言，由于路径问题，混合 Cygwin 和 MinGW 并不是一个好主意，但仍然可以在这种情况下编译和运行 Frama-C。