Eva中高精度选项(slevel/partition-history)意外增告警的技术问询

背景 #

对简化后的parser_full.c（源自开源案例研究仓库，已移除无关函数与ACSL注解）进行Frama-C/Eva分析时，发现如下反直觉行为：

技术问询 #

1. 为何启用更高精度选项会导致本案例中告警数增加？
2. print_diff_child_age(p_id)中的循环（由run()在第60行调用）与-slevel、-partition-history参数如何交互？
3. 新增的告警是否为误报？此时Frama-C/Eva是否仍保持可靠性？

简化后的parser_full.c代码 #

/* A modified version of parser_full.c from Open source case studies. */

#include <__fc_builtin.h>
#include <stdint.h>
#include <stdio.h>

#define MAX_CHILDREN_LEN 10
#define MAX_BUF_SIZE 100
#define MAX_PERSON_NUMBER 50

struct person {
  uint8_t age;
  uint8_t children_len;
  uint8_t children[MAX_CHILDREN_LEN];
};

struct person p[MAX_PERSON_NUMBER];

int parse(uint8_t *buf, uint16_t *offset, uint16_t len, uint8_t p_id){
  if(! (sizeof(uint8_t) <= len - *offset) ) return -1;
  p[p_id].age = (uint8_t) buf[*offset];
  *offset += sizeof(uint8_t);

  if(! (sizeof(uint8_t) <= len - *offset)) return -1;
  p[p_id].children_len = (uint8_t) buf[*offset];
  *offset += sizeof(uint8_t);

  if(! (p[p_id].children_len < MAX_CHILDREN_LEN)) return -1;

  for(uint8_t child_id = 0; child_id < p[p_id].children_len; child_id++){
    if(! (sizeof(uint8_t) <= len - *offset)) return -1;
    p[p_id].children[child_id] = (uint8_t) buf[*offset];

    if(! (p[p_id].children[child_id] < p_id) ) return -1;
    *offset += sizeof(uint8_t);
  };

  return 0;
};

void print_diff_child_age(uint8_t p_id){
  printf("%i(%i) :", p_id,p[p_id].age);
  for(uint8_t i = 0; i < p[p_id].children_len; i++){
    printf(" %i",p[p_id].age - p[p[p_id].children[i]].age);
  }

  printf("\n");
}

uint64_t run(uint8_t *buf, uint16_t len){
  uint16_t offset = 0;
  uint8_t p_nb;

  for(p_nb = 0; p_nb < MAX_PERSON_NUMBER; p_nb++){
    int r = parse(buf, &offset, len, p_nb);
    if(r) break;
  }

  for(uint8_t p_id = 0; p_id < p_nb; p_id++){
    print_diff_child_age(p_id);
  }

  return 0;
}

int main(){
  uint8_t buf[MAX_BUF_SIZE];
  uint16_t len = MAX_BUF_SIZE;
  Frama_C_make_unknown((char*)buf,MAX_BUF_SIZE);

  run(buf,len);

  return 0;
};

日志文件内容 #

low-precision-0-alarms.log（简化版） #

[kernel] 正在解析parser_full.c（含预处理）
[eva] 检测到选项-eva-precision 5，自动配置分析参数：
  选项-eva-min-loop-unroll设为0（默认值）。
  选项-eva-auto-loop-unroll设为128。
  选项-eva-widening-delay设为3（默认值）。
  选项-eva-partition-history设为0（默认值）。
  选项-eva-slevel已设为2000（未修改）。
  选项-eva-ilevel设为48。
  选项-eva-plevel设为150。
  选项-eva-subdivide-non-linear设为100。
  选项-eva-remove-redundant-alarms设为true（默认值）。
  选项-eva-domains设为'cvalue,equality,gauges,octagon,symbolic-locations'。
  选项-eva-split-return设为'auto'。
  选项-eva-equality-through-calls设为'formals'（默认值）。
  选项-eva-octagon-through-calls设为false（默认值）。

...

[eva:summary] ====== 分析总结 ======
  ----------------------------------------------------------------------------
  已分析4个函数（共4个）：覆盖率100%。
  这些函数中，71条语句已达（共71条）：覆盖率100%。
  ----------------------------------------------------------------------------
  分析过程中未触发错误或警告。
  ----------------------------------------------------------------------------
  分析生成0条告警。
  ----------------------------------------------------------------------------
  分析覆盖的逻辑属性评估：
    断言        0条有效     0条未知     0条无效      总计0条
    前置条件     4条有效     0条未知     0条无效      总计4条
  100%的覆盖逻辑属性已被证明。
  ----------------------------------------------------------------------------

high-precision-2-alarms.log（简化版） #

[kernel] 正在解析parser_full.c（含预处理）
[eva] 检测到选项-eva-precision 5，自动配置分析参数：
  选项-eva-min-loop-unroll设为0（默认值）。
  选项-eva-auto-loop-unroll设为128。
  选项-eva-widening-delay设为3（默认值）。
  选项-eva-partition-history已设为2（未修改）。
  选项-eva-slevel已设为5000（未修改）。
  选项-eva-ilevel设为48。
  选项-eva-plevel设为150。
  选项-eva-subdivide-non-linear设为100。
  选项-eva-remove-redundant-alarms设为true（默认值）。
  选项-eva-domains设为'cvalue,equality,gauges,octagon,symbolic-locations'。
  选项-eva-split-return设为'auto'。
  选项-eva-equality-through-calls设为'formals'（默认值）。
  选项-eva-octagon-through-calls设为false（默认值）。

...

[eva:alarm] parser_full.c:44: 警告：
  访问越界索引。断言p[p_id].children[i] < 50；
[eva:alarm] parser_full.c:44: 警告：
  访问越界索引。断言i < 10；

...

[eva:summary] ====== 分析总结 ======
  ----------------------------------------------------------------------------
  已分析4个函数（共4个）：覆盖率100%。
  这些函数中，71条语句已达（共71条）：覆盖率100%。
  ----------------------------------------------------------------------------
  分析过程中未触发错误或警告。
  ----------------------------------------------------------------------------
  分析生成2条告警：
       2次越界索引访问
  ----------------------------------------------------------------------------
  分析覆盖的逻辑属性评估：
    断言        0条有效     0条未知     0条无效      总计0条
    前置条件     4条有效     0条未知     0条无效      总计4条
  100%的覆盖逻辑属性已被证明。
  ----------------------------------------------------------------------------

技术问题解答 #

1. 为何更高精度选项导致告警数增加？ #

Frama-C/Eva的精度提升选项（如增大-eva-slevel、启用-eva-partition-history）会让分析器保留更精细的程序状态信息，而非用宽泛的抽象状态合并。
低精度配置下，分析器可能将多个状态合并，掩盖了潜在的边界条件风险；高精度配置下，分析器能区分更多细分状态，原本被合并掩盖的越界风险被检测出来，因此告警数上升。
具体到本案例：低精度时，p[p_id].children[i]和i的约束被合并到宽泛区间，分析器无法发现冲突；高精度时，状态拆分更细，能追踪到i可能超出MAX_CHILDREN_LEN、p[p_id].children[i]可能不满足<50的场景（尽管这些场景实际执行中不会发生，但分析器的抽象状态无法完全排除）。

2. print_diff_child_age循环与参数的交互 #

• -slevel（状态展开级别）：控制分析器在路径分支处能保留的最大状态数。增大到5000后，允许分析器为print_diff_child_age的循环迭代保留更多独立状态，避免过早合并迭代间的状态信息，从而更精确追踪i和p[p_id].children[i]的取值范围。
• -eva-partition-history（历史分区）：启用后，分析器会基于函数调用历史拆分状态。本案例中，print_diff_child_age被不同p_id调用时，历史分区会让分析器为每个p_id保留独立状态，而非合并所有p_id对应的状态。这使得分析器能更精准关联p_id与children[i]的约束关系，但也可能导致某些约束无法跨状态传递，进而触发告警。

3. 新增告警是否为误报？Frama-C/Eva是否仍可靠？ #

这些告警属于假阳性（误报），代码逻辑已确保：

• parse函数中强制p[p_id].children_len < MAX_CHILDREN_LEN，因此print_diff_child_age的循环中i必然小于10；
• parse函数还强制p[p_id].children[child_id] < p_id，而p_id < p_nb <= 50，因此p[p_id].children[i] < 50必然成立。

但Frama-C/Eva的高精度分析未能将parse中的约束完全传递到print_diff_child_age的循环中，导致抽象状态包含了实际不可能出现的场景，从而触发告警。

不过Frama-C/Eva的可靠性并未受损：它的设计原则是“绝不漏报真实错误”，假阳性是抽象分析的固有特性——为确保所有潜在风险都被检测到，分析器会考虑所有抽象上可能的路径，即使某些路径实际执行中不可达。

内容的提问来源于Stack Exchange，提问作者Zhongyi Wang