魔鬼在细节中，但这可能对你有用：
首先，获取Frama-C。如果您使用的是 Unix，您的发行版可能有一个包。该软件包不会是最后一个版本，但它可能已经足够好了，如果您以这种方式安装它，它将为您节省一些时间。
假设您的示例如下所示，只是大得多以至于不明显是什么问题：
int add(int x, int y)
{
static int state;
int result = x + y + state; // I tested it once and it worked.
state++;
return result;
}
键入如下命令：
frama-c -lib-entry -main add -deps ugly.c
选项-lib-entry -main add 的意思是“查看函数add”。选项-deps 计算函数依赖关系。你会在日志中找到这些“功能依赖”：
[from] Function add:
state FROM state; (and default:false)
\result FROM x; y; state; (and default:false)
这列出了add 的结果所依赖的实际 输入，以及根据这些输入计算的实际 输出，包括读取和修改的静态变量。在使用之前正确初始化的静态变量通常不会作为输入出现，除非分析器无法确定它总是在被读取之前被初始化。
日志将state 显示为\result 的依赖项。如果您希望返回的结果仅取决于参数（意味着具有相同参数的两个调用产生相同的结果），这暗示这里可能有问题，变量state。
上述行中显示的另一个提示是该函数修改了state。
这可能有帮助，也可能没有。选项-lib-entry 意味着分析器不假定任何非常量静态变量在调用分析的函数时保持其值，因此这对于您的代码来说可能过于不精确。有很多方法可以解决这个问题，但您是否愿意花时间学习这些方法取决于您。
编辑：这是一个更复杂的例子：
void initialize_1(int *p)
{
*p = 0;
}
void initialize_2(int *p)
{
*p; // I made a mistake here.
}
int add(int x, int y)
{
static int state1;
static int state2;
initialize_1(&state1);
initialize_2(&state2);
// This is safe because I have initialized state1 and state2:
int result = x + y + state1 + state2;
state1++;
state2++;
return result;
}
在此示例中，相同的命令会产生结果：
[from] Function initialize_1:
state1 FROM p
[from] Function initialize_2:
[from] Function add:
state1 FROM \nothing
state2 FROM state2
\result FROM x; y; state2
您看到的initialize_2 是一个空的依赖项列表，这意味着该函数没有分配任何内容。我将通过显示一个明确的消息而不是一个空列表来使这个案例更清楚。如果您知道initialize_1、initialize_2 或add 中的任何一个函数应该做什么，您可以将此先验知识与分析结果进行比较，并发现initialize_2 和@987654342 有问题@。
第二次编辑：现在我的示例对initialize_1 显示了一些奇怪的东西，所以也许我应该解释一下。变量state1 取决于p，因为p 用于写入state1，如果p 不同，那么state1 的最终值将不同。这是最后一个例子：
int t[10];
void initialize_index(int i)
{
t[i] = 1;
}
int main(int argc, char **argv)
{
initialize_index(argv[1][0]-'0');
}
使用命令frama-c -deps t.c，为initialize_index 计算的依赖关系是：
[from] Function initialize_index:
t[0..9] FROM i (and SELF)
这意味着每个单元格都依赖于i（如果i 是该特定单元格的索引，则可以对其进行修改）。每个单元格也可以保留其值（如果i 表示另一个单元格）：这在最新版本中用(and SELF) 提及，在以前的版本中用更模糊的(and default:true) 表示。