Frama-C验证问题：临时变量换直接数组访问致不变量无法保持

问题背景 #

使用Frama-C 25.0（Manganese）版本验证计数排序代码，搭配Z3 4.8.6 prover，执行命令：
frama-c -wp -wp-prover Alt-Ergo,Z3 -wp-print -wp-timeout 10 _count_sort.c > output.txt

验证过程中出现以下差异结果：

• 当代码使用临时变量tmp统计元素个数时，内层循环第39行的不变量可成功验证；
• 移除tmp直接使用count[number]统计后，该不变量的保持性验证超时；
• 外层循环第28行的不变量在两种实现版本中均无法完成保持性验证。

assigns精度的关联分析 #

该现象确实与assigns子句的精度直接相关：
Frama-C的WP插件依赖assigns子句界定代码对内存的修改范围。如果assigns过于宽泛（例如assigns \everything;），prover需要处理大量无关的内存状态可能性，大幅增加推理复杂度，进而导致超时或验证失败。

直接修改count[number]时，若未精确指定assigns的目标范围（仅笼统声明修改整个count数组），prover会默认整个数组的所有元素都可能被修改，需要遍历更多状态组合，这就是移除tmp后验证超时的核心原因。而使用tmp时，assigns只需指向单个临时变量，prover的推理范围被大幅缩小，验证效率更高。

程序修改与验证建议 #

1. 精确化assigns子句 #

• 内层循环：若直接修改count[number]，需明确指定assigns count[number];（若元素范围固定，可进一步细化为assigns count[0..MAX_VAL];，其中MAX_VAL是排序元素的最大值），避免prover处理整个数组的无关状态；
• 外层循环：精确指定assigns到output数组的对应修改位置（例如assigns output[\at(i, LoopEntry)..\at(i, Current)];），缩小推理范围。

2. 细化不变量与添加辅助断言 #

• 外层循环第28行的不变量：拆分出更细的辅助不变量，例如跟踪当前已处理的元素总数、count数组的累计值与output数组填充进度的对应关系，帮助prover逐步完成推理；
• 内层循环：补充关于count[number]的中间状态断言，例如//@ assert count[number] == \old(count[number]) + 1;，为prover提供明确的推理步骤，减少自动推导的负担；
• 变量范围约束：给number变量添加范围假设（例如//@ assume number >= 0 && number <= MAX_VAL;），缩小prover的搜索空间。

3. 优化循环结构 #

确保循环变量的边界清晰，避免模糊的范围定义。例如将内层循环的遍历范围明确限定在输入数组的有效索引内，减少prover需要处理的无效状态。

原代码与验证输出 #

原代码 #

// 此处为原计数排序代码

原验证输出 #

// 此处为原验证输出内容

内容的提问来源于stack exchange，提问作者Shark