如何在Frama-C/ACSL中验证二维及多维数组的有效性？

问题背景 #

需要验证一个操作n*m大小二维整数数组的C函数，一维数组的内存有效性验证注解（//@ requires \valid(arr + (0..n-1));）已知，但ACSL手册未提及二维数组的同类验证方法。尝试相关写法时，出现[kernel:annot-error]错误（提示意外token '['），原写法仅尝试检查连续内存块，未正确关联指针数组中的每个子数组。需解决：

• 如何让Frama-C正确识别int **matrix类型的二维数组
• 是否能在ACSL注解中直接使用matrix[i][j]的引用方式

用户提供的简化示例代码（example.c）如下：

/*@
  @ requires \valid(first) && \valid(last);
  @ requires (n>0) && (m>0);
  @ requires \valid(matrix + (0..n-1)*(0..m-1));
  @
  @ assigns *first, *last;
  @
  @ ensures first == matrix[0][0];
  @ ensures last == matrix[n-1][m-1];
  @*/

void matrix_elements(int **matrix, int n, int m, int *first, int *last)
{
    int felem = matrix[0][0];
    int lelem = matrix[n-1][m-1];

    *first = felem;
    *last = lelem;
}

使用环境：Frama-C 20.0（Calcium）、ACSL、Astraver，Ubuntu 22.04，执行命令：frama-c -av sample.c

解决方案 #

核心要点 #

int **matrix本质是指针数组（每个元素是指向一维int数组的指针），而非连续内存的二维数组，因此需要分两步验证内存有效性：

1. 验证指针数组matrix本身的n个指针是有效可访问的
2. 验证每个指针matrix[i]指向的一维数组包含m个有效int元素

修正后的ACSL注解 #

修正后的完整代码如下：

/*@
  @ requires \valid(first) && \valid(last);
  @ requires n > 0 && m > 0;
  @ // 验证指针数组matrix的n个指针有效
  @ requires \valid(matrix + (0..n-1));
  @ // 验证每个matrix[i]指向的数组包含m个有效int
  @ requires \forall integer i; 0 <= i < n ==> \valid(matrix[i] + (0..m-1));
  @
  @ assigns *first, *last;
  @
  @ // 注意：first是指针，需要解引用后比较
  @ ensures *first == matrix[0][0];
  @ ensures *last == matrix[n-1][m-1];
  @*/

void matrix_elements(int **matrix, int n, int m, int *first, int *last)
{
    int felem = matrix[0][0];
    int lelem = matrix[n-1][m-1];

    *first = felem;
    *last = lelem;
}

关键修正说明 #

• 内存验证：用\valid(matrix + (0..n-1))确保指针数组本身有效，再用\forall量词遍历每个指针，验证其指向的子数组有效
• 断言修正：原ensures中的first == matrix[0][0]错误，因为first是指针，需改为*first == matrix[0][0]（解引用后比较值）
• 语法合规：ACSL支持直接使用matrix[i][j]的引用方式，前提是已通过注解保证对应的内存有效性

验证执行 #

在终端执行以下命令即可正常验证：

frama-c -av example.c

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