我需要调试一个丑陋而庞大的数学C库，可能是由f2c生成的。代码正在滥用本地静态变量，不幸的是，在某些地方，它似乎利用了这样一个事实：这些变量被自动初始化为0。如果用同一个输入调用它的entry函数两次，它将给出不同的结果。如果卸载库并重新加载它，它将正常工作。它需要快一点，所以我想摆脱装载/卸载。
我的问题是，如何用valgrind或任何其他工具发现这些错误，而不必手动遍历整个代码。
我正在寻找局部静态变量被声明、先读、后写的地方。这个问题甚至更加复杂，因为静态变量有时通过指针传递得更远（是的，这太难看了）。
我理解有人会说，这样的错误不应该被自动工具发现，因为在某些情况下，这正是预期的行为。不过，有没有办法让自动初始化的局部静态变量变“脏”？
最佳答案
细节是魔鬼，但这可能对你有用：
首先，得到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
选项意味着“查看函数”。Option
-lib-entry -main add计算功能依赖项。您可以在日志中找到这些“功能依赖项”：[from] Function add:
state FROM state; (and default:false)
\result FROM x; y; state; (and default:false)
它列出了
add结果所依赖的实际输入，以及根据这些输入计算的实际输出，包括从中读取和修改的静态变量。在使用之前正确初始化的静态变量通常不会显示为输入，除非分析器无法确定它总是在被读取之前初始化的。日志显示
-deps依赖于add。如果您希望返回的结果只依赖于参数（意味着两个具有相同参数的调用会产生相同的结果），这就暗示了变量state可能有问题。上面几行中显示的另一个提示是，函数修改
\result。这可能有帮助也可能没有。选项
state意味着分析器不会假设任何非常量静态变量在调用分析中的函数时保留了其值，因此这对代码来说可能太不精确。有很多方法可以解决这个问题，但是你是否愿意花时间去学习这些方法就取决于你了。编辑：下面是一个更复杂的例子：
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
您在
state中看到的是一个空的依赖项列表，这意味着函数不赋值。我将通过显示一条显式消息而不仅仅是一个空列表来更清楚地说明这个问题。如果您知道任何函数-lib-entry、initialize_2或initialize_1应该做什么，那么您可以将这一先验知识与分析结果进行比较，发现initialize_2和add有问题。第二次编辑：现在我的例子显示了一些奇怪的
initialize_2，所以也许我应该解释一下。变量add依赖于initialize_1，即state1用于写入p，如果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');
}
使用命令
p，为state1计算的依赖项为：[from] Function initialize_index:
t[0..9] FROM i (and SELF)
这意味着每个单元格都依赖于
frama-c -deps t.c（如果initialize_index是特定单元格的索引，则可以对其进行修改）。每个单元格也可以保留其值（如果i表示另一个单元格）：在最新版本中用i表示，在以前的版本中用更模糊的i表示。