slice - 切片时将多个参数传递给 C 文件

Question

我的源代码 ac 中的主要方法接受 2 个参数：一个是文件名，另一个是整数。我像这样运行它：

      ./a.out filename1.txt 3

但是当我尝试使用带有 frama-c 的切片时

       frama-c a.c filename1.txt 3 -slice-......

Framac 抛出一个错误，说它找不到文件 3 ???

当我输入 filename1.txt_3 并在代码中分别提取它们时，我还尝试了其他选项，但即便如此，frama-c 也不喜欢它。它抱怨它找不到文件filename1.txt_3。

请让我知道如何在运行 Frama C 时向源发送多个参数

score 1 · Accepted Answer

如果您分析的程序需要命令行参数，您通常需要编写一个函数void来构建参数argc并将argv它们传递给main()分析程序的函数：

int analysis_main(void) {
  char *argv[] = { "myprogram", "filename1.txt", "3", 0 };
  return main(3, argv);
}

请注意，如果目标是使用 "filename1.txt" 作为打开fopen()和读取文件的名称fread()，并且如果文件的内容与程序的行为相关，则最好提供实现这两个函数在调用时返回所需的结果。

相反，如果分析的程序要做的第一件事是传递argv[2]给strtol()，您可能希望务实地简化程序的那一部分，而不是为提供实现strtol()，对其进行分析只会在不需要的情况下引入复杂性。

1 回答 1