Frama-C EVA分析中无法基于函数规约断言数组全域属性的问题

完全可以通过\forall构造在函数规约中对数组所有元素指定全域属性，无需逐个编写单元素断言，刚好适配你处理大规模数组的场景。

具体用法示例 #

假设你的burst_sample_adc函数用于读取ADC数据到数组中，可在函数规约的requires或ensures条款中使用\forall来定义数组元素的全域约束：

/* 假设数组长度由参数N指定，需根据实际场景调整 */
/*@ 
    requires N > 0;
    requires \valid(sample_buf + (0 .. N-1));
    // 前置条件：所有数组元素初始值在ADC合法范围（示例为0~4095）
    requires \forall integer i; 0 <= i < N ==> sample_buf[i] >= 0 && sample_buf[i] <= 4095;
    // 后置条件：采样完成后所有元素仍保持合法范围
    ensures \forall integer i; 0 <= i < N ==> sample_buf[i] >= 0 && sample_buf[i] <= 4095;
*/
void burst_sample_adc(int sample_buf[], int N);

分析验证 #

你使用的命令frama-c-gui -eva main.c -eva-use-spec burst_sample_adc会让EVA加载并应用该函数规约。分析过程中，EVA会自动检查\forall定义的全域属性：

• 若数组中存在元素违反规约中的值域约束，EVA会在GUI界面中标记对应的告警
• 无需手动为每个数组元素单独编写断言，大幅减少冗余代码

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